From: Stefano Zacchiroli Date: Fri, 30 Jan 2004 08:10:16 +0000 (+0000) Subject: added regression tests X-Git-Tag: V_0_2_3~123 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ded0396c81ec49a45d9406becb602e1071e6820b;p=helm.git added regression tests --- diff --git a/helm/gTopLevel/.cvsignore b/helm/gTopLevel/.cvsignore index 3d496b73a..61337747a 100644 --- a/helm/gTopLevel/.cvsignore +++ b/helm/gTopLevel/.cvsignore @@ -1,4 +1,7 @@ -*.cm[iox] gTopLevel gTopLevel.opt styles stylesheets meta_stylesheets +*.cm[iox] +gTopLevel gTopLevel.opt +regtest regtest.opt +styles stylesheets meta_stylesheets chosenTermEditor.ml chosenTransformer.ml disambiguatingParser.ml diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 8bfe05a39..6045cb9b9 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -1,5 +1,5 @@ termEditor.cmi: disambiguatingParser.cmi -texTermEditor.cmi: oldDisambiguate.cmi +texTermEditor.cmi: disambiguatingParser.cmi invokeTactics.cmi: termEditor.cmi termViewer.cmi hbugs.cmi: invokeTactics.cmi chosenTermEditor.cmi: disambiguatingParser.cmi @@ -13,8 +13,8 @@ disambiguatingParser.cmo: oldDisambiguate.cmi disambiguatingParser.cmi disambiguatingParser.cmx: oldDisambiguate.cmx disambiguatingParser.cmi termEditor.cmo: disambiguatingParser.cmi termEditor.cmi termEditor.cmx: disambiguatingParser.cmx termEditor.cmi -texTermEditor.cmo: oldDisambiguate.cmi texTermEditor.cmi -texTermEditor.cmx: oldDisambiguate.cmx texTermEditor.cmi +texTermEditor.cmo: disambiguatingParser.cmi texTermEditor.cmi +texTermEditor.cmx: disambiguatingParser.cmx texTermEditor.cmi xmlDiff.cmo: xmlDiff.cmi xmlDiff.cmx: xmlDiff.cmi chosenTransformer.cmo: chosenTransformer.cmi @@ -29,11 +29,15 @@ invokeTactics.cmx: logicalOperations.cmx proofEngine.cmx termEditor.cmx \ termViewer.cmx invokeTactics.cmi hbugs.cmo: invokeTactics.cmi proofEngine.cmi hbugs.cmi hbugs.cmx: invokeTactics.cmx proofEngine.cmx hbugs.cmi -chosenTermEditor.cmo: texTermEditor.cmi chosenTermEditor.cmi -chosenTermEditor.cmx: texTermEditor.cmx chosenTermEditor.cmi +chosenTermEditor.cmo: termEditor.cmi chosenTermEditor.cmi +chosenTermEditor.cmx: termEditor.cmx chosenTermEditor.cmi gTopLevel.cmo: chosenTermEditor.cmi chosenTransformer.cmi \ disambiguatingParser.cmi hbugs.cmi invokeTactics.cmi \ logicalOperations.cmi proofEngine.cmi termEditor.cmi termViewer.cmi gTopLevel.cmx: chosenTermEditor.cmx chosenTransformer.cmx \ disambiguatingParser.cmx hbugs.cmx invokeTactics.cmx \ logicalOperations.cmx proofEngine.cmx termEditor.cmx termViewer.cmx +regtest.cmo: batchParser.cmi +regtest.cmx: batchParser.cmx +batchParser.cmo: disambiguatingParser.cmi batchParser.cmi +batchParser.cmx: disambiguatingParser.cmx batchParser.cmi diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 3904c6d22..abe03e42d 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -13,8 +13,8 @@ OCAMLDEP = ocamldep -pp camlp4o LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) -all: styles gTopLevel -opt: styles gTopLevel.opt +all: styles gTopLevel regtest +opt: styles gTopLevel.opt regtest.opt start: $(MAKE) -C ../hbugs/ start @@ -27,9 +27,13 @@ INTERFACE_FILES = \ chosenTransformer.mli termViewer.mli invokeTactics.mli hbugs.mli \ chosenTermEditor.mli -DEPOBJS = $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) gTopLevel.ml +DEPOBJS = \ + $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \ + gTopLevel.ml regtest.ml batchParser.ml batchParser.mli TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) gTopLevel.cmo +REGTESTOBJS = \ + $(INTERFACE_FILES:%.mli=%.cmo) batchParser.cmo regtest.cmo $(INTERFACE_FILES:%.mli=%.cmo): $(LIBRARIES) $(INTERFACE_FILES:%.mli=%.cmx): $(LIBRARIES_OPT) @@ -47,10 +51,14 @@ depend: $(OCAMLDEP) $(DEPOBJS) > .depend gTopLevel: $(TOPLEVELOBJS) $(LIBRARIES) - $(OCAMLC) -linkpkg -o gTopLevel $(TOPLEVELOBJS) - + $(OCAMLC) -linkpkg -o $@ $(TOPLEVELOBJS) gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) - $(OCAMLOPT) -linkpkg -o gTopLevel.opt $(TOPLEVELOBJS:.cmo=.cmx) + $(OCAMLOPT) -linkpkg -o $@ $(TOPLEVELOBJS:.cmo=.cmx) + +regtest: $(REGTESTOBJS) $(LIBRARIES) + $(OCAMLC) -linkpkg -o $@ $(REGTESTOBJS) +regtest.opt: $(REGTESTOBJS:.cmo=.cmx) $(LIBRARIES) + $(OCAMLOPT) -linkpkg -o $@ $(REGTESTOBJS:.cmo=.cmx) .SUFFIXES: .ml .mli .cmo .cmi .cmx .ml.cmo: @@ -64,15 +72,20 @@ $(TOPLEVELOBJS): $(LIBRARIES) $(TOPLEVELOBJS:.cmo=.cmx)): $(LIBRARIES_OPT) clean: - rm -f *.cm[iox] *.o gTopLevel gTopLevel.opt - + rm -f *.cm[iox] *.o gTopLevel{,.opt} regtest{,.opt} install: cp gTopLevel gTopLevel.opt $(BIN_DIR) - uninstall: rm -f $(BIN_DIR)/gTopLevel $(BIN_DIR)/gTopLevel.opt -.PHONY: install uninstall clean +.PHONY: install uninstall clean test + +TESTS := $(patsubst %, %.test, $(wildcard tests/*.cic)) +gentest: $(TESTS) +tests/%.cic.test: tests/%.cic + ./regtest -gen $< +test: + ./regtest $(TESTS) ifneq ($(MAKECMDGOALS), depend) include .depend diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml new file mode 100644 index 000000000..05fd7a614 --- /dev/null +++ b/helm/gTopLevel/batchParser.ml @@ -0,0 +1,68 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +let verbose = false + +exception Failure of string +let fail msg = raise (Failure msg) + +module DisambiguateCallbacks = + struct + let output_html ?(append_NL = true) msg = + if verbose then + (if append_NL then print_string else print_endline) + (Ui_logger.string_of_html_msg msg) + + let interactive_user_uri_choice + ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id = + List.filter + (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) + + let interactive_interpretation_choice _ = fail "Multiple interpretations" + let input_or_locate_uri ~title = fail "Unknown identifier" + end + +module Disambiguate' = DisambiguatingParser.Make (DisambiguateCallbacks) + +let mqi_debug_fun = ignore +let mqi_flags = [] +let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun + +let parse = + let empty_environment = + DisambiguatingParser.EnvironmentP3.of_string + DisambiguatingParser.EnvironmentP3.empty + in + let empty_context = [] in + let empty_metasenv = [] in + fun input -> + let (_, metasenv, term) = + Disambiguate'.disambiguate_term + mqi_handle empty_context empty_metasenv input empty_environment + in + (metasenv, term) + +let parse_pp input = CicPp.ppterm (snd (parse input)) + diff --git a/helm/gTopLevel/batchParser.mli b/helm/gTopLevel/batchParser.mli new file mode 100644 index 000000000..7d8f4bcd7 --- /dev/null +++ b/helm/gTopLevel/batchParser.mli @@ -0,0 +1,36 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +exception Failure of string + + (** Parse a cic term from the given string using disambiguating parser in + * batch mode if possible, otherwise raises Failure above *) +val parse: string -> Cic.metasenv * Cic.term + + (** as above, but instead of returning the parsed cic term, pretty prints it + * (ignoring returned metasenv) + *) +val parse_pp: string -> string + diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml new file mode 100644 index 000000000..a38d5a02b --- /dev/null +++ b/helm/gTopLevel/regtest.ml @@ -0,0 +1,177 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf + +let argc = Array.length Sys.argv + +let usage () = + prerr_endline "Usage: regtest ..."; + prerr_endline " regtest (-gen|--gen) ..."; + exit 2 + +let rawsep = "###" +let sep = Pcre.regexp rawsep +let msg_prefix = "*** REGTEST *** " +let print_msg s = prerr_endline (msg_prefix ^ s) + +type state = Term | ETerm | EType | EReduced + +(* regtest file format + * < cic term in concrete syntax > + * separator (* see sep above *) + * < expected cic term after disambiguation as PPed by CicPp.ppterm > + * separator (* see sep above *) + * < expected cic type as per type_of as PPed by CicPp.ppterm > + * separator (* see sep above *) + * < expected reduced cic term as PPed by CicPp.ppterm > + *) + +type regtest = { + term: string; (* raw cic term *) + eterm: string; (* expected term *) + etype: string; (* expected type *) + ereduced: string; (* expected reduced term *) +} + + (* this should be the only function here printing on stdout *) +let print_test test fname = + let oc = open_out fname in + output_string oc + (String.concat "" + [ test.term; rawsep ^ "\n"; + test.eterm; rawsep ^ "\n"; + test.etype; rawsep ^ "\n"; + test.ereduced ]); + close_out oc + +let parse_regtest = + let term = Buffer.create 1024 in (* raw term *) + let eterm = Buffer.create 1024 in (* raw expected term *) + let etype = Buffer.create 1024 in (* raw expected type *) + let ereduced = Buffer.create 1024 in (* raw expected reducted term *) + let state = ref Term in + let bump_state () = + match !state with + | Term -> state := ETerm + | ETerm -> state := EType + | EType -> state := EReduced + | EReduced -> assert false + in + let buffer_of_state = function + | Term -> term | ETerm -> eterm | EType -> etype | EReduced -> ereduced + in + fun fname -> + state := Term; + Buffer.clear term; Buffer.clear eterm; Buffer.clear etype; + Buffer.clear ereduced; + let ic = open_in fname in + (try + while true do + let line = input_line ic in + match line with + | l when Pcre.pmatch ~rex:sep l -> bump_state () + | l -> Buffer.add_string (buffer_of_state !state) (line ^ "\n") + done + with End_of_file -> ()); + { term = Buffer.contents term; + eterm = Buffer.contents eterm; + etype = Buffer.contents etype; + ereduced = Buffer.contents ereduced } + +let as_expected expected found = (* ignores "term" field *) + let outcome = ref true in + if expected.eterm <> found.eterm then begin + print_msg "Term mismatch"; + print_msg " expected:"; + print_msg (" " ^ expected.eterm); + print_msg " found:"; + print_msg (" " ^ found.eterm); + outcome := false; + end; + if expected.etype <> found.etype then begin + print_msg "Type mismatch"; + print_msg " expected:"; + print_msg (" " ^ expected.etype); + print_msg " found:"; + print_msg (" " ^ found.etype); + outcome := false; + end; + if expected.ereduced <> found.ereduced then begin + print_msg "Reduced term mismatch"; + print_msg " expected:"; + print_msg (" " ^ expected.ereduced); + print_msg " found:"; + print_msg (" " ^ found.ereduced); + outcome := false; + end; + !outcome + +let test_this raw_term = + let empty_context = [] in + let (metasenv, cic_term) = BatchParser.parse raw_term in + let cic_type = CicTypeChecker.type_of_aux' metasenv empty_context cic_term in + let cic_reduced = CicReduction.whd empty_context cic_term in + { + term = raw_term; (* useless *) + eterm = CicPp.ppterm cic_term ^ "\n"; + etype = CicPp.ppterm cic_type ^ "\n"; + ereduced = CicPp.ppterm cic_reduced ^ "\n"; + } + +let main () = + if Sys.argv.(1) = "-gen" || Sys.argv.(1) = "--gen" then begin (* gen mode *) + print_msg "[ Gen mode ]"; + for i = 2 to argc - 1 do + let fname = Sys.argv.(i) in + let test_fname = fname ^ ".test" in + print_msg (sprintf "Generating regtest %s -> %s\n ..." + fname test_fname); + let raw_term = (parse_regtest fname).term in + let result = test_this raw_term in + print_test result test_fname + done + end else begin (* regtest mode *) + prerr_endline "[ Regtest mode ]"; + let (ok, nok) = (ref 0, ref []) in + for i = 1 to argc - 1 do + let fname = Sys.argv.(i) in + prerr_endline ("# " ^ fname); + let expected = parse_regtest fname in + let actual = test_this expected.term in + if as_expected expected actual then + incr ok + else + nok := fname :: !nok; + done; + print_msg "Regtest completed:"; + print_msg (sprintf "Succeeded: %d" !ok); + print_msg (sprintf "Failed: %d" (List.length !nok)); + List.iter (fun fname -> print_msg (sprintf " %s failed :-(" fname)) + (List.rev !nok) + end + +let _ = try main () with Invalid_argument _ -> usage () + diff --git a/helm/gTopLevel/tests/.cvsignore b/helm/gTopLevel/tests/.cvsignore new file mode 100644 index 000000000..9ed3b07ce --- /dev/null +++ b/helm/gTopLevel/tests/.cvsignore @@ -0,0 +1 @@ +*.test diff --git a/helm/gTopLevel/tests/forall00.cic b/helm/gTopLevel/tests/forall00.cic new file mode 100644 index 000000000..e53571c50 --- /dev/null +++ b/helm/gTopLevel/tests/forall00.cic @@ -0,0 +1 @@ +\forall n:nat. \forall m. n + m = n diff --git a/helm/gTopLevel/tests/match00.cic b/helm/gTopLevel/tests/match00.cic new file mode 100644 index 000000000..bcfd70ea7 --- /dev/null +++ b/helm/gTopLevel/tests/match00.cic @@ -0,0 +1,6 @@ +[\lambda x:nat. + [\lambda y:nat. Set] + match x:nat with [ O \Rightarrow nat | (S x) \Rightarrow bool ]] +match (S O):nat with +[ O \Rightarrow O +| (S x) \Rightarrow false ] diff --git a/helm/gTopLevel/tests/match01.cic b/helm/gTopLevel/tests/match01.cic new file mode 100644 index 000000000..04948778a --- /dev/null +++ b/helm/gTopLevel/tests/match01.cic @@ -0,0 +1,4 @@ +[\lambda z:nat. \lambda h:(le O z). (eq nat O O)] +match (le_n O): le with +[ le_n \Rightarrow (refl_equal nat O) +| (le_S x y) \Rightarrow (refl_equal nat O) ] diff --git a/helm/gTopLevel/tests/match02.cic b/helm/gTopLevel/tests/match02.cic new file mode 100644 index 000000000..4a5c69782 --- /dev/null +++ b/helm/gTopLevel/tests/match02.cic @@ -0,0 +1,4 @@ +[\lambda z:nat. \lambda h:(le 0 z). (le 0 (S z))] +match (le_S 0 0 (le_n 0)): le with +[ le_n \Rightarrow (le_S 0 0 (le_n 0)) +| (le_S x y) \Rightarrow (le_S 0 (S x) (le_S 0 x y)) ] diff --git a/helm/gTopLevel/tests/match03.cic b/helm/gTopLevel/tests/match03.cic new file mode 100644 index 000000000..e4064b378 --- /dev/null +++ b/helm/gTopLevel/tests/match03.cic @@ -0,0 +1,4 @@ +[\lambda x:bool. nat] +match true:bool with +[ true \Rightarrow O +| false \Rightarrow (S O) ] diff --git a/helm/gTopLevel/tests/match04.cic b/helm/gTopLevel/tests/match04.cic new file mode 100644 index 000000000..6de9a5ba1 --- /dev/null +++ b/helm/gTopLevel/tests/match04.cic @@ -0,0 +1,4 @@ +[\lambda x:nat. nat] +match O:nat with +[ O \Rightarrow O +| (S x) \Rightarrow (S (S x)) ] diff --git a/helm/gTopLevel/tests/match05.cic b/helm/gTopLevel/tests/match05.cic new file mode 100644 index 000000000..10a54db0d --- /dev/null +++ b/helm/gTopLevel/tests/match05.cic @@ -0,0 +1,4 @@ +[\lambda x:list. list] +match nil:list with +[ nil \Rightarrow nil +| (cons x y) \Rightarrow (cons x y) ] diff --git a/helm/gTopLevel/tests/match06.cic b/helm/gTopLevel/tests/match06.cic new file mode 100644 index 000000000..fd9677fc1 --- /dev/null +++ b/helm/gTopLevel/tests/match06.cic @@ -0,0 +1,3 @@ +\lambda x:False. + [\lambda h:False. True] + match x:False with []