source: src/common/IO.ma @ 2769

Last change on this file since 2769 was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 2.5 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
22definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
23λev,ty.
24match ty with
25[ ASTint sz _ ⇒ match ev with
26  [ EVint sz' i ⇒ if eq_intsize sz sz' then OK ? (Vint sz' i) else Error ? (msg IllTypedEvent)
27  | _ ⇒ Error ? (msg IllTypedEvent)]
28(*| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? (msg IllTypedEvent)] *)
29| _ ⇒ Error ? (msg IllTypedEvent)
30].
31
32definition check_eventval' : ∀v:val. ∀ty:typ. res eventval ≝
33λv,ty.
34match ty with
35[ ASTint sz _ ⇒ match v with
36  [ Vint sz' i ⇒ if eq_intsize sz sz' then OK ? (EVint sz' i) else Error ? (msg IllTypedEvent)
37  | _ ⇒ Error ? (msg IllTypedEvent) ]
38(*| ASTfloat _ ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? (msg IllTypedEvent) ]*)
39| _ ⇒ Error ? (msg IllTypedEvent)
40].
41
42let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝
43match vs with
44[ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? (msg IllTypedEvent) ]
45| cons v vt ⇒
46  match tys with
47  [ nil ⇒ Error ? (msg IllTypedEvent)
48  | cons ty tyt ⇒
49    do ev ← check_eventval' v ty;
50    do evt ← check_eventval_list vt tyt;
51    OK ? (ev::evt)
52  ]
53].
54
55(* IO monad *)
56
57(* Interactions are function calls that return a value and do not change
58   the rest of the Clight program's state. *)
59record io_out : Type[0] ≝
60{ io_function: ident
61; io_args: list eventval
62; io_in_typ: typ
63}.
64
65definition io_in ≝ λo. eventval_type (io_in_typ o).
66
67definition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝
68λfn,args,t. Interact ??? (mk_io_out fn args t) (λres. Value ??? res).
69
70definition ret: ∀T. T → (IO io_out io_in T) ≝
71λT,x.(Value ?? T x).
Note: See TracBrowser for help on using the repository browser.