source: extracted/events.ml @ 2731

Last change on this file since 2731 was 2730, checked in by sacerdot, 7 years ago

Exported 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
[2717]83open BitVectorTrie
84
[2601]85open CostLabel
86
87type eventval =
88| EVint of AST.intsize * AST.bvint
89
90(** val eventval_rect_Type4 :
91    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
92let rec eventval_rect_Type4 h_EVint = function
[2730]93| EVint (sz, x_4706) -> h_EVint sz x_4706
[2601]94
95(** val eventval_rect_Type5 :
96    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
97let rec eventval_rect_Type5 h_EVint = function
[2730]98| EVint (sz, x_4709) -> h_EVint sz x_4709
[2601]99
100(** val eventval_rect_Type3 :
101    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
102let rec eventval_rect_Type3 h_EVint = function
[2730]103| EVint (sz, x_4712) -> h_EVint sz x_4712
[2601]104
105(** val eventval_rect_Type2 :
106    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
107let rec eventval_rect_Type2 h_EVint = function
[2730]108| EVint (sz, x_4715) -> h_EVint sz x_4715
[2601]109
110(** val eventval_rect_Type1 :
111    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
112let rec eventval_rect_Type1 h_EVint = function
[2730]113| EVint (sz, x_4718) -> h_EVint sz x_4718
[2601]114
115(** val eventval_rect_Type0 :
116    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
117let rec eventval_rect_Type0 h_EVint = function
[2730]118| EVint (sz, x_4721) -> h_EVint sz x_4721
[2601]119
120(** val eventval_inv_rect_Type4 :
121    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
122let eventval_inv_rect_Type4 hterm h1 =
123  let hcut = eventval_rect_Type4 h1 hterm in hcut __
124
125(** val eventval_inv_rect_Type3 :
126    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
127let eventval_inv_rect_Type3 hterm h1 =
128  let hcut = eventval_rect_Type3 h1 hterm in hcut __
129
130(** val eventval_inv_rect_Type2 :
131    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
132let eventval_inv_rect_Type2 hterm h1 =
133  let hcut = eventval_rect_Type2 h1 hterm in hcut __
134
135(** val eventval_inv_rect_Type1 :
136    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
137let eventval_inv_rect_Type1 hterm h1 =
138  let hcut = eventval_rect_Type1 h1 hterm in hcut __
139
140(** val eventval_inv_rect_Type0 :
141    eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
142let eventval_inv_rect_Type0 hterm h1 =
143  let hcut = eventval_rect_Type0 h1 hterm in hcut __
144
145(** val eventval_discr : eventval -> eventval -> __ **)
146let eventval_discr x y =
147  Logic.eq_rect_Type2 x
148    (let EVint (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y
149
150(** val eventval_jmdiscr : eventval -> eventval -> __ **)
151let eventval_jmdiscr x y =
152  Logic.eq_rect_Type2 x
153    (let EVint (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y
154
155type event =
156| EVcost of CostLabel.costlabel
157| EVextcall of AST.ident * eventval List.list * eventval
158
159(** val event_rect_Type4 :
160    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
161    eventval -> 'a1) -> event -> 'a1 **)
162let rec event_rect_Type4 h_EVcost h_EVextcall = function
[2730]163| EVcost x_4746 -> h_EVcost x_4746
[2601]164| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
165
166(** val event_rect_Type5 :
167    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
168    eventval -> 'a1) -> event -> 'a1 **)
169let rec event_rect_Type5 h_EVcost h_EVextcall = function
[2730]170| EVcost x_4750 -> h_EVcost x_4750
[2601]171| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
172
173(** val event_rect_Type3 :
174    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
175    eventval -> 'a1) -> event -> 'a1 **)
176let rec event_rect_Type3 h_EVcost h_EVextcall = function
[2730]177| EVcost x_4754 -> h_EVcost x_4754
[2601]178| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
179
180(** val event_rect_Type2 :
181    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
182    eventval -> 'a1) -> event -> 'a1 **)
183let rec event_rect_Type2 h_EVcost h_EVextcall = function
[2730]184| EVcost x_4758 -> h_EVcost x_4758
[2601]185| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
186
187(** val event_rect_Type1 :
188    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
189    eventval -> 'a1) -> event -> 'a1 **)
190let rec event_rect_Type1 h_EVcost h_EVextcall = function
[2730]191| EVcost x_4762 -> h_EVcost x_4762
[2601]192| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
193
194(** val event_rect_Type0 :
195    (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
196    eventval -> 'a1) -> event -> 'a1 **)
197let rec event_rect_Type0 h_EVcost h_EVextcall = function
[2730]198| EVcost x_4766 -> h_EVcost x_4766
[2601]199| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
200
201(** val event_inv_rect_Type4 :
202    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
203    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
204let event_inv_rect_Type4 hterm h1 h2 =
205  let hcut = event_rect_Type4 h1 h2 hterm in hcut __
206
207(** val event_inv_rect_Type3 :
208    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
209    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
210let event_inv_rect_Type3 hterm h1 h2 =
211  let hcut = event_rect_Type3 h1 h2 hterm in hcut __
212
213(** val event_inv_rect_Type2 :
214    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
215    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
216let event_inv_rect_Type2 hterm h1 h2 =
217  let hcut = event_rect_Type2 h1 h2 hterm in hcut __
218
219(** val event_inv_rect_Type1 :
220    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
221    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
222let event_inv_rect_Type1 hterm h1 h2 =
223  let hcut = event_rect_Type1 h1 h2 hterm in hcut __
224
225(** val event_inv_rect_Type0 :
226    event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
227    List.list -> eventval -> __ -> 'a1) -> 'a1 **)
228let event_inv_rect_Type0 hterm h1 h2 =
229  let hcut = event_rect_Type0 h1 h2 hterm in hcut __
230
231(** val event_discr : event -> event -> __ **)
232let event_discr x y =
233  Logic.eq_rect_Type2 x
234    (match x with
235     | EVcost a0 -> Obj.magic (fun _ dH -> dH __)
236     | EVextcall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
237
238(** val event_jmdiscr : event -> event -> __ **)
239let event_jmdiscr x y =
240  Logic.eq_rect_Type2 x
241    (match x with
242     | EVcost a0 -> Obj.magic (fun _ dH -> dH __)
243     | EVextcall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
244
245type trace = event List.list
246
247(** val e0 : trace **)
248let e0 =
249  List.Nil
250
251(** val echarge : CostLabel.costlabel -> trace **)
252let echarge label =
253  List.Cons ((EVcost label), List.Nil)
254
255(** val eextcall : AST.ident -> eventval List.list -> eventval -> trace **)
256let eextcall name args res1 =
257  List.Cons ((EVextcall (name, args, res1)), List.Nil)
258
259(** val eapp : trace -> trace -> trace **)
260let eapp t1 t2 =
261  List.append t1 t2
262
263type traceinf = __traceinf Lazy.t
264and __traceinf =
265| Econsinf of event * traceinf
266
267(** val traceinf_inv_rect_Type4 :
268    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
269let traceinf_inv_rect_Type4 hterm h1 =
270  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
271
272(** val traceinf_inv_rect_Type3 :
273    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
274let traceinf_inv_rect_Type3 hterm h1 =
275  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
276
277(** val traceinf_inv_rect_Type2 :
278    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
279let traceinf_inv_rect_Type2 hterm h1 =
280  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
281
282(** val traceinf_inv_rect_Type1 :
283    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
284let traceinf_inv_rect_Type1 hterm h1 =
285  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
286
287(** val traceinf_inv_rect_Type0 :
288    traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
289let traceinf_inv_rect_Type0 hterm h1 =
290  let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
291
292(** val traceinf_discr : traceinf -> traceinf -> __ **)
293let traceinf_discr x y =
294  Logic.eq_rect_Type2 x
295    (let Econsinf (a0, a1) = Lazy.force x in
296    Obj.magic (fun _ dH -> dH __ __)) y
297
298(** val traceinf_jmdiscr : traceinf -> traceinf -> __ **)
299let traceinf_jmdiscr x y =
300  Logic.eq_rect_Type2 x
301    (let Econsinf (a0, a1) = Lazy.force x in
302    Obj.magic (fun _ dH -> dH __ __)) y
303
304(** val eappinf : trace -> traceinf -> traceinf **)
305let rec eappinf t t0 =
306  match t with
307  | List.Nil -> t0
308  | List.Cons (ev, t') -> lazy (Econsinf (ev, (eappinf t' t0)))
309
310(** val remove_costs : trace -> trace **)
311let remove_costs =
312  List.filter (fun e1 ->
313    match e1 with
314    | EVcost x -> Bool.False
315    | EVextcall (x, x0, x1) -> Bool.True)
316
317type traceinf' = __traceinf' Lazy.t
318and __traceinf' =
319| Econsinf' of trace * traceinf'
320
321(** val traceinf'_inv_rect_Type4 :
322    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
323let traceinf'_inv_rect_Type4 hterm h1 =
324  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
325  hcut __
326
327(** val traceinf'_inv_rect_Type3 :
328    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
329let traceinf'_inv_rect_Type3 hterm h1 =
330  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
331  hcut __
332
333(** val traceinf'_inv_rect_Type2 :
334    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
335let traceinf'_inv_rect_Type2 hterm h1 =
336  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
337  hcut __
338
339(** val traceinf'_inv_rect_Type1 :
340    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
341let traceinf'_inv_rect_Type1 hterm h1 =
342  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
343  hcut __
344
345(** val traceinf'_inv_rect_Type0 :
346    traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
347let traceinf'_inv_rect_Type0 hterm h1 =
348  let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
349  hcut __
350
351(** val traceinf'_discr : traceinf' -> traceinf' -> __ **)
352let traceinf'_discr x y =
353  Logic.eq_rect_Type2 x
354    (let Econsinf' (a0, a1) = Lazy.force x in
355    Obj.magic (fun _ dH -> dH __ __ __)) y
356
357(** val traceinf'_jmdiscr : traceinf' -> traceinf' -> __ **)
358let traceinf'_jmdiscr x y =
359  Logic.eq_rect_Type2 x
360    (let Econsinf' (a0, a1) = Lazy.force x in
361    Obj.magic (fun _ dH -> dH __ __ __)) y
362
363(** val split_traceinf' :
364    trace -> traceinf' -> (event, traceinf') Types.prod **)
365let split_traceinf' t t0 =
366  (match t with
367   | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
368   | List.Cons (e1, t') ->
369     (fun _ ->
370       (match t' with
371        | List.Nil -> (fun _ -> { Types.fst = e1; Types.snd = t0 })
372        | List.Cons (e', t'') ->
373          (fun _ -> { Types.fst = e1; Types.snd = (lazy (Econsinf' (t',
374            t0))) })) __)) __
375
376(** val traceinf_of_traceinf' : traceinf' -> traceinf **)
377let rec traceinf_of_traceinf' t' =
378  let Econsinf' (t, t'') = Lazy.force t' in
379  let { Types.fst = e1; Types.snd = tl } = split_traceinf' t t'' in
380  lazy (Econsinf (e1, (traceinf_of_traceinf' tl)))
381
Note: See TracBrowser for help on using the repository browser.