HACL_HOME 	?= ..
KREMLIN_HOME 	?= ../../kremlin
FSTAR_HOME 	?= ../../FStar
MLCRYPTO_HOME   ?= ../../MLCrypto
MITLS_HOME      ?= ../../mitls-fstar
CONCRETE_DIR	= $(HACL_HOME)/secure_api/concrete_specializations
IMPL_CHOICE	?= runtime_switch
DIST_DIR	= $(HACL_HOME)/secure_api/out/$(IMPL_CHOICE)
OUTPUT_DIR	= $(DIST_DIR)/extracted
CACHE_DIR       = $(DIST_DIR)/cache
CORECRYPTO_DIR	= $(FSTAR_HOME)/contrib/CoreCrypto/fst

# Pseudo autoconfiguration
UNAME		= $(shell uname)
SED		= $(shell which gsed >/dev/null 2>&1 && echo gsed || echo sed)
MARCH		= x86_64
ifeq ($(UNAME),Darwin)
  VARIANT=-Darwin
  DYLD_LIBRARY_PATH := $(DIST_DIR):$(DYLD_LIBRARY_PATH)
  SO = so
  QUICPROVIDER_SO_LDOPTS =
  export DYLD_LIBRARY_PATH
else ifeq ($(UNAME),Linux)
  CCOPTS_EXTRA=-fPIC
  VARIANT=-Linux
  LD_LIBRARY_PATH := $(DIST_DIR):$(LD_LIBRARY_PATH)
  SO = so
  QUICPROVIDER_SO_LDOPTS = -Xlinker -z -Xlinker noexecstack -Xlinker --version-script -Xlinker $(HACL_HOME)/secure_api/libquicprovider_version_script
  export LD_LIBRARY_PATH
else ifeq ($(OS),Windows_NT)
  CC=$(MARCH)-w64-mingw32-gcc
  AR=$(MARCH)-w64-mingw32-ar
  PATH := $(DIST_DIR):$(PATH)
  SO = dll
  QUICPROVIDER_SO_LDOPTS =
  export PATH
endif
CCOPTS=-Wall -Wextra $(CFLAGS) -I $(KREMLIN_HOME)/include $(CCOPTS_EXTRA)

# -Werror --not yet feasible because of FStar_Char_char_of_int in kremstr.h
# The include paths, including the implementation choice.
INCLUDE_PATHS=$(addprefix --include , \
	$(HACL_HOME)/specs \
	$(HACL_HOME)/code/bignum \
	$(HACL_HOME)/code/experimental/aesgcm \
	$(HACL_HOME)/code/lib/kremlin \
	$(HACL_HOME)/code/poly1305 \
	$(HACL_HOME)/code/hash \
	$(HACL_HOME)/code/salsa-family \
	$(KREMLIN_HOME)/kremlib \
	$(HACL_HOME)/secure_api \
	$(HACL_HOME)/secure_api/aead \
	$(HACL_HOME)/secure_api/prf \
	$(HACL_HOME)/secure_api/hkdf \
	$(HACL_HOME)/secure_api/vale \
	$(HACL_HOME)/secure_api/uf1cma \
	$(HACL_HOME)/secure_api/utils \
	$(HACL_HOME)/secure_api/LowCProvider/fst \
	$(CORECRYPTO_DIR) \
	$(CONCRETE_DIR) \
	$(CONCRETE_DIR)/$(IMPL_CHOICE) \
	$(HACL_HOME)/secure_api/test)

FSTAR_FLAGS=$(OTHERFLAGS) \
        --cache_dir $(CACHE_DIR) \
        --cache_checked_modules \
        $(INCLUDE_PATHS) \
        --odir $(OUTPUT_DIR) \
        --use_hints

# The F* compiler and the entry points.
FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS)

%.fst-ver: %.fst
	$(FSTAR) $^

%.fst-lax: %.fst
	$(FSTAR) $^ --lax

%.fsti-in:
	@echo $(FSTAR_FLAGS)

%.fst-in:
	@echo $(FSTAR_FLAGS)