OCAMLC = OCAMLPATH=../../METAS ocamlfind ocamlc -package helm-grafite_parser
TPTPDIR=/home/$(USER)/TPTP-v3.1.1/

opt all: tptp2grafite
	echo -n

tptp2grafite: ast.ml parser.mly lexer.mll main.ml
	$(OCAMLC) -c ast.ml
	ocamlyacc parser.mly
	$(OCAMLC) -c parser.mli
	$(OCAMLC) -c parser.ml
	ocamllex lexer.mll
	$(OCAMLC) -c lexer.ml
	$(OCAMLC) -c main.ml
	$(OCAMLC) -linkpkg -o tptp2grafite ast.cmo lexer.cmo parser.cmo main.cmo

clean:
	rm -f tptp2grafite *.cmo *.cmi parser.mli parser.ml lexer.ml rm *.output

test: tptp2grafite
	cat $(TPTPDIR)/`head -n 1 unit_equality_problems` | ./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 unit_equality_problems`; do\
		./tptp2grafite -tptppath $(TPTPDIR) $$X \
		> ../../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \
	done

parse:
	for X in `cat unit_equality_problems`; do\
	  echo "Parsing $$X"; \
		./tptp2grafite -tptppath $(TPTPDIR) $$X \
		> /dev/null || echo Failed: $$X; \
	done