author | kleing |
Tue, 11 Jul 2006 00:43:54 +0200 | |
changeset 20067 | 26bac504ef90 |
parent 19481 | a6205c6203ea |
child 20094 | 99f27df2b6d0 |
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 |
|
5 |
Concrete syntax for generic numerals. Assumes consts and syntax of |
|
6 |
theory HOL/Numeral. |
|
7 |
*) |
|
8 |
||
9 |
signature NUMERAL_SYNTAX = |
|
10 |
sig |
|
18708 | 11 |
val setup: theory -> theory |
6905 | 12 |
end; |
13 |
||
14 |
structure NumeralSyntax: NUMERAL_SYNTAX = |
|
15 |
struct |
|
16 |
||
17 |
||
18 |
(* bit strings *) (*we try to handle superfluous leading digits nicely*) |
|
19 |
||
20 |
fun prefix_len _ [] = 0 |
|
21 |
| prefix_len pred (x :: xs) = |
|
22 |
if pred x then 1 + prefix_len pred xs else 0; |
|
23 |
||
24 |
fun dest_bin_str tm = |
|
25 |
let |
|
15620
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15595
diff
changeset
|
26 |
val rev_digs = HOLogic.bin_of tm handle TERM _ => raise Match |
6905 | 27 |
val (sign, zs) = |
28 |
(case rev rev_digs of |
|
29 |
~1 :: bs => ("-", prefix_len (equal 1) bs) |
|
30 |
| 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
|
31 |
val i = HOLogic.int_of rev_digs; |
15595 | 32 |
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
|
33 |
in |
15595 | 34 |
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
|
35 |
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
|
36 |
end; |
6905 | 37 |
|
38 |
(* translation of integer numeral tokens to and from bitstrings *) |
|
39 |
||
20067
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
40 |
(*additional translations of binary and hex numbers to normal numbers*) |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
41 |
local |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
42 |
|
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
43 |
(*get A => ord"0" + 10, etc*) |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
44 |
fun remap_hex c = |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
45 |
let |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
46 |
val zero = ord"0"; |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
47 |
val a = ord"a"; |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
48 |
val ca = ord"A"; |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
49 |
val x = ord c; |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
50 |
in |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
51 |
if x >= a then chr (x - a + zero + 10) |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
52 |
else if x >= ca then chr (x - ca + zero + 10) |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
53 |
else c |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
54 |
end; |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
55 |
|
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
56 |
fun str_to_int' ("0" :: "x" :: ds) = read_radixint (16, map remap_hex ds) |> #1 |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
57 |
| str_to_int' ("0" :: "b" :: ds) = read_radixint (2, ds) |> #1 |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
58 |
| str_to_int' ds = implode ds |> IntInf.fromString |> valOf; |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
59 |
|
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
60 |
in |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
61 |
|
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
62 |
val str_to_int = str_to_int' o explode; |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
63 |
|
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
64 |
end; |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
65 |
|
11488
4ff900551340
constify numeral tokens in order to allow translations;
wenzelm
parents:
10891
diff
changeset
|
66 |
fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] = |
20067
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset
|
67 |
(Syntax.const "Numeral.number_of" $ (HOLogic.mk_binum (str_to_int str))) |
6905 | 68 |
| numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts); |
69 |
||
70 |
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
|
71 |
let val t' = Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) in |
7429 | 72 |
if not (! show_types) andalso can Term.dest_Type T then t' |
6905 | 73 |
else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T |
74 |
end |
|
13110 | 75 |
| numeral_tr' _ (*"number_of"*) T (t :: ts) = |
76 |
if T = dummyT then Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) |
|
77 |
else raise Match |
|
6905 | 78 |
| numeral_tr' _ (*"number_of"*) _ _ = raise Match; |
79 |
||
80 |
||
81 |
(* theory setup *) |
|
82 |
||
83 |
val setup = |
|
18708 | 84 |
Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #> |
85 |
Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]; |
|
6905 | 86 |
|
87 |
end; |