| 1 | |
|---|
| 2 | include "common/IOMonad.ma". |
|---|
| 3 | include "common/Events.ma". |
|---|
| 4 | |
|---|
| 5 | (* Checking types of values given to / received from an external function call. *) |
|---|
| 6 | |
|---|
| 7 | definition eventval_type : ∀ty:typ. Type[0] ≝ |
|---|
| 8 | λty. match ty with [ ASTint _ _ ⇒ int | ASTptr _ ⇒ False | ASTfloat _ ⇒ float ]. |
|---|
| 9 | |
|---|
| 10 | definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝ |
|---|
| 11 | λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint _ _ ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.EVfloat v ]. |
|---|
| 12 | *; qed. |
|---|
| 13 | |
|---|
| 14 | definition mk_val: ∀ty:typ. eventval_type ty → val ≝ |
|---|
| 15 | λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint _ _ ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ]. |
|---|
| 16 | *; qed. |
|---|
| 17 | |
|---|
| 18 | lemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty. |
|---|
| 19 | eventval_match (mk_eventval ty v) ty (mk_val ty v). |
|---|
| 20 | #ty cases ty; normalize; // * *; qed. |
|---|
| 21 | |
|---|
| 22 | axiom IllTypedEvent : String. |
|---|
| 23 | |
|---|
| 24 | definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝ |
|---|
| 25 | λev,ty. |
|---|
| 26 | match ty with |
|---|
| 27 | [ ASTint _ _ ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? (msg IllTypedEvent)] |
|---|
| 28 | | ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)] |
|---|
| 29 | | _ ⇒ Error ? (msg IllTypedEvent) |
|---|
| 30 | ]. |
|---|
| 31 | |
|---|
| 32 | definition check_eventval' : ∀v:val. ∀ty:typ. res eventval ≝ |
|---|
| 33 | λv,ty. |
|---|
| 34 | match ty with |
|---|
| 35 | [ ASTint _ _ ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? (msg IllTypedEvent) ] |
|---|
| 36 | | ASTfloat _ ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ] |
|---|
| 37 | | _ ⇒ Error ? (msg IllTypedEvent) |
|---|
| 38 | ]. |
|---|
| 39 | |
|---|
| 40 | let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝ |
|---|
| 41 | match vs with |
|---|
| 42 | [ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? (msg IllTypedEvent) ] |
|---|
| 43 | | cons v vt ⇒ |
|---|
| 44 | match tys with |
|---|
| 45 | [ nil ⇒ Error ? (msg IllTypedEvent) |
|---|
| 46 | | cons ty tyt ⇒ |
|---|
| 47 | do ev ← check_eventval' v ty; |
|---|
| 48 | do evt ← check_eventval_list vt tyt; |
|---|
| 49 | OK ? (ev::evt) |
|---|
| 50 | ] |
|---|
| 51 | ]. |
|---|
| 52 | |
|---|
| 53 | (* IO monad *) |
|---|
| 54 | |
|---|
| 55 | (* Interactions are function calls that return a value and do not change |
|---|
| 56 | the rest of the Clight program's state. *) |
|---|
| 57 | record io_out : Type[0] ≝ |
|---|
| 58 | { io_function: ident |
|---|
| 59 | ; io_args: list eventval |
|---|
| 60 | ; io_in_typ: typ |
|---|
| 61 | }. |
|---|
| 62 | |
|---|
| 63 | definition io_in ≝ λo. eventval_type (io_in_typ o). |
|---|
| 64 | |
|---|
| 65 | definition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝ |
|---|
| 66 | λfn,args,t. Interact ??? (mk_io_out fn args t) (λres. Value ??? res). |
|---|
| 67 | |
|---|
| 68 | definition ret: ∀T. T → (IO io_out io_in T) ≝ |
|---|
| 69 | λT,x.(Value ?? T x). |
|---|
