Changeset 757 for src/ASM/ASM.ma


Ignore:
Timestamp:
Apr 18, 2011, 12:30:53 PM (9 years ago)
Author:
mulligan
Message:

Lots more fixing to get both front and backends using same conventions and types.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r722 r757  
    2222| ADDR16: Word → addressing_mode.
    2323
     24(* dpm: renamed register to registr to avoid clash with brian's types *)
    2425inductive addressing_mode_tag : Type[0] ≝
    2526  direct: addressing_mode_tag
    2627| indirect: addressing_mode_tag
    2728| ext_indirect: addressing_mode_tag
    28 | register: addressing_mode_tag
     29| registr: addressing_mode_tag
    2930| acc_a: addressing_mode_tag
    3031| acc_b: addressing_mode_tag
     
    4950      | indirect ⇒ match b with [ indirect ⇒ true | _ ⇒ false ]
    5051      | ext_indirect ⇒ match b with [ ext_indirect ⇒ true | _ ⇒ false ]
    51       | register ⇒ match b with [ register ⇒ true | _ ⇒ false ]
     52      | registr ⇒ match b with [ registr ⇒ true | _ ⇒ false ]
    5253      | acc_a ⇒ match b with [ acc_a ⇒ true | _ ⇒ false ]
    5354      | acc_b ⇒ match b with [ acc_b ⇒ true | _ ⇒ false ]
     
    7374   | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]
    7475   | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ]
    75    | register ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]
     76   | registr ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]
    7677   | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ]
    7778   | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ]
     
    120121| JNZ: A → jump A
    121122| CJNE:
    122    [[acc_a]] × [[direct; data]] ⊎ [[register; indirect]] × [[data]] → A → jump A
    123 | DJNZ: [[register ; direct]] → A → jump A.
     123   [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → jump A
     124| DJNZ: [[registr ; direct]] → A → jump A.
    124125
    125126inductive preinstruction (A: Type[0]) : Type[0] ≝
    126   ADD: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
    127 | ADDC: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
    128 | SUBB: [[acc_a]] → [[ register ; direct ; indirect ; data ]] → preinstruction A
    129 | INC: [[ acc_a ; register ; direct ; indirect ; dptr ]] → preinstruction A
    130 | DEC: [[ acc_a ; register ; direct ; indirect ]] → preinstruction A
     127  ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
     128| ADDC: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
     129| SUBB: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
     130| INC: [[ acc_a ; registr ; direct ; indirect ; dptr ]] → preinstruction A
     131| DEC: [[ acc_a ; registr ; direct ; indirect ]] → preinstruction A
    131132| MUL: [[acc_a]] → [[acc_b]] → preinstruction A
    132133| DIV: [[acc_a]] → [[acc_b]] → preinstruction A
     
    135136 (* logical operations *)
    136137| ANL:
    137    [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
     138   [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
    138139   [[direct]] × [[ acc_a ; data ]] ⊎
    139140   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
    140141| ORL:
    141    [[acc_a]] × [[ register ; data ; direct ; indirect ]] ⊎
     142   [[acc_a]] × [[ registr ; data ; direct ; indirect ]] ⊎
    142143   [[direct]] × [[ acc_a ; data ]] ⊎
    143144   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
    144145| XRL:
    145    [[acc_a]] × [[ data ; register ; direct ; indirect ]] ⊎
     146   [[acc_a]] × [[ data ; registr ; direct ; indirect ]] ⊎
    146147   [[direct]] × [[ acc_a ; data ]] → preinstruction A
    147148| CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
     
    155156 (* data transfer *)
    156157| MOV:
    157     [[acc_a]] × [[ register ; direct ; indirect ; data ]] ⊎
    158     [[ register ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
    159     [[direct]] × [[ acc_a ; register ; direct ; indirect ; data ]] ⊎
     158    [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
     159    [[ registr ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
     160    [[direct]] × [[ acc_a ; registr ; direct ; indirect ; data ]] ⊎
    160161    [[dptr]] × [[data16]] ⊎
    161162    [[carry]] × [[bit_addr]] ⊎
     
    168169| PUSH: [[direct]] → preinstruction A
    169170| POP: [[direct]] → preinstruction A
    170 | XCH: [[acc_a]] → [[ register ; direct ; indirect ]] → preinstruction A
     171| XCH: [[acc_a]] → [[ registr ; direct ; indirect ]] → preinstruction A
    171172| XCHD: [[acc_a]] → [[indirect]] → preinstruction A
    172173
Note: See TracChangeset for help on using the changeset viewer.