source: extracted/events.ml @ 2649

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

...

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