author  wenzelm 
Tue, 18 Sep 2007 16:08:00 +0200  
changeset 24630  351a308ab58d 
parent 22997  d4f3b015b50b 
child 24712  64ed05609568 
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 

21780  16 
(* parse translation *) 
17 

18 
local 

19 

20 
fun mk_bin num = 

21 
let 

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

22997  23 
fun bit b bs = Syntax.const @{const_name Numeral.Bit} $ bs $ HOLogic.mk_bit b; 
24 
fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Numeral.Pls}) 

25 
 mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Numeral.Min}) 

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

26 
 mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end; 
21780  27 
in mk value end; 
28 

29 
in 

30 

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

22997  32 
Syntax.const @{const_name Numeral.number_of} $ mk_bin num 
21780  33 
 numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts); 
34 

35 
end; 

6905  36 

21780  37 

38 
(* print translation *) 

39 

40 
local 

41 

22997  42 
fun dest_bit (Const (@{const_syntax Numeral.bit.B0}, _)) = 0 
43 
 dest_bit (Const (@{const_syntax Numeral.bit.B1}, _)) = 1 

21780  44 
 dest_bit (Const ("bit.B0", _)) = 0 
45 
 dest_bit (Const ("bit.B1", _)) = 1 

46 
 dest_bit _ = raise Match; 

47 

22997  48 
fun dest_bin (Const (@{const_syntax "Numeral.Pls"}, _)) = [] 
49 
 dest_bin (Const (@{const_syntax "Numeral.Min"}, _)) = [~1] 

50 
 dest_bin (Const (@{const_syntax "Numeral.Bit"}, _) $ bs $ b) = dest_bit b :: dest_bin bs 

21780  51 
 dest_bin _ = raise Match; 
52 

53 
fun leading _ [] = 0 

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

55 

56 
fun int_of [] = 0 

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

57 
 int_of (b :: bs) = b + 2 * int_of bs; 
6905  58 

59 
fun dest_bin_str tm = 

60 
let 

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

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

66 
val i = int_of rev_digs; 

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

67 
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

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

71 
end; 
6905  72 

21780  73 
in 
6905  74 

75 
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

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

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

82 
else raise Match 

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

21780  85 
end; 
86 

6905  87 

88 
(* theory setup *) 

89 

90 
val setup = 

18708  91 
Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #> 
22997  92 
Theory.add_trfunsT [(@{const_syntax Numeral.number_of}, numeral_tr')]; 
6905  93 

94 
end; 