103 val call_ud_rect_Type4 :
104 (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1
106 val call_ud_rect_Type5 :
107 (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1
109 val call_ud_rect_Type3 :
110 (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1
112 val call_ud_rect_Type2 :
113 (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1
115 val call_ud_rect_Type1 :
116 (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1
118 val call_ud_rect_Type0 :
119 (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1
121 val call_ud_inv_rect_Type4 :
122 call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
124 val call_ud_inv_rect_Type3 :
125 call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
127 val call_ud_inv_rect_Type2 :
128 call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
130 val call_ud_inv_rect_Type1 :
131 call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
133 val call_ud_inv_rect_Type0 :
134 call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
136 val call_ud_discr : call_ud -> call_ud -> __
138 val call_ud_jmdiscr : call_ud -> call_ud -> __
140 type stacksize_info = { current : Nat.nat; maximum : Nat.nat }
142 val stacksize_info_rect_Type4 :
143 (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1
145 val stacksize_info_rect_Type5 :
146 (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1
148 val stacksize_info_rect_Type3 :
149 (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1
151 val stacksize_info_rect_Type2 :
152 (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1
154 val stacksize_info_rect_Type1 :
155 (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1
157 val stacksize_info_rect_Type0 :
158 (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1
160 val current : stacksize_info -> Nat.nat
162 val maximum : stacksize_info -> Nat.nat
164 val stacksize_info_inv_rect_Type4 :
165 stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1
167 val stacksize_info_inv_rect_Type3 :
168 stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1
170 val stacksize_info_inv_rect_Type2 :
171 stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1
173 val stacksize_info_inv_rect_Type1 :
174 stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1
176 val stacksize_info_inv_rect_Type0 :
177 stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1
179 val stacksize_info_discr : stacksize_info -> stacksize_info -> __
181 val stacksize_info_jmdiscr : stacksize_info -> stacksize_info -> __
183 val update_stacksize_info :
184 (AST.ident -> Nat.nat Types.option) -> stacksize_info -> call_ud List.list
187 val extract_call_ud_from_observables :
188 StructuredTraces.intensional_event List.list -> call_ud List.list
190 val extract_call_ud_from_tlr :
191 StructuredTraces.abstract_status -> __ -> __ ->
192 StructuredTraces.trace_label_return -> AST.ident -> call_ud List.list
194 val extract_call_ud_from_tll :
195 StructuredTraces.trace_ends_with_ret -> StructuredTraces.abstract_status ->
196 __ -> __ -> StructuredTraces.trace_label_label -> AST.ident -> call_ud