1 (* Copyright (C) 2004, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 let argc = Array.length Sys.argv
31 prerr_endline "Usage: regtest <file.test> ...";
32 prerr_endline " regtest (-gen|--gen) <file.cic> ...";
36 let sep = Pcre.regexp rawsep
37 let msg_prefix = "*** REGTEST *** "
38 let print_msg s = prerr_endline (msg_prefix ^ s)
40 type state = Term | ETerm | EType | EReduced
42 (* regtest file format
43 * < cic term in concrete syntax >
44 * separator (* see sep above *)
45 * < expected cic term after disambiguation as PPed by CicPp.ppterm >
46 * separator (* see sep above *)
47 * < expected cic type as per type_of as PPed by CicPp.ppterm >
48 * separator (* see sep above *)
49 * < expected reduced cic term as PPed by CicPp.ppterm >
53 term: string; (* raw cic term *)
54 eterm: string; (* expected term *)
55 etype: string; (* expected type *)
56 ereduced: string; (* expected reduced term *)
59 (* this should be the only function here printing on stdout *)
60 let print_test test fname =
61 let oc = open_out fname in
64 [ test.term; rawsep ^ "\n";
65 test.eterm; rawsep ^ "\n";
66 test.etype; rawsep ^ "\n";
71 let term = Buffer.create 1024 in (* raw term *)
72 let eterm = Buffer.create 1024 in (* raw expected term *)
73 let etype = Buffer.create 1024 in (* raw expected type *)
74 let ereduced = Buffer.create 1024 in (* raw expected reducted term *)
75 let state = ref Term in
78 | Term -> state := ETerm
79 | ETerm -> state := EType
80 | EType -> state := EReduced
81 | EReduced -> assert false
83 let buffer_of_state = function
84 | Term -> term | ETerm -> eterm | EType -> etype | EReduced -> ereduced
88 Buffer.clear term; Buffer.clear eterm; Buffer.clear etype;
89 Buffer.clear ereduced;
90 let ic = open_in fname in
93 let line = input_line ic in
95 | l when Pcre.pmatch ~rex:sep l -> bump_state ()
96 | l -> Buffer.add_string (buffer_of_state !state) (line ^ "\n")
98 with End_of_file -> ());
99 { term = Buffer.contents term;
100 eterm = Buffer.contents eterm;
101 etype = Buffer.contents etype;
102 ereduced = Buffer.contents ereduced }
104 let as_expected expected found = (* ignores "term" field *)
105 let outcome = ref true in
106 if expected.eterm <> found.eterm then begin
107 print_msg "Term mismatch";
108 print_msg " expected:";
109 print_msg (" " ^ expected.eterm);
111 print_msg (" " ^ found.eterm);
114 if expected.etype <> found.etype then begin
115 print_msg "Type mismatch";
116 print_msg " expected:";
117 print_msg (" " ^ expected.etype);
119 print_msg (" " ^ found.etype);
122 if expected.ereduced <> found.ereduced then begin
123 print_msg "Reduced term mismatch";
124 print_msg " expected:";
125 print_msg (" " ^ expected.ereduced);
127 print_msg (" " ^ found.ereduced);
132 let test_this raw_term =
133 let empty_context = [] in
134 let (metasenv, cic_term) = BatchParser.parse raw_term in
135 let cic_type = CicTypeChecker.type_of_aux' metasenv empty_context cic_term in
136 let cic_reduced = CicReduction.whd empty_context cic_term in
138 term = raw_term; (* useless *)
139 eterm = CicPp.ppterm cic_term ^ "\n";
140 etype = CicPp.ppterm cic_type ^ "\n";
141 ereduced = CicPp.ppterm cic_reduced ^ "\n";
145 if Sys.argv.(1) = "-gen" || Sys.argv.(1) = "--gen" then begin (* gen mode *)
146 print_msg "[ Gen mode ]";
147 for i = 2 to argc - 1 do
148 let fname = Sys.argv.(i) in
149 let test_fname = fname ^ ".test" in
150 print_msg (sprintf "Generating regtest %s -> %s\n ..."
152 let raw_term = (parse_regtest fname).term in
153 let result = test_this raw_term in
154 print_test result test_fname
156 end else begin (* regtest mode *)
157 prerr_endline "[ Regtest mode ]";
158 let (ok, nok) = (ref 0, ref []) in
159 for i = 1 to argc - 1 do
160 let fname = Sys.argv.(i) in
161 prerr_endline ("# " ^ fname);
163 let expected = parse_regtest fname in
164 let actual = test_this expected.term in
165 if as_expected expected actual then
168 nok := fname :: !nok;
169 with e -> nok := fname :: !nok
171 print_msg "Regtest completed:";
172 print_msg (sprintf "Succeeded: %d" !ok);
173 print_msg (sprintf "Failed: %d" (List.length !nok));
174 List.iter (fun fname -> print_msg (sprintf " %s failed :-(" fname))
178 let _ = try main () with Invalid_argument _ -> usage ()