source: extracted/extranat.mli @ 2601

Last change on this file since 2601 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.3 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Bool
14
15open Relations
16
17open Nat
18
19type nat_compared =
20| Nat_lt of Nat.nat * Nat.nat
21| Nat_eq of Nat.nat
22| Nat_gt of Nat.nat * Nat.nat
23
24val nat_compared_rect_Type4 :
25  (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
26  'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
27
28val nat_compared_rect_Type5 :
29  (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
30  'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
31
32val nat_compared_rect_Type3 :
33  (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
34  'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
35
36val nat_compared_rect_Type2 :
37  (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
38  'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
39
40val nat_compared_rect_Type1 :
41  (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
42  'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
43
44val nat_compared_rect_Type0 :
45  (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
46  'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
47
48val nat_compared_inv_rect_Type4 :
49  Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
50  'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __ ->
51  'a1) -> 'a1
52
53val nat_compared_inv_rect_Type3 :
54  Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
55  'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __ ->
56  'a1) -> 'a1
57
58val nat_compared_inv_rect_Type2 :
59  Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
60  'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __ ->
61  'a1) -> 'a1
62
63val nat_compared_inv_rect_Type1 :
64  Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
65  'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __ ->
66  'a1) -> 'a1
67
68val nat_compared_inv_rect_Type0 :
69  Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
70  'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __ ->
71  'a1) -> 'a1
72
73val nat_compared_discr :
74  Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __
75
76val nat_compare : Nat.nat -> Nat.nat -> nat_compared
77
78val eq_nat_dec : Nat.nat -> Nat.nat -> (__, __) Types.sum
79
Note: See TracBrowser for help on using the repository browser.