Changeset 850 for src/ASM/AssemblyProof.ma

Timestamp:

May 27, 2011, 12:58:34 AM (10 years ago)

Author:

sacerdot

Message:

More informative foldl: foldll.

File:

• src/ASM/AssemblyProof.ma (modified) (1 diff)

src/ASM/AssemblyProof.ma

@@ -205 +205 @@
  λA,P,H,x. match x with [ mk_Propify p ⇒ H p ].
 
-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 ≝
+definition app ≝
+ λA:Type[0].λl1:Propify (list A).λl2:list A.
+  match l1 with
+   [ mk_Propify l1 ⇒ mk_Propify … (l1@l2) ].
+
+lemma app_nil: ∀A,l1. app A l1 [ ] = l1.
+ #A * /3/
+qed.
+
+lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3).
+ #A * #l1 normalize //
+qed. 
+
+let rec foldli (A: Type[0]) (B: Propify (list A) → Type[0])
+ (f: ∀prefix. B prefix → ∀x.B (app … prefix [x]))
+ (prefix: Propify (list A)) (b: B prefix) (l: list A) on l :
+ B (app … prefix l) ≝
   match l with
-  [ nil ⇒ a
-  | cons hd tl ⇒ foldli A B f (match i with [ mk_Propify i ⇒ mk_Propify … (S i)]) (f i a hd) tl
+  [ nil ⇒ ? (* b *)
+  | cons hd tl ⇒ ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
   ].
+ [ applyS b
+ | <(app_assoc ?? [hd]) @(foldli A B f (app … prefix [hd]) (f prefix b hd) tl) ]
+qed.
+
+(*
+let rec foldli (A: Type[0]) (B: list A → Type[0]) (f: ∀prefix. B prefix → ∀x. B (prefix@[x]))
+ (prefix: list A) (b: B prefix) (l: list A) on l : B (prefix@l) ≝
+  match l with
+  [ nil ⇒ ? (* b *)
+  | cons hd tl ⇒
+     ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
+  ].
+ [ applyS b
+ | applyS (foldli A B f (prefix@[hd]) (f prefix b hd) tl) ]
+qed.
+*)
+
+definition foldll:
+ ∀A:Type[0].∀B: Propify (list A) → Type[0].
+  (∀prefix. B prefix → ∀x. B (app … prefix [x])) →
+   B (mk_Propify … []) → ∀l: list A. B (mk_Propify … l)
+ ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
+
+definition build_maps' ≝
+  λpseudo_program.
+  let 〈preamble,instr_list〉 ≝ pseudo_program in
+  let result ≝
+   foldl
+    (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
+          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
+           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
+    (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
+          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
+           is_prefix ? instr_list_prefix' instr_list →
+           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
+    (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
+          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
+           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
+     λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
+          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
+           is_prefix ? instr_list_prefix' instr_list →
+           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
+      let 〈labels, pc_costs〉 ≝ t in
+      let 〈program_counter, costs〉 ≝ pc_costs in
+       let 〈label, i'〉 ≝ i in
+       let labels ≝
+         match label with
+         [ None ⇒ labels
+         | Some label ⇒
+           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
+             insert ? ? label program_counter_bv labels
+         ]
+       in
+         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
+         [ None ⇒
+            let dummy ≝ 〈labels,pc_costs〉 in
+              dummy
+         | Some construct ⇒ 〈labels, construct〉
+         ]
+    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)
+  in
+   let 〈labels, pc_costs〉 ≝ result in
+   let 〈pc, costs〉 ≝ pc_costs in
+    〈labels, costs〉.
 
 definition build_maps' ≝