author | wenzelm |
Sun, 16 Jul 2000 20:53:19 +0200 | |
changeset 9360 | 82e8b18e6985 |
parent 9358 | 973672495414 |
child 9410 | 612ee826a409 |
permissions | -rw-r--r-- |
6905 | 1 |
(* Title: HOL/Numeral.thy |
2 |
ID: $Id$ |
|
3 |
Author: Larry Paulson and Markus Wenzel |
|
4 |
||
9358
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
5 |
Generic numerals represented as twos-complement bit strings, and |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
6 |
selector function as ones-complement unit strings. |
6905 | 7 |
*) |
8 |
||
9 |
theory Numeral = Datatype |
|
9035 | 10 |
files "Tools/numeral_syntax.ML": |
6905 | 11 |
|
9358
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
12 |
|
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
13 |
(* numerals *) |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
14 |
|
6905 | 15 |
datatype |
16 |
bin = Pls |
|
17 |
| Min |
|
9358
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
18 |
| Bit bin bool (infixl "BIT" 90) |
6905 | 19 |
|
20 |
axclass |
|
9035 | 21 |
number < "term" (*for numeric types: nat, int, real, ...*) |
6905 | 22 |
|
23 |
consts |
|
9035 | 24 |
number_of :: "bin => 'a::number" |
6905 | 25 |
|
26 |
syntax |
|
9358
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
27 |
"_Numeral" :: "xnum => 'a" ("_") |
6905 | 28 |
|
9035 | 29 |
setup NumeralSyntax.setup |
6905 | 30 |
|
31 |
||
9358
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
32 |
(* selector functions *) |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
33 |
|
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
34 |
(*Note that type constraints on selector functons are not handled |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
35 |
properly here*) |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
36 |
|
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
37 |
syntax |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
38 |
"_selector" :: 'a |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
39 |
"_op_selector" :: "xnum => 'a" ("op _" [0] 1000) |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
40 |
|
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
41 |
translations |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
42 |
"(_Numeral i) x" => "_selector i x" |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
43 |
|
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
44 |
parse_translation {* |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
45 |
let |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
46 |
val fstC = Syntax.const "fst"; |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
47 |
val sndC = Syntax.const "snd"; |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
48 |
fun ap_snd t = sndC $ t; |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
49 |
fun comp_snd t = Syntax.const "op o" $ t $ sndC; |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
50 |
|
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
51 |
fun selector_tr [Free (x, _), t] = |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
52 |
let val i = Syntax.read_xnum x in |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
53 |
if i = 0 orelse i = ~1 then t |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
54 |
else if i > 0 then fstC $ funpow (i - 1) ap_snd t |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
55 |
else funpow (~i - 1) ap_snd t |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
56 |
end |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
57 |
| selector_tr ts = raise TERM ("selector_tr", ts); |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
58 |
|
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
59 |
fun op_selector_tr [Free (x, _)] = |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
60 |
let val i = Syntax.read_xnum x in |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
61 |
if i = 0 orelse i = ~1 then Abs ("x", dummyT, Bound 0) |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
62 |
else if i > 0 then funpow (i - 1) comp_snd fstC |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
63 |
else funpow (~i - 2) comp_snd sndC |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
64 |
end |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
65 |
| op_selector_tr ts = raise TERM ("op_selector_tr", ts); |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
66 |
in [("_selector", selector_tr), ("_op_selector", op_selector_tr)] end |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
67 |
*} |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
68 |
|
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
69 |
print_translation {* |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
70 |
let |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
71 |
fun mk_xnum i = |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
72 |
Syntax.free ("#" ^ (if i < 0 then "-" else "") ^ (string_of_int (abs i))); |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
73 |
|
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
74 |
|
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
75 |
fun snds_tr' (i, Const ("snd", _) $ t) = snds_tr' (i + 1, t) |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
76 |
| snds_tr' x = x; |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
77 |
|
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
78 |
fun fst_tr' t = let val (i, t') = snds_tr' (0, t) in (i + 1, t') end; |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
79 |
fun snd_tr' t = let val (i, t') = snds_tr' (0, t) in (~ (i + 2), t') end; |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
80 |
|
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
81 |
fun selector_tr' f (t :: ts) = |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
82 |
let val (i, u) = f t in |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
83 |
if ~2 <= i andalso i <= 1 then raise Match |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
84 |
else Term.list_comb (mk_xnum i $ u, ts) end |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
85 |
| selector_tr' _ [] = raise Match; |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
86 |
|
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
87 |
|
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
88 |
fun o_snd_tr' i (Const ("op o", _) $ t $ Const ("snd", _)) = o_snd_tr' (i + 1) t |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
89 |
| o_snd_tr' i (Const ("fst", _)) = i + 1 |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
90 |
| o_snd_tr' i (Const ("snd", _)) = ~ (i + 2) |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
91 |
| o_snd_tr' _ _ = raise Match; |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
92 |
|
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
93 |
fun comp_tr' (t :: u :: ts) = |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
94 |
Term.list_comb (Syntax.const "_op_selector" $ |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
95 |
mk_xnum (o_snd_tr' 0 (Syntax.const "op o" $ t $ u)), ts) |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
96 |
| comp_tr' _ = raise Match; |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
97 |
in [("fst", selector_tr' fst_tr'), ("snd", selector_tr' snd_tr'), ("op o", comp_tr')] end |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
98 |
*} |
973672495414
added syntax for proper / improper selector functions;
wenzelm
parents:
9035
diff
changeset
|
99 |
|
9035 | 100 |
end |