Changeset 1515 for src/RTLabs
- Timestamp:
- Nov 18, 2011, 1:03:14 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLabsToRTL.ma
r1408 r1515 59 59 | register_ptr: register → register → register_type. 60 60 61 definition local_env ≝ BitVectorTrie (list register) 16.61 definition local_env ≝ identifier_map RegisterTag (list register). 62 62 63 63 definition mem_local_env : register → local_env → bool ≝ 64 λr . member … (word_of_identifier … r).64 λr,e. member … e r. 65 65 66 66 definition add_local_env : register → list register → local_env → local_env ≝ 67 λr . insert … (word_of_identifier … r).67 λr,v,e. add … e r v. 68 68 69 69 definition find_local_env : register → local_env → list register ≝ 70 λr: register.λ bvt. lookup … (word_of_identifier … r) bvt[].70 λr: register.λenv. lookup_def … env r []. 71 71 72 72 definition initialize_local_env_internal ≝ … … 89 89 ] 90 90 in 91 foldl … initialize_local_env_internal 〈 Stub…,runiverse〉 registers.91 foldl … initialize_local_env_internal 〈empty_map …,runiverse〉 registers. 92 92 93 93 definition map_list_local_env_internal ≝
Note: See TracChangeset
for help on using the changeset viewer.