Changeset 1515 for src/RTLabs

Timestamp:

Nov 18, 2011, 1:03:14 PM (9 years ago)

Author:

campbell

Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

• fix interpretation for - on positives
• move eq_nat_dec to a more appropriate place
• split out costs from other identifiers in ASM
• use identifier abstractions in back-end

File:

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

src/RTLabs/RTLabsToRTL.ma

@@ -59 +59 @@
   | register_ptr: register → register → register_type.
 
-definition local_env ≝ BitVectorTrie (list register) 16.
+definition local_env ≝ identifier_map RegisterTag (list register).
 
 definition mem_local_env : register → local_env → bool ≝
-  λr. member … (word_of_identifier … r).
+  λr,e. member … e r.
 
 definition add_local_env : register → list register → local_env → local_env ≝
-  λr. insert … (word_of_identifier … r).
+  λr,v,e. add … e r v.
 
 definition find_local_env : register → local_env → list register ≝
-  λr: register.λbvt. lookup … (word_of_identifier … r) bvt [].
+  λr: register.λenv. lookup_def … env r [].
 
 definition initialize_local_env_internal ≝
@@ -89 +89 @@
     ]
   in
-    foldl … initialize_local_env_internal 〈Stub …,runiverse〉 registers.
+    foldl … initialize_local_env_internal 〈empty_map …,runiverse〉 registers.
 
 definition map_list_local_env_internal ≝