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
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pcoq
open Pp
open Util
open Names
open Topconstr
open Libnames
open Bigint
exception Non_closed_number
(**********************************************************************)
(* Parsing positive via scopes *)
(**********************************************************************)
open Libnames
open Glob_term
let binnums = ["Coq";"Numbers";"BinNums"]
let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
let positive_path = make_path binnums "positive"
(* TODO: temporary hack *)
let make_kn dir id = Libnames.encode_mind dir id
let positive_kn = make_kn (make_dir binnums) (id_of_string "positive")
let glob_positive = IndRef (positive_kn,0)
let path_of_xI = ((positive_kn,0),1)
let path_of_xO = ((positive_kn,0),2)
let path_of_xH = ((positive_kn,0),3)
let glob_xI = ConstructRef path_of_xI
let glob_xO = ConstructRef path_of_xO
let glob_xH = ConstructRef path_of_xH
let pos_of_bignat dloc x =
let ref_xI = GRef (dloc, glob_xI) in
let ref_xH = GRef (dloc, glob_xH) in
let ref_xO = GRef (dloc, glob_xO) in
let rec pos_of x =
match div2_with_rest x with
| (q,false) -> GApp (dloc, ref_xO,[pos_of q])
| (q,true) when q <> zero -> GApp (dloc,ref_xI,[pos_of q])
| (q,true) -> ref_xH
in
pos_of x
let error_non_positive dloc =
user_err_loc (dloc, "interp_positive",
str "Only strictly positive numbers in type \"positive\".")
let interp_positive dloc n =
if is_strictly_pos n then pos_of_bignat dloc n
else error_non_positive dloc
(**********************************************************************)
(* Printing positive via scopes *)
(**********************************************************************)
let rec bignat_of_pos = function
| GApp (_, GRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a)
| GApp (_, GRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a))
| GRef (_, a) when a = glob_xH -> Bigint.one
| _ -> raise Non_closed_number
let uninterp_positive p =
try
Some (bignat_of_pos p)
with Non_closed_number ->
None
(************************************************************************)
(* Declaring interpreters and uninterpreters for positive *)
(************************************************************************)
let _ = Notation.declare_numeral_interpreter "positive_scope"
(positive_path,binnums)
interp_positive
([GRef (dummy_loc, glob_xI);
GRef (dummy_loc, glob_xO);
GRef (dummy_loc, glob_xH)],
uninterp_positive,
true)
(**********************************************************************)
(* Parsing N via scopes *)
(**********************************************************************)
let n_kn = make_kn (make_dir binnums) (id_of_string "N")
let glob_n = IndRef (n_kn,0)
let path_of_N0 = ((n_kn,0),1)
let path_of_Npos = ((n_kn,0),2)
let glob_N0 = ConstructRef path_of_N0
let glob_Npos = ConstructRef path_of_Npos
let n_path = make_path binnums "N"
let n_of_binnat dloc pos_or_neg n =
if n <> zero then
GApp(dloc, GRef (dloc,glob_Npos), [pos_of_bignat dloc n])
else
GRef (dloc, glob_N0)
let error_negative dloc =
user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".")
let n_of_int dloc n =
if is_pos_or_zero n then n_of_binnat dloc true n
else error_negative dloc
(**********************************************************************)
(* Printing N via scopes *)
(**********************************************************************)
let bignat_of_n = function
| GApp (_, GRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a
| GRef (_, a) when a = glob_N0 -> Bigint.zero
| _ -> raise Non_closed_number
let uninterp_n p =
try Some (bignat_of_n p)
with Non_closed_number -> None
(************************************************************************)
(* Declaring interpreters and uninterpreters for N *)
let _ = Notation.declare_numeral_interpreter "N_scope"
(n_path,binnums)
n_of_int
([GRef (dummy_loc, glob_N0);
GRef (dummy_loc, glob_Npos)],
uninterp_n,
true)
(**********************************************************************)
(* Parsing Z via scopes *)
(**********************************************************************)
let z_path = make_path binnums "Z"
let z_kn = make_kn (make_dir binnums) (id_of_string "Z")
let glob_z = IndRef (z_kn,0)
let path_of_ZERO = ((z_kn,0),1)
let path_of_POS = ((z_kn,0),2)
let path_of_NEG = ((z_kn,0),3)
let glob_ZERO = ConstructRef path_of_ZERO
let glob_POS = ConstructRef path_of_POS
let glob_NEG = ConstructRef path_of_NEG
let z_of_int dloc n =
if n <> zero then
let sgn, n =
if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
GApp(dloc, GRef (dloc,sgn), [pos_of_bignat dloc n])
else
GRef (dloc, glob_ZERO)
(**********************************************************************)
(* Printing Z via scopes *)
(**********************************************************************)
let bigint_of_z = function
| GApp (_, GRef (_,b),[a]) when b = glob_POS -> bignat_of_pos a
| GApp (_, GRef (_,b),[a]) when b = glob_NEG -> Bigint.neg (bignat_of_pos a)
| GRef (_, a) when a = glob_ZERO -> Bigint.zero
| _ -> raise Non_closed_number
let uninterp_z p =
try
Some (bigint_of_z p)
with Non_closed_number -> None
(************************************************************************)
(* Declaring interpreters and uninterpreters for Z *)
let _ = Notation.declare_numeral_interpreter "Z_scope"
(z_path,binnums)
z_of_int
([GRef (dummy_loc, glob_ZERO);
GRef (dummy_loc, glob_POS);
GRef (dummy_loc, glob_NEG)],
uninterp_z,
true)
|
