1. Language definition🔗

The Laurel language definition consists of its types, its grammar and its semantics. Currently the semantics is split into a static part, called the resolver, and a yet-to-be-built operational part.

The parts of the language definition map onto the implementation files as follows:

• Type — LaurelAST.lean defines the Laurel AST, including the program structure (StmtExpr, declarations, procedures) and the type language (HighType). LaurelTypes.lean computes the HighType of an expression from these annotations, and TypeHierarchy.lean captures the subtyping relation between user-defined types.

• Grammar — Grammar/LaurelGrammar.st is the DDM dialect that defines Laurel's concrete syntax; it is loaded into Lean by Grammar/LaurelGrammar.lean. Grammar/ConcreteToAbstractTreeTranslator.lean turns the parsed concrete tree into the LaurelAST type, and Grammar/AbstractToConcreteTreeTranslator.lean goes the other way to render an AST back to concrete syntax.

• Static semantics (resolver) — Resolution.lean resolves references and type checks the program, producing diagnostics and a SemanticModel (defined in SemanticModel.lean) that links references to their definitions.

• Operational semantics — Laurel does not yet have a standalone interpreter; its runtime meaning is given operationally by the compilation to Core described below. The pass files under StrataLaurel/Implementation/ and the pipeline in LaurelCompilationPipeline.lean therefore constitute the operational semantics, delegating to Core's own execution and verification semantics.

Laurel program type definition The Laurel type definition allows many more programs than are required for the language as it is documented for the user. The Laurel AST has some constructs that are only used by the compilation passes, but not by the source languages, to enable gradual compilation to Core. Because of these extra constructs we call the Laurel AST wide.

If two Laurel language constructs share semantic properties, we try to capture that sharing in the AST by having a shared constructor. For example, instead of having a separate constructor for StmtExpr.Forall and for StmtExpr.Exists, there is a single StmtExpr.Quantifier with a boolean field to determine its type. A more complicated example: calls to statically defined user procedures, to datatype constructors, and to datatype destructors all go through the same StmtExpr.StaticCall constructor; resolution distinguishes them by the resolved kind of the callee rather than by AST constructor. A further consolidation is in progress (WIP): calls to primitive operators and to user-defined instance procedures are planned to go through this same call constructor as well.

All information in the Laurel AST is strongly typed. There are no fields that can hold unstructured data, which could be used by extensions to Strata. Instead, Strata extensions should attach data to AST nodes by referencing them through source locations.

Resolution The static semantics of Laurel are defined by Resolution.lean. This is where Laurel references are resolved and where type checking is done. Calling resolve will produce diagnostics and a SemanticModel that can be used to navigate between definitions and references.

Identifiers that occur in a Laurel program carry an optional uniqueId: int. During resolution, every identifier that defines a new symbol is given a unique identifier, and every identifier that refers to a definition is given the unique identifier of the definition it references. The SemanticModel uses these unique identifiers to provide navigation features.

Right now, Laurel reserves identifier names that start with $ for use in its compilation passes. In the future we may improve the passes so they never generate names that collide with user-provided names.