COQROOT=/opt/coq

# set to false to use extract/kernel.ml0 instead of compiling the Coq files
# and extract...
COMPILCOQ=true

COQBIN=$(COQROOT)/bin
COQC=$(COQBIN)/coqc
COQDEP=$(COQBIN)/coqdep
COQ2HTML=$(COQBIN)/coq2html

COQFLAGS=
OPT=-opt
COQINCLUDES=-I . -I lib -I ptsmeta -I cci
COQOPTIONS=$(COQFLAGS) $(COQINCLUDES) $(OPT)

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

LIBV=$(shell ls lib/*.v)
LIBVO=$(LIBV:.v=.vo)
VO=GenericSort.vo SortV6.vo
PTSVO=ptsmeta/Mmain.vo ptsmeta/Mtermes.vo ptsmeta/McocSyntax.vo \
      ptsmeta/Menv.vo ptsmeta/MPTS_spec.vo ptsmeta/Mtyping.vo \
      ptsmeta/Mrules.vo ptsmeta/Mctxt.vo ptsmeta/Mconfluence.vo \
      ptsmeta/Mnormal.vo ptsmeta/Morder.vo \
      ptsmeta/MparCtxt.vo ptsmeta/Msoundness.vo
CCIINTERVO_HIDE=cci/Mequal.vo cci/MinvReduction.vo cci/MinvEqual.vo \
           cci/MequalDec.vo cci/Msubtyping.vo cci/MinvSubtyping.vo \
           cci/MsubtypingDec.vo cci/McciPts.vo cci/McciMeta.vo \
           cci/MsubjRed.vo cci/MsignCorrectness.vo cci/McoreDec.vo \
           cci/MfixDec.vo cci/MindDec.vo cci/McaseDec.vo cci/MsignDec.vo
CCIVO=cci/McciSyntax.vo cci/Mvect.vo cci/MtypCtxt.vo cci/Mmarks.vo \
      cci/Mrecords.vo cci/Msignature.vo cci/MlambdaRules.vo \
      cci/Mcumulativity.vo cci/MtypCase.vo cci/MtypFix.vo \
      $(CCIINTERVO) cci/Msign.vo cci/MinclSign.vo \
      cci/MwfSign.vo cci/MsignCheck.vo cci/Mkernel.vo
OBJS=$(LIBVO) $(VO) $(PTSVO) $(CCIVO)

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

world:: all
all:: coq-world bcoq

coq-world:: $(OBJS)

bcoq:: extract/bcoq

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

KERNELDEPS=cci/Mkernel.vo Extraction.vo lib/MlExtract.v \
           cci/ErrorStrings.v extract/Extract.v

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

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

extract/kernel.ml: $(KERNELDEPS)
	if $(COMPILCOQ); then \
	  $(COQC) $(COQOPTIONS) extract/Extract; \
	  mv kernel.ml* extract/; \
	  cp -f extract/kernel.ml extract/kernel.ml0; \
	else \
	  cp -f extract/kernel.ml0 extract/kernel.ml; \
	fi
extract/kernel.cmo: extract/kernel.ml extract/kernel.cmi
extract/kernel.cmi: extract/kernel.mli

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

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

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

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

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

clean::
	rm -f *.cm* *.vo */*.vo

depend::
	/bin/rm .depend
	$(COQDEP) -c $(COQINCLUDES) *.v */*.v > .depend
	$(COQDEP) -suffix .html $(COQINCLUDES) *.v */*.v >> .depend

include .depend

.SUFFIXES: .v .vo .html .ml .mli .cmo .cmi .cmx

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

.v.html:
	$(COQ2HTML) $(COQINCLUDES) $<

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

.ml.cmo:
	$(CAMLC) $(CAMLOPTIONS) $<

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