X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2FMakefile;h=e452480d8430ec07a2d6b919628c563e49f55e9e;hb=964844c87f7c3d7061dfeb7f2d84b6b8bbcdaf13;hp=c5c6e63469782de7a2a249a92201a58ef040e3b1;hpb=bc76b4d2f3c380894259b45fad52cf85ae6cee18;p=helm.git

diff --git a/helm/software/components/tptp_grafite/Makefile b/helm/software/components/tptp_grafite/Makefile
index c5c6e6346..e452480d8 100644
--- a/helm/software/components/tptp_grafite/Makefile
+++ b/helm/software/components/tptp_grafite/Makefile
@@ -1,50 +1,77 @@
 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-v4.0.1/
 
-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\
 		cat $(TPTPDIR)/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\
 	done
 
-generate:
-	for X in `cat unit_equality_problems`; do\
-		./tptp2grafite -tptppath $(TPTPDIR) $$X \
-		> ../../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \
+generate-%:
+	for X in `cat $*`; do\
+		./tptp2grafite -tptppath $(TPTPDIR) $$X.p \
+		> ../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \
 	done
 
-parse:
-	for X in `cat unit_equality_problems`; do\
+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"; \
-		./tptp2grafite -tptppath $(TPTPDIR) $$X \
+		./tptp2grafite -tptppath $(TPTPDIR) $$X.p \
 		> /dev/null || echo Failed: $$X; \
 	done
 
+thf:
+	rm -rf THF
+	mkdir THF
+	for x in `cat thf_problems`; do\
+		echo $$x;\
+		./mainTHF -tptppath $(TPTPDIR) $$x.p > THF/$$x.ma;\
+	done
+
 include ../../Makefile.defs
 include ../Makefile.common