Changeset 1515 for src/ASM/ASM.ma


Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (9 years ago)
Author:
campbell
Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r1493 r1515  
    11include "ASM/BitVector.ma".
    2 
    3 definition Identifier ≝ Word.
     2include "common/Identifiers.ma".
     3include "common/CostLabel.ma".
     4
     5axiom ASMTag : String.
     6definition Identifier ≝ identifier ASMTag.
     7definition toASM_ident : ∀tag. identifier tag → Identifier ≝ λt,i. match i with [ an_identifier id ⇒ an_identifier ASMTag id ].
    48
    59inductive addressing_mode: Type[0] ≝
     
    194198  | Instruction: preinstruction Identifier → pseudo_instruction
    195199  | Comment: String → pseudo_instruction
    196   | Cost: Identifier → pseudo_instruction
     200  | Cost: costlabel → pseudo_instruction
    197201  | Jmp: Identifier → pseudo_instruction
    198202  | Call: Identifier → pseudo_instruction
Note: See TracChangeset for help on using the changeset viewer.