UNAME := $(shell uname)
.DEFAULT_GOAL=all

ifndef HACL_HOME
  HACL_HOME:=$(abspath $(dir $(lastword $(MAKEFILE_LIST))))
  HACL_HOME:=$(HACL_HOME:/=)
endif

ifndef FSTAR_HOME
  FSTAR_HOME:=$(HACL_HOME)/../FStar
endif

ifndef KREMLIN_HOME
  KREMLIN_HOME:=$(HACL_HOME)/../kremlin
endif

export HACL_HOME
export FSTAR_HOME
export KREMLIN_HOME

# $(info $(HACL_HOME))
# $(info $(FSTAR_HOME))
# $(info $(KREMLIN_HOME))

ifeq ($(CI),true)
VERBOSE=
else
VERBOSE=-verbose
endif

#
# Kremlin
#

KREMLIB=$(KREMLIN_HOME)/kremlib/compat
KREMLIN=$(KREMLIN_HOME)/krml
KREMTEST=$(KREMLIN_HOME)/test


# Default Kremlin arguments
KREMLIN_ARGS?=
KREMLIN_ARGS+=$(KOPTS)
KREMLIN_ARGS+=-I $(KREMLIN_HOME)/kremlib/compat -I $(HACL_KREMLIN) -I $(KREMLIB) -I $(HACL_HOME)/specs -I .

ifneq (,$(EVEREST_WINDOWS))
KREMLIN_ARGS+=-falloca -ftail-calls
endif

# Compiler options
ifdef USE_CCOMP
  KREMLIN_ARGS+=-cc compcert $(VERBOSE)
else ifdef USE_CL
  KREMLIN_ARGS+=-cc msvc $(VERBOSE)
else
  KREMLIN_ARGS+=-ccopt -march=native $(VERBOSE) -ldopt -flto
endif

# BB. Check if this is necessary
# Release mode (includes testlib if not release)
ifdef HACL_RELEASE
  KREMLIN_TESTLIB=
else
  KREMLIN_TESTLIB=-add-include '"extracted/TestLib.h"' $(KREMLIB)/c/testlib.c
endif

# License header
ifdef HACL_LICENSE
  KREMLIN_ARGS+=-header $(HACL_LICENSE)
endif

#
# FStar
#

FSTAR_LIB=$(FSTAR_HOME)/ulib

HINTS_ENABLED?=--use_hints
FSTAR_INCLUDES+= \
	--include $(HACL_HOME)/lib \
	--include $(HACL_HOME)/specs \
	--query_stats

FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(HINTS_ENABLED) $(OTHERFLAGS) $(FSTAR_INCLUDES)

include $(FSTAR_HOME)/ulib/ml/Makefile.include

#
# OCaml
#

OCAMLOPT:=$(OCAMLOPT) -thread -package batteries,zarith,stdint -w -20-26-3-8-58

#
# Compilers and tools
#

HAS_CL=$(shell which cl.exe >/dev/null 2>&1 && echo true || echo false)
HAS_CCOMP=$(shell which ccomp >/dev/null 2>&1 && echo true || echo false)
GFIND=$(shell which gfind >/dev/null 2>&1 && echo gfind || echo find)

ifeq ($(OS),Windows_NT)
  GCC=x86_64-w64-mingw32-gcc.exe
  MSVC=cl.exe
else
  GCC=$(shell which gcc-8 >/dev/null 2>&1 && echo gcc-8 || (which gcc-7 >/dev/null 2>&1 && echo gcc-7 || echo gcc))
  CMAKE_COMPILER_OPTION := -DCMAKE_C_COMPILER=$(GCC)
  ENABLE_LTO=-flto
endif
GCC_OPTS=$(ENABLE_LTO) -std=c11 -D_GNU_SOURCE

#
# HACL* generalized targets
#

# ml-lib:
# 	$(MAKE) -C $(ULIB_ML)

# import-lib:
# 	@cp $(HACL_LIB_FILES) .

# import-kremlin:
# 	@cp $(HACL_KREMLIN_FILES)) .

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

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

%.fst-verify: %.fst
	$(FSTAR) $<

%.fsti-verify: %.fsti
	$(FSTAR) $<

%.fst-in:
	@echo --hint_info \
	$(HINTS_ENABLED) \
	$(OTHERFLAGS) \
	$(FSTAR_INCLUDES)

%.fsti-in:
	@echo --hint_info \
	$(HINTS_ENABLED) \
	$(OTHERFLAGS) \
	$(FSTAR_INCLUDES)

%.fst.hints: %.fst
	$(FSTAR) --record_hints --z3rlimit_factor 5 $<

%.fsti.hints: %.fsti
	$(FSTAR) --record_hints --z3rlimit_factor 5 $<

# Custom verification targets for re-located hint files
%.fst-reloc-verify: %.fst
	$(FSTAR) --hint_file $(subst -reloc-verify,,$(@F)).hints $<
%.fsti-reloc-verify: %.fsti
	$(FSTAR) --hint_file $(subst -reloc-verify,,$(@F)).hints $<
%.fst.reloc.hints: %.fst
	$(FSTAR) --hint_file $(subst .reloc,,$(@F)) --record_hints $<
%.fsti.reloc.hints: %.fsti
	$(FSTAR) --hint_file $(subst .reloc,,$(@F)) --record_hints $<

# Directories
%.dir-verify: %
	$(MAKE) -C $^ verify

%.dir-extract-c: %
	$(MAKE) -C $^ extract-c

%.dir-hints: %
	$(MAKE) -C $^ hints

# Colors
NORMAL="\\033[0;39m"
CYAN="\\033[1;36m"