FILES := magic.ml kernel.ml datatypes.ml main.ml4
CMOS := $(patsubst %.ml,%.cmo,$(FILES:.ml4=.ml))
CMXS := $(CMOS:.cmo=.cmx)
FILES += $(wildcard $(FILES:.ml=.mli))

.PHONY: all clean

all: xcoq.cmo xcoq.cmxs

kernel.ml:
	cp ../bcoq/kernel.ml $@

clean:
	rm -f Makefile.coq kernel.ml *.stamp *.cm* *.d *.o *.annot

Makefile.coq:
	coq_makefile $(FILES) -o $@

xcoq.cmo: xcoq.cmi inner.byte.stamp
	ocamlc -pack -rectypes -o $@ $(CMOS)

xcoq.cmx: xcoq.cmi inner.opt.stamp
	ocamlopt -pack -rectypes -o $@ $(CMXS)

%.cmi: %.mli
	ocamlc -c $<

%.cmxs: %.cmx
	ocamlopt -shared -o $@ $<

inner.byte.stamp: Makefile.coq $(FILES)
	$(MAKE) -f Makefile.coq ZDEBUG="-annot -rectypes -for-pack Xcoq" $(CMOS)
	touch $@

inner.opt.stamp: Makefile.coq $(FILES)
	$(MAKE) -f Makefile.coq ZDEBUG="-annot -rectypes -for-pack Xcoq" $(CMXS)
	touch $@
