From c8e4fa14b5cd0435fc38f60eedd0a5c3be0e4f43 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 14 Nov 2023 09:55:45 +0100
Subject: [PATCH] Update the JS worker

We have to update the JS worker to dump models as we don't print models
in the library anymore.
---
 src/bin/common/solving_loop.ml       |  8 ++------
 src/bin/js/worker_js.ml              | 26 ++++++++++++++++++++++++++
 src/lib/reasoners/sat_solver_sig.ml  |  4 ++++
 src/lib/reasoners/sat_solver_sig.mli |  1 +
 4 files changed, 33 insertions(+), 6 deletions(-)

diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
index ee2b15006..b3e6aed97 100644
--- a/src/bin/common/solving_loop.ml
+++ b/src/bin/common/solving_loop.ml
@@ -154,15 +154,11 @@ let main () =
     (module SatCont.Make(TH) : Sat_solver_sig.S)
   in
 
-  let pp_unknown_reason_opt ppf = function
-    | None -> Fmt.pf ppf "Decided"
-    | Some ur -> Sat_solver_sig.pp_unknown_reason ppf ur
-  in
-
   let print_model ppf (Model ((module SAT), env)) =
     let ur = SAT.get_unknown_reason env in
     Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
-      "@[<v 0>; Returned unknown reason = %a@]" pp_unknown_reason_opt ur;
+      "@[<v 0>; Returned unknown reason = %a@]"
+      Sat_solver_sig.pp_unknown_reason_opt ur;
     match SAT.get_model env with
     | None ->
       Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml
index 5b5bfc8ff..284e20fe4 100644
--- a/src/bin/js/worker_js.ml
+++ b/src/bin/js/worker_js.ml
@@ -120,6 +120,22 @@ let main worker_id content =
       Frontend.print_status status n
     in
 
+    let print_model ppf env =
+      let ur = SAT.get_unknown_reason env in
+      Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
+        "@[<v 0>; Returned unknown reason = %a@]"
+        Sat_solver_sig.pp_unknown_reason_opt ur;
+      match SAT.get_model env with
+      | None ->
+        Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
+          "@[<v 0>It seems that no model has been computed so \
+           far. You may need to change your model generation strategy \
+           or to increase your timeouts."
+
+      | Some (lazy model) ->
+        Models.output_concrete_model ppf model
+    in
+
     let solve all_context (cnf, goal_name) =
       let used_context = Frontend.choose_used_context all_context ~goal_name in
       SAT.reset_refs ();
@@ -133,6 +149,16 @@ let main worker_id content =
       if Options.get_unsat_core () then begin
         unsat_core := Explanation.get_unsat_core ftnd_env.FE.expl;
       end;
+      let () =
+        match ftnd_env.FE.res with
+        | `Sat partial_model | `Unknown partial_model ->
+          begin
+            if Options.(get_interpretation () && get_dump_models ()) then
+              print_model (Options.Output.get_fmt_models ()) partial_model;
+          end
+        | `Unsat -> ()
+      in
+      ()
     in
 
     let typed_loop all_context state td =
diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml
index 2af518fb3..9caf2c457 100644
--- a/src/lib/reasoners/sat_solver_sig.ml
+++ b/src/lib/reasoners/sat_solver_sig.ml
@@ -47,6 +47,10 @@ let pp_unknown_reason ppf = function
   | Memout -> Fmt.pf ppf "Memout"
   | Timeout t -> Fmt.pf ppf "Timeout:%a" pp_timeout_reason t
 
+let pp_unknown_reason_opt ppf = function
+  | None -> Fmt.pf ppf "Decided"
+  | Some ur -> pp_unknown_reason ppf ur
+
 module type S = sig
   type t
 
diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli
index d3e4a0404..4b1b7e703 100644
--- a/src/lib/reasoners/sat_solver_sig.mli
+++ b/src/lib/reasoners/sat_solver_sig.mli
@@ -39,6 +39,7 @@ type unknown_reason =
   | Timeout of timeout_reason
 
 val pp_unknown_reason: unknown_reason Fmt.t
+val pp_unknown_reason_opt : unknown_reason option Fmt.t
 
 module type S = sig
   type t