Added example programs to retrofit semantics

Author: didriklundberg

hol/retrofit_sem/programs/Holmakefile

@@ -0,0 +1,63 @@
+# includes
+# ----------------------------------
+
+CAKEMLDIR = ../../../cakeml
+
+DEPENDENCIES   = .. \
+ $(CAKEMLDIR)/misc \
+ $(CAKEMLDIR)/semantics \
+ $(CAKEMLDIR)/semantics/proofs \
+ $(CAKEMLDIR)/basis/pure \
+ $(CAKEMLDIR)/basis \
+ $(CAKEMLDIR)/translator \
+ $(CAKEMLDIR)/characteristic \
+ $(CAKEMLDIR)/compiler/parsing \
+ $(CAKEMLDIR)/unverified/sexpr-bootstrap
+
+# configuration
+# ----------------------------------
+HOLHEAP        = ../retrofit_sem-heap
+#NEWHOLHEAP     = 
+
+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

hol/retrofit_sem/programs/build_cake.sh

@@ -0,0 +1,19 @@
+#!/bin/bash
+
+if [ $# -ne 1 ]; then
+    echo "Usage: $0 <program_name>"
+    echo "Example: $0 port_swap"
+    exit 1
+fi
+
+PROGRAM_NAME=$1
+
+Holmake ${PROGRAM_NAME}Theory
+
+cp ${PROGRAM_NAME}.sexp compilation/
+
+cd compilation
+
+./compile_cake.sh ${PROGRAM_NAME}
+
+cd ..

hol/retrofit_sem/programs/compilation/compile_cake.sh

@@ -0,0 +1,15 @@
+#!/bin/bash
+
+progname=$1
+
+if [ -z $1 ]; then
+  echo "Usage: supply the name of the CakeML sexp file without the .sexp suffix as a command-line argument"
+  exit 0
+fi
+
+# NOTE: Always set skip_type_inference to false if you don't know what you're doing when in-lining CakeML code.
+CML_STACK_SIZE=1000 CML_HEAP_SIZE=6000 ./cake --sexp=true --exclude_prelude=true --gc=gen50000 --skip_type_inference=false --emit_empty_ffi=true --reg_alg=0 < $progname.sexp > $progname.cake.S
+#Old version:
+#CML_STACK_SIZE=1000 CML_HEAP_SIZE=6000 ./cake --sexp=true --exclude_prelude=true --skip_type_inference=false --emit_empty_ffi=true --reg_alg=0 < $progname.sexp > $progname.cake.S
+
+cc ${progname}.cake.S basis_ffi.c -lm -o ${progname}.cake