# HG changeset patch
# User haftmann
# Date 1552231005 0
# Node ID 55534affe44556bdc33ed93e19b5aa2e3a8bbb5d
# Parent  06f204a2f3c254f8bd35c512772958699f562a7f
migrated from Nums to Zarith as library for OCaml integer arithmetic

diff -r 06f204a2f3c2 -r 55534affe445 NEWS
--- 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.
diff -r 06f204a2f3c2 -r 55534affe445 lib/scripts/ocaml
--- 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
diff -r 06f204a2f3c2 -r 55534affe445 lib/scripts/ocamlexec
--- /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
diff -r 06f204a2f3c2 -r 55534affe445 src/HOL/Code_Numeral.thy
--- 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"
diff -r 06f204a2f3c2 -r 55534affe445 src/HOL/GCD.thy
--- 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>
diff -r 06f204a2f3c2 -r 55534affe445 src/HOL/Imperative_HOL/Array.thy
--- 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
diff -r 06f204a2f3c2 -r 55534affe445 src/HOL/Library/Code_Real_Approx_By_Float.thy
--- 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
diff -r 06f204a2f3c2 -r 55534affe445 src/HOL/Library/code_test.ML
--- 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 *)
diff -r 06f204a2f3c2 -r 55534affe445 src/HOL/String.thy
--- 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>
diff -r 06f204a2f3c2 -r 55534affe445 src/Tools/Code/code_ml.ML
--- 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*)
diff -r 06f204a2f3c2 -r 55534affe445 src/Tools/Code/code_target.ML
--- 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;