35 open Hints_declaration
89 type eventval_type = __
91 (** val mk_eventval : AST.typ -> eventval_type -> Events.eventval **)
92 let mk_eventval = function
93 | AST.ASTint (sz, sg) -> (fun v -> Events.EVint (sz, (Obj.magic v)))
94 | AST.ASTptr -> Obj.magic (fun _ -> assert false (* absurd case *))
96 (** val mk_val : AST.typ -> eventval_type -> Values.val0 **)
98 | AST.ASTint (sz, x) -> (fun v -> Values.Vint (sz, (Obj.magic v)))
99 | AST.ASTptr -> Obj.magic (fun _ -> assert false (* absurd case *))
101 (** val convert_eventval :
102 Events.eventval -> AST.typ -> Values.val0 Errors.res **)
103 let convert_eventval ev = function
104 | AST.ASTint (sz, x) ->
105 let Events.EVint (sz', i) = ev in
106 (match AST.eq_intsize sz sz' with
107 | Bool.True -> Errors.OK (Values.Vint (sz', i))
108 | Bool.False -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
109 | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
111 (** val check_eventval' :
112 Values.val0 -> AST.typ -> Events.eventval Errors.res **)
113 let check_eventval' v = function
114 | AST.ASTint (sz, x) ->
116 | Values.Vundef -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
117 | Values.Vint (sz', i) ->
118 (match AST.eq_intsize sz sz' with
119 | Bool.True -> Errors.OK (Events.EVint (sz', i))
120 | Bool.False -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
121 | Values.Vnull -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
122 | Values.Vptr x0 -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
123 | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
125 (** val check_eventval_list :
126 Values.val0 List.list -> AST.typ List.list -> Events.eventval List.list
128 let rec check_eventval_list vs tys =
132 | List.Nil -> Errors.OK List.Nil
133 | List.Cons (x, x0) ->
134 Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
135 | List.Cons (v, vt) ->
137 | List.Nil -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
138 | List.Cons (ty, tyt) ->
140 (Monad.m_bind0 (Monad.max_def Errors.res0)
141 (Obj.magic (check_eventval' v ty)) (fun ev ->
142 Monad.m_bind0 (Monad.max_def Errors.res0)
143 (Obj.magic (check_eventval_list vt tyt)) (fun evt ->
144 Obj.magic (Errors.OK (List.Cons (ev, evt)))))))
146 type io_out = { io_function : AST.ident; io_args : Events.eventval List.list;
147 io_in_typ : AST.typ }
149 (** val io_out_rect_Type4 :
150 (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
152 let rec io_out_rect_Type4 h_mk_io_out x_5899 =
153 let { io_function = io_function0; io_args = io_args0; io_in_typ =
154 io_in_typ0 } = x_5899
156 h_mk_io_out io_function0 io_args0 io_in_typ0
158 (** val io_out_rect_Type5 :
159 (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
161 let rec io_out_rect_Type5 h_mk_io_out x_5901 =
162 let { io_function = io_function0; io_args = io_args0; io_in_typ =
163 io_in_typ0 } = x_5901
165 h_mk_io_out io_function0 io_args0 io_in_typ0
167 (** val io_out_rect_Type3 :
168 (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
170 let rec io_out_rect_Type3 h_mk_io_out x_5903 =
171 let { io_function = io_function0; io_args = io_args0; io_in_typ =
172 io_in_typ0 } = x_5903
174 h_mk_io_out io_function0 io_args0 io_in_typ0
176 (** val io_out_rect_Type2 :
177 (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
179 let rec io_out_rect_Type2 h_mk_io_out x_5905 =
180 let { io_function = io_function0; io_args = io_args0; io_in_typ =
181 io_in_typ0 } = x_5905
183 h_mk_io_out io_function0 io_args0 io_in_typ0
185 (** val io_out_rect_Type1 :
186 (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
188 let rec io_out_rect_Type1 h_mk_io_out x_5907 =
189 let { io_function = io_function0; io_args = io_args0; io_in_typ =
190 io_in_typ0 } = x_5907
192 h_mk_io_out io_function0 io_args0 io_in_typ0
194 (** val io_out_rect_Type0 :
195 (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
197 let rec io_out_rect_Type0 h_mk_io_out x_5909 =
198 let { io_function = io_function0; io_args = io_args0; io_in_typ =
199 io_in_typ0 } = x_5909
201 h_mk_io_out io_function0 io_args0 io_in_typ0
203 (** val io_function : io_out -> AST.ident **)
204 let rec io_function xxx =
207 (** val io_args : io_out -> Events.eventval List.list **)
208 let rec io_args xxx =
211 (** val io_in_typ : io_out -> AST.typ **)
212 let rec io_in_typ xxx =
215 (** val io_out_inv_rect_Type4 :
216 io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
218 let io_out_inv_rect_Type4 hterm h1 =
219 let hcut = io_out_rect_Type4 h1 hterm in hcut __
221 (** val io_out_inv_rect_Type3 :
222 io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
224 let io_out_inv_rect_Type3 hterm h1 =
225 let hcut = io_out_rect_Type3 h1 hterm in hcut __
227 (** val io_out_inv_rect_Type2 :
228 io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
230 let io_out_inv_rect_Type2 hterm h1 =
231 let hcut = io_out_rect_Type2 h1 hterm in hcut __
233 (** val io_out_inv_rect_Type1 :
234 io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
236 let io_out_inv_rect_Type1 hterm h1 =
237 let hcut = io_out_rect_Type1 h1 hterm in hcut __
239 (** val io_out_inv_rect_Type0 :
240 io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
242 let io_out_inv_rect_Type0 hterm h1 =
243 let hcut = io_out_rect_Type0 h1 hterm in hcut __
245 (** val io_out_discr : io_out -> io_out -> __ **)
246 let io_out_discr x y =
247 Logic.eq_rect_Type2 x
248 (let { io_function = a0; io_args = a1; io_in_typ = a2 } = x in
249 Obj.magic (fun _ dH -> dH __ __ __)) y
251 (** val io_out_jmdiscr : io_out -> io_out -> __ **)
252 let io_out_jmdiscr x y =
253 Logic.eq_rect_Type2 x
254 (let { io_function = a0; io_args = a1; io_in_typ = a2 } = x in
255 Obj.magic (fun _ dH -> dH __ __ __)) y
257 type io_in = eventval_type
260 AST.ident -> Events.eventval List.list -> AST.typ -> (io_out, io_in,
261 eventval_type) IOMonad.iO **)
262 let do_io fn args t =
263 IOMonad.Interact ({ io_function = fn; io_args = args; io_in_typ = t },
264 (fun res -> IOMonad.Value res))
266 (** val ret : 'a1 -> (io_out, io_in, 'a1) IOMonad.iO **)