# Compilation of ocaml sources
#  Sources in the current directory are generated from Coq (they must be extracted before to run this makefile !)
#  Manually written sources are in subdirectories "$(MLsrc)" or in "$(VPL)/lib"
#  NB: all necessary sources are listed below through lsmli.sh

MLOPT:= # -g # to debug
VPL:=../../../vpl
MLsrc:=..
.PHONY: info clean all allclean

vpath %.mli $(MLsrc) $(VPL)/lib $(VPL)/lin
vpath %.ml $(MLsrc) $(VPL)/lib $(VPL)/lin
vpath %.cmx $(MLsrc) $(VPL)/lib $(VPL)/lin
vpath %.cmi $(MLsrc) $(VPL)/lib $(VPL)/lin

GENSOURCES := $(shell ./lsmli.sh)
CMX := $(addsuffix .cmx, $(GENSOURCES))
SD := $(addsuffix .d, $(GENSOURCES))
SDI := $(addsuffix .di, $(GENSOURCES))

INCL := -I . -I $(MLsrc) -I $(VPL)/lin -I $(VPL)/lib 

-include $(SD) $(SDI)

%.di: %.mli
	./myocamldep.sh $(INCL) $< > $@

%.d: %.ml
	./myocamldep.sh $(INCL) $< > $@

all: main
	./main
#	ocamlrun -b ./main # in order to debug

msort: 
	$(MAKE) -C $(VPL)/obj/msort/

main_mlist: Makefile $(SD) $(SDI) msort
	$(VPL)/obj/msort/msort $(CMX) > $@

main: $(MLsrc)/main.ml main_mlist $(CMX)
	ocamlfind ocamlopt $(MLOPT) -linkpkg -package zarith $(INCL) $$(cat main_mlist) $(MLsrc)/main.ml -o main

ImpureConfig.mli: ImpureConfig.ml Impure.cmi CoqPr.cmi CoqPr.di CoqPr.d Impure.d Impure.di
	ocamlfind ocamlopt $(MLOPT) -package zarith $(INCL) -i ImpureConfig.ml > ImpureConfig.mli || rm ImpureConfig.mli 

%.cmi: %.mli 
	ocamlfind ocamlopt $(MLOPT) -package zarith $(INCL) -c $< -o  $(notdir $@) 

%.cmx: %.ml %.cmi
	ocamlfind ocamlopt $(MLOPT) -package zarith $(INCL) -c $< -o  $(notdir $@)

info:
	@echo "SD:=" $(SD)
	@echo "SDI:=" $(SDI)

clean:
	$(RM) -f $(SD) $(SDI) *.cmi *.cmx main main_mlist *~ ../main.cm* 

allclean: clean
	$(RM) -f *.ml *.mli ../DemoExtract.vo

