Permalink
Browse files

Work on READMEs for #71

  • Loading branch information...
xrchz committed Aug 13, 2018
1 parent d5e487e commit 58324cb45f74096d7f329a0453773ac205cbfa29
@@ -5,9 +5,14 @@ INCLUDES = ../misc ../semantics parsing inference backend\
backend/x64\
$(HOLDIR)/examples/formal-languages/context-free

all: compilerTheory.uo compilationLib.uo
all: compilerTheory.uo compilationLib.uo README.md
.PHONY: all

README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml)
DIRS = $(wildcard */)
README.md: ../developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
../developers/readme_gen $(README_SOURCES)

ifdef POLY
HOLHEAP = heap
PARENT_HOLHEAP = backend/heap
@@ -0,0 +1,41 @@
A verified compiler for CakeML, including:
- parsing: lexer and PEG parser
- inference: type inferencer
- backend: compilation to ASM assembly language
- encoders: code generation to x86, ARM, and more

[backend](backend):
The CakeML compiler backend.

[benchmarks](benchmarks):
Two benchmark suites for the CakeML compiler.

[bootstrap](bootstrap):
Theories that perform proof-grounded bootstrapping of
the CakeML compiler in HOL.

[compilationLib.sml](compilationLib.sml):
Library for in-logic compilation of CakeML abstract syntax producing machine
code (for a variety of targets) using the CakeML compiler backend.

[compilerScript.sml](compilerScript.sml):
Definition of the CakeML compiler as a function that takes a list of command
line arguments and a string corresponding to standard input, and produces a
pair of output strings for standard error and standard output (the latter
containing the generated machine code if successful).

[encoders](encoders):
Encoders for CakeML's ASM abstract assembly language into each of the concrete
targets of the CakeML compiler.

[inference](inference):
The CakeML type inferencer.

[parsing](parsing):
The CakeML parser.

[proofs](proofs):
Correctness proof for the CakeML compiler.

[testingScript.sml](testingScript.sml):
TODO: to be deleted
@@ -0,0 +1 @@
The CakeML compiler backend.
@@ -1,4 +1,4 @@
This directory contains two benchmark suites for CakeML.
Two benchmark suites for the CakeML compiler.

Requirements
---
@@ -0,0 +1,2 @@
Theories that perform proof-grounded bootstrapping of
the CakeML compiler in HOL.
@@ -1,3 +1,7 @@
(*
Library for in-logic compilation of CakeML abstract syntax producing machine
code (for a variety of targets) using the CakeML compiler backend.
*)
structure compilationLib = struct

open preamble backendTheory
@@ -1,3 +1,9 @@
(*
Definition of the CakeML compiler as a function that takes a list of command
line arguments and a string corresponding to standard input, and produces a
pair of output strings for standard error and standard output (the latter
containing the generated machine code if successful).
*)
open preamble
lexer_funTheory lexer_implTheory
cmlParseTheory
@@ -0,0 +1,2 @@
Encoders for CakeML's ASM abstract assembly language into each of the concrete
targets of the CakeML compiler.
@@ -0,0 +1 @@
The CakeML type inferencer.
@@ -1,9 +1,3 @@
# Notes on Verified Parsing for CakeML.

The parsing function that actually runs in the CakeML system should conform to the specification, which is the grammar in `semantics/gram`. Here conforming means that if a sequence of tokens has a parse tree in the grammar, then the function should return that parse tree (*completeness*). Dually, if the function returns a parse tree, it should be correct according to the grammar (*soundness*).

The parsing function is one that executes a *Parsing Expression Grammar* (or PEG). PEGs provide an LL-like attack on input strings, but add the ability to do significant back-tracking if necessary. The CakeML PEG is specified in the file cmlPEGScript.sml. The same file includes a proof that the PEG is well-formed, which means that execution will always terminate (*totality*). As PEG execution really is a function (`peg_exec` to be precise), we also have that execution is *deterministic*. (The necessary background theory of PEGs is in the main HOL distribution.)

## Manifest

* `cmlPEG`: theory defining the PEG for CakeML. Includes a proof that the PEG is well-formed.
@@ -0,0 +1,16 @@
The CakeML parser.

The parsing function should conform to the specification, which is the grammar
in `../semantics/gram`. Here conforming means that if a sequence of tokens has a
parse tree in the grammar, then the function should return that parse tree
(*completeness*). Dually, if the function returns a parse tree, it should be
correct according to the grammar (*soundness*).

The parsing function is one that executes a *Parsing Expression Grammar* (or
PEG). PEGs provide an LL-like attack on input strings, but add the ability to
do significant back-tracking if necessary. The CakeML PEG is specified in the
file cmlPEGScript.sml. The same file includes a proof that the PEG is
well-formed, which means that execution will always terminate (*totality*). As
PEG execution really is a function (`peg_exec` to be precise), we also have
that execution is *deterministic*. (The necessary background theory of PEGs
is in the main HOL distribution.)
@@ -0,0 +1 @@
Correctness proof for the CakeML compiler.
@@ -2,4 +2,4 @@ A verified compiler for CakeML, including:
- parsing: lexer and PEG parser
- inference: type inferencer
- backend: compilation to ASM assembly language
- targets: code generation to x86, ARM, and more
- encoders: code generation to x86, ARM, and more
@@ -1,3 +1,6 @@
(*
TODO: to be deleted
*)
load "cfTacticsBaseLib";
open preamble
cmlParseTheory
@@ -1,6 +1,7 @@
README_SOURCES = $(wildcard *.sml) $(wildcard *.sh) build-sequence

README.md: $(README_SOURCES) readmePrefix readme_gen
DIRS = $(wildcard */)
README.md: $(README_SOURCES) readmePrefix readme_gen $(patsubst %,%readmePrefix,$(DIRS))
./readme_gen $(README_SOURCES)

readme_gen: readme_gen.sml
@@ -1,2 +1,2 @@
An extended worked example on using HOL and CakeML to write verified programs,
to be presented as a tutorial on CakeML at PLDI and ICFP in 2017.
that was presented as a tutorial on CakeML at PLDI and ICFP in 2017.

0 comments on commit 58324cb

Please sign in to comment.