PACKAGE = paramodulation
-REQUIRES = \
- helm-registry \
- helm-cic_transformations \
- helm-tactics \
- helm-cic_disambiguation \
- mysql
-
INTERFACE_FILES = \
utils.mli \
- inference.mli
+ inference.mli\
+ equality_indexing.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) \
- trie.ml \
- path_indexing.ml \
- discrimination_tree.ml \
indexing.ml \
saturation.ml
-# saturate_main.ml
-# test_indexing.ml
-
-
-include ../helm/ocaml/Makefile.common
-
+include ../Makefile.common
paramodulation.cmo: $(IMPLEMENTATION_FILES:%.ml=%.cmo)
$(OCAMLC) -pack -o $@ $(IMPLEMENTATION_FILES:%.ml=%.cmo)
$(OCAMLOPT) $(OCAMLARCHIVEOPTIONS) -a -o $@ \
paramodulation.cmx
-PARAMOD_OBJS = $(IMPLEMENTATION_FILES:%.ml=%.cmo) \
- saturate_main.cmo
-PARAMOD_OBJS_OPT = $(IMPLEMENTATION_FILES:%.ml=%.cmx) \
- saturate_main.cmx
-
-saturate: $(PARAMOD_OBJS) $(LIBRARIES)
- $(OCAMLC) -thread -linkpkg -o $@ $(PARAMOD_OBJS)
+PARAMOD_OBJS = $(IMPLEMENTATION_FILES:%.ml=%.cmo)
+PARAMOD_OBJS_OPT = $(IMPLEMENTATION_FILES:%.ml=%.cmx)
-saturate.opt: $(PARAMOD_OBJS_OPT) $(LIBRARIES)
- $(OCAMLOPT) -thread -linkpkg -o $@ $(PARAMOD_OBJS_OPT)
+LOCALLINKOPTS = -package helm-cic_disambiguation,helm-content_pres,helm-grafite,helm-grafite_parser
+saturate: saturate_main.ml $(PARAMOD_OBJS) $(LIBRARIES)
+ $(OCAMLC) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $(PARAMOD_OBJS) $<
+saturate.opt: saturate_main.ml $(PARAMOD_OBJS_OPT) $(LIBRARIES)
+ $(OCAMLOPT) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $(PARAMOD_OBJS_OPT) $<