New commands for test cases

Author: monadius

cw_example/test.v

@@ -2,5 +2,31 @@ Require solution.
 Require Import preloaded.
 From CW Require Import Loader.
 
-CWTest "Testing solution" solution.solution Assumes test_axiom.
+CWGroup "Tests for solution.solution".
+  CWTestCase "Type test".
+    Example solution_test : 1 + 1 = 3.
+    Proof. exact solution.solution. Qed.
+  CWTestCase "Assumptions test".
+    CWAssert "Testing solution" solution.solution Assumes test_axiom.
+CWEndGroup.
 
+CWGroup "Another test
+with line breaks".
+  CWAssert "Testing solution_test
+(line break)" solution_test Assumes test_axiom.
+CWEndGroup.
+
+CWTestCase "Without group".
+  CWAssert solution_test Assumes test_axiom.
+CWEnd.
+
+CWGroup "Nested groups".
+  CWGroup "Level 2".
+    CWTestCase "Test 1".
+      CWAssert solution_test Assumes test_axiom.
+  CWEndGroup.
+  CWTestCase "Test 2".
+    CWAssert solution_test Assumes test_axiom.
+    CWAssert solution_test Assumes test_axiom.
+  CWEnd.
+CWEndGroup.

src/coq_cw.ml

@@ -2,9 +2,45 @@ open Pp
 
 let solution_file = "/workspace/Solution.v"
 
-let passed msg = Feedback.msg_notice (str ("\n<PASSED::> " ^ msg ^ "\n"))
+let format_msg =
+  let re = Str.regexp_string "\n" in
+  Str.global_replace re "<:LF:>" 
 
-let failed msg = Feedback.msg_notice (str ("\n<FAILED::> " ^ msg ^ "\n"))
+let display tag msg =
+  Feedback.msg_notice (str (Printf.sprintf "\n<%s::>%s\n" tag (format_msg msg)))
+
+let passed = display "PASSED"
+
+let failed = display "FAILED"
+
+type group = {
+  tag : string;
+  start_time : float
+}
+
+let mk_group tag t = { tag = tag; start_time = t }
+
+let group_stack = Summary.ref ~name:"open_groups" ([] : group list)
+
+let rec end_group tag =
+  let e = Unix.gettimeofday() in
+  match !group_stack with 
+  | [] -> CErrors.user_err (str "No open groups")
+  | {tag = "IT"} :: g :: gs when tag <> "IT" ->
+    end_group "IT"; end_group tag
+  | g :: gs ->
+    if g.tag <> tag then CErrors.user_err (str "Ending incorrect group");
+    group_stack := gs;
+    display "COMPLETEDIN" (Printf.sprintf "%.2f" ((e -. g.start_time) *. 1000.))
+
+let begin_group tag name =
+  let t = Unix.gettimeofday() in
+  let () =
+    match !group_stack with
+    | {tag = "IT"} :: _ when tag = "IT" -> end_group "IT"
+    | _ -> () in
+  group_stack := mk_group tag t :: !group_stack;
+  display tag name
 
 (* Based on the PrintAssumptions code from vernac/vernacentries.ml *)
 let assumptions r =

src/coq_cw.mli

@@ -2,4 +2,8 @@ val test_axioms : ?msg:string -> Libnames.qualid -> Libnames.qualid list -> unit
 
 val test_file_size : ?fname:string -> int -> unit
 
-val test_file_regex : ?fname:string -> bool -> string -> unit
+val test_file_regex : ?fname:string -> bool -> string -> unit
+
+val begin_group : string -> string -> unit
+
+val end_group : string -> unit

src/g_coq_cw.ml4

@@ -1,23 +1,40 @@
 DECLARE PLUGIN "coq_cw_plugin"
 
-open Pp
 open Stdarg
 
+VERNAC COMMAND EXTEND CWAssert CLASSIFIED AS QUERY
+| [ "CWAssert" string_opt(msg) ref(e) "Assumes" ref_list(axioms)] -> [ 
+        Coq_cw.test_axioms ?msg e axioms
+    ]
+END
+
 VERNAC COMMAND EXTEND CWTest CLASSIFIED AS QUERY
 | [ "CWTest" string_opt(msg) ref(e) "Assumes" ref_list(axioms)] -> [ 
         Coq_cw.test_axioms ?msg e axioms
     ]
 END
 
-VERNAC COMMAND EXTEND CWGroup CLASSIFIED AS QUERY
+VERNAC COMMAND EXTEND CWGroup CLASSIFIED AS SIDEFF
 | [ "CWGroup" string(msg)] -> [ 
-        Feedback.msg_notice (str ("\n<DESCRIBE::> " ^ msg ^ "\n"))
+        Coq_cw.begin_group "DESCRIBE" msg
+    ]
+END
+
+VERNAC COMMAND EXTEND CWEndGroup CLASSIFIED AS SIDEFF
+| [ "CWEndGroup"] -> [
+        Coq_cw.end_group "DESCRIBE"
+    ]
+END
+
+VERNAC COMMAND EXTEND CWTestCase CLASSIFIED AS SIDEFF
+| [ "CWTestCase" string(msg)] -> [ 
+        Coq_cw.begin_group "IT" msg
     ]
 END
 
-VERNAC COMMAND EXTEND CWEndGroup CLASSIFIED AS QUERY
-| [ "CWEndGroup"] -> [ 
-        Feedback.msg_notice (str "\n<COMPLETEDIN::>\n")
+VERNAC COMMAND EXTEND CWEnd CLASSIFIED AS SIDEFF
+| [ "CWEnd"] -> [
+        Coq_cw.end_group "IT"
     ]
 END