Changeset 1268 for src/common


Ignore:
Timestamp:
Sep 26, 2011, 2:52:22 PM (8 years ago)
Author:
sacerdot
Message:

1) AST/Identifier.ma no longer used, utilities/IdentifierTools no longer used
2) LIN/LINToAsm porting completed but:

a) a small lemma need to be proved (easy, but boring because of foldl)
b) the code is BUGGED: labels coming from different universes

(for function names and for each function) are merged together.
However, they should be kept clearly separate. We will discuss how
to fix this issue at the next meeting in Paris.
Note: keeping 'em distinct from the very beginning also requires some
work, since some labels are entered directly by the user.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1225 r1268  
    3838definition ident_of_nat : nat → ident ≝ identifier_of_nat ?.
    3939
    40 (* XXX backend is currently using untagged words as identifiers. *)
    41 definition Identifier ≝ Word.
    42 
    4340definition Immediate ≝ nat. (* XXX is this the best place to put this? *)
    4441
     
    675672| Compare_LessEqual: Compare
    676673| Compare_GreaterEqual: Compare.
    677 
    678 (* XXX unused definitions
    679 inductive Cast: Type[0] ≝
    680   Cast_Int: Byte → Cast
    681 | Cast_AddrSymbol: Identifier → Cast
    682 | Cast_StackOffset: Immediate → Cast.
    683 
    684 inductive Data: Type[0] ≝
    685   Data_Reserve: nat → Data
    686 | Data_Int8: Byte → Data
    687 | Data_Int16: Word → Data.
    688 
    689 inductive DataSize: Type[0] ≝
    690   DataSize_Byte: DataSize
    691 | DataSize_HalfWord: DataSize
    692 | DataSize_Word: DataSize.
    693 *)
    694 
    695 definition Trace ≝ list Identifier.
    696674
    697675inductive op1: Type[0] ≝
  • src/common/CostLabel.ma

    r757 r1268  
    77(* For use in importing programs in intermediate languages. *)
    88definition costlabel_of_nat : nat → costlabel ≝ identifier_of_nat ?.
    9 
    10 (* dpm: fix identifier/costlabel mismatch *)
    11 axiom Identifier_of_costlabel: costlabel → Identifier.
Note: See TracChangeset for help on using the changeset viewer.