From 5d8d504eb46d181d7a915b2be154022ea83da4df Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 May 2006 08:26:38 +0000 Subject: [PATCH] few fixes --- components/binaries/tptp2grafite/Makefile | 6 ++++++ components/binaries/tptp2grafite/main.ml | 8 ++++++++ 2 files changed, 14 insertions(+) diff --git a/components/binaries/tptp2grafite/Makefile b/components/binaries/tptp2grafite/Makefile index 81e30eab3..d79c2661d 100644 --- a/components/binaries/tptp2grafite/Makefile +++ b/components/binaries/tptp2grafite/Makefile @@ -31,3 +31,9 @@ generate: > ../../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \ done +parse: + for X in `cat unit_equality_problems`; do\ + echo "Parsing $$X"; \ + ./tptp2grafite -tptppath /home/tassi/TPTP-v3.1.1/ $$X \ + > /dev/null || echo Failed: $$X; \ + done diff --git a/components/binaries/tptp2grafite/main.ml b/components/binaries/tptp2grafite/main.ml index 8df37fe00..315bfc100 100644 --- a/components/binaries/tptp2grafite/main.ml +++ b/components/binaries/tptp2grafite/main.ml @@ -51,6 +51,12 @@ let collect_fv_from_atom a = HExtlib.list_uniq (List.sort compare (aux a)) ;; +let collect_fv_from_formulae = function + | A.Disjunction _ -> assert false + | A.NegAtom a + | A.Atom a -> collect_fv_from_atom a +;; + let rec convert_term = function | A.Variable x -> mk_ident x | A.Constant x -> mk_ident x @@ -144,6 +150,8 @@ let convert_ast statements context = function | A.Hypothesis -> statements, f::context | A.Negated_conjecture -> + if collect_fv_from_formulae f <> [] then + (*prerr_endline "CONTIENE FV";*)(); let f = PT.Binder (`Forall, -- 2.39.2