Changeset 850
 Timestamp:
 May 27, 2011, 12:58:34 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r849 r850 205 205 λA,P,H,x. match x with [ mk_Propify p ⇒ H p ]. 206 206 207 let rec foldli (A: Type[0]) (B: Type[0]) (f: Propify nat → A → B → A) (i: Propify nat) (a: A) (l: list B) on l ≝ 207 definition app ≝ 208 λA:Type[0].λl1:Propify (list A).λl2:list A. 209 match l1 with 210 [ mk_Propify l1 ⇒ mk_Propify … (l1@l2) ]. 211 212 lemma app_nil: ∀A,l1. app A l1 [ ] = l1. 213 #A * /3/ 214 qed. 215 216 lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3). 217 #A * #l1 normalize // 218 qed. 219 220 let rec foldli (A: Type[0]) (B: Propify (list A) → Type[0]) 221 (f: ∀prefix. B prefix → ∀x.B (app … prefix [x])) 222 (prefix: Propify (list A)) (b: B prefix) (l: list A) on l : 223 B (app … prefix l) ≝ 208 224 match l with 209 [ nil ⇒ a210  cons hd tl ⇒ foldli A B f (match i with [ mk_Propify i ⇒ mk_Propify … (S i)]) (f i a hd) tl225 [ nil ⇒ ? (* b *) 226  cons hd tl ⇒ ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*) 211 227 ]. 228 [ applyS b 229  <(app_assoc ?? [hd]) @(foldli A B f (app … prefix [hd]) (f prefix b hd) tl) ] 230 qed. 231 232 (* 233 let rec foldli (A: Type[0]) (B: list A → Type[0]) (f: ∀prefix. B prefix → ∀x. B (prefix@[x])) 234 (prefix: list A) (b: B prefix) (l: list A) on l : B (prefix@l) ≝ 235 match l with 236 [ nil ⇒ ? (* b *) 237  cons hd tl ⇒ 238 ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*) 239 ]. 240 [ applyS b 241  applyS (foldli A B f (prefix@[hd]) (f prefix b hd) tl) ] 242 qed. 243 *) 244 245 definition foldll: 246 ∀A:Type[0].∀B: Propify (list A) → Type[0]. 247 (∀prefix. B prefix → ∀x. B (app … prefix [x])) → 248 B (mk_Propify … []) → ∀l: list A. B (mk_Propify … l) 249 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]). 250 251 definition build_maps' ≝ 252 λpseudo_program. 253 let 〈preamble,instr_list〉 ≝ pseudo_program in 254 let result ≝ 255 foldl 256 (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))). 257 ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧ 258 tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t))) 259 (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix. 260 let instr_list_prefix' ≝ instr_list_prefix @ [i] in 261 is_prefix ? instr_list_prefix' instr_list → 262 tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?) 263 (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))). 264 ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧ 265 tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)). 266 λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix. 267 let instr_list_prefix' ≝ instr_list_prefix @ [i] in 268 is_prefix ? instr_list_prefix' instr_list → 269 tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? . 270 let 〈labels, pc_costs〉 ≝ t in 271 let 〈program_counter, costs〉 ≝ pc_costs in 272 let 〈label, i'〉 ≝ i in 273 let labels ≝ 274 match label with 275 [ None ⇒ labels 276  Some label ⇒ 277 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 278 insert ? ? label program_counter_bv labels 279 ] 280 in 281 match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with 282 [ None ⇒ 283 let dummy ≝ 〈labels,pc_costs〉 in 284 dummy 285  Some construct ⇒ 〈labels, construct〉 286 ] 287 ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*) 288 in 289 let 〈labels, pc_costs〉 ≝ result in 290 let 〈pc, costs〉 ≝ pc_costs in 291 〈labels, costs〉. 212 292 213 293 definition build_maps' ≝
Note: See TracChangeset
for help on using the changeset viewer.