Changeset 262


Ignore:
Timestamp:
Nov 23, 2010, 4:39:31 PM (9 years ago)
Author:
sacerdot
Message:
  • new notation ...? for vectors to reduce ambiguity
  • preinstruction type ported to Matita
Location:
Deliverables/D4.1/Matita
Files:
3 edited

Legend:

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

    r260 r262  
    55include "BitVectorTrie.ma".
    66
    7 ninductive all_types : Type[0] ≝
    8    reg: all_types | direct: all_types | indirect:all_types | data:all_types
    9    | acc: all_types | rel: all_types.
    10 
    117interpretation "Cartesian" 'product A B = (Cartesian A B).
    12 interpretation "Either" 'plus A B = (Either A B).
     8notation "hvbox(a break ⊎ b)"
     9 left associative with precedence 50
     10for @{ 'disjoint_union $a $b }.
     11interpretation "Either" 'disjoint_union A B = (Either A B).
     12interpretation "Bool" 'or a b = (inclusive_disjunction a b).
    1313
    1414ninductive addressing_mode: Type[0] ≝
    1515  DIRECT: Byte → addressing_mode
    1616| INDIRECT: Bit → addressing_mode
    17 | EXTINDIRECT: Bit → addressing_mode
     17| EXT_INDIRECT: Bit → addressing_mode
    1818| REGISTER: Bit → Bit → Bit → addressing_mode
    19 | ACCUMULATORA: addressing_mode
    20 | ACCUMULATORB: addressing_mode
    21 | DPOINTER: addressing_mode
     19| ACC_A: addressing_mode
     20| ACC_B: addressing_mode
     21| DPTR: addressing_mode
    2222| DATA: Byte → addressing_mode
    2323| DATA16: Word → addressing_mode
    24 | ACCUMULATORDPOINTER: addressing_mode
    25 | ACCUMULATORPROGRAMCOUNTER: addressing_mode
    26 | EXTERNALINDIRECTDPOINTER: addressing_mode
    27 | INDIRECTDPOINTER: addressing_mode
     24| ACC_DPTR: addressing_mode
     25| ACC_PC: addressing_mode
     26| EXT_INDIRECT_DPTR: addressing_mode
     27| INDIRECT_DPTR: addressing_mode
    2828| CARRY: addressing_mode
    29 | BIT: Bit → addressing_mode
    30 | COMPLEMENTBITADDRESS: Bit → addressing_mode
     29| BIT_ADDR: Bit → addressing_mode
     30| N_BIT_ADDR: Bit → addressing_mode
    3131| RELATIVE: Byte → addressing_mode
    32 | ADDRESS11: Word11 → addressing_mode
    33 | ADDRESS16: Word → addressing_mode.
     32| ADDR11: Word11 → addressing_mode
     33| ADDR16: Word → addressing_mode.
     34
     35ninductive addressing_mode_tag : Type[0] ≝
     36  direct: addressing_mode_tag
     37| indirect: addressing_mode_tag
     38| ext_indirect: addressing_mode_tag
     39| register: addressing_mode_tag
     40| acc_a: addressing_mode_tag
     41| acc_b: addressing_mode_tag
     42| dptr: addressing_mode_tag
     43| data: addressing_mode_tag
     44| data16: addressing_mode_tag
     45| acc_dptr: addressing_mode_tag
     46| acc_pc: addressing_mode_tag
     47| ext_indirect_dptr: addressing_mode_tag
     48| indirect_dptr: addressing_mode_tag
     49| carry: addressing_mode_tag
     50| bit_addr: addressing_mode_tag
     51| n_bit_addr: addressing_mode_tag
     52| relative: addressing_mode_tag
     53| addr11: addressing_mode_tag
     54| addr16: addressing_mode_tag.
    3455
    3556(* to avoid expansion... *)
    36 nlet rec is_a (d:all_types) (A:addressing_mode) on d ≝
     57nlet rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
    3758  match d with
    38    [ reg ⇒ match A with [ REGISTER _ _ _ ⇒ true | _ ⇒ false ]
     59   [ direct ⇒ match A with [ DIRECT _ ⇒ true | _ ⇒ false ]
     60   | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]
     61   | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ]
     62   | register ⇒ match A with [ REGISTER _ _ _ ⇒ true | _ ⇒ false ]
     63   | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ]
     64   | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ]
     65   | dptr ⇒ match A with [ DPTR ⇒ true | _ ⇒ false ]
    3966   | data ⇒ match A with [ DATA _ ⇒ true | _ ⇒ false ]
    40    | rel ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ]
    41    | acc ⇒ match A with [ ACCUMULATORA ⇒ true | _ ⇒ false ]
    42    | direct ⇒ match A with [ DIRECT _ ⇒ true | _ ⇒ false ]
    43    | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]].
    44 
    45 interpretation "Bool" 'or a b = (inclusive_disjunction a b).
    46 
    47 nlet rec is_in n (l: Vector all_types (S n)) (A:addressing_mode) on l : Bool ≝
    48  match l return λm.λ_:Vector all_types m .∀K:m=S n.Bool with
     67   | data16 ⇒ match A with [ DATA16 _ ⇒ true | _ ⇒ false ]
     68   | acc_dptr ⇒ match A with [ ACC_DPTR ⇒ true | _ ⇒ false ]
     69   | acc_pc ⇒ match A with [ ACC_PC ⇒ true | _ ⇒ false ]
     70   | ext_indirect_dptr ⇒ match A with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
     71   | indirect_dptr ⇒ match A with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
     72   | carry ⇒ match A with [ CARRY ⇒ true | _ ⇒ false ]
     73   | bit_addr ⇒ match A with [ BIT_ADDR _ ⇒ true | _ ⇒ false ]
     74   | n_bit_addr ⇒ match A with [ N_BIT_ADDR _ ⇒ true | _ ⇒ false ]
     75   | relative ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ]
     76   | addr11 ⇒ match A with [ ADDR11 _ ⇒ true | _ ⇒ false ]
     77   | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ]].
     78
     79nlet rec is_in n (l: Vector addressing_mode_tag (S n)) (A:addressing_mode) on l : Bool ≝
     80 match l return λm.λ_:Vector addressing_mode_tag m .∀K:m=S n.Bool with
    4981  [ Empty ⇒ λK.⊥
    50   | Cons m he (tl: Vector all_types m) ⇒ λ_.
     82  | Cons m he (tl: Vector addressing_mode_tag m) ⇒ λ_.
    5183     match m return λz.m = z → Bool with
    5284      [ Z ⇒ λ_.is_a he A
    5385      | S p ⇒ λK.is_a he A ∨ is_in p (? tl) A] (?: m=m)] (?: S n = S n).
     86(* CSC: cast not working here: why? *)
    5487##[##4: #x; ncases K; napply x ]
    5588//; ndestruct.
    5689nqed.
    5790
    58 nrecord subaddressing_mode (n) (l: Vector all_types (S n)) : Type[0] ≝
     91ndefinition bool_to_Prop ≝
     92 λb. match b with [ true ⇒ True | false ⇒ False ].
     93
     94nrecord subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
    5995 { subaddressing_modeel:> addressing_mode;
    60    subaddressing_modein:
    61     match is_in ? l subaddressing_modeel with [ true ⇒ (? : Prop) | false ⇒ (? : Prop) ]
     96   subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
    6297 }.
    63 ##[ napply True | napply False ]
    64 nqed.
    65 
    66 ncoercion subaddressing_mode : ∀n.∀l:Vector all_types (S n).Type[0]
    67  ≝ subaddressing_mode on _l: Vector all_types (S ?) to Type[0].
    68 
    69 (*
     98
     99ncoercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0]
     100 ≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0].
     101
    70102ncoercion mk_subaddressing_mode :
    71  ∀n.∀l:Vector all_types (S n).∀a:addressing_mode.
    72   ∀p:?(*match is_in ? l a return λ_.Prop with [True ⇒ True | False ⇒ False]*).subaddressing_mode n l
    73  ≝ mk_subaddressing_mode on _a:addressing_mode to subaddressing_mode ? ?.
    74 *)
    75 
    76 ninductive Jump (A: Type[0]): Type[0] ≝
    77   JC: A → Jump A
    78 | JNC: A → Jump A
    79 | JB: Bit → A → Jump A
    80 | JNB: Bit → A → Jump A
    81 | JBC: Bit → A → Jump A
    82 | JZ: A → Jump A
    83 | JNZ: A → Jump A
    84 | CJNE: (([acc] × [direct; data]) + [reg; indirect] × [data]) → A → Jump A
    85 | DJNZ: [reg ; direct] → A → Jump A
    86 | ADD: [acc] → [reg; direct; indirect; data] → Jump A.
    87 
    88 ndefinition xxx: Jump Nat.
    89  napply (DJNZ ? (mk_subaddressing_mode ?? (REGISTER [true] [true] [true]) ?) (Z: Nat)).
     103 ∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode.
     104  ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l
     105 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
     106
     107ninductive jump (A: Type[0]): Type[0] ≝
     108  JC: A → jump A
     109| JNC: A → jump A
     110| JB: Bit → A → jump A
     111| JNB: Bit → A → jump A
     112| JBC: Bit → A → jump A
     113| JZ: A → jump A
     114| JNZ: A → jump A
     115| CJNE:
     116   [[acc_a]] × [[direct; data]] ⊎
     117   [[register; indirect]] × [[data]] → A → jump A
     118| DJNZ: [[register ; direct]] → A → jump A.
     119
     120ninductive preinstruction (A: Type[0]) : Type[0] ≝
     121   ADD: [[acc_a]] × [[ register ; direct ; indirect ; data ]] -> preinstruction A
     122 | ADDC: [[acc_a]] × [[ register ; direct ; indirect ; data ]] -> preinstruction A
     123 | SUBB: [[acc_a]] × [[ register ; direct ; indirect ; data ]] -> preinstruction A
     124 | INC: [[ acc_a ; register ; direct ; indirect ; dptr ]] -> preinstruction A
     125 | DEC: [[ acc_a ; register ; direct ; indirect ]] -> preinstruction A
     126 | MUL: [[acc_a]] × [[acc_b]] -> preinstruction A
     127 | DIV: [[acc_a]] × [[acc_b]] -> preinstruction A
     128 | DA: [[acc_a]] -> preinstruction A
     129
     130 (* logical operations *)
     131 | ANL:
     132   [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
     133   [[direct]] × [[ acc_a ; data ]] ⊎
     134   [[carry]] × [[ bit_addr ; n_bit_addr]] -> preinstruction A
     135 | ORL:
     136   [[acc_a]] × [[ register ; data ; direct ; indirect ]] ⊎
     137   [[direct]] × [[ acc_a ; data ]] ⊎
     138   [[carry]] × [[ bit_addr ; n_bit_addr]] -> preinstruction A
     139 | XRL:
     140   [[acc_a]] × [[ data ; register ; direct ; indirect ]] ⊎
     141   [[direct]] × [[ acc_a ; data ]] -> preinstruction A
     142 | CLR: [[ acc_a ; carry ; bit_addr ]] -> preinstruction A
     143 | CPL: [[ acc_a ; carry ; bit_addr ]] -> preinstruction A
     144 | RL: [[acc_a]] -> preinstruction A
     145 | RLC: [[acc_a]] -> preinstruction A
     146 | RR: [[acc_a]] -> preinstruction A
     147 | RRC: [[acc_a]] -> preinstruction A
     148 | SWAP: [[acc_a]] -> preinstruction A
     149
     150 (* data transfer *)
     151 | MOV:
     152    [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
     153    [[ register ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
     154    [[direct]] × [[ acc_a ; register ; direct ; indirect ; data ]] ⊎
     155    [[dptr]] × [[data16]] ⊎
     156    [[carry]] × [[bit_addr]] ⊎
     157    [[bit_addr]] × [[carry]] -> preinstruction A
     158 | MOVC: [[acc_a]] × [[ acc_dptr ; acc_pc ]] -> preinstruction A
     159 | MOVX:
     160    [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
     161    [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] -> preinstruction A
     162 | SETB: [[ carry ; bit_addr ]] -> preinstruction A
     163 | PUSH: [[direct]] -> preinstruction A
     164 | POP: [[direct]] -> preinstruction A
     165 | XCH: [[acc_a]] × [[ register ; direct ; indirect ]] -> preinstruction A
     166 | XCHD: [[acc_a]] × [[indirect]] -> preinstruction A
     167
     168 (* program branching *)
     169 | Jump: jump A → preinstruction A
     170 | ACALL: [[addr11]] -> preinstruction A
     171 | LCALL: [[addr16]] -> preinstruction A
     172 | RET: preinstruction A
     173 | RETI: preinstruction A
     174 | AJMP: [[addr11]] -> preinstruction A
     175 | LJMP: [[addr16]] -> preinstruction A
     176 | SJMP: [[relative]] -> preinstruction A
     177 | JMP: [[indirect_dptr]] -> preinstruction A
     178 | NOP: preinstruction A.
     179
     180
     181ndefinition xxx: jump Nat.
     182 napply (DJNZ ? (REGISTER [true] [true] [true]) Z).
    90183 napply I;
    91184nqed.
  • Deliverables/D4.1/Matita/BitVector.ma

    r260 r262  
    4141  λb: BitVector n.
    4242  λm: Nat.
    43     set_index Bool n b m.
     43    set_index_weak Bool n b m.
    4444   
    4545ndefinition drop ≝
  • Deliverables/D4.1/Matita/Vector.ma

    r261 r262  
    2626(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    2727
    28 interpretation "Vector nil" 'nil = (Empty ?).
     28notation "[[ list0 x sep ; ]]"
     29  non associative with precedence 90
     30  for ${fold right @'vnil rec acc @{'vcons $x $acc}}.
     31
     32interpretation "Vector vnil" 'vnil = (Empty ?).
     33interpretation "Vector vcons" 'vcons hd tl = (Cons ? ? hd tl).
    2934interpretation "Vector cons" 'cons hd tl = (Cons ? ? hd tl).
    30 
    31 notation "hvbox (v break !! n)"
    32   non associative with precedence 90
    33   for @{ 'get_index $v $n }.
    3435
    3536(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    8182   
    8283interpretation "Vector get_index" 'get_index v n = (get_index ? ? v n).
    83    
     84
     85(*
    8486nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝
    8587  (match m with
     
    98100    nassumption.
    99101nqed.
     102*)
    100103   
    101104nlet rec set_index_weak (A: Type[0]) (n: Nat)
     
    224227    ].
    225228   
    226 notation "v break @ q"
    227   right associative with precedence 47
    228   for @{ 'append $v $q }.
    229  
    230229interpretation "Vector append" 'append hd tl = (append ? ? hd tl).
    231230   
Note: See TracChangeset for help on using the changeset viewer.