author  wenzelm 
Sun, 05 Sep 2010 21:41:24 +0200  
changeset 39134  917b4b6ba3d2 
parent 35430  df2862dc23a8 
child 42245  29e3967550d5 
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 

35123  12 
structure Numeral_Syntax: NUMERAL_SYNTAX = 
6905  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, _)] = 

35115  30 
Syntax.const @{const_syntax 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 

35115  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 

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 = 
35115  67 
Syntax.const @{syntax_const "_Numeral"} $ 
68 
(Syntax.const @{syntax_const "_numeral"} $ Syntax.free (dest_bin_str t)); 

29316  69 

21780  70 
in 
6905  71 

39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
35430
diff
changeset

72 
fun numeral_tr' ctxt show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) = 
29316  73 
let val t' = 
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
35430
diff
changeset

74 
if not (Config.get ctxt show_types) andalso can Term.dest_Type T then syntax_numeral t 
29316  75 
else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T 
76 
in list_comb (t', ts) end 

39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
35430
diff
changeset

77 
 numeral_tr' _ _ (*"number_of"*) T (t :: ts) = 
29316  78 
if T = dummyT then list_comb (syntax_numeral t, ts) 
13110  79 
else raise Match 
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
35430
diff
changeset

80 
 numeral_tr' _ _ (*"number_of"*) _ _ = raise Match; 
6905  81 

21780  82 
end; 
83 

6905  84 

85 
(* theory setup *) 

86 

87 
val setup = 

35115  88 
Sign.add_trfuns ([], [(@{syntax_const "_Numeral"}, numeral_tr)], [], []) #> 
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
35430
diff
changeset

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

91 
end; 