thf problems list for tptp 4.0.1

[helm.git] / helm / software / components / tptp_grafite / Makefile

diff --git a/helm/software/components/tptp_grafite/Makefile b/helm/software/components/tptp_grafite/Makefile
index 4e4d316772c34cfa56a245b86aaa265612504e8b..b89f39ed5124a98e46480b34d229739afb7f391d 100644 (file)
--- a/helm/software/components/tptp_grafite/Makefile
+++ b/helm/software/components/tptp_grafite/Makefile
@@ -1,31 +1,44 @@
 PACKAGE = tptp_grafite
 PREDICATES = 
 
-INTERFACE_FILES= parser.mli tptp2grafite.mli
+INTERFACE_FILES= parser.mli parserTHF.mli tptp2grafite.mli
 
-IMPLEMENTATION_FILES = ast.ml lexer.ml $(INTERFACE_FILES:%.mli=%.ml)
+IMPLEMENTATION_FILES = ast.ml lexer.ml astTHF.ml lexerTHF.ml $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL = 
 EXTRA_OBJECTS_TO_CLEAN =
 
-TPTPDIR=/home/$(USER)/TPTP-v3.1.1/
+TPTPDIR= /home/$(USER)/work-area/TPTP-v3.2.0/
 
-all: tptp2grafite
-clean: clean_tests
+all: tptp2grafite mainTHF
+clean: clean_tests clean_generated
+
+clean_generated:
+       rm -f parser.mli parser.ml parserTHF.mli parserTHF.ml 
+       rm -f lexer.ml lexerTHF.ml
 
 clean_tests:
        rm -f tptp2grafite
 
-parser.mli parser.ml:parser.mly
-       ocamlyacc parser.mly
-lexer.ml:
-       ocamllex lexer.mll
+lexer.cmo: parser.cmi
+lexer.cmx: parser.cmi
+lexerTHF.cmo: parserTHF.cmi
+lexerTHF.cmx: parserTHF.cmi
+
+%.mli %.ml: %.mly
+       ocamlyacc $*.mly
+%.ml:%.mll
+       ocamllex $*.mll
 
 LOCAL_LINKOPTS = -package helm-$(PACKAGE) -linkpkg
 tptp2grafite: main.ml tptp_grafite.cma
        @echo "  OCAMLC $<"
        @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
 
-test: tptp2grafite
+mainTHF: mainTHF.ml tptp_grafite.cma 
+       @echo "  OCAMLC $<"
+       @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
+
+test: tptp2grafite mainTHF
 
 testall: tptp2grafite
        for X in `cat unit_equality_problems`; do\
@@ -38,6 +51,12 @@ generate-%:
                > ../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \
        done
 
+ngenerate-%:
+       for X in `cat $*`; do\
+               ./tptp2grafite -ng -tptppath $(TPTPDIR) $$X.p \
+               > ../../matita/contribs/ng_TPTP/$$X.ma || echo Failed: $$X; \
+       done
+
 parse-%:
        for X in `cat $*`; do\
          echo "Parsing $$X"; \