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