Changeset 13


Ignore:
Timestamp:
Jul 19, 2010, 4:30:09 PM (10 years ago)
Author:
campbell
Message:

Minor syntactic changes.

Location:
C-semantics
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Cexec.ma

    r11 r13  
    323323  match e' with
    324324  [ Evar id ⇒
    325       match (get ? PTree ? id en) with
    326       [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol Genv ? ge id);: OK ? 〈l,zero〉) (* global *)
     325      match (get id en) with
     326      [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈l,zero〉) (* global *)
    327327      | Some l ⇒ Some ? (OK ? 〈l,zero〉) (* local *)
    328328      ]
     
    388388  match h with [ mk_pair id ty ⇒
    389389    match alloc m 0 (sizeof ty) with [ mk_pair m1 b1 ⇒
    390       match exec_alloc_variables (set ? PTree ? id b1 en) m1 vars with
     390      match exec_alloc_variables (set id b1 en) m1 vars with
    391391      [ sig_intro r p ⇒ r ]
    392392]]]. nwhd; //;
    393 nelim (exec_alloc_variables (set ident PTree block c3 c7 en) c6 c1);
     393nelim (exec_alloc_variables (set ident ? block c3 c7 en) c6 c1);
    394394#H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
    395395napply (alloc_variables_cons … IH); /2/;
     
    404404      [ nil ⇒ Some ? (Error ?)
    405405      | cons v1 vl ⇒ Some ? (
    406           b ← opt_to_res ? (get ? PTree ? id e);:
     406          b ← opt_to_res ? (get id e);:
    407407          m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);:
    408408          err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
     
    511511    vf ← exec_expr ge e m a;:
    512512    vargs ← exec_exprlist ge e m al;:
    513     fd ← opt_to_res ? (find_funct Genv ? ge vf);:
     513    fd ← opt_to_res ? (find_funct ? ? ge vf);:
    514514    p ← assert_type_eq (type_of_fundef fd) (typeof a);:
    515515    k' ← match lhs with
     
    609609  let m0 ≝ init_mem Genv ?? p in
    610610  Some ? (
    611     b ← opt_to_res ? (find_symbol Genv ? ge (prog_main ?? p));:
    612     f ← opt_to_res ? (find_funct_ptr Genv ? ge b);:
     611    b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));:
     612    f ← opt_to_res ? (find_funct_ptr ? ? ge b);:
    613613    OK ? (Callstate f (nil ?) Kstop m0)).
    614614nwhd;
  • C-semantics/Csem.ma

    r3 r13  
    444444ndefinition env ≝ (tree_t ? PTree) block. (* map variable -> location *)
    445445
    446 ndefinition empty_env: env ≝ (empty ? PTree block).
     446ndefinition empty_env: env ≝ (empty ).
    447447
    448448(* * [load_value_of_type ty m b ofs] computes the value of a datum
     
    487487      ∀e,m,id,ty,vars,m1,b1,m2,e2.
    488488      alloc m 0 (sizeof ty) = 〈m1, b1〉 →
    489       alloc_variables (set ? PTree ? id b1 e) m1 vars e2 m2 →
     489      alloc_variables (set id b1 e) m1 vars e2 m2 →
    490490      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
    491491
     
    503503  | bind_parameters_cons:
    504504      ∀e,m,id,ty,params,v1,vl,b,m1,m2.
    505       get ? PTree ? id e = Some ? b →
     505      get ??? id e = Some ? b →
    506506      store_value_of_type ty m b zero v1 = Some ? m1 →
    507507      bind_parameters e m1 params vl m2 →
     
    511511
    512512ndefinition blocks_of_env : env → list block ≝ λe.
    513   map ?? (snd ident block) (elements ? PTree ? e).
     513  map ?? (snd ident block) (elements ??? e).
    514514
    515515(* * Selection of the appropriate case of a [switch], given the value [n]
     
    611611with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr -> block -> int -> Prop ≝
    612612  | eval_Evar_local:   ∀id,l,ty.
    613       (* XXX notation? e!id*) get ? PTree ? id e = Some ? l ->
     613      (* XXX notation? e!id*) get ??? id e = Some ? l ->
    614614      eval_lvalue ge e m (Expr (Evar id) ty) l zero
    615615  | eval_Evar_global: ∀id,l,ty.
    616       (* XXX e!id *) get ? PTree ? id e = None ? ->
    617       find_symbol Genv ? ge id = Some ? l ->
     616      (* XXX e!id *) get ??? id e = None ? ->
     617      find_symbol ?? ge id = Some ? l ->
    618618      eval_lvalue ge e m (Expr (Evar id) ty) l zero
    619619  | eval_Ederef: ∀a,ty,l,ofs.
     
    774774      eval_expr ge e m a vf ->
    775775      eval_exprlist ge e m al vargs ->
    776       find_funct Genv ? ge vf = Some ? fd ->
     776      find_funct ?? ge vf = Some ? fd ->
    777777      type_of_fundef fd = typeof a ->
    778778      step ge (State f (Scall (None ?) a al) k e m)
     
    783783      eval_expr ge e m a vf ->
    784784      eval_exprlist ge e m al vargs ->
    785       find_funct Genv ? ge vf = Some ? fd ->
     785      find_funct ?? ge vf = Some ? fd ->
    786786      type_of_fundef fd = typeof a ->
    787787      step ge (State f (Scall (Some ? lhs) a al) k e m)
     
    12451245      let ge := globalenv Genv ?? p in
    12461246      let m0 := init_mem Genv ?? p in
    1247       find_symbol Genv ? ge (prog_main ?? p) = Some ? b ->
    1248       find_funct_ptr Genv ? ge b = Some ? f ->
     1247      find_symbol ?? ge (prog_main ?? p) = Some ? b ->
     1248      find_funct_ptr ?? ge b = Some ? f ->
    12491249      initial_state p (Callstate f (nil ?) Kstop m0).
    12501250
     
    12611261
    12621262ndefinition exec_program : program → program_behavior → Prop ≝ λp,beh.
    1263   program_behaves (mk_transrel ?? step) (initial_state p) final_state (globalenv Genv ?? p) beh.
     1263  program_behaves (mk_transrel ?? step) (initial_state p) final_state (globalenv ??? p) beh.
    12641264(*
    12651265(** Big-step execution of a whole program.  *)
Note: See TracChangeset for help on using the changeset viewer.