source: extracted/types.mli @ 2746

Last change on this file since 2746 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.9 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11type void = unit (* empty inductive *)
12
13val void_rect_Type4 : void -> 'a1
14
15val void_rect_Type5 : void -> 'a1
16
17val void_rect_Type3 : void -> 'a1
18
19val void_rect_Type2 : void -> 'a1
20
21val void_rect_Type1 : void -> 'a1
22
23val void_rect_Type0 : void -> 'a1
24
25type unit0 =
26| It
27
28val unit_rect_Type4 : 'a1 -> unit0 -> 'a1
29
30val unit_rect_Type5 : 'a1 -> unit0 -> 'a1
31
32val unit_rect_Type3 : 'a1 -> unit0 -> 'a1
33
34val unit_rect_Type2 : 'a1 -> unit0 -> 'a1
35
36val unit_rect_Type1 : 'a1 -> unit0 -> 'a1
37
38val unit_rect_Type0 : 'a1 -> unit0 -> 'a1
39
40val unit_inv_rect_Type4 : unit0 -> (__ -> 'a1) -> 'a1
41
42val unit_inv_rect_Type3 : unit0 -> (__ -> 'a1) -> 'a1
43
44val unit_inv_rect_Type2 : unit0 -> (__ -> 'a1) -> 'a1
45
46val unit_inv_rect_Type1 : unit0 -> (__ -> 'a1) -> 'a1
47
48val unit_inv_rect_Type0 : unit0 -> (__ -> 'a1) -> 'a1
49
50val unit_discr : unit0 -> unit0 -> __
51
52type ('a, 'b) sum =
53| Inl of 'a
54| Inr of 'b
55
56val sum_rect_Type4 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
57
58val sum_rect_Type5 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
59
60val sum_rect_Type3 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
61
62val sum_rect_Type2 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
63
64val sum_rect_Type1 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
65
66val sum_rect_Type0 : ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3
67
68val sum_inv_rect_Type4 :
69  ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3
70
71val sum_inv_rect_Type3 :
72  ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3
73
74val sum_inv_rect_Type2 :
75  ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3
76
77val sum_inv_rect_Type1 :
78  ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3
79
80val sum_inv_rect_Type0 :
81  ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3
82
83val sum_discr : ('a1, 'a2) sum -> ('a1, 'a2) sum -> __
84
85type 'a option =
86| None
87| Some of 'a
88
89val option_rect_Type4 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
90
91val option_rect_Type5 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
92
93val option_rect_Type3 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
94
95val option_rect_Type2 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
96
97val option_rect_Type1 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
98
99val option_rect_Type0 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2
100
101val option_inv_rect_Type4 :
102  'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2
103
104val option_inv_rect_Type3 :
105  'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2
106
107val option_inv_rect_Type2 :
108  'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2
109
110val option_inv_rect_Type1 :
111  'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2
112
113val option_inv_rect_Type0 :
114  'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2
115
116val option_discr : 'a1 option -> 'a1 option -> __
117
118val option_map : ('a1 -> 'a2) -> 'a1 option -> 'a2 option
119
120val option_map_def : ('a1 -> 'a2) -> 'a2 -> 'a1 option -> 'a2
121
122val refute_none_by_refl :
123  ('a1 -> 'a2) -> 'a1 option -> ('a1 -> __ -> 'a3) -> 'a3
124
125type ('a, 'f) dPair = { dpi1 : 'a; dpi2 : 'f }
126
127val dPair_rect_Type4 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
128
129val dPair_rect_Type5 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
130
131val dPair_rect_Type3 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
132
133val dPair_rect_Type2 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
134
135val dPair_rect_Type1 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
136
137val dPair_rect_Type0 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3
138
139val dpi1 : ('a1, 'a2) dPair -> 'a1
140
141val dpi2 : ('a1, 'a2) dPair -> 'a2
142
143val dPair_inv_rect_Type4 :
144  ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
145
146val dPair_inv_rect_Type3 :
147  ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
148
149val dPair_inv_rect_Type2 :
150  ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
151
152val dPair_inv_rect_Type1 :
153  ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
154
155val dPair_inv_rect_Type0 :
156  ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
157
158val dPair_discr : ('a1, 'a2) dPair -> ('a1, 'a2) dPair -> __
159
160type 'a sig0 =
161  'a
162  (* singleton inductive, whose constructor was mk_Sig *)
163
164val sig_rect_Type4 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
165
166val sig_rect_Type5 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
167
168val sig_rect_Type3 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
169
170val sig_rect_Type2 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
171
172val sig_rect_Type1 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
173
174val sig_rect_Type0 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2
175
176val pi1 : 'a1 sig0 -> 'a1
177
178val sig_inv_rect_Type4 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2
179
180val sig_inv_rect_Type3 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2
181
182val sig_inv_rect_Type2 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2
183
184val sig_inv_rect_Type1 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2
185
186val sig_inv_rect_Type0 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2
187
188val sig_discr : 'a1 sig0 -> 'a1 sig0 -> __
189
190type ('a, 'b) prod = { fst : 'a; snd : 'b }
191
192val prod_rect_Type4 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
193
194val prod_rect_Type5 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
195
196val prod_rect_Type3 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
197
198val prod_rect_Type2 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
199
200val prod_rect_Type1 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
201
202val prod_rect_Type0 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3
203
204val fst : ('a1, 'a2) prod -> 'a1
205
206val snd : ('a1, 'a2) prod -> 'a2
207
208val prod_inv_rect_Type4 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
209
210val prod_inv_rect_Type3 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
211
212val prod_inv_rect_Type2 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
213
214val prod_inv_rect_Type1 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
215
216val prod_inv_rect_Type0 : ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
217
218val prod_discr : ('a1, 'a2) prod -> ('a1, 'a2) prod -> __
219
220val coerc_pair_sigma : ('a1, 'a2) prod -> ('a1, 'a2 sig0) prod
221
Note: See TracBrowser for help on using the repository browser.