source: driver/extracted/logic.mli @ 3106

Last change on this file since 3106 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: 2.6 KB
Line 
1open Preamble
2
3open Core_notation
4
5open Pts
6
7open Hints_declaration
8
9val eq_rect_Type4 : 'a1 -> 'a2 -> 'a1 -> 'a2
10
11val eq_rect_Type5 : 'a1 -> 'a2 -> 'a1 -> 'a2
12
13val eq_rect_Type3 : 'a1 -> 'a2 -> 'a1 -> 'a2
14
15val eq_rect_Type2 : 'a1 -> 'a2 -> 'a1 -> 'a2
16
17val eq_rect_Type1 : 'a1 -> 'a2 -> 'a1 -> 'a2
18
19val eq_rect_Type0 : 'a1 -> 'a2 -> 'a1 -> 'a2
20
21val eq_rect_r : 'a1 -> 'a1 -> 'a2 -> 'a2
22
23val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2
24
25val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2
26
27val eq_rect_Type2_r : 'a1 -> 'a2 -> 'a1 -> 'a2
28
29val eq_rect_Type3_r : 'a1 -> 'a2 -> 'a1 -> 'a2
30
31val rewrite_l : 'a1 -> 'a2 -> 'a1 -> 'a2
32
33val rewrite_r : 'a1 -> 'a2 -> 'a1 -> 'a2
34
35val eq_coerc : 'a1 -> 'a2
36
37val true_rect_Type4 : 'a1 -> 'a1
38
39val true_rect_Type5 : 'a1 -> 'a1
40
41val true_rect_Type3 : 'a1 -> 'a1
42
43val true_rect_Type2 : 'a1 -> 'a1
44
45val true_rect_Type1 : 'a1 -> 'a1
46
47val true_rect_Type0 : 'a1 -> 'a1
48
49val true_inv_rect_Type4 : (__ -> 'a1) -> 'a1
50
51val true_inv_rect_Type3 : (__ -> 'a1) -> 'a1
52
53val true_inv_rect_Type2 : (__ -> 'a1) -> 'a1
54
55val true_inv_rect_Type1 : (__ -> 'a1) -> 'a1
56
57val true_inv_rect_Type0 : (__ -> 'a1) -> 'a1
58
59val true_discr : __ -> __
60
61val false_rect_Type4 : __ -> 'a1
62
63val false_rect_Type5 : __ -> 'a1
64
65val false_rect_Type3 : __ -> 'a1
66
67val false_rect_Type2 : __ -> 'a1
68
69val false_rect_Type1 : __ -> 'a1
70
71val false_rect_Type0 : __ -> 'a1
72
73val not_rect_Type4 : (__ -> 'a1) -> 'a1
74
75val not_rect_Type5 : (__ -> 'a1) -> 'a1
76
77val not_rect_Type3 : (__ -> 'a1) -> 'a1
78
79val not_rect_Type2 : (__ -> 'a1) -> 'a1
80
81val not_rect_Type1 : (__ -> 'a1) -> 'a1
82
83val not_rect_Type0 : (__ -> 'a1) -> 'a1
84
85val not_inv_rect_Type4 : (__ -> __ -> 'a1) -> 'a1
86
87val not_inv_rect_Type3 : (__ -> __ -> 'a1) -> 'a1
88
89val not_inv_rect_Type2 : (__ -> __ -> 'a1) -> 'a1
90
91val not_inv_rect_Type1 : (__ -> __ -> 'a1) -> 'a1
92
93val not_inv_rect_Type0 : (__ -> __ -> 'a1) -> 'a1
94
95val and_rect_Type4 : (__ -> __ -> 'a1) -> 'a1
96
97val and_rect_Type5 : (__ -> __ -> 'a1) -> 'a1
98
99val and_rect_Type3 : (__ -> __ -> 'a1) -> 'a1
100
101val and_rect_Type2 : (__ -> __ -> 'a1) -> 'a1
102
103val and_rect_Type1 : (__ -> __ -> 'a1) -> 'a1
104
105val and_rect_Type0 : (__ -> __ -> 'a1) -> 'a1
106
107val and_inv_rect_Type4 : (__ -> __ -> __ -> 'a1) -> 'a1
108
109val and_inv_rect_Type3 : (__ -> __ -> __ -> 'a1) -> 'a1
110
111val and_inv_rect_Type2 : (__ -> __ -> __ -> 'a1) -> 'a1
112
113val and_inv_rect_Type1 : (__ -> __ -> __ -> 'a1) -> 'a1
114
115val and_inv_rect_Type0 : (__ -> __ -> __ -> 'a1) -> 'a1
116
117val r0 : 'a1 -> 'a1
118
119val r1 : 'a1 -> 'a2 -> 'a1 -> 'a2
120
121val r2 : 'a1 -> 'a2 -> 'a3 -> 'a1 -> 'a2 -> 'a3
122
123val r3 : 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a1 -> 'a2 -> 'a3 -> 'a4
124
125val r4 : 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5 -> 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5
126
127val streicherK : 'a1 -> 'a2 -> 'a2
128
Note: See TracBrowser for help on using the repository browser.