1 (* Title: HOL/Tools/numeral_syntax.ML |
|
2 Authors: Markus Wenzel, TU Muenchen |
|
3 |
|
4 Concrete syntax for generic numerals -- preserves leading zeros/ones. |
|
5 *) |
|
6 |
|
7 signature NUMERAL_SYNTAX = |
|
8 sig |
|
9 val setup: theory -> theory |
|
10 end; |
|
11 |
|
12 structure Numeral_Syntax: NUMERAL_SYNTAX = |
|
13 struct |
|
14 |
|
15 (* parse translation *) |
|
16 |
|
17 local |
|
18 |
|
19 fun mk_bin num = |
|
20 let |
|
21 fun bit b bs = HOLogic.mk_bit b $ bs; |
|
22 fun mk 0 = Syntax.const @{const_name Int.Pls} |
|
23 | mk ~1 = Syntax.const @{const_name Int.Min} |
|
24 | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end; |
|
25 in mk (#value (Lexicon.read_xnum num)) end; |
|
26 |
|
27 in |
|
28 |
|
29 fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ numeral_tr [t] $ u |
|
30 | numeral_tr [t as Const (num, _)] = Syntax.const @{const_syntax Int.number_of} $ mk_bin num |
|
31 | numeral_tr ts = raise TERM ("numeral_tr", ts); |
|
32 |
|
33 end; |
|
34 |
|
35 |
|
36 (* print translation *) |
|
37 |
|
38 local |
|
39 |
|
40 fun dest_bin (Const (@{const_syntax Int.Pls}, _)) = [] |
|
41 | dest_bin (Const (@{const_syntax Int.Min}, _)) = [~1] |
|
42 | dest_bin (Const (@{const_syntax Int.Bit0}, _) $ bs) = 0 :: dest_bin bs |
|
43 | dest_bin (Const (@{const_syntax Int.Bit1}, _) $ bs) = 1 :: dest_bin bs |
|
44 | dest_bin _ = raise Match; |
|
45 |
|
46 fun leading _ [] = 0 |
|
47 | leading (i: int) (j :: js) = if i = j then 1 + leading i js else 0; |
|
48 |
|
49 fun int_of [] = 0 |
|
50 | int_of (b :: bs) = b + 2 * int_of bs; |
|
51 |
|
52 fun dest_bin_str tm = |
|
53 let |
|
54 val rev_digs = dest_bin tm; |
|
55 val (sign, z) = |
|
56 (case rev rev_digs of |
|
57 ~1 :: bs => ("-", leading 1 bs) |
|
58 | bs => ("", leading 0 bs)); |
|
59 val i = int_of rev_digs; |
|
60 val num = string_of_int (abs i); |
|
61 in |
|
62 if (i = 0 orelse i = 1) andalso z = 0 then raise Match |
|
63 else sign ^ implode (replicate z "0") ^ num |
|
64 end; |
|
65 |
|
66 fun syntax_numeral t = |
|
67 Syntax.const @{syntax_const "_Numeral"} $ |
|
68 (Syntax.const @{syntax_const "_numeral"} $ Syntax.free (dest_bin_str t)); |
|
69 |
|
70 in |
|
71 |
|
72 fun numeral_tr' ctxt (Type (@{type_name fun}, [_, T])) (t :: ts) = |
|
73 let val t' = |
|
74 if not (Config.get ctxt show_types) andalso can Term.dest_Type T then syntax_numeral t |
|
75 else |
|
76 Syntax.const @{syntax_const "_constrain"} $ syntax_numeral t $ |
|
77 Syntax_Phases.term_of_typ ctxt T |
|
78 in list_comb (t', ts) end |
|
79 | numeral_tr' _ T (t :: ts) = |
|
80 if T = dummyT then list_comb (syntax_numeral t, ts) |
|
81 else raise Match |
|
82 | numeral_tr' _ _ _ = raise Match; |
|
83 |
|
84 end; |
|
85 |
|
86 |
|
87 (* theory setup *) |
|
88 |
|
89 val setup = |
|
90 Sign.add_trfuns ([], [(@{syntax_const "_Numeral"}, numeral_tr)], [], []) #> |
|
91 Sign.add_advanced_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')]; |
|
92 |
|
93 end; |
|