Skip to content

Commit a2d4bc2

Browse files
myreenmyreen
authored
Merge pull request #1183 from CakeML/scheme
Scheme
2 parents 26fdfd0 + 0983d75 commit a2d4bc2

38 files changed

+5452
-0
lines changed

‎compiler/README.md

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,3 +42,6 @@ Correctness proof for the CakeML compiler.
4242
[repl](repl):
4343
Some definitions and proofs used in the proof of the CakeML
4444
and Candle read-eval-print loop (REPL).
45+
46+
[scheme](scheme):
47+
A compiler from Scheme to CakeML

‎compiler/scheme/Holmakefile

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
INCLUDES = $(CAKEMLDIR)/translator \
2+
$(CAKEMLDIR)/basis \
3+
$(CAKEMLDIR)/basis/pure \
4+
$(CAKEMLDIR)/compiler/parsing \
5+
$(CAKEMLDIR)/semantics \
6+
$(CAKEMLDIR)/misc \
7+
$(HOLDIR)/examples/formal-languages/context-free
8+
9+
all: $(DEFAULT_TARGETS) README.md
10+
.PHONY: all
11+
12+
README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
13+
# Filter out unverified/ (they don't have a readmePrefix)
14+
DIRS = $(patsubst examples/,,$(patsubst unverified/,,$(wildcard */)))
15+
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix unverified/README.md examples/README.md $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
16+
$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
17+
18+
ifdef POLY
19+
HOLHEAP = $(CAKEMLDIR)/misc/cakeml-heap
20+
endif

‎compiler/scheme/README.md

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
A compiler from Scheme to CakeML
2+
3+
[compilation](compilation):
4+
Compilation scripts for the Scheme-to-CakeML compiler.
5+
6+
[examples](examples):
7+
Example Scheme programs compiled using the Scheme compiler
8+
9+
[proofs](proofs):
10+
Proofs for Scheme to CakeML compiler
11+
12+
[scheme_astScript.sml](scheme_astScript.sml):
13+
AST of Scheme
14+
15+
[scheme_compilerScript.sml](scheme_compilerScript.sml):
16+
Definition of a compiler from Scheme to CakeML
17+
18+
[scheme_parsingScript.sml](scheme_parsingScript.sml):
19+
Parser for Scheme
20+
21+
[scheme_semanticsScript.sml](scheme_semanticsScript.sml):
22+
Semantics of Scheme
23+
24+
[scheme_to_cakeScript.sml](scheme_to_cakeScript.sml):
25+
Code generator for Scheme to CakeML compiler
26+
27+
[scheme_valuesScript.sml](scheme_valuesScript.sml):
28+
Definition of Scheme values
29+
30+
[translation](translation):
31+
CakeML translation of Scheme-to-CakeML compiler
32+
33+
[unverified](unverified):
34+
An unverified compiler from Scheme to ML written in Haskell

‎compiler/scheme/compilation/Holmakefile

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
INCLUDES = $(CAKEMLDIR)/compiler/scheme/translation $(CAKEMLDIR)/compiler $(CAKEMLDIR)/cv_translator $(CAKEMLDIR)/developers/bin
2+
3+
all: $(DEFAULT_TARGETS) README.md
4+
.PHONY: all
5+
README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
6+
DIRS = $(wildcard */)
7+
README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
8+
$(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES)
9+
10+
ifdef POLY
11+
HOLHEAP = $(CAKEMLDIR)/cv_translator/cake_compile_heap
12+
endif

‎compiler/scheme/compilation/README.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
Compilation scripts for the Scheme-to-CakeML compiler.
2+
3+
[scheme_compilerCompileScript.sml](scheme_compilerCompileScript.sml):
4+
In-logic compilation of the Scheme-to-CakeML compiler

‎compiler/scheme/compilation/readmePrefix

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Compilation scripts for the Scheme-to-CakeML compiler.

‎compiler/scheme/compilation/scheme_compilerCompileScript.sml

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
(*
2+
In-logic compilation of the Scheme-to-CakeML compiler
3+
*)
4+
5+
open preamble scheme_compilerProgTheory eval_cake_compile_x64Lib;
6+
7+
val _ = new_theory "scheme_compilerCompile";
8+
9+
Theorem scheme_compiler_compiled =
10+
eval_cake_compile_x64 "" scheme_compiler_prog_def
11+
"scheme_compiler.S";
12+
13+
val _ = export_theory ();

‎compiler/scheme/examples/Makefile

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
.PHONY: all clean
2+
3+
OS ?= $(shell uname)
4+
5+
ifeq ($(OS),Windows_NT)
6+
PREF =
7+
SUFF = .exe
8+
EVALFLAG =
9+
else
10+
PREF = ./
11+
SUFF =
12+
EVALFLAG = -DEVAL
13+
endif
14+
15+
CAKEOPT = --sexp=true
16+
17+
ifeq ($(OS),Darwin)
18+
# These options avoid linker warnings on macOS
19+
LDFLAGS += -Wl,-no_pie
20+
EVALFLAG =
21+
endif
22+
23+
ALL = $(patsubst %.scm,%.cake$(SUFF),$(wildcard *.scm))
24+
25+
CFLAGS+=-O2
26+
LDLIBS+=-lm
27+
28+
ARCH=x64
29+
WORD_SIZE=64
30+
31+
all: $(ALL)
32+
33+
%.cake.S: %.scm cake scheme_compiler$(SUFF)
34+
cat $< | $(PREF)scheme_compiler$(SUFF) | $(PREF)cake$(SUFF) $(CAKEOPT) > $@
35+
36+
%.cake$(SUFF) : %.cake.S ../../../basis/basis_ffi.c
37+
$(CC) $< ../../../basis/basis_ffi.c $(LOADLIBES) $(LDLIBS) -o $@ $(LDFLAGS)
38+
39+
scheme_compiler.S: ../compilation/scheme_compiler.S
40+
cp $< $@
41+
42+
scheme_compiler$(SUFF): scheme_compiler.S ../../../basis/basis_ffi.c
43+
$(CC) -o $@ scheme_compiler.S ../../../basis/basis_ffi.c $(LDLIBS)
44+
45+
cake.S:
46+
@if [ ! -f "../../bootstrap/compilation/x64/64/$(@F)" ] ; then $(MAKE) download ; else cp ../../bootstrap/compilation/x64/64/$(@F) $@ ; fi
47+
48+
download:
49+
@echo "$(red)Could not find \`cake.S\`. Downloading the latest version from CakeML's GitHub releases.$(reset)"
50+
curl -LO https://github.com/CakeML/cakeml/releases/latest/download/cake-$(ARCH)-$(WORD_SIZE).tar.gz
51+
@tar -zxf cake-$(ARCH)-$(WORD_SIZE).tar.gz --strip-components 1 cake-$(ARCH)-$(WORD_SIZE)/cake.S
52+
@rm cake-$(ARCH)-$(WORD_SIZE).tar.gz
53+
54+
cake$(SUFF): cake.S ../../../basis/basis_ffi.c
55+
$(CC) $(CFLAGS) $< ../../../basis/basis_ffi.c $(LOADLIBES) $(EVALFLAG) -o $@ $(LDFLAGS) $(LDLIBS)
56+
57+
clean:
58+
rm cake$(SUFF) cake.S scheme_compiler$(SUFF) scheme_compiler.S *.cake.S *.cake$(SUFF)

‎compiler/scheme/examples/README.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Example Scheme programs compiled using the Scheme compiler

‎compiler/scheme/examples/facimp.scm

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
(letrec ((fac (lambda (x)
2+
(letrec ((st 0) (acc 1)) (begin
3+
(call/cc (lambda (k) (set! st k)))
4+
(if (eqv? x 0) acc (st (begin (set! acc ( * acc x)) (set! x (- x 1)))))))))) (fac 6))

0 commit comments

Comments
 (0)