Skip to content

Latest commit

 

History

History
88 lines (65 loc) · 2.97 KB

README.md

File metadata and controls

88 lines (65 loc) · 2.97 KB
Raw

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.