Changeset 10 for C-semantics/AST.ma

Timestamp:

Jul 6, 2010, 11:53:23 AM (11 years ago)

Author:

campbell

Message:

Add binary arithmetic libraries, use for integers and identifiers (but
we're not doing modular arithmetic yet.)
Add a dummy "tree" implementation to make environment lookups executable.
Fix if .. then .. else .. precedence.

File:

• C-semantics/AST.ma (modified) (3 diffs)

C-semantics/AST.ma

@@ -21 +21 @@
 include "Integers.ma".
 include "Floats.ma".
+include "binary/positive.ma".
 
 (* * * Syntactic elements *)
@@ -26 +27 @@
 (* * Identifiers (names of local variables, of global symbols and functions,
   etc) are represented by the type [positive] of positive integers. *)
+
+ndefinition ident ≝ Pos.
+
+ndefinition ident_eq : ∀x,y:ident. (x=y) + (x≠y).
+#x y; nlapply (pos_compare_to_Prop x y); ncases (pos_compare x y);
+##[ #H; @2; /2/; ##| #H; @1; //; ##| #H; @2; /2/ ##] nqed.
+
 (*
-Definition ident := positive.
-
-Definition ident_eq := peq.
-*)
 (* XXX: we use nats for now, but if in future we use binary like compcert
         then the maps will be easier to define. *)
@@ -45 +49 @@
   ##]
 ##] nqed. 
-
+*)
 (* * The intermediate languages are weakly typed, using only two types:
   [Tint] for integers and pointers, and [Tfloat] for floating-point