The definition of the CakeML language. The definition is (mostly) expressed in Lem, but the generated HOL is included. The directory includes definitions of:

• the concrete syntax,
• the abstract syntax,
• big step semantics (both functional and relational),
• a small step semantics,
• the semantics of FFI calls, and,
• the type system.

The Lem version used: rems-project/lem@194778e97d1e9a41ebbe34a8e4d5fb2d10395ba7

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: Infixes are assigned to 9 different levels. From tightest to loosest, they are

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

namespace.lem: Defines a datatype for nested namespaces where names can be either short (e.g. foo) or long (e.g. ModuleA.InnerB.bar).

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.

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.