initial initiave to translate bdd hol4 to cakeml

Author: AnoudAlshnakat

hol/policy_to_table/bdd_cake_trans/Holmakefile

@@ -0,0 +1,66 @@
+# includes
+# ----------------------------------
+
+CAKEMLDIR = ../../../cakeml
+
+DEPENDENCIES   = .. \
+ $(CAKEMLDIR)/misc \
+ $(CAKEMLDIR)/semantics \
+ $(CAKEMLDIR)/semantics/proofs \
+ $(CAKEMLDIR)/basis/pure \
+ $(CAKEMLDIR)/basis \
+ $(CAKEMLDIR)/translator \
+ $(CAKEMLDIR)/cv_translator \
+ $(CAKEMLDIR)/characteristic \
+ $(CAKEMLDIR)/compiler/parsing \
+ $(CAKEMLDIR)/unverified/sexpr-bootstrap
+
+
+# configuration
+# ----------------------------------
+HOLHEAP        = ../policy_to_table-heap
+NEWHOLHEAP     = bdd_cake_trans-heap
+
+HEAPINC_EXTRA  = wordsLib
+
+
+# included lines follow
+# ----------------------------------
+
+# automatic Holmake targets (all theories and non-"Script.sml" .sml files)
+# automatic heap inclusion by name pattern
+# ----------------------------------
+SMLFILES       = $(subst *.sml,,  $(patsubst %Script.sml,%Theory.sml,$(wildcard *.sml)))
+TARGETS        = $(patsubst %.sml,%.uo,$(SMLFILES))
+
+HEAPINC        = $(subst *Theory,,$(patsubst %Script.sml,%Theory    ,$(wildcard *Script.sml))) \
+                 $(subst *Syntax,,$(patsubst       %.sml,%          ,$(wildcard *Syntax.sml))) \
+                 $(subst *Simps,, $(patsubst       %.sml,%          ,$(wildcard *Simps.sml ))) \
+                 $(subst *Lib,,   $(patsubst       %.sml,%          ,$(wildcard *Lib.sml   ))) \
+                 $(HEAPINC_EXTRA)
+
+
+# general configs
+# ----------------------------------
+all: $(TARGETS) $(if $(NEWHOLHEAP),$(NEWHOLHEAP),)
+
+INCLUDES       = $(DEPENDENCIES) $(if $(HOLHEAP),$(shell dirname $(HOLHEAP)),)
+
+EXTRA_CLEANS   = $(if $(NEWHOLHEAP),$(NEWHOLHEAP) $(NEWHOLHEAP).o,) $(wildcard *.exe)
+
+OPTIONS        = QUIT_ON_FAILURE
+
+default: all
+
+.PHONY: all default
+
+
+# holheap part
+# ----------------------------------
+ifdef POLY
+
+$(NEWHOLHEAP): $(TARGETS) $(HOLHEAP)
+	$(protect $(HOLDIR)/bin/buildheap) $(if $(HOLHEAP),-b $(HOLHEAP),) -o $@ $(HEAPINC)
+
+endif
+