src/HOL/Tools/numeral.ML
author haftmann
Tue, 05 Jun 2012 07:05:56 +0200
changeset 48072 ace701efe203
parent 47108 2a1953f0d20d
child 51314 eac4bb5adbf9
permissions -rw-r--r--
prefer records with speaking labels over deeply nested tuples
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
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    19
fun mk_cbit 0 = @{cterm "Num.Bit0"}
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    20
  | mk_cbit 1 = @{cterm "Num.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
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    23
fun mk_cnumeral i =
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    24
  let
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    25
    fun mk 1 = @{cterm "Num.One"}
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    26
      | mk i =
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 23575
diff changeset
    27
      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
    28
        Thm.apply (mk_cbit r) (mk q)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    29
      end
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    30
  in
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    31
    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
    32
  end
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    33
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
(* number *)
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    36
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    37
local
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    38
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    39
val zero = @{cpat "0"};
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    40
val zeroT = Thm.ctyp_of_term zero;
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    41
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    42
val one = @{cpat "1"};
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    43
val oneT = Thm.ctyp_of_term one;
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    44
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    45
val numeral = @{cpat "numeral"};
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    46
val numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term numeral)));
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    47
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    48
val neg_numeral = @{cpat "neg_numeral"};
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    49
val neg_numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term neg_numeral)));
23575
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
fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
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
in
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    54
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    55
fun mk_cnumber T 0 = instT T zeroT zero
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    56
  | mk_cnumber T 1 = instT T oneT one
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    57
  | mk_cnumber T i =
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    58
    if i > 0 then Thm.apply (instT T numeralT numeral) (mk_cnumeral i)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    59
    else Thm.apply (instT T neg_numeralT neg_numeral) (mk_cnumeral (~i));
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    60
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    61
end;
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    62
25932
db0fd0ecdcd4 explicit auxiliary function for code setup
haftmann
parents: 25919
diff changeset
    63
db0fd0ecdcd4 explicit auxiliary function for code setup
haftmann
parents: 25919
diff changeset
    64
(* code generator *)
db0fd0ecdcd4 explicit auxiliary function for code setup
haftmann
parents: 25919
diff changeset
    65
28090
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    66
local open Basic_Code_Thingol in
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    67
34944
970e1466028d code literals: distinguish numeral classes by different entries
haftmann
parents: 34898
diff changeset
    68
fun add_code number_of negative print target thy =
28090
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    69
  let
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    70
    fun dest_numeral one' bit0' bit1' thm t =
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28308
diff changeset
    71
      let
48072
ace701efe203 prefer records with speaking labels over deeply nested tuples
haftmann
parents: 47108
diff changeset
    72
        fun dest_bit (IConst { name = c, ... }) = if c = bit0' then 0
28663
bd8438543bf2 code identifier namings are no longer imperative
haftmann
parents: 28308
diff changeset
    73
              else if c = bit1' then 1
33989
cb136b5f6050 more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents: 32010
diff changeset
    74
              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
    75
          | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
48072
ace701efe203 prefer records with speaking labels over deeply nested tuples
haftmann
parents: 47108
diff changeset
    76
        fun dest_num (IConst { name = c, ... }) = if c = one' then 1
33989
cb136b5f6050 more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents: 32010
diff changeset
    77
              else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    78
          | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
33989
cb136b5f6050 more speaking function names for Code_Printer; added doublesemicolon
haftmann
parents: 32010
diff changeset
    79
          | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    80
      in if negative then ~ (dest_num t) else dest_num t end;
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    81
    fun pretty literals [one', bit0', bit1'] _ thm _ _ [(t, _)] =
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    82
      (Code_Printer.str o print literals o dest_numeral one' bit0' bit1' thm) t;
28090
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    83
  in
38923
79d7f2b4cf71 more coherent naming of syntax data structures
haftmann
parents: 37881
diff changeset
    84
    thy |> Code_Target.add_const_syntax target number_of
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    85
      (SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Num.One},
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    86
        @{const_name Num.Bit0}, @{const_name Num.Bit1}], pretty))))
28090
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    87
  end;
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    88
29af3c712d2b distributed literal code generation out of central infrastructure
haftmann
parents: 28064
diff changeset
    89
end; (*local*)
25932
db0fd0ecdcd4 explicit auxiliary function for code setup
haftmann
parents: 25919
diff changeset
    90
23575
543803006b3f Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff changeset
    91
end;