1(*  Title:      HOL/Tools/numeral.ML
2    Author:     Makarius
3
4Logical and syntactic operations on numerals (see also HOL/Tools/hologic.ML).
5*)
6
7signature NUMERAL =
8sig
9  val mk_cnumber: ctyp -> int -> cterm
10  val mk_number_syntax: int -> term
11  val dest_num_syntax: term -> int
12  val add_code: string -> (int -> int) -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
13end;
14
15structure Numeral: NUMERAL =
16struct
17
18(* numeral *)
19
20fun dest_num_syntax (Const (\<^const_syntax>\<open>Num.Bit0\<close>, _) $ t) = 2 * dest_num_syntax t
21  | dest_num_syntax (Const (\<^const_syntax>\<open>Num.Bit1\<close>, _) $ t) = 2 * dest_num_syntax t + 1
22  | dest_num_syntax (Const (\<^const_syntax>\<open>Num.One\<close>, _)) = 1;
23
24fun mk_num_syntax n =
25  if n > 0 then
26    (case IntInf.quotRem (n, 2) of
27      (0, 1) => Syntax.const \<^const_syntax>\<open>One\<close>
28    | (n, 0) => Syntax.const \<^const_syntax>\<open>Bit0\<close> $ mk_num_syntax n
29    | (n, 1) => Syntax.const \<^const_syntax>\<open>Bit1\<close> $ mk_num_syntax n)
30  else raise Match
31
32fun mk_cbit 0 = \<^cterm>\<open>Num.Bit0\<close>
33  | mk_cbit 1 = \<^cterm>\<open>Num.Bit1\<close>
34  | mk_cbit _ = raise CTERM ("mk_cbit", []);
35
36fun mk_cnumeral i =
37  let
38    fun mk 1 = \<^cterm>\<open>Num.One\<close>
39      | mk i =
40      let val (q, r) = Integer.div_mod i 2 in
41        Thm.apply (mk_cbit r) (mk q)
42      end
43  in
44    if i > 0 then mk i else raise CTERM ("mk_cnumeral: negative input", [])
45  end
46
47
48(* number *)
49
50local
51
52val cterm_of = Thm.cterm_of \<^context>;
53fun tvar S = (("'a", 0), S);
54
55val zero_tvar = tvar \<^sort>\<open>zero\<close>;
56val zero = cterm_of (Const (\<^const_name>\<open>zero_class.zero\<close>, TVar zero_tvar));
57
58val one_tvar = tvar \<^sort>\<open>one\<close>;
59val one = cterm_of (Const (\<^const_name>\<open>one_class.one\<close>, TVar one_tvar));
60
61val numeral_tvar = tvar \<^sort>\<open>numeral\<close>;
62val numeral = cterm_of (Const (\<^const_name>\<open>numeral\<close>, \<^typ>\<open>num\<close> --> TVar numeral_tvar));
63
64val uminus_tvar = tvar \<^sort>\<open>uminus\<close>;
65val uminus = cterm_of (Const (\<^const_name>\<open>uminus\<close>, TVar uminus_tvar --> TVar uminus_tvar));
66
67fun instT T v = Thm.instantiate_cterm ([(v, T)], []);
68
69in
70
71fun mk_cnumber T 0 = instT T zero_tvar zero
72  | mk_cnumber T 1 = instT T one_tvar one
73  | mk_cnumber T i =
74      if i > 0 then
75        Thm.apply (instT T numeral_tvar numeral) (mk_cnumeral i)
76      else
77        Thm.apply (instT T uminus_tvar uminus)
78          (Thm.apply (instT T numeral_tvar numeral) (mk_cnumeral (~ i)));
79
80end;
81
82fun mk_number_syntax n =
83  if n = 0 then Syntax.const \<^const_syntax>\<open>Groups.zero\<close>
84  else if n = 1 then Syntax.const \<^const_syntax>\<open>Groups.one\<close>
85  else Syntax.const \<^const_syntax>\<open>numeral\<close> $ mk_num_syntax n;
86
87
88(* code generator *)
89
90local open Basic_Code_Thingol in
91
92fun dest_num_code (IConst { sym = Code_Symbol.Constant \<^const_name>\<open>Num.One\<close>, ... }) = SOME 1
93  | dest_num_code (IConst { sym = Code_Symbol.Constant \<^const_name>\<open>Num.Bit0\<close>, ... } `$ t) =
94     (case dest_num_code t of
95        SOME n => SOME (2 * n)
96      | _ => NONE)
97  | dest_num_code (IConst { sym = Code_Symbol.Constant \<^const_name>\<open>Num.Bit1\<close>, ... } `$ t) =
98     (case dest_num_code t of
99        SOME n => SOME (2 * n + 1)
100      | _ => NONE)
101  | dest_num_code _ = NONE;
102
103fun add_code number_of preproc print target thy =
104  let
105    fun pretty literals _ thm _ _ [(t, _)] =
106      case dest_num_code t of
107        SOME n => (Code_Printer.str o print literals o preproc) n
108      | NONE => Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term";
109  in
110    thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,
111      [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
112  end;
113
114end; (*local*)
115
116end;
117