coqsrc=$(wildcard *.v)

TARGEXTRACT= exo_induc_fct.vo exo_inter.vo
TARGETS= Correctness.vo $(TARGEXTRACT) bib prog


default: ${TARGETS}

prepare_bench: Correctness.vo

.PHONY: depend clean allclean bib prog perf long precise comp comprecise

.SUFFIXES: .tex .ps .pdf .dvi .v .vo

%.vo: %.v
	time coqc $*.v

%.cmo: %.cmi %.ml
	ocamlc -g -c $*.ml

%.cmi: %.mli
	ocamlc -g -c $*.mli

# dependencies

depend: coq.depend

coq.depend: $(coqsrc) 
	coqdep *.v > coq.depend

$(TARGEXTRACT): coq.depend 

# dependency graphs

graph: coq.depend.ps

%.depend.ps: %.depend
	cat $< | dependot | dot -Tps > $@

# Performance of extracted code

prog_ready: $(TARGEXTRACT) Makefile.perf main.ml
	mkdir -p Perf
	cp -a main.ml analysis.ml Perf
	cp -a Makefile.perf Perf/Makefile
	(cd Perf; make depend)
	touch $@

bib: prog_ready
	(cd Perf; make bib)

prog: prog_ready
	(cd Perf; make prog)

perf: prog_ready
	(cd Perf; make)

long: prog_ready
	(cd Perf; make long)

precise: prog_ready
	(cd Perf; make precise)

comp: prog_ready
	(cd Perf; make comp)

longcomp: prog_ready
	(cd Perf; make longcomp)

copy: prog_ready
	(cd Perf; make copy)


# cleaning 

clean:
	rm -f *.vo *~ *.sv *.depend.ps .depend
	rm -f prog
	rm -rf Perf prog_ready
	rm -rf result*

allclean: clean
	rm -f *.depend

sinclude coq.depend