source: extracted/jmeq.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: 3.9 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11type sigma =
12  __
13  (* singleton inductive, whose constructor was mk_Sigma *)
14
15(** val sigma_rect_Type4 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
16let rec sigma_rect_Type4 h_mk_Sigma x_890 =
17  let x_891 = x_890 in h_mk_Sigma __ x_891
18
19(** val sigma_rect_Type5 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
20let rec sigma_rect_Type5 h_mk_Sigma x_893 =
21  let x_894 = x_893 in h_mk_Sigma __ x_894
22
23(** val sigma_rect_Type3 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
24let rec sigma_rect_Type3 h_mk_Sigma x_896 =
25  let x_897 = x_896 in h_mk_Sigma __ x_897
26
27(** val sigma_rect_Type2 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
28let rec sigma_rect_Type2 h_mk_Sigma x_899 =
29  let x_900 = x_899 in h_mk_Sigma __ x_900
30
31(** val sigma_rect_Type1 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
32let rec sigma_rect_Type1 h_mk_Sigma x_902 =
33  let x_903 = x_902 in h_mk_Sigma __ x_903
34
35(** val sigma_rect_Type0 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
36let rec sigma_rect_Type0 h_mk_Sigma x_905 =
37  let x_906 = x_905 in h_mk_Sigma __ x_906
38
39(** val sigma_inv_rect_Type4 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
40let sigma_inv_rect_Type4 hterm h1 =
41  let hcut = sigma_rect_Type4 h1 hterm in hcut __
42
43(** val sigma_inv_rect_Type3 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
44let sigma_inv_rect_Type3 hterm h1 =
45  let hcut = sigma_rect_Type3 h1 hterm in hcut __
46
47(** val sigma_inv_rect_Type2 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
48let sigma_inv_rect_Type2 hterm h1 =
49  let hcut = sigma_rect_Type2 h1 hterm in hcut __
50
51(** val sigma_inv_rect_Type1 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
52let sigma_inv_rect_Type1 hterm h1 =
53  let hcut = sigma_rect_Type1 h1 hterm in hcut __
54
55(** val sigma_inv_rect_Type0 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
56let sigma_inv_rect_Type0 hterm h1 =
57  let hcut = sigma_rect_Type0 h1 hterm in hcut __
58
59type p1 = __
60
61(** val p2 : sigma -> p1 **)
62let p2 s =
63  let x = s in x
64
65(** val jmeq_rect_Type4 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
66let rec jmeq_rect_Type4 x h_refl_jmeq x_929 =
67  h_refl_jmeq
68
69(** val jmeq_rect_Type5 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
70let rec jmeq_rect_Type5 x h_refl_jmeq x_932 =
71  h_refl_jmeq
72
73(** val jmeq_rect_Type3 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
74let rec jmeq_rect_Type3 x h_refl_jmeq x_935 =
75  h_refl_jmeq
76
77(** val jmeq_rect_Type2 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
78let rec jmeq_rect_Type2 x h_refl_jmeq x_938 =
79  h_refl_jmeq
80
81(** val jmeq_rect_Type1 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
82let rec jmeq_rect_Type1 x h_refl_jmeq x_941 =
83  h_refl_jmeq
84
85(** val jmeq_rect_Type0 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
86let rec jmeq_rect_Type0 x h_refl_jmeq x_944 =
87  h_refl_jmeq
88
89(** val jmeq_inv_rect_Type4 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
90let jmeq_inv_rect_Type4 x2 x4 h1 =
91  let hcut = jmeq_rect_Type4 x2 h1 x4 in hcut __ __
92
93(** val jmeq_inv_rect_Type3 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
94let jmeq_inv_rect_Type3 x2 x4 h1 =
95  let hcut = jmeq_rect_Type3 x2 h1 x4 in hcut __ __
96
97(** val jmeq_inv_rect_Type2 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
98let jmeq_inv_rect_Type2 x2 x4 h1 =
99  let hcut = jmeq_rect_Type2 x2 h1 x4 in hcut __ __
100
101(** val jmeq_inv_rect_Type1 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
102let jmeq_inv_rect_Type1 x2 x4 h1 =
103  let hcut = jmeq_rect_Type1 x2 h1 x4 in hcut __ __
104
105(** val jmeq_inv_rect_Type0 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
106let jmeq_inv_rect_Type0 x2 x4 h1 =
107  let hcut = jmeq_rect_Type0 x2 h1 x4 in hcut __ __
108
109(** val jmeq_discr : 'a1 -> 'a2 -> __ **)
110let jmeq_discr a2 a4 =
111  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH)) __
112
113(** val cast : 'a1 -> 'a2 **)
114let cast x =
115  (fun x0 -> Obj.magic x0) x
116
117type ('a, 'x) curry = 'x
118
119(** val g : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
120let g x h y =
121  (fun _ -> Logic.eq_rect_Type0 __ h __) __
122
123type 'p pP = 'p
124
125(** val e : 'a1 -> 'a2 pP -> 'a1 -> 'a2 pP **)
126let e a h b =
127  let x = g a h b in x
128
129(** val jmeq_elim : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
130let jmeq_elim x x0 y =
131  e x x0 y
132
Note: See TracBrowser for help on using the repository browser.