Changeset 174


Ignore:
Timestamp:
Oct 13, 2010, 12:19:19 PM (9 years ago)
Author:
campbell
Message:

Add a form of non-terminating functional semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r156 r174  
    905905].
    906906*)
     907
     908(* A (possibly non-terminating) execution. *)
     909ncoinductive execution : Type ≝
     910| e_stop : trace → state → execution
     911| e_step : trace → state → execution → execution
     912| e_wrong : execution
     913| e_interact : io_out → (eventval → execution) → execution.
     914
     915nlet corec exec_inf_aux (ge:genv) (s:IO eventval io_out (trace×state)) : execution ≝
     916match s with
     917[ Wrong ⇒ e_wrong
     918| Value v ⇒ match v with [ mk_pair t s' ⇒
     919    match is_final_state s' with
     920    [ inl _ ⇒ e_stop t s'
     921    | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
     922| Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
     923].
     924
     925ndefinition exec_inf : program → execution ≝
     926λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p;: ret ? 〈E0,sig_eject ?? s〉).
     927
Note: See TracChangeset for help on using the changeset viewer.