author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 29316  0a7fcdd77f4b 
child 35115  446c5063e4fd 
permissions  rwrr 
6905  1 
(* Title: HOL/Tools/numeral_syntax.ML 
20067
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset

2 
Authors: Markus Wenzel, TU Muenchen 
6905  3 

21780  4 
Concrete syntax for generic numerals  preserves leading zeros/ones. 
6905  5 
*) 
6 

7 
signature NUMERAL_SYNTAX = 

8 
sig 

18708  9 
val setup: theory > theory 
6905  10 
end; 
11 

12 
structure NumeralSyntax: NUMERAL_SYNTAX = 

13 
struct 

14 

21780  15 
(* parse translation *) 
16 

17 
local 

18 

19 
fun mk_bin num = 

20 
let 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

21 
fun bit b bs = HOLogic.mk_bit b $ bs; 
29316  22 
fun mk 0 = Syntax.const @{const_name Int.Pls} 
23 
 mk ~1 = Syntax.const @{const_name Int.Min} 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
22997
diff
changeset

24 
 mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end; 
29316  25 
in mk (#value (Syntax.read_xnum num)) end; 
21780  26 

27 
in 

28 

29 
fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] = 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24712
diff
changeset

30 
Syntax.const @{const_name Int.number_of} $ mk_bin num 
21780  31 
 numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts); 
32 

33 
end; 

6905  34 

21780  35 

36 
(* print translation *) 

37 

38 
local 

39 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24712
diff
changeset

40 
fun dest_bin (Const (@{const_syntax "Int.Pls"}, _)) = [] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24712
diff
changeset

41 
 dest_bin (Const (@{const_syntax "Int.Min"}, _)) = [~1] 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

42 
 dest_bin (Const (@{const_syntax "Int.Bit0"}, _) $ bs) = 0 :: dest_bin bs 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

43 
 dest_bin (Const (@{const_syntax "Int.Bit1"}, _) $ bs) = 1 :: dest_bin bs 
21780  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 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
22997
diff
changeset

50 
 int_of (b :: bs) = b + 2 * int_of bs; 
6905  51 

52 
fun dest_bin_str tm = 

53 
let 

21780  54 
val rev_digs = dest_bin tm; 
55 
val (sign, z) = 

6905  56 
(case rev rev_digs of 
21780  57 
~1 :: bs => ("", leading 1 bs) 
58 
 bs => ("", leading 0 bs)); 

59 
val i = int_of rev_digs; 

24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
22997
diff
changeset

60 
val num = string_of_int (abs i); 
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11488
diff
changeset

61 
in 
21780  62 
if (i = 0 orelse i = 1) andalso z = 0 then raise Match 
63 
else sign ^ implode (replicate z "0") ^ num 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11488
diff
changeset

64 
end; 
6905  65 

29316  66 
fun syntax_numeral t = 
67 
Syntax.const "_Numeral" $ (Syntax.const "_numeral" $ Syntax.free (dest_bin_str t)); 

68 

21780  69 
in 
6905  70 

71 
fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) = 

29316  72 
let val t' = 
73 
if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t 

74 
else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T 

75 
in list_comb (t', ts) end 

13110  76 
 numeral_tr' _ (*"number_of"*) T (t :: ts) = 
29316  77 
if T = dummyT then list_comb (syntax_numeral t, ts) 
13110  78 
else raise Match 
6905  79 
 numeral_tr' _ (*"number_of"*) _ _ = raise Match; 
80 

21780  81 
end; 
82 

6905  83 

84 
(* theory setup *) 

85 

86 
val setup = 

24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24630
diff
changeset

87 
Sign.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24712
diff
changeset

88 
Sign.add_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')]; 
6905  89 

90 
end; 