Changeset 1599 for src/ASM


Ignore:
Timestamp:
Dec 13, 2011, 1:34:37 AM (8 years ago)
Author:
sacerdot
Message:

Start of merging of stuff into the standard library of Matita.

Location:
src/ASM
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1485 r1599  
    2222         of add_with_carries *)
    2323     if last_carry then
    24       let bit ≝ exclusive_disjunction (exclusive_disjunction b c) true in
     24      let bit ≝ xorb (xorb b c) true in
    2525      let carry ≝ carry_of b c true in
    2626       〈bit:::lower_bits, carry:::carries〉
    2727     else
    28       let bit ≝ exclusive_disjunction (exclusive_disjunction b c) false in
     28      let bit ≝ xorb (xorb b c) false in
    2929      let carry ≝ carry_of b c false in
    3030       〈bit:::lower_bits, carry:::carries〉     
     
    4343     let 〈lower_bits, borrows〉 ≝ r in
    4444     let last_borrow ≝ match borrows with [ VEmpty ⇒ init_borrow | VCons _ bw _ ⇒ bw ] in
    45      let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_borrow in
     45     let bit ≝ xorb (xorb b c) last_borrow in
    4646     let borrow ≝ borrow_of b c last_borrow in
    4747       〈bit:::lower_bits, borrow:::borrows〉
     
    6060    let 〈result, carries〉 ≝ add_with_carries n b c carry in
    6161    let cy_flag ≝ get_index_v ?? carries 0 ? in
    62     let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in
     62    let ov_flag ≝ xorb cy_flag (get_index_v ?? carries 1 ?) in
    6363    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
    6464      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
     
    7676    let 〈result, carries〉 ≝ sub_with_borrows n b c carry in
    7777    let cy_flag ≝ get_index_v ?? carries 0 ? in
    78     let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in
     78    let ov_flag ≝ xorb cy_flag (get_index_v ?? carries 1 ?) in
    7979    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
    8080      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
     
    311311      [ VEmpty ⇒ false
    312312      | VCons _ bwpn _ ⇒
    313         if exclusive_disjunction bwn bwpn then
     313        if xorb bwn bwpn then
    314314          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
    315315        else
     
    349349        let 〈c1,r〉 ≝ d in
    350350          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
    351            (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
     351           (xorb (xorb b1 b2) c1) ::: r〉)
    352352     〈d, [[ ]]〉 ? b c.
    353353   
  • src/ASM/BitVector.ma

    r1521 r1599  
    8787  λb: BitVector n.
    8888  λc: BitVector n.
    89     zip_with ? ? ? n (exclusive_disjunction) b c.
     89    zip_with ? ? ? n xorb b c.
    9090   
    9191interpretation "BitVector exclusive disjunction"
    92   'exclusive_disjunction b c = (exclusive_disjunction ? b c).
     92  'exclusive_disjunction b c = (xorb b c).
    9393   
    9494definition negation_bv ≝
  • src/ASM/JMCoercions.ma

    r1335 r1599  
    11include "basics/jmeq.ma".
    22include "basics/types.ma".
    3 include "basics/list.ma".
     3include "basics/lists/list.ma".
    44
    55definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
  • src/ASM/Status.ma

    r1588 r1599  
    11081108lemma snd_fetch_pseudo_instruction:
    11091109 ∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = \snd (half_add ? ppc (bitvector_of_nat ? 1)).
    1110  #l #ppc whd in ⊢ (??%?); whd in ⊢ (?? match % with [_ ⇒ ?]?); @pair_elim'
    1111  #lft #rgt @pair_elim' #x #y #_ @pair_elim' #a #b #_ normalize #H
    1112  generalize in match (pair_destruct_2 ????? H); normalize #K >K %
     1110 #l #ppc whd in ⊢ (??(???%)?); @pair_elim
     1111 #lft #rgt @pair_elim #x #y #_ #_ %
    11131112qed.
    11141113
  • src/ASM/String.ma

    r698 r1599  
    1 include "basics/list.ma".
     1include "basics/lists/list.ma".
    22
    33include "ASM/Char.ma".
  • src/ASM/Util.ma

    r1598 r1599  
    1 include "basics/list.ma".
     1include "basics/lists/list.ma".
    22include "basics/types.ma".
    33include "arithmetics/nat.ma".
    4 
    5 include "utilities/pair.ma".
    64include "ASM/JMCoercions.ma".
    75
     
    649647
    650648   
    651 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
    652  for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
    653 notation < "hvbox('if' \nbsp term 19 e \nbsp break 'then' \nbsp term 19 t \nbsp break 'else' \nbsp term 48 f \nbsp)" non associative with precedence 19
    654  for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
    655 
    656649let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
    657650                        (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝
     
    684677    | S o ⇒ f (iterate A f a o)
    685678    ].
    686 
    687 (* Yeah, I probably ought to do something more general... *)
    688 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
    689 with precedence 90 for @{ 'triple $a $b $c}.
    690 interpretation "Triple construction" 'triple x y z = (mk_Prod ? ? (mk_Prod ? ? x y) z).
    691 
    692 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
    693 with precedence 90 for @{ 'quadruple $a $b $c $d}.
    694 interpretation "Quadruple construction" 'quadruple w x y z = (mk_Prod ? ? (mk_Prod ? ? w x) (mk_Prod ? ? y z)).
    695 
    696 notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
    697  with precedence 10
    698 for @{ match $t with [ pair ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ pair ${ident w} ${ident x} ⇒ match ${fresh yz} with [ pair ${ident y} ${ident z} ⇒ $s ] ] ] }.
    699 
    700 notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
    701  with precedence 10
    702 for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }.
    703 
    704 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
    705  with precedence 10
    706 for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.
    707 
    708 axiom pair_elim':
    709   ∀A,B,C: Type[0].
    710   ∀T: A → B → C.
    711   ∀p.
    712   ∀P: A×B → C → Prop.
    713     (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
    714       P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
    715 
    716 axiom pair_elim'':
    717   ∀A,B,C,C': Type[0].
    718   ∀T: A → B → C.
    719   ∀T': A → B → C'.
    720   ∀p.
    721   ∀P: A×B → C → C' → Prop.
    722     (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
    723       P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
    724 
    725 lemma pair_destruct_1:
    726  ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
    727  #A #B #a #b *; /2/
    728 qed.
    729 
    730 lemma pair_destruct_2:
    731  ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
    732  #A #B #a #b *; /2/
    733 qed.
    734 
    735 
    736 let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
    737   match b with
    738     [ true ⇒
    739       match c with
    740         [ false ⇒ true
    741         | true ⇒ false
    742         ]
    743     | false ⇒
    744       match c with
    745         [ false ⇒ false
    746         | true ⇒ true
    747         ]
    748     ].
    749 
    750 (* dpm: conflicts with library definitions
    751 interpretation "Nat less than" 'lt m n = (ltb m n).
    752 interpretation "Nat greater than" 'gt m n = (gtb m n).
    753 interpretation "Nat greater than eq" 'geq m n = (geb m n).
    754 *)
    755679
    756680let rec division_aux (m: nat) (n : nat) (p: nat) ≝
     
    891815  elim b
    892816  normalize
    893   [ /2/
     817  [ /2 by conj/
    894818  | # K
    895819    destruct
  • src/ASM/Vector.ma

    r1598 r1599  
    44(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    55
    6 include "basics/list.ma".
     6include "basics/lists/list.ma".
    77include "basics/bool.ma".
    88include "basics/types.ma".
Note: See TracChangeset for help on using the changeset viewer.