Changeset 2645 for src/ASM


Ignore:
Timestamp:
Feb 7, 2013, 9:22:22 PM (7 years ago)
Author:
sacerdot
Message:
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
Location:
src/ASM
Files:
1 deleted
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2316 r2645  
    44include "common/LabelledObjects.ma".
    55
    6 axiom ASMTag : String.
    76definition Identifier ≝ identifier ASMTag.
    87definition toASM_ident : ∀tag. identifier tag → Identifier ≝ λt,i. match i with [ an_identifier id ⇒ an_identifier ASMTag id ].
  • src/ASM/BitVector.ma

    r2601 r2645  
    1010include "ASM/FoldStuff.ma".
    1111include "ASM/Vector.ma".
    12 include "ASM/String.ma".
    1312
    1413(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    226225qed.
    227226
    228 (*
    229 axiom bitvector_of_string:
    230   ∀n: nat.
    231   ∀s: String.
    232     BitVector n.
    233    
    234 axiom string_of_bitvector:
    235   ∀n: nat.
    236   ∀b: BitVector n.
    237     String.
    238 *)
    239 
    240227lemma bitvector_3_cases:
    241228  ∀w: BitVector 3.
  • src/ASM/I8051.ma

    r2286 r2645  
    11include "arithmetics/nat.ma".
    22include "basics/jmeq.ma".
    3 
    4 include "ASM/String.ma".
    5 (*include "ASM/ASM.ma".*)
    63include "ASM/Arithmetic.ma". 
    74
     
    104101    eqb r_as_nat s_as_nat.
    105102
    106 axiom print_register: Register → String.
    107 
    108103(* dpm: registers for stack manipulation *)
    109104definition RegisterSST ≝ Register10.
Note: See TracChangeset for help on using the changeset viewer.