# A shared set of local definitions for local Makefiles. See curve25519/Makefile
# for comments.

HACL_HOME ?= .

OUTPUT_DIR=$(HACL_HOME)/obj

# This uses the definition of ALL_HACL_DIRS, and transitively includes
# Makefile.include
include $(HACL_HOME)/Makefile.common

# All the files in the current directory ought to be verified.
FSTAR_ROOTS?=$(wildcard *.fst *.fsti)

# This is the right way to ensure the .depend file always gets re-built.
ifndef NODEPEND
ifndef MAKE_RESTARTS
.depend: .FORCE
	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \
	    --extract '-* +FStar.Kremlin.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \
	    > $@

.PHONY: .FORCE
.FORCE:
endif
endif

include .depend

%.checked: FSTAR_FLAGS=
$(OUTPUT_DIR)/Vale.%.checked: FSTAR_FLAGS=$(VALE_FSTAR_FLAGS)

# Producing .checked and .krml.
%.checked:
	$(FSTAR) $(FSTAR_FLAGS) $< --hint_file $(HACL_HOME)/hints/$(notdir $*).hints && \
	  touch -c $@

%.krml:
	$(FSTAR) --codegen Kremlin \
	    --extract_module $(basename $(notdir $(subst .checked,,$<))) \
	    $(notdir $(subst .checked,,$<))

CODEGEN=OCaml

%.ml:
	$(FSTAR) --codegen $(CODEGEN) \
	    --extract_module $(basename $(notdir $(subst .checked,,$<))) \
	    $(notdir $(subst .checked,,$<))

%.cmx: %.ml
	$(OCAMLOPT) -c $< -o $@

# Useful definitions for C compilation

CFLAGS += -Idist -I$(KREMLIN_HOME)/include

KREMLIB_A=$(KREMLIN_HOME)/kremlib/dist/minimal/libkremlib.a

%.exe:
	$(CC) $^ $(KREMLIB_A) -o $@

# Tactic; sadly not shareable because obj vs. $(HACL_HOME)/obj

$(HACL_HOME)/obj/Meta_Interface.ml: CODEGEN = Plugin
$(HACL_HOME)/obj/Meta_Interface.ml: $(HACL_HOME)/obj/Meta.Interface.fst.checked

$(HACL_HOME)/obj/Hacl.Meta.%.checked: FSTAR_FLAGS += --load Meta.Interface
ifneq (,$(wildcard Hacl.Meta.*.fst))
$(patsubst %,$(HACL_HOME)/obj/%.checked,$(wildcard Hacl.Meta.*.fst)): $(HACL_HOME)/obj/Meta_Interface.ml
endif