Last change
on this file since 2960 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

Rev  Line  

[2601]  1  open Preamble 

 2  

 3  open Hints_declaration 

 4  

 5  open Core_notation 

 6  

 7  open Pts 

 8  

 9  open Logic 

 10  

 11  open Relations 

 12  

 13  type nat = 

 14   O 

 15   S of nat 

 16  

 17  val nat_rect_Type4 : 'a1 > (nat > 'a1 > 'a1) > nat > 'a1 

 18  

 19  val nat_rect_Type3 : 'a1 > (nat > 'a1 > 'a1) > nat > 'a1 

 20  

 21  val nat_rect_Type2 : 'a1 > (nat > 'a1 > 'a1) > nat > 'a1 

 22  

 23  val nat_rect_Type1 : 'a1 > (nat > 'a1 > 'a1) > nat > 'a1 

 24  

 25  val nat_rect_Type0 : 'a1 > (nat > 'a1 > 'a1) > nat > 'a1 

 26  

 27  val nat_inv_rect_Type4 : 

 28  nat > (__ > 'a1) > (nat > (__ > 'a1) > __ > 'a1) > 'a1 

 29  

 30  val nat_inv_rect_Type3 : 

 31  nat > (__ > 'a1) > (nat > (__ > 'a1) > __ > 'a1) > 'a1 

 32  

 33  val nat_inv_rect_Type2 : 

 34  nat > (__ > 'a1) > (nat > (__ > 'a1) > __ > 'a1) > 'a1 

 35  

 36  val nat_inv_rect_Type1 : 

 37  nat > (__ > 'a1) > (nat > (__ > 'a1) > __ > 'a1) > 'a1 

 38  

 39  val nat_inv_rect_Type0 : 

 40  nat > (__ > 'a1) > (nat > (__ > 'a1) > __ > 'a1) > 'a1 

 41  

 42  val nat_discr : nat > nat > __ 

 43  

 44  val pred : nat > nat 

 45  

 46  val plus : nat > nat > nat 

 47  

 48  val times : nat > nat > nat 

 49  

 50  val minus : nat > nat > nat 

 51  

 52  open Bool 

 53  

 54  val eqb : nat > nat > Bool.bool 

 55  

 56  val leb : nat > nat > Bool.bool 

 57  

 58  val min : nat > nat > nat 

 59  

 60  val max : nat > nat > nat 

 61  

Note: See
TracBrowser
for help on using the repository browser.