src/HOL/Tools/numeral.ML
changeset 34944 970e1466028d
parent 34898 62d70417f8ce
child 37881 096c8397c989
equal deleted inserted replaced
34943:e97b22500a5c 34944:970e1466028d
     6 
     6 
     7 signature NUMERAL =
     7 signature NUMERAL =
     8 sig
     8 sig
     9   val mk_cnumeral: int -> cterm
     9   val mk_cnumeral: int -> cterm
    10   val mk_cnumber: ctyp -> int -> cterm
    10   val mk_cnumber: ctyp -> int -> cterm
    11   val add_code: string -> bool -> bool -> (string -> Pretty.T) -> string -> theory -> theory
    11   val add_code: string -> bool -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
    12 end;
    12 end;
    13 
    13 
    14 structure Numeral: NUMERAL =
    14 structure Numeral: NUMERAL =
    15 struct
    15 struct
    16 
    16 
    54 
    54 
    55 (* code generator *)
    55 (* code generator *)
    56 
    56 
    57 local open Basic_Code_Thingol in
    57 local open Basic_Code_Thingol in
    58 
    58 
    59 fun add_code number_of negative unbounded print target thy =
    59 fun add_code number_of negative print target thy =
    60   let
    60   let
    61     fun dest_numeral pls' min' bit0' bit1' thm =
    61     fun dest_numeral pls' min' bit0' bit1' thm =
    62       let
    62       let
    63         fun dest_bit (IConst (c, _)) = if c = bit0' then 0
    63         fun dest_bit (IConst (c, _)) = if c = bit0' then 0
    64               else if c = bit1' then 1
    64               else if c = bit1' then 1
    72               let val (n, b) = (dest_num t2, dest_bit t1)
    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
    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";
    74           | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
    75       in dest_num end;
    75       in dest_num end;
    76     fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
    76     fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
    77       (print o Code_Printer.literal_numeral literals unbounded
    77       (Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
    78         o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
       
    79   in
    78   in
    80     thy |> Code_Target.add_syntax_const target number_of
    79     thy |> Code_Target.add_syntax_const target number_of
    81       (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
    80       (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
    82         @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
    81         @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
    83   end;
    82   end;