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-v4.0.1/
  11
  12 all: tptp2grafite mainTHF
  13 clean: clean_tests clean_generated
  14
  15 clean_generated:
  16         rm -f parser.mli parser.ml parserTHF.mli parserTHF.ml
  17         rm -f lexer.ml lexerTHF.ml
  18
  19 clean_tests:
  20         rm -f tptp2grafite
  21
  22 lexer.cmo: parser.cmi
  23 lexer.cmx: parser.cmi
  24 lexerTHF.cmo: parserTHF.cmi
  25 lexerTHF.cmx: parserTHF.cmi
  26
  27 %.mli %.ml: %.mly
  28         ocamlyacc $*.mly
  29 %.ml:%.mll
  30         ocamllex $*.mll
  31
  32 LOCAL_LINKOPTS = -package helm-$(PACKAGE) -linkpkg
  33 tptp2grafite: main.ml tptp_grafite.cma
  34         @echo "  OCAMLC $<"
  35         @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
  36
  37 mainTHF: mainTHF.ml tptp_grafite.cma
  38         @echo "  OCAMLC $<"
  39         @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
  40
  41 test: tptp2grafite mainTHF
  42
  43 testall: tptp2grafite
  44         for X in `cat unit_equality_problems`; do\
  45                 cat $(TPTPDIR)/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\
  46         done
  47
  48 generate-%:
  49         for X in `cat $*`; do\
  50                 ./tptp2grafite -tptppath $(TPTPDIR) $$X.p \
  51                 > ../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \
  52         done
  53
  54 ngenerate-%:
  55         for X in `cat $*`; do\
  56                 ./tptp2grafite -ng -tptppath $(TPTPDIR) $$X.p \
  57                 > ../../matita/contribs/ng_TPTP/$$X.ma || echo Failed: $$X; \
  58         done
  59
  60 parse-%:
  61         for X in `cat $*`; do\
  62           echo "Parsing $$X"; \
  63                 ./tptp2grafite -tptppath $(TPTPDIR) $$X.p \
  64                 > /dev/null || echo Failed: $$X; \
  65         done
  66
  67 thf:
  68         rm -rf THF
  69         mkdir THF
  70         for x in `cat thf_problems`; do\
  71                 echo $$x;\
  72                 ./mainTHF -tptppath $(TPTPDIR) $$x.p > THF/$$x.ma;\
  73         done
  74
  75 include ../../Makefile.defs
  76 include ../Makefile.common
  77