Changeset 1050
 Timestamp:
 Jul 4, 2011, 10:43:37 AM (9 years ago)
 Location:
 src
 Files:

 2 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 ≝ 
src/utilities/HMap.ma
r1049 r1050 170 170 ]. 171 171 172 definition map_single_l_safe ≝ 173 λkey_type. 174 λelt_type. 175 λkey: key_type. 176 λelt: elt_type. 177 λleft: map key_type elt_type. 178 λright: map key_type elt_type. 179 λprf: map_not_nil_p key_type elt_type right. 180 match right return λx. map_not_nil_p key_type elt_type x → map key_type elt_type with 181 [ map_nil ⇒ λright_nil_absrd. ? 182  map_fork r_sz r_key r_elt r_l r_r ⇒ 183 λright_fork_prf. map_binsert ? ? r_key r_elt (map_binsert ? ? key elt left r_l) r_r 184 ] prf. 185 normalize in right_nil_absrd; 186 cases right_nil_absrd 187 qed. 188 172 189 definition map_single_r ≝ 173 190 λkey_type. … … 181 198  map_fork l_sz l_key l_elt l_l l_r ⇒ 182 199 Some ? (map_binsert ? ? l_key l_elt l_l (map_binsert ? ? key elt l_r right)) 200 ]. 201 202 definition map_single_r_safe ≝ 203 λkey_type. 204 λelt_type. 205 λkey: key_type. 206 λelt: elt_type. 207 λleft: map key_type elt_type. 208 λright: map key_type elt_type. 209 λprf: map_not_nil_p key_type elt_type left. 210 match left return λx. map_not_nil_p key_type elt_type x → map key_type elt_type with 211 [ map_nil ⇒ λleft_nil_absrd. ? 212  map_fork l_sz l_key l_elt l_l l_r ⇒ 213 λleft_fork_prf. map_binsert ? ? l_key l_elt l_l (map_binsert ? ? key elt l_r right) 214 ] prf. 215 normalize in left_nil_absrd; 216 cases left_nil_absrd 217 qed. 218 219 definition map_double_r_property_p ≝ 220 λkey_type. 221 λelt_type. 222 λleft: map key_type elt_type. 223 match left with 224 [ map_nil ⇒ False 225  map_fork l_sz l_key l_elt l_l l_r ⇒ 226 match l_r with 227 [ map_nil ⇒ False 228  _ ⇒ True 229 ] 183 230 ]. 184 231 … … 199 246 ] 200 247 ]. 248 249 definition map_double_r_safe ≝ 250 λkey_type. 251 λelt_type. 252 λkey: key_type. 253 λelt: elt_type. 254 λleft: map key_type elt_type. 255 λright: map key_type elt_type. 256 λprf: map_double_r_property_p key_type elt_type left. 257 match left return λx. map_double_r_property_p key_type elt_type x → map key_type elt_type with 258 [ map_nil ⇒ λleft_nil_absrd. ? 259  map_fork l_sz l_key l_elt l_l l_r ⇒ λouter_prf. 260 match l_r return λx. map_double_r_property_p key_type elt_type x → map key_type elt_type with 261 [ map_nil ⇒ λl_r_nil_absrd. ? 262  map_fork lr_sz lr_key lr_elt lr_l lr_r ⇒ 263 λl_r_fork_prf. map_binsert … lr_key lr_elt (map_binsert … l_key l_elt l_l lr_l) (map_binsert … key elt lr_r right) 264 ] ? 265 ] prf. 266 [1: normalize in left_nil_absrd; 267 cases left_nil_absrd; 268 3: normalize in l_r_nil_absrd; 269 cases l_r_nil_absrd; 270 2: normalize in outer_prf; 271 generalize in match outer_prf; 272 cases l_r; 273 [ normalize // 274  #SZ #KEY_TYPE #ELT_TYPE #LEFT #RIGHT 275 normalize 276 #HYP 277 ] 278 qed. 201 279 202 280 definition map_double_l ≝
Note: See TracChangeset
for help on using the changeset viewer.