feat: create option to print rewrite hints (impermeable#44)

andres-erbsen · Dec 31, 2023 · e9aeb7e · e9aeb7e
1 parent b08e218
commit e9aeb7e
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 4 deletions.
diff --git 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
@@ -36,15 +36,20 @@ 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
 *)
 let automation_routine (depth: int) (lems: Tactypes.delayed_open_constr list) (databases: hint_db_name list): unit tactic =
   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
@@ -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