Changeset 1882 for src/ASM/ASM.ma


Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (9 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r1522 r1882  
    22include "common/Identifiers.ma".
    33include "common/CostLabel.ma".
     4include "common/LabelledObjects.ma".
    45
    56axiom ASMTag : String.
     
    203204  | Mov: [[dptr]] → Identifier → pseudo_instruction.
    204205
    205 definition labelled_instruction ≝ option Identifier × pseudo_instruction.
     206definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction.
    206207definition preamble ≝ (identifier_map SymbolTag nat) × (list (Identifier × Word)).
    207208definition assembly_program ≝ list instruction.
Note: See TracChangeset for help on using the changeset viewer.