source: driver/extracted/jmeq.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: 1.7 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
15val sigma_rect_Type4 : (__ -> __ -> 'a1) -> sigma -> 'a1
16
17val sigma_rect_Type5 : (__ -> __ -> 'a1) -> sigma -> 'a1
18
19val sigma_rect_Type3 : (__ -> __ -> 'a1) -> sigma -> 'a1
20
21val sigma_rect_Type2 : (__ -> __ -> 'a1) -> sigma -> 'a1
22
23val sigma_rect_Type1 : (__ -> __ -> 'a1) -> sigma -> 'a1
24
25val sigma_rect_Type0 : (__ -> __ -> 'a1) -> sigma -> 'a1
26
27val sigma_inv_rect_Type4 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1
28
29val sigma_inv_rect_Type3 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1
30
31val sigma_inv_rect_Type2 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1
32
33val sigma_inv_rect_Type1 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1
34
35val sigma_inv_rect_Type0 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1
36
37type p1 = __
38
39val p2 : sigma -> p1
40
41val jmeq_rect_Type4 : 'a1 -> 'a2 -> 'a3 -> 'a2
42
43val jmeq_rect_Type5 : 'a1 -> 'a2 -> 'a3 -> 'a2
44
45val jmeq_rect_Type3 : 'a1 -> 'a2 -> 'a3 -> 'a2
46
47val jmeq_rect_Type2 : 'a1 -> 'a2 -> 'a3 -> 'a2
48
49val jmeq_rect_Type1 : 'a1 -> 'a2 -> 'a3 -> 'a2
50
51val jmeq_rect_Type0 : 'a1 -> 'a2 -> 'a3 -> 'a2
52
53val jmeq_inv_rect_Type4 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3
54
55val jmeq_inv_rect_Type3 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3
56
57val jmeq_inv_rect_Type2 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3
58
59val jmeq_inv_rect_Type1 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3
60
61val jmeq_inv_rect_Type0 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3
62
63val jmeq_discr : 'a1 -> 'a2 -> __
64
65val cast : 'a1 -> 'a2
66
67type ('a, 'x) curry = 'x
68
69val g : 'a1 -> 'a2 -> 'a1 -> 'a2
70
71type 'p pP = 'p
72
73val e : 'a1 -> 'a2 pP -> 'a1 -> 'a2 pP
74
75val jmeq_elim : 'a1 -> 'a2 -> 'a1 -> 'a2
76
Note: See TracBrowser for help on using the repository browser.