Changeset 697 for src/ASM


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

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

Location:
src/ASM
Files:
7 edited
1 copied

Legend:

Unmodified
Added
Removed
  • src/ASM

  • src/ASM/Arithmetic.ma

    r690 r697  
    88      | true ⇒ S O
    99      ].
     10
     11definition carry_of : bool → bool → bool → bool ≝
     12λa,b,c. match a with [ false ⇒ b ∧ c | true ⇒ b ∨ c ].
     13
     14definition add_with_carries : ∀n:nat. BitVector n → BitVector n → bool →
     15                                      BitVector n × (BitVector n) ≝
     16  λn,x,y,init_carry.
     17  fold_right2_i ???
     18   (λn,b,c,r.
     19     let 〈lower_bits, carries〉 ≝ r in
     20     let last_carry ≝ match carries with [ VEmpty ⇒ init_carry | VCons _ cy _ ⇒ cy ] in
     21     let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_carry in
     22     let carry ≝ carry_of b c last_carry in
     23       〈bit:::lower_bits, carry:::carries〉
     24   )
     25   〈[[ ]], [[ ]]〉 n x y.
     26
     27(* Essentially the only difference for subtraction. *)
     28definition borrow_of : bool → bool → bool → bool ≝
     29λa,b,c. match a with [ false ⇒ b ∨ c | true ⇒ b ∧ c ].
     30
     31definition sub_with_borrows : ∀n:nat. BitVector n → BitVector n → bool →
     32                                      BitVector n × (BitVector n) ≝
     33  λn,x,y,init_borrow.
     34  fold_right2_i ???
     35   (λn,b,c,r.
     36     let 〈lower_bits, borrows〉 ≝ r in
     37     let last_borrow ≝ match borrows with [ VEmpty ⇒ init_borrow | VCons _ bw _ ⇒ bw ] in
     38     let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_borrow in
     39     let borrow ≝ borrow_of b c last_borrow in
     40       〈bit:::lower_bits, borrow:::borrows〉
     41   )
     42   〈[[ ]], [[ ]]〉 n x y.
    1043   
    1144definition add_n_with_carry:
    12       ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝
     45      ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. n ≥ 5 →
     46      (BitVector n) × (BitVector 3) ≝
    1347  λn: nat.
    1448  λb: BitVector n.
    1549  λc: BitVector n.
    1650  λcarry: bool.
    17     let b_as_nat ≝ nat_of_bitvector n b in
    18     let c_as_nat ≝ nat_of_bitvector n c in
    19     let carry_as_nat ≝ nat_of_bool carry in
    20     let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in
    21     let ac_flag ≝ geb ((modulus b_as_nat (2 * n)) +
    22                   (modulus c_as_nat (2 * n)) +
    23                   c_as_nat) (2 * n) in
    24     let bit_xxx ≝ geb ((modulus b_as_nat (2^(n - 1))) +
    25                   (modulus c_as_nat (2^(n - 1))) +
    26                   c_as_nat) (2^(n - 1)) in
    27     let result ≝ modulus result_old (2^n) in
    28     let cy_flag ≝ geb result_old (2^n) in
    29     let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
    30       mk_pair ? ? (bitvector_of_nat n result)
    31                        ([[ cy_flag ; ac_flag ; ov_flag ]]).
    32 
    33 definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝
     51  λpf:n ≥ 5.
     52 
     53    let 〈result, carries〉 ≝ add_with_carries n b c carry in
     54    let cy_flag ≝ get_index_v ?? carries 0 ? in
     55    let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in
     56    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
     57      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
     58// @(transitive_le  … pf) /2/
     59qed.
     60
     61definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. n ≥ 5 →
     62                                            (BitVector n) × (BitVector 3) ≝
    3463  λn: nat.
    3564  λb: BitVector n.
    3665  λc: BitVector n.
    3766  λcarry: bool.
    38      let b_as_nat ≝ nat_of_bitvector n b in
    39      let c_as_nat ≝ nat_of_bitvector n c in
    40      let carry_as_nat ≝ nat_of_bool carry in
    41      let temporary ≝ (b_as_nat mod (2 * n)) - (c_as_nat mod (2 * n)) in
    42      let ac_flag ≝ ltb (b_as_nat mod (2 * n)) ((c_as_nat mod (2 * n)) + carry_as_nat) in
    43      let bit_six ≝ ltb (b_as_nat mod (2^(n - 1))) ((c_as_nat mod (2^(n - 1))) + carry_as_nat) in
    44      let 〈b',cy_flag〉 ≝
    45        if geb b_as_nat (c_as_nat + carry_as_nat) then
    46          〈b_as_nat, false〉
    47        else
    48          〈b_as_nat + (2^n), true〉
    49      in
    50        let ov_flag ≝ exclusive_disjunction cy_flag bit_six in
    51          〈bitvector_of_nat n ((b' - c_as_nat) - carry_as_nat), [[ cy_flag; ac_flag; ov_flag ]]〉.         
    52          
     67  λpf:n ≥ 5.
     68 
     69    let 〈result, carries〉 ≝ sub_with_borrows n b c carry in
     70    let cy_flag ≝ get_index_v ?? carries 0 ? in
     71    let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in
     72    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
     73      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
     74// @(transitive_le  … pf) /2/
     75qed.
     76
    5377definition add_8_with_carry ≝ add_n_with_carry 8.
    5478definition add_16_with_carry ≝ add_n_with_carry 16.
     
    5983  λn: nat.
    6084  λb: BitVector n.
    61     let b_as_nat ≝ (nat_of_bitvector n b) + 1 in
    62     let overflow ≝ geb b_as_nat 2^n in
    63       match overflow with
    64         [ false ⇒ bitvector_of_nat n b_as_nat
    65         | true ⇒ zero n
    66         ].
     85    \fst (add_with_carries n b (zero n) true).
    6786       
    6887definition decrement ≝
    6988  λn: nat.
    7089  λb: BitVector n.
    71     let b_as_nat ≝ nat_of_bitvector n b in
    72       match b_as_nat with
    73         [ O ⇒ maximum n
    74         | S o ⇒ bitvector_of_nat n o
    75         ].
     90    \fst (sub_with_borrows n b (zero n) true).
    7691   
    7792definition two_complement_negation ≝
     
    8499  λn: nat.
    85100  λb, c: BitVector n.
    86     let 〈res,flags〉 ≝ add_n_with_carry n b c false in
     101    let 〈res,flags〉 ≝ add_with_carries n b c false in
    87102      res.
    88103   
     
    111126        Some ? (bitvector_of_nat n result)
    112127    ].
    113    
    114 alias id "option1" = "cic:/matita/basics/sums/option.ind(1,0,1)".
    115      
    116 definition division_s: ∀n. ∀b, c: BitVector n. option1 (BitVector n) ≝
     128     
     129definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
    117130  λn.
    118131    match n with
     
    156169    let b_nat ≝ nat_of_bitvector ? b in
    157170    let c_nat ≝ nat_of_bitvector ? c in
    158     let result ≝ modulus b_nat c_nat in
    159       bitvector_of_nat (n + n) result.
     171    match c_nat with
     172    [ O ⇒ None ?
     173    | _ ⇒
     174      let result ≝ modulus b_nat c_nat in
     175      Some ? (bitvector_of_nat n result)
     176    ].
    160177           
    161178definition modulus_s ≝
     
    170187     
    171188definition lt_u ≝
    172   λn.
    173   λb, c: BitVector n.
    174     let b_nat ≝ nat_of_bitvector ? b in
    175     let c_nat ≝ nat_of_bitvector ? c in
    176       ltb b_nat c_nat.
     189  fold_right2_i ???
     190    (λ_.λa,b,r.
     191      match a with
     192      [ true ⇒ b ∧ r
     193      | false ⇒ b ∨ r
     194      ])
     195    false.
    177196     
    178197definition gt_u ≝ λn, b, c. lt_u n c b.
     
    181200
    182201definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
    183      
     202
    184203definition lt_s ≝
    185204  λn.
    186205  λb, c: BitVector n.
    187     let 〈result, flags〉 ≝ sub_n_with_carry n b c false in
    188     let ov_flag ≝ get_index_v ? ? flags 2 ? in
    189      if ov_flag then
    190        true
    191      else
    192        ((match n return λn'.BitVector n' → bool with
    193        [ O ⇒ λ_.false
    194        | S o ⇒
    195          λresult'.(get_index_v ? ? result' O ?)
    196        ]) result).
    197   //
    198 qed.
    199 
     206    let 〈result, borrows〉 ≝ sub_with_borrows n b c false in
     207    match borrows with
     208    [ VEmpty ⇒ false
     209    | VCons _ bwn tl ⇒
     210      match tl with
     211      [ VEmpty ⇒ false
     212      | VCons _ bwpn _ ⇒
     213        if exclusive_disjunction bwn bwpn then
     214          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
     215        else
     216          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
     217      ]
     218    ].
     219   
    200220definition gt_s ≝ λn,b,c. lt_s n c b.
    201221
  • src/ASM/BitVector.ma

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

    r690 r697  
    1 include "basics/sums.ma".
     1include "basics/types.ma".
    22
    33include "cerco/BitVector.ma".
  • src/ASM/Char.ma

    r690 r697  
    11(*include "logic/pts.ma".*)
    22
    3 include "core_notation.ma".
    43include "basics/pts.ma".
    54
  • src/ASM/Util.ma

    r690 r697  
    11include "arithmetics/nat.ma".
    22include "basics/list.ma".
    3 include "basics/sums.ma".
     3include "basics/types.ma".
    44
    55definition if_then_else ≝
     
    1313  ].
    1414   
     15(*
    1516notation "hvbox('if' b 'then' t 'else' f)"
    1617  non associative with precedence 83
    1718  for @{ 'if_then_else $b $t $f }.
     19*)
     20notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
     21notation < "'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 }.
    1822
    1923interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f).
     
    2731
    2832definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
     33
     34let rec revapp (T:Type[0]) (l:list T) (r:list T) on l : list T ≝
     35match l with
     36[ nil ⇒ r
     37| cons h t ⇒ revapp T t (h::r)
     38].
     39
     40definition rev ≝ λT:Type[0].λl. revapp T l [ ].
    2941
    3042lemma eq_rect_Type0_r :
     
    6476notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
    6577 with precedence 10
    66 for @{ match $t with [ mk_pair ${ident x} ${ident y} ⇒ $s ] }.
     78for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
    6779
    6880notation "⊥" with precedence 90
     
    100112
    101113let rec division_aux (m: nat) (n : nat) (p: nat) ≝
    102   match ltb n p with
     114  match ltb n (S p) with
    103115    [ true ⇒ O
    104116    | false ⇒
     
    147159definition divide_with_remainder ≝
    148160  λm, n: nat.
    149     mk_pair ? ? (m ÷ n) (modulus m n).
     161    pair ? ? (m ÷ n) (modulus m n).
    150162   
    151163let rec exponential (m: nat) (n: nat) on n ≝
  • src/ASM/Vector.ma

    r690 r697  
    66include "basics/list.ma".
    77include "basics/bool.ma".
    8 include "basics/sums.ma".
     8include "basics/types.ma".
    99
    1010include "cerco/Util.ma".
     
    1212include "arithmetics/nat.ma".
    1313
     14include "oldlib/eq.ma".
    1415
    1516(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    159160      | VCons o he tl ⇒ λK.
    160161        match split A m' n (tl⌈Vector A o ↦ Vector A (m' + n)⌉) with
    161         [ mk_pair v1 v2 ⇒ 〈he:::v1, v2〉
     162        [ pair v1 v2 ⇒ 〈he:::v1, v2〉
    162163        ]
    163164      ] (?: (S (m' + n)) = S (m' + n))].
     
    200201    ].
    201202
     203let rec fold_right_i (A: Type[0]) (B: nat → Type[0]) (n: nat)
     204                     (f: ∀n. A → B n → B (S n)) (x: B 0) (v: Vector A n) on v ≝
     205  match v with
     206    [ VEmpty ⇒ x
     207    | VCons n hd tl ⇒ f ? hd (fold_right_i A B n f x tl)
     208    ].
     209
    202210let rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0])
    203211                      (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
     
    228236  match v with
    229237    [ VEmpty ⇒ x
    230     | VCons n hd tl ⇒ f (fold_left A B n f x tl) hd
     238    | VCons n hd tl ⇒ fold_left A B n f (f x hd) tl
    231239    ].
    232240   
     
    269277  λv: Vector A n.
    270278  λq: Vector B n.
    271     zip_with A B (A × B) n (mk_pair A B) v q.
     279    zip_with A B (A × B) n (pair A B) v q.
    272280
    273281(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    319327(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    320328
    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.
     329(* At some points matita will attempt to reduce reverse with a known vector,
     330   which reduces the equality proof for the cast.  Normalising this proof needs
     331   to be fast enough to keep matita usable. *)
     332let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝
     333match 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.
     337
     338let rec revapp (A: Type[0]) (n: nat) (m:nat)
     339                (v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝
     340  match v return λn'.λ_. Vector A (n' + m) with
     341    [ VEmpty ⇒ acc
     342    | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉
     343    ].
     344> plus_n_Sm_fast @refl qed.
     345
     346let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝
     347  (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉.
     348< plus_n_O @refl qed.
    329349
    330350(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    436456qed.
    437457
     458lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Prop. ∀v:Vector A n.
     459  match n return λn'. (Vector A n' → Prop) → Vector A n' → Prop with
     460  [ O ⇒ λP.λv.P [[ ]] → P v
     461  | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
     462  ] P v.
     463@(λA,n. λP:Vector A n → Prop. λv. match v return
     464?
     465with [ VEmpty ⇒ ? | VCons m h t ⇒ ? ] P)
     466[ // | // ] qed.
     467(* XXX Proof below fails at qed.
     468#A #n #P * [ #H @H | #m #h #t #H @H ] qed.
     469*)
     470
     471lemma eq_v_elim: ∀P:bool → Prop. ∀A,f.
     472  (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
     473  ∀n,x,y.
     474  (x = y → P true) →
     475  (x ≠ y → P false) →
     476  P (eq_v A n f x y).
     477#P #A #f #f_elim #n #x elim x
     478[ #y @(vector_inv_n … y)
     479  normalize /2/
     480| #m #h #t #IH #y @(vector_inv_n … y)
     481  #h' #t' #Ht #Hf whd in ⊢ (?%)
     482  @(f_elim ? h h') #Eh
     483  [ @IH [ #Et @Ht >Eh >Et @refl | #NEt @Hf % #E' destruct (E') elim NEt /2/ ]
     484  | @Hf % #E' destruct (E') elim Eh /2/
     485  ]
     486] qed.
     487
    438488(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    439489(* Subvectors.                                                                *)
Note: See TracChangeset for help on using the changeset viewer.