author | wenzelm |
Tue, 12 Dec 2006 12:03:46 +0100 | |
changeset 21789 | c4f6bb392030 |
parent 21780 | ec264b9daf94 |
child 21821 | 7fa19d17f488 |
permissions | -rw-r--r-- |
6905 | 1 |
(* Title: HOL/Tools/numeral_syntax.ML |
2 |
ID: $Id$ |
|
20067
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
3 |
Authors: Markus Wenzel, TU Muenchen |
6905 | 4 |
|
21780 | 5 |
Concrete syntax for generic numerals -- preserves leading zeros/ones. |
6905 | 6 |
*) |
7 |
||
8 |
signature NUMERAL_SYNTAX = |
|
9 |
sig |
|
18708 | 10 |
val setup: theory -> theory |
6905 | 11 |
end; |
12 |
||
13 |
structure NumeralSyntax: NUMERAL_SYNTAX = |
|
14 |
struct |
|
15 |
||
16 |
||
21780 | 17 |
(* parse translation *) |
18 |
||
19 |
local |
|
20 |
||
21 |
fun mk_bin num = |
|
22 |
let |
|
23 |
val {leading_zeros = z, value, ...} = Syntax.read_xnum num; |
|
24 |
fun bit b bs = Syntax.const "\\<^const>Numeral.Bit" $ bs $ HOLogic.mk_bit b; |
|
25 |
fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const "\\<^const>Numeral.Pls") |
|
26 |
| mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const "\\<^const>Numeral.Min") |
|
21789 | 27 |
| mk i = let val (q, r) = IntInf.divMod (i, 2) in bit (IntInf.toInt r) (mk q) end; |
21780 | 28 |
in mk value end; |
29 |
||
30 |
in |
|
31 |
||
32 |
fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] = |
|
33 |
Syntax.const "Numeral.number_of" $ mk_bin num |
|
34 |
| numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts); |
|
35 |
||
36 |
end; |
|
6905 | 37 |
|
21780 | 38 |
|
39 |
(* print translation *) |
|
40 |
||
41 |
local |
|
42 |
||
43 |
fun dest_bit (Const ("Numeral.bit.B0", _)) = 0 |
|
44 |
| dest_bit (Const ("Numeral.bit.B1", _)) = 1 |
|
45 |
| dest_bit (Const ("bit.B0", _)) = 0 |
|
46 |
| dest_bit (Const ("bit.B1", _)) = 1 |
|
47 |
| dest_bit _ = raise Match; |
|
48 |
||
49 |
fun dest_bin (Const ("\\<^const>Numeral.Pls", _)) = [] |
|
50 |
| dest_bin (Const ("\\<^const>Numeral.Min", _)) = [~1] |
|
51 |
| dest_bin (Const ("\\<^const>Numeral.Bit", _) $ bs $ b) = dest_bit b :: dest_bin bs |
|
52 |
| dest_bin _ = raise Match; |
|
53 |
||
54 |
fun leading _ [] = 0 |
|
55 |
| leading (i: int) (j :: js) = if i = j then 1 + leading i js else 0; |
|
56 |
||
57 |
fun int_of [] = 0 |
|
58 |
| int_of (b :: bs) = IntInf.fromInt b + 2 * int_of bs; |
|
6905 | 59 |
|
60 |
fun dest_bin_str tm = |
|
61 |
let |
|
21780 | 62 |
val rev_digs = dest_bin tm; |
63 |
val (sign, z) = |
|
6905 | 64 |
(case rev rev_digs of |
21780 | 65 |
~1 :: bs => ("-", leading 1 bs) |
66 |
| bs => ("", leading 0 bs)); |
|
67 |
val i = int_of rev_digs; |
|
15595 | 68 |
val num = IntInf.toString (IntInf.abs i); |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11488
diff
changeset
|
69 |
in |
21780 | 70 |
if (i = 0 orelse i = 1) andalso z = 0 then raise Match |
71 |
else sign ^ implode (replicate z "0") ^ num |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11488
diff
changeset
|
72 |
end; |
6905 | 73 |
|
21780 | 74 |
in |
6905 | 75 |
|
76 |
fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) = |
|
11488
4ff900551340
constify numeral tokens in order to allow translations;
wenzelm
parents:
10891
diff
changeset
|
77 |
let val t' = Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) in |
7429 | 78 |
if not (! show_types) andalso can Term.dest_Type T then t' |
6905 | 79 |
else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T |
80 |
end |
|
13110 | 81 |
| numeral_tr' _ (*"number_of"*) T (t :: ts) = |
82 |
if T = dummyT then Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) |
|
83 |
else raise Match |
|
6905 | 84 |
| numeral_tr' _ (*"number_of"*) _ _ = raise Match; |
85 |
||
21780 | 86 |
end; |
87 |
||
6905 | 88 |
|
89 |
(* theory setup *) |
|
90 |
||
91 |
val setup = |
|
18708 | 92 |
Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #> |
93 |
Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]; |
|
6905 | 94 |
|
95 |
end; |