source: extracted/events.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

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 Exp
22
23open Arithmetic
24
25open Extranat
26
27open Vector
28
29open FoldStuff
30
31open BitVector
32
33open Z
34
35open BitVectorZ
36
37open Pointers
38
39open ErrorMessages
40
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 BitVectorTrie
84
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
93| EVint (sz, x_5485) -> h_EVint sz x_5485
94
95(** val eventval_rect_Type5 :
96    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
97let rec eventval_rect_Type5 h_EVint = function
98| EVint (sz, x_5488) -> h_EVint sz x_5488
99
100(** val eventval_rect_Type3 :
101    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
102let rec eventval_rect_Type3 h_EVint = function
103| EVint (sz, x_5491) -> h_EVint sz x_5491
104
105(** val eventval_rect_Type2 :
106    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
107let rec eventval_rect_Type2 h_EVint = function
108| EVint (sz, x_5494) -> h_EVint sz x_5494
109
110(** val eventval_rect_Type1 :
111    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
112let rec eventval_rect_Type1 h_EVint = function
113| EVint (sz, x_5497) -> h_EVint sz x_5497
114
115(** val eventval_rect_Type0 :
116    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
117let rec eventval_rect_Type0 h_EVint = function
118| EVint (sz, x_5500) -> h_EVint sz x_5500
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
163| EVcost x_5525 -> h_EVcost x_5525
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
170| EVcost x_5529 -> h_EVcost x_5529
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
177| EVcost x_5533 -> h_EVcost x_5533
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
184| EVcost x_5537 -> h_EVcost x_5537
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
191| EVcost x_5541 -> h_EVcost x_5541
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
198| EVcost x_5545 -> h_EVcost x_5545
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.