author  wenzelm 
Tue, 12 Dec 2006 12:03:46 +0100  
changeset 21789  c4f6bb392030 
parent 21780  ec264b9daf94 
child 21821  7fa19d17f488 
permissions  rwrr 
6905  1 
(* Title: HOL/Tools/numeral_syntax.ML 
2 
ID: $Id$ 

20067
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19481
diff
changeset

3 
Authors: Markus Wenzel, TU Muenchen 
6905  4 

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

8 
signature NUMERAL_SYNTAX = 

9 
sig 

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

13 
structure NumeralSyntax: NUMERAL_SYNTAX = 

14 
struct 

15 

16 

21780  17 
(* parse translation *) 
18 

19 
local 

20 

21 
fun mk_bin num = 

22 
let 

23 
val {leading_zeros = z, value, ...} = Syntax.read_xnum num; 

24 
fun bit b bs = Syntax.const "\\<^const>Numeral.Bit" $ bs $ HOLogic.mk_bit b; 

25 
fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const "\\<^const>Numeral.Pls") 

26 
 mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const "\\<^const>Numeral.Min") 

21789  27 
 mk i = let val (q, r) = IntInf.divMod (i, 2) in bit (IntInf.toInt r) (mk q) end; 
21780  28 
in mk value end; 
29 

30 
in 

31 

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

33 
Syntax.const "Numeral.number_of" $ mk_bin num 

34 
 numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts); 

35 

36 
end; 

6905  37 

21780  38 

39 
(* print translation *) 

40 

41 
local 

42 

43 
fun dest_bit (Const ("Numeral.bit.B0", _)) = 0 

44 
 dest_bit (Const ("Numeral.bit.B1", _)) = 1 

45 
 dest_bit (Const ("bit.B0", _)) = 0 

46 
 dest_bit (Const ("bit.B1", _)) = 1 

47 
 dest_bit _ = raise Match; 

48 

49 
fun dest_bin (Const ("\\<^const>Numeral.Pls", _)) = [] 

50 
 dest_bin (Const ("\\<^const>Numeral.Min", _)) = [~1] 

51 
 dest_bin (Const ("\\<^const>Numeral.Bit", _) $ bs $ b) = dest_bit b :: dest_bin bs 

52 
 dest_bin _ = raise Match; 

53 

54 
fun leading _ [] = 0 

55 
 leading (i: int) (j :: js) = if i = j then 1 + leading i js else 0; 

56 

57 
fun int_of [] = 0 

58 
 int_of (b :: bs) = IntInf.fromInt b + 2 * int_of bs; 

6905  59 

60 
fun dest_bin_str tm = 

61 
let 

21780  62 
val rev_digs = dest_bin tm; 
63 
val (sign, z) = 

6905  64 
(case rev rev_digs of 
21780  65 
~1 :: bs => ("", leading 1 bs) 
66 
 bs => ("", leading 0 bs)); 

67 
val i = int_of rev_digs; 

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

69 
in 
21780  70 
if (i = 0 orelse i = 1) andalso z = 0 then raise Match 
71 
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

72 
end; 
6905  73 

21780  74 
in 
6905  75 

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

11488
4ff900551340
constify numeral tokens in order to allow translations;
wenzelm
parents:
10891
diff
changeset

77 
let val t' = Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) in 
7429  78 
if not (! show_types) andalso can Term.dest_Type T then t' 
6905  79 
else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T 
80 
end 

13110  81 
 numeral_tr' _ (*"number_of"*) T (t :: ts) = 
82 
if T = dummyT then Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) 

83 
else raise Match 

6905  84 
 numeral_tr' _ (*"number_of"*) _ _ = raise Match; 
85 

21780  86 
end; 
87 

6905  88 

89 
(* theory setup *) 

90 

91 
val setup = 

18708  92 
Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #> 
93 
Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]; 

6905  94 

95 
end; 