src/HOL/Tools/numeral.ML
author haftmann
Tue Jun 05 07:05:56 2012 +0200 (2012-06-05)
changeset 48072 ace701efe203
parent 47108 2a1953f0d20d
child 51314 eac4bb5adbf9
permissions -rw-r--r--
prefer records with speaking labels over deeply nested tuples
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@47108
    19
fun mk_cbit 0 = @{cterm "Num.Bit0"}
huffman@47108
    20
  | mk_cbit 1 = @{cterm "Num.Bit1"}
wenzelm@23575
    21
  | mk_cbit _ = raise CTERM ("mk_cbit", []);
wenzelm@23575
    22
huffman@47108
    23
fun mk_cnumeral i =
huffman@47108
    24
  let
huffman@47108
    25
    fun mk 1 = @{cterm "Num.One"}
huffman@47108
    26
      | mk i =
wenzelm@24630
    27
      let val (q, r) = Integer.div_mod i 2 in
huffman@47108
    28
        Thm.apply (mk_cbit r) (mk q)
huffman@47108
    29
      end
huffman@47108
    30
  in
huffman@47108
    31
    if i > 0 then mk i else raise CTERM ("mk_cnumeral: negative input", [])
huffman@47108
    32
  end
wenzelm@23575
    33
wenzelm@23575
    34
wenzelm@23575
    35
(* number *)
wenzelm@23575
    36
wenzelm@23575
    37
local
wenzelm@23575
    38
wenzelm@23575
    39
val zero = @{cpat "0"};
wenzelm@23575
    40
val zeroT = Thm.ctyp_of_term zero;
wenzelm@23575
    41
wenzelm@23575
    42
val one = @{cpat "1"};
wenzelm@23575
    43
val oneT = Thm.ctyp_of_term one;
wenzelm@23575
    44
huffman@47108
    45
val numeral = @{cpat "numeral"};
huffman@47108
    46
val numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term numeral)));
huffman@47108
    47
huffman@47108
    48
val neg_numeral = @{cpat "neg_numeral"};
huffman@47108
    49
val neg_numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term neg_numeral)));
wenzelm@23575
    50
wenzelm@23575
    51
fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
wenzelm@23575
    52
wenzelm@23575
    53
in
wenzelm@23575
    54
wenzelm@23575
    55
fun mk_cnumber T 0 = instT T zeroT zero
wenzelm@23575
    56
  | mk_cnumber T 1 = instT T oneT one
huffman@47108
    57
  | mk_cnumber T i =
huffman@47108
    58
    if i > 0 then Thm.apply (instT T numeralT numeral) (mk_cnumeral i)
huffman@47108
    59
    else Thm.apply (instT T neg_numeralT neg_numeral) (mk_cnumeral (~i));
wenzelm@23575
    60
wenzelm@23575
    61
end;
wenzelm@23575
    62
haftmann@25932
    63
haftmann@25932
    64
(* code generator *)
haftmann@25932
    65
haftmann@28090
    66
local open Basic_Code_Thingol in
haftmann@28090
    67
haftmann@34944
    68
fun add_code number_of negative print target thy =
haftmann@28090
    69
  let
huffman@47108
    70
    fun dest_numeral one' bit0' bit1' thm t =
haftmann@28663
    71
      let
haftmann@48072
    72
        fun dest_bit (IConst { name = c, ... }) = if c = bit0' then 0
haftmann@28663
    73
              else if c = bit1' then 1
haftmann@33989
    74
              else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"
haftmann@33989
    75
          | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
haftmann@48072
    76
        fun dest_num (IConst { name = c, ... }) = if c = one' then 1
haftmann@33989
    77
              else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
huffman@47108
    78
          | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
haftmann@33989
    79
          | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
huffman@47108
    80
      in if negative then ~ (dest_num t) else dest_num t end;
huffman@47108
    81
    fun pretty literals [one', bit0', bit1'] _ thm _ _ [(t, _)] =
huffman@47108
    82
      (Code_Printer.str o print literals o dest_numeral one' bit0' bit1' thm) t;
haftmann@28090
    83
  in
haftmann@38923
    84
    thy |> Code_Target.add_const_syntax target number_of
huffman@47108
    85
      (SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Num.One},
huffman@47108
    86
        @{const_name Num.Bit0}, @{const_name Num.Bit1}], pretty))))
haftmann@28090
    87
  end;
haftmann@28090
    88
haftmann@28090
    89
end; (*local*)
haftmann@25932
    90
wenzelm@23575
    91
end;