Changeset 820 for src/ASM/ASM.ma


Ignore:
Timestamp:
May 20, 2011, 6:09:00 PM (9 years ago)
Author:
mulligan
Message:

changes to get the semantics of pseudoassembly working

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r757 r820  
    112112 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
    113113
    114 inductive jump (A: Type[0]): Type[0] ≝
    115   JC: A → jump A
    116 | JNC: A → jump A
    117 | JB: [[bit_addr]] → A → jump A
    118 | JNB: [[bit_addr]] → A → jump A
    119 | JBC: [[bit_addr]] → A → jump A
    120 | JZ: A → jump A
    121 | JNZ: A → jump A
    122 | CJNE:
    123    [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → jump A
    124 | DJNZ: [[registr ; direct]] → A → jump A.
    125 
    126114inductive preinstruction (A: Type[0]) : Type[0] ≝
    127115  ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
     
    134122| DA: [[acc_a]] → preinstruction A
    135123
     124(* conditional jumps *)
     125| JC: A → preinstruction A
     126| JNC: A → preinstruction A
     127| JB: [[bit_addr]] → A → preinstruction A
     128| JNB: [[bit_addr]] → A → preinstruction A
     129| JBC: [[bit_addr]] → A → preinstruction A
     130| JZ: A → preinstruction A
     131| JNZ: A → preinstruction A
     132| CJNE:
     133   [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → preinstruction A
     134| DJNZ: [[registr ; direct]] → A → preinstruction A
    136135 (* logical operations *)
    137136| ANL:
     
    162161    [[carry]] × [[bit_addr]] ⊎
    163162    [[bit_addr]] × [[carry]] → preinstruction A
    164 | MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → preinstruction A
    165163| MOVX:
    166164    [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
     
    173171
    174172 (* program branching *)
    175 | Jump: jump A → preinstruction A
    176 | ACALL: [[addr11]] → preinstruction A
    177 | LCALL: [[addr16]] → preinstruction A
    178173| RET: preinstruction A
    179174| RETI: preinstruction A
    180 | AJMP: [[addr11]] → preinstruction A
    181 | LJMP: [[addr16]] → preinstruction A
    182 | SJMP: [[relative]] → preinstruction A
    183 | JMP: [[indirect_dptr]] → preinstruction A
    184175| NOP: preinstruction A.
    185176
    186 definition instruction ≝ preinstruction [[relative]].
     177inductive instruction: Type[0] ≝
     178  | ACALL: [[addr11]] → instruction
     179  | LCALL: [[addr16]] → instruction
     180  | AJMP: [[addr11]] → instruction
     181  | LJMP: [[addr16]] → instruction
     182  | SJMP: [[relative]] → instruction
     183  | JMP: [[indirect_dptr]] → instruction
     184  | MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → instruction
     185  | RealInstruction: preinstruction [[ relative ]] → instruction.
     186 
     187coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝
     188  RealInstruction on _p: preinstruction ? to instruction.
    187189
    188190inductive pseudo_instruction: Type[0] ≝
    189   Instruction: instruction → pseudo_instruction
    190 | Comment: String → pseudo_instruction
    191 | Cost: Identifier → pseudo_instruction
    192 | Jmp: Identifier → pseudo_instruction
    193 | Call: Identifier → pseudo_instruction
    194 | Mov: [[dptr]] → Identifier → pseudo_instruction
    195 | WithLabel: jump Identifier → pseudo_instruction.
     191  | Instruction: preinstruction Identifier → pseudo_instruction
     192  | Comment: String → pseudo_instruction
     193  | Cost: Identifier → pseudo_instruction
     194  | Jmp: Identifier → pseudo_instruction
     195  | Call: Identifier → pseudo_instruction
     196  | Mov: [[dptr]] → Identifier → pseudo_instruction.
    196197
    197198definition labelled_instruction ≝ option Identifier × pseudo_instruction.
    198 
    199199definition preamble ≝ list (Identifier × nat).
    200 
    201 definition assembly_program ≝ preamble × (list labelled_instruction).
     200definition assembly_program ≝ list instruction.
     201definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).
Note: See TracChangeset for help on using the changeset viewer.