PACKAGE = tptp_grafite
PREDICATES = 

INTERFACE_FILES= parser.mli tptp2grafite.mli

IMPLEMENTATION_FILES = ast.ml lexer.ml $(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL = 
EXTRA_OBJECTS_TO_CLEAN =

TPTPDIR= /home/$(USER)/work-area/TPTP-v3.2.0/

all: tptp2grafite
clean: clean_tests

clean_tests:
	rm -f tptp2grafite

parser.mli parser.ml:parser.mly
	ocamlyacc parser.mly
lexer.ml:
	ocamllex lexer.mll

LOCAL_LINKOPTS = -package helm-$(PACKAGE) -linkpkg
tptp2grafite: main.ml tptp_grafite.cma
	@echo "  OCAMLC $<"
	@$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<

test: tptp2grafite

testall: tptp2grafite
	for X in `cat unit_equality_problems`; do\
		cat $(TPTPDIR)/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\
	done

generate-%:
	for X in `cat $*`; do\
		./tptp2grafite -tptppath $(TPTPDIR) $$X.p \
		> ../../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"; \
		./tptp2grafite -tptppath $(TPTPDIR) $$X.p \
		> /dev/null || echo Failed: $$X; \
	done

include ../../Makefile.defs
include ../Makefile.common