Changeset 697 for src/ASM

Ignore:
Timestamp:
Mar 18, 2011, 1:28:33 PM (9 years ago)
Message:

Merge Clight branch of vectors and friends.
Start making stuff build.

Location:
src/ASM
Files:
7 edited
1 copied

Unmodified
Removed
• src/ASM

• Property svn:mergeinfo set to (toggle deleted branches) /src/Clight/cerco merged eligible /Deliverables/D3.1/C-semantics/cerco 531-693 /Deliverables/D4.1/Matita/new-matita-development 476-530
• src/ASM/Arithmetic.ma

 r690 | true ⇒ S O ]. definition carry_of : bool → bool → bool → bool ≝ λa,b,c. match a with [ false ⇒ b ∧ c | true ⇒ b ∨ c ]. definition add_with_carries : ∀n:nat. BitVector n → BitVector n → bool → BitVector n × (BitVector n) ≝ λn,x,y,init_carry. fold_right2_i ??? (λn,b,c,r. let 〈lower_bits, carries〉 ≝ r in let last_carry ≝ match carries with [ VEmpty ⇒ init_carry | VCons _ cy _ ⇒ cy ] in let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_carry in let carry ≝ carry_of b c last_carry in 〈bit:::lower_bits, carry:::carries〉 ) 〈[[ ]], [[ ]]〉 n x y. (* Essentially the only difference for subtraction. *) definition borrow_of : bool → bool → bool → bool ≝ λa,b,c. match a with [ false ⇒ b ∨ c | true ⇒ b ∧ c ]. definition sub_with_borrows : ∀n:nat. BitVector n → BitVector n → bool → BitVector n × (BitVector n) ≝ λn,x,y,init_borrow. fold_right2_i ??? (λn,b,c,r. let 〈lower_bits, borrows〉 ≝ r in let last_borrow ≝ match borrows with [ VEmpty ⇒ init_borrow | VCons _ bw _ ⇒ bw ] in let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_borrow in let borrow ≝ borrow_of b c last_borrow in 〈bit:::lower_bits, borrow:::borrows〉 ) 〈[[ ]], [[ ]]〉 n x y. definition add_n_with_carry: ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝ ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. n ≥ 5 → (BitVector n) × (BitVector 3) ≝ λn: nat. λb: BitVector n. λc: BitVector n. λcarry: bool. let b_as_nat ≝ nat_of_bitvector n b in let c_as_nat ≝ nat_of_bitvector n c in let carry_as_nat ≝ nat_of_bool carry in let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in let ac_flag ≝ geb ((modulus b_as_nat (2 * n)) + (modulus c_as_nat (2 * n)) + c_as_nat) (2 * n) in let bit_xxx ≝ geb ((modulus b_as_nat (2^(n - 1))) + (modulus c_as_nat (2^(n - 1))) + c_as_nat) (2^(n - 1)) in let result ≝ modulus result_old (2^n) in let cy_flag ≝ geb result_old (2^n) in let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in mk_pair ? ? (bitvector_of_nat n result) ([[ cy_flag ; ac_flag ; ov_flag ]]). definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝ λpf:n ≥ 5. let 〈result, carries〉 ≝ add_with_carries n b c carry in let cy_flag ≝ get_index_v ?? carries 0 ? in let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *) 〈result, [[ cy_flag; ac_flag; ov_flag ]]〉. // @(transitive_le  … pf) /2/ qed. definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. n ≥ 5 → (BitVector n) × (BitVector 3) ≝ λn: nat. λb: BitVector n. λc: BitVector n. λcarry: bool. let b_as_nat ≝ nat_of_bitvector n b in let c_as_nat ≝ nat_of_bitvector n c in let carry_as_nat ≝ nat_of_bool carry in let temporary ≝ (b_as_nat mod (2 * n)) - (c_as_nat mod (2 * n)) in let ac_flag ≝ ltb (b_as_nat mod (2 * n)) ((c_as_nat mod (2 * n)) + carry_as_nat) in let bit_six ≝ ltb (b_as_nat mod (2^(n - 1))) ((c_as_nat mod (2^(n - 1))) + carry_as_nat) in let 〈b',cy_flag〉 ≝ if geb b_as_nat (c_as_nat + carry_as_nat) then 〈b_as_nat, false〉 else 〈b_as_nat + (2^n), true〉 in let ov_flag ≝ exclusive_disjunction cy_flag bit_six in 〈bitvector_of_nat n ((b' - c_as_nat) - carry_as_nat), [[ cy_flag; ac_flag; ov_flag ]]〉. λpf:n ≥ 5. let 〈result, carries〉 ≝ sub_with_borrows n b c carry in let cy_flag ≝ get_index_v ?? carries 0 ? in let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *) 〈result, [[ cy_flag; ac_flag; ov_flag ]]〉. // @(transitive_le  … pf) /2/ qed. definition add_8_with_carry ≝ add_n_with_carry 8. definition add_16_with_carry ≝ add_n_with_carry 16. λn: nat. λb: BitVector n. let b_as_nat ≝ (nat_of_bitvector n b) + 1 in let overflow ≝ geb b_as_nat 2^n in match overflow with [ false ⇒ bitvector_of_nat n b_as_nat | true ⇒ zero n ]. \fst (add_with_carries n b (zero n) true). definition decrement ≝ λn: nat. λb: BitVector n. let b_as_nat ≝ nat_of_bitvector n b in match b_as_nat with [ O ⇒ maximum n | S o ⇒ bitvector_of_nat n o ]. \fst (sub_with_borrows n b (zero n) true). definition two_complement_negation ≝ λn: nat. λb, c: BitVector n. let 〈res,flags〉 ≝ add_n_with_carry n b c false in let 〈res,flags〉 ≝ add_with_carries n b c false in res. Some ? (bitvector_of_nat n result) ]. alias id "option1" = "cic:/matita/basics/sums/option.ind(1,0,1)". definition division_s: ∀n. ∀b, c: BitVector n. option1 (BitVector n) ≝ definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝ λn. match n with let b_nat ≝ nat_of_bitvector ? b in let c_nat ≝ nat_of_bitvector ? c in let result ≝ modulus b_nat c_nat in bitvector_of_nat (n + n) result. match c_nat with [ O ⇒ None ? | _ ⇒ let result ≝ modulus b_nat c_nat in Some ? (bitvector_of_nat n result) ]. definition modulus_s ≝ definition lt_u ≝ λn. λb, c: BitVector n. let b_nat ≝ nat_of_bitvector ? b in let c_nat ≝ nat_of_bitvector ? c in ltb b_nat c_nat. fold_right2_i ??? (λ_.λa,b,r. match a with [ true ⇒ b ∧ r | false ⇒ b ∨ r ]) false. definition gt_u ≝ λn, b, c. lt_u n c b. definition gte_u ≝ λn, b, c. ¬(lt_u n b c). definition lt_s ≝ λn. λb, c: BitVector n. let 〈result, flags〉 ≝ sub_n_with_carry n b c false in let ov_flag ≝ get_index_v ? ? flags 2 ? in if ov_flag then true else ((match n return λn'.BitVector n' → bool with [ O ⇒ λ_.false | S o ⇒ λresult'.(get_index_v ? ? result' O ?) ]) result). // qed. let 〈result, borrows〉 ≝ sub_with_borrows n b c false in match borrows with [ VEmpty ⇒ false | VCons _ bwn tl ⇒ match tl with [ VEmpty ⇒ false | VCons _ bwpn _ ⇒ if exclusive_disjunction bwn bwpn then match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ] else match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ] ] ]. definition gt_s ≝ λn,b,c. lt_s n c b.
• src/ASM/BitVector.ma

 r690 false) b c. lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y. (x = y → P true) → (x ≠ y → P false) → P (eq_bv n x y). #P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf) #Q * *; normalize /3/ qed. let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝ let biglist ≝ rev ? (bitvector_of_nat_aux m m) in
• src/ASM/BitVectorTrie.ma

 r690 include "basics/sums.ma". include "basics/types.ma". include "cerco/BitVector.ma".
• src/ASM/Char.ma

 r690 (*include "logic/pts.ma".*) include "core_notation.ma". include "basics/pts.ma".
• src/ASM/Util.ma

 r690 include "arithmetics/nat.ma". include "basics/list.ma". include "basics/sums.ma". include "basics/types.ma". definition if_then_else ≝ ]. (* notation "hvbox('if' b 'then' t 'else' f)" non associative with precedence 83 for @{ 'if_then_else \$b \$t \$f }. *) notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else \$e \$t \$f }. notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else \$e \$t \$f }. interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f). definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O. let rec revapp (T:Type[0]) (l:list T) (r:list T) on l : list T ≝ match l with [ nil ⇒ r | cons h t ⇒ revapp T t (h::r) ]. definition rev ≝ λT:Type[0].λl. revapp T l [ ]. lemma eq_rect_Type0_r : notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" with precedence 10 for @{ match \$t with [ mk_pair \${ident x} \${ident y} ⇒ \$s ] }. for @{ match \$t with [ pair \${ident x} \${ident y} ⇒ \$s ] }. notation "⊥" with precedence 90 let rec division_aux (m: nat) (n : nat) (p: nat) ≝ match ltb n p with match ltb n (S p) with [ true ⇒ O | false ⇒ definition divide_with_remainder ≝ λm, n: nat. mk_pair ? ? (m ÷ n) (modulus m n). pair ? ? (m ÷ n) (modulus m n). let rec exponential (m: nat) (n: nat) on n ≝
• src/ASM/Vector.ma

 r690 include "basics/list.ma". include "basics/bool.ma". include "basics/sums.ma". include "basics/types.ma". include "cerco/Util.ma". include "arithmetics/nat.ma". include "oldlib/eq.ma". (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) | VCons o he tl ⇒ λK. match split A m' n (tl⌈Vector A o ↦ Vector A (m' + n)⌉) with [ mk_pair v1 v2 ⇒ 〈he:::v1, v2〉 [ pair v1 v2 ⇒ 〈he:::v1, v2〉 ] ] (?: (S (m' + n)) = S (m' + n))]. ]. let rec fold_right_i (A: Type[0]) (B: nat → Type[0]) (n: nat) (f: ∀n. A → B n → B (S n)) (x: B 0) (v: Vector A n) on v ≝ match v with [ VEmpty ⇒ x | VCons n hd tl ⇒ f ? hd (fold_right_i A B n f x tl) ]. let rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0]) (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat) match v with [ VEmpty ⇒ x | VCons n hd tl ⇒ f (fold_left A B n f x tl) hd | VCons n hd tl ⇒ fold_left A B n f (f x hd) tl ]. λv: Vector A n. λq: Vector B n. zip_with A B (A × B) n (mk_pair A B) v q. zip_with A B (A × B) n (pair A B) v q. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v ≝ match v return (λm.λv. Vector A m) with [ VEmpty ⇒ [[ ]] | VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]]) ]. // qed. (* At some points matita will attempt to reduce reverse with a known vector, which reduces the equality proof for the cast.  Normalising this proof needs to be fast enough to keep matita usable. *) let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝ match n return λn'.∀m.S(n'+m) = n'+S m with [ O ⇒ λm.refl ?? | S n' ⇒ λm. ? ]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed. let rec revapp (A: Type[0]) (n: nat) (m:nat) (v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝ match v return λn'.λ_. Vector A (n' + m) with [ VEmpty ⇒ acc | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉ ]. > plus_n_Sm_fast @refl qed. let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝ (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉. < plus_n_O @refl qed. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) qed. lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Prop. ∀v:Vector A n. match n return λn'. (Vector A n' → Prop) → Vector A n' → Prop with [ O ⇒ λP.λv.P [[ ]] → P v | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v ] P v. @(λA,n. λP:Vector A n → Prop. λv. match v return ? with [ VEmpty ⇒ ? | VCons m h t ⇒ ? ] P) [ // | // ] qed. (* XXX Proof below fails at qed. #A #n #P * [ #H @H | #m #h #t #H @H ] qed. *) lemma eq_v_elim: ∀P:bool → Prop. ∀A,f. (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) → ∀n,x,y. (x = y → P true) → (x ≠ y → P false) → P (eq_v A n f x y). #P #A #f #f_elim #n #x elim x [ #y @(vector_inv_n … y) normalize /2/ | #m #h #t #IH #y @(vector_inv_n … y) #h' #t' #Ht #Hf whd in ⊢ (?%) @(f_elim ? h h') #Eh [ @IH [ #Et @Ht >Eh >Et @refl | #NEt @Hf % #E' destruct (E') elim NEt /2/ ] | @Hf % #E' destruct (E') elim Eh /2/ ] ] qed. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Subvectors.                                                                *)
Note: See TracChangeset for help on using the changeset viewer.