source: src/common/IO.ma @ 2530

Last change on this file since 2530 was 2468, checked in by garnier, 7 years ago

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

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 return λ_. Type[0] with [ ASTptr ⇒ False | ASTint sz _ ⇒ bvint sz ].
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 ⇒ ?  (*| 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 ⇒ ? (*| 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.