CWFile commands

Author: monadius

src/coq_cw.ml

@@ -1,15 +1,21 @@
 open Pp
 
+let solution_file = "/workspace/Solution.v"
+
+let passed msg = Feedback.msg_notice (str ("\n<PASSED::> " ^ msg ^ "\n"))
+
+let failed msg = Feedback.msg_notice (str ("\n<FAILED::> " ^ msg ^ "\n"))
+
 (* unused *)
-let extract_axioms s =
+(* let extract_axioms s =
   let fold t typ accu =
     match t with
     | Printer.Variable _ -> failwith "Variable"
     | Printer.Opaque _ -> failwith "Opaque"
     | Printer.Transparent _ -> failwith "Transparent"
     | Printer.Axiom _ -> typ :: accu
   in
-  Printer.ContextObjectMap.fold fold s []
+  Printer.ContextObjectMap.fold fold s [] *)
 
 (* TODO: compare axiom names (constants) also *)
 let test_assumptions msg env sigma s ax_tys =
@@ -24,7 +30,7 @@ let test_assumptions msg env sigma s ax_tys =
       let ety = EConstr.of_constr ty in
       if List.exists (unify ety) ax_tys then ()
       else begin
-        Feedback.msg_notice (str ("\n<FAILED::> " ^ msg ^ "\n"));
+        failed msg;
         CErrors.user_err (str "Axiom: " ++ Printer.pr_econstr_env env sigma ety)
       end
     | _ -> ()
@@ -51,4 +57,35 @@ let test ?(msg = "Axioms") c_ref ax_refs =
         let sigma, ty = Typing.type_of env sigma (EConstr.of_constr c) in
         sigma, ty :: tys) (sigma, []) ax_grs_cstrs in
   test_assumptions msg env sigma assumptions ax_tys;
-  Feedback.msg_notice (str ("\n<PASSED::> " ^ msg ^ "\n"))
+  passed msg
+
+(** Tests that the file size is less than a given number *)
+let test_file_size ?(fname = solution_file) size =
+  try
+    let stats = Unix.stat fname in
+    if stats.Unix.st_size < size then
+      passed (Format.sprintf "Size %d < %d" stats.Unix.st_size size)
+    else begin
+      let msg = Format.sprintf "Size %d >= %d" stats.Unix.st_size size in 
+      failed msg;
+      CErrors.user_err (str msg)
+    end
+  with Unix.Unix_error _ -> CErrors.user_err (str ("Bad file name: " ^ fname))
+
+(** Tests that the file's content matches a given regular expression*)
+let test_file_regex ?(fname = solution_file) match_flag regex =
+  let re = Str.regexp regex in
+  let ic = open_in fname in
+  let n = in_channel_length ic in
+  let s = really_input_string ic n in
+  let () = close_in ic in
+  let matched = try ignore (Str.search_forward re s 0); true
+                with Not_found -> false in
+  if matched = match_flag then
+    passed "OK"
+  else begin
+    failed "Bad match";
+    CErrors.user_err (str "Bad match")
+  end
+
+

src/coq_cw.mli

@@ -1 +1,5 @@
-val test : ?msg:string -> Libnames.qualid -> Libnames.qualid list -> unit
+val test : ?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

src/g_coq_cw.ml4

@@ -20,3 +20,21 @@ VERNAC COMMAND EXTEND CWEndGroup CLASSIFIED AS QUERY
         Feedback.msg_notice (str "\n<COMPLETEDIN::>\n")
     ]
 END
+
+VERNAC COMMAND EXTEND CWFileSize CLASSIFIED AS QUERY
+| [ "CWFile" string_opt(fname) "Size" "<" int(size)] -> [ 
+        Coq_cw.test_file_size ?fname size
+    ]
+END
+
+VERNAC COMMAND EXTEND CWFileMatch CLASSIFIED AS QUERY
+| [ "CWFile" string_opt(fname) "Matches" string(regex)] -> [ 
+        Coq_cw.test_file_regex ?fname true regex
+    ]
+END
+
+VERNAC COMMAND EXTEND CWFileNegMatch CLASSIFIED AS QUERY
+| [ "CWFile" string_opt(fname) "Does" "Not" "Match" string(regex)] -> [ 
+        Coq_cw.test_file_regex ?fname false regex
+    ]
+END

theories/Demo.v

@@ -29,4 +29,13 @@ CWTest "lemma2" lemma2 Assumes my_ax.
 CWTest lemma3 Assumes classic my_ax.
 Fail CWTest lemma3 Assumes my_ax.
 
-CWEndGroup.
+CWEndGroup.
+
+CWFile "theories/Demo.v" Size < 1000.
+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".