Skip to content

Latest commit

 

History

History
 
 

semantics

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

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.