Renamed some commands and updated examples

Author: monadius

.gitignore

@@ -3,7 +3,7 @@
 *~
 .vscode/
 *.d
-Makefile
+/Makefile
 Makefile.conf
 .merlin
 *.vo

cw_example/Makefile

@@ -0,0 +1,4 @@
+all:
+	coqc Preloaded.v
+	coqc Solution.v
+	coqc -I ../src -Q ../theories CW SolutionTest.v

cw_example/SolutionTest.v

@@ -3,11 +3,17 @@ Require Import Preloaded.
 From CW Require Import Loader.
 
 CWGroup "Tests for Solution.solution".
-  CWTestCase "Type test".
+  CWTest "Type test".
+    (* The expected type should be in parentheses *)
     Fail CWAssert "Should fail" Solution.solution : (1 + 1 = 2).
     CWAssert Solution.solution : (1 + 1 = 3).
-  CWTestCase "Assumptions test".
+  (* CWEndTest is optional before CWTest or CWEndGroup *)
+  CWEndTest.
+  CWTest "Assumptions test".
     CWAssert "Testing solution" Solution.solution Assumes test_axiom.
+  CWTest "Type test 2".
+    Definition expected := 1 + 1 = 3.
+    CWAssert Solution.solution : expected.
 CWEndGroup.
 
 Definition solution_test := Solution.solution.
@@ -18,17 +24,17 @@ with line breaks".
 (line break)" solution_test Assumes test_axiom.
 CWEndGroup.
 
-CWTestCase "Without group".
+CWTest "Without group".
   CWAssert solution_test Assumes test_axiom.
-CWEnd.
+CWEndTest.
 
 CWGroup "Nested groups".
   CWGroup "Level 2".
-    CWTestCase "Test 1".
+    CWTest "Test 1".
       CWAssert solution_test Assumes test_axiom.
   CWEndGroup.
-  CWTestCase "Test 2".
+  CWTest "Test 2".
     CWAssert solution_test Assumes test_axiom.
     CWAssert solution_test Assumes test_axiom.
-  CWEnd.
+  CWEndTest.
 CWEndGroup.

cw_example/build.sh

@@ -14,12 +14,6 @@ VERNAC COMMAND EXTEND CWAssertAssumptions CLASSIFIED AS QUERY
     ]
 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 SIDEFF
 | [ "CWGroup" string(msg)] -> [ 
         Coq_cw.begin_group "DESCRIBE" msg
@@ -32,14 +26,14 @@ VERNAC COMMAND EXTEND CWEndGroup CLASSIFIED AS SIDEFF
     ]
 END
 
-VERNAC COMMAND EXTEND CWTestCase CLASSIFIED AS SIDEFF
-| [ "CWTestCase" string(msg)] -> [ 
+VERNAC COMMAND EXTEND CWTest CLASSIFIED AS SIDEFF
+| [ "CWTest" string(msg)] -> [ 
         Coq_cw.begin_group "IT" msg
     ]
 END
 
-VERNAC COMMAND EXTEND CWEnd CLASSIFIED AS SIDEFF
-| [ "CWEnd"] -> [
+VERNAC COMMAND EXTEND CWEndTest CLASSIFIED AS SIDEFF
+| [ "CWEndTest"] -> [
         Coq_cw.end_group "IT"
     ]
 END

src/g_coq_cw.ml4

@@ -25,23 +25,27 @@ End Test.
 
 CWGroup "Assumption Tests".
 
-Fail CWTest lemma1 Assumes.
-CWTest lemma1 Assumes my_ax.
-Fail CWTest lemma1 Assumes Classical_Prop.classic.
-Fail CWTest "lemma1" lemma1 Assumes lemma2.
-CWTest lemma1 Assumes Classical_Prop.classic my_ax.
-Fail CWTest "lemma2" lemma2 Assumes my_ax.
+Fail CWAssert lemma1 Assumes.
+CWAssert lemma1 Assumes my_ax.
+Fail CWAssert lemma1 Assumes Classical_Prop.classic.
+Fail CWAssert "lemma1" lemma1 Assumes lemma2.
+CWAssert lemma1 Assumes Classical_Prop.classic my_ax.
+Fail CWAssert "lemma2" lemma2 Assumes my_ax.
 
-CWTest Test.lemma3 Assumes Classical_Prop.classic my_ax.
-Fail CWTest Test.lemma3 Assumes my_ax.
+CWAssert Test.lemma3 Assumes Classical_Prop.classic my_ax.
+Fail CWAssert Test.lemma3 Assumes my_ax.
 
 CWEndGroup.
 
-CWFile "theories/Demo.v" Size < 1000.
+CWGroup "File Tests".
+
+CWFile "theories/Demo.v" Size < 1100.
 Fail CWFile "theories/Demo.v" Size < 200.
 
 CWFile "theories/Demo.v" Matches "Axiom".
 Fail CWFile "theories/Demo.v" Matches "$Theorem".
 
 Fail CWFile "theories/Demo.v" Does Not Match "Axiom".
 CWFile "theories/Demo.v" Does Not Match "$Theorem".
+
+CWEndGroup.

theories/Demo.v

@@ -16,13 +16,16 @@ Proof. intros. unfold fib_prog at 1. rewrite fix_sub_eq.
 
 From CW Require Import Loader.
 
-CWTest fib0 Assumes.
-CWTest fib1 Assumes.
-Fail CWTest fibSS Assumes.
+CWGroup "Program tests".
 
-CWTest fibSS Assumes proof_irrelevance.
-Fail CWTest fibSS Assumes functional_extensionality_dep.
+CWAssert fib0 Assumes.
+CWAssert fib1 Assumes.
+Fail CWAssert fibSS Assumes.
 
+CWAssert fibSS Assumes proof_irrelevance.
+Fail CWAssert fibSS Assumes functional_extensionality_dep.
+
+CWEndGroup.
 
 From Equations Require Import Equations.
 
@@ -34,18 +37,27 @@ Check fibE_equation_3.
 
 Print Assumptions fibE_equation_3.
 
-Fail CWTest fibE_equation_3 Assumes.
-Fail CWTest fibE_equation_3 Assumes proof_irrelevance.
-CWTest fibE_equation_3 Assumes functional_extensionality_dep.
+CWGroup "Equations tests".
+
+Fail CWAssert fibE_equation_3 Assumes.
+Fail CWAssert fibE_equation_3 Assumes proof_irrelevance.
+CWAssert fibE_equation_3 Assumes functional_extensionality_dep.
+
+CWEndGroup.
 
 From Coq Require Import Reals.
 
 Print Assumptions sqrt_pos.
 
-Fail CWTest sqrt_pos Assumes.
-CWTest sqrt_pos Assumes R R0 R1 R1_neq_R0 Rinv total_order_T
-     completeness archimed Rplus_opp_r Rplus_lt_compat_l
-     Rplus_comm Rplus_assoc Rplus_0_l Rplus Ropp
-     Rmult_plus_distr_l Rmult_lt_compat_l Rmult_comm
-     Rmult_assoc Rmult_1_l Rmult Rlt_trans Rlt_asym
-     Rlt Rinv_l Rinv up.
+CWGroup "Real numbers".
+
+Fail CWAssert sqrt_pos Assumes.
+CWAssert "Real Number Axioms" sqrt_pos Assumes
+  R R0 R1 Rplus Rmult Ropp Rinv Rlt up
+  Rplus_comm Rplus_assoc Rplus_opp_r Rplus_0_l
+  Rmult_comm Rmult_assoc Rinv_l Rmult_1_l R1_neq_R0
+  Rmult_plus_distr_l total_order_T
+  Rlt_asym Rlt_trans Rplus_lt_compat_l Rmult_lt_compat_l
+  archimed completeness.  
+
+CWEndGroup.