19 open Hints_declaration
89 type ('outty, 'inty) trans_system = { is_final : (__ -> __ -> Integers.int
91 step : (__ -> __ -> ('outty, 'inty,
92 (Events.trace, __) Types.prod)
95 val trans_system_rect_Type4 :
96 (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
97 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
100 val trans_system_rect_Type5 :
101 (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
102 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
105 val trans_system_rect_Type3 :
106 (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
107 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
110 val trans_system_rect_Type2 :
111 (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
112 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
115 val trans_system_rect_Type1 :
116 (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
117 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
120 val trans_system_rect_Type0 :
121 (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
122 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
125 type ('outty, 'inty) global
127 type ('outty, 'inty) state
130 ('a1, 'a2) trans_system -> __ -> __ -> Integers.int Types.option
133 ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2, (Events.trace, __)
134 Types.prod) IOMonad.iO
136 val trans_system_inv_rect_Type4 :
137 ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
138 Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
139 IOMonad.iO) -> __ -> 'a3) -> 'a3
141 val trans_system_inv_rect_Type3 :
142 ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
143 Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
144 IOMonad.iO) -> __ -> 'a3) -> 'a3
146 val trans_system_inv_rect_Type2 :
147 ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
148 Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
149 IOMonad.iO) -> __ -> 'a3) -> 'a3
151 val trans_system_inv_rect_Type1 :
152 ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
153 Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
154 IOMonad.iO) -> __ -> 'a3) -> 'a3
156 val trans_system_inv_rect_Type0 :
157 ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
158 Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
159 IOMonad.iO) -> __ -> 'a3) -> 'a3
162 Nat.nat -> ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2, (Events.trace,
163 __) Types.prod) IOMonad.iO
166 ('a1 -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list ->
167 (Events.trace, 'a2 List.list) Types.prod Errors.res
169 type await_value_stuff = { avs_exec : (__, __) trans_system; avs_g :
170 __; avs_inv : (__ -> Bool.bool) }
172 val await_value_stuff_rect_Type4 :
173 (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
174 await_value_stuff -> 'a1
176 val await_value_stuff_rect_Type5 :
177 (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
178 await_value_stuff -> 'a1
180 val await_value_stuff_rect_Type3 :
181 (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
182 await_value_stuff -> 'a1
184 val await_value_stuff_rect_Type2 :
185 (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
186 await_value_stuff -> 'a1
188 val await_value_stuff_rect_Type1 :
189 (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
190 await_value_stuff -> 'a1
192 val await_value_stuff_rect_Type0 :
193 (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
194 await_value_stuff -> 'a1
200 val avs_exec : await_value_stuff -> (__, __) trans_system
202 val avs_g : await_value_stuff -> __
204 val avs_inv : await_value_stuff -> __ -> Bool.bool
206 val await_value_stuff_inv_rect_Type4 :
207 await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
208 Bool.bool) -> __ -> 'a1) -> 'a1
210 val await_value_stuff_inv_rect_Type3 :
211 await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
212 Bool.bool) -> __ -> 'a1) -> 'a1
214 val await_value_stuff_inv_rect_Type2 :
215 await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
216 Bool.bool) -> __ -> 'a1) -> 'a1
218 val await_value_stuff_inv_rect_Type1 :
219 await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
220 Bool.bool) -> __ -> 'a1) -> 'a1
222 val await_value_stuff_inv_rect_Type0 :
223 await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
224 Bool.bool) -> __ -> 'a1) -> 'a1
226 type ('state, 'output, 'input) execution = ('state, 'output, 'input) __execution Lazy.t
227 and ('state, 'output, 'input) __execution =
228 | E_stop of Events.trace * Integers.int * 'state
229 | E_step of Events.trace * 'state * ('state, 'output, 'input) execution
230 | E_wrong of Errors.errmsg
231 | E_interact of 'output * ('input -> ('state, 'output, 'input) execution)
233 val execution_inv_rect_Type4 :
234 ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
235 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
236 (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
239 val execution_inv_rect_Type3 :
240 ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
241 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
242 (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
245 val execution_inv_rect_Type2 :
246 ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
247 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
248 (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
251 val execution_inv_rect_Type1 :
252 ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
253 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
254 (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
257 val execution_inv_rect_Type0 :
258 ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
259 'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
260 (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
263 val execution_discr :
264 ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __
266 val execution_jmdiscr :
267 ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __
270 ('a1, 'a2) trans_system -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
271 IOMonad.iO -> (__, 'a1, 'a2) execution
273 type ('outty, 'inty) fullexec = { es1 : ('outty, 'inty) trans_system;
274 make_global : (__ -> __);
275 make_initial_state : (__ -> __ Errors.res) }
277 val fullexec_rect_Type4 :
278 (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
279 'a3) -> ('a1, 'a2) fullexec -> 'a3
281 val fullexec_rect_Type5 :
282 (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
283 'a3) -> ('a1, 'a2) fullexec -> 'a3
285 val fullexec_rect_Type3 :
286 (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
287 'a3) -> ('a1, 'a2) fullexec -> 'a3
289 val fullexec_rect_Type2 :
290 (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
291 'a3) -> ('a1, 'a2) fullexec -> 'a3
293 val fullexec_rect_Type1 :
294 (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
295 'a3) -> ('a1, 'a2) fullexec -> 'a3
297 val fullexec_rect_Type0 :
298 (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
299 'a3) -> ('a1, 'a2) fullexec -> 'a3
301 type ('outty, 'inty) program
303 val es1 : ('a1, 'a2) fullexec -> ('a1, 'a2) trans_system
305 val make_global : ('a1, 'a2) fullexec -> __ -> __
307 val make_initial_state : ('a1, 'a2) fullexec -> __ -> __ Errors.res
309 val fullexec_inv_rect_Type4 :
310 ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
311 -> __ Errors.res) -> __ -> 'a3) -> 'a3
313 val fullexec_inv_rect_Type3 :
314 ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
315 -> __ Errors.res) -> __ -> 'a3) -> 'a3
317 val fullexec_inv_rect_Type2 :
318 ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
319 -> __ Errors.res) -> __ -> 'a3) -> 'a3
321 val fullexec_inv_rect_Type1 :
322 ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
323 -> __ Errors.res) -> __ -> 'a3) -> 'a3
325 val fullexec_inv_rect_Type0 :
326 ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
327 -> __ Errors.res) -> __ -> 'a3) -> 'a3
329 val exec_inf : ('a1, 'a2) fullexec -> __ -> (__, 'a1, 'a2) execution
331 type 'x execution_prefix = (Events.trace, 'x) Types.prod List.list
334 ('a3, 'a1, 'a2) execution -> Nat.nat -> ('a3 execution_prefix, ('a3, 'a1,
335 'a2) execution) Types.prod Types.option
338 Nat.nat -> ('a1, 'a2) fullexec -> __ -> __ -> ((__, Events.trace)
339 Types.prod List.list, __) Types.prod Errors.res
341 val gather_trace : ('a1, Events.trace) Types.prod List.list -> Events.trace
343 val switch_trace_aux :
344 Events.trace -> ('a1, Events.trace) Types.prod List.list -> 'a1 ->
345 (Events.trace, 'a1) Types.prod List.list
348 ('a1, Events.trace) Types.prod List.list -> 'a1 -> (Events.trace, 'a1)