Changeset 1268 for src/common/AST.ma


Ignore:
Timestamp:
Sep 26, 2011, 2:52:22 PM (9 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.

File:
1 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] ≝
Note: See TracChangeset for help on using the changeset viewer.