Changeset 9 for C-semantics/AST.ma


Ignore:
Timestamp:
Jun 21, 2010, 4:22:09 PM (10 years ago)
Author:
campbell
Message:

Enough of an executable semantics to execute a not-quite-trivial program,
plus a patch for compcert to convert C to a matita definition.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/AST.ma

    r3 r9  
    3131Definition ident_eq := peq.
    3232*)
    33 (* TODO: define ident *)
    34 naxiom ident:Type[0].
    35 naxiom ident_eq: ∀x,y:ident. (x=y) + (x≠y).
     33(* XXX: we use nats for now, but if in future we use binary like compcert
     34        then the maps will be easier to define. *)
     35ndefinition ident ≝ nat.
     36ndefinition ident_eq : ∀x,y:ident. (x=y) + (x≠y).
     37#x; nelim x;
     38##[ #y; ncases y; /3/;
     39##| #x'; #IH; #y; ncases y;
     40  ##[ @2; @; #H; ndestruct
     41  ##| #y'; nelim (IH y');
     42    ##[ #e; ndestruct; /2/
     43    ##| #ne; @2; /2/;
     44    ##]
     45  ##]
     46##] nqed.
    3647
    3748(* * The intermediate languages are weakly typed, using only two types:
Note: See TracChangeset for help on using the changeset viewer.