Ignore:
Timestamp:
Nov 24, 2010, 5:18:11 PM (9 years ago)
Author:
sacerdot
Message:

More curryfication.

File:
1 edited

Legend:

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

    r271 r278  
    110110
    111111ninductive preinstruction (A: Type[0]) : Type[0] ≝
    112    ADD: [[acc_a]] -> [[ register ; direct ; indirect ; data ]] -> preinstruction A
    113  | ADDC: [[acc_a]] × [[ register ; direct ; indirect ; data ]] -> preinstruction A
    114  | SUBB: [[acc_a]] × [[ register ; direct ; indirect ; data ]] -> preinstruction A
    115  | INC: [[ acc_a ; register ; direct ; indirect ; dptr ]] -> preinstruction A
    116  | DEC: [[ acc_a ; register ; direct ; indirect ]] -> preinstruction A
    117  | MUL: [[acc_a]] × [[acc_b]] -> preinstruction A
    118  | DIV: [[acc_a]] × [[acc_b]] -> preinstruction A
    119  | DA: [[acc_a]] -> preinstruction A
     112   ADD: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
     113 | ADDC: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
     114 | SUBB: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
     115 | INC: [[ acc_a ; register ; direct ; indirect ; dptr ]] preinstruction A
     116 | DEC: [[ acc_a ; register ; direct ; indirect ]] preinstruction A
     117 | MUL: [[acc_a]] → [[acc_b]] → preinstruction A
     118 | DIV: [[acc_a]] → [[acc_b]] → preinstruction A
     119 | DA: [[acc_a]] preinstruction A
    120120
    121121 (* logical operations *)
     
    123123   [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
    124124   [[direct]] × [[ acc_a ; data ]] ⊎
    125    [[carry]] × [[ bit_addr ; n_bit_addr]] -> preinstruction A
     125   [[carry]] × [[ bit_addr ; n_bit_addr]] preinstruction A
    126126 | ORL:
    127127   [[acc_a]] × [[ register ; data ; direct ; indirect ]] ⊎
    128128   [[direct]] × [[ acc_a ; data ]] ⊎
    129    [[carry]] × [[ bit_addr ; n_bit_addr]] -> preinstruction A
     129   [[carry]] × [[ bit_addr ; n_bit_addr]] preinstruction A
    130130 | XRL:
    131131   [[acc_a]] × [[ data ; register ; direct ; indirect ]] ⊎
    132    [[direct]] × [[ acc_a ; data ]] -> preinstruction A
    133  | CLR: [[ acc_a ; carry ; bit_addr ]] -> preinstruction A
    134  | CPL: [[ acc_a ; carry ; bit_addr ]] -> preinstruction A
    135  | RL: [[acc_a]] -> preinstruction A
    136  | RLC: [[acc_a]] -> preinstruction A
    137  | RR: [[acc_a]] -> preinstruction A
    138  | RRC: [[acc_a]] -> preinstruction A
    139  | SWAP: [[acc_a]] -> preinstruction A
     132   [[direct]] × [[ acc_a ; data ]] preinstruction A
     133 | CLR: [[ acc_a ; carry ; bit_addr ]] preinstruction A
     134 | CPL: [[ acc_a ; carry ; bit_addr ]] preinstruction A
     135 | RL: [[acc_a]] preinstruction A
     136 | RLC: [[acc_a]] preinstruction A
     137 | RR: [[acc_a]] preinstruction A
     138 | RRC: [[acc_a]] preinstruction A
     139 | SWAP: [[acc_a]] preinstruction A
    140140
    141141 (* data transfer *)
     
    146146    [[dptr]] × [[data16]] ⊎
    147147    [[carry]] × [[bit_addr]] ⊎
    148     [[bit_addr]] × [[carry]] -> preinstruction A
    149  | MOVC: [[acc_a]] × [[ acc_dptr ; acc_pc ]] -> preinstruction A
     148    [[bit_addr]] × [[carry]] preinstruction A
     149 | MOVC: [[acc_a]] × [[ acc_dptr ; acc_pc ]] preinstruction A
    150150 | MOVX:
    151151    [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
    152     [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] -> preinstruction A
    153  | SETB: [[ carry ; bit_addr ]] -> preinstruction A
    154  | PUSH: [[direct]] -> preinstruction A
    155  | POP: [[direct]] -> preinstruction A
    156  | XCH: [[acc_a]] × [[ register ; direct ; indirect ]] -> preinstruction A
    157  | XCHD: [[acc_a]] × [[indirect]] -> preinstruction A
     152    [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] preinstruction A
     153 | SETB: [[ carry ; bit_addr ]] preinstruction A
     154 | PUSH: [[direct]] preinstruction A
     155 | POP: [[direct]] preinstruction A
     156 | XCH: [[acc_a]] → [[ register ; direct ; indirect ]] → preinstruction A
     157 | XCHD: [[acc_a]] → [[indirect]] → preinstruction A
    158158
    159159 (* program branching *)
    160160 | Jump: jump A → preinstruction A
    161  | ACALL: [[addr11]] -> preinstruction A
    162  | LCALL: [[addr16]] -> preinstruction A
     161 | ACALL: [[addr11]] preinstruction A
     162 | LCALL: [[addr16]] preinstruction A
    163163 | RET: preinstruction A
    164164 | RETI: preinstruction A
    165  | AJMP: [[addr11]] -> preinstruction A
    166  | LJMP: [[addr16]] -> preinstruction A
    167  | SJMP: [[relative]] -> preinstruction A
    168  | JMP: [[indirect_dptr]] -> preinstruction A
     165 | AJMP: [[addr11]] preinstruction A
     166 | LJMP: [[addr16]] preinstruction A
     167 | SJMP: [[relative]] preinstruction A
     168 | JMP: [[indirect_dptr]] preinstruction A
    169169 | NOP: preinstruction A.
    170170
     
    176176 | Jmp: String → labelled_instruction
    177177 | Call: String → labelled_instruction
    178  | Mov: [[dptr]] × String → labelled_instruction
     178 | Mov: [[dptr]] String → labelled_instruction
    179179 | WithLabel: preinstruction String → labelled_instruction.
    180180
Note: See TracChangeset for help on using the changeset viewer.