-*.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
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
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
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
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
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)
$(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:
$(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
--- /dev/null
+(* 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))
+
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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 <file.test> ...";
+ prerr_endline " regtest (-gen|--gen) <file.cic> ...";
+ 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 ()
+
--- /dev/null
+\forall n:nat. \forall m. n + m = n
--- /dev/null
+[\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 ]
--- /dev/null
+[\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) ]
--- /dev/null
+[\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)) ]
--- /dev/null
+[\lambda x:bool. nat]
+match true:bool with
+[ true \Rightarrow O
+| false \Rightarrow (S O) ]
--- /dev/null
+[\lambda x:nat. nat]
+match O:nat with
+[ O \Rightarrow O
+| (S x) \Rightarrow (S (S x)) ]
--- /dev/null
+[\lambda x:list. list]
+match nil:list with
+[ nil \Rightarrow nil
+| (cons x y) \Rightarrow (cons x y) ]
--- /dev/null
+\lambda x:False.
+ [\lambda h:False. True]
+ match x:False with []
projects / helm.git / commitdiff