author | wenzelm |
Sat, 17 Oct 2009 14:43:18 +0200 | |
changeset 32960 | 69916a850301 |
parent 26190 | cf51a23c0cd0 |
child 35112 | ff6f60e6ab85 |
permissions | -rw-r--r-- |
9570 | 1 |
(* Title: ZF/Tools/numeral_syntax.ML |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
||
4 |
Concrete syntax for generic numerals. Assumes consts and syntax of |
|
23146 | 5 |
theory Bin. |
9570 | 6 |
*) |
7 |
||
8 |
signature NUMERAL_SYNTAX = |
|
9 |
sig |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
10 |
val dest_bin : term -> int |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
11 |
val mk_bin : int -> term |
9570 | 12 |
val int_tr : term list -> term |
13 |
val int_tr' : bool -> typ -> term list -> term |
|
18708 | 14 |
val setup : theory -> theory |
9570 | 15 |
end; |
16 |
||
17 |
structure NumeralSyntax: NUMERAL_SYNTAX = |
|
18 |
struct |
|
19 |
||
20 |
(* Bits *) |
|
21 |
||
26190 | 22 |
fun mk_bit 0 = @{term "0"} |
23 |
| mk_bit 1 = @{term "succ(0)"} |
|
9570 | 24 |
| mk_bit _ = sys_error "mk_bit"; |
25 |
||
26190 | 26 |
fun dest_bit (Const (@{const_name "0"}, _)) = 0 |
27 |
| dest_bit (Const (@{const_name succ}, _) $ Const (@{const_name "0"}, _)) = 1 |
|
9570 | 28 |
| dest_bit _ = raise Match; |
29 |
||
30 |
||
31 |
(* Bit strings *) (*we try to handle superfluous leading digits nicely*) |
|
32 |
||
33 |
fun prefix_len _ [] = 0 |
|
34 |
| prefix_len pred (x :: xs) = |
|
35 |
if pred x then 1 + prefix_len pred xs else 0; |
|
36 |
||
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
37 |
fun mk_bin i = |
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
10917
diff
changeset
|
38 |
let fun bin_of_int 0 = [] |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26190
diff
changeset
|
39 |
| bin_of_int ~1 = [~1] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26190
diff
changeset
|
40 |
| bin_of_int n = (n mod 2) :: bin_of_int (n div 2); |
9570 | 41 |
|
26190 | 42 |
fun term_of [] = @{const Pls} |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26190
diff
changeset
|
43 |
| term_of [~1] = @{const Min} |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26190
diff
changeset
|
44 |
| term_of (b :: bs) = @{const Bit} $ term_of bs $ mk_bit b; |
9570 | 45 |
in |
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
10917
diff
changeset
|
46 |
term_of (bin_of_int i) |
9570 | 47 |
end; |
48 |
||
49 |
(*we consider all "spellings", since they could vary depending on the caller*) |
|
50 |
fun bin_of (Const ("Pls", _)) = [] |
|
51 |
| bin_of (Const ("bin.Pls", _)) = [] |
|
52 |
| bin_of (Const ("Bin.bin.Pls", _)) = [] |
|
53 |
| bin_of (Const ("Min", _)) = [~1] |
|
54 |
| bin_of (Const ("bin.Min", _)) = [~1] |
|
55 |
| bin_of (Const ("Bin.bin.Min", _)) = [~1] |
|
56 |
| bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs |
|
57 |
| bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs |
|
58 |
| bin_of (Const ("Bin.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs |
|
59 |
| bin_of _ = raise Match; |
|
60 |
||
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
10917
diff
changeset
|
61 |
(*Convert a list of bits to an integer*) |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
62 |
fun integ_of [] = 0 |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
63 |
| integ_of (b :: bs) = b + 2 * integ_of bs; |
9570 | 64 |
|
65 |
val dest_bin = integ_of o bin_of; |
|
66 |
||
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
10917
diff
changeset
|
67 |
(*leading 0s and (for negative numbers) -1s cause complications, though they |
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
10917
diff
changeset
|
68 |
should never arise in normal use. The formalization used in HOL prevents |
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
10917
diff
changeset
|
69 |
them altogether.*) |
9570 | 70 |
fun show_int t = |
71 |
let |
|
72 |
val rev_digs = bin_of t; |
|
73 |
val (sign, zs) = |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26190
diff
changeset
|
74 |
(case rev rev_digs of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26190
diff
changeset
|
75 |
~1 :: bs => ("-", prefix_len (equal 1) bs) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26190
diff
changeset
|
76 |
| bs => ("", prefix_len (equal 0) bs)); |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
77 |
val num = string_of_int (abs (integ_of rev_digs)); |
9570 | 78 |
in |
79 |
"#" ^ sign ^ implode (replicate zs "0") ^ num |
|
80 |
end; |
|
81 |
||
82 |
||
83 |
||
84 |
(* translation of integer constant tokens to and from binary *) |
|
85 |
||
86 |
fun int_tr (*"_Int"*) [t as Free (str, _)] = |
|
21781 | 87 |
Syntax.const "integ_of" $ mk_bin (#value (Syntax.read_xnum str)) |
9570 | 88 |
| int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts); |
89 |
||
10917 | 90 |
fun int_tr' _ _ (*"integ_of"*) [t] = Syntax.const "_Int" $ Syntax.free (show_int t) |
9570 | 91 |
| int_tr' (_:bool) (_:typ) _ = raise Match; |
92 |
||
93 |
||
94 |
val setup = |
|
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24630
diff
changeset
|
95 |
(Sign.add_trfuns ([], [("_Int", int_tr)], [], []) #> |
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24630
diff
changeset
|
96 |
Sign.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]); |
9570 | 97 |
|
98 |
end; |