source: extracted/events.mli @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 5.0 KB
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open Extralib
10
11open Lists
12
13open Identifiers
14
15open Floats
16
17open Integers
18
19open AST
20
21open Division
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 Option
40
41open Setoids
42
43open Monad
44
45open Positive
46
47open Char
48
49open String
50
51open PreIdentifiers
52
53open Errors
54
55open Div_and_mod
56
57open Jmeq
58
59open Russell
60
61open Util
62
63open Bool
64
65open Relations
66
67open Nat
68
69open List
70
71open Hints_declaration
72
73open Core_notation
74
75open Pts
76
77open Logic
78
79open Types
80
81open Coqlib
82
83open Values
84
85open CostLabel
86
87type eventval =
88| EVint of AST.intsize * AST.bvint
89
90val eventval_rect_Type4 :
91  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
92
93val eventval_rect_Type5 :
94  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
95
96val eventval_rect_Type3 :
97  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
98
99val eventval_rect_Type2 :
100  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
101
102val eventval_rect_Type1 :
103  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
104
105val eventval_rect_Type0 :
106  (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
107
108val eventval_inv_rect_Type4 :
109  eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
110
111val eventval_inv_rect_Type3 :
112  eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
113
114val eventval_inv_rect_Type2 :
115  eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
116
117val eventval_inv_rect_Type1 :
118  eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
119
120val eventval_inv_rect_Type0 :
121  eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
122
123val eventval_discr : eventval -> eventval -> __
124
125val eventval_jmdiscr : eventval -> eventval -> __
126
127type event =
128| EVcost of CostLabel.costlabel
129| EVextcall of AST.ident * eventval List.list * eventval
130
131val event_rect_Type4 :
132  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
133  eventval -> 'a1) -> event -> 'a1
134
135val event_rect_Type5 :
136  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
137  eventval -> 'a1) -> event -> 'a1
138
139val event_rect_Type3 :
140  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
141  eventval -> 'a1) -> event -> 'a1
142
143val event_rect_Type2 :
144  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
145  eventval -> 'a1) -> event -> 'a1
146
147val event_rect_Type1 :
148  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
149  eventval -> 'a1) -> event -> 'a1
150
151val event_rect_Type0 :
152  (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
153  eventval -> 'a1) -> event -> 'a1
154
155val event_inv_rect_Type4 :
156  event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
157  List.list -> eventval -> __ -> 'a1) -> 'a1
158
159val event_inv_rect_Type3 :
160  event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
161  List.list -> eventval -> __ -> 'a1) -> 'a1
162
163val event_inv_rect_Type2 :
164  event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
165  List.list -> eventval -> __ -> 'a1) -> 'a1
166
167val event_inv_rect_Type1 :
168  event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
169  List.list -> eventval -> __ -> 'a1) -> 'a1
170
171val event_inv_rect_Type0 :
172  event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
173  List.list -> eventval -> __ -> 'a1) -> 'a1
174
175val event_discr : event -> event -> __
176
177val event_jmdiscr : event -> event -> __
178
179type trace = event List.list
180
181val e0 : trace
182
183val echarge : CostLabel.costlabel -> trace
184
185val eextcall : AST.ident -> eventval List.list -> eventval -> trace
186
187val eapp : trace -> trace -> trace
188
189type traceinf = __traceinf Lazy.t
190and __traceinf =
191| Econsinf of event * traceinf
192
193val traceinf_inv_rect_Type4 :
194  traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
195
196val traceinf_inv_rect_Type3 :
197  traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
198
199val traceinf_inv_rect_Type2 :
200  traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
201
202val traceinf_inv_rect_Type1 :
203  traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
204
205val traceinf_inv_rect_Type0 :
206  traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
207
208val traceinf_discr : traceinf -> traceinf -> __
209
210val traceinf_jmdiscr : traceinf -> traceinf -> __
211
212val eappinf : trace -> traceinf -> traceinf
213
214val remove_costs : trace -> trace
215
216type traceinf' = __traceinf' Lazy.t
217and __traceinf' =
218| Econsinf' of trace * traceinf'
219
220val traceinf'_inv_rect_Type4 :
221  traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
222
223val traceinf'_inv_rect_Type3 :
224  traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
225
226val traceinf'_inv_rect_Type2 :
227  traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
228
229val traceinf'_inv_rect_Type1 :
230  traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
231
232val traceinf'_inv_rect_Type0 :
233  traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
234
235val traceinf'_discr : traceinf' -> traceinf' -> __
236
237val traceinf'_jmdiscr : traceinf' -> traceinf' -> __
238
239val split_traceinf' : trace -> traceinf' -> (event, traceinf') Types.prod
240
241val traceinf_of_traceinf' : traceinf' -> traceinf
242
Note: See TracBrowser for help on using the repository browser.