Changeset 1050 for src/RTLabs/RTLAbstoRTL.ma
 Timestamp:
 Jul 4, 2011, 10:43:37 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1049 r1050 123 123 124 124 definition initialize_local_env_internal ≝ 125 λeq.126 125 λruniverse. 127 λptrs.128 126 λlenv. 129 127 λr. 130 let fresh ≝ snd ? ? (fresh_reg runiverse) in 131 let rt ≝ 132 match member ? eq r ptrs with 133 [ true ⇒ register_ptr r fresh 134  false ⇒ register_int r 135 ] 136 in 137 add_local_env ? ? 〈r, rt〉 lenv. 128 λt. 129 match size_of_sig_type t with 130 [ None ⇒ None ? 131  Some size ⇒ 132 let rs ≝ register_freshes runiverse size in 133 add_local_env r rs lenv 134 ]. 138 135 139 136 definition initialize_local_env ≝ … … 141 138 λptrs. 142 139 λregisters. 143 foldl ? ? (initialize_local_env_internal (eq_identifier RegisterTag) runiverse ptrs) [ ] registers. 140 let registers ≝ registers @ 141 match result with 142 [ None ⇒ [ ] 143  Some rt ⇒ [ rt ] 144 ] 145 in 146 foldl ? ? (initialize_local_env_internal runiverse) [ ] registers. 147 148 149 let initialize_local_env runiverse registers result = 150 let registers = 151 registers @ (match result with None > []  Some (r, t) > [(r, t)]) in 152 let f lenv (r, t) = 153 let rs = register_freshes runiverse (size_of_sig_type t) in 154 add_local_env r rs lenv in 155 List.fold_left f Register.Map.empty registers 156 157 158 definition map_list_local_env_internal ≝ 159 λlenv. 160 λres. 161 λr. 162 res @ (find_local_env r lenv). 163 164 definition map_list_local_env ≝ 165 λlenv. 166 λregs. 167 168 169 let map_list_local_env lenv regs = 170 let f res r = res @ (find_local_env r lenv) in 171 List.fold_left f [] regs 144 172 145 173 definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset
for help on using the changeset viewer.