src/HOL/Tools/numeral.ML
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58410 6d46ad54a2ab
child 59586 ddf6deaadfe8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 (*  Title:      HOL/Tools/numeral.ML
     2     Author:     Makarius
     3 
     4 Logical operations on numerals (see also HOL/Tools/hologic.ML).
     5 *)
     6 
     7 signature NUMERAL =
     8 sig
     9   val mk_cnumeral: int -> cterm
    10   val mk_cnumber: ctyp -> int -> cterm
    11   val mk_number_syntax: int -> term
    12   val add_code: string -> (int -> int) -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
    13 end;
    14 
    15 structure Numeral: NUMERAL =
    16 struct
    17 
    18 (* numeral *)
    19 
    20 fun mk_cbit 0 = @{cterm "Num.Bit0"}
    21   | mk_cbit 1 = @{cterm "Num.Bit1"}
    22   | mk_cbit _ = raise CTERM ("mk_cbit", []);
    23 
    24 fun mk_cnumeral i =
    25   let
    26     fun mk 1 = @{cterm "Num.One"}
    27       | mk i =
    28       let val (q, r) = Integer.div_mod i 2 in
    29         Thm.apply (mk_cbit r) (mk q)
    30       end
    31   in
    32     if i > 0 then mk i else raise CTERM ("mk_cnumeral: negative input", [])
    33   end
    34 
    35 
    36 (* number *)
    37 
    38 local
    39 
    40 val zero = @{cpat "0"};
    41 val zeroT = Thm.ctyp_of_term zero;
    42 
    43 val one = @{cpat "1"};
    44 val oneT = Thm.ctyp_of_term one;
    45 
    46 val numeral = @{cpat "numeral"};
    47 val numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term numeral)));
    48 
    49 val uminus = @{cpat "uminus"};
    50 val uminusT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term uminus)));
    51 
    52 fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
    53 
    54 in
    55 
    56 fun mk_cnumber T 0 = instT T zeroT zero
    57   | mk_cnumber T 1 = instT T oneT one
    58   | mk_cnumber T i =
    59     if i > 0 then Thm.apply (instT T numeralT numeral) (mk_cnumeral i)
    60     else Thm.apply (instT T uminusT uminus) (Thm.apply (instT T numeralT numeral) (mk_cnumeral (~i)));
    61 
    62 end;
    63 
    64 fun mk_num_syntax n =
    65   if n > 0 then
    66     (case IntInf.quotRem (n, 2) of
    67       (0, 1) => Syntax.const @{const_syntax One}
    68     | (n, 0) => Syntax.const @{const_syntax Bit0} $ mk_num_syntax n
    69     | (n, 1) => Syntax.const @{const_syntax Bit1} $ mk_num_syntax n)
    70   else raise Match
    71 
    72 fun mk_number_syntax n =
    73   if n = 0 then Syntax.const @{const_syntax Groups.zero}
    74   else if n = 1 then Syntax.const @{const_syntax Groups.one}
    75   else Syntax.const @{const_syntax numeral} $ mk_num_syntax n;
    76 
    77 
    78 (* code generator *)
    79 
    80 local open Basic_Code_Thingol in
    81 
    82 fun add_code number_of preproc print target thy =
    83   let
    84     fun pretty literals _ thm _ _ [(t, _)] =
    85       let
    86         fun dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... }) = 0
    87           | dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... }) = 1
    88           | dest_bit _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal bit";
    89         fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = 1
    90           | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
    91           | dest_num _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term";
    92       in (Code_Printer.str o print literals o preproc o dest_num) t end;
    93   in
    94     thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,
    95       [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
    96   end;
    97 
    98 end; (*local*)
    99 
   100 end;