Changeset 10 for C-semantics/AST.ma
- Timestamp:
- Jul 6, 2010, 11:53:23 AM (11 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
C-semantics/AST.ma
r9 r10 21 21 include "Integers.ma". 22 22 include "Floats.ma". 23 include "binary/positive.ma". 23 24 24 25 (* * * Syntactic elements *) … … 26 27 (* * Identifiers (names of local variables, of global symbols and functions, 27 28 etc) are represented by the type [positive] of positive integers. *) 29 30 ndefinition ident ≝ Pos. 31 32 ndefinition ident_eq : ∀x,y:ident. (x=y) + (x≠y). 33 #x y; nlapply (pos_compare_to_Prop x y); ncases (pos_compare x y); 34 ##[ #H; @2; /2/; ##| #H; @1; //; ##| #H; @2; /2/ ##] nqed. 35 28 36 (* 29 Definition ident := positive.30 31 Definition ident_eq := peq.32 *)33 37 (* XXX: we use nats for now, but if in future we use binary like compcert 34 38 then the maps will be easier to define. *) … … 45 49 ##] 46 50 ##] nqed. 47 51 *) 48 52 (* * The intermediate languages are weakly typed, using only two types: 49 53 [Tint] for integers and pointers, and [Tfloat] for floating-point
Note: See TracChangeset
for help on using the changeset viewer.