allow individual printing of numerals during code serialization
authorhaftmann
Thu Jan 14 17:47:38 2010 +0100 (2010-01-14)
changeset 3489862d70417f8ce
parent 34895 19fd499cddff
child 34899 8674bb6f727b
allow individual printing of numerals during code serialization
src/HOL/Code_Numeral.thy
src/HOL/Tools/numeral.ML
     1.1 --- a/src/HOL/Code_Numeral.thy	Wed Jan 13 12:20:37 2010 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Thu Jan 14 17:47:38 2010 +0100
     1.3 @@ -296,8 +296,11 @@
     1.4  
     1.5  setup {*
     1.6    fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
     1.7 -    false false) ["SML", "Haskell", "Scala"]
     1.8 -  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} false true "OCaml"
     1.9 +    false false Code_Printer.str) ["SML", "Haskell"]
    1.10 +  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.11 +    false true Code_Printer.str "OCaml"
    1.12 +  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.13 +    false false Code_Printer.str "Scala"
    1.14  *}
    1.15  
    1.16  code_reserved SML Int int
    1.17 @@ -323,9 +326,10 @@
    1.18    (Scala infixl 8 "*")
    1.19  
    1.20  code_const div_mod_code_numeral
    1.21 -  (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
    1.22 -  (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))")
    1.23 +  (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
    1.24 +  (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
    1.25    (Haskell "divMod")
    1.26 +  (Scala "!((n: Int) => (m: Int) =>/ if (m == 0)/ (0, n) else/ (n '/ m, n % m))")
    1.27  
    1.28  code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.29    (SML "!((_ : Int.int) = _)")
    1.30 @@ -337,12 +341,12 @@
    1.31    (SML "Int.<=/ ((_),/ (_))")
    1.32    (OCaml "Big'_int.le'_big'_int")
    1.33    (Haskell infix 4 "<=")
    1.34 -  (Scala infix 4 "<=")
    1.35 +  (Scala infixl 4 "<=")
    1.36  
    1.37  code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.38    (SML "Int.</ ((_),/ (_))")
    1.39    (OCaml "Big'_int.lt'_big'_int")
    1.40    (Haskell infix 4 "<")
    1.41 -  (Scala infix 4 "<")
    1.42 +  (Scala infixl 4 "<")
    1.43  
    1.44  end
     2.1 --- a/src/HOL/Tools/numeral.ML	Wed Jan 13 12:20:37 2010 +0100
     2.2 +++ b/src/HOL/Tools/numeral.ML	Thu Jan 14 17:47:38 2010 +0100
     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 -> bool -> string -> theory -> theory
     2.8 +  val add_code: string -> bool -> bool -> (string -> Pretty.T) -> string -> theory -> theory
     2.9  end;
    2.10  
    2.11  structure Numeral: NUMERAL =
    2.12 @@ -56,7 +56,7 @@
    2.13  
    2.14  local open Basic_Code_Thingol in
    2.15  
    2.16 -fun add_code number_of negative unbounded target thy =
    2.17 +fun add_code number_of negative unbounded print target thy =
    2.18    let
    2.19      fun dest_numeral pls' min' bit0' bit1' thm =
    2.20        let
    2.21 @@ -74,11 +74,12 @@
    2.22            | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
    2.23        in dest_num end;
    2.24      fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
    2.25 -      (Code_Printer.str o Code_Printer.literal_numeral literals unbounded
    2.26 +      (print o Code_Printer.literal_numeral literals unbounded
    2.27          o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
    2.28    in
    2.29      thy |> Code_Target.add_syntax_const target number_of
    2.30 -      (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min}, @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
    2.31 +      (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
    2.32 +        @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
    2.33    end;
    2.34  
    2.35  end; (*local*)