# HG changeset patch
# User wenzelm
# Date 1598131345 -7200
# Node ID 6dba090358d26b9138b270b262d42e9d685dfe0f
# Parent  16f2288b30cf834a31a4f28a0f5308ad5847f070
invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process);

diff -r 16f2288b30cf -r 6dba090358d2 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Sat Aug 22 23:11:48 2020 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sat Aug 22 23:22:25 2020 +0200
@@ -701,7 +701,7 @@
   | precedence_i (Num _) = no_prec
   | precedence_i (IntReg _) = no_prec
 
-fun write_problem_file out problems =
+fun write_problem out problems =
   let
     fun out_outmost_f (And (f1, f2)) =
         (out_outmost_f f1; out "\n   && "; out_outmost_f f2)
@@ -964,12 +964,6 @@
   handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems",
                                         "expected number after \"PROBLEM\"")
 
-fun read_output_file path =
-  (false,
-   read_next_problems (Substring.full (File.read path), [], [])
-   |>> rev ||> rev)
-  handle IO.Io _ => (true, ([], [])) | OS.SysErr _ => (true, ([], []))
-
 
 (** Main Kodkod entry point **)
 
@@ -981,8 +975,7 @@
    is partly due to the JVM and partly due to the ML "bash" function. *)
 val fudge_ms = 250
 
-fun uncached_solve_any_problem overlord deadline max_threads max_solutions
-                               problems =
+fun uncached_solve_any_problem overlord deadline max_threads max_solutions problems =
   let
     val j = find_index (curry (op =) True o #formula) problems
     val indexed_problems = if j >= 0 then
@@ -994,82 +987,99 @@
                              (0 upto length problems - 1)
     val reindex = fst o nth indexed_problems
 
-    val timeout = Time.toMilliseconds (deadline - Time.now ()) - fudge_ms
+    val external_process =
+      not (Options.default_bool \<^system_option>\<open>kodkod_scala\<close>) orelse overlord
+    val timeout0 = Time.toMilliseconds (deadline - Time.now ())
+    val timeout = if external_process then timeout0 - fudge_ms else timeout0
+
+    val solve_all = max_solutions > 1
   in
     if null indexed_problems then
       Normal ([], triv_js, "")
     else if timeout <= 0 then TimedOut triv_js
     else
       let
-        val (serial_str, temp_dir) = serial_string_and_temporary_dir overlord
-        fun path_for suf =
-          Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf)
-        val in_path = path_for "kki"
-        val in_buf = Unsynchronized.ref Buffer.empty
-        fun out s = Unsynchronized.change in_buf (Buffer.add s)
-        val out_path = path_for "out"
-        val err_path = path_for "err"
-        val _ = write_problem_file out (map snd indexed_problems)
-        val _ = File.write_buffer in_path (!in_buf)
-        fun remove_temporary_files () =
-          if overlord then ()
-          else List.app (ignore o try File.rm) [in_path, out_path, err_path]
-      in
-        let
-          val outcome =
+        val kki =
+          let
+            val buf = Unsynchronized.ref Buffer.empty
+            fun out s = Unsynchronized.change buf (Buffer.add s)
+            val _ = write_problem out (map snd indexed_problems)
+          in Buffer.content (! buf) end
+        val (rc, out, err) =
+          if external_process then
             let
-              val code =
-                Isabelle_System.bash ("cd " ^ Bash.string temp_dir ^ ";\n\
-                      \\"$KODKODI/bin/kodkodi\"" ^
-                      (" -max-msecs " ^ string_of_int timeout) ^
-                      (if max_solutions > 1 then " -solve-all" else "") ^
-                      " -max-solutions " ^ string_of_int max_solutions ^
-                      (if max_threads > 0 then
-                         " -max-threads " ^ string_of_int max_threads
-                       else
-                         "") ^
-                      " < " ^ File.bash_path in_path ^
-                      " > " ^ File.bash_path out_path ^
-                      " 2> " ^ File.bash_path err_path)
-              val (io_error, (ps, nontriv_js)) =
-                read_output_file out_path
-                ||> apfst (map (apfst reindex)) ||> apsnd (map reindex)
-              val js = triv_js @ nontriv_js
-              val first_error =
-                (File.fold_lines (fn line => fn "" => line | s => s) err_path ""
-                 handle IO.Io _ => "" | OS.SysErr _ => "")
-                |> perhaps (try (unsuffix "\r"))
-                |> perhaps (try (unsuffix "."))
-                |> perhaps (try (unprefix "Solve error: "))
-                |> perhaps (try (unprefix "Error: "))
-              fun has_error s =
-                first_error |> Substring.full |> Substring.position s |> snd
-                            |> Substring.isEmpty |> not
+              val (serial_str, temp_dir) = serial_string_and_temporary_dir overlord
+              fun path_for suf = Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf)
+              val kki_path = path_for "kki"
+              val out_path = path_for "out"
+              val err_path = path_for "err"
+
+              fun remove_temporary_files () =
+                if overlord then ()
+                else List.app (ignore o try File.rm) [kki_path, out_path, err_path]
             in
-              if null ps then
-                if code = 2 then
-                  TimedOut js
-                else if code = 0 then
-                  Normal ([], js, first_error)
-                else if code = 127 then
-                  JavaNotFound
-                else if has_error "UnsupportedClassVersionError" then
-                  JavaTooOld
-                else if has_error "NoClassDefFoundError" then
-                  KodkodiNotInstalled
-                else if is_kodkodi_too_old () then
-                  KodkodiTooOld
-                else if first_error <> "" then
-                  Error (first_error, js)
-                else if io_error then
-                  Error ("I/O error", js)
-                else
-                  Error ("Unknown error", js)
-              else
-                Normal (ps, js, first_error)
+              let
+                val _ = File.write kki_path kki
+                val rc =
+                  Isabelle_System.bash ("cd " ^ Bash.string temp_dir ^ ";\n\
+                    \\"$KODKODI/bin/kodkodi\"" ^
+                    (" -max-msecs " ^ string_of_int timeout) ^
+                    (if solve_all then " -solve-all" else "") ^
+                    " -max-solutions " ^ string_of_int max_solutions ^
+                    (if max_threads > 0 then " -max-threads " ^ string_of_int max_threads else "") ^
+                    " < " ^ File.bash_path kki_path ^
+                    " > " ^ File.bash_path out_path ^
+                    " 2> " ^ File.bash_path err_path)
+                val out = File.read out_path
+                val err = File.read err_path
+                val _ = remove_temporary_files ()
+              in (rc, out, err) end
+              handle exn => (remove_temporary_files (); Exn.reraise exn)
             end
-        in remove_temporary_files (); outcome end
-        handle exn => (remove_temporary_files (); Exn.reraise exn)
+          else
+            (timeout, (solve_all, (max_solutions, (max_threads, kki))))
+            |> let open XML.Encode in pair int (pair bool (pair int (pair int string))) end
+            |> YXML.string_of_body
+            |> \<^scala>\<open>kodkod\<close>
+            |> YXML.parse_body
+            |> let open XML.Decode in triple int string string end
+
+        val (ps, nontriv_js) =
+          read_next_problems (Substring.full out, [], [])
+          |>> rev ||> rev
+          |> apfst (map (apfst reindex)) |> apsnd (map reindex)
+        val js = triv_js @ nontriv_js
+
+        val first_error =
+          trim_split_lines err
+          |> find_first (fn line => line <> "")
+          |> the_default ""
+          |> perhaps (try (unsuffix "."))
+          |> perhaps (try (unprefix "Solve error: "))
+          |> perhaps (try (unprefix "Error: "))
+        fun has_error s =
+          first_error |> Substring.full |> Substring.position s |> snd
+                      |> Substring.isEmpty |> not
+      in
+        if null ps then
+          if rc = 2 then
+            TimedOut js
+          else if rc = 0 then
+            Normal ([], js, first_error)
+          else if rc = 127 then
+            JavaNotFound
+          else if has_error "UnsupportedClassVersionError" then
+            JavaTooOld
+          else if has_error "NoClassDefFoundError" then
+            KodkodiNotInstalled
+          else if is_kodkodi_too_old () then
+            KodkodiTooOld
+          else if first_error <> "" then
+            Error (first_error, js)
+          else
+            Error ("Unknown error", js)
+        else
+          Normal (ps, js, first_error)
       end
   end
 
diff -r 16f2288b30cf -r 6dba090358d2 src/HOL/Tools/Nitpick/kodkod.scala
--- a/src/HOL/Tools/Nitpick/kodkod.scala	Sat Aug 22 23:11:48 2020 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Sat Aug 22 23:22:25 2020 +0200
@@ -21,6 +21,12 @@
     def ok: Boolean = rc == 0
     def check: String =
       if (ok) out else error(if (err.isEmpty) "Error" else err)
+
+    def encode: XML.Body =
+    {
+      import XML.Encode._
+      triple(int, string, string)((rc, out, err))
+    }
   }
 
   def execute(source: String,
@@ -101,4 +107,28 @@
     execute(
       """solver: "MiniSat\n"""" +
       File.read(Path.explode("$KODKODI/examples/weber3.kki"))).check
+
+
+  /* scala function */
+
+  object Fun extends Scala.Fun("kodkod")
+  {
+    def apply(args: String): String =
+    {
+      val (timeout, (solve_all, (max_solutions, (max_threads, kki)))) =
+      {
+        import XML.Decode._
+        pair(int, pair(bool, pair(int, pair(int, string))))(YXML.parse_body(args))
+      }
+      val result =
+        execute(kki,
+          solve_all = solve_all,
+          max_solutions = max_solutions,
+          timeout = Time.ms(timeout),
+          max_threads = max_threads)
+      YXML.string_of_body(result.encode)
+    }
+  }
 }
+
+class Scala_Functions extends Scala.Functions(Kodkod.Fun)
diff -r 16f2288b30cf -r 6dba090358d2 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Sat Aug 22 23:11:48 2020 +0200
+++ b/src/HOL/Tools/etc/options	Sat Aug 22 23:22:25 2020 +0200
@@ -37,3 +37,6 @@
 
 public option MaSh : string = "sml"
   -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"
+
+public option kodkod_scala : bool = false
+  -- "invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process)"
diff -r 16f2288b30cf -r 6dba090358d2 src/HOL/Tools/etc/settings
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/etc/settings	Sat Aug 22 23:22:25 2020 +0200
@@ -0,0 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
+isabelle_scala_service 'isabelle.nitpick.Scala_Functions'