source: extracted/events.ml @ 2968

Last change on this file since 2968 was 2827, checked in by sacerdot, 7 years ago

Everything extracted again.

File size: 11.1 KB
RevLine 
[2601]1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open Extralib
10
11open Lists
12
13open Identifiers
14
15open Integers
16
17open AST
18
19open Division
20
[2717]21open Exp
22
[2601]23open Arithmetic
24
25open Extranat
26
27open Vector
28
29open FoldStuff
30
31open BitVector
32
33open Z
34
35open BitVectorZ
36
37open Pointers
38
[2649]39open ErrorMessages
40
[2601]41open Option
42
43open Setoids
44
45open Monad
46
47open Positive
48
49open PreIdentifiers
50
51open Errors
52
53open Div_and_mod
54
55open Jmeq
56
57open Russell
58
59open Util
60
61open Bool
62
63open Relations
64
65open Nat
66
67open List
68
69open Hints_declaration
70
71open Core_notation
72
73open Pts
74
75open Logic
76
77open Types
78
79open Coqlib
80
81open Values
82
83open CostLabel
84
85type eventval =
86| EVint of AST.intsize * AST.bvint
87
88(** val eventval_rect_Type4 :
89    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
90let rec eventval_rect_Type4 h_EVint = function
[2827]91| EVint (sz, x_5524) -> h_EVint sz x_5524
[2601]92
93(** val eventval_rect_Type5 :
94    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
95let rec eventval_rect_Type5 h_EVint = function
[2827]96| EVint (sz, x_5527) -> h_EVint sz x_5527
[2601]97
98(** val eventval_rect_Type3 :
99    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
100let rec eventval_rect_Type3 h_EVint = function
[2827]101| EVint (sz, x_5530) -> h_EVint sz x_5530
[2601]102
103(** val eventval_rect_Type2 :
104    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
105let rec eventval_rect_Type2 h_EVint = function
[2827]106| EVint (sz, x_5533) -> h_EVint sz x_5533
[2601]107
108(** val eventval_rect_Type1 :
109    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
110let rec eventval_rect_Type1 h_EVint = function
[2827]111| EVint (sz, x_5536) -> h_EVint sz x_5536
[2601]112
113(** val eventval_rect_Type0 :
114    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
115let rec eventval_rect_Type0 h_EVint = function
[2827]116| EVint (sz, x_5539) -> h_EVint sz x_5539
[2601]117
118(** val eventval_inv_rect_Type4 :
119    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
120let eventval_inv_rect_Type4 hterm h1 =
121  let hcut = eventval_rect_Type4 h1 hterm in hcut __
122
123(** val eventval_inv_rect_Type3 :
124    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
125let eventval_inv_rect_Type3 hterm h1 =
126  let hcut = eventval_rect_Type3 h1 hterm in hcut __
127
128(** val eventval_inv_rect_Type2 :
129    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
130let eventval_inv_rect_Type2 hterm h1 =
131  let hcut = eventval_rect_Type2 h1 hterm in hcut __
132
133(** val eventval_inv_rect_Type1 :
134    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
135let eventval_inv_rect_Type1 hterm h1 =
136  let hcut = eventval_rect_Type1 h1 hterm in hcut __
137
138(** val eventval_inv_rect_Type0 :
139    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
140let eventval_inv_rect_Type0 hterm h1 =
141  let hcut = eventval_rect_Type0 h1 hterm in hcut __
142
143(** val eventval_discr : eventval -> eventval -> __ **)
144let eventval_discr x y =
145  Logic.eq_rect_Type2 x
146    (let EVint (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y
147
148(** val eventval_jmdiscr : eventval -> eventval -> __ **)
149let eventval_jmdiscr x y =
150  Logic.eq_rect_Type2 x
151    (let EVint (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y
152
153type event =
154| EVcost of CostLabel.costlabel
155| EVextcall of AST.ident * eventval List.list * eventval
156
157(** val event_rect_Type4 :
158    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
159    eventval -> 'a1) -> event -> 'a1 **)
160let rec event_rect_Type4 h_EVcost h_EVextcall = function
[2827]161| EVcost x_5564 -> h_EVcost x_5564
[2601]162| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
163
164(** val event_rect_Type5 :
165    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
166    eventval -> 'a1) -> event -> 'a1 **)
167let rec event_rect_Type5 h_EVcost h_EVextcall = function
[2827]168| EVcost x_5568 -> h_EVcost x_5568
[2601]169| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
170
171(** val event_rect_Type3 :
172    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
173    eventval -> 'a1) -> event -> 'a1 **)
174let rec event_rect_Type3 h_EVcost h_EVextcall = function
[2827]175| EVcost x_5572 -> h_EVcost x_5572
[2601]176| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
177
178(** val event_rect_Type2 :
179    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
180    eventval -> 'a1) -> event -> 'a1 **)
181let rec event_rect_Type2 h_EVcost h_EVextcall = function
[2827]182| EVcost x_5576 -> h_EVcost x_5576
[2601]183| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
184
185(** val event_rect_Type1 :
186    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
187    eventval -> 'a1) -> event -> 'a1 **)
188let rec event_rect_Type1 h_EVcost h_EVextcall = function
[2827]189| EVcost x_5580 -> h_EVcost x_5580
[2601]190| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
191
192(** val event_rect_Type0 :
193    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
194    eventval -> 'a1) -> event -> 'a1 **)
195let rec event_rect_Type0 h_EVcost h_EVextcall = function
[2827]196| EVcost x_5584 -> h_EVcost x_5584
[2601]197| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
198
199(** val event_inv_rect_Type4 :
200    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
201    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
202let event_inv_rect_Type4 hterm h1 h2 =
203  let hcut = event_rect_Type4 h1 h2 hterm in hcut __
204
205(** val event_inv_rect_Type3 :
206    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
207    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
208let event_inv_rect_Type3 hterm h1 h2 =
209  let hcut = event_rect_Type3 h1 h2 hterm in hcut __
210
211(** val event_inv_rect_Type2 :
212    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
213    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
214let event_inv_rect_Type2 hterm h1 h2 =
215  let hcut = event_rect_Type2 h1 h2 hterm in hcut __
216
217(** val event_inv_rect_Type1 :
218    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
219    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
220let event_inv_rect_Type1 hterm h1 h2 =
221  let hcut = event_rect_Type1 h1 h2 hterm in hcut __
222
223(** val event_inv_rect_Type0 :
224    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
225    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
226let event_inv_rect_Type0 hterm h1 h2 =
227  let hcut = event_rect_Type0 h1 h2 hterm in hcut __
228
229(** val event_discr : event -> event -> __ **)
230let event_discr x y =
231  Logic.eq_rect_Type2 x
232    (match x with
233     | EVcost a0 -> Obj.magic (fun _ dH -> dH __)
234     | EVextcall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
235
236(** val event_jmdiscr : event -> event -> __ **)
237let event_jmdiscr x y =
238  Logic.eq_rect_Type2 x
239    (match x with
240     | EVcost a0 -> Obj.magic (fun _ dH -> dH __)
241     | EVextcall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
242
243type trace = event List.list
244
245(** val e0 : trace **)
246let e0 =
247  List.Nil
248
249(** val echarge : CostLabel.costlabel -> trace **)
250let echarge label =
251  List.Cons ((EVcost label), List.Nil)
252
253(** val eextcall : AST.ident -> eventval List.list -> eventval -> trace **)
[2773]254let eextcall name args res =
255  List.Cons ((EVextcall (name, args, res)), List.Nil)
[2601]256
257(** val eapp : trace -> trace -> trace **)
258let eapp t1 t2 =
259  List.append t1 t2
260
261type traceinf = __traceinf Lazy.t
262and __traceinf =
263| Econsinf of event * traceinf
264
265(** val traceinf_inv_rect_Type4 :
266    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
267let traceinf_inv_rect_Type4 hterm h1 =
268  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
269
270(** val traceinf_inv_rect_Type3 :
271    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
272let traceinf_inv_rect_Type3 hterm h1 =
273  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
274
275(** val traceinf_inv_rect_Type2 :
276    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
277let traceinf_inv_rect_Type2 hterm h1 =
278  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
279
280(** val traceinf_inv_rect_Type1 :
281    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
282let traceinf_inv_rect_Type1 hterm h1 =
283  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
284
285(** val traceinf_inv_rect_Type0 :
286    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
287let traceinf_inv_rect_Type0 hterm h1 =
288  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
289
290(** val traceinf_discr : traceinf -> traceinf -> __ **)
291let 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
295
296(** val traceinf_jmdiscr : traceinf -> traceinf -> __ **)
297let 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
301
302(** val eappinf : trace -> traceinf -> traceinf **)
303let rec eappinf t t0 =
304  match t with
305  | List.Nil -> t0
306  | List.Cons (ev, t') -> lazy (Econsinf (ev, (eappinf t' t0)))
307
308(** val remove_costs : trace -> trace **)
309let remove_costs =
[2773]310  List.filter (fun e ->
311    match e with
[2601]312    | EVcost x -> Bool.False
313    | EVextcall (x, x0, x1) -> Bool.True)
314
315type traceinf' = __traceinf' Lazy.t
316and __traceinf' =
317| Econsinf' of trace * traceinf'
318
319(** val traceinf'_inv_rect_Type4 :
320    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
321let traceinf'_inv_rect_Type4 hterm h1 =
322  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
323  hcut __
324
325(** val traceinf'_inv_rect_Type3 :
326    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
327let traceinf'_inv_rect_Type3 hterm h1 =
328  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
329  hcut __
330
331(** val traceinf'_inv_rect_Type2 :
332    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
333let traceinf'_inv_rect_Type2 hterm h1 =
334  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
335  hcut __
336
337(** val traceinf'_inv_rect_Type1 :
338    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
339let traceinf'_inv_rect_Type1 hterm h1 =
340  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
341  hcut __
342
343(** val traceinf'_inv_rect_Type0 :
344    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
345let traceinf'_inv_rect_Type0 hterm h1 =
346  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
347  hcut __
348
349(** val traceinf'_discr : traceinf' -> traceinf' -> __ **)
350let 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
354
355(** val traceinf'_jmdiscr : traceinf' -> traceinf' -> __ **)
356let 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
360
361(** val split_traceinf' :
362    trace -> traceinf' -> (event, traceinf') Types.prod **)
363let split_traceinf' t t0 =
364  (match t with
365   | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
[2773]366   | List.Cons (e, t') ->
[2601]367     (fun _ ->
368       (match t' with
[2773]369        | List.Nil -> (fun _ -> { Types.fst = e; Types.snd = t0 })
[2601]370        | List.Cons (e', t'') ->
[2773]371          (fun _ -> { Types.fst = e; Types.snd = (lazy (Econsinf' (t',
[2601]372            t0))) })) __)) __
373
374(** val traceinf_of_traceinf' : traceinf' -> traceinf **)
375let rec traceinf_of_traceinf' t' =
376  let Econsinf' (t, t'') = Lazy.force t' in
[2773]377  let { Types.fst = e; Types.snd = tl } = split_traceinf' t t'' in
378  lazy (Econsinf (e, (traceinf_of_traceinf' tl)))
[2601]379
Note: See TracBrowser for help on using the repository browser.