source: extracted/extranat.ml @ 2746

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:

  1. 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.
  2. 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: 5.1 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Bool
14
15open Relations
16
17open Nat
18
19type nat_compared =
20| Nat_lt of Nat.nat * Nat.nat
21| Nat_eq of Nat.nat
22| Nat_gt of Nat.nat * Nat.nat
23
24(** val nat_compared_rect_Type4 :
25    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
26    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
27let rec nat_compared_rect_Type4 h_nat_lt h_nat_eq h_nat_gt x_723 x_722 = function
28| Nat_lt (n, m) -> h_nat_lt n m
29| Nat_eq n -> h_nat_eq n
30| Nat_gt (n, m) -> h_nat_gt n m
31
32(** val nat_compared_rect_Type5 :
33    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
34    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
35let rec nat_compared_rect_Type5 h_nat_lt h_nat_eq h_nat_gt x_729 x_728 = function
36| Nat_lt (n, m) -> h_nat_lt n m
37| Nat_eq n -> h_nat_eq n
38| Nat_gt (n, m) -> h_nat_gt n m
39
40(** val nat_compared_rect_Type3 :
41    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
42    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
43let rec nat_compared_rect_Type3 h_nat_lt h_nat_eq h_nat_gt x_735 x_734 = function
44| Nat_lt (n, m) -> h_nat_lt n m
45| Nat_eq n -> h_nat_eq n
46| Nat_gt (n, m) -> h_nat_gt n m
47
48(** val nat_compared_rect_Type2 :
49    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
50    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
51let rec nat_compared_rect_Type2 h_nat_lt h_nat_eq h_nat_gt x_741 x_740 = function
52| Nat_lt (n, m) -> h_nat_lt n m
53| Nat_eq n -> h_nat_eq n
54| Nat_gt (n, m) -> h_nat_gt n m
55
56(** val nat_compared_rect_Type1 :
57    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
58    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
59let rec nat_compared_rect_Type1 h_nat_lt h_nat_eq h_nat_gt x_747 x_746 = function
60| Nat_lt (n, m) -> h_nat_lt n m
61| Nat_eq n -> h_nat_eq n
62| Nat_gt (n, m) -> h_nat_gt n m
63
64(** val nat_compared_rect_Type0 :
65    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
66    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
67let rec nat_compared_rect_Type0 h_nat_lt h_nat_eq h_nat_gt x_753 x_752 = function
68| Nat_lt (n, m) -> h_nat_lt n m
69| Nat_eq n -> h_nat_eq n
70| Nat_gt (n, m) -> h_nat_gt n m
71
72(** val nat_compared_inv_rect_Type4 :
73    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
74    'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __
75    -> 'a1) -> 'a1 **)
76let nat_compared_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
77  let hcut = nat_compared_rect_Type4 h1 h2 h3 x1 x2 hterm in hcut __ __
78
79(** val nat_compared_inv_rect_Type3 :
80    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
81    'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __
82    -> 'a1) -> 'a1 **)
83let nat_compared_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
84  let hcut = nat_compared_rect_Type3 h1 h2 h3 x1 x2 hterm in hcut __ __
85
86(** val nat_compared_inv_rect_Type2 :
87    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
88    'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __
89    -> 'a1) -> 'a1 **)
90let nat_compared_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
91  let hcut = nat_compared_rect_Type2 h1 h2 h3 x1 x2 hterm in hcut __ __
92
93(** val nat_compared_inv_rect_Type1 :
94    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
95    'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __
96    -> 'a1) -> 'a1 **)
97let nat_compared_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
98  let hcut = nat_compared_rect_Type1 h1 h2 h3 x1 x2 hterm in hcut __ __
99
100(** val nat_compared_inv_rect_Type0 :
101    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
102    'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __
103    -> 'a1) -> 'a1 **)
104let nat_compared_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
105  let hcut = nat_compared_rect_Type0 h1 h2 h3 x1 x2 hterm in hcut __ __
106
107(** val nat_compared_discr :
108    Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __ **)
109let nat_compared_discr a1 a2 x y =
110  Logic.eq_rect_Type2 x
111    (match x with
112     | Nat_lt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
113     | Nat_eq a0 -> Obj.magic (fun _ dH -> dH __)
114     | Nat_gt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
115
116(** val nat_compare : Nat.nat -> Nat.nat -> nat_compared **)
117let rec nat_compare n m =
118  match n with
119  | Nat.O ->
120    (match m with
121     | Nat.O -> Nat_eq Nat.O
122     | Nat.S m' -> Nat_lt (Nat.O, m'))
123  | Nat.S n' ->
124    (match m with
125     | Nat.O -> Nat_gt (n', Nat.O)
126     | Nat.S m' ->
127       (match nat_compare n' m' with
128        | Nat_lt (x, y) -> Nat_lt ((Nat.S x), y)
129        | Nat_eq x -> Nat_eq (Nat.S x)
130        | Nat_gt (x, y) -> Nat_gt (x, (Nat.S y))))
131
132(** val eq_nat_dec : Nat.nat -> Nat.nat -> (__, __) Types.sum **)
133let rec eq_nat_dec n m =
134  match n with
135  | Nat.O ->
136    (match m with
137     | Nat.O -> Types.Inl __
138     | Nat.S m' -> Types.Inr __)
139  | Nat.S n' ->
140    (match m with
141     | Nat.O -> Types.Inr __
142     | Nat.S m' ->
143       (match eq_nat_dec n' m' with
144        | Types.Inl _ -> Types.Inl __
145        | Types.Inr _ -> Types.Inr __))
146
Note: See TracBrowser for help on using the repository browser.