tuned
authorhaftmann
Thu Sep 18 18:48:04 2014 +0200 (2014-09-18)
changeset 58399c5430cf9aa87
parent 58398 f38717f175d9
child 58400 d0d3c30806b4
tuned
src/HOL/Code_Numeral.thy
src/HOL/Tools/numeral.ML
     1.1 --- a/src/HOL/Code_Numeral.thy	Thu Sep 18 18:48:04 2014 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Thu Sep 18 18:48:04 2014 +0200
     1.3 @@ -544,13 +544,10 @@
     1.4      and (Scala) "BigInt(0)"
     1.5  
     1.6  setup {*
     1.7 -  fold (Numeral.add_code @{const_name Code_Numeral.Pos}
     1.8 -    false Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
     1.9 -*}
    1.10 -
    1.11 -setup {*
    1.12 -  fold (Numeral.add_code @{const_name Code_Numeral.Neg}
    1.13 -    true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
    1.14 +  fold (fn target =>
    1.15 +    Numeral.add_code @{const_name Code_Numeral.Pos} I Code_Printer.literal_numeral target
    1.16 +    #> Numeral.add_code @{const_name Code_Numeral.Neg} (op ~) Code_Printer.literal_numeral target)
    1.17 +    ["SML", "OCaml", "Haskell", "Scala"]
    1.18  *}
    1.19  
    1.20  code_printing
     2.1 --- a/src/HOL/Tools/numeral.ML	Thu Sep 18 18:48:04 2014 +0200
     2.2 +++ b/src/HOL/Tools/numeral.ML	Thu Sep 18 18:48:04 2014 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  sig
     2.5    val mk_cnumeral: int -> cterm
     2.6    val mk_cnumber: ctyp -> int -> cterm
     2.7 -  val add_code: string -> bool -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
     2.8 +  val add_code: string -> (int -> int) -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
     2.9  end;
    2.10  
    2.11  structure Numeral: NUMERAL =
    2.12 @@ -65,9 +65,9 @@
    2.13  
    2.14  local open Basic_Code_Thingol in
    2.15  
    2.16 -fun add_code number_of negative print target thy =
    2.17 +fun add_code number_of preproc print target thy =
    2.18    let
    2.19 -    fun dest_numeral thm t =
    2.20 +    fun pretty literals _ thm _ _ [(t, _)] =
    2.21        let
    2.22          fun dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... }) = 0
    2.23            | dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... }) = 1
    2.24 @@ -75,9 +75,7 @@
    2.25          fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = 1
    2.26            | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
    2.27            | dest_num _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term";
    2.28 -      in if negative then ~ (dest_num t) else dest_num t end;
    2.29 -    fun pretty literals _ thm _ _ [(t, _)] =
    2.30 -      (Code_Printer.str o print literals o dest_numeral thm) t;
    2.31 +      in (Code_Printer.str o print literals o preproc o dest_num) t end;
    2.32    in
    2.33      thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,
    2.34        [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))