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.6 KB

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  let eq_rect_Type0_r1 a p x0 = 

31  Logic.eq_rect_r a x0 p 

32  

33  (** val eq_rect_r2 : 'a1 > 'a1 > 'a2 > 'a2 **) 

34  let eq_rect_r2 a x x0 = 

35  (fun _ h > h) __ x0 

36  

37  (** val eq_rect_Type2_r0 : 'a1 > 'a2 > 'a1 > 'a2 **) 

38  let eq_rect_Type2_r0 a p x0 = 

39  eq_rect_r2 a x0 p 

40  

41  (** val dec_bounded_forall : 

42  (Nat.nat > (__, __) Types.sum) > Nat.nat > (__, __) Types.sum **) 

43  let dec_bounded_forall hP_dec k = 

44  Nat.nat_rect_Type0 (Types.Inl __) (fun k0 hind > 

45  match hind with 

46   Types.Inl _ > 

47  (match hP_dec k0 with 

48   Types.Inl _ > Types.Inl __ 

49   Types.Inr _ > Types.Inr __) 

50   Types.Inr _ > Types.Inr __) k 

51  

52  (** val dec_bounded_exists : 

53  (Nat.nat > (__, __) Types.sum) > Nat.nat > (__, __) Types.sum **) 

54  let dec_bounded_exists hP_dec k = 

55  Nat.nat_rect_Type0 (Types.Inr __) (fun k0 hind > 

56  match hind with 

57   Types.Inl _ > Types.Inl __ 

58   Types.Inr _ > 

59  (match hP_dec k0 with 

60   Types.Inl _ > Types.Inl __ 

61   Types.Inr _ > Types.Inr __)) k 

62  

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

64  let dec_true f h = 

65  match f with 

66   Types.Inl x > h x 

67   Types.Inr _ > assert false (* absurd case *) 

68  

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

70  let dec_false f h = 

71  match f with 

72   Types.Inl _ > assert false (* absurd case *) 

73   Types.Inr x > h x 

74  

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