#######################################################################
#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
# <O___,, #          PPS - Université Paris Diderot-Paris 7           #
#   \VV/  #############################################################
#    //   #      This file is distributed under the terms of the      #
#         #       GNU Lesser General Public License Version 2.1       #
#######################################################################

OCAMLC		:= ocamlc
OCAMLOPT	:= ocamlopt
OCAMLDEP	:= ocamldep

OCAMLPATH	:= $(shell $(OCAMLC) -where)
HASNATDYNLINK	:= $(if $(wildcard $(OCAMLPATH)/dynlink.cmxa),yes,)

COQROOT		:= $(shell coqtop -where)
COQMKTOP	:= coqmktop
COQC		:= coqc
COQDEP		:= coqdep

STATIC_PLUGINS	:= $(COQROOT)/plugins/quote/quote.cmo $(COQROOT)/plugins/extraction/extraction_plugin.cma
STATIC_PLUGINX	:= $(COQROOT)/plugins/quote/quote.cmx $(COQROOT)/plugins/extraction/extraction_plugin.cmxa

COQ_MLLIBS	:= \
	kernel interp lib library proofs pretyping parsing \
	tactics toplevel plugins/extraction plugins/quote

COQ_MLINCLUDES	:= $(foreach lib,$(COQ_MLLIBS), -I $(COQROOT)/$(lib))

camlp4deps	= $(shell sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*\*)@\1@p' $(1))
pp		= -pp "camlp5o $(COQ_MLINCLUDES) pa_extend.cmo $(COQROOT)/$(call camlp4deps,$<) -loc loc -impl"

MLFLAGS		:= $(COQ_MLINCLUDES) -I +camlp5 -rectypes -annot

MODULES_CMO	:= intextr_core.cmo g_intextr.cmo
MODULES_CMX	:= $(MODULES_CMO:.cmo=.cmx)

MODULES_VO	:= \
  Ml.vo MlSem.vo InternalExtraction.vo \
  Examples.vo

MODULES_CMXS	:= $(if $(HASNATDYNLINK),intextr.cmxs)

ifeq ($(VERBOSE),1)
 SHOW = @true ""
 HIDE =
else
 SHOW = @echo ""
 HIDE = @
endif


.PHONY: all

all: intextr.cma $(MODULES_CMXS) $(MODULES_VO)

coq-intextr.byte: intextr.cma
	$(SHOW)'COQMKTOP    -top -o $@'
	$(HIDE)$(COQMKTOP) -top -o $@ $(STATIC_PLUGINS) $<

coq-intextr.opt: intextr.cmxa
	$(SHOW)'COQMKTOP    -opt -o $@'
	$(HIDE)$(COQMKTOP) -opt -o $@ $(STATIC_PLUGINX) $<

intextr.cma: $(MODULES_CMO)
	$(SHOW)'OCAMLC      -a -o $@'
	$(HIDE)$(OCAMLC) -a -o $@ $^

intextr.cmxa: $(MODULES_CMX)
	$(SHOW)'OCAMLOPT    -a -o $@'
	$(HIDE)$(OCAMLOPT) -a -o $@ $^

intextr.cmxs: intextr.cmxa
	$(SHOW)'OCAMLOPT    -shared -o $@'
	$(HIDE)$(OCAMLOPT) -shared -linkall -o $@ $<

clean:
	$(SHOW)'CLEAN'
	$(HIDE)-rm -f *~ *.cm[aoix] *.cmxa *.cmxs *.vo *.glob *.annot *.o *.a \
	  coq-intextr.* .depend


# Automatic rules

%.cmo: %.ml
	$(SHOW)'OCAMLC      $<'
	$(HIDE)$(OCAMLC) $(MLFLAGS) -c $<

%.cmi: %.mli
	$(SHOW)'OCAMLC      $<'
	$(HIDE)$(OCAMLC) $(MLFLAGS) -c $<

%.cmo: %.ml4
	$(SHOW)'OCAMLC4     $<'
	$(HIDE)$(OCAMLC) $(MLFLAGS) $(pp) -c -impl $<

%.cmx: %.ml
	$(SHOW)'OCAMLOPT    $<'
	$(HIDE)$(OCAMLOPT) $(MLFLAGS) -c $<

%.cmx: %.ml4
	$(SHOW)'OCAMLOPT4   $<'
	$(HIDE)$(OCAMLOPT) $(MLFLAGS) $(pp) -c -impl $<

%.vo: %.v
	$(SHOW)'COQC        $@'
	$(HIDE)$(COQC) -q $<


# Dependencies

g_intextr.cmo: intextr_core.cmo g_intextr.ml4
g_intextr.cmx: intextr_core.cmx g_intextr.ml4

-include .depend

.depend: *.ml *.v
	$(SHOW)'DEPEND'
	$(HIDE)-rm -f .depend
	$(HIDE)$(OCAMLDEP) *.ml > .depend
	$(HIDE)$(COQDEP) -I $(COQROOT) -I . *.v >> .depend
