Ignore:
Timestamp:
Feb 16, 2011, 4:25:02 PM (9 years ago)
Author:
campbell
Message:

Minimal integration of bitvectors into Clight semantics

  • does a "round trip" through Z for most operations (slow)
  • a few extra bits for equality on vectors
  • version of reverse that doesn't make matita fall over on size 32 vectors during disambiguation and automation
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/cerco/Vector.ma

    r534 r535  
    1212include "arithmetics/nat.ma".
    1313
     14include "oldlib/eq.ma".
    1415
    1516(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    319320(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    320321
    321 let rec reverse (A: Type[0]) (n: nat)
    322                  (v: Vector A n) on v ≝
    323   match v return (λm.λv. Vector A m) with
    324     [ VEmpty ⇒ [[ ]]
    325     | VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]])
    326     ].
    327     //
    328 qed.
     322(* At some points matita will attempt to reduce reverse with a known vector,
     323   which reduces the equality proof for the cast.  Normalising this proof needs
     324   to be fast enough to keep matita usable. *)
     325let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝
     326match n return λn'.∀m.S(n'+m) = n'+S m with
     327[ O ⇒ λm.refl ??
     328| S n' ⇒ λm. ?
     329]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed.
     330
     331let rec revapp (A: Type[0]) (n: nat) (m:nat)
     332                (v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝
     333  match v return λn'.λ_. Vector A (n' + m) with
     334    [ VEmpty ⇒ acc
     335    | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉
     336    ].
     337> plus_n_Sm_fast @refl qed.
     338
     339let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝
     340  (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉.
     341< plus_n_O @refl qed.
    329342
    330343(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    436449qed.
    437450
     451lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Prop. ∀v:Vector A n.
     452  match n return λn'. (Vector A n' → Prop) → Vector A n' → Prop with
     453  [ O ⇒ λP.λv.P [[ ]] → P v
     454  | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
     455  ] P v.
     456@(λA,n. λP:Vector A n → Prop. λv. match v return
     457?
     458with [ VEmpty ⇒ ? | VCons m h t ⇒ ? ] P)
     459[ // | // ] qed.
     460(* XXX Proof below fails at qed.
     461#A #n #P * [ #H @H | #m #h #t #H @H ] qed.
     462*)
     463
     464lemma eq_v_elim: ∀P:bool → Prop. ∀A,f.
     465  (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
     466  ∀n,x,y.
     467  (x = y → P true) →
     468  (x ≠ y → P false) →
     469  P (eq_v A n f x y).
     470#P #A #f #f_elim #n #x elim x
     471[ #y @(vector_inv_n … y)
     472  normalize /2/
     473| #m #h #t #IH #y @(vector_inv_n … y)
     474  #h' #t' #Ht #Hf whd in ⊢ (?%)
     475  @(f_elim ? h h') #Eh
     476  [ @IH [ #Et @Ht >Eh >Et @refl | #NEt @Hf % #E' destruct (E') elim NEt /2/ ]
     477  | @Hf % #E' destruct (E') elim Eh /2/
     478  ]
     479] qed.
     480
    438481(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    439482(* Subvectors.                                                                *)
Note: See TracChangeset for help on using the changeset viewer.