Changeset 248


Ignore:
Timestamp:
Nov 22, 2010, 11:43:04 AM (9 years ago)
Author:
mulligan
Message:

More changes. Added datatype for addressing modes.

Location:
Deliverables/D4.1/Matita
Files:
1 added
6 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/ASM.ma

    r247 r248  
     1include "Universes.ma".
     2include "Equality.ma".
     3include "BitVector.ma".
     4
    15ninductive AddressingMode: Type[0] ≝
    2   Direct: BitVector eight → AddressingMode
    3 |
     6  Direct: Byte → AddressingMode
     7| Indirect: Bit → AddressingMode
     8| ExtIndirect: Bit → AddressingMode
     9| Register: Bit → Bit → Bit → AddressingMode
     10| AccumulatorA: AddressingMode
     11| AccumulatorB: AddressingMode
     12| DPointer: AddressingMode
     13| Data: Byte → AddressingMode
     14| Data16: Word → AddressingMode
     15| AccumulatorDPointer: AddressingMode
     16| AccumulatorProgramCounter: AddressingMode
     17| ExternalIndirectDPointer: AddressingMode
     18| IndirectDPointer: AddressingMode
     19| Carry: AddressingMode
     20| Bit: Bit → AddressingMode
     21| ComplementBit: Bit → AddressingMode
     22| Relative: Byte → AddressingMode
     23| Address11: Word11 → AddressingMode
     24| Address16: Word → AddressingMode.
  • Deliverables/D4.1/Matita/Arithmetic.ma

    r246 r248  
    1 include "Infrastructure/Universes.ma".
    2 include "Infrastructure/Equality.ma".
    3 include "Infrastructure/Connectives.ma".
    4 
    5 include "Common/Nat/Nat.ma".
    6 include "Common/Nat/Addition.ma".
    7 include "Common/Nat/Multiplication.ma".
    8 include "Common/Nat/Division_Modulus.ma".
    9 include "Common/Nat/Order.ma".
    10 
    11 include "Programming/Datatypes/Bool.ma".
    12 
    13 include "Programming/Datatypes/Listlike/Vector/BitVector.ma".
    14 include "Programming/Datatypes/Listlike/List/List.ma".
     1include "Universes.ma".
     2include "Equality.ma".
     3include "Connectives.ma".
     4include "Nat.ma".
     5include "Exponential.ma".
     6include "Bool.ma".
     7include "BitVector.ma".
     8include "List.ma".
    159   
    1610ndefinition eight ≝ exponential (S(S(Z))) (S(S(S(Z)))).
    1711ndefinition sixteen ≝ eight + eight.
    18 ndefinition one_hundred_and_twenty_eight ≝ sixteen × eight.
     12ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
    1913ndefinition two_hundred_and_fifty_six ≝
    2014  one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.                                         
     15   
     16ndefinition nat_of_bool ≝
     17  λb: Bool.
     18    match b with
     19      [ False ⇒ Z
     20      | True ⇒ S Z
     21      ].
    2122   
    2223ndefinition add_n_with_carry:
     
    3031    let carry_as_nat ≝ nat_of_bool carry in
    3132    let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in
    32     let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) × n)) +
    33                   (modulus c_as_nat ((S (S Z)) × n)) +
    34                   c_as_nat) ≥ ((S (S Z)) × n) in
     33    let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) * n)) +
     34                  (modulus c_as_nat ((S (S Z)) * n)) +
     35                  c_as_nat) ≥ ((S (S Z)) * n) in
    3536    let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n - (S Z)))) +
    3637                  (modulus c_as_nat ((S (S Z))^(n - (S Z)))) +
     
    3940    let cy_flag ≝ (result_old ≥ ((S (S Z))^n)) in
    4041    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
    41       ? (mk_Cartesian (BitVector n) ? (bitvector_of_nat n result)
     42      ? (mk_Cartesian (BitVector n) ? (? (bitvector_of_nat n result))
    4243                          (cy_flag :: ac_flag :: ov_flag :: Empty Bool)).
    4344    //.
     
    6465ndefinition add_16_with_carry ≝ add_n_with_carry sixteen.
    6566
     67(*
    6668ndefinition increment ≝
    6769  λn: Nat.
     
    7072    let overflow ≝ b_as_nat ≥ (S (S Z))^n in
    7173      match overflow with
    72         [ True ⇒ bitvector_of_nat n Z
    73         | False ⇒ bitvector_of_nat n b_as_nat
     74        [ False ⇒ bitvector_of_nat n b_as_nat
     75        | True ⇒ bitvector_of_nat n Z
    7476        ].
    7577       
     
    9294  //.
    9395nqed.
     96
     97*)
  • Deliverables/D4.1/Matita/BitVector.ma

    r246 r248  
    2323ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))).
    2424ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).
     25ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))).
    2526
    2627(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    196197    | Cons o hd tl ⇒
    197198      let hdval ≝ match hd with [ True ⇒ S Z | False ⇒ Z ] in
    198         ((exponential (S (S Z)) o) × hdval) + nat_of_bitvector o tl
     199        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
    199200    ].
  • Deliverables/D4.1/Matita/BitVectorTrie.ma

    r246 r248  
    1 include "Programming/Datatypes/Listlike/Vector/BitVector.ma".
    2 include "Programming/Datatypes/Compare.ma".
    3 include "Programming/Datatypes/Bool.ma".
    4 include "Programming/Datatypes/Maybe.ma".
     1include "BitVector.ma".
     2include "Compare.ma".
     3include "Bool.ma".
     4include "Maybe.ma".
    55
    66ninductive BitVectorTrie (A: Type[0]): Nat → Type[0] ≝
     
    9292nqed.
    9393
    94 ncheck length.
    95 
    9694(*
    9795nlemma test:
     
    104102  #N H V IH.
    105103  ncases H.
    106 *)
    107104
    108105nlemma insert_lookup_leaf:
     
    118115  @.
    119116  #N H V IH.
     117*)
  • Deliverables/D4.1/Matita/List.ma

    r247 r248  
    55include "Util.ma".
    66include "Universes.ma".
     7include "Bool.ma".
    78include "Nat.ma".
    89(* include "Maybe.ma". *)
     
    3940(* Lookup.                                                                    *)
    4041(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    41      
     42   
     43(*   
    4244nlet rec get_index (A: Type[0]) (l: List A) (n: Nat) on n ≝
    4345  match n with
     
    8486          ]
    8587    ].
     88*)
    8689   
    8790(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    205208    ].
    206209   
    207 nlet rec member_with (A: Type[0]) (a: A) (f: A → A → Bool) (l: List A) on l
    208   match l with
    209     [ Empty ⇒ False
     210nlet rec member_with (A: Type[0]) (a: A) (f: A → A → Bool) (l: List A) on l: Bool
     211  match l with
     212    [ Empty ⇒ cic:/matita/Cerco/Bool/Bool.con(0,2,0)
    210213    | Cons hd tl ⇒ inclusive_disjunction (f hd a) (member_with A a f tl)
    211214    ].
     
    318321  nelim l.
    319322  nnormalize.
    320   napplyS append_empty_left_neutral.
     323  nrewrite > (append_empty_left_neutral ? ?).
     324  @.
    321325  #H L A.
    322326  nnormalize.
    323327  nrewrite > A.
    324   napplyS append_associative.
     328  nrewrite > (append_associative ? (reverse ? m) (reverse ? L) (Cons ? H (Empty ?))).
     329  @.
    325330nqed.
    326331
     
    378383  #H L H2.
    379384  nnormalize.
    380   //.
     385  nrewrite > H2.
     386  @.
    381387nqed.
    382388
     
    391397  #H L H2.
    392398  nnormalize.
    393   //.
    394 nqed.
    395 
     399  nrewrite > H2.
     400  @.
     401nqed.
     402
     403(*
    396404nlemma empty_get_index_nothing:
    397405  ∀A: Type[0].
     
    404412  //.
    405413nqed.
     414*)
    406415
    407416nlemma rotate_right_empty:
  • Deliverables/D4.1/Matita/Vector.ma

    r246 r248  
    1111include "List.ma".
    1212include "Cartesian.ma".
    13 
     13include "Maybe.ma".
    1414include "Equality.ma".
    1515
     
    221221    | Cons o hd tl ⇒ ? (append A o ? (reverse A o tl) (Cons A Z hd (Empty A)))
    222222    ].
     223    nrewrite < (succ_plus ? ?).
     224    nrewrite > (plus_zero ?).
    223225    //.
    224226nqed.
     
    262264          ]
    263265    ].
     266    nrewrite < (succ_plus ? ?).
     267    nrewrite > (plus_zero ?).
    264268    //.
    265269nqed.
Note: See TracChangeset for help on using the changeset viewer.