source: driver/extracted/div_and_mod.ml @ 3106

Last change on this file since 3106 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.4 KB
Line 
1open Preamble
2
3open Bool
4
5open Hints_declaration
6
7open Core_notation
8
9open Pts
10
11open Logic
12
13open Relations
14
15open Nat
16
17(** val mod_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat **)
18let rec mod_aux p m n =
19  match p with
20  | Nat.O -> m
21  | Nat.S q ->
22    (match Nat.leb m n with
23     | Bool.True -> m
24     | Bool.False -> mod_aux q (Nat.minus m (Nat.S n)) n)
25
26(** val mod0 : Nat.nat -> Nat.nat -> Nat.nat **)
27let mod0 n = function
28| Nat.O -> n
29| Nat.S p -> mod_aux n n p
30
31(** val div_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat **)
32let rec div_aux p m n =
33  match p with
34  | Nat.O -> Nat.O
35  | Nat.S q ->
36    (match Nat.leb m n with
37     | Bool.True -> Nat.O
38     | Bool.False -> Nat.S (div_aux q (Nat.minus m (Nat.S n)) n))
39
40(** val div : Nat.nat -> Nat.nat -> Nat.nat **)
41let div n = function
42| Nat.O -> Nat.S n
43| Nat.S p -> div_aux n n p
44
45(** val div_mod_spec_rect_Type4 :
46    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
47let rec div_mod_spec_rect_Type4 n m q r h_div_mod_spec_intro =
48  h_div_mod_spec_intro __ __
49
50(** val div_mod_spec_rect_Type5 :
51    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
52let rec div_mod_spec_rect_Type5 n m q r h_div_mod_spec_intro =
53  h_div_mod_spec_intro __ __
54
55(** val div_mod_spec_rect_Type3 :
56    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
57let rec div_mod_spec_rect_Type3 n m q r h_div_mod_spec_intro =
58  h_div_mod_spec_intro __ __
59
60(** val div_mod_spec_rect_Type2 :
61    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
62let rec div_mod_spec_rect_Type2 n m q r h_div_mod_spec_intro =
63  h_div_mod_spec_intro __ __
64
65(** val div_mod_spec_rect_Type1 :
66    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
67let rec div_mod_spec_rect_Type1 n m q r h_div_mod_spec_intro =
68  h_div_mod_spec_intro __ __
69
70(** val div_mod_spec_rect_Type0 :
71    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
72let rec div_mod_spec_rect_Type0 n m q r h_div_mod_spec_intro =
73  h_div_mod_spec_intro __ __
74
75(** val div_mod_spec_inv_rect_Type4 :
76    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) ->
77    'a1 **)
78let div_mod_spec_inv_rect_Type4 x1 x2 x3 x4 h1 =
79  let hcut = div_mod_spec_rect_Type4 x1 x2 x3 x4 h1 in hcut __
80
81(** val div_mod_spec_inv_rect_Type3 :
82    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) ->
83    'a1 **)
84let div_mod_spec_inv_rect_Type3 x1 x2 x3 x4 h1 =
85  let hcut = div_mod_spec_rect_Type3 x1 x2 x3 x4 h1 in hcut __
86
87(** val div_mod_spec_inv_rect_Type2 :
88    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) ->
89    'a1 **)
90let div_mod_spec_inv_rect_Type2 x1 x2 x3 x4 h1 =
91  let hcut = div_mod_spec_rect_Type2 x1 x2 x3 x4 h1 in hcut __
92
93(** val div_mod_spec_inv_rect_Type1 :
94    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) ->
95    'a1 **)
96let div_mod_spec_inv_rect_Type1 x1 x2 x3 x4 h1 =
97  let hcut = div_mod_spec_rect_Type1 x1 x2 x3 x4 h1 in hcut __
98
99(** val div_mod_spec_inv_rect_Type0 :
100    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) ->
101    'a1 **)
102let div_mod_spec_inv_rect_Type0 x1 x2 x3 x4 h1 =
103  let hcut = div_mod_spec_rect_Type0 x1 x2 x3 x4 h1 in hcut __
104
105(** val div_mod_spec_discr :
106    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> __ **)
107let div_mod_spec_discr a1 a2 a3 a4 =
108  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
109
Note: See TracBrowser for help on using the repository browser.