COQC=coqc
COQDEP=coqdep
COQTOP=coqtop

COQFLAGS=
OPT=-opt
COQINCLUDES=-R . ExtractionInCoq
COQOPTIONS=$(COQFLAGS) $(COQINCLUDES) $(OPT)

CAMLC=ocamlc -c
CAMLOPTC=ocamlopt -c
CAMLLINK=ocamlc
CAMLDEP=ocamldep
CAMLOPTLINK=ocamlopt
CAMLINCLUDES=-I bcoq -I +camlp5
CAMLP4=-pp "camlp5o pa_extend.cmo"
CAMLOPTIONS=$(CAMLINCLUDES) $(CAMLP4)


#######################################################
## Main targets

.PHONY: world all coq-world bcoq depend clean distclean

world: coq-world bcoq
all: world bcoq/bcoq.opt
bcoq: coq-world bcoq/bcoq

#######################################################
## Extraction and build of Bcoq

KERNEL=bcoq/kernel.ml bcoq/kernel.mli

BCOQFILES=bcoq/magic.cmo bcoq/kernel.cmo \
          bcoq/libkernel.cmo bcoq/term_printer.cmo \
          bcoq/lexer.cmo bcoq/parser.cmo bcoq/clflags.cmo \
          bcoq/checker.cmo
BCOQOPTFILES=$(BCOQFILES:.cmo=.cmx)

BCOQ=bcoq/bcoq.cma bcoq/launch.cmo
BCOQOPT=bcoq/bcoq.cmxa bcoq/launch.cmx

coq-world: $(KERNEL)

bcoq/bcoq: $(KERNEL) $(BCOQ)
	$(CAMLLINK) $(CAMLOPTIONS) -o $@ nums.cma gramlib.cma $(BCOQ)

bcoq/bcoq.cma: $(BCOQFILES)
	$(CAMLLINK) $(CAMLOPTIONS) -a -o $@ $(BCOQFILES)

bcoq/bcoq.opt: $(BCOQOPT)
	$(CAMLOPTLINK) $(CAMLOPTIONS) -o $@ gramlib.cmxa $(BCOQOPT)

bcoq/bcoq.cmxa: $(BCOQOPTFILES)
	$(CAMLOPTLINK) $(CAMLOPTIONS) -a -o $@ $(BCOQOPTFILES)

axioms.txt: Extraction/Extraction.vo
	coqchk -o -silent $(COQINCLUDES) ExtractionInCoq.Extraction.Extraction > $@

#########################################################
### Misc. targets
#########################################################

clean:
	find . -regex '.*\.\(vo\|cm[iox]\|cmx[as]\|glob\)$$' -delete

distclean: clean
	rm -f .depend

depend:
	rm -f .depend
	$(MAKE) .depend

.depend:
	find . -name '*.v' -print0 | xargs -0 $(COQDEP) -c $(COQINCLUDES) > $@
	find . -name '*.v' -print0 | xargs -0 $(COQDEP) -suffix .html -c $(COQINCLUDES) >> $@
	sed -i -e 's|./bcoq/kernel.vo ./bcoq/kernel.glob:|bcoq/kernel.ml bcoq/kernel.mli:|' $@
# kernel.ml{,i} are generated by extraction, create dummy ones for dependency computation
	touch bcoq/kernel.ml bcoq/kernel.mli
	$(CAMLDEP) $(CAMLOPTIONS) bcoq/*.ml bcoq/*.mli >> $@
	rm bcoq/kernel.ml bcoq/kernel.mli

include .depend

%.vo %.glob: %.v
	$(COQC) $(COQOPTIONS) $<

%.cmi: %.mli
	$(CAMLC) $(CAMLOPTIONS) $<

%.cmo: %.ml
	$(CAMLC) $(CAMLOPTIONS) -annot $<

%.cmx: %.ml
	$(CAMLOPTC) $(CAMLOPTIONS) $<

%.ml %.mli: %.v
	$(COQC) $(COQOPTIONS) $<; \
	  RV=$$?; \
	  rm -f $*.vo $*.glob; \
	  exit $$RV

bcoq/kernel.ml: Extraction/Extraction.vo
