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

val call_ud_rect_Type5 :
  (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1

val call_ud_rect_Type3 :
  (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1

val call_ud_rect_Type2 :
  (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1

val call_ud_rect_Type1 :
  (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1

val call_ud_rect_Type0 :
  (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1

val call_ud_inv_rect_Type4 :
  call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1

val call_ud_inv_rect_Type3 :
  call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1

val call_ud_inv_rect_Type2 :
  call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1

val call_ud_inv_rect_Type1 :
  call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1

val call_ud_inv_rect_Type0 :
  call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1

val call_ud_discr : call_ud -> call_ud -> __

val call_ud_jmdiscr : call_ud -> call_ud -> __

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

val stacksize_info_rect_Type4 :
  (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1

val stacksize_info_rect_Type5 :
  (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1

val stacksize_info_rect_Type3 :
  (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1

val stacksize_info_rect_Type2 :
  (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1

val stacksize_info_rect_Type1 :
  (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1

val stacksize_info_rect_Type0 :
  (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1

val current : stacksize_info -> Nat.nat

val maximum : stacksize_info -> Nat.nat

val stacksize_info_inv_rect_Type4 :
  stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1

val stacksize_info_inv_rect_Type3 :
  stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1

val stacksize_info_inv_rect_Type2 :
  stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1

val stacksize_info_inv_rect_Type1 :
  stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1

val stacksize_info_inv_rect_Type0 :
  stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1

val stacksize_info_discr : stacksize_info -> stacksize_info -> __

val stacksize_info_jmdiscr : stacksize_info -> stacksize_info -> __

val update_stacksize_info :
  (AST.ident -> Nat.nat Types.option) -> stacksize_info -> call_ud List.list
  -> stacksize_info

val extract_call_ud_from_observables :
  StructuredTraces.intensional_event List.list -> call_ud List.list

val extract_call_ud_from_tlr :
  StructuredTraces.abstract_status -> __ -> __ ->
  StructuredTraces.trace_label_return -> AST.ident -> call_ud List.list

val extract_call_ud_from_tll :
  StructuredTraces.trace_ends_with_ret -> StructuredTraces.abstract_status ->
  __ -> __ -> StructuredTraces.trace_label_label -> AST.ident -> call_ud
  List.list