117 open Hints_declaration
129 open RTLabs_semantics
139 type ('o, 'i) flat_trace = ('o, 'i) __flat_trace Lazy.t
140 and ('o, 'i) __flat_trace =
141 | Ft_stop of RTLabs_semantics.state
142 | Ft_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
143 * ('o, 'i) flat_trace
145 (** val flat_trace_inv_rect_Type4 :
146 RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace
147 -> (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
148 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __
149 -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
150 let flat_trace_inv_rect_Type4 x3 x4 hterm h1 h2 =
154 | Ft_stop x -> h1 x __
155 | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2
159 (** val flat_trace_inv_rect_Type3 :
160 RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace
161 -> (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
162 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __
163 -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
164 let flat_trace_inv_rect_Type3 x3 x4 hterm h1 h2 =
168 | Ft_stop x -> h1 x __
169 | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2
173 (** val flat_trace_inv_rect_Type2 :
174 RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace
175 -> (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
176 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __
177 -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
178 let flat_trace_inv_rect_Type2 x3 x4 hterm h1 h2 =
182 | Ft_stop x -> h1 x __
183 | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2
187 (** val flat_trace_inv_rect_Type1 :
188 RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace
189 -> (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
190 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __
191 -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
192 let flat_trace_inv_rect_Type1 x3 x4 hterm h1 h2 =
196 | Ft_stop x -> h1 x __
197 | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2
201 (** val flat_trace_inv_rect_Type0 :
202 RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace
203 -> (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
204 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __
205 -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3 **)
206 let flat_trace_inv_rect_Type0 x3 x4 hterm h1 h2 =
210 | Ft_stop x -> h1 x __
211 | Ft_step (x, x0, x1, x2) -> h2 x x0 x1 __ x2
215 (** val flat_trace_discr :
216 RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace
217 -> ('a1, 'a2) flat_trace -> __ **)
218 let flat_trace_discr a3 a4 x y =
219 Logic.eq_rect_Type2 x
222 | Ft_stop a0 -> Obj.magic (fun _ dH -> dH __ __)
223 | Ft_step (a0, a10, a20, a40) ->
224 Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
226 (** val flat_trace_jmdiscr :
227 RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace
228 -> ('a1, 'a2) flat_trace -> __ **)
229 let flat_trace_jmdiscr a3 a4 x y =
230 Logic.eq_rect_Type2 x
233 | Ft_stop a0 -> Obj.magic (fun _ dH -> dH __ __)
234 | Ft_step (a0, a10, a20, a40) ->
235 Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
237 (** val make_flat_trace :
238 __ -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace **)
239 let rec make_flat_trace ge s =
241 SmallstepExec.exec_inf_aux
242 RTLabs_semantics.rTLabs_fullexec.SmallstepExec.es1 ge
243 (Obj.magic (RTLabs_semantics.eval_statement (Obj.magic ge) s))
247 | SmallstepExec.E_stop (tr, i, s') ->
248 (fun _ -> lazy (Ft_step (s, tr, (Obj.magic s'), (lazy (Ft_stop
250 | SmallstepExec.E_step (tr, s', e') ->
251 (fun _ -> lazy (Ft_step (s, tr, (Obj.magic s'),
252 (make_flat_trace ge (Obj.magic s')))))
253 | SmallstepExec.E_wrong m -> (fun _ -> assert false (* absurd case *))
254 | SmallstepExec.E_interact (o, f) ->
255 (fun _ -> assert false (* absurd case *))) __
257 (** val make_whole_flat_trace :
258 __ -> __ -> (IO.io_out, IO.io_in) flat_trace **)
259 let make_whole_flat_trace p s =
260 let ge = RTLabs_semantics.rTLabs_fullexec.SmallstepExec.make_global p in
262 SmallstepExec.exec_inf_aux
263 RTLabs_semantics.rTLabs_fullexec.SmallstepExec.es1 ge (IOMonad.Value
264 { Types.fst = Events.e0; Types.snd = s })
268 | SmallstepExec.E_stop (tr, i, s') ->
269 (fun _ -> lazy (Ft_stop (Obj.magic s)))
270 | SmallstepExec.E_step (x, x0, e') ->
271 (fun _ -> make_flat_trace ge (Obj.magic s))
272 | SmallstepExec.E_wrong m -> (fun _ -> assert false (* absurd case *))
273 | SmallstepExec.E_interact (o, f) ->
274 (fun _ -> assert false (* absurd case *))) __
277 | Wr_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
278 * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
279 | Wr_call of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
280 * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
281 | Wr_ret of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
282 * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
283 | Wr_base of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
284 * (IO.io_out, IO.io_in) flat_trace
286 (** val will_return_rect_Type4 :
287 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
288 RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
289 flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state
290 -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
291 IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
292 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
293 Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
294 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
295 RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
296 'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
297 flat_trace -> will_return -> 'a1 **)
298 let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1409 s x_1408 = function
299 | Wr_step (s0, tr, s', depth, trace, x_1411) ->
300 h_wr_step s0 tr s' depth __ trace __ x_1411
301 (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
303 | Wr_call (s0, tr, s', depth, trace, x_1413) ->
304 h_wr_call s0 tr s' depth __ trace __ x_1413
305 (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
306 depth) s' trace x_1413)
307 | Wr_ret (s0, tr, s', depth, trace, x_1415) ->
308 h_wr_ret s0 tr s' depth __ trace __ x_1415
309 (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
311 | Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
313 (** val will_return_rect_Type3 :
314 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
315 RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
316 flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state
317 -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
318 IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
319 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
320 Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
321 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
322 RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
323 'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
324 flat_trace -> will_return -> 'a1 **)
325 let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1437 s x_1436 = function
326 | Wr_step (s0, tr, s', depth, trace, x_1439) ->
327 h_wr_step s0 tr s' depth __ trace __ x_1439
328 (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
330 | Wr_call (s0, tr, s', depth, trace, x_1441) ->
331 h_wr_call s0 tr s' depth __ trace __ x_1441
332 (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
333 depth) s' trace x_1441)
334 | Wr_ret (s0, tr, s', depth, trace, x_1443) ->
335 h_wr_ret s0 tr s' depth __ trace __ x_1443
336 (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
338 | Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
340 (** val will_return_rect_Type2 :
341 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
342 RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
343 flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state
344 -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
345 IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
346 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
347 Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
348 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
349 RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
350 'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
351 flat_trace -> will_return -> 'a1 **)
352 let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1451 s x_1450 = function
353 | Wr_step (s0, tr, s', depth, trace, x_1453) ->
354 h_wr_step s0 tr s' depth __ trace __ x_1453
355 (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
357 | Wr_call (s0, tr, s', depth, trace, x_1455) ->
358 h_wr_call s0 tr s' depth __ trace __ x_1455
359 (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
360 depth) s' trace x_1455)
361 | Wr_ret (s0, tr, s', depth, trace, x_1457) ->
362 h_wr_ret s0 tr s' depth __ trace __ x_1457
363 (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
365 | Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
367 (** val will_return_rect_Type1 :
368 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
369 RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
370 flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state
371 -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
372 IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
373 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
374 Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
375 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
376 RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
377 'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
378 flat_trace -> will_return -> 'a1 **)
379 let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1465 s x_1464 = function
380 | Wr_step (s0, tr, s', depth, trace, x_1467) ->
381 h_wr_step s0 tr s' depth __ trace __ x_1467
382 (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
384 | Wr_call (s0, tr, s', depth, trace, x_1469) ->
385 h_wr_call s0 tr s' depth __ trace __ x_1469
386 (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
387 depth) s' trace x_1469)
388 | Wr_ret (s0, tr, s', depth, trace, x_1471) ->
389 h_wr_ret s0 tr s' depth __ trace __ x_1471
390 (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
392 | Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
394 (** val will_return_rect_Type0 :
395 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
396 RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
397 flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state
398 -> Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
399 IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
400 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
401 Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
402 'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
403 RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
404 'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
405 flat_trace -> will_return -> 'a1 **)
406 let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_1479 s x_1478 = function
407 | Wr_step (s0, tr, s', depth, trace, x_1481) ->
408 h_wr_step s0 tr s' depth __ trace __ x_1481
409 (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
411 | Wr_call (s0, tr, s', depth, trace, x_1483) ->
412 h_wr_call s0 tr s' depth __ trace __ x_1483
413 (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
414 depth) s' trace x_1483)
415 | Wr_ret (s0, tr, s', depth, trace, x_1485) ->
416 h_wr_ret s0 tr s' depth __ trace __ x_1485
417 (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
419 | Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
421 (** val will_return_inv_rect_Type4 :
422 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
423 IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
424 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
425 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
426 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
427 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
428 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
429 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
430 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
431 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
432 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
433 Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in)
434 flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
435 let will_return_inv_rect_Type4 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
436 let hcut = will_return_rect_Type4 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
439 (** val will_return_inv_rect_Type3 :
440 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
441 IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
442 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
443 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
444 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
445 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
446 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
447 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
448 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
449 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
450 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
451 Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in)
452 flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
453 let will_return_inv_rect_Type3 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
454 let hcut = will_return_rect_Type3 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
457 (** val will_return_inv_rect_Type2 :
458 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
459 IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
460 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
461 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
462 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
463 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
464 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
465 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
466 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
467 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
468 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
469 Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in)
470 flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
471 let will_return_inv_rect_Type2 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
472 let hcut = will_return_rect_Type2 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
475 (** val will_return_inv_rect_Type1 :
476 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
477 IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
478 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
479 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
480 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
481 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
482 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
483 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
484 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
485 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
486 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
487 Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in)
488 flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
489 let will_return_inv_rect_Type1 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
490 let hcut = will_return_rect_Type1 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
493 (** val will_return_inv_rect_Type0 :
494 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
495 IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
496 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
497 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
498 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
499 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
500 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
501 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
502 Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
503 IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ ->
504 'a1) -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state ->
505 Events.trace -> RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in)
506 flat_trace -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
507 let will_return_inv_rect_Type0 x1 x2 x3 x4 hterm h1 h2 h3 h4 =
508 let hcut = will_return_rect_Type0 x1 h1 h2 h3 h4 x2 x3 x4 hterm in
511 (** val will_return_jmdiscr :
512 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
513 IO.io_in) flat_trace -> will_return -> will_return -> __ **)
514 let will_return_jmdiscr a1 a2 a3 a4 x y =
515 Logic.eq_rect_Type2 x
517 | Wr_step (a0, a10, a20, a30, a5, a7) ->
518 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
519 | Wr_call (a0, a10, a20, a30, a5, a7) ->
520 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
521 | Wr_ret (a0, a10, a20, a30, a5, a7) ->
522 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
523 | Wr_base (a0, a10, a20, a40) ->
524 Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
526 (** val will_return_length :
527 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
528 IO.io_in) flat_trace -> will_return -> Nat.nat **)
529 let rec will_return_length ge d s tr = function
530 | Wr_step (x, x0, x1, x2, x4, t') ->
531 Nat.S (will_return_length ge x2 x1 x4 t')
532 | Wr_call (x, x0, x1, x2, x4, t') ->
533 Nat.S (will_return_length ge (Nat.S x2) x1 x4 t')
534 | Wr_ret (x, x0, x1, x2, x4, t') -> Nat.S (will_return_length ge x2 x1 x4 t')
535 | Wr_base (x, x0, x1, x3) -> Nat.S Nat.O
537 (** val will_return_end :
538 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
539 IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state,
540 (IO.io_out, IO.io_in) flat_trace) Types.dPair **)
541 let rec will_return_end ge d s tr = function
542 | Wr_step (x, x0, x1, x2, x4, t') -> will_return_end ge x2 x1 x4 t'
543 | Wr_call (x, x0, x1, x2, x4, t') -> will_return_end ge (Nat.S x2) x1 x4 t'
544 | Wr_ret (x, x0, x1, x2, x4, t') -> will_return_end ge x2 x1 x4 t'
545 | Wr_base (x, x0, x1, tr') -> { Types.dpi1 = x1; Types.dpi2 = tr' }
547 (** val will_return_call :
548 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state ->
549 Events.trace -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
550 flat_trace -> will_return -> will_return Types.sig0 **)
551 let will_return_call ge d s tr s' trace tERM =
552 will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace))) tERM
553 (fun h19 h20 h21 h22 _ h24 _ h26 h27 _ _ _ _ -> assert false
554 (* absurd case *)) (fun h33 h34 h35 h36 _ h38 _ h40 h41 _ _ _ _ ->
555 Logic.eq_rect_Type0_r h36 (fun tERM0 h410 _ ->
556 Logic.eq_rect_Type0_r h33 (fun _ _ _ tERM1 h411 _ ->
557 Obj.magic flat_trace_jmdiscr ge h33 (lazy (Ft_step (h33, tr, s',
558 trace))) (lazy (Ft_step (h33, h34, h35, h38))) __ (fun _ ->
559 Logic.streicherK h33 (fun _ ->
560 Logic.eq_rect_Type0_r h34 (fun _ _ tERM2 h412 _ _ ->
561 Logic.eq_rect_Type0_r h35 (fun trace0 _ _ tERM3 h413 _ _ ->
562 Logic.eq_rect_Type0_r __ (fun _ tERM4 h414 _ _ ->
563 Logic.eq_rect_Type0_r h38 (fun _ tERM5 h415 _ ->
564 Logic.streicherK (lazy (Ft_step (h33, h34, h35, h38)))
565 (Logic.eq_rect_Type0_r (Wr_call (h33, h34, h35, h36,
566 h38, h40)) (fun h416 -> h40) tERM5 h415)) trace0 __
567 tERM4 h414 __) __ __ tERM3 h413 __) s' trace __ __ tERM2
568 h412 __) tr __ __ tERM1 h411 __))) s __ __ __ tERM0 h410 __)
569 d tERM h41 __) (fun h47 h48 h49 h50 _ h52 _ h54 h55 _ _ _ _ ->
570 assert false (* absurd case *)) (fun h61 h62 h63 _ h65 _ _ _ _ _ ->
571 assert false (* absurd case *))
573 (** val will_return_return :
574 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state ->
575 Events.trace -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
576 flat_trace -> will_return -> __ **)
577 let will_return_return ge d s tr s' trace tERM =
578 will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace))) tERM
579 (fun h19 h20 h21 h22 _ h24 _ h26 h27 _ _ _ _ -> assert false
580 (* absurd case *)) (fun h33 h34 h35 h36 _ h38 _ h40 h41 _ _ _ _ ->
581 assert false (* absurd case *))
582 (fun h47 h48 h49 h50 _ h52 _ h54 h55 _ _ _ _ ->
583 Logic.eq_rect_Type0_r (Nat.S h50) (fun tERM0 h550 _ ->
584 Logic.eq_rect_Type0_r h47 (fun _ _ _ tERM1 h551 _ ->
585 Obj.magic flat_trace_jmdiscr ge h47 (lazy (Ft_step (h47, tr, s',
586 trace))) (lazy (Ft_step (h47, h48, h49, h52))) __ (fun _ ->
587 Logic.streicherK h47 (fun _ ->
588 Logic.eq_rect_Type0_r h48 (fun _ _ tERM2 h552 _ _ ->
589 Logic.eq_rect_Type0_r h49 (fun trace0 _ _ tERM3 h553 _ _ ->
590 Logic.eq_rect_Type0_r __ (fun _ tERM4 h554 _ _ ->
591 Logic.eq_rect_Type0_r h52 (fun _ tERM5 h555 _ ->
592 Logic.streicherK (lazy (Ft_step (h47, h48, h49, h52)))
593 (Logic.eq_rect_Type0_r (Wr_ret (h47, h48, h49, h50,
594 h52, h54)) (fun h556 -> h54) tERM5 h555)) trace0 __
595 tERM4 h554 __) __ __ tERM3 h553 __) s' trace __ __ tERM2
596 h552 __) tr __ __ tERM1 h551 __))) s __ __ __ tERM0 h550 __)
597 d tERM h55 __) (Obj.magic __)
599 (** val will_return_notfn :
600 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state ->
601 Events.trace -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
602 flat_trace -> (__, __) Types.sum -> will_return -> will_return Types.sig0 **)
603 let will_return_notfn ge d s tr s' trace = function
606 will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace)))
607 tERM (fun h290 h291 h292 h293 _ h295 _ h297 h298 _ _ _ _ ->
608 Logic.eq_rect_Type0_r h293 (fun tERM0 h2980 _ ->
609 Logic.eq_rect_Type0_r h290 (fun _ _ _ tERM1 h2981 _ ->
610 Obj.magic flat_trace_jmdiscr ge h290 (lazy (Ft_step (h290, tr, s',
611 trace))) (lazy (Ft_step (h290, h291, h292, h295))) __ (fun _ ->
612 Logic.streicherK h290 (fun _ ->
613 Logic.eq_rect_Type0_r h291 (fun _ _ tERM2 h2982 _ _ ->
614 Logic.eq_rect_Type0_r h292 (fun trace0 _ _ tERM3 h2983 _ _ ->
615 Logic.eq_rect_Type0_r __ (fun _ tERM4 h2984 _ _ ->
616 Logic.eq_rect_Type0_r h295 (fun _ tERM5 h2985 _ ->
617 Logic.streicherK (lazy (Ft_step (h290, h291, h292,
619 (Logic.eq_rect_Type0_r (Wr_step (h290, h291, h292,
620 h293, h295, h297)) (fun h2986 -> h297) tERM5 h2985))
621 trace0 __ tERM4 h2984 __) __ __ tERM3 h2983 __) s'
622 trace __ __ tERM2 h2982 __) tr __ __ tERM1 h2981 __))) s __
623 __ __ tERM0 h2980 __) d tERM h298 __)
624 (fun h304 h305 h306 h307 _ h309 _ h311 h312 _ _ _ _ -> assert false
626 (fun h318 h319 h320 h321 _ h323 _ h325 h326 _ _ _ _ -> assert false
627 (* absurd case *)) (fun h332 h333 h334 _ h336 _ _ _ _ _ -> assert false
631 will_return_inv_rect_Type0 ge d s (lazy (Ft_step (s, tr, s', trace)))
632 tERM (fun h343 h344 h345 h346 _ h348 _ h350 h351 _ _ _ _ ->
633 Logic.eq_rect_Type0_r h346 (fun tERM0 h3510 _ ->
634 Logic.eq_rect_Type0_r h343 (fun _ _ _ tERM1 h3511 _ ->
635 Obj.magic flat_trace_jmdiscr ge h343 (lazy (Ft_step (h343, tr, s',
636 trace))) (lazy (Ft_step (h343, h344, h345, h348))) __ (fun _ ->
637 Logic.streicherK h343 (fun _ ->
638 Logic.eq_rect_Type0_r h344 (fun _ _ tERM2 h3512 _ _ ->
639 Logic.eq_rect_Type0_r h345 (fun trace0 _ _ tERM3 h3513 _ _ ->
640 Logic.eq_rect_Type0_r __ (fun _ tERM4 h3514 _ _ ->
641 Logic.eq_rect_Type0_r h348 (fun _ tERM5 h3515 _ ->
642 Logic.streicherK (lazy (Ft_step (h343, h344, h345,
644 (Logic.eq_rect_Type0_r (Wr_step (h343, h344, h345,
645 h346, h348, h350)) (fun h3516 -> h350) tERM5 h3515))
646 trace0 __ tERM4 h3514 __) __ __ tERM3 h3513 __) s'
647 trace __ __ tERM2 h3512 __) tr __ __ tERM1 h3511 __))) s __
648 __ __ tERM0 h3510 __) d tERM h351 __)
649 (fun h357 h358 h359 h360 _ h362 _ h364 h365 _ _ _ _ -> assert false
651 (fun h371 h372 h373 h374 _ h376 _ h378 h379 _ _ _ _ -> assert false
652 (* absurd case *)) (fun h385 h386 h387 _ h389 _ _ _ _ _ -> assert false
655 (** val will_return_prepend :
656 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
657 IO.io_in) flat_trace -> will_return -> Nat.nat -> RTLabs_semantics.state
658 -> (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return **)
659 let will_return_prepend ge d1 s1 tr1 t1 d2 s2 t2 x =
660 will_return_rect_Type0 ge (fun s tr s' depth _ t _ t0 iH d3 s3 t3 t4 _ ->
661 Wr_step (s, tr, s', (Nat.plus depth (Nat.S d3)), t, (iH d3 s3 t3 t4 __)))
662 (fun s tr s' depth _ t _ t0 iH d3 s3 t3 t4 _ -> Wr_call (s, tr, s',
663 (Nat.plus depth (Nat.S d3)), t, (iH d3 s3 t3 t4 __)))
664 (fun s tr s' depth _ t _ t0 iH s3 s20 t3 t4 _ -> Wr_ret (s, tr, s',
665 (Nat.plus depth (Nat.S s3)), t, (iH s3 s20 t3 t4 __)))
666 (fun s tr s' _ t _ d3 s3 t3 t4 _ ->
667 Obj.magic Types.dPair_discr { Types.dpi1 = s'; Types.dpi2 = t }
668 { Types.dpi1 = s3; Types.dpi2 = t3 } __ (fun _ ->
669 Logic.eq_rect_Type0_r s3 (fun _ t0 _ _ ->
670 Logic.eq_rect_Type0_r t3 (fun _ ->
671 Logic.streicherK { Types.dpi1 = s3; Types.dpi2 = t3 } (Wr_ret (s,
672 tr, s3, d3, t3, t4))) t0 __) s' __ t __)) d1 s1 tr1 t1 d2 s2 t2 x
675 (** val nat_jmdiscr : Nat.nat -> Nat.nat -> __ **)
676 let nat_jmdiscr x y =
677 Logic.eq_rect_Type2 x
679 | Nat.O -> Obj.magic (fun _ dH -> dH)
680 | Nat.S a0 -> Obj.magic (fun _ dH -> dH __)) y
682 (** val will_return_remove_call :
683 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
684 IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return ->
685 RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return **)
686 let will_return_remove_call ge d1x s1x t1x t1 d2 x s2 t2 =
687 will_return_rect_Type0 ge (fun s tr s' d1 _ t _ t0 iH d3 t3 s3 t4 _ ->
689 (will_return_inv_rect_Type0 ge (Nat.plus d1 (Nat.S d3)) s
690 (lazy (Ft_step (s, tr, s', t))) t3
691 (fun h1 h2 h3 h4 _ h6 _ h8 h9 _ _ _ _ ->
692 Logic.eq_rect_Type0 (Nat.plus d1 (Nat.S d3)) (fun h80 h90 _ ->
693 Logic.eq_rect_Type0_r h1 (fun _ _ t20 _ _ h91 _ ->
694 Obj.magic flat_trace_jmdiscr ge h1 (lazy (Ft_step (h1, tr, s',
695 t))) (lazy (Ft_step (h1, h2, h3, h6))) __ (fun _ ->
696 Logic.streicherK h1 (fun _ ->
697 Logic.eq_rect_Type0_r h2 (fun _ t21 _ _ h92 _ _ ->
698 Logic.eq_rect_Type0_r h3
699 (fun t5 t6 iH0 _ t22 _ _ h93 _ _ ->
700 Logic.eq_rect_Type0_r __ (fun t23 _ _ h94 _ _ ->
701 Logic.eq_rect_Type0_r h6 (fun t7 iH1 t24 _ _ h95 _ ->
702 Logic.streicherK (lazy (Ft_step (h1, h2, h3, h6)))
703 (Logic.eq_rect_Type0_r (Wr_step (h1, h2, h3,
704 (Nat.plus d1 (Nat.S d3)), h6, h80)) (fun h96 ->
705 h80) t24 h95)) t5 t6 iH0 t23 __ __ h94 __) __ t22
706 __ __ h93 __) s' t t0 iH __ t21 __ __ h92 __) tr __ t20
707 __ __ h91 __))) s __ __ t3 __ __ h90 __) h4 h8 h9 __)
708 (fun h15 h16 h17 h18 _ h20 _ h22 h23 _ _ _ _ -> assert false
709 (* absurd case *)) (fun h29 h30 h31 h32 _ h34 _ h36 h37 _ _ _ _ ->
710 assert false (* absurd case *)) (fun h43 h44 h45 _ h47 _ _ _ _ _ ->
711 assert false (* absurd case *))) s3 t4 __)
712 (fun s tr s' d1 _ t _ t0 iH d3 t3 s3 t4 _ ->
714 (will_return_inv_rect_Type0 ge (Nat.plus d1 (Nat.S d3)) s
715 (lazy (Ft_step (s, tr, s', t))) t3
716 (fun h1 h2 h3 h4 _ h6 _ h8 h9 _ _ _ _ -> assert false
717 (* absurd case *)) (fun h15 h16 h17 h18 _ h20 _ h22 h23 _ _ _ _ ->
718 Logic.eq_rect_Type0 (Nat.plus d1 (Nat.S d3)) (fun h220 h230 _ ->
719 Logic.eq_rect_Type0_r h15 (fun _ _ t20 _ _ h231 _ ->
720 Obj.magic flat_trace_jmdiscr ge h15 (lazy (Ft_step (h15, tr, s',
721 t))) (lazy (Ft_step (h15, h16, h17, h20))) __ (fun _ ->
722 Logic.streicherK h15 (fun _ ->
723 Logic.eq_rect_Type0_r h16 (fun _ t21 _ _ h232 _ _ ->
724 Logic.eq_rect_Type0_r h17
725 (fun t5 t6 iH0 _ t22 _ _ h233 _ _ ->
726 Logic.eq_rect_Type0_r __ (fun t23 _ _ h234 _ _ ->
727 Logic.eq_rect_Type0_r h20 (fun t7 iH1 t24 _ _ h235 _ ->
728 Logic.streicherK (lazy (Ft_step (h15, h16, h17,
730 (Logic.eq_rect_Type0_r (Wr_call (h15, h16, h17,
731 (Nat.plus d1 (Nat.S d3)), h20, h220))
732 (fun h236 -> h220) t24 h235)) t5 t6 iH0 t23 __ __
733 h234 __) __ t22 __ __ h233 __) s' t t0 iH __ t21 __
734 __ h232 __) tr __ t20 __ __ h231 __))) s __ __ t3 __ __
735 h230 __) h18 h22 h23 __)
736 (fun h29 h30 h31 h32 _ h34 _ h36 h37 _ _ _ _ -> assert false
737 (* absurd case *)) (fun h43 h44 h45 _ h47 _ _ _ _ _ -> assert false
738 (* absurd case *))) s3 t4 __)
739 (fun s tr s' d1 _ t _ t0 iH d3 t3 s3 t4 _ ->
741 (will_return_inv_rect_Type0 ge (Nat.plus (Nat.S d1) (Nat.S d3)) s
742 (lazy (Ft_step (s, tr, s', t))) t3
743 (fun h1 h2 h3 h4 _ h6 _ h8 h9 _ _ _ _ -> assert false
744 (* absurd case *)) (fun h15 h16 h17 h18 _ h20 _ h22 h23 _ _ _ _ ->
745 assert false (* absurd case *))
746 (fun h29 h30 h31 h32 _ h34 _ h36 h37 _ _ _ _ ->
747 Obj.magic nat_jmdiscr (Nat.S (Nat.plus d1 (Nat.S d3))) (Nat.S h32) __
748 (Logic.eq_rect_Type0_r h29 (fun _ _ t20 _ h370 _ _ ->
749 Obj.magic flat_trace_jmdiscr ge h29 (lazy (Ft_step (h29, tr, s',
750 t))) (lazy (Ft_step (h29, h30, h31, h34))) __ (fun _ ->
751 Logic.streicherK h29 (fun _ ->
752 Logic.eq_rect_Type0_r h30 (fun _ t21 _ h371 _ _ _ ->
753 Logic.eq_rect_Type0_r h31
754 (fun t5 t6 iH0 _ t22 _ h372 _ _ _ ->
755 Logic.eq_rect_Type0_r __ (fun t23 _ h373 _ _ _ ->
756 Logic.eq_rect_Type0_r h34 (fun t7 iH1 t24 _ h374 _ _ ->
757 Logic.streicherK (lazy (Ft_step (h29, h30, h31,
759 Logic.eq_rect_Type0 (Nat.plus d1 (Nat.S d3))
760 (fun h360 _ h375 _ ->
761 Logic.streicherK (Nat.S (Nat.plus d1 (Nat.S d3)))
762 (Logic.eq_rect_Type0_r (Wr_ret (h29, h30, h31,
763 (Nat.plus d1 (Nat.S d3)), h34, h360))
764 (fun h376 -> h360) t24 h375)) h32 h36 __ h374
765 __)) t5 t6 iH0 t23 __ h373 __ __) __ t22 __ h372
766 __ __) s' t t0 iH __ t21 __ h371 __ __) tr __ t20 __
767 h370 __ __))) s __ __ t3 __ h37 __ __))
768 (fun h43 h44 h45 _ h47 _ _ _ _ _ -> assert false (* absurd case *)))
769 s3 t4 __) (fun s tr s' _ t _ d3 t3 s3 t4 _ ->
770 Obj.magic Types.dPair_discr { Types.dpi1 = s'; Types.dpi2 = t }
771 { Types.dpi1 = s3; Types.dpi2 = t4 } __ (fun _ ->
772 Logic.eq_rect_Type0_r s3 (fun _ t0 t20 _ _ ->
773 Logic.eq_rect_Type0_r t4 (fun t21 _ ->
774 Logic.streicherK { Types.dpi1 = s3; Types.dpi2 = t4 }
775 (will_return_inv_rect_Type0 ge (Nat.plus Nat.O (Nat.S d3)) s
776 (lazy (Ft_step (s, tr, s3, t4))) t21
777 (fun h1 h2 h3 h4 _ h6 _ h8 h9 _ _ _ _ -> assert false
779 (fun h15 h16 h17 h18 _ h20 _ h22 h23 _ _ _ _ -> assert false
781 (fun h29 h30 h31 h32 _ h34 _ h36 h37 _ _ _ _ ->
782 Obj.magic nat_jmdiscr (Nat.S d3) (Nat.S h32) __
783 (Logic.eq_rect_Type0_r h29 (fun _ _ t22 h370 _ _ ->
784 Obj.magic flat_trace_jmdiscr ge h29 (lazy (Ft_step (h29,
785 tr, s3, t4))) (lazy (Ft_step (h29, h30, h31, h34))) __
787 Logic.streicherK h29 (fun _ ->
788 Logic.eq_rect_Type0_r h30 (fun _ t23 h371 _ _ _ ->
789 Logic.eq_rect_Type0_r h31
790 (fun t24 _ t25 h372 _ _ _ ->
791 Logic.eq_rect_Type0_r __ (fun t26 h373 _ _ _ ->
792 Logic.eq_rect_Type0_r h34 (fun t27 h374 _ _ ->
793 Logic.streicherK (lazy (Ft_step (h29, h30, h31,
795 Logic.eq_rect_Type0_r h32
797 Logic.streicherK (Nat.S h32)
798 (Logic.eq_rect_Type0_r (Wr_ret (h29, h30,
799 h31, h32, h34, h36)) (fun h376 -> h36)
800 t28 h375)) d3 __ t27 h374 __)) t24 t26
801 h373 __ __) __ t25 h372 __ __) s3 t4 __ t23
802 h371 __ __) tr __ t22 h370 __ __))) s __ __ t21 h37
803 __ __)) (fun h43 h44 h45 _ h47 _ _ _ _ _ -> assert false
804 (* absurd case *)))) t0 t20 __) s' __ t t3 __)) d1x s1x t1x t1
807 (** val will_return_lower :
808 RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
809 IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return **)
810 let will_return_lower ge d0 s0 t0 tM d' =
811 will_return_rect_Type0 ge (fun s tr s' d _ tr0 _ tM1 iH d'0 _ -> Wr_step
812 (s, tr, s', d'0, tr0, (iH d'0 __)))
813 (fun s tr s' d _ tr0 _ tM1 iH d'0 _ -> Wr_call (s, tr, s', d'0, tr0,
814 (iH (Nat.S d'0) __))) (fun s tr s' d _ tr0 _ tM1 iH clearme ->
816 | Nat.O -> (fun _ -> Wr_base (s, tr, s', tr0))
817 | Nat.S d'0 -> (fun _ -> Wr_ret (s, tr, s', d'0, tr0, (iH d'0 __))))
818 (fun s tr s' _ tr0 _ clearme ->
820 | Nat.O -> (fun _ -> Wr_base (s, tr, s', tr0))
821 | Nat.S d'0 -> (fun _ -> assert false (* absurd case *))) d0 s0 t0 tM d'
824 (** val list_jmdiscr : 'a1 List.list -> 'a1 List.list -> __ **)
825 let list_jmdiscr x y =
826 Logic.eq_rect_Type2 x
828 | List.Nil -> Obj.magic (fun _ dH -> dH)
829 | List.Cons (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
831 type 't trace_result = { new_state : RTLabs_abstract.rTLabs_ext_state;
832 remainder : (IO.io_out, IO.io_in) flat_trace;
833 new_trace : 't; terminates : __ }
835 (** val trace_result_rect_Type4 :
836 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
837 -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
838 -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
839 (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
840 trace_result -> 'a2 **)
841 let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_2020 =
842 let { new_state = new_state0; remainder = remainder0; new_trace =
843 new_trace0; terminates = terminates0 } = x_2020
845 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
847 (** val trace_result_rect_Type5 :
848 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
849 -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
850 -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
851 (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
852 trace_result -> 'a2 **)
853 let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_2022 =
854 let { new_state = new_state0; remainder = remainder0; new_trace =
855 new_trace0; terminates = terminates0 } = x_2022
857 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
859 (** val trace_result_rect_Type3 :
860 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
861 -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
862 -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
863 (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
864 trace_result -> 'a2 **)
865 let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_2024 =
866 let { new_state = new_state0; remainder = remainder0; new_trace =
867 new_trace0; terminates = terminates0 } = x_2024
869 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
871 (** val trace_result_rect_Type2 :
872 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
873 -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
874 -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
875 (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
876 trace_result -> 'a2 **)
877 let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_2026 =
878 let { new_state = new_state0; remainder = remainder0; new_trace =
879 new_trace0; terminates = terminates0 } = x_2026
881 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
883 (** val trace_result_rect_Type1 :
884 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
885 -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
886 -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
887 (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
888 trace_result -> 'a2 **)
889 let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_2028 =
890 let { new_state = new_state0; remainder = remainder0; new_trace =
891 new_trace0; terminates = terminates0 } = x_2028
893 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
895 (** val trace_result_rect_Type0 :
896 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
897 -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
898 -> will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state ->
899 (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
900 trace_result -> 'a2 **)
901 let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_2030 =
902 let { new_state = new_state0; remainder = remainder0; new_trace =
903 new_trace0; terminates = terminates0 } = x_2030
905 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
908 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
909 -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
910 -> will_return -> Nat.nat -> 'a1 trace_result ->
911 RTLabs_abstract.rTLabs_ext_state **)
912 let rec new_state ge depth ends start full original_terminates limit xxx =
916 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
917 -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
918 -> will_return -> Nat.nat -> 'a1 trace_result -> (IO.io_out, IO.io_in)
920 let rec remainder ge depth ends start full original_terminates limit xxx =
924 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
925 -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
926 -> will_return -> Nat.nat -> 'a1 trace_result -> 'a1 **)
927 let rec new_trace ge depth ends start full original_terminates limit xxx =
931 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
932 -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
933 -> will_return -> Nat.nat -> 'a1 trace_result -> __ **)
934 let rec terminates ge depth ends start full original_terminates limit xxx =
937 (** val trace_result_inv_rect_Type4 :
938 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
939 -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
940 -> will_return -> Nat.nat -> 'a1 trace_result ->
941 (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
942 __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **)
943 let trace_result_inv_rect_Type4 x1 x2 x3 x4 x5 x6 x8 hterm h1 =
944 let hcut = trace_result_rect_Type4 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __
946 (** val trace_result_inv_rect_Type3 :
947 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
948 -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
949 -> will_return -> Nat.nat -> 'a1 trace_result ->
950 (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
951 __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **)
952 let trace_result_inv_rect_Type3 x1 x2 x3 x4 x5 x6 x8 hterm h1 =
953 let hcut = trace_result_rect_Type3 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __
955 (** val trace_result_inv_rect_Type2 :
956 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
957 -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
958 -> will_return -> Nat.nat -> 'a1 trace_result ->
959 (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
960 __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **)
961 let trace_result_inv_rect_Type2 x1 x2 x3 x4 x5 x6 x8 hterm h1 =
962 let hcut = trace_result_rect_Type2 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __
964 (** val trace_result_inv_rect_Type1 :
965 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
966 -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
967 -> will_return -> Nat.nat -> 'a1 trace_result ->
968 (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
969 __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **)
970 let trace_result_inv_rect_Type1 x1 x2 x3 x4 x5 x6 x8 hterm h1 =
971 let hcut = trace_result_rect_Type1 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __
973 (** val trace_result_inv_rect_Type0 :
974 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
975 -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
976 -> will_return -> Nat.nat -> 'a1 trace_result ->
977 (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
978 __ -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2 **)
979 let trace_result_inv_rect_Type0 x1 x2 x3 x4 x5 x6 x8 hterm h1 =
980 let hcut = trace_result_rect_Type0 x1 x2 x3 x4 x5 x6 x8 h1 hterm in hcut __
982 (** val trace_result_jmdiscr :
983 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
984 -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace
985 -> will_return -> Nat.nat -> 'a1 trace_result -> 'a1 trace_result -> __ **)
986 let trace_result_jmdiscr a1 a2 a3 a4 a5 a6 a8 x y =
987 Logic.eq_rect_Type2 x
988 (let { new_state = a0; remainder = a10; new_trace = a30; terminates =
991 Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
993 type 't sub_trace_result = { ends : StructuredTraces.trace_ends_with_ret;
994 trace_res : 't trace_result }
996 (** val sub_trace_result_rect_Type4 :
997 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
998 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
999 (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1000 sub_trace_result -> 'a2 **)
1001 let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_2048 =
1002 let { ends = ends0; trace_res = trace_res0 } = x_2048 in
1003 h_mk_sub_trace_result ends0 trace_res0
1005 (** val sub_trace_result_rect_Type5 :
1006 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1007 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1008 (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1009 sub_trace_result -> 'a2 **)
1010 let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_2050 =
1011 let { ends = ends0; trace_res = trace_res0 } = x_2050 in
1012 h_mk_sub_trace_result ends0 trace_res0
1014 (** val sub_trace_result_rect_Type3 :
1015 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1016 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1017 (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1018 sub_trace_result -> 'a2 **)
1019 let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_2052 =
1020 let { ends = ends0; trace_res = trace_res0 } = x_2052 in
1021 h_mk_sub_trace_result ends0 trace_res0
1023 (** val sub_trace_result_rect_Type2 :
1024 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1025 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1026 (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1027 sub_trace_result -> 'a2 **)
1028 let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_2054 =
1029 let { ends = ends0; trace_res = trace_res0 } = x_2054 in
1030 h_mk_sub_trace_result ends0 trace_res0
1032 (** val sub_trace_result_rect_Type1 :
1033 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1034 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1035 (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1036 sub_trace_result -> 'a2 **)
1037 let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_2056 =
1038 let { ends = ends0; trace_res = trace_res0 } = x_2056 in
1039 h_mk_sub_trace_result ends0 trace_res0
1041 (** val sub_trace_result_rect_Type0 :
1042 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1043 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1044 (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
1045 sub_trace_result -> 'a2 **)
1046 let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_2058 =
1047 let { ends = ends0; trace_res = trace_res0 } = x_2058 in
1048 h_mk_sub_trace_result ends0 trace_res0
1051 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1052 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1053 sub_trace_result -> StructuredTraces.trace_ends_with_ret **)
1054 let rec ends ge depth start full original_terminates limit xxx =
1058 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1059 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1060 sub_trace_result -> 'a1 trace_result **)
1061 let rec trace_res ge depth start full original_terminates limit xxx =
1064 (** val sub_trace_result_inv_rect_Type4 :
1065 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1066 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1067 sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
1068 trace_result -> __ -> 'a2) -> 'a2 **)
1069 let sub_trace_result_inv_rect_Type4 x1 x2 x3 x4 x5 x7 hterm h1 =
1070 let hcut = sub_trace_result_rect_Type4 x1 x2 x3 x4 x5 x7 h1 hterm in
1073 (** val sub_trace_result_inv_rect_Type3 :
1074 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1075 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1076 sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
1077 trace_result -> __ -> 'a2) -> 'a2 **)
1078 let sub_trace_result_inv_rect_Type3 x1 x2 x3 x4 x5 x7 hterm h1 =
1079 let hcut = sub_trace_result_rect_Type3 x1 x2 x3 x4 x5 x7 h1 hterm in
1082 (** val sub_trace_result_inv_rect_Type2 :
1083 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1084 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1085 sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
1086 trace_result -> __ -> 'a2) -> 'a2 **)
1087 let sub_trace_result_inv_rect_Type2 x1 x2 x3 x4 x5 x7 hterm h1 =
1088 let hcut = sub_trace_result_rect_Type2 x1 x2 x3 x4 x5 x7 h1 hterm in
1091 (** val sub_trace_result_inv_rect_Type1 :
1092 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1093 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1094 sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
1095 trace_result -> __ -> 'a2) -> 'a2 **)
1096 let sub_trace_result_inv_rect_Type1 x1 x2 x3 x4 x5 x7 hterm h1 =
1097 let hcut = sub_trace_result_rect_Type1 x1 x2 x3 x4 x5 x7 h1 hterm in
1100 (** val sub_trace_result_inv_rect_Type0 :
1101 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1102 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1103 sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
1104 trace_result -> __ -> 'a2) -> 'a2 **)
1105 let sub_trace_result_inv_rect_Type0 x1 x2 x3 x4 x5 x7 hterm h1 =
1106 let hcut = sub_trace_result_rect_Type0 x1 x2 x3 x4 x5 x7 h1 hterm in
1109 (** val sub_trace_result_discr :
1110 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1111 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1112 sub_trace_result -> 'a1 sub_trace_result -> __ **)
1113 let sub_trace_result_discr a1 a2 a3 a4 a5 a7 x y =
1114 Logic.eq_rect_Type2 x
1115 (let { ends = a0; trace_res = a10 } = x in
1116 Obj.magic (fun _ dH -> dH __ __)) y
1118 (** val sub_trace_result_jmdiscr :
1119 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1120 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
1121 sub_trace_result -> 'a1 sub_trace_result -> __ **)
1122 let sub_trace_result_jmdiscr a1 a2 a3 a4 a5 a7 x y =
1123 Logic.eq_rect_Type2 x
1124 (let { ends = a0; trace_res = a10 } = x in
1125 Obj.magic (fun _ dH -> dH __ __)) y
1127 (** val replace_trace :
1128 RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret
1129 -> RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state
1130 -> (IO.io_out, IO.io_in) flat_trace -> (IO.io_out, IO.io_in) flat_trace
1131 -> will_return -> will_return -> Nat.nat -> Nat.nat -> 'a1 trace_result
1132 -> 'a2 -> 'a2 trace_result **)
1133 let replace_trace ge d e s1 s2 t1 t2 tM1 tM2 l1 l2 r trace =
1134 { new_state = r.new_state; remainder = r.remainder; new_trace = trace;
1137 | StructuredTraces.Ends_with_ret ->
1139 (will_return_end ge d s1.RTLabs_abstract.ras_state t1 tM1)
1141 let { new_state = x; remainder = x0; new_trace = x1; terminates =
1145 | Nat.O -> Obj.magic __
1147 (fun tM10 tM20 ns rem _ t1NS _ clearme0 ->
1148 let tMa = Obj.magic clearme0 in Obj.magic tMa)) tM1 tM2 x x0
1150 (will_return_end ge d s2.RTLabs_abstract.ras_state t2 tM2)
1151 | StructuredTraces.Doesnt_end_with_ret ->
1153 (will_return_end ge d s1.RTLabs_abstract.ras_state t1 tM1)
1155 let { new_state = ns; remainder = rem; new_trace = t1NS;
1156 terminates = clearme0 } = clearme
1158 let tMa = Obj.magic clearme0 in Obj.magic tMa)
1159 (will_return_end ge d s2.RTLabs_abstract.ras_state t2 tM2)) r) }
1161 (** val replace_sub_trace :
1162 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1163 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
1164 (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return -> Nat.nat
1165 -> Nat.nat -> 'a1 sub_trace_result -> 'a2 -> 'a2 sub_trace_result **)
1166 let replace_sub_trace ge d s1 s2 t1 t2 tM1 tM2 l1 l2 r trace =
1167 { ends = r.ends; trace_res =
1168 (replace_trace ge d r.ends s1 s2 t1 t2 tM1 tM2 l1 l2 r.trace_res trace) }
1170 (** val make_label_return :
1171 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1172 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1173 StructuredTraces.trace_label_return trace_result **)
1174 let rec make_label_return ge depth s trace tERMINATES tIME =
1176 | Nat.O -> (fun _ -> assert false (* absurd case *))
1179 let r = make_label_label ge depth s trace tERMINATES tIME0 in
1181 | StructuredTraces.Ends_with_ret ->
1183 replace_trace ge depth StructuredTraces.Ends_with_ret s s trace
1184 trace tERMINATES tERMINATES
1185 (will_return_length ge depth s.RTLabs_abstract.ras_state trace
1187 (will_return_length ge depth s.RTLabs_abstract.ras_state trace
1188 tERMINATES) r0 (StructuredTraces.Tlr_base ((Obj.magic s),
1189 (Obj.magic r0.new_state), r0.new_trace)))
1190 | StructuredTraces.Doesnt_end_with_ret ->
1193 make_label_return ge depth r0.new_state r0.remainder
1194 (Types.pi1 (Obj.magic r0.terminates)) tIME0
1196 replace_trace ge depth StructuredTraces.Ends_with_ret
1197 r0.new_state s r0.remainder trace
1198 (Types.pi1 (Obj.magic r0.terminates)) tERMINATES
1199 (will_return_length ge depth
1200 r0.new_state.RTLabs_abstract.ras_state r0.remainder
1201 (Types.pi1 (Obj.magic r0.terminates)))
1202 (will_return_length ge depth s.RTLabs_abstract.ras_state trace
1203 tERMINATES) r' (StructuredTraces.Tlr_step ((Obj.magic s),
1204 (Obj.magic r0.new_state), (Obj.magic r'.new_state),
1205 r0.new_trace, r'.new_trace)))) r.trace_res)) __
1206 (** val make_label_label :
1207 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1208 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1209 StructuredTraces.trace_label_label sub_trace_result **)
1210 and make_label_label ge depth s trace tERMINATES tIME =
1212 | Nat.O -> (fun _ -> assert false (* absurd case *))
1215 let r = make_any_label ge depth s trace tERMINATES tIME0 in
1216 replace_sub_trace ge depth s s trace trace tERMINATES tERMINATES
1217 (will_return_length ge depth s.RTLabs_abstract.ras_state trace
1219 (will_return_length ge depth s.RTLabs_abstract.ras_state trace
1220 tERMINATES) r (StructuredTraces.Tll_base (r.ends, (Obj.magic s),
1221 (Obj.magic r.trace_res.new_state), r.trace_res.new_trace)))) __
1222 (** val make_any_label :
1223 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1224 (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
1225 StructuredTraces.trace_any_label sub_trace_result **)
1226 and make_any_label ge depth s0 trace tERMINATES tIME =
1228 | Nat.O -> (fun _ -> assert false (* absurd case *))
1231 (let { RTLabs_abstract.ras_state = s; RTLabs_abstract.ras_fn_stack =
1234 (fun trace0 _ tM _ ->
1238 (fun _ _ tERMINATES0 _ -> assert false (* absurd case *))
1239 | Ft_step (start, tr, next, trace') ->
1240 (fun _ _ tERMINATES0 _ ->
1241 let start' = { RTLabs_abstract.ras_state = start;
1242 RTLabs_abstract.ras_fn_stack = stk }
1244 let next' = RTLabs_abstract.next_state ge start' next tr in
1245 (match RTLabs_abstract.rTLabs_classify start with
1246 | StructuredTraces.Cl_return ->
1247 (fun _ -> { ends = StructuredTraces.Ends_with_ret; trace_res =
1248 { new_state = next'; remainder = trace'; new_trace =
1249 (StructuredTraces.Tal_base_return ((Obj.magic start'),
1250 (Obj.magic next'))); terminates =
1251 (will_return_return ge depth start tr next trace'
1253 | StructuredTraces.Cl_jump ->
1254 (fun _ -> { ends = StructuredTraces.Doesnt_end_with_ret;
1255 trace_res = { new_state = next'; remainder = trace';
1256 new_trace = (StructuredTraces.Tal_base_not_return
1257 ((Obj.magic start'), (Obj.magic next'))); terminates =
1259 (will_return_notfn ge depth start tr next trace'
1260 (Types.Inr __) tERMINATES0)) } })
1261 | StructuredTraces.Cl_call ->
1264 make_label_return ge (Nat.S depth) next' trace'
1266 (will_return_call ge depth start tr next trace'
1269 (match RTLabs_abstract.rTLabs_cost
1270 r.new_state.RTLabs_abstract.ras_state with
1272 (fun _ -> { ends = StructuredTraces.Doesnt_end_with_ret;
1273 trace_res = { new_state = r.new_state; remainder =
1274 r.remainder; new_trace =
1275 (StructuredTraces.Tal_base_call ((Obj.magic start'),
1276 (Obj.magic next'), (Obj.magic r.new_state),
1277 r.new_trace)); terminates =
1278 (let tMr = Obj.magic r.terminates in Obj.magic tMr) } })
1282 make_any_label ge depth r.new_state r.remainder
1283 (Types.pi1 (Obj.magic r.terminates)) tIME0
1285 replace_sub_trace ge depth r.new_state start'
1286 r.remainder (lazy (Ft_step (start, tr, next,
1287 trace'))) (Types.pi1 (Obj.magic r.terminates))
1289 (will_return_length ge depth
1290 r.new_state.RTLabs_abstract.ras_state r.remainder
1291 (Types.pi1 (Obj.magic r.terminates)))
1292 (will_return_length ge depth start (lazy (Ft_step
1293 (start, tr, next, trace'))) tERMINATES0) r'
1294 (StructuredTraces.Tal_step_call (r'.ends,
1295 (Obj.magic start'), (Obj.magic next'),
1296 (Obj.magic r.new_state),
1297 (Obj.magic r'.trace_res.new_state), r.new_trace,
1298 r'.trace_res.new_trace)))) __)
1299 | StructuredTraces.Cl_tailcall ->
1300 (fun _ -> assert false (* absurd case *))
1301 | StructuredTraces.Cl_other ->
1303 (match RTLabs_abstract.rTLabs_cost next with
1305 (fun _ -> { ends = StructuredTraces.Doesnt_end_with_ret;
1306 trace_res = { new_state = next'; remainder = trace';
1307 new_trace = (StructuredTraces.Tal_base_not_return
1308 ((Obj.magic start'), (Obj.magic next'))); terminates =
1310 (will_return_notfn ge depth start tr next trace'
1311 (Types.Inl __) tERMINATES0)) } })
1315 make_any_label ge depth next' trace'
1317 (will_return_notfn ge depth start tr next trace'
1318 (Types.Inl __) tERMINATES0)) tIME0
1320 replace_sub_trace ge depth next' start' trace'
1321 (lazy (Ft_step (start, tr, next, trace')))
1323 (will_return_notfn ge depth start tr next trace'
1324 (Types.Inl __) tERMINATES0)) tERMINATES0
1325 (will_return_length ge depth
1326 next'.RTLabs_abstract.ras_state trace'
1328 (will_return_notfn ge depth start tr next trace'
1329 (Types.Inl __) tERMINATES0)))
1330 (will_return_length ge depth start (lazy (Ft_step
1331 (start, tr, next, trace'))) tERMINATES0) r
1332 (StructuredTraces.Tal_step_default (r.ends,
1333 (Obj.magic start'), (Obj.magic next'),
1334 (Obj.magic r.trace_res.new_state),
1335 r.trace_res.new_trace)))) __)) __)) __ __ tM __))
1336 trace __ tERMINATES __)) __
1338 (** val make_label_return' :
1339 RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
1340 (IO.io_out, IO.io_in) flat_trace -> will_return ->
1341 StructuredTraces.trace_label_return trace_result **)
1342 let rec make_label_return' ge depth s trace tERMINATES =
1343 make_label_return ge depth s trace tERMINATES
1344 (Nat.plus (Nat.S (Nat.S Nat.O))
1345 (Nat.times (Nat.S (Nat.S (Nat.S Nat.O)))
1346 (will_return_length ge depth s.RTLabs_abstract.ras_state trace
1349 (** val actual_successor :
1350 RTLabs_semantics.state -> Graphs.label Types.option **)
1351 let actual_successor = function
1352 | RTLabs_semantics.State (f, fs, m) -> Types.Some f.RTLabs_semantics.next
1353 | RTLabs_semantics.Callstate (x, x0, x1, x2, fs, x3) ->
1355 | List.Nil -> Types.None
1356 | List.Cons (f, x4) -> Types.Some f.RTLabs_semantics.next)
1357 | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Types.None
1358 | RTLabs_semantics.Finalstate x -> Types.None
1360 (** val steps_for_statement : RTLabs_syntax.statement -> Nat.nat **)
1361 let steps_for_statement s =
1364 | RTLabs_syntax.St_skip x -> Nat.O
1365 | RTLabs_syntax.St_cost (x, x0) -> Nat.O
1366 | RTLabs_syntax.St_const (x, x0, x1, x2) -> Nat.O
1367 | RTLabs_syntax.St_op1 (x, x0, x1, x2, x3, x4) -> Nat.O
1368 | RTLabs_syntax.St_op2 (x, x0, x1, x2, x3, x4, x5, x6) -> Nat.O
1369 | RTLabs_syntax.St_load (x, x0, x1, x2) -> Nat.O
1370 | RTLabs_syntax.St_store (x, x0, x1, x2) -> Nat.O
1371 | RTLabs_syntax.St_call_id (x, x0, x1, x2) -> Nat.S Nat.O
1372 | RTLabs_syntax.St_call_ptr (x, x0, x1, x2) -> Nat.S Nat.O
1373 | RTLabs_syntax.St_cond (x, x0, x1) -> Nat.O
1374 | RTLabs_syntax.St_return -> Nat.S Nat.O)
1379 (** val remainder_ok_rect_Type4 :
1380 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1381 IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1383 let rec remainder_ok_rect_Type4 ge s t h_mk_remainder_ok = function
1384 | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1386 (** val remainder_ok_rect_Type5 :
1387 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1388 IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1390 let rec remainder_ok_rect_Type5 ge s t h_mk_remainder_ok = function
1391 | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1393 (** val remainder_ok_rect_Type3 :
1394 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1395 IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1397 let rec remainder_ok_rect_Type3 ge s t h_mk_remainder_ok = function
1398 | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1400 (** val remainder_ok_rect_Type2 :
1401 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1402 IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1404 let rec remainder_ok_rect_Type2 ge s t h_mk_remainder_ok = function
1405 | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1407 (** val remainder_ok_rect_Type1 :
1408 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1409 IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1411 let rec remainder_ok_rect_Type1 ge s t h_mk_remainder_ok = function
1412 | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1414 (** val remainder_ok_rect_Type0 :
1415 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1416 IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
1418 let rec remainder_ok_rect_Type0 ge s t h_mk_remainder_ok = function
1419 | Mk_remainder_ok -> h_mk_remainder_ok __ __ __ __
1421 (** val remainder_ok_inv_rect_Type4 :
1422 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1423 IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ ->
1425 let remainder_ok_inv_rect_Type4 x1 x2 x3 hterm h1 =
1426 let hcut = remainder_ok_rect_Type4 x1 x2 x3 h1 hterm in hcut __
1428 (** val remainder_ok_inv_rect_Type3 :
1429 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1430 IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ ->
1432 let remainder_ok_inv_rect_Type3 x1 x2 x3 hterm h1 =
1433 let hcut = remainder_ok_rect_Type3 x1 x2 x3 h1 hterm in hcut __
1435 (** val remainder_ok_inv_rect_Type2 :
1436 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1437 IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ ->
1439 let remainder_ok_inv_rect_Type2 x1 x2 x3 hterm h1 =
1440 let hcut = remainder_ok_rect_Type2 x1 x2 x3 h1 hterm in hcut __
1442 (** val remainder_ok_inv_rect_Type1 :
1443 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1444 IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ ->
1446 let remainder_ok_inv_rect_Type1 x1 x2 x3 hterm h1 =
1447 let hcut = remainder_ok_rect_Type1 x1 x2 x3 h1 hterm in hcut __
1449 (** val remainder_ok_inv_rect_Type0 :
1450 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1451 IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ ->
1453 let remainder_ok_inv_rect_Type0 x1 x2 x3 hterm h1 =
1454 let hcut = remainder_ok_rect_Type0 x1 x2 x3 h1 hterm in hcut __
1456 (** val remainder_ok_discr :
1457 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1458 IO.io_in) flat_trace -> remainder_ok -> remainder_ok -> __ **)
1459 let remainder_ok_discr a1 a2 a3 x y =
1460 Logic.eq_rect_Type2 x
1461 (let Mk_remainder_ok = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
1463 (** val remainder_ok_jmdiscr :
1464 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
1465 IO.io_in) flat_trace -> remainder_ok -> remainder_ok -> __ **)
1466 let remainder_ok_jmdiscr a1 a2 a3 x y =
1467 Logic.eq_rect_Type2 x
1468 (let Mk_remainder_ok = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
1470 (** val init_state_is :
1471 RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state ->
1472 (Pointers.block, __) Types.dPair **)
1473 let init_state_is p s =
1474 RTLabs_semantics.bind_ok (Globalenvs.init_mem (fun x -> x) p) (fun x ->
1475 let main = p.AST.prog_main in
1477 (Monad.m_bind0 (Monad.max_def Errors.res0)
1479 (Errors.opt_to_res (List.Cons ((Errors.MSG
1480 ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
1481 (PreIdentifiers.SymbolTag, main)), List.Nil))))
1482 (Globalenvs.find_symbol (RTLabs_semantics.make_global p) main)))
1484 Monad.m_bind0 (Monad.max_def Errors.res0)
1486 (Errors.opt_to_res (List.Cons ((Errors.MSG
1487 ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
1488 (PreIdentifiers.SymbolTag, main)), List.Nil))))
1489 (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global p) b)))
1491 Obj.magic (Errors.OK (RTLabs_semantics.Callstate (main, f,
1492 List.Nil, Types.None, List.Nil, x))))))) s (fun m _ _ ->
1493 RTLabs_semantics.bind_ok
1494 (Errors.opt_to_res (List.Cons ((Errors.MSG
1495 ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
1496 (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil))))
1497 (Globalenvs.find_symbol (RTLabs_semantics.make_global p)
1498 p.AST.prog_main)) (fun x ->
1500 (Monad.m_bind0 (Monad.max_def Errors.res0)
1502 (Errors.opt_to_res (List.Cons ((Errors.MSG
1503 ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
1504 (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil))))
1505 (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global p) x)))
1507 Obj.magic (Errors.OK (RTLabs_semantics.Callstate (p.AST.prog_main,
1508 f, List.Nil, Types.None, List.Nil, m)))))) s (fun b _ _ ->
1509 RTLabs_semantics.bind_ok
1510 (Errors.opt_to_res (List.Cons ((Errors.MSG
1511 ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
1512 (PreIdentifiers.SymbolTag, p.AST.prog_main)), List.Nil))))
1513 (Globalenvs.find_funct_ptr (RTLabs_semantics.make_global p) b))
1514 (fun x -> Errors.OK (RTLabs_semantics.Callstate (p.AST.prog_main, x,
1515 List.Nil, Types.None, List.Nil, m))) s (fun f _ _ ->
1516 Obj.magic Errors.res_discr (Errors.OK (RTLabs_semantics.Callstate
1517 (p.AST.prog_main, f, List.Nil, Types.None, List.Nil, m)))
1518 (Errors.OK s) __ (fun _ ->
1519 Logic.eq_rect_Type0 (RTLabs_semantics.Callstate (p.AST.prog_main,
1520 f, List.Nil, Types.None, List.Nil, m)) (fun _ ->
1521 Logic.streicherK (Errors.OK (RTLabs_semantics.Callstate
1522 (p.AST.prog_main, f, List.Nil, Types.None, List.Nil, m)))
1523 { Types.dpi1 = b; Types.dpi2 = __ }) s __))))
1525 (** val ras_state_initial :
1526 RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state ->
1527 RTLabs_abstract.rTLabs_ext_state **)
1528 let ras_state_initial p s =
1529 { RTLabs_abstract.ras_state = s; RTLabs_abstract.ras_fn_stack = (List.Cons
1530 ((init_state_is p s).Types.dpi1, List.Nil)) }
1532 (** val deprop_execute :
1533 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1534 -> Events.trace Types.sig0 **)
1535 let rec deprop_execute ge s s' =
1536 (match RTLabs_semantics.eval_statement ge s with
1537 | IOMonad.Interact (x, x0) -> (fun _ -> assert false (* absurd case *))
1538 | IOMonad.Value ts -> (fun _ -> ts.Types.fst)
1539 | IOMonad.Wrong x -> (fun _ -> assert false (* absurd case *))) __
1541 (** val deprop_as_execute :
1542 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1543 RTLabs_abstract.rTLabs_ext_state -> Events.trace Types.sig0 **)
1544 let rec deprop_as_execute ge s s' =
1545 deprop_execute ge s.RTLabs_abstract.ras_state s'.RTLabs_abstract.ras_state
1547 type ('o, 'i) partial_flat_trace =
1548 | Pft_base of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
1549 | Pft_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
1550 * RTLabs_semantics.state * ('o, 'i) partial_flat_trace
1552 (** val partial_flat_trace_rect_Type4 :
1553 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
1554 RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
1555 Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
1556 ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
1557 RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
1558 let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_2393 x_2392 = function
1559 | Pft_base (s, tr, s') -> h_pft_base s tr s' __
1560 | Pft_step (s, tr, s', s'', x_2396) ->
1561 h_pft_step s tr s' s'' __ x_2396
1562 (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_2396)
1564 (** val partial_flat_trace_rect_Type3 :
1565 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
1566 RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
1567 Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
1568 ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
1569 RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
1570 let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_2409 x_2408 = function
1571 | Pft_base (s, tr, s') -> h_pft_base s tr s' __
1572 | Pft_step (s, tr, s', s'', x_2412) ->
1573 h_pft_step s tr s' s'' __ x_2412
1574 (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_2412)
1576 (** val partial_flat_trace_rect_Type2 :
1577 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
1578 RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
1579 Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
1580 ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
1581 RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
1582 let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_2417 x_2416 = function
1583 | Pft_base (s, tr, s') -> h_pft_base s tr s' __
1584 | Pft_step (s, tr, s', s'', x_2420) ->
1585 h_pft_step s tr s' s'' __ x_2420
1586 (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_2420)
1588 (** val partial_flat_trace_rect_Type1 :
1589 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
1590 RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
1591 Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
1592 ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
1593 RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
1594 let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_2425 x_2424 = function
1595 | Pft_base (s, tr, s') -> h_pft_base s tr s' __
1596 | Pft_step (s, tr, s', s'', x_2428) ->
1597 h_pft_step s tr s' s'' __ x_2428
1598 (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_2428)
1600 (** val partial_flat_trace_rect_Type0 :
1601 RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
1602 RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
1603 Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
1604 ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
1605 RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
1606 let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_2433 x_2432 = function
1607 | Pft_base (s, tr, s') -> h_pft_base s tr s' __
1608 | Pft_step (s, tr, s', s'', x_2436) ->
1609 h_pft_step s tr s' s'' __ x_2436
1610 (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_2436)
1612 (** val partial_flat_trace_inv_rect_Type4 :
1613 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1614 -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
1615 Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
1616 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
1617 RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
1618 __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
1619 let partial_flat_trace_inv_rect_Type4 x3 x4 x5 hterm h1 h2 =
1620 let hcut = partial_flat_trace_rect_Type4 x3 h1 h2 x4 x5 hterm in
1623 (** val partial_flat_trace_inv_rect_Type3 :
1624 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1625 -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
1626 Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
1627 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
1628 RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
1629 __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
1630 let partial_flat_trace_inv_rect_Type3 x3 x4 x5 hterm h1 h2 =
1631 let hcut = partial_flat_trace_rect_Type3 x3 h1 h2 x4 x5 hterm in
1634 (** val partial_flat_trace_inv_rect_Type2 :
1635 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1636 -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
1637 Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
1638 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
1639 RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
1640 __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
1641 let partial_flat_trace_inv_rect_Type2 x3 x4 x5 hterm h1 h2 =
1642 let hcut = partial_flat_trace_rect_Type2 x3 h1 h2 x4 x5 hterm in
1645 (** val partial_flat_trace_inv_rect_Type1 :
1646 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1647 -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
1648 Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
1649 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
1650 RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
1651 __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
1652 let partial_flat_trace_inv_rect_Type1 x3 x4 x5 hterm h1 h2 =
1653 let hcut = partial_flat_trace_rect_Type1 x3 h1 h2 x4 x5 hterm in
1656 (** val partial_flat_trace_inv_rect_Type0 :
1657 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1658 -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state ->
1659 Events.trace -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
1660 (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
1661 RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ ->
1662 __ -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3 **)
1663 let partial_flat_trace_inv_rect_Type0 x3 x4 x5 hterm h1 h2 =
1664 let hcut = partial_flat_trace_rect_Type0 x3 h1 h2 x4 x5 hterm in
1667 (** val partial_flat_trace_jmdiscr :
1668 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1669 -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) partial_flat_trace -> __ **)
1670 let partial_flat_trace_jmdiscr a3 a4 a5 x y =
1671 Logic.eq_rect_Type2 x
1673 | Pft_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1674 | Pft_step (a0, a10, a20, a30, a50) ->
1675 Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
1677 (** val append_partial_flat_trace :
1678 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1679 -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2)
1680 partial_flat_trace -> ('a1, 'a2) partial_flat_trace **)
1681 let rec append_partial_flat_trace ge s1 s2 s3 = function
1682 | Pft_base (s, tr, s') -> (fun x -> Pft_step (s, tr, s', s3, x))
1683 | Pft_step (s, tr, s', s'', tr') ->
1684 (fun tr2 -> Pft_step (s, tr, s', s3,
1685 (append_partial_flat_trace ge s' s'' s3 tr' tr2)))
1687 (** val partial_to_flat_trace :
1688 RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
1689 -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) flat_trace -> ('a1, 'a2)
1691 let rec partial_to_flat_trace ge s1 s2 = function
1692 | Pft_base (s, tr0, s') -> (fun x -> lazy (Ft_step (s, tr0, s', x)))
1693 | Pft_step (s, tr0, s', s'', tr') ->
1694 (fun tr'' -> lazy (Ft_step (s, tr0, s',
1695 (partial_to_flat_trace ge s' s'' tr' tr''))))
1697 (** val flat_trace_of_label_return :
1698 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1699 RTLabs_abstract.rTLabs_ext_state -> StructuredTraces.trace_label_return
1700 -> (IO.io_out, IO.io_in) partial_flat_trace **)
1701 let rec flat_trace_of_label_return ge s s' = function
1702 | StructuredTraces.Tlr_base (s1, s2, tll) ->
1703 flat_trace_of_label_label ge StructuredTraces.Ends_with_ret (Obj.magic s1)
1705 | StructuredTraces.Tlr_step (s1, s2, s3, tll, tlr) ->
1706 append_partial_flat_trace ge (Obj.magic s1).RTLabs_abstract.ras_state
1707 (Obj.magic s2).RTLabs_abstract.ras_state
1708 (Obj.magic s3).RTLabs_abstract.ras_state
1709 (flat_trace_of_label_label ge StructuredTraces.Doesnt_end_with_ret
1710 (Obj.magic s1) (Obj.magic s2) tll)
1711 (flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic s3) tlr)
1712 (** val flat_trace_of_label_label :
1713 RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
1714 RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
1715 StructuredTraces.trace_label_label -> (IO.io_out, IO.io_in)
1716 partial_flat_trace **)
1717 and flat_trace_of_label_label ge ends0 s s' = function
1718 | StructuredTraces.Tll_base (e, s1, s2, tal) ->
1719 flat_trace_of_any_label ge e (Obj.magic s1) (Obj.magic s2) tal
1720 (** val flat_trace_of_any_label :
1721 RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
1722 RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
1723 StructuredTraces.trace_any_label -> (IO.io_out, IO.io_in)
1724 partial_flat_trace **)
1725 and flat_trace_of_any_label ge ends0 s s' = function
1726 | StructuredTraces.Tal_base_not_return (s1, s2) ->
1727 let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1728 Pft_base ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1729 (Obj.magic s2).RTLabs_abstract.ras_state)
1730 | StructuredTraces.Tal_base_return (s1, s2) ->
1731 let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1732 Pft_base ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1733 (Obj.magic s2).RTLabs_abstract.ras_state)
1734 | StructuredTraces.Tal_base_call (s1, s2, s3, tlr) ->
1736 flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic s3) tlr
1738 let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1739 Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1740 (Obj.magic s2).RTLabs_abstract.ras_state,
1741 (Obj.magic s3).RTLabs_abstract.ras_state, suffix')
1742 | StructuredTraces.Tal_base_tailcall (s1, s2, s3, tlr) ->
1743 assert false (* absurd case *)
1744 | StructuredTraces.Tal_step_call (ends1, s1, s2, s3, s4, tlr, tal) ->
1745 let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1746 Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1747 (Obj.magic s2).RTLabs_abstract.ras_state,
1748 (Obj.magic s4).RTLabs_abstract.ras_state,
1749 (append_partial_flat_trace ge (Obj.magic s2).RTLabs_abstract.ras_state
1750 (Obj.magic s3).RTLabs_abstract.ras_state
1751 (Obj.magic s4).RTLabs_abstract.ras_state
1752 (flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic s3) tlr)
1753 (flat_trace_of_any_label ge ends1 (Obj.magic s3) (Obj.magic s4) tal)))
1754 | StructuredTraces.Tal_step_default (ends1, s1, s2, s3, tal) ->
1755 let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1756 Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1757 (Obj.magic s2).RTLabs_abstract.ras_state,
1758 (Obj.magic s3).RTLabs_abstract.ras_state,
1759 (flat_trace_of_any_label ge ends1 (Obj.magic s2) (Obj.magic s3) tal))
1761 (** val flat_trace_of_any_call :
1762 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1763 RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
1764 Events.trace -> StructuredTraces.trace_any_call -> (IO.io_out, IO.io_in)
1765 partial_flat_trace **)
1766 let rec flat_trace_of_any_call ge s s' s'' et tr =
1768 | StructuredTraces.Tac_base s1 ->
1769 (fun _ -> Pft_base ((Obj.magic s1).RTLabs_abstract.ras_state, et,
1770 s''.RTLabs_abstract.ras_state))
1771 | StructuredTraces.Tac_step_call (s1, s2, s3, s4, tlr, tac) ->
1773 let et0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s4) in
1774 Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, et0,
1775 (Obj.magic s4).RTLabs_abstract.ras_state,
1776 s''.RTLabs_abstract.ras_state,
1777 (append_partial_flat_trace ge (Obj.magic s4).RTLabs_abstract.ras_state
1778 (Obj.magic s2).RTLabs_abstract.ras_state
1779 s''.RTLabs_abstract.ras_state
1780 (flat_trace_of_label_return ge (Obj.magic s4) (Obj.magic s2) tlr)
1781 (flat_trace_of_any_call ge (Obj.magic s2) (Obj.magic s3) s'' et tac))))
1782 | StructuredTraces.Tac_step_default (s1, s2, s3, tal) ->
1784 let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s3) in
1785 Pft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1786 (Obj.magic s3).RTLabs_abstract.ras_state,
1787 s''.RTLabs_abstract.ras_state,
1788 (flat_trace_of_any_call ge (Obj.magic s3) (Obj.magic s2) s'' et tal))))
1791 (** val flat_trace_of_label_call :
1792 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1793 RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
1794 Events.trace -> StructuredTraces.trace_label_call -> (IO.io_out,
1795 IO.io_in) partial_flat_trace **)
1796 let rec flat_trace_of_label_call ge s s' s'' et tr =
1797 (let StructuredTraces.Tlc_base (s1, s2, tac) = tr in
1799 flat_trace_of_any_call ge (Obj.magic s1) (Obj.magic s2) s'' et tac)) __
1801 (** val flat_trace_of_label_diverges :
1802 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1803 StructuredTraces.trace_label_diverges -> (IO.io_out, IO.io_in) flat_trace **)
1804 let rec flat_trace_of_label_diverges ge s tr =
1807 | StructuredTraces.Tld_step (sx, sy, tll, tld) ->
1808 (let { RTLabs_abstract.ras_state = sy'; RTLabs_abstract.ras_fn_stack =
1809 stk } = Obj.magic sy
1812 (match flat_trace_of_label_label ge StructuredTraces.Doesnt_end_with_ret
1813 (Obj.magic sx) { RTLabs_abstract.ras_state = sy';
1814 RTLabs_abstract.ras_fn_stack = stk } tll0 with
1815 | Pft_base (s1, tr0, s2) ->
1816 (fun _ tld0 -> lazy (Ft_step (s1, tr0, s2,
1817 (flat_trace_of_label_diverges ge { RTLabs_abstract.ras_state = s2;
1818 RTLabs_abstract.ras_fn_stack = stk } tld0))))
1819 | Pft_step (s1, et, s2, s3, tr') ->
1820 (fun _ tld0 -> lazy (Ft_step (s1, et, s2,
1821 (add_partial_flat_trace ge s2 { RTLabs_abstract.ras_state = s3;
1822 RTLabs_abstract.ras_fn_stack = stk } tr' tld0))))) __)) tll tld
1823 | StructuredTraces.Tld_base (s1, s2, s3, tlc, tld) ->
1824 (let { RTLabs_abstract.ras_state = s3'; RTLabs_abstract.ras_fn_stack =
1825 stk } = Obj.magic s3
1829 deprop_as_execute ge (Obj.magic s2) { RTLabs_abstract.ras_state = s3';
1830 RTLabs_abstract.ras_fn_stack = stk }
1832 (match flat_trace_of_label_call ge (Obj.magic s1) (Obj.magic s2)
1833 { RTLabs_abstract.ras_state = s3';
1834 RTLabs_abstract.ras_fn_stack = stk } tr0 tlc with
1835 | Pft_base (s10, tr1, s20) ->
1836 (fun _ tld0 -> lazy (Ft_step (s10, tr1, s20,
1837 (flat_trace_of_label_diverges ge { RTLabs_abstract.ras_state = s20;
1838 RTLabs_abstract.ras_fn_stack = stk } tld0))))
1839 | Pft_step (s10, et, s20, s30, tr') ->
1840 (fun _ tld0 -> lazy (Ft_step (s10, et, s20,
1841 (add_partial_flat_trace ge s20 { RTLabs_abstract.ras_state = s30;
1842 RTLabs_abstract.ras_fn_stack = stk } tr' tld0))))) __)) __ tld
1843 (** val add_partial_flat_trace :
1844 RTLabs_semantics.genv -> RTLabs_semantics.state ->
1845 RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in)
1846 partial_flat_trace -> StructuredTraces.trace_label_diverges ->
1847 (IO.io_out, IO.io_in) flat_trace **)
1848 and add_partial_flat_trace ge s s' =
1849 let { RTLabs_abstract.ras_state = sx; RTLabs_abstract.ras_fn_stack =
1854 | Pft_base (s0, tr, s'0) ->
1855 (fun _ tr0 -> lazy (Ft_step (s0, tr, s'0,
1856 (flat_trace_of_label_diverges ge { RTLabs_abstract.ras_state = s'0;
1857 RTLabs_abstract.ras_fn_stack = stk } tr0))))
1858 | Pft_step (s1, et, s2, s3, tr') ->
1859 (fun _ tr -> lazy (Ft_step (s1, et, s2,
1860 (add_partial_flat_trace ge s2 { RTLabs_abstract.ras_state = s3;
1861 RTLabs_abstract.ras_fn_stack = stk } tr' tr))))) __)
1863 (** val flat_trace_of_whole_program :
1864 RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
1865 StructuredTraces.trace_whole_program -> (IO.io_out, IO.io_in) flat_trace **)
1866 let rec flat_trace_of_whole_program ge s = function
1867 | StructuredTraces.Twp_terminating (s1, s2, sf, tlr) ->
1868 let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1869 lazy (Ft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1870 (Obj.magic s2).RTLabs_abstract.ras_state,
1871 (partial_to_flat_trace ge (Obj.magic s2).RTLabs_abstract.ras_state
1872 (Obj.magic sf).RTLabs_abstract.ras_state
1873 (flat_trace_of_label_return ge (Obj.magic s2) (Obj.magic sf) tlr)
1874 (lazy (Ft_stop (Obj.magic sf).RTLabs_abstract.ras_state)))))
1875 | StructuredTraces.Twp_diverges (s1, s2, tld) ->
1876 let tr0 = deprop_as_execute ge (Obj.magic s1) (Obj.magic s2) in
1877 lazy (Ft_step ((Obj.magic s1).RTLabs_abstract.ras_state, tr0,
1878 (Obj.magic s2).RTLabs_abstract.ras_state,
1879 (flat_trace_of_label_diverges ge (Obj.magic s2) tld)))
1882 RTLabs_semantics.genv -> __ -> Pointers.block Types.option **)
1884 match (Obj.magic s).RTLabs_abstract.ras_fn_stack with
1885 | List.Nil -> Types.None
1886 | List.Cons (h, t) ->
1887 (match (Obj.magic s).RTLabs_abstract.ras_state with
1888 | RTLabs_semantics.State (x, x0, x1) -> Types.Some h
1889 | RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) ->
1891 | List.Nil -> Types.None
1892 | List.Cons (h', x5) -> Types.Some h')
1893 | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Types.Some h
1894 | RTLabs_semantics.Finalstate x -> Types.Some h)
1896 (** val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __ **)
1897 let option_jmdiscr x y =
1898 Logic.eq_rect_Type2 x
1900 | Types.None -> Obj.magic (fun _ dH -> dH)
1901 | Types.Some a0 -> Obj.magic (fun _ dH -> dH __)) y