Permalink
Browse files

Work on READMEs for semantics, for #71

  • Loading branch information...
xrchz committed Aug 15, 2018
1 parent 3f35a6b commit e627e661b58f0da2e53d47834a889d02e646a6fd
View
@@ -46,7 +46,7 @@ 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
[developers](developers):
This directory contains scripts for automating routine tasks, e.g., for
@@ -61,7 +61,7 @@ and what we want to use for CakeML development.
[semantics](semantics):
The definition of the CakeML language. The definition is (mostly)
expressed in Lem (http://www.cs.kent.ac.uk/~sao/lem), but the
expressed in [Lem](http://www.cs.kent.ac.uk/~sao/lem), but the
generated HOL is also included. The directory includes definitions of:
- the concrete syntax
- the abstract syntax
@@ -75,7 +75,7 @@ A proof-producing translator from HOL functions to CakeML.
[tutorial](tutorial):
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.
[unverified](unverified):
Various unverified tools, e.g. tools for converting OCaml to CakeML
View
@@ -1,5 +1,5 @@
OPTIONS = QUIT_ON_FAILURE
INCLUDES = ../misc $(HOLDIR)/examples/formal-languages/context-free $(HOLDIR)/examples/fun-op-sem/lprefix_lub ffi
INCLUDES = ../developers ../misc $(HOLDIR)/examples/formal-languages/context-free $(HOLDIR)/examples/fun-op-sem/lprefix_lub ffi
THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
TARGETS0 = $(patsubst %Theory.sml,,$(THYFILES))
@@ -38,6 +38,16 @@ namespaceScript.sml: namespace.lem $(LEMLIB) ffi/ffi.lem addancs
$(LEM_CMD) $< && ./addancs $@ integer words string alist; \
else touch namespaceScript.sml ; fi
OTHER_SCRIPTS = cmlPtreeConversion gram lexer_fun namespaceProps semantics termination tokenUtils
README_SOURCES = $(LEMS) ast.lem tokens.lem namespace.lem\
grammar.txt addancs.sml astPP.sml\
$(patsubst %,%Script.sml,$(OTHER_SCRIPTS))\
$(wildcard *Syntax.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
EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o addancs
View
@@ -0,0 +1,96 @@
The definition of the CakeML language. The definition is (mostly)
expressed in [Lem](http://www.cs.kent.ac.uk/~sao/lem), but the
generated HOL is also included. The directory includes definitions of:
- the concrete syntax
- the abstract syntax
- small step semantics
- big step semantics (both functional and relational)
- semantics of FFI calls
- a type system
[addancs.sml](addancs.sml):
A script to add a set_grammar_ancestry line to a generated Script.sml file.
[alt_semantics](alt_semantics):
Alternative definitions of the semantics:
- using inductive relations (as opposed to functional big-step style), and,
- as a small-step relation.
[ast.lem](ast.lem):
Definition of CakeML abstract syntax (AST).
[astPP.sml](astPP.sml):
Pretty printing for CakeML AST
[astSyntax.sml](astSyntax.sml):
ML functions for manipulating HOL terms and types defined as part of the
CakeML semantics, in particular CakeML abstract syntax.
[cmlPtreeConversionScript.sml](cmlPtreeConversionScript.sml):
Specification of how to convert parse trees to abstract syntax.
[evaluate.lem](evaluate.lem):
Functional big-step semantics for evaluation of CakeML programs.
[ffi](ffi):
Definition of CakeML's observational semantics, in particular traces of calls
over the Foreign-Function Interface (FFI).
[fpSem.lem](fpSem.lem):
Definitions of the floating point operations used in CakeML.
[gramScript.sml](gramScript.sml):
Definition of CakeML's Context-Free Grammar.
The grammar specifies how token lists should be converted to syntax trees.
[grammar.txt](grammar.txt):
V ::= "op" ID | ID
[lexer_funScript.sml](lexer_funScript.sml):
A functional specification of lexing from strings to token lists.
[namespace.lem](namespace.lem):
TODO: document
[namespacePropsScript.sml](namespacePropsScript.sml):
Proofs about the namespace datatype.
TODO: move to proofs directory?
[primTypes.lem](primTypes.lem):
Definition of the primitive types that are in scope before any CakeML program
starts. Some of them are generated by running an initial program.
[proofs](proofs):
Theorems about CakeML's syntax and semantics.
[semanticPrimitives.lem](semanticPrimitives.lem):
Definitions of semantic primitives (e.g., values, and functions for doing
primitive operations) used in the semantics.
[semanticPrimitivesSyntax.sml](semanticPrimitivesSyntax.sml):
ML functions for manipulating the HOL terms and types defined in
semanticPrimitivesTheory.
[semanticsComputeLib.sml](semanticsComputeLib.sml):
compset for parts of the semantics, including the lexer.
[semanticsLib.sml](semanticsLib.sml):
TODO: move
[semanticsScript.sml](semanticsScript.sml):
The top-level semantics of CakeML programs.
[terminationScript.sml](terminationScript.sml):
Termination proofs for functions defined in .lem files whose termination is
not proved automatically.
[tokenUtilsScript.sml](tokenUtilsScript.sml):
Utility functions over tokens.
TODO: perhaps should just appear in tokensTheory.
[tokens.lem](tokens.lem):
The tokens of CakeML concrete syntax.
Some tokens are from Standard ML and not used in CakeML.
[typeSystem.lem](typeSystem.lem):
Specification of CakeML's type system.
View
@@ -1,3 +1,6 @@
(*
A script to add a set_grammar_ancestry line to a generated Script.sml file.
*)
fun warn s =
(TextIO.output(TextIO.stdErr, s ^ "\n"); TextIO.flushOut TextIO.stdErr)
@@ -0,0 +1,3 @@
Alternative definitions of the semantics:
- using inductive relations (as opposed to functional big-step style), and,
- as a small-step relation.
View
@@ -1,3 +1,6 @@
(*
Definition of CakeML abstract syntax (AST).
*)
open import Pervasives
open import Lib
open import Namespace
View
@@ -1,4 +1,6 @@
(*Pretty printing for CakeML AST*)
(*
Pretty printing for CakeML AST
*)
structure astPP=
struct
open HolKernel boolLib bossLib Parse astTheory stringLib
View
@@ -1,3 +1,7 @@
(*
ML functions for manipulating HOL terms and types defined as part of the
CakeML semantics, in particular CakeML abstract syntax.
*)
structure astSyntax = struct
local
open HolKernel boolLib bossLib;
@@ -1,11 +1,11 @@
(*
Specification of how to convert parse trees to abstract syntax.
*)
open preamble gramTheory tokenUtilsTheory astTheory
val _ = new_theory "cmlPtreeConversion"
(* ----------------------------------------------------------------------
Parse trees to abstract syntax
---------------------------------------------------------------------- *)
val _ = set_grammar_ancestry ["gram", "tokenUtils", "ast", "namespace"]
val _ = patternMatchesLib.ENABLE_PMATCH_CASES();
View
@@ -1,3 +1,6 @@
(*
Functional big-step semantics for evaluation of CakeML programs.
*)
open import Pervasives_extra
open import Lib
open import Ast
@@ -0,0 +1,2 @@
Definition of CakeML's observational semantics, in particular traces of calls
over the Foreign-Function Interface (FFI).
View
@@ -1,3 +1,6 @@
(*
Definitions of the floating point operations used in CakeML.
*)
open import Pervasives
open import Lib
View
@@ -1,3 +1,8 @@
(*
Definition of CakeML's Context-Free Grammar.
The grammar specifies how token lists should be converted to syntax trees.
*)
open HolKernel Parse boolLib bossLib
open tokensTheory grammarTheory locationTheory
@@ -7,10 +12,6 @@ open lcsymtacs grammarLib
val _ = new_theory "gram"
val _ = set_grammar_ancestry ["tokens", "grammar", "location"]
(* ----------------------------------------------------------------------
Define the CakeML Context-Free Grammar
---------------------------------------------------------------------- *)
val tokmap0 =
List.foldl (fn ((s,t), acc) => Binarymap.insert(acc,s,t))
(Binarymap.mkDict String.compare)
@@ -1,3 +1,6 @@
(*
A functional specification of lexing from strings to token lists.
*)
open HolKernel Parse boolLib bossLib;
val _ = new_theory "lexer_fun";
View
@@ -1,3 +1,6 @@
(*
TODO: document
*)
open import Pervasives
open import Set_extra
@@ -1,3 +1,7 @@
(*
Proofs about the namespace datatype.
TODO: move to proofs directory?
*)
open preamble;
open astTheory;
open namespaceTheory;
View
@@ -1,3 +1,7 @@
(*
Definition of the primitive types that are in scope before any CakeML program
starts. Some of them are generated by running an initial program.
*)
open import Pervasives
open import Ast
open import SemanticPrimitives
@@ -0,0 +1 @@
Theorems about CakeML's syntax and semantics.
View
@@ -1,5 +1,5 @@
The definition of the CakeML language. The definition is (mostly)
expressed in Lem (http://www.cs.kent.ac.uk/~sao/lem), but the
expressed in [Lem](http://www.cs.kent.ac.uk/~sao/lem), but the
generated HOL is also included. The directory includes definitions of:
- the concrete syntax
- the abstract syntax
@@ -1,3 +1,7 @@
(*
Definitions of semantic primitives (e.g., values, and functions for doing
primitive operations) used in the semantics.
*)
open import Pervasives
open import Lib
import List_extra
@@ -1,3 +1,7 @@
(*
ML functions for manipulating the HOL terms and types defined in
semanticPrimitivesTheory.
*)
structure semanticPrimitivesSyntax = struct
local
open HolKernel boolLib bossLib semanticPrimitivesTheory namespaceTheory;
@@ -1,3 +1,6 @@
(*
compset for parts of the semantics, including the lexer.
*)
structure semanticsComputeLib :> semanticsComputeLib =
struct
@@ -1,3 +1,6 @@
(*
TODO: move
*)
structure semanticsLib :> semanticsLib =
struct
@@ -1,3 +1,6 @@
(*
The top-level semantics of CakeML programs.
*)
open preamble;
open lexer_funTheory
open cmlPtreeConversionTheory; (* TODO: should be included in termination *)
@@ -1,3 +1,7 @@
(*
Termination proofs for functions defined in .lem files whose termination is
not proved automatically.
*)
open preamble intSimps;
open libTheory astTheory open namespaceTheory semanticPrimitivesTheory typeSystemTheory;
open evaluateTheory;
@@ -1,13 +1,13 @@
(*
Utility functions over tokens.
TODO: perhaps should just appear in tokensTheory.
*)
open preamble tokensTheory
val _ = new_theory "tokenUtils"
val _ = set_grammar_ancestry ["tokens", "grammar"]
(* ----------------------------------------------------------------------
Utility functions over tokens; perhaps should just appear in
TokensTheory
---------------------------------------------------------------------- *)
val isInt_def = Define`
isInt (IntT i) = T ∧
isInt _ = F
View
@@ -1,5 +1,8 @@
(*
The tokens of CakeML concrete syntax.
Some tokens are from Standard ML and not used in CakeML.
*)
open import Pervasives_extra
(* Tokens for Standard ML. NB, not all of them are used in CakeML *)
type token =
| WhitespaceT of nat | NewlineT | LexErrorT
| HashT | LparT | RparT | StarT | CommaT | ArrowT | DotsT | ColonT | SealT
View
@@ -1,3 +1,6 @@
(*
Specification of CakeML's type system.
*)
open import Pervasives_extra
open import Lib
open import Ast

0 comments on commit e627e66

Please sign in to comment.