| 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 return λ_. Type[0] with [ ASTptr ⇒ False | ASTint sz _ ⇒ bvint sz ]. |
|---|
| 9 | |
|---|
| 10 | definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝ |
|---|
| 11 | λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint sz sg ⇒ λv.EVint sz v | ASTptr ⇒ ? (*| 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 sz _ ⇒ λv.Vint sz v | ASTptr ⇒ ? (*| 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 sz _ ⇒ match ev with |
|---|
| 28 | [ EVint sz' i ⇒ if eq_intsize sz sz' then OK ? (Vint sz' i) else Error ? (msg IllTypedEvent) |
|---|
| 29 | | _ ⇒ Error ? (msg IllTypedEvent)] |
|---|
| 30 | (*| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)] *) |
|---|
| 31 | | _ ⇒ Error ? (msg IllTypedEvent) |
|---|
| 32 | ]. |
|---|
| 33 | |
|---|
| 34 | definition check_eventval' : ∀v:val. ∀ty:typ. res eventval ≝ |
|---|
| 35 | λv,ty. |
|---|
| 36 | match ty with |
|---|
| 37 | [ ASTint sz _ ⇒ match v with |
|---|
| 38 | [ Vint sz' i ⇒ if eq_intsize sz sz' then OK ? (EVint sz' i) else Error ? (msg IllTypedEvent) |
|---|
| 39 | | _ ⇒ Error ? (msg IllTypedEvent) ] |
|---|
| 40 | (*| ASTfloat _ ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]*) |
|---|
| 41 | | _ ⇒ Error ? (msg IllTypedEvent) |
|---|
| 42 | ]. |
|---|
| 43 | |
|---|
| 44 | let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝ |
|---|
| 45 | match vs with |
|---|
| 46 | [ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? (msg IllTypedEvent) ] |
|---|
| 47 | | cons v vt ⇒ |
|---|
| 48 | match tys with |
|---|
| 49 | [ nil ⇒ Error ? (msg IllTypedEvent) |
|---|
| 50 | | cons ty tyt ⇒ |
|---|
| 51 | do ev ← check_eventval' v ty; |
|---|
| 52 | do evt ← check_eventval_list vt tyt; |
|---|
| 53 | OK ? (ev::evt) |
|---|
| 54 | ] |
|---|
| 55 | ]. |
|---|
| 56 | |
|---|
| 57 | (* IO monad *) |
|---|
| 58 | |
|---|
| 59 | (* Interactions are function calls that return a value and do not change |
|---|
| 60 | the rest of the Clight program's state. *) |
|---|
| 61 | record io_out : Type[0] ≝ |
|---|
| 62 | { io_function: ident |
|---|
| 63 | ; io_args: list eventval |
|---|
| 64 | ; io_in_typ: typ |
|---|
| 65 | }. |
|---|
| 66 | |
|---|
| 67 | definition io_in ≝ λo. eventval_type (io_in_typ o). |
|---|
| 68 | |
|---|
| 69 | definition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝ |
|---|
| 70 | λfn,args,t. Interact ??? (mk_io_out fn args t) (λres. Value ??? res). |
|---|
| 71 | |
|---|
| 72 | definition ret: ∀T. T → (IO io_out io_in T) ≝ |
|---|
| 73 | λT,x.(Value ?? T x). |
|---|
