open Preamble

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open Hide

open Integers

open AST

open Division

open Exp

open Arithmetic

open Extranat

open Vector

open FoldStuff

open BitVector

open Z

open BitVectorZ

open Pointers

open Coqlib

open Values

open Events

open IOMonad

open IO

open Sets

open Listb

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Setoids

open Monad

open Option

open Div_and_mod

open Russell

open Util

open Lists

open Positive

open Identifiers

open CostLabel

open Jmeq

open StructuredTraces

type call_ud =
| Up of AST.ident
| Down of AST.ident

(** val call_ud_rect_Type4 :
    (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
let rec call_ud_rect_Type4 h_up h_down = function
| Up x_23575 -> h_up x_23575
| Down x_23576 -> h_down x_23576

(** val call_ud_rect_Type5 :
    (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
let rec call_ud_rect_Type5 h_up h_down = function
| Up x_23580 -> h_up x_23580
| Down x_23581 -> h_down x_23581

(** val call_ud_rect_Type3 :
    (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
let rec call_ud_rect_Type3 h_up h_down = function
| Up x_23585 -> h_up x_23585
| Down x_23586 -> h_down x_23586

(** val call_ud_rect_Type2 :
    (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
let rec call_ud_rect_Type2 h_up h_down = function
| Up x_23590 -> h_up x_23590
| Down x_23591 -> h_down x_23591

(** val call_ud_rect_Type1 :
    (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
let rec call_ud_rect_Type1 h_up h_down = function
| Up x_23595 -> h_up x_23595
| Down x_23596 -> h_down x_23596

(** val call_ud_rect_Type0 :
    (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
let rec call_ud_rect_Type0 h_up h_down = function
| Up x_23600 -> h_up x_23600
| Down x_23601 -> h_down x_23601

(** val call_ud_inv_rect_Type4 :
    call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
let call_ud_inv_rect_Type4 hterm h1 h2 =
  let hcut = call_ud_rect_Type4 h1 h2 hterm in hcut __

(** val call_ud_inv_rect_Type3 :
    call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
let call_ud_inv_rect_Type3 hterm h1 h2 =
  let hcut = call_ud_rect_Type3 h1 h2 hterm in hcut __

(** val call_ud_inv_rect_Type2 :
    call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
let call_ud_inv_rect_Type2 hterm h1 h2 =
  let hcut = call_ud_rect_Type2 h1 h2 hterm in hcut __

(** val call_ud_inv_rect_Type1 :
    call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
let call_ud_inv_rect_Type1 hterm h1 h2 =
  let hcut = call_ud_rect_Type1 h1 h2 hterm in hcut __

(** val call_ud_inv_rect_Type0 :
    call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
let call_ud_inv_rect_Type0 hterm h1 h2 =
  let hcut = call_ud_rect_Type0 h1 h2 hterm in hcut __

(** val call_ud_discr : call_ud -> call_ud -> __ **)
let call_ud_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Up a0 -> Obj.magic (fun _ dH -> dH __)
     | Down a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val call_ud_jmdiscr : call_ud -> call_ud -> __ **)
let call_ud_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Up a0 -> Obj.magic (fun _ dH -> dH __)
     | Down a0 -> Obj.magic (fun _ dH -> dH __)) y

type stacksize_info = { current : Nat.nat; maximum : Nat.nat }

(** val stacksize_info_rect_Type4 :
    (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
let rec stacksize_info_rect_Type4 h_mk_stacksize_info x_23636 =
  let { current = current0; maximum = maximum0 } = x_23636 in
  h_mk_stacksize_info current0 maximum0

(** val stacksize_info_rect_Type5 :
    (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
let rec stacksize_info_rect_Type5 h_mk_stacksize_info x_23638 =
  let { current = current0; maximum = maximum0 } = x_23638 in
  h_mk_stacksize_info current0 maximum0

(** val stacksize_info_rect_Type3 :
    (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
let rec stacksize_info_rect_Type3 h_mk_stacksize_info x_23640 =
  let { current = current0; maximum = maximum0 } = x_23640 in
  h_mk_stacksize_info current0 maximum0

(** val stacksize_info_rect_Type2 :
    (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
let rec stacksize_info_rect_Type2 h_mk_stacksize_info x_23642 =
  let { current = current0; maximum = maximum0 } = x_23642 in
  h_mk_stacksize_info current0 maximum0

(** val stacksize_info_rect_Type1 :
    (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
let rec stacksize_info_rect_Type1 h_mk_stacksize_info x_23644 =
  let { current = current0; maximum = maximum0 } = x_23644 in
  h_mk_stacksize_info current0 maximum0

(** val stacksize_info_rect_Type0 :
    (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
let rec stacksize_info_rect_Type0 h_mk_stacksize_info x_23646 =
  let { current = current0; maximum = maximum0 } = x_23646 in
  h_mk_stacksize_info current0 maximum0

(** val current : stacksize_info -> Nat.nat **)
let rec current xxx =
  xxx.current

(** val maximum : stacksize_info -> Nat.nat **)
let rec maximum xxx =
  xxx.maximum

(** val stacksize_info_inv_rect_Type4 :
    stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1 **)
let stacksize_info_inv_rect_Type4 hterm h1 =
  let hcut = stacksize_info_rect_Type4 h1 hterm in hcut __

(** val stacksize_info_inv_rect_Type3 :
    stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1 **)
let stacksize_info_inv_rect_Type3 hterm h1 =
  let hcut = stacksize_info_rect_Type3 h1 hterm in hcut __

(** val stacksize_info_inv_rect_Type2 :
    stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1 **)
let stacksize_info_inv_rect_Type2 hterm h1 =
  let hcut = stacksize_info_rect_Type2 h1 hterm in hcut __

(** val stacksize_info_inv_rect_Type1 :
    stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1 **)
let stacksize_info_inv_rect_Type1 hterm h1 =
  let hcut = stacksize_info_rect_Type1 h1 hterm in hcut __

(** val stacksize_info_inv_rect_Type0 :
    stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1 **)
let stacksize_info_inv_rect_Type0 hterm h1 =
  let hcut = stacksize_info_rect_Type0 h1 hterm in hcut __

(** val stacksize_info_discr : stacksize_info -> stacksize_info -> __ **)
let stacksize_info_discr x y =
  Logic.eq_rect_Type2 x
    (let { current = a0; maximum = a1 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val stacksize_info_jmdiscr : stacksize_info -> stacksize_info -> __ **)
let stacksize_info_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { current = a0; maximum = a1 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val update_stacksize_info :
    (AST.ident -> Nat.nat Types.option) -> stacksize_info -> call_ud
    List.list -> stacksize_info **)
let update_stacksize_info stacksizes =
  let get_stacksize = fun f ->
    match stacksizes f with
    | Types.None -> Nat.O
    | Types.Some n -> n
  in
  let f = fun ud acc ->
    match ud with
    | Up i ->
      let new_stack = Nat.plus (get_stacksize i) acc.current in
      let new_max = Nat.max acc.maximum new_stack in
      { current = new_stack; maximum = new_max }
    | Down i ->
      let new_stack = Nat.minus acc.current (get_stacksize i) in
      { current = new_stack; maximum = acc.maximum }
  in
  List.foldr f

(** val extract_call_ud_from_observables :
    StructuredTraces.intensional_event List.list -> call_ud List.list **)
let extract_call_ud_from_observables =
  let f = fun ev ->
    match ev with
    | StructuredTraces.IEVcost x -> List.Nil
    | StructuredTraces.IEVcall i -> List.Cons ((Up i), List.Nil)
    | StructuredTraces.IEVtailcall (i, j) ->
      List.Cons ((Down i), (List.Cons ((Up j), List.Nil)))
    | StructuredTraces.IEVret i -> List.Cons ((Down i), List.Nil)
  in
  List.foldr (fun ev -> List.append (f ev)) List.Nil

(** val extract_call_ud_from_tlr :
    StructuredTraces.abstract_status -> __ -> __ ->
    StructuredTraces.trace_label_return -> AST.ident -> call_ud List.list **)
let extract_call_ud_from_tlr s st1 st2 tlr curr =
  extract_call_ud_from_observables
    (Types.pi1
      (StructuredTraces.observables_trace_label_return s st1 st2 tlr curr))

(** val extract_call_ud_from_tll :
    StructuredTraces.trace_ends_with_ret -> StructuredTraces.abstract_status
    -> __ -> __ -> StructuredTraces.trace_label_label -> AST.ident -> call_ud
    List.list **)
let extract_call_ud_from_tll s fl st1 st2 tll curr =
  extract_call_ud_from_observables
    (Types.pi1
      (StructuredTraces.observables_trace_label_label fl s st1 st2 tll curr))