Changeset 10 for C-semantics/AST.ma


Ignore:
Timestamp:
Jul 6, 2010, 11:53:23 AM (10 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:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/AST.ma

    r9 r10  
    2121include "Integers.ma".
    2222include "Floats.ma".
     23include "binary/positive.ma".
    2324
    2425(* * * Syntactic elements *)
     
    2627(* * Identifiers (names of local variables, of global symbols and functions,
    2728  etc) are represented by the type [positive] of positive integers. *)
     29
     30ndefinition ident ≝ Pos.
     31
     32ndefinition 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
    2836(*
    29 Definition ident := positive.
    30 
    31 Definition ident_eq := peq.
    32 *)
    3337(* XXX: we use nats for now, but if in future we use binary like compcert
    3438        then the maps will be easier to define. *)
     
    4549  ##]
    4650##] nqed.
    47 
     51*)
    4852(* * The intermediate languages are weakly typed, using only two types:
    4953  [Tint] for integers and pointers, and [Tfloat] for floating-point
Note: See TracChangeset for help on using the changeset viewer.