source: extracted/iO.ml @ 2716

Last change on this file since 2716 was 2649, checked in by sacerdot, 7 years ago

...

File size: 6.9 KB
Line 
1open Preamble
2
3open Proper
4
5open ErrorMessages
6
7open Option
8
9open Setoids
10
11open Monad
12
13open Positive
14
15open PreIdentifiers
16
17open Errors
18
19open Div_and_mod
20
21open Jmeq
22
23open Russell
24
25open Util
26
27open Bool
28
29open Relations
30
31open Nat
32
33open List
34
35open Hints_declaration
36
37open Core_notation
38
39open Pts
40
41open Logic
42
43open Types
44
45open Extralib
46
47open IOMonad
48
49open CostLabel
50
51open PositiveMap
52
53open Deqsets
54
55open Lists
56
57open Identifiers
58
59open Integers
60
61open AST
62
63open Division
64
65open Arithmetic
66
67open Extranat
68
69open Vector
70
71open FoldStuff
72
73open BitVector
74
75open Z
76
77open BitVectorZ
78
79open Pointers
80
81open Coqlib
82
83open Values
84
85open Events
86
87type eventval_type = __
88
89(** val mk_eventval : AST.typ -> eventval_type -> Events.eventval **)
90let mk_eventval = function
91| AST.ASTint (sz, sg) -> (fun v -> Events.EVint (sz, (Obj.magic v)))
92| AST.ASTptr -> Obj.magic (fun _ -> assert false (* absurd case *))
93
94(** val mk_val : AST.typ -> eventval_type -> Values.val0 **)
95let mk_val = function
96| AST.ASTint (sz, x) -> (fun v -> Values.Vint (sz, (Obj.magic v)))
97| AST.ASTptr -> Obj.magic (fun _ -> assert false (* absurd case *))
98
99(** val convert_eventval :
100    Events.eventval -> AST.typ -> Values.val0 Errors.res **)
101let convert_eventval ev = function
102| AST.ASTint (sz, x) ->
103  let Events.EVint (sz', i) = ev in
104  (match AST.eq_intsize sz sz' with
105   | Bool.True -> Errors.OK (Values.Vint (sz', i))
106   | Bool.False -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
107| AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
108
109(** val check_eventval' :
110    Values.val0 -> AST.typ -> Events.eventval Errors.res **)
111let check_eventval' v = function
112| AST.ASTint (sz, x) ->
113  (match v with
114   | Values.Vundef -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
115   | Values.Vint (sz', i) ->
116     (match AST.eq_intsize sz sz' with
117      | Bool.True -> Errors.OK (Events.EVint (sz', i))
118      | Bool.False -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
119   | Values.Vnull -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
120   | Values.Vptr x0 -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
121| AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
122
123(** val check_eventval_list :
124    Values.val0 List.list -> AST.typ List.list -> Events.eventval List.list
125    Errors.res **)
126let rec check_eventval_list vs tys =
127  match vs with
128  | List.Nil ->
129    (match tys with
130     | List.Nil -> Errors.OK List.Nil
131     | List.Cons (x, x0) ->
132       Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
133  | List.Cons (v, vt) ->
134    (match tys with
135     | List.Nil -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
136     | List.Cons (ty, tyt) ->
137       Obj.magic
138         (Monad.m_bind0 (Monad.max_def Errors.res0)
139           (Obj.magic (check_eventval' v ty)) (fun ev ->
140           Monad.m_bind0 (Monad.max_def Errors.res0)
141             (Obj.magic (check_eventval_list vt tyt)) (fun evt ->
142             Obj.magic (Errors.OK (List.Cons (ev, evt)))))))
143
144type io_out = { io_function : AST.ident; io_args : Events.eventval List.list;
145                io_in_typ : AST.typ }
146
147(** val io_out_rect_Type4 :
148    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
149    'a1 **)
150let rec io_out_rect_Type4 h_mk_io_out x_3363 =
151  let { io_function = io_function0; io_args = io_args0; io_in_typ =
152    io_in_typ0 } = x_3363
153  in
154  h_mk_io_out io_function0 io_args0 io_in_typ0
155
156(** val io_out_rect_Type5 :
157    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
158    'a1 **)
159let rec io_out_rect_Type5 h_mk_io_out x_3365 =
160  let { io_function = io_function0; io_args = io_args0; io_in_typ =
161    io_in_typ0 } = x_3365
162  in
163  h_mk_io_out io_function0 io_args0 io_in_typ0
164
165(** val io_out_rect_Type3 :
166    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
167    'a1 **)
168let rec io_out_rect_Type3 h_mk_io_out x_3367 =
169  let { io_function = io_function0; io_args = io_args0; io_in_typ =
170    io_in_typ0 } = x_3367
171  in
172  h_mk_io_out io_function0 io_args0 io_in_typ0
173
174(** val io_out_rect_Type2 :
175    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
176    'a1 **)
177let rec io_out_rect_Type2 h_mk_io_out x_3369 =
178  let { io_function = io_function0; io_args = io_args0; io_in_typ =
179    io_in_typ0 } = x_3369
180  in
181  h_mk_io_out io_function0 io_args0 io_in_typ0
182
183(** val io_out_rect_Type1 :
184    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
185    'a1 **)
186let rec io_out_rect_Type1 h_mk_io_out x_3371 =
187  let { io_function = io_function0; io_args = io_args0; io_in_typ =
188    io_in_typ0 } = x_3371
189  in
190  h_mk_io_out io_function0 io_args0 io_in_typ0
191
192(** val io_out_rect_Type0 :
193    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
194    'a1 **)
195let rec io_out_rect_Type0 h_mk_io_out x_3373 =
196  let { io_function = io_function0; io_args = io_args0; io_in_typ =
197    io_in_typ0 } = x_3373
198  in
199  h_mk_io_out io_function0 io_args0 io_in_typ0
200
201(** val io_function : io_out -> AST.ident **)
202let rec io_function xxx =
203  xxx.io_function
204
205(** val io_args : io_out -> Events.eventval List.list **)
206let rec io_args xxx =
207  xxx.io_args
208
209(** val io_in_typ : io_out -> AST.typ **)
210let rec io_in_typ xxx =
211  xxx.io_in_typ
212
213(** val io_out_inv_rect_Type4 :
214    io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
215    'a1) -> 'a1 **)
216let io_out_inv_rect_Type4 hterm h1 =
217  let hcut = io_out_rect_Type4 h1 hterm in hcut __
218
219(** val io_out_inv_rect_Type3 :
220    io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
221    'a1) -> 'a1 **)
222let io_out_inv_rect_Type3 hterm h1 =
223  let hcut = io_out_rect_Type3 h1 hterm in hcut __
224
225(** val io_out_inv_rect_Type2 :
226    io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
227    'a1) -> 'a1 **)
228let io_out_inv_rect_Type2 hterm h1 =
229  let hcut = io_out_rect_Type2 h1 hterm in hcut __
230
231(** val io_out_inv_rect_Type1 :
232    io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
233    'a1) -> 'a1 **)
234let io_out_inv_rect_Type1 hterm h1 =
235  let hcut = io_out_rect_Type1 h1 hterm in hcut __
236
237(** val io_out_inv_rect_Type0 :
238    io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
239    'a1) -> 'a1 **)
240let io_out_inv_rect_Type0 hterm h1 =
241  let hcut = io_out_rect_Type0 h1 hterm in hcut __
242
243(** val io_out_discr : io_out -> io_out -> __ **)
244let io_out_discr x y =
245  Logic.eq_rect_Type2 x
246    (let { io_function = a0; io_args = a1; io_in_typ = a2 } = x in
247    Obj.magic (fun _ dH -> dH __ __ __)) y
248
249(** val io_out_jmdiscr : io_out -> io_out -> __ **)
250let io_out_jmdiscr x y =
251  Logic.eq_rect_Type2 x
252    (let { io_function = a0; io_args = a1; io_in_typ = a2 } = x in
253    Obj.magic (fun _ dH -> dH __ __ __)) y
254
255type io_in = eventval_type
256
257(** val do_io :
258    AST.ident -> Events.eventval List.list -> AST.typ -> (io_out, io_in,
259    eventval_type) IOMonad.iO **)
260let do_io fn args t =
261  IOMonad.Interact ({ io_function = fn; io_args = args; io_in_typ = t },
262    (fun res1 -> IOMonad.Value res1))
263
264(** val ret : 'a1 -> (io_out, io_in, 'a1) IOMonad.iO **)
265let ret x =
266  IOMonad.Value x
267
Note: See TracBrowser for help on using the repository browser.