The definition of the CakeML language. 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.
alt_semantics: Alternative definitions of the semantics:
- using inductive relations (as opposed to functional big-step style), and,
- as a small-step relation.
astPP.sml: Pretty printing for CakeML AST
astScript.sml: Definition of CakeML abstract syntax (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.
evaluateScript.sml: 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).
fpOptScript.sml: Model of floating-point optimizations
fpSemScript.sml: Definitions of the floating point operations used in CakeML.
fpValTreeScript.sml: Values used to model floating-points, in the style of Icing
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.
namespaceScript.sml: Defines a datatype for nested namespaces where names can be either short (e.g. foo) or long (e.g. ModuleA.InnerB.bar).
primTypesScript.sml: 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.
realOpsScript.sml: Real-valued operations for source semantics
semanticPrimitivesScript.sml: 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.
tokenUtilsScript.sml: Utility functions over tokens. TODO: perhaps should just appear in tokensTheory.
tokensScript.sml: The tokens CakeML concrete syntax. Some tokens are from Standard ML and not used in CakeML.
typeSystemScript.sml: Specification of CakeML's type system.