helm/software/components/tptp_grafite/Makefile

   1 PACKAGE = tptp_grafite
   2 PREDICATES =
   3
   4 INTERFACE_FILES= parser.mli parserTHF.mli tptp2grafite.mli
   5
   6 IMPLEMENTATION_FILES = ast.ml lexer.ml astTHF.ml lexerTHF.ml $(INTERFACE_FILES:%.mli=%.ml)
   7 EXTRA_OBJECTS_TO_INSTALL =
   8 EXTRA_OBJECTS_TO_CLEAN =
   9
  10 TPTPDIR= /home/$(USER)/work-area/TPTP-v3.2.0/
  11
  12 all: tptp2grafite mainTHF
  13 clean: clean_tests
  14
  15 clean_tests:
  16         rm -f tptp2grafite
  17
  18 %.mli %.ml: %.mly
  19         ocamlyacc $*.mly
  20 %.ml:%.mll
  21         ocamllex $*.mll
  22
  23 LOCAL_LINKOPTS = -package helm-$(PACKAGE) -linkpkg
  24 tptp2grafite: main.ml tptp_grafite.cma
  25         @echo "  OCAMLC $<"
  26         @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
  27
  28 mainTHF: mainTHF.ml tptp_grafite.cma
  29         @echo "  OCAMLC $<"
  30         @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
  31
  32 test: tptp2grafite mainTHF
  33
  34 testall: tptp2grafite
  35         for X in `cat unit_equality_problems`; do\
  36                 cat $(TPTPDIR)/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\
  37         done
  38
  39 generate-%:
  40         for X in `cat $*`; do\
  41                 ./tptp2grafite -tptppath $(TPTPDIR) $$X.p \
  42                 > ../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \
  43         done
  44
  45 ngenerate-%:
  46         for X in `cat $*`; do\
  47                 ./tptp2grafite -ng -tptppath $(TPTPDIR) $$X.p \
  48                 > ../../matita/contribs/ng_TPTP/$$X.ma || echo Failed: $$X; \
  49         done
  50
  51 parse-%:
  52         for X in `cat $*`; do\
  53           echo "Parsing $$X"; \
  54                 ./tptp2grafite -tptppath $(TPTPDIR) $$X.p \
  55                 > /dev/null || echo Failed: $$X; \
  56         done
  57
  58 include ../../Makefile.defs
  59 include ../Makefile.common
  60