source: extracted/identifiers.mli @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 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: 7.2 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Char
14
15open Bool
16
17open Relations
18
19open Nat
20
21open List
22
23open String
24
25open Positive
26
27open Setoids
28
29open Monad
30
31open Option
32
33open Div_and_mod
34
35open Jmeq
36
37open Russell
38
39open Util
40
41open Lists
42
43open Extralib
44
45open PreIdentifiers
46
47open Errors
48
49type universe =
50  Positive.pos
51  (* singleton inductive, whose constructor was mk_universe *)
52
53val universe_rect_Type4 :
54  String.string -> (Positive.pos -> 'a1) -> universe -> 'a1
55
56val universe_rect_Type5 :
57  String.string -> (Positive.pos -> 'a1) -> universe -> 'a1
58
59val universe_rect_Type3 :
60  String.string -> (Positive.pos -> 'a1) -> universe -> 'a1
61
62val universe_rect_Type2 :
63  String.string -> (Positive.pos -> 'a1) -> universe -> 'a1
64
65val universe_rect_Type1 :
66  String.string -> (Positive.pos -> 'a1) -> universe -> 'a1
67
68val universe_rect_Type0 :
69  String.string -> (Positive.pos -> 'a1) -> universe -> 'a1
70
71val next_identifier : String.string -> universe -> Positive.pos
72
73val universe_inv_rect_Type4 :
74  String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1
75
76val universe_inv_rect_Type3 :
77  String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1
78
79val universe_inv_rect_Type2 :
80  String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1
81
82val universe_inv_rect_Type1 :
83  String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1
84
85val universe_inv_rect_Type0 :
86  String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1
87
88val universe_discr : String.string -> universe -> universe -> __
89
90val universe_jmdiscr : String.string -> universe -> universe -> __
91
92val new_universe : String.string -> universe
93
94val fresh :
95  String.string -> universe -> (PreIdentifiers.identifier, universe)
96  Types.prod
97
98type fresh_for_univ = __
99
100type env_fresh_for_univ = __
101
102val eq_identifier :
103  String.string -> PreIdentifiers.identifier -> PreIdentifiers.identifier ->
104  Bool.bool
105
106val eq_identifier_elim :
107  String.string -> PreIdentifiers.identifier -> PreIdentifiers.identifier ->
108  (__ -> 'a1) -> (__ -> 'a1) -> 'a1
109
110open Deqsets
111
112val deq_identifier : String.string -> Deqsets.deqSet
113
114val word_of_identifier :
115  String.string -> PreIdentifiers.identifier -> Positive.pos
116
117val identifier_eq :
118  String.string -> PreIdentifiers.identifier -> PreIdentifiers.identifier ->
119  (__, __) Types.sum
120
121val identifier_of_nat : String.string -> Nat.nat -> PreIdentifiers.identifier
122
123type distinct_env = __
124
125val duplicateVariable : String.string
126
127val check_member_env :
128  String.string -> PreIdentifiers.identifier -> (PreIdentifiers.identifier,
129  'a1) Types.prod List.list -> __ Errors.res
130
131val check_distinct_env :
132  String.string -> (PreIdentifiers.identifier, 'a1) Types.prod List.list ->
133  __ Errors.res
134
135open PositiveMap
136
137type 'a identifier_map =
138  'a PositiveMap.positive_map
139  (* singleton inductive, whose constructor was an_id_map *)
140
141val identifier_map_rect_Type4 :
142  String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
143  identifier_map -> 'a2
144
145val identifier_map_rect_Type5 :
146  String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
147  identifier_map -> 'a2
148
149val identifier_map_rect_Type3 :
150  String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
151  identifier_map -> 'a2
152
153val identifier_map_rect_Type2 :
154  String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
155  identifier_map -> 'a2
156
157val identifier_map_rect_Type1 :
158  String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
159  identifier_map -> 'a2
160
161val identifier_map_rect_Type0 :
162  String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
163  identifier_map -> 'a2
164
165val identifier_map_inv_rect_Type4 :
166  String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map -> __
167  -> 'a2) -> 'a2
168
169val identifier_map_inv_rect_Type3 :
170  String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map -> __
171  -> 'a2) -> 'a2
172
173val identifier_map_inv_rect_Type2 :
174  String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map -> __
175  -> 'a2) -> 'a2
176
177val identifier_map_inv_rect_Type1 :
178  String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map -> __
179  -> 'a2) -> 'a2
180
181val identifier_map_inv_rect_Type0 :
182  String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map -> __
183  -> 'a2) -> 'a2
184
185val identifier_map_discr :
186  String.string -> 'a1 identifier_map -> 'a1 identifier_map -> __
187
188val identifier_map_jmdiscr :
189  String.string -> 'a1 identifier_map -> 'a1 identifier_map -> __
190
191val empty_map : String.string -> 'a1 identifier_map
192
193val lookup0 :
194  String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
195  Types.option
196
197val lookup_def :
198  String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1 ->
199  'a1
200
201val member0 :
202  String.string -> 'a1 identifier_map -> PreIdentifiers.identifier ->
203  Bool.bool
204
205val lookup_safe :
206  String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
207
208val add :
209  String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1 ->
210  'a1 identifier_map
211
212val elements :
213  String.string -> 'a1 identifier_map -> (PreIdentifiers.identifier, 'a1)
214  Types.prod List.list
215
216val idmap_all :
217  String.string -> 'a1 identifier_map -> (PreIdentifiers.identifier -> 'a1 ->
218  __ -> Bool.bool) -> Bool.bool
219
220val missingId : String.string
221
222val update0 :
223  String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1 ->
224  'a1 identifier_map Errors.res
225
226val remove :
227  String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
228  identifier_map
229
230val foldi0 :
231  String.string -> (PreIdentifiers.identifier -> 'a1 -> 'a2 -> 'a2) -> 'a1
232  identifier_map -> 'a2 -> 'a2
233
234val fold_inf :
235  String.string -> 'a1 identifier_map -> (PreIdentifiers.identifier -> 'a1 ->
236  __ -> 'a2 -> 'a2) -> 'a2 -> 'a2
237
238val find0 :
239  String.string -> 'a1 identifier_map -> (PreIdentifiers.identifier -> 'a1 ->
240  Bool.bool) -> (PreIdentifiers.identifier, 'a1) Types.prod Types.option
241
242val lookup_present :
243  String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
244
245val update_present :
246  String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1 ->
247  'a1 identifier_map
248
249type fresh_for_map = __
250
251type identifier_set = Types.unit0 identifier_map
252
253val empty_set : String.string -> identifier_set
254
255val add_set :
256  String.string -> identifier_set -> PreIdentifiers.identifier ->
257  identifier_set
258
259val singleton_set :
260  String.string -> PreIdentifiers.identifier -> identifier_set
261
262val union_set :
263  String.string -> 'a1 identifier_map -> 'a2 identifier_map -> identifier_set
264
265val minus_set :
266  String.string -> 'a1 identifier_map -> 'a2 identifier_map -> 'a1
267  identifier_map
268
269val identifierSet : String.string -> Setoids.setoid
270
271val id_map_size : String.string -> 'a1 identifier_map -> Nat.nat
272
273open Proper
274
275val set_from_list :
276  String.string -> PreIdentifiers.identifier List.list -> Types.unit0
277  identifier_map
278
279val choose :
280  String.string -> 'a1 identifier_map -> ((PreIdentifiers.identifier, 'a1)
281  Types.prod, 'a1 identifier_map) Types.prod Types.option
282
283val try_remove :
284  String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> ('a1,
285  'a1 identifier_map) Types.prod Types.option
286
287val id_set_of_map : String.string -> 'a1 identifier_map -> identifier_set
288
289val set_of_list :
290  String.string -> PreIdentifiers.identifier List.list -> identifier_set
291
292val domain_of_map : String.string -> 'a1 identifier_map -> identifier_set
293
Note: See TracBrowser for help on using the repository browser.