103 (** val call_ud_rect_Type4 :
104 (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
105 let rec call_ud_rect_Type4 h_up h_down = function
106 | Up x_23575 -> h_up x_23575
107 | Down x_23576 -> h_down x_23576
109 (** val call_ud_rect_Type5 :
110 (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
111 let rec call_ud_rect_Type5 h_up h_down = function
112 | Up x_23580 -> h_up x_23580
113 | Down x_23581 -> h_down x_23581
115 (** val call_ud_rect_Type3 :
116 (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
117 let rec call_ud_rect_Type3 h_up h_down = function
118 | Up x_23585 -> h_up x_23585
119 | Down x_23586 -> h_down x_23586
121 (** val call_ud_rect_Type2 :
122 (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
123 let rec call_ud_rect_Type2 h_up h_down = function
124 | Up x_23590 -> h_up x_23590
125 | Down x_23591 -> h_down x_23591
127 (** val call_ud_rect_Type1 :
128 (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
129 let rec call_ud_rect_Type1 h_up h_down = function
130 | Up x_23595 -> h_up x_23595
131 | Down x_23596 -> h_down x_23596
133 (** val call_ud_rect_Type0 :
134 (AST.ident -> 'a1) -> (AST.ident -> 'a1) -> call_ud -> 'a1 **)
135 let rec call_ud_rect_Type0 h_up h_down = function
136 | Up x_23600 -> h_up x_23600
137 | Down x_23601 -> h_down x_23601
139 (** val call_ud_inv_rect_Type4 :
140 call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
141 let call_ud_inv_rect_Type4 hterm h1 h2 =
142 let hcut = call_ud_rect_Type4 h1 h2 hterm in hcut __
144 (** val call_ud_inv_rect_Type3 :
145 call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
146 let call_ud_inv_rect_Type3 hterm h1 h2 =
147 let hcut = call_ud_rect_Type3 h1 h2 hterm in hcut __
149 (** val call_ud_inv_rect_Type2 :
150 call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
151 let call_ud_inv_rect_Type2 hterm h1 h2 =
152 let hcut = call_ud_rect_Type2 h1 h2 hterm in hcut __
154 (** val call_ud_inv_rect_Type1 :
155 call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
156 let call_ud_inv_rect_Type1 hterm h1 h2 =
157 let hcut = call_ud_rect_Type1 h1 h2 hterm in hcut __
159 (** val call_ud_inv_rect_Type0 :
160 call_ud -> (AST.ident -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1 **)
161 let call_ud_inv_rect_Type0 hterm h1 h2 =
162 let hcut = call_ud_rect_Type0 h1 h2 hterm in hcut __
164 (** val call_ud_discr : call_ud -> call_ud -> __ **)
165 let call_ud_discr x y =
166 Logic.eq_rect_Type2 x
168 | Up a0 -> Obj.magic (fun _ dH -> dH __)
169 | Down a0 -> Obj.magic (fun _ dH -> dH __)) y
171 (** val call_ud_jmdiscr : call_ud -> call_ud -> __ **)
172 let call_ud_jmdiscr x y =
173 Logic.eq_rect_Type2 x
175 | Up a0 -> Obj.magic (fun _ dH -> dH __)
176 | Down a0 -> Obj.magic (fun _ dH -> dH __)) y
178 type stacksize_info = { current : Nat.nat; maximum : Nat.nat }
180 (** val stacksize_info_rect_Type4 :
181 (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
182 let rec stacksize_info_rect_Type4 h_mk_stacksize_info x_23636 =
183 let { current = current0; maximum = maximum0 } = x_23636 in
184 h_mk_stacksize_info current0 maximum0
186 (** val stacksize_info_rect_Type5 :
187 (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
188 let rec stacksize_info_rect_Type5 h_mk_stacksize_info x_23638 =
189 let { current = current0; maximum = maximum0 } = x_23638 in
190 h_mk_stacksize_info current0 maximum0
192 (** val stacksize_info_rect_Type3 :
193 (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
194 let rec stacksize_info_rect_Type3 h_mk_stacksize_info x_23640 =
195 let { current = current0; maximum = maximum0 } = x_23640 in
196 h_mk_stacksize_info current0 maximum0
198 (** val stacksize_info_rect_Type2 :
199 (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
200 let rec stacksize_info_rect_Type2 h_mk_stacksize_info x_23642 =
201 let { current = current0; maximum = maximum0 } = x_23642 in
202 h_mk_stacksize_info current0 maximum0
204 (** val stacksize_info_rect_Type1 :
205 (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
206 let rec stacksize_info_rect_Type1 h_mk_stacksize_info x_23644 =
207 let { current = current0; maximum = maximum0 } = x_23644 in
208 h_mk_stacksize_info current0 maximum0
210 (** val stacksize_info_rect_Type0 :
211 (Nat.nat -> Nat.nat -> 'a1) -> stacksize_info -> 'a1 **)
212 let rec stacksize_info_rect_Type0 h_mk_stacksize_info x_23646 =
213 let { current = current0; maximum = maximum0 } = x_23646 in
214 h_mk_stacksize_info current0 maximum0
216 (** val current : stacksize_info -> Nat.nat **)
217 let rec current xxx =
220 (** val maximum : stacksize_info -> Nat.nat **)
221 let rec maximum xxx =
224 (** val stacksize_info_inv_rect_Type4 :
225 stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1 **)
226 let stacksize_info_inv_rect_Type4 hterm h1 =
227 let hcut = stacksize_info_rect_Type4 h1 hterm in hcut __
229 (** val stacksize_info_inv_rect_Type3 :
230 stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1 **)
231 let stacksize_info_inv_rect_Type3 hterm h1 =
232 let hcut = stacksize_info_rect_Type3 h1 hterm in hcut __
234 (** val stacksize_info_inv_rect_Type2 :
235 stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1 **)
236 let stacksize_info_inv_rect_Type2 hterm h1 =
237 let hcut = stacksize_info_rect_Type2 h1 hterm in hcut __
239 (** val stacksize_info_inv_rect_Type1 :
240 stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1 **)
241 let stacksize_info_inv_rect_Type1 hterm h1 =
242 let hcut = stacksize_info_rect_Type1 h1 hterm in hcut __
244 (** val stacksize_info_inv_rect_Type0 :
245 stacksize_info -> (Nat.nat -> Nat.nat -> __ -> 'a1) -> 'a1 **)
246 let stacksize_info_inv_rect_Type0 hterm h1 =
247 let hcut = stacksize_info_rect_Type0 h1 hterm in hcut __
249 (** val stacksize_info_discr : stacksize_info -> stacksize_info -> __ **)
250 let stacksize_info_discr x y =
251 Logic.eq_rect_Type2 x
252 (let { current = a0; maximum = a1 } = x in
253 Obj.magic (fun _ dH -> dH __ __)) y
255 (** val stacksize_info_jmdiscr : stacksize_info -> stacksize_info -> __ **)
256 let stacksize_info_jmdiscr x y =
257 Logic.eq_rect_Type2 x
258 (let { current = a0; maximum = a1 } = x in
259 Obj.magic (fun _ dH -> dH __ __)) y
261 (** val update_stacksize_info :
262 (AST.ident -> Nat.nat Types.option) -> stacksize_info -> call_ud
263 List.list -> stacksize_info **)
264 let update_stacksize_info stacksizes =
265 let get_stacksize = fun f ->
266 match stacksizes f with
267 | Types.None -> Nat.O
270 let f = fun ud acc ->
273 let new_stack = Nat.plus (get_stacksize i) acc.current in
274 let new_max = Nat.max acc.maximum new_stack in
275 { current = new_stack; maximum = new_max }
277 let new_stack = Nat.minus acc.current (get_stacksize i) in
278 { current = new_stack; maximum = acc.maximum }
282 (** val extract_call_ud_from_observables :
283 StructuredTraces.intensional_event List.list -> call_ud List.list **)
284 let extract_call_ud_from_observables =
287 | StructuredTraces.IEVcost x -> List.Nil
288 | StructuredTraces.IEVcall i -> List.Cons ((Up i), List.Nil)
289 | StructuredTraces.IEVtailcall (i, j) ->
290 List.Cons ((Down i), (List.Cons ((Up j), List.Nil)))
291 | StructuredTraces.IEVret i -> List.Cons ((Down i), List.Nil)
293 List.foldr (fun ev -> List.append (f ev)) List.Nil
295 (** val extract_call_ud_from_tlr :
296 StructuredTraces.abstract_status -> __ -> __ ->
297 StructuredTraces.trace_label_return -> AST.ident -> call_ud List.list **)
298 let extract_call_ud_from_tlr s st1 st2 tlr curr =
299 extract_call_ud_from_observables
301 (StructuredTraces.observables_trace_label_return s st1 st2 tlr curr))
303 (** val extract_call_ud_from_tll :
304 StructuredTraces.trace_ends_with_ret -> StructuredTraces.abstract_status
305 -> __ -> __ -> StructuredTraces.trace_label_label -> AST.ident -> call_ud
307 let extract_call_ud_from_tll s fl st1 st2 tll curr =
308 extract_call_ud_from_observables
310 (StructuredTraces.observables_trace_label_label fl s st1 st2 tll curr))