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 | EMetasenv | 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 emetasenv : string; (* expected metasenv *)
55 eterm: string; (* expected term *)
56 etype: string; (* expected type *)
57 ereduced: string; (* expected reduced term *)
60 (* this should be the only function here printing on stdout *)
61 let print_test test fname =
62 let oc = open_out fname in
65 [ test.term; rawsep ^ "\n";
66 test.emetasenv; rawsep ^ "\n";
67 test.eterm; rawsep ^ "\n";
68 test.etype; rawsep ^ "\n";
73 let term = Buffer.create 1024 in (* raw term *)
74 let emetasenv = Buffer.create 1024 in (* expected metasenv *)
75 let eterm = Buffer.create 1024 in (* raw expected term *)
76 let etype = Buffer.create 1024 in (* raw expected type *)
77 let ereduced = Buffer.create 1024 in (* raw expected reducted term *)
78 let state = ref Term in
81 | Term -> state := EMetasenv
82 | EMetasenv -> state := ETerm
83 | ETerm -> state := EType
84 | EType -> state := EReduced
85 | EReduced -> assert false
87 let buffer_of_state = function
88 | Term -> term | EMetasenv -> emetasenv | ETerm -> eterm | EType -> etype | EReduced -> ereduced
92 Buffer.clear term; Buffer.clear emetasenv; Buffer.clear eterm;
93 Buffer.clear etype; Buffer.clear ereduced;
94 let ic = open_in fname in
97 let line = input_line ic in
99 | l when Pcre.pmatch ~rex:sep l -> bump_state ()
100 | l -> Buffer.add_string (buffer_of_state !state) (line ^ "\n")
102 with End_of_file -> ());
103 { term = Buffer.contents term;
104 emetasenv = Buffer.contents emetasenv;
105 eterm = Buffer.contents eterm;
106 etype = Buffer.contents etype;
107 ereduced = Buffer.contents ereduced }
109 let as_expected expected found = (* ignores "term" field *)
110 let outcome = ref true in
111 if expected.eterm <> found.eterm then begin
112 print_msg "Term mismatch";
113 print_msg " expected:";
114 print_msg (" " ^ expected.eterm);
116 print_msg (" " ^ found.eterm);
119 if expected.etype <> found.etype then begin
120 print_msg "Type mismatch";
121 print_msg " expected:";
122 print_msg (" " ^ expected.etype);
124 print_msg (" " ^ found.etype);
127 if expected.ereduced <> found.ereduced then begin
128 print_msg "Reduced term mismatch";
129 print_msg " expected:";
130 print_msg (" " ^ expected.ereduced);
132 print_msg (" " ^ found.ereduced);
137 let test_this raw_term =
138 let empty_context = [] in
139 let (metasenv, cic_term) = BatchParser.parse raw_term in
142 CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv empty_context cic_term)
148 CicPp.ppterm (CicReduction.whd empty_context cic_term)
153 term = raw_term; (* useless *)
154 emetasenv = CicMetaSubst.ppmetasenv metasenv [] ^ "\n";
155 eterm = CicPp.ppterm cic_term ^ "\n";
156 etype = etype ^ "\n";
157 ereduced = ereduced ^ "\n";
161 if Sys.argv.(1) = "-gen" || Sys.argv.(1) = "--gen" then begin (* gen mode *)
162 print_msg "[ Gen mode ]";
163 for i = 2 to argc - 1 do
164 let fname = Sys.argv.(i) in
165 let test_fname = fname ^ ".test" in
166 print_msg (sprintf "Generating regtest %s -> %s\n ..."
168 let raw_term = (parse_regtest fname).term in
169 let result = test_this raw_term in
170 print_test result test_fname
172 end else begin (* regtest mode *)
173 prerr_endline "[ Regtest mode ]";
174 let (ok, nok) = (ref 0, ref []) in
175 for i = 1 to argc - 1 do
176 let fname = Sys.argv.(i) in
177 prerr_endline ("# " ^ fname);
179 let expected = parse_regtest fname in
180 let actual = test_this expected.term in
181 if as_expected expected actual then
184 nok := fname :: !nok;
185 with e -> nok := fname :: !nok
187 print_msg "Regtest completed:";
188 print_msg (sprintf "Succeeded: %d" !ok);
189 print_msg (sprintf "Failed: %d" (List.length !nok));
190 List.iter (fun fname -> print_msg (sprintf " %s failed :-(" fname))
194 let _ = try main () with Invalid_argument _ -> usage ()