69 open Hints_declaration
86 | EVint of AST.intsize * AST.bvint
88 (** val eventval_rect_Type4 :
89 (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
90 let rec eventval_rect_Type4 h_EVint = function
91 | EVint (sz, x_5537) -> h_EVint sz x_5537
93 (** val eventval_rect_Type5 :
94 (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
95 let rec eventval_rect_Type5 h_EVint = function
96 | EVint (sz, x_5540) -> h_EVint sz x_5540
98 (** val eventval_rect_Type3 :
99 (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
100 let rec eventval_rect_Type3 h_EVint = function
101 | EVint (sz, x_5543) -> h_EVint sz x_5543
103 (** val eventval_rect_Type2 :
104 (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
105 let rec eventval_rect_Type2 h_EVint = function
106 | EVint (sz, x_5546) -> h_EVint sz x_5546
108 (** val eventval_rect_Type1 :
109 (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
110 let rec eventval_rect_Type1 h_EVint = function
111 | EVint (sz, x_5549) -> h_EVint sz x_5549
113 (** val eventval_rect_Type0 :
114 (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
115 let rec eventval_rect_Type0 h_EVint = function
116 | EVint (sz, x_5552) -> h_EVint sz x_5552
118 (** val eventval_inv_rect_Type4 :
119 eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
120 let eventval_inv_rect_Type4 hterm h1 =
121 let hcut = eventval_rect_Type4 h1 hterm in hcut __
123 (** val eventval_inv_rect_Type3 :
124 eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
125 let eventval_inv_rect_Type3 hterm h1 =
126 let hcut = eventval_rect_Type3 h1 hterm in hcut __
128 (** val eventval_inv_rect_Type2 :
129 eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
130 let eventval_inv_rect_Type2 hterm h1 =
131 let hcut = eventval_rect_Type2 h1 hterm in hcut __
133 (** val eventval_inv_rect_Type1 :
134 eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
135 let eventval_inv_rect_Type1 hterm h1 =
136 let hcut = eventval_rect_Type1 h1 hterm in hcut __
138 (** val eventval_inv_rect_Type0 :
139 eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
140 let eventval_inv_rect_Type0 hterm h1 =
141 let hcut = eventval_rect_Type0 h1 hterm in hcut __
143 (** val eventval_discr : eventval -> eventval -> __ **)
144 let eventval_discr x y =
145 Logic.eq_rect_Type2 x
146 (let EVint (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y
148 (** val eventval_jmdiscr : eventval -> eventval -> __ **)
149 let eventval_jmdiscr x y =
150 Logic.eq_rect_Type2 x
151 (let EVint (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y
154 | EVcost of CostLabel.costlabel
155 | EVextcall of AST.ident * eventval List.list * eventval
157 (** val event_rect_Type4 :
158 (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
159 eventval -> 'a1) -> event -> 'a1 **)
160 let rec event_rect_Type4 h_EVcost h_EVextcall = function
161 | EVcost x_5577 -> h_EVcost x_5577
162 | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
164 (** val event_rect_Type5 :
165 (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
166 eventval -> 'a1) -> event -> 'a1 **)
167 let rec event_rect_Type5 h_EVcost h_EVextcall = function
168 | EVcost x_5581 -> h_EVcost x_5581
169 | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
171 (** val event_rect_Type3 :
172 (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
173 eventval -> 'a1) -> event -> 'a1 **)
174 let rec event_rect_Type3 h_EVcost h_EVextcall = function
175 | EVcost x_5585 -> h_EVcost x_5585
176 | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
178 (** val event_rect_Type2 :
179 (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
180 eventval -> 'a1) -> event -> 'a1 **)
181 let rec event_rect_Type2 h_EVcost h_EVextcall = function
182 | EVcost x_5589 -> h_EVcost x_5589
183 | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
185 (** val event_rect_Type1 :
186 (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
187 eventval -> 'a1) -> event -> 'a1 **)
188 let rec event_rect_Type1 h_EVcost h_EVextcall = function
189 | EVcost x_5593 -> h_EVcost x_5593
190 | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
192 (** val event_rect_Type0 :
193 (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
194 eventval -> 'a1) -> event -> 'a1 **)
195 let rec event_rect_Type0 h_EVcost h_EVextcall = function
196 | EVcost x_5597 -> h_EVcost x_5597
197 | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
199 (** val event_inv_rect_Type4 :
200 event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
201 List.list -> eventval -> __ -> 'a1) -> 'a1 **)
202 let event_inv_rect_Type4 hterm h1 h2 =
203 let hcut = event_rect_Type4 h1 h2 hterm in hcut __
205 (** val event_inv_rect_Type3 :
206 event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
207 List.list -> eventval -> __ -> 'a1) -> 'a1 **)
208 let event_inv_rect_Type3 hterm h1 h2 =
209 let hcut = event_rect_Type3 h1 h2 hterm in hcut __
211 (** val event_inv_rect_Type2 :
212 event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
213 List.list -> eventval -> __ -> 'a1) -> 'a1 **)
214 let event_inv_rect_Type2 hterm h1 h2 =
215 let hcut = event_rect_Type2 h1 h2 hterm in hcut __
217 (** val event_inv_rect_Type1 :
218 event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
219 List.list -> eventval -> __ -> 'a1) -> 'a1 **)
220 let event_inv_rect_Type1 hterm h1 h2 =
221 let hcut = event_rect_Type1 h1 h2 hterm in hcut __
223 (** val event_inv_rect_Type0 :
224 event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
225 List.list -> eventval -> __ -> 'a1) -> 'a1 **)
226 let event_inv_rect_Type0 hterm h1 h2 =
227 let hcut = event_rect_Type0 h1 h2 hterm in hcut __
229 (** val event_discr : event -> event -> __ **)
230 let event_discr x y =
231 Logic.eq_rect_Type2 x
233 | EVcost a0 -> Obj.magic (fun _ dH -> dH __)
234 | EVextcall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
236 (** val event_jmdiscr : event -> event -> __ **)
237 let event_jmdiscr x y =
238 Logic.eq_rect_Type2 x
240 | EVcost a0 -> Obj.magic (fun _ dH -> dH __)
241 | EVextcall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
243 type trace = event List.list
245 (** val e0 : trace **)
249 (** val echarge : CostLabel.costlabel -> trace **)
251 List.Cons ((EVcost label), List.Nil)
253 (** val eextcall : AST.ident -> eventval List.list -> eventval -> trace **)
254 let eextcall name args res =
255 List.Cons ((EVextcall (name, args, res)), List.Nil)
257 (** val eapp : trace -> trace -> trace **)
261 type traceinf = __traceinf Lazy.t
263 | Econsinf of event * traceinf
265 (** val traceinf_inv_rect_Type4 :
266 traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
267 let traceinf_inv_rect_Type4 hterm h1 =
268 let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
270 (** val traceinf_inv_rect_Type3 :
271 traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
272 let traceinf_inv_rect_Type3 hterm h1 =
273 let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
275 (** val traceinf_inv_rect_Type2 :
276 traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
277 let traceinf_inv_rect_Type2 hterm h1 =
278 let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
280 (** val traceinf_inv_rect_Type1 :
281 traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
282 let traceinf_inv_rect_Type1 hterm h1 =
283 let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
285 (** val traceinf_inv_rect_Type0 :
286 traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
287 let traceinf_inv_rect_Type0 hterm h1 =
288 let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
290 (** val traceinf_discr : traceinf -> traceinf -> __ **)
291 let traceinf_discr x y =
292 Logic.eq_rect_Type2 x
293 (let Econsinf (a0, a1) = Lazy.force x in
294 Obj.magic (fun _ dH -> dH __ __)) y
296 (** val traceinf_jmdiscr : traceinf -> traceinf -> __ **)
297 let traceinf_jmdiscr x y =
298 Logic.eq_rect_Type2 x
299 (let Econsinf (a0, a1) = Lazy.force x in
300 Obj.magic (fun _ dH -> dH __ __)) y
302 (** val eappinf : trace -> traceinf -> traceinf **)
303 let rec eappinf t t0 =
306 | List.Cons (ev, t') -> lazy (Econsinf (ev, (eappinf t' t0)))
308 (** val remove_costs : trace -> trace **)
310 List.filter (fun e ->
312 | EVcost x -> Bool.False
313 | EVextcall (x, x0, x1) -> Bool.True)
315 type traceinf' = __traceinf' Lazy.t
317 | Econsinf' of trace * traceinf'
319 (** val traceinf'_inv_rect_Type4 :
320 traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
321 let traceinf'_inv_rect_Type4 hterm h1 =
322 let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
325 (** val traceinf'_inv_rect_Type3 :
326 traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
327 let traceinf'_inv_rect_Type3 hterm h1 =
328 let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
331 (** val traceinf'_inv_rect_Type2 :
332 traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
333 let traceinf'_inv_rect_Type2 hterm h1 =
334 let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
337 (** val traceinf'_inv_rect_Type1 :
338 traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
339 let traceinf'_inv_rect_Type1 hterm h1 =
340 let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
343 (** val traceinf'_inv_rect_Type0 :
344 traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
345 let traceinf'_inv_rect_Type0 hterm h1 =
346 let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
349 (** val traceinf'_discr : traceinf' -> traceinf' -> __ **)
350 let traceinf'_discr x y =
351 Logic.eq_rect_Type2 x
352 (let Econsinf' (a0, a1) = Lazy.force x in
353 Obj.magic (fun _ dH -> dH __ __ __)) y
355 (** val traceinf'_jmdiscr : traceinf' -> traceinf' -> __ **)
356 let traceinf'_jmdiscr x y =
357 Logic.eq_rect_Type2 x
358 (let Econsinf' (a0, a1) = Lazy.force x in
359 Obj.magic (fun _ dH -> dH __ __ __)) y
361 (** val split_traceinf' :
362 trace -> traceinf' -> (event, traceinf') Types.prod **)
363 let split_traceinf' t t0 =
365 | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
366 | List.Cons (e, t') ->
369 | List.Nil -> (fun _ -> { Types.fst = e; Types.snd = t0 })
370 | List.Cons (e', t'') ->
371 (fun _ -> { Types.fst = e; Types.snd = (lazy (Econsinf' (t',
374 (** val traceinf_of_traceinf' : traceinf' -> traceinf **)
375 let rec traceinf_of_traceinf' t' =
376 let Econsinf' (t, t'') = Lazy.force t' in
377 let { Types.fst = e; Types.snd = tl } = split_traceinf' t t'' in
378 lazy (Econsinf (e, (traceinf_of_traceinf' tl)))