Changeset 13

Timestamp:

Jul 19, 2010, 4:30:09 PM (11 years ago)

Author:

campbell

Message:

Minor syntactic changes.

Location:

C-semantics

Files:

• Cexec.ma (modified) (5 diffs)
• Csem.ma (modified) (9 diffs)

C-semantics/Cexec.ma

@@ -323 +323 @@
   match e' with
   [ Evar id ⇒ 
-      match (get ? PTree ? id en) with
-      [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol Genv ? ge id);: OK ? 〈l,zero〉) (* global *)
+      match (get … id en) with
+      [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈l,zero〉) (* global *)
       | Some l ⇒ Some ? (OK ? 〈l,zero〉) (* local *)
       ]
@@ -388 +388 @@
   match h with [ mk_pair id ty ⇒
     match alloc m 0 (sizeof ty) with [ mk_pair m1 b1 ⇒
-      match exec_alloc_variables (set ? PTree ? id b1 en) m1 vars with
+      match exec_alloc_variables (set … id b1 en) m1 vars with
       [ sig_intro r p ⇒ r ]
 ]]]. nwhd; //;
-nelim (exec_alloc_variables (set ident PTree block c3 c7 en) c6 c1);
+nelim (exec_alloc_variables (set ident ? block c3 c7 en) c6 c1);
 #H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
 napply (alloc_variables_cons … IH); /2/;
@@ -404 +404 @@
       [ nil ⇒ Some ? (Error ?)
       | cons v1 vl ⇒ Some ? (
-          b ← opt_to_res ? (get ? PTree ? id e);:
+          b ← opt_to_res ? (get … id e);:
           m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);:
           err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
@@ -511 +511 @@
     vf ← exec_expr ge e m a;:
     vargs ← exec_exprlist ge e m al;:
-    fd ← opt_to_res ? (find_funct Genv ? ge vf);:
+    fd ← opt_to_res ? (find_funct ? ? ge vf);:
     p ← assert_type_eq (type_of_fundef fd) (typeof a);:
     k' ← match lhs with
@@ -609 +609 @@
   let m0 ≝ init_mem Genv ?? p in
   Some ? (
-    b ← opt_to_res ? (find_symbol Genv ? ge (prog_main ?? p));:
-    f ← opt_to_res ? (find_funct_ptr Genv ? ge b);:
+    b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));:
+    f ← opt_to_res ? (find_funct_ptr ? ? ge b);:
     OK ? (Callstate f (nil ?) Kstop m0)).
 nwhd;

C-semantics/Csem.ma

@@ -444 +444 @@
 ndefinition env ≝ (tree_t ? PTree) block. (* map variable -> location *)
 
-ndefinition empty_env: env ≝ (empty ? PTree block).
+ndefinition empty_env: env ≝ (empty …).
 
 (* * [load_value_of_type ty m b ofs] computes the value of a datum
@@ -487 +487 @@
       ∀e,m,id,ty,vars,m1,b1,m2,e2.
       alloc m 0 (sizeof ty) = 〈m1, b1〉 →
-      alloc_variables (set ? PTree ? id b1 e) m1 vars e2 m2 →
+      alloc_variables (set … id b1 e) m1 vars e2 m2 →
       alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
 
@@ -503 +503 @@
   | bind_parameters_cons:
       ∀e,m,id,ty,params,v1,vl,b,m1,m2.
-      get ? PTree ? id e = Some ? b →
+      get ??? id e = Some ? b →
       store_value_of_type ty m b zero v1 = Some ? m1 →
       bind_parameters e m1 params vl m2 →
@@ -511 +511 @@
 
 ndefinition blocks_of_env : env → list block ≝ λe.
-  map ?? (snd ident block) (elements ? PTree ? e).
+  map ?? (snd ident block) (elements ??? e).
 
 (* * Selection of the appropriate case of a [switch], given the value [n]
@@ -611 +611 @@
 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr -> block -> int -> Prop ≝
   | eval_Evar_local:   ∀id,l,ty.
-      (* XXX notation? e!id*) get ? PTree ? id e = Some ? l ->
+      (* XXX notation? e!id*) get ??? id e = Some ? l ->
       eval_lvalue ge e m (Expr (Evar id) ty) l zero
   | eval_Evar_global: ∀id,l,ty.
-      (* XXX e!id *) get ? PTree ? id e = None ? ->
-      find_symbol Genv ? ge id = Some ? l ->
+      (* XXX e!id *) get ??? id e = None ? ->
+      find_symbol ?? ge id = Some ? l ->
       eval_lvalue ge e m (Expr (Evar id) ty) l zero
   | eval_Ederef: ∀a,ty,l,ofs.
@@ -774 +774 @@
       eval_expr ge e m a vf ->
       eval_exprlist ge e m al vargs ->
-      find_funct Genv ? ge vf = Some ? fd ->
+      find_funct ?? ge vf = Some ? fd ->
       type_of_fundef fd = typeof a ->
       step ge (State f (Scall (None ?) a al) k e m)
@@ -783 +783 @@
       eval_expr ge e m a vf ->
       eval_exprlist ge e m al vargs ->
-      find_funct Genv ? ge vf = Some ? fd ->
+      find_funct ?? ge vf = Some ? fd ->
       type_of_fundef fd = typeof a ->
       step ge (State f (Scall (Some ? lhs) a al) k e m)
@@ -1245 +1245 @@
       let ge := globalenv Genv ?? p in
       let m0 := init_mem Genv ?? p in
-      find_symbol Genv ? ge (prog_main ?? p) = Some ? b ->
-      find_funct_ptr Genv ? ge b = Some ? f ->
+      find_symbol ?? ge (prog_main ?? p) = Some ? b ->
+      find_funct_ptr ?? ge b = Some ? f ->
       initial_state p (Callstate f (nil ?) Kstop m0).
 
@@ -1261 +1261 @@
 
 ndefinition exec_program : program → program_behavior → Prop ≝ λp,beh.
-  program_behaves (mk_transrel ?? step) (initial_state p) final_state (globalenv Genv ?? p) beh.
+  program_behaves (mk_transrel ?? step) (initial_state p) final_state (globalenv ??? p) beh.
 (*
 (** Big-step execution of a whole program.  *)