Changeset 737 for src/Clight
 Timestamp:
 Apr 4, 2011, 5:13:09 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/AST.ma
r726 r737 22 22 include "common/Floats.ma". 23 23 include "ASM/BitVector.ma". 24 include "common/Identifiers.ma". 24 25 25 26 (* * * Syntactic elements *) 26 27 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 32 axiom SymbolTag : String. 33 34 definition ident ≝ Identifier SymbolTag. 35 36 definition ident_eq : ∀x,y:ident. (x=y) + (x≠y) ≝ identifier_eq ?. 37 38 definition ident_of_nat : nat → ident ≝ identifier_of_nat ?. 40 39 41 40 (* Memory spaces *)
Note: See TracChangeset
for help on using the changeset viewer.