wip

Author: gebner

src/checker/Pulse.Checker.Prover.fst

@@ -668,18 +668,27 @@ let try_prove (g: env) (ctxt goals: slprop) allow_amb : T.Tac (prover_result g [
     cont_elab_equiv before h1 (VE_Refl _ _),
     cont_elab_equiv after (VE_Refl _ _) h2 |)
 
+let pp_slprops ts = ts
+  |> List.Tot.map elab_slprop
+  |> sort_terms
+  |> T.map pp
+  |> separate hardline
+
 let prove rng (g: env) (ctxt goals: slprop) allow_amb :
     T.Tac (g':env { env_extends g' g } &
       ctxt': slprop &
       continuation_elaborator g ctxt g' (goals `tm_star` ctxt')) =
   let (| g', ctxt', goals', solved', k |) = try_prove g ctxt goals allow_amb in
   if Cons? goals' then
-    T.fail_doc_at [
-      text "Cannot prove any of:";
-      separate hardline (T.map (fun t -> pp (elab_slprop t)) goals');
-      text "In context:";
-      separate hardline (T.map (fun t -> pp (elab_slprop t)) ctxt');
-    ] (Some rng)
+    T.fail_doc_at ([
+        text (if List.length goals' > 1 then "Cannot prove any of:" else "Cannot prove:") ^^
+          indent (pp_slprops goals');
+        text "In the context:" ^^ indent (pp_slprops ctxt');
+      ] @ (if Pulse.Config.debug_flag "initial_solver_state" then [
+        text "The prover was started with goal:" ^^ indent (pp goals);
+        text "and initial context:" ^^ indent (pp ctxt);
+      ] else []))
+    (Some rng)
   else
     let before, after = k g' in
     let h: slprop_equiv g' (elab_slprops (solved' @ ctxt')) (elab_slprops (ctxt' @ solved' @ goals')) = RU.magic () in