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