author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 34944  970e1466028d 
child 37881  096c8397c989 
permissions  rwrr 
28308  1 
(* Title: HOL/Tools/numeral.ML 
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

2 
Author: Makarius 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

3 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

4 
Logical operations on numerals (see also HOL/hologic.ML). 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

5 
*) 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

6 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

7 
signature NUMERAL = 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

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

9 
val mk_cnumeral: int > cterm 
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23575
diff
changeset

10 
val mk_cnumber: ctyp > int > cterm 
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34898
diff
changeset

11 
val add_code: string > bool > (Code_Printer.literals > int > string) > string > theory > theory 
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

12 
end; 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

13 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

14 
structure Numeral: NUMERAL = 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

15 
struct 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

16 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

17 
(* numeral *) 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

18 

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

19 
fun mk_cbit 0 = @{cterm "Int.Bit0"} 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25967
diff
changeset

20 
 mk_cbit 1 = @{cterm "Int.Bit1"} 
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

21 
 mk_cbit _ = raise CTERM ("mk_cbit", []); 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

22 

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

23 
fun mk_cnumeral 0 = @{cterm "Int.Pls"} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset

24 
 mk_cnumeral ~1 = @{cterm "Int.Min"} 
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

25 
 mk_cnumeral i = 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23575
diff
changeset

26 
let val (q, r) = Integer.div_mod i 2 in 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25967
diff
changeset

27 
Thm.capply (mk_cbit r) (mk_cnumeral q) 
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

28 
end; 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

29 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

30 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

31 
(* number *) 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

32 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

33 
local 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

34 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

35 
val zero = @{cpat "0"}; 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

36 
val zeroT = Thm.ctyp_of_term zero; 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

37 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

38 
val one = @{cpat "1"}; 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

39 
val oneT = Thm.ctyp_of_term one; 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

40 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

41 
val number_of = @{cpat "number_of"}; 
32010  42 
val numberT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of))); 
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

43 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

44 
fun instT T V = Thm.instantiate_cterm ([(V, T)], []); 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

45 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

46 
in 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

47 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

48 
fun mk_cnumber T 0 = instT T zeroT zero 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

49 
 mk_cnumber T 1 = instT T oneT one 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

50 
 mk_cnumber T i = Thm.capply (instT T numberT number_of) (mk_cnumeral i); 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

51 

543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

52 
end; 
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

53 

25932  54 

55 
(* code generator *) 

56 

28090
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

57 
local open Basic_Code_Thingol in 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

58 

34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34898
diff
changeset

59 
fun add_code number_of negative print target thy = 
28090
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

60 
let 
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
28708
diff
changeset

61 
fun dest_numeral pls' min' bit0' bit1' thm = 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28308
diff
changeset

62 
let 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28308
diff
changeset

63 
fun dest_bit (IConst (c, _)) = if c = bit0' then 0 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28308
diff
changeset

64 
else if c = bit1' then 1 
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32010
diff
changeset

65 
else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit" 
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32010
diff
changeset

66 
 dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"; 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28308
diff
changeset

67 
fun dest_num (IConst (c, _)) = if c = pls' then SOME 0 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28308
diff
changeset

68 
else if c = min' then 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28308
diff
changeset

69 
if negative then SOME ~1 else NONE 
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32010
diff
changeset

70 
else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit" 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28308
diff
changeset

71 
 dest_num (t1 `$ t2) = 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28308
diff
changeset

72 
let val (n, b) = (dest_num t2, dest_bit t1) 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28308
diff
changeset

73 
in case n of SOME n => SOME (2 * n + b)  NONE => NONE end 
33989
cb136b5f6050
more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents:
32010
diff
changeset

74 
 dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term"; 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28308
diff
changeset

75 
in dest_num end; 
31056
01ac77eb660b
robustifed infrastructure for complex term syntax during code generation
haftmann
parents:
28708
diff
changeset

76 
fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] = 
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34898
diff
changeset

77 
(Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t; 
28090
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

78 
in 
31375  79 
thy > Code_Target.add_syntax_const target number_of 
34898
62d70417f8ce
allow individual printing of numerals during code serialization
haftmann
parents:
33989
diff
changeset

80 
(SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min}, 
62d70417f8ce
allow individual printing of numerals during code serialization
haftmann
parents:
33989
diff
changeset

81 
@{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))) 
28090
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

82 
end; 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

83 

29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

84 
end; (*local*) 
25932  85 

23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset

86 
end; 