src/HOL/Tools/numeral.ML
author haftmann
Sat Jan 25 23:50:49 2014 +0100 (2014-01-25)
changeset 55147 bce3dbc11f95
parent 54489 03ff4d1e6784
child 55148 7e1b7cb54114
permissions -rw-r--r--
prefer explicit code symbol type over ad-hoc name mangling
     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 add_code: string -> bool -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
    12 end;
    13 
    14 structure Numeral: NUMERAL =
    15 struct
    16 
    17 (* numeral *)
    18 
    19 fun mk_cbit 0 = @{cterm "Num.Bit0"}
    20   | mk_cbit 1 = @{cterm "Num.Bit1"}
    21   | mk_cbit _ = raise CTERM ("mk_cbit", []);
    22 
    23 fun mk_cnumeral i =
    24   let
    25     fun mk 1 = @{cterm "Num.One"}
    26       | mk i =
    27       let val (q, r) = Integer.div_mod i 2 in
    28         Thm.apply (mk_cbit r) (mk q)
    29       end
    30   in
    31     if i > 0 then mk i else raise CTERM ("mk_cnumeral: negative input", [])
    32   end
    33 
    34 
    35 (* number *)
    36 
    37 local
    38 
    39 val zero = @{cpat "0"};
    40 val zeroT = Thm.ctyp_of_term zero;
    41 
    42 val one = @{cpat "1"};
    43 val oneT = Thm.ctyp_of_term one;
    44 
    45 val numeral = @{cpat "numeral"};
    46 val numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term numeral)));
    47 
    48 val uminus = @{cpat "uminus"};
    49 val uminusT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term uminus)));
    50 
    51 fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
    52 
    53 in
    54 
    55 fun mk_cnumber T 0 = instT T zeroT zero
    56   | mk_cnumber T 1 = instT T oneT one
    57   | mk_cnumber T i =
    58     if i > 0 then Thm.apply (instT T numeralT numeral) (mk_cnumeral i)
    59     else Thm.apply (instT T uminusT uminus) (Thm.apply (instT T numeralT numeral) (mk_cnumeral (~i)));
    60 
    61 end;
    62 
    63 
    64 (* code generator *)
    65 
    66 local open Basic_Code_Thingol in
    67 
    68 fun add_code number_of negative print target thy =
    69   let
    70     fun dest_numeral one' bit0' bit1' thm t =
    71       let
    72         fun dest_bit (IConst { sym = Code_Symbol.Constant c, ... }) = if c = bit0' then 0
    73               else if c = bit1' then 1
    74               else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"
    75           | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
    76         fun dest_num (IConst { sym = Code_Symbol.Constant c, ... }) = if c = one' then 1
    77               else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
    78           | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
    79           | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
    80       in if negative then ~ (dest_num t) else dest_num t end;
    81     fun pretty literals [one', bit0', bit1'] _ thm _ _ [(t, _)] =
    82       (Code_Printer.str o print literals o dest_numeral one' bit0' bit1' thm) t;
    83   in
    84     thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,
    85       [(target, SOME (Code_Printer.complex_const_syntax
    86         (1, ([@{const_name Num.One}, @{const_name Num.Bit0}, @{const_name Num.Bit1}], pretty))))]))
    87   end;
    88 
    89 end; (*local*)
    90 
    91 end;