Changeset 850


Ignore:
Timestamp:
May 27, 2011, 12:58:34 AM (8 years ago)
Author:
sacerdot
Message:

More informative foldl: foldll.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r849 r850  
    205205 λA,P,H,x. match x with [ mk_Propify p ⇒ H p ].
    206206
    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 ≝
     207definition 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
     212lemma app_nil: ∀A,l1. app A l1 [ ] = l1.
     213 #A * /3/
     214qed.
     215
     216lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3).
     217 #A * #l1 normalize //
     218qed.
     219
     220let 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) ≝
    208224  match l with
    209   [ nil ⇒ a
    210   | cons hd tl ⇒ foldli A B f (match i with [ mk_Propify i ⇒ mk_Propify … (S i)]) (f i a hd) tl
     225  [ nil ⇒ ? (* b *)
     226  | cons hd tl ⇒ ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
    211227  ].
     228 [ applyS b
     229 | <(app_assoc ?? [hd]) @(foldli A B f (app … prefix [hd]) (f prefix b hd) tl) ]
     230qed.
     231
     232(*
     233let 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) ]
     242qed.
     243*)
     244
     245definition 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
     251definition 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〉.
    212292
    213293definition build_maps' ≝
Note: See TracChangeset for help on using the changeset viewer.