author | wenzelm |
Sun, 10 Dec 2006 22:27:06 +0100 | |
changeset 21763 | 12a2773e3608 |
parent 20094 | 99f27df2b6d0 |
child 21780 | ec264b9daf94 |
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 |
|
21763 | 5 |
Concrete syntax for generic numerals. |
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 |
||
17 |
(* bit strings *) (*we try to handle superfluous leading digits nicely*) |
|
18 |
||
19 |
fun prefix_len _ [] = 0 |
|
20 |
| prefix_len pred (x :: xs) = |
|
21 |
if pred x then 1 + prefix_len pred xs else 0; |
|
22 |
||
23 |
fun dest_bin_str tm = |
|
24 |
let |
|
15620
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15595
diff
changeset
|
25 |
val rev_digs = HOLogic.bin_of tm handle TERM _ => raise Match |
6905 | 26 |
val (sign, zs) = |
27 |
(case rev rev_digs of |
|
28 |
~1 :: bs => ("-", prefix_len (equal 1) bs) |
|
29 |
| bs => ("", prefix_len (equal 0) bs)); |
|
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15620
diff
changeset
|
30 |
val i = HOLogic.int_of rev_digs; |
15595 | 31 |
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
|
32 |
in |
15595 | 33 |
if i = IntInf.fromInt 0 orelse i = IntInf.fromInt 1 then raise Match |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11488
diff
changeset
|
34 |
else sign ^ implode (replicate zs "0") ^ num |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11488
diff
changeset
|
35 |
end; |
6905 | 36 |
|
20094
99f27df2b6d0
removed str_to_int in favour of general Syntax.read_xnum;
wenzelm
parents:
20067
diff
changeset
|
37 |
|
6905 | 38 |
(* translation of integer numeral tokens to and from bitstrings *) |
39 |
||
11488
4ff900551340
constify numeral tokens in order to allow translations;
wenzelm
parents:
10891
diff
changeset
|
40 |
fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] = |
20094
99f27df2b6d0
removed str_to_int in favour of general Syntax.read_xnum;
wenzelm
parents:
20067
diff
changeset
|
41 |
(Syntax.const "Numeral.number_of" $ (HOLogic.mk_binum (Syntax.read_xnum str))) |
6905 | 42 |
| numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts); |
43 |
||
44 |
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
|
45 |
let val t' = Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) in |
7429 | 46 |
if not (! show_types) andalso can Term.dest_Type T then t' |
6905 | 47 |
else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T |
48 |
end |
|
13110 | 49 |
| numeral_tr' _ (*"number_of"*) T (t :: ts) = |
50 |
if T = dummyT then Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) |
|
51 |
else raise Match |
|
6905 | 52 |
| numeral_tr' _ (*"number_of"*) _ _ = raise Match; |
53 |
||
54 |
||
55 |
(* theory setup *) |
|
56 |
||
57 |
val setup = |
|
18708 | 58 |
Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #> |
59 |
Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]; |
|
6905 | 60 |
|
61 |
end; |