author | wenzelm |
Sat, 13 Feb 2010 23:24:57 +0100 | |
changeset 35123 | e286d5df187a |
parent 35112 | ff6f60e6ab85 |
child 40314 | b5ec88d9ac03 |
permissions | -rw-r--r-- |
9570 | 1 |
(* Title: ZF/Tools/numeral_syntax.ML |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
||
4 |
Concrete syntax for generic numerals. Assumes consts and syntax of |
|
23146 | 5 |
theory Bin. |
9570 | 6 |
*) |
7 |
||
8 |
signature NUMERAL_SYNTAX = |
|
9 |
sig |
|
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
10 |
val make_binary: int -> int list |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
11 |
val dest_binary: int list -> int |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
12 |
val int_tr: term list -> term |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
13 |
val int_tr': bool -> typ -> term list -> term |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
14 |
val setup: theory -> theory |
9570 | 15 |
end; |
16 |
||
35123 | 17 |
structure Numeral_Syntax: NUMERAL_SYNTAX = |
9570 | 18 |
struct |
19 |
||
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
20 |
(* bits *) |
9570 | 21 |
|
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
22 |
fun mk_bit 0 = Syntax.const @{const_syntax "0"} |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
23 |
| mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax 0} |
9570 | 24 |
| mk_bit _ = sys_error "mk_bit"; |
25 |
||
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
26 |
fun dest_bit (Const (@{const_syntax "0"}, _)) = 0 |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
27 |
| dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax "0"}, _)) = 1 |
9570 | 28 |
| dest_bit _ = raise Match; |
29 |
||
30 |
||
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
31 |
(* bit strings *) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
32 |
|
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
33 |
fun make_binary 0 = [] |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
34 |
| make_binary ~1 = [~1] |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
35 |
| make_binary n = (n mod 2) :: make_binary (n div 2); |
9570 | 36 |
|
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
37 |
fun dest_binary [] = 0 |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
38 |
| dest_binary (b :: bs) = b + 2 * dest_binary bs; |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
39 |
|
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
40 |
|
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
41 |
(*try to handle superfluous leading digits nicely*) |
9570 | 42 |
fun prefix_len _ [] = 0 |
43 |
| prefix_len pred (x :: xs) = |
|
44 |
if pred x then 1 + prefix_len pred xs else 0; |
|
45 |
||
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23146
diff
changeset
|
46 |
fun mk_bin i = |
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
47 |
let |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
48 |
fun term_of [] = Syntax.const @{const_syntax Pls} |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
49 |
| term_of [~1] = Syntax.const @{const_syntax Min} |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
50 |
| term_of (b :: bs) = Syntax.const @{const_syntax Bit} $ term_of bs $ mk_bit b; |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
51 |
in term_of (make_binary i) end; |
9570 | 52 |
|
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
53 |
fun bin_of (Const (@{const_syntax Pls}, _)) = [] |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
54 |
| bin_of (Const (@{const_syntax Min}, _)) = [~1] |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
55 |
| bin_of (Const (@{const_syntax Bit}, _) $ bs $ b) = dest_bit b :: bin_of bs |
9570 | 56 |
| bin_of _ = raise Match; |
57 |
||
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
58 |
(*Leading 0s and (for negative numbers) -1s cause complications, though they |
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
10917
diff
changeset
|
59 |
should never arise in normal use. The formalization used in HOL prevents |
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
10917
diff
changeset
|
60 |
them altogether.*) |
9570 | 61 |
fun show_int t = |
62 |
let |
|
63 |
val rev_digs = bin_of t; |
|
64 |
val (sign, zs) = |
|
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
65 |
(case rev rev_digs of |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
66 |
~1 :: bs => ("-", prefix_len (equal 1) bs) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
67 |
| bs => ("", prefix_len (equal 0) bs)); |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
68 |
val num = string_of_int (abs (dest_binary rev_digs)); |
9570 | 69 |
in |
70 |
"#" ^ sign ^ implode (replicate zs "0") ^ num |
|
71 |
end; |
|
72 |
||
73 |
||
74 |
(* translation of integer constant tokens to and from binary *) |
|
75 |
||
76 |
fun int_tr (*"_Int"*) [t as Free (str, _)] = |
|
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
77 |
Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Syntax.read_xnum str)) |
9570 | 78 |
| int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts); |
79 |
||
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
80 |
fun int_tr' _ _ (*"integ_of"*) [t] = |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
81 |
Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t) |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
82 |
| int_tr' (_: bool) (_: typ) _ = raise Match; |
9570 | 83 |
|
84 |
||
85 |
val setup = |
|
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
86 |
(Sign.add_trfuns ([], [(@{syntax_const "_Int"}, int_tr)], [], []) #> |
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset
|
87 |
Sign.add_trfunsT [(@{const_syntax integ_of}, int_tr')]); |
9570 | 88 |
|
89 |
end; |