The definition of the CakeML language. The definition is (mostly) expressed in 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: A script to add a set_grammar_ancestry line to a generated Script.sml file.

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: Definition of CakeML abstract syntax (AST).

astPP.sml: Pretty printing for CakeML AST

astSyntax.sml: ML functions for manipulating HOL terms and types defined as part of the CakeML semantics, in particular CakeML abstract syntax.

cmlPtreeConversionScript.sml: Specification of how to convert parse trees to abstract syntax.

evaluate.lem: Functional big-step semantics for evaluation of CakeML programs.

ffi: Definition of CakeML's observational semantics, in particular traces of calls over the Foreign-Function Interface (FFI).

fpSem.lem: Definitions of the floating point operations used in CakeML.

gramScript.sml: Definition of CakeML's Context-Free Grammar. The grammar specifies how token lists should be converted to syntax trees.

grammar.txt: V ::= "op" ID | ID

lexer_funScript.sml: A functional specification of lexing from strings to token lists.

namespace.lem: TODO: document

namespacePropsScript.sml: Proofs about the namespace datatype. TODO: move to proofs directory?

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: Theorems about CakeML's syntax and semantics.

semanticPrimitives.lem: Definitions of semantic primitives (e.g., values, and functions for doing primitive operations) used in the semantics.

semanticPrimitivesSyntax.sml: ML functions for manipulating the HOL terms and types defined in semanticPrimitivesTheory.

semanticsComputeLib.sml: compset for parts of the semantics, including the lexer.

semanticsLib.sml: TODO: move

semanticsScript.sml: The top-level semantics of CakeML programs.

terminationScript.sml: Termination proofs for functions defined in .lem files whose termination is not proved automatically.

tokenUtilsScript.sml: Utility functions over tokens. TODO: perhaps should just appear in tokensTheory.

tokens.lem: The tokens of CakeML concrete syntax. Some tokens are from Standard ML and not used in CakeML.

typeSystem.lem: Specification of CakeML's type system.