Changeset 1050 for src/RTLabs

Timestamp:

Jul 4, 2011, 10:43:37 AM (10 years ago)

Author:

mulligan

Message:

adding dependent types to map datastructure to remove all option types. some changes to rtlabs to rtl translation pass.

File:

• src/RTLabs/RTLAbstoRTL.ma (modified) (2 diffs)

src/RTLabs/RTLAbstoRTL.ma

@@ -123 +123 @@
 
 definition initialize_local_env_internal ≝
-  λeq.
   λruniverse.
-  λptrs.
   λlenv.
   λr.
-    let fresh ≝ snd ? ? (fresh_reg runiverse) in
-    let rt ≝
-      match member ? eq r ptrs with
-      [ true  ⇒ register_ptr r fresh
-      | false ⇒ register_int r
-      ]
-    in
-    add_local_env ? ? 〈r, rt〉 lenv.
+  λt.
+  match size_of_sig_type t with
+  [ None ⇒ None ?
+  | Some size ⇒
+    let rs ≝ register_freshes runiverse size in
+      add_local_env r rs lenv
+  ].
 
 definition initialize_local_env ≝
@@ -141 +138 @@
   λptrs.
   λregisters.
-    foldl ? ? (initialize_local_env_internal (eq_identifier RegisterTag) runiverse ptrs) [ ] registers.
+  let registers ≝ registers @
+    match result with
+    [ None ⇒ [ ]
+    | Some rt ⇒ [ rt ]
+    ]
+  in
+    foldl ? ? (initialize_local_env_internal runiverse) [ ] registers.
+
+
+let initialize_local_env runiverse registers result =
+  let registers =
+    registers @ (match result with None -> [] | Some (r, t) -> [(r, t)]) in
+  let f lenv (r, t) =
+    let rs = register_freshes runiverse (size_of_sig_type t) in
+    add_local_env r rs lenv in
+  List.fold_left f Register.Map.empty registers
+  
+  
+definition map_list_local_env_internal ≝
+  λlenv.
+  λres.
+  λr.
+    res @ (find_local_env r lenv).
+    
+definition map_list_local_env ≝
+  λlenv.
+  λregs.
+  
+
+let map_list_local_env lenv regs =
+  let f res r = res @ (find_local_env r lenv) in
+  List.fold_left f [] regs
 
 definition filter_and_to_list_local_env_internal ≝