Last change
on this file since 2731 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:
637 bytes

Line  

1  open Preamble 

2  

3  open Hints_declaration 

4  

5  open Core_notation 

6  

7  open Pts 

8  

9  open Logic 

10  

11  open Types 

12  

13  open Bool 

14  

15  open Relations 

16  

17  open Nat 

18  

19  open List 

20  

21  open Div_and_mod 

22  

23  open Jmeq 

24  

25  open Russell 

26  

27  open Util 

28  

29  val eq_rect_Type0_r1 : 'a1 > 'a2 > 'a1 > 'a2 

30  

31  val eq_rect_r2 : 'a1 > 'a1 > 'a2 > 'a2 

32  

33  val eq_rect_Type2_r0 : 'a1 > 'a2 > 'a1 > 'a2 

34  

35  val dec_bounded_forall : 

36  (Nat.nat > (__, __) Types.sum) > Nat.nat > (__, __) Types.sum 

37  

38  val dec_bounded_exists : 

39  (Nat.nat > (__, __) Types.sum) > Nat.nat > (__, __) Types.sum 

40  

41  val dec_true : (__, __) Types.sum > (__ > 'a1) > 'a1 

42  

43  val dec_false : (__, __) Types.sum > (__ > 'a1) > 'a1 

44  

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