CWAssert for checking type

Author: monadius

cw_example/test.v

@@ -4,12 +4,14 @@ From CW Require Import Loader.
 
 CWGroup "Tests for solution.solution".
   CWTestCase "Type test".
-    Example solution_test : 1 + 1 = 3.
-    Proof. exact solution.solution. Qed.
+    Fail CWAssert "Should fail" solution.solution : (1 + 1 = 2).
+    CWAssert solution.solution : (1 + 1 = 3).
   CWTestCase "Assumptions test".
     CWAssert "Testing solution" solution.solution Assumes test_axiom.
 CWEndGroup.
 
+Definition solution_test := solution.solution.
+
 CWGroup "Another test
 with line breaks".
   CWAssert "Testing solution_test

src/coq_cw.ml

@@ -42,6 +42,27 @@ let begin_group tag name =
   group_stack := mk_group tag t :: !group_stack;
   display tag name
 
+let locate r =
+  try
+    let gr = Smartlocate.locate_global_with_alias r in
+    (gr, Globnames.printable_constr_of_global gr)
+  with Not_found -> CErrors.user_err (str "Not found: " ++ Libnames.pr_qualid r)
+  
+let test_type ?(msg = "Type Test") r c_ty =
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
+  let tm = EConstr.of_constr (snd (locate r)) in
+  let sigma, expected_ty = Constrintern.interp_constr_evars env sigma c_ty in
+  let actual_ty = Retyping.get_type_of ~lax:true env sigma tm in
+  match Reductionops.infer_conv env sigma actual_ty expected_ty with
+  | Some _ -> passed msg
+  | None ->
+    let p_actual = Printer.pr_econstr_env env sigma actual_ty in
+    let p_expected = Printer.pr_econstr_env env sigma expected_ty in
+    failed (Printf.sprintf "%s\nActual type = %s\nExpected type = %s"
+              msg (string_of_ppcmds p_actual) (string_of_ppcmds p_expected));
+    CErrors.user_err (str "Incorrect Type: " ++ Printer.pr_econstr_env env sigma tm)
+
 (* Based on the PrintAssumptions code from vernac/vernacentries.ml *)
 let assumptions r =
   try

src/coq_cw.mli

@@ -1,5 +1,7 @@
 val test_axioms : ?msg:string -> Libnames.qualid -> Libnames.qualid list -> unit
 
+val test_type : ?msg:string -> Libnames.qualid -> Constrexpr.constr_expr -> unit
+
 val test_file_size : ?fname:string -> int -> unit
 
 val test_file_regex : ?fname:string -> bool -> string -> unit

src/g_coq_cw.ml4

@@ -2,7 +2,13 @@ DECLARE PLUGIN "coq_cw_plugin"
 
 open Stdarg
 
-VERNAC COMMAND EXTEND CWAssert CLASSIFIED AS QUERY
+VERNAC COMMAND EXTEND CWAssertType CLASSIFIED AS QUERY
+| [ "CWAssert" string_opt(msg) ref(r) ":" constr(ty)] -> [ 
+        Coq_cw.test_type ?msg r ty
+    ]
+END
+
+VERNAC COMMAND EXTEND CWAssertAssumptions CLASSIFIED AS QUERY
 | [ "CWAssert" string_opt(msg) ref(e) "Assumes" ref_list(axioms)] -> [ 
         Coq_cw.test_axioms ?msg e axioms
     ]