src/HOL/Tools/numeral.ML
author haftmann
Wed Dec 08 13:34:50 2010 +0100 (2010-12-08)
changeset 41075 4bed56dc95fb
parent 38923 79d7f2b4cf71
child 46497 89ccf66aa73d
permissions -rw-r--r--
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann@28308
     1
(*  Title:      HOL/Tools/numeral.ML
wenzelm@23575
     2
    Author:     Makarius
wenzelm@23575
     3
wenzelm@23575
     4
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm@23575
     5
*)
wenzelm@23575
     6
wenzelm@23575
     7
signature NUMERAL =
wenzelm@23575
     8
sig
wenzelm@24630
     9
  val mk_cnumeral: int -> cterm
wenzelm@24630
    10
  val mk_cnumber: ctyp -> int -> cterm
haftmann@34944
    11
  val add_code: string -> bool -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
wenzelm@23575
    12
end;
wenzelm@23575
    13
wenzelm@23575
    14
structure Numeral: NUMERAL =
wenzelm@23575
    15
struct
wenzelm@23575
    16
wenzelm@23575
    17
(* numeral *)
wenzelm@23575
    18
huffman@26086
    19
fun mk_cbit 0 = @{cterm "Int.Bit0"}
huffman@26086
    20
  | mk_cbit 1 = @{cterm "Int.Bit1"}
wenzelm@23575
    21
  | mk_cbit _ = raise CTERM ("mk_cbit", []);
wenzelm@23575
    22
haftmann@25919
    23
fun mk_cnumeral 0 = @{cterm "Int.Pls"}
haftmann@25919
    24
  | mk_cnumeral ~1 = @{cterm "Int.Min"}
wenzelm@23575
    25
  | mk_cnumeral i =
wenzelm@24630
    26
      let val (q, r) = Integer.div_mod i 2 in
huffman@26086
    27
        Thm.capply (mk_cbit r) (mk_cnumeral q)
wenzelm@23575
    28
      end;
wenzelm@23575
    29
wenzelm@23575
    30
wenzelm@23575
    31
(* number *)
wenzelm@23575
    32
wenzelm@23575
    33
local
wenzelm@23575
    34
wenzelm@23575
    35
val zero = @{cpat "0"};
wenzelm@23575
    36
val zeroT = Thm.ctyp_of_term zero;
wenzelm@23575
    37
wenzelm@23575
    38
val one = @{cpat "1"};
wenzelm@23575
    39
val oneT = Thm.ctyp_of_term one;
wenzelm@23575
    40
wenzelm@23575
    41
val number_of = @{cpat "number_of"};
wenzelm@32010
    42
val numberT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of)));
wenzelm@23575
    43
wenzelm@23575
    44
fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
wenzelm@23575
    45
wenzelm@23575
    46
in
wenzelm@23575
    47
wenzelm@23575
    48
fun mk_cnumber T 0 = instT T zeroT zero
wenzelm@23575
    49
  | mk_cnumber T 1 = instT T oneT one
wenzelm@23575
    50
  | mk_cnumber T i = Thm.capply (instT T numberT number_of) (mk_cnumeral i);
wenzelm@23575
    51
wenzelm@23575
    52
end;
wenzelm@23575
    53
haftmann@25932
    54
haftmann@25932
    55
(* code generator *)
haftmann@25932
    56
haftmann@28090
    57
local open Basic_Code_Thingol in
haftmann@28090
    58
haftmann@34944
    59
fun add_code number_of negative print target thy =
haftmann@28090
    60
  let
haftmann@31056
    61
    fun dest_numeral pls' min' bit0' bit1' thm =
haftmann@28663
    62
      let
haftmann@28663
    63
        fun dest_bit (IConst (c, _)) = if c = bit0' then 0
haftmann@28663
    64
              else if c = bit1' then 1
haftmann@33989
    65
              else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"
haftmann@33989
    66
          | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
haftmann@28663
    67
        fun dest_num (IConst (c, _)) = if c = pls' then SOME 0
haftmann@28663
    68
              else if c = min' then
haftmann@28663
    69
                if negative then SOME ~1 else NONE
haftmann@33989
    70
              else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
haftmann@28663
    71
          | dest_num (t1 `$ t2) =
haftmann@28663
    72
              let val (n, b) = (dest_num t2, dest_bit t1)
haftmann@28663
    73
              in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
haftmann@33989
    74
          | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
haftmann@28663
    75
      in dest_num end;
haftmann@31056
    76
    fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
haftmann@34944
    77
      (Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
haftmann@28090
    78
  in
haftmann@38923
    79
    thy |> Code_Target.add_const_syntax target number_of
haftmann@37881
    80
      (SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
haftmann@37881
    81
        @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))))
haftmann@28090
    82
  end;
haftmann@28090
    83
haftmann@28090
    84
end; (*local*)
haftmann@25932
    85
wenzelm@23575
    86
end;