source: extracted/nat.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: 3.2 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Relations
12
13type nat =
14| O
15| S of nat
16
17(** val nat_rect_Type4 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
18let rec nat_rect_Type4 h_O h_S = function
19| O -> h_O
20| S x_565 -> h_S x_565 (nat_rect_Type4 h_O h_S x_565)
21
22(** val nat_rect_Type3 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
23let rec nat_rect_Type3 h_O h_S = function
24| O -> h_O
25| S x_573 -> h_S x_573 (nat_rect_Type3 h_O h_S x_573)
26
27(** val nat_rect_Type2 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
28let rec nat_rect_Type2 h_O h_S = function
29| O -> h_O
30| S x_577 -> h_S x_577 (nat_rect_Type2 h_O h_S x_577)
31
32(** val nat_rect_Type1 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
33let rec nat_rect_Type1 h_O h_S = function
34| O -> h_O
35| S x_581 -> h_S x_581 (nat_rect_Type1 h_O h_S x_581)
36
37(** val nat_rect_Type0 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
38let rec nat_rect_Type0 h_O h_S = function
39| O -> h_O
40| S x_585 -> h_S x_585 (nat_rect_Type0 h_O h_S x_585)
41
42(** val nat_inv_rect_Type4 :
43    nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
44let nat_inv_rect_Type4 hterm h1 h2 =
45  let hcut = nat_rect_Type4 h1 h2 hterm in hcut __
46
47(** val nat_inv_rect_Type3 :
48    nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
49let nat_inv_rect_Type3 hterm h1 h2 =
50  let hcut = nat_rect_Type3 h1 h2 hterm in hcut __
51
52(** val nat_inv_rect_Type2 :
53    nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
54let nat_inv_rect_Type2 hterm h1 h2 =
55  let hcut = nat_rect_Type2 h1 h2 hterm in hcut __
56
57(** val nat_inv_rect_Type1 :
58    nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
59let nat_inv_rect_Type1 hterm h1 h2 =
60  let hcut = nat_rect_Type1 h1 h2 hterm in hcut __
61
62(** val nat_inv_rect_Type0 :
63    nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
64let nat_inv_rect_Type0 hterm h1 h2 =
65  let hcut = nat_rect_Type0 h1 h2 hterm in hcut __
66
67(** val nat_discr : nat -> nat -> __ **)
68let nat_discr x y =
69  Logic.eq_rect_Type2 x
70    (match x with
71     | O -> Obj.magic (fun _ dH -> dH)
72     | S a0 -> Obj.magic (fun _ dH -> dH __)) y
73
74(** val pred : nat -> nat **)
75let pred = function
76| O -> O
77| S p -> p
78
79(** val plus : nat -> nat -> nat **)
80let rec plus n m =
81  match n with
82  | O -> m
83  | S p -> S (plus p m)
84
85(** val times : nat -> nat -> nat **)
86let rec times n m =
87  match n with
88  | O -> O
89  | S p -> plus m (times p m)
90
91(** val minus : nat -> nat -> nat **)
92let rec minus n m =
93  match n with
94  | O -> O
95  | S p ->
96    (match m with
97     | O -> S p
98     | S q -> minus p q)
99
100open Bool
101
102(** val eqb : nat -> nat -> Bool.bool **)
103let rec eqb n m =
104  match n with
105  | O ->
106    (match m with
107     | O -> Bool.True
108     | S q -> Bool.False)
109  | S p ->
110    (match m with
111     | O -> Bool.False
112     | S q -> eqb p q)
113
114(** val leb : nat -> nat -> Bool.bool **)
115let rec leb n m =
116  match n with
117  | O -> Bool.True
118  | S p ->
119    (match m with
120     | O -> Bool.False
121     | S q -> leb p q)
122
123(** val min : nat -> nat -> nat **)
124let min n m =
125  match leb n m with
126  | Bool.True -> n
127  | Bool.False -> m
128
129(** val max : nat -> nat -> nat **)
130let max n m =
131  match leb n m with
132  | Bool.True -> m
133  | Bool.False -> n
134
Note: See TracBrowser for help on using the repository browser.