source: extracted/logic.ml @ 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: 6.3 KB
Line 
1open Preamble
2
3open Core_notation
4
5open Pts
6
7open Hints_declaration
8
9(** val eq_rect_Type4 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
10let rec eq_rect_Type4 x h_refl x_4 =
11  h_refl
12
13(** val eq_rect_Type5 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
14let rec eq_rect_Type5 x h_refl x_7 =
15  h_refl
16
17(** val eq_rect_Type3 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
18let rec eq_rect_Type3 x h_refl x_10 =
19  h_refl
20
21(** val eq_rect_Type2 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
22let rec eq_rect_Type2 x h_refl x_13 =
23  h_refl
24
25(** val eq_rect_Type1 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
26let rec eq_rect_Type1 x h_refl x_16 =
27  h_refl
28
29(** val eq_rect_Type0 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
30let rec eq_rect_Type0 x h_refl x_19 =
31  h_refl
32
33(** val eq_rect_r : 'a1 -> 'a1 -> 'a2 -> 'a2 **)
34let eq_rect_r a x x0 =
35  (fun _ auto -> auto) __ x0
36
37(** val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
38let eq_rect_Type0_r a h x =
39  (fun _ auto -> auto) __ h
40
41(** val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
42let eq_rect_Type1_r a h x =
43  (fun _ auto -> auto) __ h
44
45(** val eq_rect_Type2_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
46let eq_rect_Type2_r a h x =
47  (fun _ auto -> auto) __ h
48
49(** val eq_rect_Type3_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
50let eq_rect_Type3_r a h x =
51  (fun _ auto -> auto) __ h
52
53(** val rewrite_l : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
54let rewrite_l x hx y =
55  hx
56
57(** val rewrite_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
58let rewrite_r x hx y =
59  hx
60
61(** val eq_coerc : 'a1 -> 'a2 **)
62let eq_coerc ha =
63  eq_rect_Type0 __ (Obj.magic ha) __
64
65(** val true_rect_Type4 : 'a1 -> 'a1 **)
66let rec true_rect_Type4 h_I =
67  h_I
68
69(** val true_rect_Type5 : 'a1 -> 'a1 **)
70let rec true_rect_Type5 h_I =
71  h_I
72
73(** val true_rect_Type3 : 'a1 -> 'a1 **)
74let rec true_rect_Type3 h_I =
75  h_I
76
77(** val true_rect_Type2 : 'a1 -> 'a1 **)
78let rec true_rect_Type2 h_I =
79  h_I
80
81(** val true_rect_Type1 : 'a1 -> 'a1 **)
82let rec true_rect_Type1 h_I =
83  h_I
84
85(** val true_rect_Type0 : 'a1 -> 'a1 **)
86let rec true_rect_Type0 h_I =
87  h_I
88
89(** val true_inv_rect_Type4 : (__ -> 'a1) -> 'a1 **)
90let true_inv_rect_Type4 h1 =
91  let hcut = true_rect_Type4 h1 in hcut __
92
93(** val true_inv_rect_Type3 : (__ -> 'a1) -> 'a1 **)
94let true_inv_rect_Type3 h1 =
95  let hcut = true_rect_Type3 h1 in hcut __
96
97(** val true_inv_rect_Type2 : (__ -> 'a1) -> 'a1 **)
98let true_inv_rect_Type2 h1 =
99  let hcut = true_rect_Type2 h1 in hcut __
100
101(** val true_inv_rect_Type1 : (__ -> 'a1) -> 'a1 **)
102let true_inv_rect_Type1 h1 =
103  let hcut = true_rect_Type1 h1 in hcut __
104
105(** val true_inv_rect_Type0 : (__ -> 'a1) -> 'a1 **)
106let true_inv_rect_Type0 h1 =
107  let hcut = true_rect_Type0 h1 in hcut __
108
109(** val true_discr : __ -> __ **)
110let true_discr _ =
111  eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH)) __
112
113(** val false_rect_Type4 : __ -> 'a1 **)
114let rec false_rect_Type4 _ =
115  assert false (* absurd case *)
116
117(** val false_rect_Type5 : __ -> 'a1 **)
118let rec false_rect_Type5 _ =
119  assert false (* absurd case *)
120
121(** val false_rect_Type3 : __ -> 'a1 **)
122let rec false_rect_Type3 _ =
123  assert false (* absurd case *)
124
125(** val false_rect_Type2 : __ -> 'a1 **)
126let rec false_rect_Type2 _ =
127  assert false (* absurd case *)
128
129(** val false_rect_Type1 : __ -> 'a1 **)
130let rec false_rect_Type1 _ =
131  assert false (* absurd case *)
132
133(** val false_rect_Type0 : __ -> 'a1 **)
134let rec false_rect_Type0 _ =
135  assert false (* absurd case *)
136
137(** val not_rect_Type4 : (__ -> 'a1) -> 'a1 **)
138let rec not_rect_Type4 h_nmk =
139  h_nmk __
140
141(** val not_rect_Type5 : (__ -> 'a1) -> 'a1 **)
142let rec not_rect_Type5 h_nmk =
143  h_nmk __
144
145(** val not_rect_Type3 : (__ -> 'a1) -> 'a1 **)
146let rec not_rect_Type3 h_nmk =
147  h_nmk __
148
149(** val not_rect_Type2 : (__ -> 'a1) -> 'a1 **)
150let rec not_rect_Type2 h_nmk =
151  h_nmk __
152
153(** val not_rect_Type1 : (__ -> 'a1) -> 'a1 **)
154let rec not_rect_Type1 h_nmk =
155  h_nmk __
156
157(** val not_rect_Type0 : (__ -> 'a1) -> 'a1 **)
158let rec not_rect_Type0 h_nmk =
159  h_nmk __
160
161(** val not_inv_rect_Type4 : (__ -> __ -> 'a1) -> 'a1 **)
162let not_inv_rect_Type4 h1 =
163  let hcut = not_rect_Type4 h1 in hcut __
164
165(** val not_inv_rect_Type3 : (__ -> __ -> 'a1) -> 'a1 **)
166let not_inv_rect_Type3 h1 =
167  let hcut = not_rect_Type3 h1 in hcut __
168
169(** val not_inv_rect_Type2 : (__ -> __ -> 'a1) -> 'a1 **)
170let not_inv_rect_Type2 h1 =
171  let hcut = not_rect_Type2 h1 in hcut __
172
173(** val not_inv_rect_Type1 : (__ -> __ -> 'a1) -> 'a1 **)
174let not_inv_rect_Type1 h1 =
175  let hcut = not_rect_Type1 h1 in hcut __
176
177(** val not_inv_rect_Type0 : (__ -> __ -> 'a1) -> 'a1 **)
178let not_inv_rect_Type0 h1 =
179  let hcut = not_rect_Type0 h1 in hcut __
180
181(** val and_rect_Type4 : (__ -> __ -> 'a1) -> 'a1 **)
182let rec and_rect_Type4 h_conj =
183  h_conj __ __
184
185(** val and_rect_Type5 : (__ -> __ -> 'a1) -> 'a1 **)
186let rec and_rect_Type5 h_conj =
187  h_conj __ __
188
189(** val and_rect_Type3 : (__ -> __ -> 'a1) -> 'a1 **)
190let rec and_rect_Type3 h_conj =
191  h_conj __ __
192
193(** val and_rect_Type2 : (__ -> __ -> 'a1) -> 'a1 **)
194let rec and_rect_Type2 h_conj =
195  h_conj __ __
196
197(** val and_rect_Type1 : (__ -> __ -> 'a1) -> 'a1 **)
198let rec and_rect_Type1 h_conj =
199  h_conj __ __
200
201(** val and_rect_Type0 : (__ -> __ -> 'a1) -> 'a1 **)
202let rec and_rect_Type0 h_conj =
203  h_conj __ __
204
205(** val and_inv_rect_Type4 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
206let and_inv_rect_Type4 h1 =
207  let hcut = and_rect_Type4 h1 in hcut __
208
209(** val and_inv_rect_Type3 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
210let and_inv_rect_Type3 h1 =
211  let hcut = and_rect_Type3 h1 in hcut __
212
213(** val and_inv_rect_Type2 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
214let and_inv_rect_Type2 h1 =
215  let hcut = and_rect_Type2 h1 in hcut __
216
217(** val and_inv_rect_Type1 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
218let and_inv_rect_Type1 h1 =
219  let hcut = and_rect_Type1 h1 in hcut __
220
221(** val and_inv_rect_Type0 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
222let and_inv_rect_Type0 h1 =
223  let hcut = and_rect_Type0 h1 in hcut __
224
225(** val r0 : 'a1 -> 'a1 **)
226let r0 t =
227  t
228
229(** val r1 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
230let r1 x h_refl x_19 =
231  eq_rect_Type0 x h_refl x_19
232
233(** val r2 : 'a1 -> 'a2 -> 'a3 -> 'a1 -> 'a2 -> 'a3 **)
234let r2 a0 a1 a2 b0 b1 =
235  eq_rect_Type0 (r1 a0 a1 b0) (r1 a0 a2 b0) b1
236
237(** val r3 : 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a1 -> 'a2 -> 'a3 -> 'a4 **)
238let r3 a0 a1 a2 a3 b0 b1 b2 =
239  eq_rect_Type0 (r2 a0 a1 a2 b0 b1) (r2 a0 a1 a3 b0 b1) b2
240
241(** val r4 :
242    'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5 -> 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5 **)
243let r4 a0 a1 a2 a3 a4 b0 b1 b2 b3 =
244  eq_rect_Type0 (r3 a0 a1 a2 a3 b0 b1 b2) (r3 a0 a1 a2 a4 b0 b1 b2) b3
245
246(** val streicherK : 'a1 -> 'a2 -> 'a2 **)
247let streicherK t h =
248  eq_rect_Type3_r __ h __
249
Note: See TracBrowser for help on using the repository browser.