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

ifeq (,$(filter %-in,$(MAKECMDGOALS)))
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
endif

HACL_HOME ?= .

OUTPUT_DIR=$(HACL_HOME)/obj

CFLAGS += -DHACL_CAN_COMPILE_INTRINSICS -DHACL_CAN_COMPILE_VALE -DHACL_CAN_COMPILE_INLINE_ASM -DHACL_CAN_COMPILE_VEC128 -DHACL_CAN_COMPILE_VEC256

# 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.
ifeq (,$(filter %-in,$(MAKECMDGOALS)))
ifndef NODEPEND
ifndef MAKE_RESTARTS
.depend: .FORCE
	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \
	    --extract 'Kremlin:*' \
	    --extract 'OCaml:-* +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
endif

%.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 -I$(KREMLIN_HOME)/kremlib/dist/minimal

%.exe:
	$(CC) $^ -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