source: src/common/IO.ma @ 879

Last change on this file since 879 was 879, checked in by campbell, 9 years ago

Refine "AST" types to include size/signedness information.

File size: 2.4 KB
RevLine 
[731]1
2include "common/IOMonad.ma".
3include "common/Events.ma".
4
5(* Checking types of values given to / received from an external function call. *)
6
7definition eventval_type : ∀ty:typ. Type[0] ≝
[879]8λty. match ty with [ ASTint _ _ ⇒ int | ASTptr _ ⇒ False | ASTfloat _ ⇒ float ].
[731]9
10definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
[879]11λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint _ _ ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.EVfloat v ].
[731]12*; qed.
13
14definition mk_val: ∀ty:typ. eventval_type ty → val ≝
[879]15λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint _ _ ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ].
[731]16*; qed.
17
18lemma 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
[797]22axiom IllTypedEvent : String.
23
[731]24definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
25λev,ty.
26match ty with
[879]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)]
[797]29| _ ⇒ Error ? (msg IllTypedEvent)
[731]30].
31
32definition check_eventval' : ∀v:val. ∀ty:typ. res eventval ≝
33λv,ty.
34match ty with
[879]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) ]
[797]37| _ ⇒ Error ? (msg IllTypedEvent)
[731]38].
39
40let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝
41match vs with
[797]42[ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? (msg IllTypedEvent) ]
[731]43| cons v vt ⇒
44  match tys with
[797]45  [ nil ⇒ Error ? (msg IllTypedEvent)
[731]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. *)
57record io_out : Type[0] ≝
58{ io_function: ident
59; io_args: list eventval
60; io_in_typ: typ
61}.
62
63definition io_in ≝ λo. eventval_type (io_in_typ o).
64
65definition 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
68definition ret: ∀T. T → (IO io_out io_in T) ≝
69λT,x.(Value ?? T x).
Note: See TracBrowser for help on using the repository browser.