Changeset 1075 for src/utilities/RegisterSet.ma

Timestamp:

Jul 18, 2011, 5:21:14 PM (10 years ago)

Author:

mulligan

Message:

nearly completed rtl -> ertl pass removing all option types with dep. types

File:

• src/utilities/RegisterSet.ma (modified) (2 diffs)

src/utilities/RegisterSet.ma

@@ -6 +6 @@
   rs_set: Type[0];
   rs_empty: rs_set;
-  rs_singleton: register → rs_set;
-  rs_fold: ∀A: Type[0]. (register → A → A) → rs_set → A → A;
-  rs_insert: register → rs_set → rs_set;
-  rs_exists: register → rs_set → bool;
+  rs_singleton: Register → rs_set;
+  rs_fold: ∀A: Type[0]. (Register → A → A) → rs_set → A → A;
+  rs_insert: Register → rs_set → rs_set;
+  rs_exists: Register → rs_set → bool;
   rs_union: rs_set → rs_set → rs_set;
-  rs_to_list: rs_set → list register;
-  rs_from_list: list register → rs_set
+  rs_to_list: rs_set → list Register;
+  rs_from_list: list Register → rs_set
 }.
 
 (* dpm: horrendously inefficient, but will do for now *)
 
-definition rs_list_set_empty: list register ≝ [ ].
+definition rs_list_set_empty: list Register ≝ [ ].
 
-definition rs_list_set_singleton: register → list register ≝ λr. [ r ].
+definition rs_list_set_singleton: Register → list Register ≝ λr. [ r ].
 
 definition rs_list_set_fold ≝
   λA: Type[0].
-  λf: register → A → A.
-  λl: list register.
+  λf: Register → A → A.
+  λl: list Register.
   λa: A.
     foldr ? ? f a l.
     
 definition rs_list_set_insert ≝
-  λr: register.
-  λs: list register.
-  match member ? (eq_identifier ?) r s with
+  λr: Register.
+  λs: list Register.
+  match member ? eq_Register r s with
   [ true ⇒ r :: s
   | false ⇒ s
@@ -37 +37 @@
   
 definition rs_list_set_exists ≝
-  λr: register.
-  λs: list register.
-    member ? (eq_identifier ?) r s.
+  λr: Register.
+  λs: list Register.
+    member ? eq_Register r s.
     
 definition rs_list_set_union ≝
-  λr: list register.
-  λs: list register.
-    nub_by ? (eq_identifier ?) (r @ s).
+  λr: list Register.
+  λs: list Register.
+    nub_by ? eq_Register (r @ s).
   
 definition rs_list_set_from_list ≝
-  λr: list register.
-    nub_by ? (eq_identifier ?) r.
+  λr: list Register.
+    nub_by ? eq_Register r.
   
 definition register_list_set: register_set ≝
-  mk_register_set (list register) rs_list_set_empty
+  mk_register_set (list Register) rs_list_set_empty
                   rs_list_set_singleton rs_list_set_fold
                   rs_list_set_insert rs_list_set_exists