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