From e9aeb7e0278c7d428ea34f29dac113fd204a81fb Mon Sep 17 00:00:00 2001
From: jim-portegies <36723906+jim-portegies@users.noreply.github.com>
Date: Sun, 31 Dec 2023 08:52:00 +0100
Subject: [PATCH] feat: create option to print rewrite hints (#44)

---
 src/g_waterproof.mlg | 14 ++++++++++++++
 src/waterprove.ml    | 13 +++++++++----
 src/waterprove.mli   |  5 +++++
 3 files changed, 28 insertions(+), 4 deletions(-)

diff --git a/src/g_waterproof.mlg b/src/g_waterproof.mlg
index 9bf4ee32..effd7060 100644
--- a/src/g_waterproof.mlg
+++ b/src/g_waterproof.mlg
@@ -64,6 +64,20 @@ VERNAC COMMAND EXTEND AutomationDebugDisableSideEff CLASSIFIED AS SIDEFF
     }
 END
 
+VERNAC COMMAND EXTEND AutomationPrintRewriteHintsEnableSideEff CLASSIFIED AS SIDEFF
+  | [ "Waterproof" "Enable" "Printing" "Rewrite" "Hints"] ->
+    {
+      print_rewrite_hints := true
+    }
+END
+
+VERNAC COMMAND EXTEND AutomationPrintRewriteHintsDisableSideEff CLASSIFIED AS SIDEFF
+  | [ "Waterproof" "Disable" "Printing" "Rewrite" "Hints" ] ->
+    {
+      print_rewrite_hints := false
+    }
+END
+
 VERNAC COMMAND EXTEND PrintVersionSideEff CLASSIFIED AS SIDEFF
   | [ "Waterproof" "Print" "Version" ] ->
     {
diff --git a/src/waterprove.ml b/src/waterprove.ml
index 74f75ee7..a63a3116 100644
--- a/src/waterprove.ml
+++ b/src/waterprove.ml
@@ -36,6 +36,11 @@ let automation_shield: bool ref = Summary.ref ~name:"automation_shield" true
 *)
 let automation_debug : bool ref = Summary.ref ~name:"automation_debug" false
 
+(**
+  Should rewrite hints be printed ?
+*)
+let print_rewrite_hints : bool ref = Summary.ref ~name:"print_rewrite_hints" false
+
 (**
   Function that will actually call automation functions
 *)
@@ -43,8 +48,8 @@ let automation_routine (depth: int) (lems: Tactypes.delayed_open_constr list) (d
   Tacticals.tclFIRST [
     Tacticals.tclCOMPLETE @@ tclIGNORE @@ wp_auto !automation_debug depth lems databases;
     Tacticals.tclCOMPLETE @@ tclIGNORE @@ wp_eauto !automation_debug depth lems databases;
-    Tacticals.tclCOMPLETE @@ tclIGNORE @@ wp_autorewrite !automation_debug @@ wp_auto !automation_debug depth lems databases;
-    Tacticals.tclCOMPLETE @@ tclIGNORE @@ wp_autorewrite !automation_debug @@ wp_eauto !automation_debug depth lems databases
+    Tacticals.tclCOMPLETE @@ tclIGNORE @@ wp_autorewrite ~print_hints:(!print_rewrite_hints) !automation_debug @@ wp_auto !automation_debug depth lems databases;
+    Tacticals.tclCOMPLETE @@ tclIGNORE @@ wp_autorewrite ~print_hints:(!print_rewrite_hints) !automation_debug @@ wp_eauto !automation_debug depth lems databases
   ]
 
 (**
@@ -54,8 +59,8 @@ let restricted_automation_routine (depth: int) (lems: Tactypes.delayed_open_cons
   Tacticals.tclFIRST [
     Tacticals.tclCOMPLETE @@ tclIGNORE @@ rwp_auto !automation_debug depth lems databases must_use forbidden;
     Tacticals.tclCOMPLETE @@ tclIGNORE @@ rwp_eauto !automation_debug depth lems databases must_use forbidden;
-    Tacticals.tclCOMPLETE @@ tclIGNORE @@ wp_autorewrite !automation_debug @@ wp_auto !automation_debug depth lems databases;
-    Tacticals.tclCOMPLETE @@ tclIGNORE @@ wp_autorewrite !automation_debug @@ wp_eauto !automation_debug depth lems databases
+    Tacticals.tclCOMPLETE @@ tclIGNORE @@ wp_autorewrite ~print_hints:(!print_rewrite_hints) !automation_debug @@ wp_auto !automation_debug depth lems databases;
+    Tacticals.tclCOMPLETE @@ tclIGNORE @@ wp_autorewrite ~print_hints:(!print_rewrite_hints) !automation_debug @@ wp_eauto !automation_debug depth lems databases
   ]
 
 (**
diff --git a/src/waterprove.mli b/src/waterprove.mli
index 01dd493f..02df44f4 100644
--- a/src/waterprove.mli
+++ b/src/waterprove.mli
@@ -26,6 +26,11 @@ val automation_shield : bool ref
 *)
 val automation_debug : bool ref
 
+(**
+  Should rewrite hints be printed ?
+*)
+val print_rewrite_hints: bool ref
+
 (**
   Waterprove