author | paulson |
Thu, 01 Jul 2004 12:29:53 +0200 | |
changeset 15013 | 34264f5e4691 |
parent 14981 | e73f8140af78 |
child 15595 | dc8a41c7cefc |
permissions | -rw-r--r-- |
6905 | 1 |
(* Title: HOL/Tools/numeral_syntax.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
5 |
Concrete syntax for generic numerals. Assumes consts and syntax of |
|
6 |
theory HOL/Numeral. |
|
7 |
*) |
|
8 |
||
9 |
signature NUMERAL_SYNTAX = |
|
10 |
sig |
|
10891 | 11 |
val setup: (theory -> theory) list |
6905 | 12 |
end; |
13 |
||
14 |
structure NumeralSyntax: NUMERAL_SYNTAX = |
|
15 |
struct |
|
16 |
||
17 |
||
18 |
(* bits *) |
|
19 |
||
20 |
fun dest_bit (Const ("False", _)) = 0 |
|
21 |
| dest_bit (Const ("True", _)) = 1 |
|
22 |
| dest_bit _ = raise Match; |
|
23 |
||
24 |
||
25 |
(* bit strings *) (*we try to handle superfluous leading digits nicely*) |
|
26 |
||
27 |
fun prefix_len _ [] = 0 |
|
28 |
| prefix_len pred (x :: xs) = |
|
29 |
if pred x then 1 + prefix_len pred xs else 0; |
|
30 |
||
15013 | 31 |
fun bin_of (Const ("Numeral.Pls", _)) = [] |
32 |
| bin_of (Const ("Numeral.Min", _)) = [~1] |
|
13495 | 33 |
| bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs |
6905 | 34 |
| bin_of _ = raise Match; |
35 |
||
7550 | 36 |
val dest_bin = HOLogic.int_of o bin_of; |
6905 | 37 |
|
38 |
fun dest_bin_str tm = |
|
39 |
let |
|
40 |
val rev_digs = bin_of tm; |
|
41 |
val (sign, zs) = |
|
42 |
(case rev rev_digs of |
|
43 |
~1 :: bs => ("-", prefix_len (equal 1) bs) |
|
44 |
| bs => ("", prefix_len (equal 0) bs)); |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11488
diff
changeset
|
45 |
val i = HOLogic.int_of rev_digs; |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11488
diff
changeset
|
46 |
val num = string_of_int (abs i); |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11488
diff
changeset
|
47 |
in |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11488
diff
changeset
|
48 |
if i = 0 orelse i = 1 then raise Match |
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11488
diff
changeset
|
49 |
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
|
50 |
end; |
6905 | 51 |
|
52 |
||
53 |
(* translation of integer numeral tokens to and from bitstrings *) |
|
54 |
||
11488
4ff900551340
constify numeral tokens in order to allow translations;
wenzelm
parents:
10891
diff
changeset
|
55 |
fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] = |
10693 | 56 |
(Syntax.const "Numeral.number_of" $ HOLogic.mk_bin (Syntax.read_xnum str)) |
6905 | 57 |
| numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts); |
58 |
||
59 |
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
|
60 |
let val t' = Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) in |
7429 | 61 |
if not (! show_types) andalso can Term.dest_Type T then t' |
6905 | 62 |
else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T |
63 |
end |
|
13110 | 64 |
| numeral_tr' _ (*"number_of"*) T (t :: ts) = |
65 |
if T = dummyT then Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) |
|
66 |
else raise Match |
|
6905 | 67 |
| numeral_tr' _ (*"number_of"*) _ _ = raise Match; |
68 |
||
69 |
||
70 |
(* theory setup *) |
|
71 |
||
72 |
val setup = |
|
15013 | 73 |
[Theory.hide_consts false ["Numeral.Pls", "Numeral.Min"], |
13495 | 74 |
Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []), |
6905 | 75 |
Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]]; |
76 |
||
77 |
||
78 |
end; |