src/HOL/Tools/numeral.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 34944 970e1466028d
child 37881 096c8397c989
permissions -rw-r--r--
tuned titles
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28308
d4396a28fb29 fixed headers
haftmann
parents: 28262
diff changeset
     1
(*  Title:      HOL/Tools/numeral.ML
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
     3
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
     4
Logical operations on numerals (see also HOL/hologic.ML).
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
     5
*)
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
signature NUMERAL =
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
     8
sig
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 23575
diff changeset
     9
  val mk_cnumeral: int -> cterm
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 23575
diff changeset
    10
  val mk_cnumber: ctyp -> int -> cterm
34944
970e1466028d code literals: distinguish numeral classes by different entries
haftmann
parents: 34898
diff changeset
    11
  val add_code: string -> bool -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    12
end;
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    13
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    14
structure Numeral: NUMERAL =
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    15
struct
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    16
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    17
(* numeral *)
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    18
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25967
diff changeset
    19
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
    20
  | mk_cbit 1 = @{cterm "Int.Bit1"}
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    21
  | mk_cbit _ = raise CTERM ("mk_cbit", []);
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    22
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 24630
diff changeset
    23
fun mk_cnumeral 0 = @{cterm "Int.Pls"}
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 24630
diff changeset
    24
  | mk_cnumeral ~1 = @{cterm "Int.Min"}
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    25
  | mk_cnumeral i =
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 23575
diff changeset
    26
      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
    27
        Thm.capply (mk_cbit r) (mk_cnumeral q)
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    28
      end;
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    29
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
(* number *)
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    32
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    33
local
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    34
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    35
val zero = @{cpat "0"};
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    36
val zeroT = Thm.ctyp_of_term zero;
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    37
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    38
val one = @{cpat "1"};
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    39
val oneT = Thm.ctyp_of_term one;
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    40
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    41
val number_of = @{cpat "number_of"};
32010
cb1a1c94b4cd more antiquotations;
wenzelm
parents: 31375
diff changeset
    42
val numberT = Thm.ctyp_of @{theory} (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
    43
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    44
fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    45
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    46
in
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    47
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    48
fun mk_cnumber T 0 = instT T zeroT zero
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    49
  | mk_cnumber T 1 = instT T oneT one
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    50
  | 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
    51
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    52
end;
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    53
25932
db0fd0ecdcd4 explicit auxiliary function for code setup
haftmann
parents: 25919
diff changeset
    54
db0fd0ecdcd4 explicit auxiliary function for code setup
haftmann
parents: 25919
diff changeset
    55
(* code generator *)
db0fd0ecdcd4 explicit auxiliary function for code setup
haftmann
parents: 25919
diff changeset
    56
28090
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    57
local open Basic_Code_Thingol in
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    58
34944
970e1466028d code literals: distinguish numeral classes by different entries
haftmann
parents: 34898
diff changeset
    59
fun add_code number_of negative print target thy =
28090
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    60
  let
31056
01ac77eb660b robustifed infrastructure for complex term syntax during code generation
haftmann
parents: 28708
diff changeset
    61
    fun dest_numeral pls' min' bit0' bit1' thm =
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28308
diff changeset
    62
      let
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28308
diff changeset
    63
        fun dest_bit (IConst (c, _)) = if c = bit0' then 0
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28308
diff changeset
    64
              else if c = bit1' then 1
33989
cb136b5f6050 more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents: 32010
diff changeset
    65
              else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"
cb136b5f6050 more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents: 32010
diff changeset
    66
          | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28308
diff changeset
    67
        fun dest_num (IConst (c, _)) = if c = pls' then SOME 0
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28308
diff changeset
    68
              else if c = min' then
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28308
diff changeset
    69
                if negative then SOME ~1 else NONE
33989
cb136b5f6050 more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents: 32010
diff changeset
    70
              else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28308
diff changeset
    71
          | dest_num (t1 `$ t2) =
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28308
diff changeset
    72
              let val (n, b) = (dest_num t2, dest_bit t1)
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28308
diff changeset
    73
              in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
33989
cb136b5f6050 more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents: 32010
diff changeset
    74
          | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28308
diff changeset
    75
      in dest_num end;
31056
01ac77eb660b robustifed infrastructure for complex term syntax during code generation
haftmann
parents: 28708
diff changeset
    76
    fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
34944
970e1466028d code literals: distinguish numeral classes by different entries
haftmann
parents: 34898
diff changeset
    77
      (Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
28090
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    78
  in
31375
815426e7dd3b tuned whitespace
haftmann
parents: 31056
diff changeset
    79
    thy |> Code_Target.add_syntax_const target number_of
34898
62d70417f8ce allow individual printing of numerals during code serialization
haftmann
parents: 33989
diff changeset
    80
      (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
62d70417f8ce allow individual printing of numerals during code serialization
haftmann
parents: 33989
diff changeset
    81
        @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
28090
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    82
  end;
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    83
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    84
end; (*local*)
25932
db0fd0ecdcd4 explicit auxiliary function for code setup
haftmann
parents: 25919
diff changeset
    85
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    86
end;