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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Coqast
open Pcoq
open Pp
open Util
open Names
open Ast
open Extend
open Topconstr
open Libnames
open Bignat
(**********************************************************************)
(* Parsing positive via scopes *)
(**********************************************************************)
open Libnames
open Rawterm
let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
let fast_integer_module = make_dir ["Coq";"ZArith";"fast_integer"]
(* TODO: temporary hack *)
let make_path dir id = Libnames.encode_kn dir id
let positive_path = make_path fast_integer_module (id_of_string "positive")
let path_of_xI = ((positive_path,0),1)
let path_of_xO = ((positive_path,0),2)
let path_of_xH = ((positive_path,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 = RRef (dloc, glob_xI) in
let ref_xH = RRef (dloc, glob_xH) in
let ref_xO = RRef (dloc, glob_xO) in
let rec pos_of x =
match div2_with_rest x with
| (q,false) -> RApp (dloc, ref_xO,[pos_of q])
| (q,true) when is_nonzero q -> RApp (dloc,ref_xI,[pos_of q])
| (q,true) -> ref_xH
in
pos_of x
let interp_positive dloc = function
| POS n when is_nonzero n -> pos_of_bignat dloc n
| _ ->
user_err_loc (dloc, "interp_positive",
str "Only strictly positive numbers in type \"positive\"!")
let rec pat_pos_of_bignat dloc x name =
match div2_with_rest x with
| (q,false) ->
PatCstr (dloc,path_of_xO,[pat_pos_of_bignat dloc q Anonymous],name)
| (q,true) when is_nonzero q ->
PatCstr (dloc,path_of_xI,[pat_pos_of_bignat dloc q Anonymous],name)
| (q,true) ->
PatCstr (dloc,path_of_xH,[],name)
let pat_interp_positive dloc = function
| POS n -> pat_pos_of_bignat dloc n
| NEG n ->
user_err_loc (dloc, "interp_positive",
str "No negative number in type \"positive\"!")
(**********************************************************************)
(* Printing positive via scopes *)
(**********************************************************************)
exception Non_closed_number
let rec bignat_of_pos = function
| RApp (_, RRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a)
| RApp (_, RRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a))
| RRef (_, a) when a = glob_xH -> Bignat.one
| _ -> raise Non_closed_number
let uninterp_positive p =
try
Some (POS (bignat_of_pos p))
with Non_closed_number ->
None
(***********************************************************************)
(* Declaring interpreters and uninterpreters for positive *)
(***********************************************************************)
let _ = Symbols.declare_numeral_interpreter "positive_scope"
["Coq";"ZArith";"fast_integer"]
(interp_positive,Some pat_interp_positive)
([RRef (dummy_loc, glob_xI);
RRef (dummy_loc, glob_xO);
RRef (dummy_loc, glob_xH)],
uninterp_positive,
None)
(**********************************************************************)
(* Parsing Z via scopes *)
(**********************************************************************)
let z_path = make_path fast_integer_module (id_of_string "Z")
let glob_z = IndRef (z_path,0)
let path_of_ZERO = ((z_path,0),1)
let path_of_POS = ((z_path,0),2)
let path_of_NEG = ((z_path,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_posint dloc pos_or_neg n =
if is_nonzero n then
let sgn = if pos_or_neg then glob_POS else glob_NEG in
RApp(dloc, RRef (dloc,sgn), [pos_of_bignat dloc n])
else
RRef (dloc, glob_ZERO)
let z_of_int dloc z =
match z with
| POS n -> z_of_posint dloc true n
| NEG n -> z_of_posint dloc false n
let pat_z_of_posint dloc pos_or_neg n name =
if is_nonzero n then
let sgn = if pos_or_neg then path_of_POS else path_of_NEG in
PatCstr (dloc, sgn, [pat_pos_of_bignat dloc n Anonymous], name)
else
PatCstr (dloc, path_of_ZERO, [], name)
let pat_z_of_int dloc n name =
match n with
| POS n -> pat_z_of_posint dloc true n name
| NEG n -> pat_z_of_posint dloc false n name
(**********************************************************************)
(* Printing Z via scopes *)
(**********************************************************************)
let bigint_of_z = function
| RApp (_, RRef (_,b),[a]) when b = glob_POS -> POS (bignat_of_pos a)
| RApp (_, RRef (_,b),[a]) when b = glob_NEG -> NEG (bignat_of_pos a)
| RRef (_, a) when a = glob_ZERO -> POS (Bignat.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 _ = Symbols.declare_numeral_interpreter "Z_scope"
["Coq";"ZArith";"fast_integer"]
(z_of_int,Some pat_z_of_int)
([RRef (dummy_loc, glob_ZERO);
RRef (dummy_loc, glob_POS);
RRef (dummy_loc, glob_NEG)],
uninterp_z,
None)
|
