Changeset 1052 for src/RTLabs

Timestamp:

Jul 4, 2011, 3:31:18 PM (10 years ago)

Author:

mulligan

Message:

removed offsets after reading cerco mailing list

File:

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

src/RTLabs/RTLAbstoRTL.ma

@@ -102 +102 @@
       〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
 
+definition float_free_p ≝
+  λsig.
+  match sig with
+  [ ASTfloat _ ⇒ False
+  | _ ⇒ True
+  ].
+
 definition size_of_sig_type ≝
   λsig.
-  match sig with
+  λprf: float_free_p sig.
+  match sig return λx. float_free_p x → nat with
   [ ASTint isize sign ⇒
-    let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
-      Some ? (isize' ÷ (nat_of_bitvector ? int_size))
-  | ASTfloat _ ⇒ None ?
-  | ASToffset ⇒ Some ? (nat_of_bitvector ? int_size)
-  | ASTptr rgn ⇒ Some ? (nat_of_bitvector ? ptr_size)
-  ].
+    λast_int_prf.
+      let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
+        isize' ÷ (nat_of_bitvector ? int_size)
+  | ASTfloat _ ⇒
+    λast_float_prf. ?
+  | ASToffset ⇒
+    λast_offset_prf.
+      nat_of_bitvector ? int_size
+  | ASTptr rgn ⇒
+    λast_ptr_prf.
+      nat_of_bitvector ? ptr_size
+  ].
+  normalize in ast_float_prf;
+  cases ast_float_prf;
+qed.
 
 inductive register_type: Type[0] ≝
@@ -117 +134 @@
   | register_ptr: register → register → register_type.
 
-definition local_env ≝ map register (list register).
-definition mem_local_env ≝ map_member register (list register) register_ord.
-definition add_local_env ≝ map_insert register (list register) register_ord.
-definition find_local_env ≝ map_lookup register (list register) register_ord.
+definition local_env ≝ BitVectorTrie (list register).
+
+definition mem_local_env ≝
+  λr: register.
+  match r with
+  [ an_identifier w ⇒ member (list register) 16 w
+  ].
+
+definition add_local_env ≝
+  λr: register.
+  match r with
+  [ an_identifier w ⇒ insert (list register) 16 w
+  ].
+
+definition find_local_env ≝
+  λr: register.
+  λbvt.
+  match r with
+  [ an_identifier w ⇒ lookup (list register) 16 w bvt [ ]
+  ].
 
 definition initialize_local_env_internal ≝
@@ -131 +164 @@
   | Some size ⇒
     let rs ≝ register_freshes runiverse size in
-      add_local_env r rs lenv
+      Some ? (add_local_env r rs lenv)
   ].
 
@@ -144 +177 @@
     ]
   in
-    foldl ? ? (initialize_local_env_internal runiverse) [ ] registers.
-
+    foldl ? ? (
+      λbvt. λr.
+      match bvt with
+      [ None ⇒ None ?
+      | Some bvt' ⇒ initialize_local_env_internal runiverse bvt' r typ
+      ]) ? ?.
 
 let initialize_local_env runiverse registers result =
   let registers =
-    registers @ (match result with None -> [] | Some (r, t) -> [(r, t)]) in
+    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 ≝