Changeset 1211 for src/utilities

Timestamp:

Sep 14, 2011, 4:14:59 PM (8 years ago)

Author:

mulligan

Message:

fixed interference file

Location:

src/utilities

Files:

• Interference.ma (modified) (1 diff)
• adt/register_table.ma (modified) (1 diff)

src/utilities/Interference.ma

@@ -9 +9 @@
 include "utilities/adt/register_table.ma".
 
-definition vertex_set ≝ set_adt vertex vertex_ordered.
-definition vertex_priority_set ≝ priority_set_adt vertex vertex_ordered.
-definition Register_set ≝ set_adt Register Register_ordered.
+definition vertex_set ≝ set vertex.
+definition vertex_priority_set ≝ priority_set vertex.
+definition Register_set ≝ set Register.
 
-record graph
-  (set_impl: set_adt … Register Register_ordered): Type[1] ≝
+record graph: Type[1] ≝
 {
-  ig_reg_table  : register_table_adt set_impl;
-  ig_vertex_set : vertex_set;
-  ig_vertex_pset: vertex_priority_set;
-  ig_Reg_set    : Register_set;
-  ig_regmap     : register_table set_impl ig_reg_table;
-  ig_ivv        : set … ig_vertex_set vertex;
-  ig_ivh        : set … ig_Reg_set Register;
-  ig_pvv        : set … ig_vertex_set vertex;
-  ig_pvh        : set … ig_Reg_set Register;
-  ig_degree     : priority_set … ig_vertex_pset vertex;
-  ig_nmr        : priority_set … ig_vertex_pset vertex
+  ig_regmap     : register_table;
+  ig_ivv        : vertex_set;
+  ig_ivh        : Register_set;
+  ig_pvv        : vertex_set;
+  ig_pvh        : Register_set;
+  ig_degree     : vertex_priority_set;
+  ig_nmr        : vertex_priority_set
 }.
 
 definition ig_create ≝
-  λReg_set_impl: set_adt … Register Register_ordered.
-  λvertex_set_impl: set_adt … vertex vertex_ordered.
-  λvertex_priority_set_impl: priority_set_adt … vertex vertex_ordered.
-  λReg_table_impl: register_table_adt Reg_set_impl. 
   λregs.
   let 〈ignore_int, table'', priority''〉 ≝
     foldr … (λr. λv_table_priority'.
       let 〈v, table', priority'〉 ≝ v_table_priority' in
-      let table'' ≝ rt_add ? Reg_table_impl r v table' in
-      let priority'' ≝ ps_insert ? ? vertex_priority_set_impl v 0 priority' in
+      let table'' ≝ rt_add r v table' in
+      let priority'' ≝ ps_insert ? v 0 priority' in
         〈v + 1, table'', priority''〉) 〈0, rt_empty …, ps_empty …〉 regs
   in
-      mk_graph Reg_set_impl
-      Reg_table_impl vertex_set_impl vertex_priority_set_impl
-      Reg_set_impl table'' (set_empty …) (set_empty …) (set_empty …)
+      mk_graph table'' (set_empty …) (set_empty …) (set_empty …)
       (set_empty …) priority'' priority''.
 

src/utilities/adt/register_table.ma

@@ -20 +20 @@
 axiom rt_remove: vertex → register_table → register_table.
 
-axiom rt_fold: ∀a: Type[0]. (vertex → set … set_impl Register → a → a) →
-   register_table → a → a;
+axiom rt_fold: ∀a: Type[0]. (vertex → set Register → a → a) →
+   register_table → a → a.
 
 axiom rt_coalesce: vertex → vertex → register_table → register_table.