Scheme

compiler/README.md

@@ -42,3 +42,6 @@ Correctness proof for the CakeML compiler.
 [repl](repl):
 Some definitions and proofs used in the proof of the CakeML
 and Candle read-eval-print loop (REPL).
+
+[scheme](scheme):
+A compiler from Scheme to CakeML

compiler/scheme/Holmakefile

@@ -0,0 +1,20 @@
+INCLUDES = $(CAKEMLDIR)/translator \
+           $(CAKEMLDIR)/basis \
+           $(CAKEMLDIR)/basis/pure \
+           $(CAKEMLDIR)/compiler/parsing \
+           $(CAKEMLDIR)/semantics \
+           $(CAKEMLDIR)/misc \
+           $(HOLDIR)/examples/formal-languages/context-free
+
+all: $(DEFAULT_TARGETS) README.md
+.PHONY: all
+
+README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
+# Filter out unverified/ (they don't have a readmePrefix)
+DIRS = $(patsubst examples/,,$(patsubst unverified/,,$(wildcard */)))
+README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix unverified/README.md examples/README.md $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
+	$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
+
+ifdef POLY
+HOLHEAP = $(CAKEMLDIR)/misc/cakeml-heap
+endif

compiler/scheme/README.md

@@ -0,0 +1,34 @@
+A compiler from Scheme to CakeML
+
+[compilation](compilation):
+Compilation scripts for the Scheme-to-CakeML compiler.
+
+[examples](examples):
+Example Scheme programs compiled using the Scheme compiler
+
+[proofs](proofs):
+Proofs for Scheme to CakeML compiler
+
+[scheme_astScript.sml](scheme_astScript.sml):
+AST of Scheme
+
+[scheme_compilerScript.sml](scheme_compilerScript.sml):
+Definition of a compiler from Scheme to CakeML
+
+[scheme_parsingScript.sml](scheme_parsingScript.sml):
+Parser for Scheme
+
+[scheme_semanticsScript.sml](scheme_semanticsScript.sml):
+Semantics of Scheme
+
+[scheme_to_cakeScript.sml](scheme_to_cakeScript.sml):
+Code generator for Scheme to CakeML compiler
+
+[scheme_valuesScript.sml](scheme_valuesScript.sml):
+Definition of Scheme values
+
+[translation](translation):
+CakeML translation of Scheme-to-CakeML compiler
+
+[unverified](unverified):
+An unverified compiler from Scheme to ML written in Haskell

compiler/scheme/compilation/Holmakefile

@@ -0,0 +1,12 @@
+INCLUDES = $(CAKEMLDIR)/compiler/scheme/translation $(CAKEMLDIR)/compiler $(CAKEMLDIR)/cv_translator $(CAKEMLDIR)/developers/bin
+
+all: $(DEFAULT_TARGETS) README.md
+.PHONY: all
+README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
+DIRS = $(wildcard */)
+README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
+	$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
+
+ifdef POLY
+HOLHEAP = $(CAKEMLDIR)/cv_translator/cake_compile_heap
+endif

compiler/scheme/compilation/README.md

@@ -0,0 +1,4 @@
+Compilation scripts for the Scheme-to-CakeML compiler.
+
+[scheme_compilerCompileScript.sml](scheme_compilerCompileScript.sml):
+In-logic compilation of the Scheme-to-CakeML compiler

compiler/scheme/compilation/readmePrefix

@@ -0,0 +1 @@
+Compilation scripts for the Scheme-to-CakeML compiler.

compiler/scheme/compilation/scheme_compilerCompileScript.sml

@@ -0,0 +1,13 @@
+(*
+  In-logic compilation of the Scheme-to-CakeML compiler
+*)
+
+open preamble scheme_compilerProgTheory eval_cake_compile_x64Lib;
+
+val _ = new_theory "scheme_compilerCompile";
+
+Theorem scheme_compiler_compiled =
+        eval_cake_compile_x64 "" scheme_compiler_prog_def
+                                "scheme_compiler.S";
+
+val _ = export_theory ();

compiler/scheme/examples/Makefile

@@ -0,0 +1,58 @@
+.PHONY: all clean
+
+OS ?= $(shell uname)
+
+ifeq ($(OS),Windows_NT)
+	PREF =
+	SUFF = .exe
+	EVALFLAG =
+else
+	PREF = ./
+	SUFF =
+	EVALFLAG = -DEVAL
+endif
+
+CAKEOPT = --sexp=true
+
+ifeq ($(OS),Darwin)
+	# These options avoid linker warnings on macOS
+	LDFLAGS += -Wl,-no_pie
+	EVALFLAG =
+endif
+
+ALL = $(patsubst %.scm,%.cake$(SUFF),$(wildcard *.scm))
+
+CFLAGS+=-O2
+LDLIBS+=-lm
+
+ARCH=x64
+WORD_SIZE=64
+
+all: $(ALL)
+
+%.cake.S: %.scm cake scheme_compiler$(SUFF)
+	cat $< | $(PREF)scheme_compiler$(SUFF) | $(PREF)cake$(SUFF) $(CAKEOPT) > $@
+
+%.cake$(SUFF) : %.cake.S ../../../basis/basis_ffi.c
+	$(CC) $< ../../../basis/basis_ffi.c $(LOADLIBES) $(LDLIBS) -o $@ $(LDFLAGS)
+
+scheme_compiler.S: ../compilation/scheme_compiler.S
+	cp $< $@
+
+scheme_compiler$(SUFF): scheme_compiler.S ../../../basis/basis_ffi.c
+	$(CC) -o $@ scheme_compiler.S ../../../basis/basis_ffi.c $(LDLIBS)
+
+cake.S:
+	@if [ ! -f "../../bootstrap/compilation/x64/64/$(@F)" ] ; then $(MAKE) download ; else cp ../../bootstrap/compilation/x64/64/$(@F) $@ ; fi
+
+download:
+	@echo "$(red)Could not find \`cake.S\`. Downloading the latest version from CakeML's GitHub releases.$(reset)"
+	curl -LO https://github.com/CakeML/cakeml/releases/latest/download/cake-$(ARCH)-$(WORD_SIZE).tar.gz
+	@tar -zxf cake-$(ARCH)-$(WORD_SIZE).tar.gz --strip-components 1 cake-$(ARCH)-$(WORD_SIZE)/cake.S
+	@rm cake-$(ARCH)-$(WORD_SIZE).tar.gz
+
+cake$(SUFF): cake.S ../../../basis/basis_ffi.c
+	$(CC) $(CFLAGS) $< ../../../basis/basis_ffi.c $(LOADLIBES) $(EVALFLAG) -o $@ $(LDFLAGS) $(LDLIBS)
+
+clean:
+	rm cake$(SUFF) cake.S scheme_compiler$(SUFF) scheme_compiler.S *.cake.S *.cake$(SUFF)

compiler/scheme/examples/README.md

@@ -0,0 +1 @@
+Example Scheme programs compiled using the Scheme compiler

compiler/scheme/examples/facimp.scm

@@ -0,0 +1,4 @@
+(letrec ((fac (lambda (x)
+  (letrec ((st 0) (acc 1)) (begin
+    (call/cc (lambda (k) (set! st k)))
+    (if (eqv? x 0) acc (st (begin (set! acc ( * acc x)) (set! x (- x 1)))))))))) (fac 6))

compiler/scheme/examples/fib.scm

@@ -0,0 +1,7 @@
+(letrec
+    ((fib (lambda (n)
+              (if (eqv? n 0) n
+                   (if (eqv? n 1) n
+                       (+ (fib (- n 1))
+                          (fib (- n 2))))))))
+    (fib 30))

compiler/scheme/examples/list.scm

@@ -0,0 +1,9 @@
+(letrec (
+  (cons (lambda (car cdr) (lambda (b) (if b car cdr))))
+  (car (lambda (cons) (cons #t)))
+  (cdr (lambda (cons) (cons #f)))
+  (nil 999)
+  (nil? (lambda (l) (eqv? l nil)))
+  (length (lambda (l) (if (nil? l) 0 (+ 1 (length (cdr l))))))
+  (index (lambda (n l) (if (eqv? n 0) (car l) (index (- n 1) (cdr l)))))
+) (index 1 (cons 10 (cons 20 (cons 30 nil)))))

compiler/scheme/examples/nondet.scm

@@ -0,0 +1,35 @@
+(letrec
+    ((nondet
+      (lambda (fun)
+          (call/cc
+           (lambda (cc)
+               (letrec ((k cc))
+                   (fun
+                    (lambda (f n m)
+                         (letrec ((i n)
+                                  (last k))
+                             (begin
+                              (call/cc
+                               (lambda (cc) (set! k (lambda (v) (begin (set! i (+ i 1)) (cc v))))))
+                              (if (eqv? i m)
+                                  (begin (set! k last) (k (- 1)))
+                                  (f i)))))
+                    (lambda () (k (- 1)))))))))
+
+     (triangle
+      (lambda (n)
+          (if (eqv? n 0) n
+              (+ n (triangle (- n 1))))))
+     (fib
+      (lambda (n)
+          (if (eqv? n 0) n
+              (if (eqv? n 1) n
+                  (+ (fib (- n 1))
+                     (fib (- n 2))))))))
+
+    ;(display
+     (nondet
+      (lambda (choose fail)
+          (letrec ((x (choose triangle 3 10))
+                   (y (choose fib 3 10)))
+              (if (eqv? x y) x (fail))))));)

compiler/scheme/examples/print.scm

@@ -0,0 +1 @@
+(letrec ((touch 0)) (begin (set! touch 1) touch))

compiler/scheme/examples/tailfib.scm

@@ -0,0 +1,5 @@
+(letrec
+    ((fib (lambda (n a b)
+              (if (eqv? n 0) a
+                  (fib (- n 1) (+ a b) a)))))
+    (fib 35 0 1))

compiler/scheme/proofs/Holmakefile

@@ -0,0 +1,21 @@
+INCLUDES = $(CAKEMLDIR)/translator \
+           $(CAKEMLDIR)/basis \
+           $(CAKEMLDIR)/basis/pure \
+           $(CAKEMLDIR)/compiler/parsing \
+           $(CAKEMLDIR)/semantics \
+           $(CAKEMLDIR)/misc \
+           $(HOLDIR)/examples/formal-languages/context-free \
+           $(CAKEMLDIR)/compiler/scheme
+
+all: $(DEFAULT_TARGETS) README.md
+.PHONY: all
+
+README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
+# Filter out tests/ (they don't have a readmePrefix)
+DIRS = $(patsubst tests/,,$(wildcard */))
+README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
+	$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
+
+ifdef POLY
+HOLHEAP = $(CAKEMLDIR)/misc/cakeml-heap
+endif

compiler/scheme/proofs/README.md

@@ -0,0 +1,7 @@
+Proofs for Scheme to CakeML compiler
+
+[scheme_semanticsPropsScript.sml](scheme_semanticsPropsScript.sml):
+Proofs of Scheme semantics properties
+
+[scheme_to_cakeProofScript.sml](scheme_to_cakeProofScript.sml):
+Proof of semantic preservation from Scheme to CakeML

compiler/scheme/proofs/readmePrefix

@@ -0,0 +1 @@
+Proofs for Scheme to CakeML compiler