|
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:
- 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.
- 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.2 KB
|
| Line | |
|---|
| 1 | open Preamble |
|---|
| 2 | |
|---|
| 3 | open Core_notation |
|---|
| 4 | |
|---|
| 5 | open Pts |
|---|
| 6 | |
|---|
| 7 | open Hints_declaration |
|---|
| 8 | |
|---|
| 9 | open Logic |
|---|
| 10 | |
|---|
| 11 | open Types |
|---|
| 12 | |
|---|
| 13 | open Relations |
|---|
| 14 | |
|---|
| 15 | type setoid = |
|---|
| 16 | | Mk_Setoid |
|---|
| 17 | |
|---|
| 18 | val setoid_rect_Type4 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 |
|---|
| 19 | |
|---|
| 20 | val setoid_rect_Type5 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 |
|---|
| 21 | |
|---|
| 22 | val setoid_rect_Type3 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 |
|---|
| 23 | |
|---|
| 24 | val setoid_rect_Type2 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 |
|---|
| 25 | |
|---|
| 26 | val setoid_rect_Type1 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 |
|---|
| 27 | |
|---|
| 28 | val setoid_rect_Type0 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 |
|---|
| 29 | |
|---|
| 30 | type std_supp |
|---|
| 31 | |
|---|
| 32 | type std_eq = __ |
|---|
| 33 | |
|---|
| 34 | val setoid_inv_rect_Type4 : |
|---|
| 35 | setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 |
|---|
| 36 | |
|---|
| 37 | val setoid_inv_rect_Type3 : |
|---|
| 38 | setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 |
|---|
| 39 | |
|---|
| 40 | val setoid_inv_rect_Type2 : |
|---|
| 41 | setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 |
|---|
| 42 | |
|---|
| 43 | val setoid_inv_rect_Type1 : |
|---|
| 44 | setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 |
|---|
| 45 | |
|---|
| 46 | val setoid_inv_rect_Type0 : |
|---|
| 47 | setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 |
|---|
| 48 | |
|---|
| 49 | val as_std : setoid |
|---|
| 50 | |
|---|
| 51 | val std_prod : setoid -> setoid -> setoid |
|---|
| 52 | |
|---|
| 53 | val std_union : setoid -> setoid -> setoid |
|---|
| 54 | |
|---|
Note: See
TracBrowser
for help on using the repository browser.
