include ../../Makefile.common

ifeq (3.81,$(MAKE_VERSION))
  $(error You seem to be using the OSX antiquated Make version. Hint: brew \
    install make, then invoke gmake instead of make)
endif

FSTAR_EXE ?= fstar.exe

TEST_OPTS	= -warn-error @4 -verbose -skip-makefiles
KRML_BIN	= ../../_build/default/src/Karamel.exe
KRML		= $(KRML_BIN) -fstar $(FSTAR_EXE) $(KOPTS) $(TEST_OPTS)
CACHE_DIR	= .cache
FSTAR		= $(FSTAR_EXE) --cache_checked_modules \
  --cache_dir $(CACHE_DIR) \
  --include ../../krmllib/compat --include ../../krmllib/obj \
  --include ../../krmllib --include ../../runtime \
  --ext optimize_let_vc \
  --already_cached 'Prims FStar C TestLib Spec.Loops -C.Compat -C.Nullity LowStar WasmSupport' \
  --trivial_pre_for_unannotated_effectful_fns false \
  --cmi --warn_error -274
SED=$(shell which gsed >/dev/null 2>&1 && echo gsed || echo sed)

all: derived.rust-test

FSTAR_FILES=$(wildcard *.fst *.fsti)

.PRECIOUS: %.krml

# Use F*'s dependency mechanism and fill out the missing rules.

ifndef MAKE_RESTARTS
ifndef NODEPEND
.depend: .FORCE
	$(FSTAR) --dep full $(FSTAR_FILES) --extract 'krml:*,-Prims' --output_deps_to $@

.PHONY: .FORCE
.FORCE:
endif
endif

include .depend

$(CACHE_DIR)/%.checked: | .depend
	$(call run-with-log,$(FSTAR) $(OTHERFLAGS) $< && touch $@,[RUST_PROPERERASURE_BUNDLE_VERIFY] $*,$(CACHE_DIR)/$*)

%.krml: | .depend
	$(call run-with-log,$(FSTAR) $(OTHERFLAGS) --codegen krml \
	  --extract_module $(basename $(notdir $(subst .checked,,$<))) \
	  $(notdir $(subst .checked,,$<))\
	  ,[RUST_PROPERERASURE_BUNDLE_EXTRACT_KRML] $(basename $*),$*)

########
# Rust #
########

.PRECIOUS: %.rs
derived.rs: $(ALL_KRML_FILES) $(KRML_BIN)
	$(KRML) -minimal -bundle 'FStar.*,LowStar.*,C,C.*,Prims' -bundle 'Base+Caller=Derived[rename=Derived]' \
	  -backend rust $(EXTRA) -tmpdir $(dir $@) $(filter %.krml,$^)
	$(SED) -i 's/\(patterns..\)/\1\nmod lowstar { pub mod ignore { pub fn ignore<T>(_x: T) {}}}\n/' $@
	echo 'fn main () { let r = main_ (); if r != 0 { println!("main_ returned: {}\\n", r); panic!() } }' >> $@

%.rust-test: %.rs
	rustc $< -o $*.exe && ./$*.exe

clean:
	rm -rf .cache .depend *.krml *.rs *.exe *.output *.err *.cmd *.time

.PHONY: all clean
