Changeset 744 for src/ASM/Vector.ma

Timestamp:

Apr 7, 2011, 6:53:59 PM (11 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:

• src/ASM/Vector.ma (modified) (7 diffs)

src/ASM/Vector.ma

@@ -12 +12 @@
 include "arithmetics/nat.ma".
 
+include "utilities/extranat.ma".
 include "utilities/oldlib/eq.ma".
 
@@ -152 +153 @@
 qed.
 
-let rec split (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
+definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝
+λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with
+[ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ].
+
+definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝
+λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with
+[ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].
+
+let rec split' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
  match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
   [ O ⇒ λv. 〈[[ ]], v〉
-  | S m' ⇒ λv.
-    match v return λl. λ_: Vector A l. l = S (plus m' n) → (Vector A (S m')) × (Vector A n) with
-      [ VEmpty ⇒ λK. ⊥
-      | VCons o he tl ⇒ λK.
-        match split A m' n (tl⌈Vector A o ↦ Vector A (m' + n)⌉) with
-        [ pair v1 v2 ⇒ 〈he:::v1, v2〉
-        ]
-      ] (?: (S (m' + n)) = S (m' + n))].
-      //
-      [ destruct
-      | lapply (injective_S … K)
-        //
-      ]
-qed.
+  | S m' ⇒ λv. let 〈l,r〉 ≝ split' A m' n (tail ?? v) in 〈head' ?? v:::l, r〉
+  ].
+(* Prevent undesirable unfolding. *)
+let rec split (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝
+ split' A m n v.
+
 
 definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
@@ -329 +330 @@
 (* 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.
+   to be fast enough to keep matita usable, so use plus_n_Sm_fast. *)
 
 let rec revapp (A: Type[0]) (n: nat) (m:nat)
@@ -347 +343 @@
   (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉.
 < plus_n_O @refl qed.
+
+let rec pad_vector (A:Type[0]) (a:A) (n,m:nat) (v:Vector A m) on n : Vector A (n+m) ≝
+match n return λn.Vector A (n+m) with
+[ O ⇒ v
+| S n' ⇒ a:::(pad_vector A a n' m v)
+].
 
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
@@ -404 +406 @@
 qed.
 
+
+(* XXX this is horrible - but useful to ensure that we can normalise in the proof assistant. *)
+definition switch_bv_plus : ∀A:Type[0]. ∀n,m. Vector A (n+m) → Vector A (m+n) ≝
+λA,n,m. match commutative_plus_faster n m with [ refl ⇒ λi.i ].
+
 definition shift_right_1 ≝
   λA: Type[0].
@@ -409 +416 @@
   λv: Vector A (S n).
   λa: A.
-    reverse … (shift_left_1 … (reverse … v) a).
-    
-definition shift_left ≝
+    let 〈v',dropped〉 ≝ split ? n 1 (switch_bv_plus ? 1 n v) in a:::v'.
+(*    reverse … (shift_left_1 … (reverse … v) a).*)
+
+definition shift_left : ∀A:Type[0]. ∀n,m:nat. Vector A n → A → Vector A n ≝
   λA: Type[0].
   λn, m: nat.
-  λv: Vector A (S n).
-  λa: A.
-    iterate … (λx. shift_left_1 … x a) v m.
+    match nat_compare n m return λx,y.λ_. Vector A x → A → Vector A x with
+    [ nat_lt _ _ ⇒ λv,a. replicate … a
+    | nat_eq _   ⇒ λv,a. replicate … a
+    | nat_gt d m ⇒ λv,a. let 〈v0,v'〉 ≝ split … v in switch_bv_plus … (v' @@ (replicate … a))
+    ].
+
+(*    iterate … (λx. shift_left_1 … x a) v m.*)
     
 definition shift_right ≝
@@ -428 +440 @@
 (* Decidable equality.                                                        *)
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
-
-definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝
-λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with
-[ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ].
-
-definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝
-λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with
-[ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].
 
 let rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝