# Ensure LEM_DIR is set before running Holmake, e.g., by using the accompanying Makefile

LEM_SCRIPTS = sail2_instr_kindsScript.sml sail2_valuesScript.sml sail2_operatorsScript.sml \
  sail2_operators_mwordsScript.sml sail2_operators_bitlistsScript.sml \
  sail2_state_monadScript.sml sail2_stateScript.sml sail2_promptScript.sml sail2_prompt_monadScript.sml \
  sail2_undefinedScript.sml sail2_stringScript.sml sail2_concurrency_interfaceScript.sml \
  sail2_concurrency_interface_mwordsScript.sml sail2_concurrency_interface_bitlistsScript.sml \
  sail2_undefined_concurrency_interfaceScript.sml sail2_monadic_combinatorsScript.sml

LEM_CLEANS = $(LEM_SCRIPTS)

SCRIPTS = $(LEM_SCRIPTS) \
  sail2_valuesAuxiliaryScript.sml sail2_stateAuxiliaryScript.sml

THYS = $(patsubst %Script.sml,%Theory.uo,$(SCRIPTS))

INCLUDES = $(LEM_DIR)/hol-lib

all: $(THYS)
.PHONY: all

ifdef POLY
HOLHEAP = sail-heap
EXTRA_CLEANS = $(LEM_CLEANS) $(HOLHEAP) $(HOLHEAP).o

BASE_HEAP = $(LEM_DIR)/hol-lib/lemheap

# The command to build heaps has changed after Trindemossen-2 release, so allow
# both for now, and we can drop the first after the next HOL release.
$(HOLHEAP): $(BASE_HEAP)
	if type $(protect $(HOLDIR)/bin/buildheap) >/dev/null 2>/dev/null; then \
	  $(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) -b $(BASE_HEAP); else \
	  $(protect $(HOLDIR)/bin/hol) buildheap -o $(HOLHEAP) -b $(BASE_HEAP); fi

all: $(HOLHEAP)

else

EXTRA_CLEANS = $(LEM_CLEANS)

endif
