Changeset 744 for src/ASM/Vector.ma


Ignore:
Timestamp:
Apr 7, 2011, 6:53:59 PM (9 years ago)
Author:
campbell
Message:

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Vector.ma

    r726 r744  
    1212include "arithmetics/nat.ma".
    1313
     14include "utilities/extranat.ma".
    1415include "utilities/oldlib/eq.ma".
    1516
     
    152153qed.
    153154
    154 let rec split (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
     155definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝
     156λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with
     157[ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ].
     158
     159definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝
     160λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with
     161[ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].
     162
     163let rec split' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
    155164 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
    156165  [ O ⇒ λv. 〈[[ ]], v〉
    157   | S m' ⇒ λv.
    158     match v return λl. λ_: Vector A l. l = S (plus m' n) → (Vector A (S m')) × (Vector A n) with
    159       [ VEmpty ⇒ λK. ⊥
    160       | VCons o he tl ⇒ λK.
    161         match split A m' n (tl⌈Vector A o ↦ Vector A (m' + n)⌉) with
    162         [ pair v1 v2 ⇒ 〈he:::v1, v2〉
    163         ]
    164       ] (?: (S (m' + n)) = S (m' + n))].
    165       //
    166       [ destruct
    167       | lapply (injective_S … K)
    168         //
    169       ]
    170 qed.
     166  | S m' ⇒ λv. let 〈l,r〉 ≝ split' A m' n (tail ?? v) in 〈head' ?? v:::l, r〉
     167  ].
     168(* Prevent undesirable unfolding. *)
     169let rec split (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝
     170 split' A m n v.
     171
    171172
    172173definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
     
    329330(* At some points matita will attempt to reduce reverse with a known vector,
    330331   which reduces the equality proof for the cast.  Normalising this proof needs
    331    to be fast enough to keep matita usable. *)
    332 let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝
    333 match n return λn'.∀m.S(n'+m) = n'+S m with
    334 [ O ⇒ λm.refl ??
    335 | S n' ⇒ λm. ?
    336 ]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed.
     332   to be fast enough to keep matita usable, so use plus_n_Sm_fast. *)
    337333
    338334let rec revapp (A: Type[0]) (n: nat) (m:nat)
     
    347343  (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉.
    348344< plus_n_O @refl qed.
     345
     346let rec pad_vector (A:Type[0]) (a:A) (n,m:nat) (v:Vector A m) on n : Vector A (n+m) ≝
     347match n return λn.Vector A (n+m) with
     348[ O ⇒ v
     349| S n' ⇒ a:::(pad_vector A a n' m v)
     350].
    349351
    350352(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    404406qed.
    405407
     408
     409(* XXX this is horrible - but useful to ensure that we can normalise in the proof assistant. *)
     410definition switch_bv_plus : ∀A:Type[0]. ∀n,m. Vector A (n+m) → Vector A (m+n) ≝
     411λA,n,m. match commutative_plus_faster n m with [ refl ⇒ λi.i ].
     412
    406413definition shift_right_1 ≝
    407414  λA: Type[0].
     
    409416  λv: Vector A (S n).
    410417  λa: A.
    411     reverse … (shift_left_1 … (reverse … v) a).
    412    
    413 definition shift_left ≝
     418    let 〈v',dropped〉 ≝ split ? n 1 (switch_bv_plus ? 1 n v) in a:::v'.
     419(*    reverse … (shift_left_1 … (reverse … v) a).*)
     420
     421definition shift_left : ∀A:Type[0]. ∀n,m:nat. Vector A n → A → Vector A n ≝
    414422  λA: Type[0].
    415423  λn, m: nat.
    416   λv: Vector A (S n).
    417   λa: A.
    418     iterate … (λx. shift_left_1 … x a) v m.
     424    match nat_compare n m return λx,y.λ_. Vector A x → A → Vector A x with
     425    [ nat_lt _ _ ⇒ λv,a. replicate … a
     426    | nat_eq _   ⇒ λv,a. replicate … a
     427    | nat_gt d m ⇒ λv,a. let 〈v0,v'〉 ≝ split … v in switch_bv_plus … (v' @@ (replicate … a))
     428    ].
     429
     430(*    iterate … (λx. shift_left_1 … x a) v m.*)
    419431   
    420432definition shift_right ≝
     
    428440(* Decidable equality.                                                        *)
    429441(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    430 
    431 definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝
    432 λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with
    433 [ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ].
    434 
    435 definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝
    436 λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with
    437 [ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].
    438442
    439443let rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝
Note: See TracChangeset for help on using the changeset viewer.