Changeset 737 for src/Clight/AST.ma


Ignore:
Timestamp:
Apr 4, 2011, 5:13:09 PM (10 years ago)
Author:
campbell
Message:

Use more abstract identifiers in Clight / RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/AST.ma

    r726 r737  
    2222include "common/Floats.ma".
    2323include "ASM/BitVector.ma".
     24include "common/Identifiers.ma".
    2425
    2526(* * * Syntactic elements *)
    2627
    27 (* * Identifiers (names of local variables, of global symbols and functions,
    28   etc) are represented by the type [positive] of positive integers. *)
    29 
    30 definition ident ≝ Word.
    31 
    32 definition ident_eq : ∀x,y:ident. (x=y) + (x≠y).
    33 #x #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %) #E
    34 [ % | %2 ]
    35 lapply E @eq_bv_elim
    36 [ 1,4: #H #_ @H | *: #_ #H destruct ]
    37 qed.
    38 
    39 definition ident_of_nat ≝ bitvector_of_nat 16.
     28(* Global variables and functions are represented by identifiers with the
     29   tag for symbols.  Note that Clight also uses them for locals due to
     30   the ambiguous syntax. *)
     31
     32axiom SymbolTag : String.
     33
     34definition ident ≝ Identifier SymbolTag.
     35
     36definition ident_eq : ∀x,y:ident. (x=y) + (x≠y) ≝ identifier_eq ?.
     37
     38definition ident_of_nat : nat → ident ≝ identifier_of_nat ?.
    4039
    4140(* Memory spaces *)
Note: See TracChangeset for help on using the changeset viewer.