blob: a3a4d45c13abae8043be45a5e06b0e2064d2598c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Extraction to Ocaml: conversion from/to [int]
Nota: no check that [int] values aren't generating overflows *)
Require Coq.extraction.Extraction.
Require Import Arith ZArith.
Parameter int : Type.
Parameter int_zero : int.
Parameter int_succ : int -> int.
Parameter int_opp : int -> int.
Parameter int_twice : int -> int.
Extract Inlined Constant int => int.
Extract Inlined Constant int_zero => "0".
Extract Inlined Constant int_succ => "succ".
Extract Inlined Constant int_opp => "-".
Extract Inlined Constant int_twice => "2 *".
Definition int_of_nat : nat -> int :=
(fix loop acc n :=
match n with
| O => acc
| S n => loop (int_succ acc) n
end) int_zero.
Fixpoint int_of_pos p :=
match p with
| xH => int_succ int_zero
| xO p => int_twice (int_of_pos p)
| xI p => int_succ (int_twice (int_of_pos p))
end.
Fixpoint int_of_z z :=
match z with
| Z0 => int_zero
| Zpos p => int_of_pos p
| Zneg p => int_opp (int_of_pos p)
end.
Fixpoint int_of_n n :=
match n with
| N0 => int_zero
| Npos p => int_of_pos p
end.
(** NB: as for [pred] or [minus], [nat_of_int], [n_of_int] and
[pos_of_int] are total and return zero (resp. one) for
non-positive inputs. *)
Parameter int_natlike_rec : forall A, A -> (A->A) -> int -> A.
Extract Constant int_natlike_rec =>
"fun fO fS ->
let rec loop acc i = if i <= 0 then acc else loop (fS acc) (i-1)
in loop fO".
Definition nat_of_int : int -> nat := int_natlike_rec _ O S.
Parameter int_poslike_rec : forall A, A -> (A->A) -> (A->A) -> int -> A.
Extract Constant int_poslike_rec =>
"fun f1 f2x f2x1 ->
let rec loop i = if i <= 1 then f1 else
if i land 1 = 0 then f2x (loop (i lsr 1)) else f2x1 (loop (i lsr 1))
in loop".
Definition pos_of_int : int -> positive := int_poslike_rec _ xH xO xI.
Parameter int_zlike_case : forall A, A -> (int->A) -> (int->A) -> int -> A.
Extract Constant int_zlike_case =>
"fun f0 fpos fneg i ->
if i = 0 then f0 else if i>0 then fpos i else fneg (-i)".
Definition z_of_int : int -> Z :=
int_zlike_case _ Z0 (fun i => Zpos (pos_of_int i))
(fun i => Zneg (pos_of_int i)).
Definition n_of_int : int -> N :=
int_zlike_case _ N0 (fun i => Npos (pos_of_int i)) (fun _ => N0).
(** Warning: [z_of_int] is currently wrong for Ocaml's [min_int],
since [min_int] has no positive opposite ([-min_int = min_int]).
*)
(*
Extraction "/tmp/test.ml"
nat_of_int int_of_nat
pos_of_int int_of_pos
z_of_int int_of_z
n_of_int int_of_n.
*)
|
