Makefile.include

ifeq (,$(FSTAR_HOME))
  $(error FSTAR_HOME is not defined)
endif

ifeq (,$(STEEL_HOME))
  $(error STEEL_HOME is not defined)
endif

ifeq (,$(KRML_HOME))
  $(error KRML_HOME is not defined)
endif

ifndef FSTAR_ULIB
  FSTAR_ULIB := $(shell if test -d "$(FSTAR_HOME)/ulib" ; then echo "$(FSTAR_HOME)/ulib" ; else echo "$(FSTAR_HOME)/lib/fstar" ; fi)
endif

ifndef STEEL_LIB
  STEEL_LIB := $(shell if test -f "$(FSTAR_HOME)/ulib/experimental/Steel.Effect.fsti" ; then echo "$(FSTAR_HOME)/ulib/experimental" ; else echo "$(STEEL_HOME)/lib/steel" ; fi)
endif

ifndef KRML_LIB
  KRML_LIB := $(shell if test -d "$(KRML_HOME)/krmllib" ; then echo "$(KRML_HOME)/krmllib" ; else echo "$(KRML_HOME)/lib/krml" ; fi)
endif

PROJECT_HOME ?= .

# Prettifying output, except if we are in verbose mode
Q?=@
SIL?=--silent
ifneq ($(V),)
	Q=
	SIL=
endif

SOURCE_DIRS = \
  $(PROJECT_HOME)/lib_avl_common \
  $(PROJECT_HOME)/lib_avl_mono \
  $(PROJECT_HOME)/lib_bitmap \
  $(PROJECT_HOME)/lib_list \
  $(PROJECT_HOME)/lib_misc \
  $(PROJECT_HOME)/src

  #$(PROJECT_HOME)/lib_avl \

INCLUDE_DIRS = \
  $(SOURCE_DIRS) \
  $(FSTAR_ULIB)/.cache \
  $(STEEL_LIB)

FSTAR_EMACS_PARAMS = $(addprefix --include ,$(INCLUDE_DIRS)) \
  --load_cmxs steel \
  --compat_pre_typed_indexed_effects

%.fst-in %.fsti-in:
	@echo $(FSTAR_EMACS_PARAMS)