Changeset 189 for C-semantics/CexecIO.ma


Ignore:
Timestamp:
Oct 18, 2010, 11:36:07 AM (9 years ago)
Author:
campbell
Message:

Rework monad notation so that it is displayed well in proof mode.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r175 r189  
    160160*)
    161161
    162 nlet rec try_cast_null (m:mem) (i:int) (ty:type) (ty':type) : res (Σv':val. cast m (Vint i) ty ty' v') ≝
     162nlet rec try_cast_null (m:mem) (i:int) (ty:type) (ty':type) on i : res (Σv':val. cast m (Vint i) ty ty' v') ≝
    163163match eq i zero with
    164164[ true ⇒
     
    194194#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    195195
    196 nlet rec exec_cast (m:mem) (v:val) (ty:type) (ty':type) : res (Σv':val. cast m v ty ty' v') ≝
     196ndefinition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res (Σv':val. cast m v ty ty' v') ≝
     197λm:mem. λv:val. λty:type. λty':type.
    197198match v with
    198199[ Vint i ⇒
     
    202203    [ Tint sz2 si2 ⇒ Some ? (OK ? (Vint (cast_int_int sz2 si2 i)))
    203204    | Tfloat sz2 ⇒ Some ? (OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i))))
    204     | Tpointer _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r)
    205     | Tarray _ _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r)
    206     | Tfunction _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r)
     205    | Tpointer _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
     206    | Tarray _ _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
     207    | Tfunction _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
    207208    | _ ⇒ Some ? (Error ?)
    208209    ]
    209   | Tpointer _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r)
    210   | Tarray _ _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r)
    211   | Tfunction _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r)
     210  | Tpointer _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
     211  | Tarray _ _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
     212  | Tfunction _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
    212213  | _ ⇒ Some ? (Error ?)
    213214  ]
     
    224225| Vptr p b ofs ⇒
    225226  Some ? (
    226     s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];:
    227     u ← match ms_eq_dec p s with [ inl _ ⇒ OK ? something | inr _ ⇒ Error ? ];:
    228     s' ← match ty' with
     227    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];
     228    do u ← match ms_eq_dec p s with [ inl _ ⇒ OK ? something | inr _ ⇒ Error ? ];
     229    do s' ← match ty' with
    229230         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
    230          | _ ⇒ Error ? ];:
     231         | _ ⇒ Error ? ];
    231232    if is_pointer_compat (block_space m b) s'
    232233    then OK ? (Vptr s' b ofs)
     
    270271  | Econst_float f ⇒ Some ? (OK ? 〈Vfloat f, E0〉)
    271272  | Evar _ ⇒ Some ? (
    272       〈l,tr〉 ← exec_lvalue' ge en m e' ty;:
    273       v ← opt_to_res ? (load_value_of_type' ty m l);:
     273      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
     274      do v ← opt_to_res ? (load_value_of_type' ty m l);
    274275      OK ? 〈v,tr〉)
    275276  | Ederef _ ⇒ Some ? (
    276       〈l,tr〉 ← exec_lvalue' ge en m e' ty;:
    277       v ← opt_to_res ? (load_value_of_type' ty m l);:
     277      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
     278      do v ← opt_to_res ? (load_value_of_type' ty m l);
    278279      OK ? 〈v,tr〉)
    279280  | Efield _ _ ⇒ Some ? (
    280       〈l,tr〉 ← exec_lvalue' ge en m e' ty;:
    281       v ← opt_to_res ? (load_value_of_type' ty m l);:
     281      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
     282      do v ← opt_to_res ? (load_value_of_type' ty m l);
    282283      OK ? 〈v,tr〉)
    283284  | Eaddrof a ⇒ Some ? (
    284       〈plo,tr〉 ← exec_lvalue ge en m a;:
     285      do 〈plo,tr〉 ← exec_lvalue ge en m a;
    285286      OK ? 〈match plo with [ mk_pair pl ofs ⇒ match pl with [ mk_pair pcl loc ⇒ Vptr pcl loc ofs ] ], tr〉)
    286287  | Esizeof ty' ⇒ Some ? (OK ? 〈Vint (repr (sizeof ty')), E0〉)
    287288  | Eunop op a ⇒ Some ? (
    288       〈v1,tr〉 ← exec_expr ge en m a;:
    289       v ← opt_to_res ? (sem_unary_operation op v1 (typeof a));:
     289      do 〈v1,tr〉 ← exec_expr ge en m a;
     290      do v ← opt_to_res ? (sem_unary_operation op v1 (typeof a));
    290291      OK ? 〈v,tr〉)
    291292  | Ebinop op a1 a2 ⇒ Some ? (
    292       〈v1,tr1〉 ← exec_expr ge en m a1;:
    293       〈v2,tr2〉 ← exec_expr ge en m a2;:
    294       v ← opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);:
     293      do 〈v1,tr1〉 ← exec_expr ge en m a1;
     294      do 〈v2,tr2〉 ← exec_expr ge en m a2;
     295      do v ← opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);
    295296      OK ? 〈v,tr1⧺tr2〉)
    296297  | Econdition a1 a2 a3 ⇒ Some ? (
    297       〈v,tr1〉 ← exec_expr ge en m a1;:
    298       b ← bool_of_val_3 v (typeof a1);:
    299       〈v',tr2〉 ← match b return λ_.res (val×trace) with
     298      do 〈v,tr1〉 ← exec_expr ge en m a1;
     299      do b ← bool_of_val_3 v (typeof a1);
     300      do 〈v',tr2〉 ← match b return λ_.res (val×trace) with
    300301                 [ true ⇒ (exec_expr ge en m a2)
    301                  | false ⇒ (exec_expr ge en m a3) ];:
     302                 | false ⇒ (exec_expr ge en m a3) ];
    302303      OK ? 〈v',tr1⧺tr2〉)
    303304(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
    304305  | Eorbool a1 a2 ⇒ Some ? (
    305       〈v1,tr1〉 ← exec_expr ge en m a1;:
    306       b1 ← bool_of_val_3 v1 (typeof a1);:
     306      do 〈v1,tr1〉 ← exec_expr ge en m a1;
     307      do b1 ← bool_of_val_3 v1 (typeof a1);
    307308      match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 | false ⇒
    308         〈v2,tr2〉 ← exec_expr ge en m a2;:
    309         b2 ← bool_of_val_3 v2 (typeof a2);:
     309        do 〈v2,tr2〉 ← exec_expr ge en m a2;
     310        do b2 ← bool_of_val_3 v2 (typeof a2);
    310311        OK ? 〈of_bool b2, tr1⧺tr2〉 ])
    311312  | Eandbool a1 a2 ⇒ Some ? (
    312       〈v1,tr1〉 ← exec_expr ge en m a1;:
    313       b1 ← bool_of_val_3 v1 (typeof a1);:
     313      do 〈v1,tr1〉 ← exec_expr ge en m a1;
     314      do b1 ← bool_of_val_3 v1 (typeof a1);
    314315      match b1 return λ_.res (val×trace) with [ true ⇒
    315         〈v2,tr2〉 ← exec_expr ge en m a2;:
    316         b2 ← bool_of_val_3 v2 (typeof a2);:
     316        do 〈v2,tr2〉 ← exec_expr ge en m a2;
     317        do b2 ← bool_of_val_3 v2 (typeof a2);
    317318        OK ? 〈of_bool b2, tr1⧺tr2〉
    318319      | false ⇒ OK ? 〈Vfalse,tr1〉 ])
    319320  | Ecast ty' a ⇒ Some ? (
    320       〈v,tr〉 ← exec_expr ge en m a;:
    321       v' ← exec_cast m v (typeof a) ty';:
     321      do 〈v,tr〉 ← exec_expr ge en m a;
     322      do v' ← exec_cast m v (typeof a) ty';
    322323      OK ? 〈(* XXX *)sig_eject ?? v',tr〉)
    323324  | Ecost l a ⇒ Some ? (
    324       〈v,tr〉 ← exec_expr ge en m a;:
     325      do 〈v,tr〉 ← exec_expr ge en m a;
    325326      OK ? 〈v,tr⧺(Echarge l)〉)
    326327  ]
     
    330331  [ Evar id ⇒
    331332      match (get … id en) with
    332       [ None ⇒ Some ? (〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈〈〈sp,l〉,zero〉,E0〉) (* global *)
     333      [ None ⇒ Some ? (do 〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈〈sp,l〉,zero〉,E0〉) (* global *)
    333334      | Some loc ⇒ Some ? (OK ? 〈〈〈Any,loc〉,zero〉,E0〉) (* local *)
    334335      ]
    335336  | Ederef a ⇒ Some ? (
    336       〈v,tr〉 ← exec_expr ge en m a;:
     337      do 〈v,tr〉 ← exec_expr ge en m a;
    337338      match v with
    338339      [ Vptr sp l ofs ⇒ OK ? 〈〈〈sp,l〉,ofs〉,tr〉
     
    342343      match (typeof a) with
    343344      [ Tstruct id fList ⇒ Some ? (
    344           〈plofs,tr〉 ← exec_lvalue ge en m a;:
    345           delta ← field_offset i fList;:
     345          do 〈plofs,tr〉 ← exec_lvalue ge en m a;
     346          do delta ← field_offset i fList;
    346347          OK ? 〈〈\fst plofs,add (\snd plofs) (repr delta)〉,tr〉)
    347348      | Tunion id fList ⇒ Some ? (
    348           〈plofs,tr〉 ← exec_lvalue ge en m a;:
     349          do 〈plofs,tr〉 ← exec_lvalue ge en m a;
    349350          OK ? 〈plofs,tr〉)
    350351      | _ ⇒ Some ? (Error ?)
     
    418419[ nil ⇒ Some ? (OK ? 〈nil val, E0〉)
    419420| cons e1 es ⇒ Some ? (
    420   〈v,tr1〉 ← exec_expr ge e m e1;:
    421   〈vs,tr2〉 ← exec_exprlist ge e m es;:
     421  do 〈v,tr1〉 ← exec_expr ge e m e1;
     422  do 〈vs,tr2〉 ← exec_exprlist ge e m es;
    422423  OK ? 〈cons val v vs, tr1⧺tr2〉)
    423424]. nwhd; //;
     
    454455      [ nil ⇒ Some ? (Error ?)
    455456      | cons v1 vl ⇒ Some ? (
    456           b ← opt_to_res ? (get … id e);:
    457           m1 ← opt_to_res ? (store_value_of_type ty m Any b zero v1);:
     457          do b ← opt_to_res ? (get … id e);
     458          do m1 ← opt_to_res ? (store_value_of_type ty m Any b zero v1);
    458459          err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
    459460      ]
     
    598599  [ nil ⇒ Some ? (Error ?)
    599600  | cons ty tyt ⇒ Some ? (
    600     ev ← check_eventval' v ty;:
    601     evt ← check_eventval_list vt tyt;:
     601    do ev ← check_eventval' v ty;
     602    do evt ← check_eventval_list vt tyt;
    602603    OK ? ((sig_eject ?? ev)::evt))
    603604  ]
Note: See TracChangeset for help on using the changeset viewer.