Printing <PASSED::> and <FAILED::> + CWGroup and CWEndGroup

Author: monadius

.gitignore

@@ -1,3 +1,4 @@
+\#*
 .DS_Store
 *~
 .vscode/

README.md

@@ -13,15 +13,21 @@ Now run `make`.
 
 Run `make .merlin` to create the `.merlin` file.
 
-## Examples
+## New Vernacular Commands
 
-A new vernacular command `CWTest qualid Assumes qualid*` is defined.
+A new vernacular command `CWTest msg? qualid Assumes qualid*` is defined.
 This command fails if the tested `qualid` depends on an axiom which is not listed
 after `Assumes`:
 
 ```coq
-CWTest lemma Assumes proof_irrelevance functional_extensionality.
+CWTest "Testing lemma" lemma Assumes proof_irrelevance functional_extensionality.
 ```
 
+The string argument after `CWTest` (`msg`) is optional.
+
+Two other commands are `CWGroup msg` and `CWEndGroup`.
+
+## Examples
+
 See [theories/Demo.v](theories/Demo.v) and [theories/Demo2.v](theories/Demo2.v)
 for more examples.

src/coq_cw.ml

@@ -12,7 +12,7 @@ let extract_axioms s =
   Printer.ContextObjectMap.fold fold s []
 
 (* TODO: compare axiom names (constants) also *)
-let test_assumptions env sigma s ax_tys =
+let test_assumptions msg env sigma s ax_tys =
   let unify ty1 ty2 = 
     match Reductionops.infer_conv env sigma ty1 ty2 with
     | Some _ -> true
@@ -23,7 +23,10 @@ let test_assumptions env sigma s ax_tys =
     | Printer.Axiom _ ->
       let ety = EConstr.of_constr ty in
       if List.exists (unify ety) ax_tys then ()
-      else CErrors.user_err (str "Axiom: " ++ Printer.pr_econstr_env env sigma ety)
+      else begin
+        Feedback.msg_notice (str ("\n<FAILED::> " ^ msg ^ "\n"));
+        CErrors.user_err (str "Axiom: " ++ Printer.pr_econstr_env env sigma ety)
+      end
     | _ -> ()
   in
   Printer.ContextObjectMap.iter iter s
@@ -35,7 +38,7 @@ let locate r =
     (gr, Globnames.printable_constr_of_global gr)
   with Not_found -> CErrors.user_err (str "Not found: " ++ Libnames.pr_qualid r)
 
-let test c_ref ax_refs = 
+let test ?(msg = "Axioms") c_ref ax_refs = 
   let env = Global.env() in
   let sigma = Evd.from_env env in
   let (gr, cstr) = locate c_ref in
@@ -47,5 +50,5 @@ let test c_ref ax_refs =
       (fun (sigma, tys) (_, c) ->
         let sigma, ty = Typing.type_of env sigma (EConstr.of_constr c) in
         sigma, ty :: tys) (sigma, []) ax_grs_cstrs in
-  test_assumptions env sigma assumptions ax_tys;
-  Feedback.msg_notice (str "SUCCESS")
+  test_assumptions msg env sigma assumptions ax_tys;
+  Feedback.msg_notice (str ("\n<PASSED::> " ^ msg ^ "\n"))

src/coq_cw.mli

@@ -1 +1 @@
-val test : Libnames.qualid -> Libnames.qualid list -> unit
+val test : ?msg:string -> Libnames.qualid -> Libnames.qualid list -> unit

src/g_coq_cw.ml4

@@ -1,9 +1,22 @@
 DECLARE PLUGIN "coq_cw_plugin"
 
+open Pp
 open Stdarg
 
 VERNAC COMMAND EXTEND CWTest CLASSIFIED AS QUERY
-| [ "CWTest" ref(e) "Assumes" ref_list(axioms)] -> [
-    Coq_cw.test e axioms
+| [ "CWTest" string_opt(msg) ref(e) "Assumes" ref_list(axioms)] -> [ 
+        Coq_cw.test ?msg e axioms
     ]
-END
+END
+
+VERNAC COMMAND EXTEND CWGroup CLASSIFIED AS QUERY
+| [ "CWGroup" string(msg)] -> [ 
+        Feedback.msg_notice (str ("\n<DESCRIBE::> " ^ msg ^ "\n"))
+    ]
+END
+
+VERNAC COMMAND EXTEND CWEndGroup CLASSIFIED AS QUERY
+| [ "CWEndGroup"] -> [ 
+        Feedback.msg_notice (str "\n<COMPLETEDIN::>\n")
+    ]
+END

theories/Demo.v

@@ -16,13 +16,17 @@ Lemma lemma3 : (2 = 3) \/ ~(2 = 3).
 Proof.
 apply classic.
 Qed.
-  
+
+CWGroup "Assumption Tests".
+
 Fail CWTest lemma1 Assumes.
 CWTest lemma1 Assumes my_ax.
 Fail CWTest lemma1 Assumes classic.
-CWTest lemma1 Assumes lemma2.
+CWTest "lemma1" lemma1 Assumes lemma2.
 CWTest lemma1 Assumes classic my_ax.
-CWTest lemma2 Assumes my_ax.
+CWTest "lemma2" lemma2 Assumes my_ax.
 
 CWTest lemma3 Assumes classic my_ax.
-Fail CWTest lemma3 Assumes my_ax.
+Fail CWTest lemma3 Assumes my_ax.
+
+CWEndGroup.