Changeset 271


Ignore:
Timestamp:
Nov 24, 2010, 1:00:41 AM (9 years ago)
Author:
sacerdot
Message:

assembly1 defined on ACALL and ADD: it seems it will become too slow...

Location:
Deliverables/D4.1/Matita
Files:
4 edited

Legend:

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

    r268 r271  
    110110
    111111ninductive preinstruction (A: Type[0]) : Type[0] ≝
    112    ADD: [[acc_a]] × [[ register ; direct ; indirect ; data ]] -> preinstruction A
     112   ADD: [[acc_a]] -> [[ register ; direct ; indirect ; data ]] -> preinstruction A
    113113 | ADDC: [[acc_a]] × [[ register ; direct ; indirect ; data ]] -> preinstruction A
    114114 | SUBB: [[acc_a]] × [[ register ; direct ; indirect ; data ]] -> preinstruction A
  • Deliverables/D4.1/Matita/Assembly.ma

    r269 r271  
    11include "ASM.ma".
    22
     3(*
     4ndefinition from_addressing_mode_tag ≝
     5 λT:Type[0].λt:addressing_mode_tag.
     6  match t with
     7   [ direct ⇒ Byte → T
     8   | indirect ⇒ Bit → T
     9   | ext_indirect ⇒ Bit → T
     10   | register ⇒ Bit → Bit → Bit → T
     11   | acc_a ⇒ T
     12   | acc_b ⇒ T
     13   | dptr ⇒ T
     14   | data ⇒ Byte → T
     15   | data16 ⇒ Word → T
     16   | acc_dptr ⇒ T
     17   | acc_pc ⇒ T
     18   | ext_indirect_dptr ⇒ T
     19   | indirect_dptr ⇒ T
     20   | carry ⇒ T
     21   | bit_addr ⇒ Bit → T
     22   | n_bit_addr ⇒ Bit → T
     23   | relative ⇒ Byte → T
     24   | addr11 ⇒ Word11 → T
     25   | addr16 ⇒ Word → T ].
     26*)
     27(*
     28nlet rec elim_addr (T:addressing_mode → Type[0]) n l on l
     29: subaddressing_mode n l → Type[0] ≝
     30 match l
     31  return λm.λl:Vector addressing_mode_tag m.
     32   ∀proof:m = S n.
     33    subaddressing_mode n (match proof with [refl ⇒ l]) → Type[0] with
     34  [ Empty ⇒ λK.λ_.Nat
     35  | Cons o he tl ⇒ λK.λv.Nat(*
     36     match o
     37      return λy.∀p:S y = S n.
     38       subaddressing_mode y
     39        (v⌈Vector addressing_mode_tag (S y) ↦ Vector addressing_mode_tag (S n)⌉)
     40        → Type[0]
     41     with
     42      [ Z ⇒ λK.λv.(? : Type[0])
     43      | S p ⇒ λK.λv.(? : Type[0])
     44      ]*)
     45  ] (?: S n = S n).
     46##[##1: @
     47  | ndestruct
     48  |##7: //
     49  | normalize;
     50
     51nlet rec elim_addr n (v: Vector addressing_mode_tag (S n)) on v
     52: subaddressing_mode n v Type[0]
     53
     54 match v return λx.λ_.x = S n. Type[0] with
     55  [ Empty ⇒ λK.⊥
     56  | Cons o he tl ⇒ λK.
     57     match o with
     58      [ Z ⇒
     59      | S m ⇒
     60      ]
     61  ] (? : S n = S n).
     62*)
     63
     64notation "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
     65 with precedence 10
     66for @{ match $t with [ mk_Cartesian ${ident x} ${ident y} ⇒ $s ] }.
     67
     68ncheck (let 〈x,z〉 ≝ 〈Z,Z〉 in 〈x,z〉).
     69
    370ndefinition assembly1 ≝
    4  λi.match i with
     71 λA.λi: preinstruction A.match i with
    572  [ ACALL addr ⇒
    6      let w ≝
    7       match addr with [ mk_subaddressing_mode addr1 proof1 ⇒
    8        match addr1 return λx.∀proof: bool_to_Prop (is_in ?? x).? with
    9         [ ADDR11 w ⇒ λ_.w | _ ⇒ λK.⊥ ] proof1] in
    10      match split ?? (S (S (S (S (S (S (S (S Z)))))))) w with
    11       [ mk_Cartesian v1 v2 ⇒
    12          v1 @ [[true; false; false; false; true]] @ v2 ]
    13   | _ ⇒ ? ].
    14 ##[##28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45: napply K;
    15 ##|##47:
    16  
    17       let (a10,a9,a8,b1) = from_word11 w in
    18         [mk_byte_from_bits ((a10,a9,a8,true),(false,false,false,true)); b1]
    19   | `ADD (`A,`REG (r1,r2,r3)) ->
    20      [mk_byte_from_bits ((false,false,true,false),(true,r1,r2,r3))]
    21   | `ADD (`A, `DIRECT b1) ->
    22      [mk_byte_from_bits ((false,false,true,false),(false,true,false,true)); b1]
    23   | `ADD (`A, `INDIRECT i1) ->
    24      [mk_byte_from_bits ((false,false,true,false),(false,true,true,i1))]
    25   | `ADD (`A, `DATA b1) ->
    26      [mk_byte_from_bits ((false,false,true,false),(false,true,false,false)); b1]
     73     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
     74      [ ADDR11 w ⇒ λ_.
     75         let 〈v1,v2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S Z))) w in
     76          [ (v1 @ [[true; false; false; false; true]]) ; v2 ]
     77      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     78  | ADD addr1 addr2 ⇒
     79     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     80      [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;false;true;false;true;r1;r2;r2]]) ]
     81      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
     82      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
     83      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
     84      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     85  | _ ⇒ [ ([[false;false;false;false;false;false;false;false]]) ]].
     86
     87
    2788  | `ADDC (`A, `REG(r1,r2,r3)) ->
    2889     [mk_byte_from_bits ((false,false,true,true),(true,r1,r2,r3))]
  • Deliverables/D4.1/Matita/BitVector.ma

    r270 r271  
    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)))))))))))))))).
    25 ndefinition Word11 ≝ BitVector (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 Z))))))))))).
    2626
    2727(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    200200        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
    201201    ].
    202    
     202
     203(*
    203204nlet rec equality (n: Nat) (b: BitVector n) (c: BitVector n) on b ≝
    204205  match b with
     
    209210    | Cons
    210211    ].
     212*)
  • Deliverables/D4.1/Matita/depends

    r268 r271  
    11Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
     2Status.ma Arithmetic.ma BitVectorTrie.ma
    23Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma
    34BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
     
    1415List.ma Bool.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
    1516Util.ma Nat.ma
    16 Interpret.ma Arithmetic.ma BitVectorTrie.ma
    1717BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma
    1818Compare.ma Universes.ma
Note: See TracChangeset for help on using the changeset viewer.