author  wenzelm 
Sun, 09 Apr 2006 18:51:15 +0200  
changeset 19381  6cd8abc7f15b 
parent 18708  4b3dadb4fe33 
child 19481  a6205c6203ea 
permissions  rwrr 
6905  1 
(* Title: HOL/Tools/numeral_syntax.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

5 
Concrete syntax for generic numerals. Assumes consts and syntax of 

6 
theory HOL/Numeral. 

7 
*) 

8 

9 
signature NUMERAL_SYNTAX = 

10 
sig 

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

14 
structure NumeralSyntax: NUMERAL_SYNTAX = 

15 
struct 

16 

17 

18 
(* bit strings *) (*we try to handle superfluous leading digits nicely*) 

19 

20 
fun prefix_len _ [] = 0 

21 
 prefix_len pred (x :: xs) = 

22 
if pred x then 1 + prefix_len pred xs else 0; 

23 

24 
fun dest_bin_str tm = 

25 
let 

15620
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15595
diff
changeset

26 
val rev_digs = HOLogic.bin_of tm handle TERM _ => raise Match 
6905  27 
val (sign, zs) = 
28 
(case rev rev_digs of 

29 
~1 :: bs => ("", prefix_len (equal 1) bs) 

30 
 bs => ("", prefix_len (equal 0) bs)); 

15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15620
diff
changeset

31 
val i = HOLogic.int_of rev_digs; 
15595  32 
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

33 
in 
15595  34 
if i = IntInf.fromInt 0 orelse i = IntInf.fromInt 1 then raise Match 
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11488
diff
changeset

35 
else sign ^ implode (replicate zs "0") ^ num 
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11488
diff
changeset

36 
end; 
6905  37 

38 
(* translation of integer numeral tokens to and from bitstrings *) 

39 

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

40 
fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] = 
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15620
diff
changeset

41 
(Syntax.const "Numeral.number_of" $ (HOLogic.mk_bin (valOf (IntInf.fromString str)))) 
6905  42 
 numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts); 
43 

44 
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

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

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

51 
else raise Match 

6905  52 
 numeral_tr' _ (*"number_of"*) _ _ = raise Match; 
53 

54 

55 
(* theory setup *) 

56 

57 
val setup = 

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

6905  60 

61 
end; 