source: src/common/IO.ma @ 1021

Last change on this file since 1021 was 961, checked in by campbell, 10 years ago

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File size: 2.6 KB
Line 
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] ≝
8λty. match ty with [ ASTint sz _ ⇒ bvint sz | ASTptr _ ⇒ False | ASTfloat _ ⇒ float ].
9
10definition 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 r ⇒ ? | ASTfloat _ ⇒ λv.EVfloat v ].
12*; qed.
13
14definition 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 r ⇒ ? | ASTfloat _ ⇒ λv.Vfloat v ].
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
22axiom IllTypedEvent : String.
23
24definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
25λev,ty.
26match 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
34definition check_eventval' : ∀v:val. ∀ty:typ. res eventval ≝
35λv,ty.
36match 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
44let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝
45match 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. *)
61record io_out : Type[0] ≝
62{ io_function: ident
63; io_args: list eventval
64; io_in_typ: typ
65}.
66
67definition io_in ≝ λo. eventval_type (io_in_typ o).
68
69definition 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
72definition ret: ∀T. T → (IO io_out io_in T) ≝
73λT,x.(Value ?? T x).
Note: See TracBrowser for help on using the repository browser.