OCaml builtin intergers are elusive; avoid
authorhaftmann
Tue Jun 02 15:53:05 2009 +0200 (2009-06-02)
changeset 31377a48f9ef9de15
parent 31376 4356b52b03f7
child 31378 d1cbf6393964
OCaml builtin intergers are elusive; avoid
src/HOL/Code_Numeral.thy
src/HOL/Library/Code_Integer.thy
src/HOL/Library/Efficient_Nat.thy
src/Tools/code/code_ml.ML
     1.1 --- a/src/HOL/Code_Numeral.thy	Tue Jun 02 15:53:04 2009 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Tue Jun 02 15:53:05 2009 +0200
     1.3 @@ -279,7 +279,7 @@
     1.4  
     1.5  code_type code_numeral
     1.6    (SML "int")
     1.7 -  (OCaml "int")
     1.8 +  (OCaml "Big'_int.big'_int")
     1.9    (Haskell "Int")
    1.10  
    1.11  code_instance code_numeral :: eq
    1.12 @@ -287,45 +287,46 @@
    1.13  
    1.14  setup {*
    1.15    fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.16 -    false false) ["SML", "OCaml", "Haskell"]
    1.17 +    false false) ["SML", "Haskell"]
    1.18 +  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} false true "OCaml"
    1.19  *}
    1.20  
    1.21  code_reserved SML Int int
    1.22 -code_reserved OCaml Pervasives int
    1.23 +code_reserved OCaml Big_int
    1.24  
    1.25  code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.26    (SML "Int.+/ ((_),/ (_))")
    1.27 -  (OCaml "Pervasives.( + )")
    1.28 +  (OCaml "Big'_int.add'_big'_int")
    1.29    (Haskell infixl 6 "+")
    1.30  
    1.31  code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.32    (SML "Int.max/ (_/ -/ _,/ 0 : int)")
    1.33 -  (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
    1.34 +  (OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
    1.35    (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
    1.36  
    1.37  code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.38    (SML "Int.*/ ((_),/ (_))")
    1.39 -  (OCaml "Pervasives.( * )")
    1.40 +  (OCaml "Big'_int.mult'_big'_int")
    1.41    (Haskell infixl 7 "*")
    1.42  
    1.43  code_const div_mod_code_numeral
    1.44    (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
    1.45 -  (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
    1.46 +  (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))")
    1.47    (Haskell "divMod")
    1.48  
    1.49  code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.50    (SML "!((_ : Int.int) = _)")
    1.51 -  (OCaml "!((_ : int) = _)")
    1.52 +  (OCaml "Big'_int.eq'_big'_int")
    1.53    (Haskell infixl 4 "==")
    1.54  
    1.55  code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.56    (SML "Int.<=/ ((_),/ (_))")
    1.57 -  (OCaml "!((_ : int) <= _)")
    1.58 +  (OCaml "Big'_int.le'_big'_int")
    1.59    (Haskell infix 4 "<=")
    1.60  
    1.61  code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.62    (SML "Int.</ ((_),/ (_))")
    1.63 -  (OCaml "!((_ : int) < _)")
    1.64 +  (OCaml "Big'_int.lt'_big'_int")
    1.65    (Haskell infix 4 "<")
    1.66  
    1.67  end
     2.1 --- a/src/HOL/Library/Code_Integer.thy	Tue Jun 02 15:53:04 2009 +0200
     2.2 +++ b/src/HOL/Library/Code_Integer.thy	Tue Jun 02 15:53:05 2009 +0200
     2.3 @@ -93,11 +93,10 @@
     2.4  
     2.5  code_const Code_Numeral.int_of
     2.6    (SML "IntInf.fromInt")
     2.7 -  (OCaml "Big'_int.big'_int'_of'_int")
     2.8 +  (OCaml "_")
     2.9    (Haskell "toEnum")
    2.10  
    2.11  code_reserved SML IntInf
    2.12 -code_reserved OCaml Big_int
    2.13  
    2.14  text {* Evaluation *}
    2.15  
     3.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Jun 02 15:53:04 2009 +0200
     3.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jun 02 15:53:05 2009 +0200
     3.3 @@ -371,12 +371,12 @@
     3.4  
     3.5  code_const Code_Numeral.of_nat
     3.6    (SML "IntInf.toInt")
     3.7 -  (OCaml "Big'_int.int'_of'_big'_int")
     3.8 +  (OCaml "_")
     3.9    (Haskell "fromEnum")
    3.10  
    3.11  code_const Code_Numeral.nat_of
    3.12    (SML "IntInf.fromInt")
    3.13 -  (OCaml "Big'_int.big'_int'_of'_int")
    3.14 +  (OCaml "_")
    3.15    (Haskell "toEnum")
    3.16  
    3.17  text {* Using target language arithmetic operations whenever appropriate *}
     4.1 --- a/src/Tools/code/code_ml.ML	Tue Jun 02 15:53:04 2009 +0200
     4.2 +++ b/src/Tools/code/code_ml.ML	Tue Jun 02 15:53:05 2009 +0200
     4.3 @@ -444,7 +444,8 @@
     4.4                |>> (fn p => concat
     4.5                    [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
     4.6              val (ps, vars') = fold_map pr binds vars;
     4.7 -          in Pretty.chunks (ps @| pr_term is_closure thm vars' NOBR body) end
     4.8 +            fun mk_brack (p :: ps) = Pretty.block [str "(", p] :: ps;
     4.9 +          in Pretty.chunks (mk_brack ps @| Pretty.block [pr_term is_closure thm vars' NOBR body, str ")"]) end
    4.10        | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
    4.11            let
    4.12              fun pr delim (pat, body) =
    4.13 @@ -649,7 +650,7 @@
    4.14                str ("type '" ^ v),
    4.15                (str o deresolve) class,
    4.16                str "=",
    4.17 -              enum_default "();;" ";" "{" "};;" (
    4.18 +              enum_default "unit;;" ";" "{" "};;" (
    4.19                  map pr_superclass_field superclasses
    4.20                  @ map pr_classparam_field classparams
    4.21                )
    4.22 @@ -708,17 +709,17 @@
    4.23        val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
    4.24          then chr i else c
    4.25      in s end;
    4.26 +  fun bignum_ocaml k = if k <= 1073741823
    4.27 +    then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
    4.28 +    else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
    4.29  in Literals {
    4.30    literal_char = enclose "'" "'" o char_ocaml,
    4.31    literal_string = quote o translate_string char_ocaml,
    4.32    literal_numeral = fn unbounded => fn k => if k >= 0 then
    4.33 -      if unbounded then
    4.34 -        "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
    4.35 +      if unbounded then bignum_ocaml k
    4.36        else string_of_int k
    4.37      else
    4.38 -      if unbounded then
    4.39 -        "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
    4.40 -          o string_of_int o op ~) k ^ ")"
    4.41 +      if unbounded then "(Big_int.minus_big_int " ^ bignum_ocaml (~ k) ^ ")"
    4.42        else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
    4.43    literal_list = Pretty.enum ";" "[" "]",
    4.44    infix_cons = (6, "::")