Ignore:
Timestamp:
Jan 23, 2012, 6:31:27 PM (7 years ago)
Author:
campbell
Message:

Update Cminor and RTLabs semantics to use new monad definitions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r1626 r1655  
    295295definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
    296296λge,st.
    297 match st with
    298 [ State f s en fInv Inv m sp k kInv st ⇒
    299     match s return λs. stmt_inv f en s → ? with
     297match st return λ_. IO ??? with
     298[ State f s en fInv Inv m sp k kInv st ⇒ err_to_io ??? (
     299    match s return λs. stmt_inv f en s → res (trace × state) with
    300300    [ St_skip ⇒ λInv.
    301         match k return λk. cont_inv f en k → ? with
    302         [ Kseq s' k' ⇒ λkInv. ret ? 〈E0, State f s' en fInv ? m sp k' ? st〉
    303         | Kblock k' ⇒ λkInv. ret ? 〈E0, State f St_skip en fInv ? m sp k' ? st〉
     301        match k return λk. cont_inv f en k → res ? with
     302        [ Kseq s' k' ⇒ λkInv. return 〈E0, State f s' en fInv ? m sp k' ? st〉
     303        | Kblock k' ⇒ λkInv. return 〈E0, State f St_skip en fInv ? m sp k' ? st〉
    304304          (* cminor allows functions without an explicit return statement *)
    305         | Kend ⇒ λkInv. ret ? 〈E0, Returnstate (None ?) (free m sp) st〉
     305        | Kend ⇒ λkInv. return 〈E0, Returnstate (None ?) (free m sp) st〉
    306306        ] kInv
    307307    | St_assign _ id e ⇒ λInv.
    308308        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    309309        let en' ≝ update_present ?? en id ? v in
    310         ret ? 〈tr, State f St_skip en' ? ? m sp k ? st〉
     310        return 〈tr, State f St_skip en' ? ? m sp k ? st〉
    311311    | St_store _ _ chunk edst e ⇒ λInv.
    312312        ! 〈tr,vdst〉 ← eval_expr ge ? edst en ? sp m;
    313313        ! 〈tr',v〉 ← eval_expr ge ? e en ? sp m;
    314314        ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vdst v);
    315         ret ? 〈tr ⧺ tr', State f St_skip en fInv ? m' sp k ? st〉
     315        return 〈tr ⧺ tr', State f St_skip en fInv ? m' sp k ? st〉
    316316
    317317    | St_call dst ef args ⇒ λInv.
     
    319319        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    320320        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ mk_DPair _ _ ⇒ ? ] → ? with [ mk_DPair ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
    321         ret ? 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉
     321        return 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉
    322322    | St_tailcall ef args ⇒ λInv.
    323323        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
    324324        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    325325        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ mk_DPair _ _ ⇒ ? ] → ? with [ mk_DPair ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
    326         ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) st〉
     326        return 〈tr ⧺ tr', Callstate fd vargs (free m sp) st〉
    327327       
    328     | St_seq s1 s2 ⇒ λInv. ret ? 〈E0, State f s1 en fInv ? m sp (Kseq s2 k) ? st〉
     328    | St_seq s1 s2 ⇒ λInv. return 〈E0, State f s1 en fInv ? m sp (Kseq s2 k) ? st〉
    329329    | St_ifthenelse _ _ e strue sfalse ⇒ λInv.
    330330        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    331331        ! b ← eval_bool_of_val v;
    332         ret ? 〈tr, State f (if b then strue else sfalse) en fInv ? m sp k ? st〉
    333     | St_loop s ⇒ λInv. ret ? 〈E0, State f s en fInv ? m sp (Kseq (St_loop s) k) ? st〉
    334     | St_block s ⇒ λInv. ret ? 〈E0, State f s en fInv ? m sp (Kblock k) ? st〉
     332        return 〈tr, State f (if b then strue else sfalse) en fInv ? m sp k ? st〉
     333    | St_loop s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kseq (St_loop s) k) ? st〉
     334    | St_block s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kblock k) ? st〉
    335335    | St_exit n ⇒ λInv.
    336336        ! k' ← k_exit n k ?? kInv;
    337         ret ? 〈E0, State f St_skip en fInv ? m sp k' ? st〉
     337        return 〈E0, State f St_skip en fInv ? m sp k' ? st〉
    338338    | St_switch sz _ e cs default ⇒ λInv.
    339339        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
     
    341341        [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.
    342342            ! k' ← k_exit (find_case ?? i cs default) k ?? kInv;
    343             ret ? 〈tr, State f St_skip en fInv ? m sp k' ? st〉)
    344             (Wrong ??? (msg BadSwitchValue))
    345         | _ ⇒ Wrong ??? (msg BadSwitchValue)
     343            return 〈tr, State f St_skip en fInv ? m sp k' ? st〉)
     344            (Error ? (msg BadSwitchValue))
     345        | _ ⇒ Error ? (msg BadSwitchValue)
    346346        ]
    347347    | St_return eo ⇒
    348348        match eo return λeo. stmt_inv f en (St_return eo) → ? with
    349         [ None ⇒ λInv. ret ? 〈E0, Returnstate (None ?) (free m sp) st〉
     349        [ None ⇒ λInv. return 〈E0, Returnstate (None ?) (free m sp) st〉
    350350        | Some e ⇒
    351351            match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ mk_DPair ty e ⇒ λInv.
    352352              ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    353               ret ? 〈tr, Returnstate (Some ? v) (free m sp) st〉
     353              return 〈tr, Returnstate (Some ? v) (free m sp) st〉
    354354            ]
    355355        ]
    356     | St_label l s' ⇒ λInv. ret ? 〈E0, State f s' en fInv ? m sp k ? st〉
     356    | St_label l s' ⇒ λInv. return 〈E0, State f s' en fInv ? m sp k ? st〉
    357357    | St_goto l ⇒ λInv.
    358358        match find_label_always l (f_body f) Kend ? f en ?? with [ mk_Sig sk Inv' ⇒
    359           ret ? 〈E0, State f (\fst sk) en fInv ? m sp (\snd sk) ? st〉
     359          return 〈E0, State f (\fst sk) en fInv ? m sp (\snd sk) ? st〉
    360360        ]
    361361    | St_cost l s' ⇒ λInv.
    362         ret ? 〈Echarge l, State f s' en fInv ? m sp k ? st〉
    363     ] Inv
     362        return 〈Echarge l, State f s' en fInv ? m sp k ? st〉
     363    ] Inv)
    364364| Callstate fd args m st ⇒
    365365    match fd with
    366     [ Internal f ⇒
     366    [ Internal f ⇒ err_to_io ?? (trace × state) (
    367367        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
    368368        ! en ← bind_params args (f_params f);
    369         ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉
     369        return 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉)
    370370    | External fn ⇒
    371         ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
     371        ! evargs ← err_to_io ??? (check_eventval_list args (sig_args (ef_sig fn)));
    372372        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    373373        let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in
    374         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m st〉
    375     ]
    376 | Returnstate res m st ⇒
     374        return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m st〉
     375    ]
     376| Returnstate result m st ⇒ err_to_io ??? (
    377377    match st with
    378378    [ Scall dst f sp en dstP fInv k Inv st' ⇒
    379         match res with
     379        match result with
    380380        [ None ⇒ match dst with
    381                  [ None ⇒ ret ? 〈E0, State f St_skip en ? ? m sp k ? st'〉
    382                  | Some _ ⇒ Wrong ??? (msg ReturnMismatch)]
    383         | Some v ⇒ match dst return λdst. match dst with [ None ⇒ ? | Some _ ⇒ ?] → ? with
    384                    [ None ⇒ λ_. Wrong ??? (msg ReturnMismatch)
    385                    | Some idty ⇒ λdstP. ret ? 〈E0, State f St_skip (update_present ?? en (\fst idty) dstP v) ? ? m sp k ? st'〉
     381                 [ None ⇒ return 〈E0, State f St_skip en ? ? m sp k ? st'〉
     382                 | Some _ ⇒ Error ? (msg ReturnMismatch)]
     383        | Some v ⇒ match dst return λdst. match dst with [ None ⇒ True | Some idty ⇒ present ?? en (\fst idty) ] → res (trace × state) with
     384                   [ None ⇒ λ_. Error ? (msg ReturnMismatch)
     385                   | Some idty ⇒ λdstP. return 〈E0, State f St_skip (update_present ?? en (\fst idty) dstP v) ? ? m sp k ? st'〉
    386386                   ] dstP
    387387        ]
    388     | _ ⇒ Wrong ??? (msg BadState)
    389     ]
     388    | _ ⇒ Error ? (msg BadState)
     389    ])
    390390].
    391391try @(π1 kInv)
     
    401401try @(π1 Inv)
    402402try @(π2 Inv)
    403 [ @stmt_inv_update @fInv
    404 | % [ @(π2 Inv) | @kInv ]
    405 | cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ]
    406 | % [ @Inv | @kInv ]
     403[ @fInv
     404| @(π2 Inv')
     405| @(π1 Inv')
    407406| @(pi2 … k')
    408407| @(pi2 … k')
    409 | @(π1 Inv')
    410 | @(π2 Inv')
    411 | @fInv
    412 | @I
    413 | 11,12:
     408| % [ @Inv | @kInv ]
     409| cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ]
     410| % [ @(π2 Inv) | @kInv ]
     411| @stmt_inv_update @fInv
     412| 10,11:
    414413  @(stmt_P_mp … (f_inv f))
    415414  #s * #V #L %
     
    422421  | 2,4: @L
    423422  ]
     423| @I
     424| @cont_inv_update @Inv
     425| @stmt_inv_update @fInv
     426| @Inv
    424427| @fInv
    425 | @Inv
    426 | @stmt_inv_update @fInv
    427 | @cont_inv_update @Inv
    428428] qed.
    429429
Note: See TracChangeset for help on using the changeset viewer.