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
|
(***********************************************************************)
(* 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
let get_z_sign loc =
let ast_of_id id = Astterm.globalize_constr (Nvar(loc,id)) in
((ast_of_id "xI", ast_of_id "xO", ast_of_id "xH"),
(ast_of_id "ZERO", ast_of_id "POS", ast_of_id "NEG"),
(ast_of_id "My_special_variable0", ast_of_id "My_special_variable1"))
let int_array_of_string s =
let a = Array.create (String.length s) 0 in
for i = 0 to String.length s - 1 do
a.(i) <- int_of_string (String.sub s i 1)
done;
a
let string_of_int_array s =
String.concat "" (Array.to_list (Array.map string_of_int s))
let is_nonzero a =
let b = ref false in Array.iter (fun x -> b := x <> 0 || !b) a; !b
let div2_with_rest n =
let len = Array.length n in
let q = Array.create len 0 in
for i = 0 to len - 2 do
q.(i) <- q.(i) + n.(i) / 2; q.(i + 1) <- 5 * (n.(i) mod 2)
done;
q.(len - 1) <- q.(len - 1) + n.(len - 1) / 2;
q, n.(len - 1) mod 2
let add_1 n =
let m = Array.copy n
and i = ref (Array.length n - 1) in
m.(!i) <- m.(!i) + 1;
while m.(!i) = 10 && !i > 0 do
m.(!i) <- 0; decr i; m.(!i) <- m.(!i) + 1
done;
if !i = 0 && m.(0) = 10 then begin
m.(0) <- 0; Array.concat [[| 1 |]; m]
end else
m
let rec mult_2 n =
let m = Array.copy n in
m.(Array.length n - 1) <- 2 * m.(Array.length n - 1);
for i = Array.length n - 2 downto 0 do
m.(i) <- 2 * m.(i);
if m.(i + 1) >= 10 then begin
m.(i + 1) <- m.(i + 1) - 10; m.(i) <- m.(i) + 1
end
done;
if m.(0) >= 10 then begin
m.(0) <- m.(0) - 10; Array.concat [[| 1 |]; m]
end else
m
let pos_of_int_array astxI astxO astxH x =
let rec pos_of x =
match div2_with_rest x with
| (q, 1) ->
if is_nonzero q then ope("APPLIST", [astxI; pos_of q]) else astxH
| (q, 0) -> ope("APPLIST", [astxO; pos_of q])
| _ -> anomaly "n mod 2 is neither 1 nor 0. Do you bielive that ?"
in
pos_of x
let z_of_string pos_or_neg s dloc =
let ((astxI,astxO,astxH),(astZERO,astPOS,astNEG),_) = get_z_sign dloc in
let v = int_array_of_string s in
if is_nonzero v then
if pos_or_neg then
ope("APPLIST",[astPOS; pos_of_int_array astxI astxO astxH v])
else
ope("APPLIST",[astNEG; pos_of_int_array astxI astxO astxH v])
else
astZERO
exception Non_closed_number
let rec int_array_of_pos c1 c2 c3 p =
match p with
| Node (_,"APPLIST", [b; a]) when alpha_eq(b,c1) ->
mult_2 (int_array_of_pos c1 c2 c3 a)
| Node (_,"APPLIST", [b; a]) when alpha_eq(b,c2) ->
add_1 (mult_2 (int_array_of_pos c1 c2 c3 a))
| a when alpha_eq(a,c3) -> [| 1 |]
| _ -> raise Non_closed_number
let int_array_option_of_pos astxI astxO astxH p =
try
Some (int_array_of_pos astxO astxI astxH p)
with Non_closed_number ->
None
let inside_printer posneg std_pr p =
let ((astxI,astxO,astxH),_,(myvar0,myvar1)) = get_z_sign dummy_loc in
match (int_array_option_of_pos astxI astxO astxH p) with
| Some n ->
if posneg then
[< 'sTR (string_of_int_array n) >]
else
[< 'sTR "(-"; 'sTR (string_of_int_array n); 'sTR ")" >]
| None ->
let c = if posneg then myvar0 else myvar1 in
std_pr (ope("ZEXPR",[ope("APPLIST",[c; p])]))
let outside_printer posneg std_pr p =
let ((astxI,astxO,astxH),_,(myvar0,myvar1)) = get_z_sign dummy_loc in
match (int_array_option_of_pos astxI astxO astxH p) with
| Some n ->
if posneg then
[< 'sTR "`"; 'sTR (string_of_int_array n); 'sTR "`">]
else
[< 'sTR "`-"; 'sTR (string_of_int_array n); 'sTR "`" >]
| None ->
let c = if posneg then myvar0 else myvar1 in
[< 'sTR "("; std_pr (ope("APPLIST",[c; p])); 'sTR ")" >]
(* Declare pretty-printers for integers *)
let _ = Esyntax.Ppprim.add ("positive_printer", (outside_printer true))
let _ = Esyntax.Ppprim.add ("negative_printer", (outside_printer false))
let _ = Esyntax.Ppprim.add ("positive_printer_inside", (inside_printer true))
let _ = Esyntax.Ppprim.add ("negative_printer_inside", (inside_printer false))
(* Declare the primitive parser *)
open Pcoq
let number =
match create_entry (get_univ "znatural") "number" ETast with
| Ast n -> n
| _ -> anomaly "G_zsyntax.number"
let negnumber =
match create_entry (get_univ "znatural") "negnumber" ETast with
| Ast n -> n
| _ -> anomaly "G_zsyntax.negnumber"
let _ =
Gram.extend number None
[None, None,
[[Gramext.Stoken ("INT", "")],
Gramext.action (z_of_string true)]]
let _ =
Gram.extend negnumber None
[None, None,
[[Gramext.Stoken ("INT", "")],
Gramext.action (z_of_string false)]]
|
