--- a/NEWS Sun Mar 10 15:16:45 2019 +0000
+++ b/NEWS Sun Mar 10 15:16:45 2019 +0000
@@ -123,6 +123,15 @@
* Code generation for OCaml: proper strings are used for literals.
Minor INCOMPATIBILITY.
+* Code generation for OCaml: Zarith superseedes Nums as library for
+integer arithmetic. Use the following incantation to obtain a suitable
+component setup:
+
+ isabelle ocaml_setup
+ isabelle ocaml_opam install zarith
+
+Minor INCOMPATIBILITY
+
* Code generation for Haskell: code includes for Haskell must contain
proper module frame, nothing is added magically any longer.
INCOMPATIBILITY.
--- a/lib/scripts/ocaml Sun Mar 10 15:16:45 2019 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Invoke ocaml via "opam".
-
-if [ -d "$ISABELLE_OPAM_ROOT" ]
-then
- isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocaml "$@"
-else
- echo "Cannot execute ocaml: missing Isabelle OCaml setup" >&2
- exit 127
-fi
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/ocamlexec Sun Mar 10 15:16:45 2019 +0000
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius; Florian Haftmann
+#
+# Invoke command in OCaml environment setup by "opam".
+
+if [ -d "$ISABELLE_OPAM_ROOT" ]
+then
+ isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- "$@"
+else
+ echo "Cannot execute: missing Isabelle OCaml setup" >&2
+ exit 127
+fi
--- a/src/HOL/Code_Numeral.thy Sun Mar 10 15:16:45 2019 +0000
+++ b/src/HOL/Code_Numeral.thy Sun Mar 10 15:16:45 2019 +0000
@@ -652,7 +652,7 @@
code_printing
type_constructor integer \<rightharpoonup>
(SML) "IntInf.int"
- and (OCaml) "Big'_int.big'_int"
+ and (OCaml) "Z.t"
and (Haskell) "Integer"
and (Scala) "BigInt"
and (Eval) "int"
@@ -662,7 +662,7 @@
code_printing
constant "0::integer" \<rightharpoonup>
(SML) "!(0/ :/ IntInf.int)"
- and (OCaml) "Big'_int.zero'_big'_int"
+ and (OCaml) "Z.zero"
and (Haskell) "!(0/ ::/ Integer)"
and (Scala) "BigInt(0)"
@@ -676,25 +676,25 @@
code_printing
constant "plus :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
(SML) "IntInf.+ ((_), (_))"
- and (OCaml) "Big'_int.add'_big'_int"
+ and (OCaml) "Z.add"
and (Haskell) infixl 6 "+"
and (Scala) infixl 7 "+"
and (Eval) infixl 8 "+"
| constant "uminus :: integer \<Rightarrow> _" \<rightharpoonup>
(SML) "IntInf.~"
- and (OCaml) "Big'_int.minus'_big'_int"
+ and (OCaml) "Z.neg"
and (Haskell) "negate"
and (Scala) "!(- _)"
and (Eval) "~/ _"
| constant "minus :: integer \<Rightarrow> _" \<rightharpoonup>
(SML) "IntInf.- ((_), (_))"
- and (OCaml) "Big'_int.sub'_big'_int"
+ and (OCaml) "Z.sub"
and (Haskell) infixl 6 "-"
and (Scala) infixl 7 "-"
and (Eval) infixl 8 "-"
| constant Code_Numeral.dup \<rightharpoonup>
(SML) "IntInf.*/ (2,/ (_))"
- and (OCaml) "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)"
+ and (OCaml) "Z.shift'_left/ _/ 1"
and (Haskell) "!(2 * _)"
and (Scala) "!(2 * _)"
and (Eval) "!(2 * _)"
@@ -705,37 +705,37 @@
and (Scala) "!sys.error(\"sub\")"
| constant "times :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
(SML) "IntInf.* ((_), (_))"
- and (OCaml) "Big'_int.mult'_big'_int"
+ and (OCaml) "Z.mul"
and (Haskell) infixl 7 "*"
and (Scala) infixl 8 "*"
and (Eval) infixl 9 "*"
| constant Code_Numeral.divmod_abs \<rightharpoonup>
(SML) "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)"
- and (OCaml) "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)"
+ and (OCaml) "!(fun k l ->/ if Z.equal Z.zero l then/ (Z.zero, l) else/ Z.div'_rem/ (Z.abs k)/ (Z.abs l))"
and (Haskell) "divMod/ (abs _)/ (abs _)"
and (Scala) "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))"
and (Eval) "Integer.div'_mod/ (abs _)/ (abs _)"
| constant "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
(SML) "!((_ : IntInf.int) = _)"
- and (OCaml) "Big'_int.eq'_big'_int"
+ and (OCaml) "Z.equal"
and (Haskell) infix 4 "=="
and (Scala) infixl 5 "=="
and (Eval) infixl 6 "="
| constant "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
(SML) "IntInf.<= ((_), (_))"
- and (OCaml) "Big'_int.le'_big'_int"
+ and (OCaml) "Z.leq"
and (Haskell) infix 4 "<="
and (Scala) infixl 4 "<="
and (Eval) infixl 6 "<="
| constant "less :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
(SML) "IntInf.< ((_), (_))"
- and (OCaml) "Big'_int.lt'_big'_int"
+ and (OCaml) "Z.lt"
and (Haskell) infix 4 "<"
and (Scala) infixl 4 "<"
and (Eval) infixl 6 "<"
| constant "abs :: integer \<Rightarrow> _" \<rightharpoonup>
(SML) "IntInf.abs"
- and (OCaml) "Big'_int.abs'_big'_int"
+ and (OCaml) "Z.abs"
and (Haskell) "Prelude.abs"
and (Scala) "_.abs"
and (Eval) "abs"
--- a/src/HOL/GCD.thy Sun Mar 10 15:16:45 2019 +0000
+++ b/src/HOL/GCD.thy Sun Mar 10 15:16:45 2019 +0000
@@ -2735,7 +2735,7 @@
code_printing
constant "gcd :: integer \<Rightarrow> _" \<rightharpoonup>
- (OCaml) "Big'_int.gcd'_big'_int"
+ (OCaml) "!(fun k l -> if Z.equal k Z.zero then/ Z.abs l else if Z.equal/ l Z.zero then Z.abs k else Z.gcd k l)"
and (Haskell) "Prelude.gcd"
and (Scala) "_.gcd'((_)')"
\<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
--- a/src/HOL/Imperative_HOL/Array.thy Sun Mar 10 15:16:45 2019 +0000
+++ b/src/HOL/Imperative_HOL/Array.thy Sun Mar 10 15:16:45 2019 +0000
@@ -458,13 +458,13 @@
code_printing type_constructor array \<rightharpoonup> (OCaml) "_/ array"
code_printing constant Array \<rightharpoonup> (OCaml) "failwith/ \"bare Array\""
-code_printing constant Array.new' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)"
+code_printing constant Array.new' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.make/ (Z.to'_int/ _)/ _)"
code_printing constant Array.of_list \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.of'_list/ _)"
code_printing constant Array.make' \<rightharpoonup> (OCaml)
- "(fun/ ()/ ->/ Array.init/ (Big'_int.int'_of'_big'_int/ _)/ (fun k'_ ->/ _/ (Big'_int.big'_int'_of'_int/ k'_)))"
-code_printing constant Array.len' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))"
-code_printing constant Array.nth' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))"
-code_printing constant Array.upd' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)"
+ "(fun/ ()/ ->/ Array.init/ (Z.to'_int/ _)/ (fun k'_ ->/ _/ (Z.of'_int/ k'_)))"
+code_printing constant Array.len' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Z.of'_int/ (Array.length/ _))"
+code_printing constant Array.nth' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.get/ _/ (Z.to'_int/ _))"
+code_printing constant Array.upd' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.set/ _/ (Z.to'_int/ _)/ _)"
code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (OCaml) infixl 4 "="
code_reserved OCaml Array
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Sun Mar 10 15:16:45 2019 +0000
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Sun Mar 10 15:16:45 2019 +0000
@@ -155,7 +155,7 @@
code_printing
constant real_of_integer \<rightharpoonup>
(SML) "Real.fromInt"
- and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
+ and (OCaml) "Pervasives.float/ (Big'_int.to'_int (_))"
context
begin
--- a/src/HOL/Library/code_test.ML Sun Mar 10 15:16:45 2019 +0000
+++ b/src/HOL/Library/code_test.ML Sun Mar 10 15:16:45 2019 +0000
@@ -442,7 +442,7 @@
(* driver for OCaml *)
val ocamlN = "OCaml"
-val ISABELLE_OCAMLC = "ISABELLE_OCAMLC"
+val ISABELLE_OPAM_ROOT = "ISABELLE_OPAM_ROOT"
fun mk_driver_ocaml _ path _ value_name =
let
@@ -467,9 +467,9 @@
val compiled_path = Path.append path (Path.basic "test")
val compile_cmd =
- "\"$ISABELLE_OCAMLC\" -w pu -o " ^ File.bash_path compiled_path ^
- " -I " ^ File.bash_path path ^
- " nums.cma " ^ File.bash_path code_path ^ " " ^ File.bash_path driver_path
+ "\"$ISABELLE_ROOT/lib/scripts/ocamlexec\" ocamlfind ocamlopt -w pu -package zarith -linkpkg " ^
+ " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path path ^ " " ^
+ File.bash_path code_path ^ " " ^ File.bash_path driver_path
val run_cmd = File.bash_path compiled_path
in
@@ -478,7 +478,7 @@
end
fun evaluate_in_ocaml ctxt =
- evaluate mk_driver_ocaml (SOME (ISABELLE_OCAMLC, "ocamlc executable")) ocamlN ctxt
+ evaluate mk_driver_ocaml (SOME (ISABELLE_OPAM_ROOT, "ocaml opam environment")) ocamlN ctxt
(* driver for GHC *)
--- a/src/HOL/String.thy Sun Mar 10 15:16:45 2019 +0000
+++ b/src/HOL/String.thy Sun Mar 10 15:16:45 2019 +0000
@@ -673,7 +673,7 @@
(SML) "!(String.implode/ o List.map (fn k => if 0 <= k andalso k < 128 then (Char.chr o IntInf.toInt) k else raise Fail \"Non-ASCII character in literal\"))"
and (OCaml) "!(let xs = _
and chr k =
- let l = Big'_int.int'_of'_big'_int k
+ let l = Z.to'_int k
in if 0 <= l && l < 128
then Char.chr l
else failwith \"Non-ASCII character in literal\"
@@ -683,7 +683,7 @@
| constant String.asciis_of_literal \<rightharpoonup>
(SML) "!(List.map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail \"Non-ASCII character in literal\" end) /o String.explode)"
and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (let k = Char.code (String.get s i) in
- if k < 128 then Big'_int.big'_int'_of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (String.length s - 1) [])"
+ if k < 128 then Z.of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (String.length s - 1) [])"
and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))"
and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; if (k < 128) BigInt(k) else sys.error(\"Non-ASCII character in literal\") }))"
| class_instance String.literal :: equal \<rightharpoonup>
--- a/src/Tools/Code/code_ml.ML Sun Mar 10 15:16:45 2019 +0000
+++ b/src/Tools/Code/code_ml.ML Sun Mar 10 15:16:45 2019 +0000
@@ -717,10 +717,10 @@
val literals_ocaml = let
fun numeral_ocaml k = if k < 0
- then "(Big_int.minus_big_int " ^ numeral_ocaml (~ k) ^ ")"
+ then "(Z.neg " ^ numeral_ocaml (~ k) ^ ")"
else if k <= 1073741823
- then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
- else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
+ then "(Z.of_int " ^ string_of_int k ^ ")"
+ else "(Z.of_string " ^ quote (string_of_int k) ^ ")"
in Literals {
literal_string = print_ocaml_string,
literal_numeral = numeral_ocaml,
@@ -885,9 +885,11 @@
evaluation_args = []})
#> Code_Target.add_language
(target_OCaml, {serializer = serializer_ocaml, literals = literals_ocaml,
- check = {env_var = "ISABELLE_OCAML",
- make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
- make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu -safe-string nums.cma ROOT.ocaml"},
+ check = {env_var = "ISABELLE_OPAM_ROOT",
+ make_destination = fn p => Path.append p (Path.explode "ROOT.ml")
+ (*extension demanded by OCaml compiler*),
+ make_command = fn _ =>
+ "\"$ISABELLE_ROOT/lib/scripts/ocamlexec\" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml"},
evaluation_args = []})
#> Code_Target.set_printings (Type_Constructor ("fun",
[(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
@@ -904,6 +906,6 @@
"sig", "struct", "then", "to", "true", "try", "type", "val",
"virtual", "when", "while", "with"
]
- #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"]);
+ #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Z"]);
end; (*struct*)
--- a/src/Tools/Code/code_target.ML Sun Mar 10 15:16:45 2019 +0000
+++ b/src/Tools/Code/code_target.ML Sun Mar 10 15:16:45 2019 +0000
@@ -422,8 +422,9 @@
val _ = export_result ctxt (SOME (SOME destination)) 80
(invoke_serializer ctxt target_name generatedN args program all_public syms)
val cmd = make_command generatedN;
+ val context_cmd = "cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1";
in
- if Isabelle_System.bash ("cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
+ if Isabelle_System.bash context_cmd <> 0
then error ("Code check failed for " ^ target_name ^ ": " ^ cmd)
else ()
end;