generated_ml=datatypes.ml peano.ml binPos.ml binNat.ml binInt.ml \
	specif.ml sumbool.ml zArith_dec.ml genericTactics.ml \
	compare_dec.ml words.ml balancedWords.ml other.ml exo_induc_fct.ml \
	wordsContinuity.ml exo_inter.ml

generated_mli=$(generated_ml:.ml=.mli)

mlsrc=$(generated_ml) $(generated_mli) main.mli main.ml

cmos=$(generated_ml:.ml=.cmo) main.cmo
cma=bibal.cma

cmx=$(cmos:.cmo=.cmx)
cmxa=bibal.cmxa

default: prog

include ../Makefile.gplot

copy: alltarg
	echo "copie interdite, donnees en dur"
#	cp -a $(ALLTARG) ../types06

#

.PHONY: extract bib depend clean datclean 

.SUFFIXES: .ml .mli .mlo .cmi .cmo .cmx .cma .cmxa

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

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

%.cmx: %.cmi %.ml
	ocamlopt -c $*.ml

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

# extracted code to run

$(generated_ml) $(generated_mli): extraction.v
	coqc -I .. $<

extraction.v:
	cp -a ../$@ .

main.ml:
	cp -a ../$@ .

main.mli:
	touch $@

extract: $(generated_ml) $(generated_mli)

$(cma): $(generated_ml:.ml=.cmo)
	ocamlc -g -a $(generated_ml:.ml=.cmo) -o $@

$(cmxa): $(generated_ml:.ml=.cmx)
	ocamlopt -a $(generated_ml:.ml=.cmx) -o $@

bib: $(cma) $(cmxa)

prog.byte: ml.depend ${cmos}
	ocamlc -g -o $@ unix.cma ${cmos}

prog: ml.depend ${cmx}
	ocamlopt -o $@ unix.cmxa ${cmx}

# performance of extracted code

# quick

resultivt.dat: prog
	./$< ivt 100 400 15 5 $@ | tee $@

resultind.dat: prog
	./$< ind 100 13000 15 20 $@ | tee $@

resultindB1.dat: prog
	./$< ind1 100 27000 15 20 $@ | tee $@

resultdirect.dat: prog
	./$< direct 100 13000 15 1000 $@ | tee $@

# precise (and long)

resultivt+.dat: prog
	./$< ivt 100 1000 15 30 $@ | tee $@

resultind+.dat: prog
	./$< ind 100 25000 15 200 $@ | tee $@

resultdirect+.dat: prog
	./$< direct 100 25000 15 200 $@ | tee $@

# long (not very precise)
resultivtlong.dat: prog
	./$< ivt 100 4000 15 1 $@ | tee $@

# comparisons ivt / ind and ind / direct

resultcompb1.dat: prog
	./$< indvt1 15 100 15 500 $@ | tee $@

resultcompb1+.dat: prog
	./$< indvt1 100 700 15 500 $@ | tee $@

resultcompb2.dat: prog
	./$< indvt2 15 100 15 500 $@ | tee $@

resultcompb2+.dat: prog
	./$< indvt2 100 700 15 500 $@ | tee $@

resultcompdirect.dat: prog
	./$< directind 100 5000 15 1000 $@ | tee $@

# extreme cases

resultindabm1.dat: prog
	./$< indabm1 100 2000 15 100 $@ | tee $@

resultindabm2.dat: prog
	./$< indabm2 100 2000 15 100 $@ | tee $@

resultdirectabm.dat: prog
	./$< directabm 100 3000 15 4000 $@ | tee $@

resultivtabm2.dat: prog
	./$< ivtabm2 100 350 15 100 $@ | tee $@

resultivtindanbn2.dat: prog
	./$< ivtindanbn2 100 350 15 100 $@ | tee $@

# dependencies

depend: ml.depend

ml.depend: $(mlsrc)
	ocamldep *.ml *.mli > ml.depend

# dependency graphs
# http://www-verimag.imag.fr/~monin/Soft/Dependot/

graph: ml.depend.ps 

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

# cleaning 

clean:
	rm -f *~ *.depend.ps .depend
	rm -f prog prog.byte
	rm -f ${generated_ml:.ml.cmo}
	rm -f ${generated_ml:.ml.cmi}
	rm -f $(mlsrc) logic.ml* ml.depend
	rm -f *.fmt *.logfmt resu*.ps

datclean: clean
	rm -f *.dat

sinclude ml.depend