Changeset 698 for src/ASM/ASM.ma


Ignore:
Timestamp:
Mar 18, 2011, 1:47:53 PM (9 years ago)
Author:
mulligan
Message:

Commit with changes to files to get our files to typecheck.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r690 r698  
    1 include "cerco/BitVector.ma".
    2 include "cerco/String.ma".
     1include "common/AST.ma".
    32
    43inductive addressing_mode: Type[0] ≝
     
    65| INDIRECT: Bit → addressing_mode
    76| EXT_INDIRECT: Bit → addressing_mode
    8 | REGISTER: BitVector (S (S (S O))) → addressing_mode
     7| REGISTER: BitVector 3 → addressing_mode
    98| ACC_A: addressing_mode
    109| ACC_B: addressing_mode
     
    191190inductive labelled_instruction: Type[0] ≝
    192191  Instruction: instruction → labelled_instruction
    193 | Cost: String → labelled_instruction
    194 | Jmp: String → labelled_instruction
    195 | Call: String → labelled_instruction
    196 | Mov: [[dptr]] → String → labelled_instruction
    197 | Label: String → labelled_instruction
    198 | WithLabel: jump String → labelled_instruction.
    199 
    200 definition preamble ≝ list (String × nat).
     192| Cost: Identifier → labelled_instruction
     193| Jmp: Identifier → labelled_instruction
     194| Call: Identifier → labelled_instruction
     195| Mov: [[dptr]] → Identifier → labelled_instruction
     196| Label: Identifier → labelled_instruction
     197| WithLabel: jump Identifier → labelled_instruction.
     198
     199definition preamble ≝ list (Identifier × nat).
    201200
    202201definition assembly_program ≝ preamble × (list labelled_instruction).
Note: See TracChangeset for help on using the changeset viewer.