src/HOL/Tools/numeral.ML
author wenzelm
Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787 64b47495676d
parent 62597 b3f2b8c906a6
child 68028 1f9f973eed2a
permissions -rw-r--r--
obsolete;
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
51314
eac4bb5adbf9 just one HOLogic.Trueprop_conv, with regular exception CTERM;
wenzelm
parents: 48072
diff changeset
     4
Logical operations on numerals (see also HOL/Tools/hologic.ML).
23575
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_cnumber: ctyp -> int -> cterm
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 58399
diff changeset
    10
  val mk_number_syntax: int -> term
62597
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    11
  val mk_cnumeral: int -> cterm
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    12
  val mk_num_syntax: int -> term
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    13
  val dest_num_syntax: term -> int
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    14
  val dest_num: Code_Thingol.iterm -> int option
58399
haftmann
parents: 55236
diff changeset
    15
  val add_code: string -> (int -> int) -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    16
end;
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    17
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    18
structure Numeral: NUMERAL =
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    19
struct
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    20
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    21
(* numeral *)
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    22
62597
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    23
fun dest_num_syntax (Const (@{const_syntax Num.Bit0}, _) $ t) = 2 * dest_num_syntax t
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    24
  | dest_num_syntax (Const (@{const_syntax Num.Bit1}, _) $ t) = 2 * dest_num_syntax t + 1
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    25
  | dest_num_syntax (Const (@{const_syntax Num.One}, _)) = 1;
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    26
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    27
fun mk_num_syntax n =
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    28
  if n > 0 then
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    29
    (case IntInf.quotRem (n, 2) of
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    30
      (0, 1) => Syntax.const @{const_syntax One}
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    31
    | (n, 0) => Syntax.const @{const_syntax Bit0} $ mk_num_syntax n
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    32
    | (n, 1) => Syntax.const @{const_syntax Bit1} $ mk_num_syntax n)
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    33
  else raise Match
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    34
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    35
fun mk_cbit 0 = @{cterm "Num.Bit0"}
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    36
  | mk_cbit 1 = @{cterm "Num.Bit1"}
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    37
  | mk_cbit _ = raise CTERM ("mk_cbit", []);
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    38
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    39
fun mk_cnumeral i =
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    40
  let
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    41
    fun mk 1 = @{cterm "Num.One"}
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    42
      | mk i =
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 23575
diff changeset
    43
      let val (q, r) = Integer.div_mod i 2 in
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    44
        Thm.apply (mk_cbit r) (mk q)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    45
      end
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    46
  in
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    47
    if i > 0 then mk i else raise CTERM ("mk_cnumeral: negative input", [])
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    48
  end
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    49
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    50
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    51
(* number *)
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    52
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    53
local
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    54
61150
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    55
val cterm_of = Thm.cterm_of @{context};
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    56
fun tvar S = (("'a", 0), S);
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    57
61150
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    58
val zero_tvar = tvar @{sort zero};
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    59
val zero = cterm_of (Const (@{const_name zero_class.zero}, TVar zero_tvar));
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    60
61150
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    61
val one_tvar = tvar @{sort one};
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    62
val one = cterm_of (Const (@{const_name one_class.one}, TVar one_tvar));
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    63
61150
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    64
val numeral_tvar = tvar @{sort numeral};
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    65
val numeral = cterm_of (Const (@{const_name numeral}, @{typ num} --> TVar numeral_tvar));
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    66
61150
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    67
val uminus_tvar = tvar @{sort uminus};
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    68
val uminus = cterm_of (Const (@{const_name uminus}, TVar uminus_tvar --> TVar uminus_tvar));
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    69
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    70
fun instT T v = Thm.instantiate_cterm ([(v, T)], []);
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    71
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    72
in
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    73
61150
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    74
fun mk_cnumber T 0 = instT T zero_tvar zero
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    75
  | mk_cnumber T 1 = instT T one_tvar one
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    76
  | mk_cnumber T i =
61150
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    77
      if i > 0 then
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    78
        Thm.apply (instT T numeral_tvar numeral) (mk_cnumeral i)
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    79
      else
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    80
        Thm.apply (instT T uminus_tvar uminus)
d85d8f5e921b tuned -- avoid slightly odd @{cpat};
wenzelm
parents: 60642
diff changeset
    81
          (Thm.apply (instT T numeral_tvar numeral) (mk_cnumeral (~ i)));
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    82
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    83
end;
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    84
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 58399
diff changeset
    85
fun mk_number_syntax n =
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 58399
diff changeset
    86
  if n = 0 then Syntax.const @{const_syntax Groups.zero}
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 58399
diff changeset
    87
  else if n = 1 then Syntax.const @{const_syntax Groups.one}
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 58399
diff changeset
    88
  else Syntax.const @{const_syntax numeral} $ mk_num_syntax n;
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 58399
diff changeset
    89
25932
db0fd0ecdcd4 explicit auxiliary function for code setup
haftmann
parents: 25919
diff changeset
    90
db0fd0ecdcd4 explicit auxiliary function for code setup
haftmann
parents: 25919
diff changeset
    91
(* code generator *)
db0fd0ecdcd4 explicit auxiliary function for code setup
haftmann
parents: 25919
diff changeset
    92
28090
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    93
local open Basic_Code_Thingol in
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    94
62597
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    95
fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = SOME 1
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    96
  | dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... } `$ t) =
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    97
     (case dest_num t of
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    98
        SOME n => SOME (2 * n)
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
    99
      | _ => NONE)
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
   100
  | dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... } `$ t) =
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
   101
     (case dest_num t of
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
   102
        SOME n => SOME (2 * n + 1)
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
   103
      | _ => NONE)
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
   104
  | dest_num _ = NONE;
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
   105
58399
haftmann
parents: 55236
diff changeset
   106
fun add_code number_of preproc print target thy =
28090
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
   107
  let
58399
haftmann
parents: 55236
diff changeset
   108
    fun pretty literals _ thm _ _ [(t, _)] =
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28308
diff changeset
   109
      let
62597
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
   110
        val n = case dest_num t of
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
   111
          SOME n => n
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
   112
        | NONE => Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term"
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61150
diff changeset
   113
      in (Code_Printer.str o print literals o preproc) n end;
28090
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
   114
  in
52435
6646bb548c6b migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents: 51314
diff changeset
   115
    thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,
55148
7e1b7cb54114 avoid (now superfluous) indirect passing of constant names
haftmann
parents: 55147
diff changeset
   116
      [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
28090
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
   117
  end;
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
   118
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
   119
end; (*local*)
25932
db0fd0ecdcd4 explicit auxiliary function for code setup
haftmann
parents: 25919
diff changeset
   120
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
   121
end;