Makefile.benchmark.coq.local

# Workaround for the issue that building the benchmark programs require two
# versions of OCaml.
OCAML_OPAMSWITCH?=
ifeq (,$(OCAML_OPAMSWITCH))
DUNE?= dune
else
DUNE?= opam exec --switch $(OCAML_OPAMSWITCH) -- dune
endif

HSDIR := benchmark/haskell
MLDIR := benchmark/ocaml

EXTRACTED_HS_FILES := \
  $(HSDIR)/MergesortCoqCbn.hs \
  $(HSDIR)/MergesortCoqCbnAcc.hs \
  $(HSDIR)/MergesortCoqCbv.hs \
  $(HSDIR)/MergesortCoqCbvAcc.hs

HS_FLAGS := -with-rtsopts="-T -I0 -A8G -G1 -m1" -O2

EXTRACTED_ML_FILES := \
  $(MLDIR)/mergesort_coq_cbn.ml \
  $(MLDIR)/mergesort_coq_cbnacc.ml \
  $(MLDIR)/mergesort_coq_cbv.ml \
  $(MLDIR)/mergesort_coq_cbvacc.ml \
  $(MLDIR)/mergesort_coq_cbn_tmc.ml \
  $(MLDIR)/mergesort_coq_cbnacc_tmc.ml

EXTRACTED_BINARIES := \
  $(HSDIR)/Benchmark $(HSDIR)/BenchmarkExp \
  $(MLDIR)/benchmark $(MLDIR)/benchmark_exp

$(HSDIR)/Benchmark: $(HSDIR)/Benchmark.hs $(HSDIR)/Benchlib.hs \
                    $(EXTRACTED_HS_FILES)
	cd $(HSDIR) && stack ghc Benchmark.hs -- $(HS_FLAGS)

$(HSDIR)/BenchmarkExp: $(HSDIR)/BenchmarkExp.hs $(HSDIR)/Benchlib.hs \
                       $(EXTRACTED_HS_FILES)
	cd $(HSDIR) && stack ghc BenchmarkExp.hs -- $(HS_FLAGS)

$(MLDIR)/benchmark: $(MLDIR)/benchmark.ml $(MLDIR)/benchlib.ml \
                        $(EXTRACTED_ML_FILES) $(EXTRACTED_ML_FILES:.ml=.mli)
	cd $(MLDIR) && \
	  $(DUNE) build benchmark.exe && \
	  ln -s _build/default/benchmark.exe benchmark

$(MLDIR)/benchmark_exp: $(MLDIR)/benchmark_exp.ml $(MLDIR)/benchlib.ml \
                        $(EXTRACTED_ML_FILES) $(EXTRACTED_ML_FILES:.ml=.mli)
	cd $(MLDIR) && \
	  $(DUNE) build benchmark_exp.exe && \
	  ln -s _build/default/benchmark_exp.exe benchmark_exp

$(HSDIR)/MergesortCoqCbn.hs $(MLDIR)/mergesort_coq_cbn.ml: \
    benchmark/extraction_cbn.vo

$(HSDIR)/MergesortCoqCbnAcc.hs $(MLDIR)/mergesort_coq_cbnacc.ml: \
    benchmark/extraction_cbnacc.vo

$(HSDIR)/MergesortCoqCbv.hs $(MLDIR)/mergesort_coq_cbv.ml: \
    benchmark/extraction_cbv.vo

$(HSDIR)/MergesortCoqCbvAcc.hs $(MLDIR)/mergesort_coq_cbvacc.ml: \
    benchmark/extraction_cbvacc.vo

$(MLDIR)/%_tmc.ml: $(MLDIR)/%.ml $(MLDIR)/%_tmc.patch
	patch $^ -o $@

$(MLDIR)/%_tmc.mli: $(MLDIR)/%.mli
	cp $< $@

post-all:: $(EXTRACTED_BINARIES)

clean::
	$(HIDE)rm -f $(EXTRACTED_HS_FILES)
	$(HIDE)rm -f $(HS_FILES:.hs=.hi)
	$(HIDE)rm -f $(HS_FILES:.hs=.o)
	$(HIDE)rm -f $(EXTRACTED_ML_FILES)
	$(HIDE)rm -f $(EXTRACTED_ML_FILES:.ml=.mli)
	$(HIDE)rm -f $(EXTRACTED_BINARIES)