author  wenzelm 
Wed, 17 Sep 2008 21:27:08 +0200  
changeset 28262  aa7ca36d67fd 
parent 28090  29af3c712d2b 
child 28308  d4396a28fb29 
permissions  rwrr 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
24630
diff
changeset

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

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

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

4 

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

5 
Logical operations on numerals (see also HOL/hologic.ML). 
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 

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

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

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

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

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

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

14 

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

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

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

17 

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

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

19 

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

20 
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

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

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

23 

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

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

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

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

27 
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

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

29 
end; 
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 

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

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

33 

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

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

35 

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

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

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

38 

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

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

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

41 

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

42 
val number_of = @{cpat "number_of"}; 
28262
aa7ca36d67fd
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
wenzelm
parents:
28090
diff
changeset

43 
val numberT = Thm.ctyp_of (the_context ()) (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

44 

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

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

46 

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

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

48 

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

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

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

51 
 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

52 

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

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

54 

25932  55 

56 
(* code generator *) 

57 

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

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

59 

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

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

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

62 
val pls' = Code_Name.const thy @{const_name Int.Pls}; 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

63 
val min' = Code_Name.const thy @{const_name Int.Min}; 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

64 
val bit0' = Code_Name.const thy @{const_name Int.Bit0}; 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

65 
val bit1' = Code_Name.const thy @{const_name Int.Bit1}; 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

66 
val pr_numeral = (Code_Printer.literal_numeral o Code_Target.the_literals thy) target; 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

67 
fun dest_bit thm (IConst (c, _)) = if c = bit0' then 0 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

68 
else if c = bit1' then 1 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

69 
else Code_Printer.nerror thm "Illegal numeral expression: illegal bit" 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

70 
 dest_bit thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit"; 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

71 
fun dest_numeral thm (IConst (c, _)) = if c = pls' then SOME 0 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

72 
else if c = min' then 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

73 
if negative then SOME ~1 else NONE 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

74 
else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit" 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

75 
 dest_numeral thm (t1 `$ t2) = 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

76 
let val (n, b) = (dest_numeral thm t2, dest_bit thm t1) 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

77 
in case n of SOME n => SOME (2 * n + b)  NONE => NONE end 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

78 
 dest_numeral thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term"; 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

79 
fun pretty _ thm _ _ _ [(t, _)] = 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

80 
(Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral thm) t; 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

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

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

83 
> Code_Target.add_syntax_const target number_of (SOME (1, pretty)) 
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset

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

85 

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

86 
end; (*local*) 
25932  87 

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

88 
end; 