src/HOL/Tools/numeral.ML
author haftmann
Wed Dec 08 13:34:50 2010 +0100 (2010-12-08)
changeset 41075 4bed56dc95fb
parent 38923 79d7f2b4cf71
child 46497 89ccf66aa73d
permissions -rw-r--r--
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
     1 (*  Title:      HOL/Tools/numeral.ML
     2     Author:     Makarius
     3 
     4 Logical operations on numerals (see also HOL/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 "Int.Bit0"}
    20   | mk_cbit 1 = @{cterm "Int.Bit1"}
    21   | mk_cbit _ = raise CTERM ("mk_cbit", []);
    22 
    23 fun mk_cnumeral 0 = @{cterm "Int.Pls"}
    24   | mk_cnumeral ~1 = @{cterm "Int.Min"}
    25   | mk_cnumeral i =
    26       let val (q, r) = Integer.div_mod i 2 in
    27         Thm.capply (mk_cbit r) (mk_cnumeral q)
    28       end;
    29 
    30 
    31 (* number *)
    32 
    33 local
    34 
    35 val zero = @{cpat "0"};
    36 val zeroT = Thm.ctyp_of_term zero;
    37 
    38 val one = @{cpat "1"};
    39 val oneT = Thm.ctyp_of_term one;
    40 
    41 val number_of = @{cpat "number_of"};
    42 val numberT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of)));
    43 
    44 fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
    45 
    46 in
    47 
    48 fun mk_cnumber T 0 = instT T zeroT zero
    49   | mk_cnumber T 1 = instT T oneT one
    50   | mk_cnumber T i = Thm.capply (instT T numberT number_of) (mk_cnumeral i);
    51 
    52 end;
    53 
    54 
    55 (* code generator *)
    56 
    57 local open Basic_Code_Thingol in
    58 
    59 fun add_code number_of negative print target thy =
    60   let
    61     fun dest_numeral pls' min' bit0' bit1' thm =
    62       let
    63         fun dest_bit (IConst (c, _)) = if c = bit0' then 0
    64               else if c = bit1' then 1
    65               else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"
    66           | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
    67         fun dest_num (IConst (c, _)) = if c = pls' then SOME 0
    68               else if c = min' then
    69                 if negative then SOME ~1 else NONE
    70               else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
    71           | dest_num (t1 `$ t2) =
    72               let val (n, b) = (dest_num t2, dest_bit t1)
    73               in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
    74           | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
    75       in dest_num end;
    76     fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
    77       (Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
    78   in
    79     thy |> Code_Target.add_const_syntax target number_of
    80       (SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
    81         @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))))
    82   end;
    83 
    84 end; (*local*)
    85 
    86 end;