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:
964 bytes

Line  

1  open Preamble 

2  

3  open Bool 

4  

5  open Relations 

6  

7  open Nat 

8  

9  open Hints_declaration 

10  

11  open Core_notation 

12  

13  open Pts 

14  

15  open Logic 

16  

17  open Types 

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 all0 : ('a1 > Bool.bool) > 'a1 List.list > Bool.bool 

30  

31  type all2 = __ 

32  

33  val map_All : ('a1 > __ > 'a2) > 'a1 List.list > 'a2 List.list 

34  

35  open Setoids 

36  

37  open Monad 

38  

39  open Option 

40  

41  val append0 : 'a1 List.list List.aop 

42  

43  val list0 : Monad.monadProps 

44  

45  val count : ('a1 > Bool.bool) > 'a1 List.list > Nat.nat 

46  

47  val position_of_safe : ('a1 > Bool.bool) > 'a1 List.list > Nat.nat 

48  

49  val index_of : ('a1 > Bool.bool) > 'a1 List.list > Nat.nat 

50  

51  val ordered_insert : 

52  ('a1 > 'a1 > Bool.bool) > 'a1 > 'a1 List.list > 'a1 List.list 

53  

54  val insert_sort : ('a1 > 'a1 > Bool.bool) > 'a1 List.list > 'a1 List.list 

55  

56  val range_strong_internal : 

57  Nat.nat > Nat.nat > Nat.nat > Nat.nat Types.sig0 List.list 

58  

59  val range_strong : Nat.nat > Nat.nat Types.sig0 List.list 

60  

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