1.1. Strata Dialect Concepts🔗

Each Strata dialect introduces declarations that ultimately define the IR. There are five basic types of declarations:

• A Syntactic Category declaration represents a concept in a Strata dialect definition such as an expression, type, statement, or binding. They are defined by operators.

• A Operator declaration defines information that may be stored in a syntactic category, along with how it is textually presented. Operators have arguments that may reference categories or types, and use metadata to define how their arguments affect Strata typechecking.

• A Type declaration declares a new builtin type for the dialect that all programs in a dialect may refer to. Types declarations do not introduce new syntactic categories in a dialect, but rather extend a dialect Init.Type with new types that may be referred to. This allows Strata to support type variables and polymorphism.

• A Function declaration introduces a new function into Strata's builtin expression syntactic category Init.Expr. Functions have a user- definable syntax like operators, but can be polymorphic and are type checked after parsing.

• A Metadata declaration introduces a new attribute that may be attached to other Strata declarations. There are builtin metadata attributes used to control parsing and typechecking in dialects. Dialects may introduce new metadata to provide a mechanism for associating properties with declarations.

1.2. Strata Examples🔗

As a simple example, we define a sequence of progressively more complex Strata dialects with Boolean and arithmetic expressions as well as a simple assertion language. Each example provides just enough detail to help readers understand the example code. The Dialect Language Reference contains additional detail on the commands.

dialect BoolDialect;
// Introduce Boolean type
type BoolType;

// Introduce literals as constants.
fn true_lit : BoolType => "true";
fn false_lit : BoolType => "false";

// Introduce basic Boolean operations.
fn not_expr (a : BoolType) : BoolType => "-" a;
fn and (a : BoolType, b : BoolType) : BoolType => @[prec(10), leftassoc] a " && " b;
fn or (a : BoolType, b : BoolType) : BoolType => @[prec(8), leftassoc] a " || " b;
fn imp (a : BoolType, b : BoolType) : BoolType => @[prec(8), leftassoc] a " ==> " b;

// Introduce equality operations that work for arbitrary types.
// The type is inferred.
fn equal (tp : Type, a : tp, b : tp) : BoolType => @[prec(15)] a " == " b;
fn not_equal (tp : Type, a : tp, b : tp) : BoolType => @[prec(15)] a " != " b;

We can then extend these operations with an Integer type and operations.

dialect Arith;
import BoolDialect;

type Int;
fn neg_expr (a : Int) : Int => "- " a;
fn add_expr (a : Int, b : Int) : Int => @[prec(25), leftassoc] a " + " b;
fn sub_expr (a : Int, b : Int) : Int => @[prec(25), leftassoc] a " - " b;
fn mul_expr (a : Int, b : Int) : Int => @[prec(30), leftassoc] a " * " b;
fn exp_expr (a : Int, b : Int) : Int => @[prec(32), rightassoc] a " ^ " b;

fn le (a : Int, b : Int) : BoolType => @[prec(15)] a " <= " b;
fn lt (a : Int, b : Int) : BoolType => @[prec(15)] a " < " b;
fn ge (a : Int, b : Int) : BoolType => @[prec(15)] a " >= " b;
fn gt (a : Int, b : Int) : BoolType => @[prec(15)] a " > " b;

By itself, these dialects do not define a new language. To define a language, one needs to extends a builtin Command category with new commands. This is done with the following dialect that introduces commands for assertions and defining functions:

dialect AssertLang;
import Arith; // Automatically imports BoolDialect dependency of Arith

// This introduces a new operator into the Command category.
op assert (b : BoolType) : Command => "assert " b ";";

// Introduce a category for arguments.
category ArgDecl;
@[declare(var, tp)]
op decl (var : Ident, tp : Type) : ArgDecl => var " : " tp;

category ArgDecls;
op decls (l : CommaSepBy ArgDecl) : ArgDecls => "(" l ")";

@[declareFn(name, args, tp)]
op defFun (name : Ident, args : ArgDecls, tp : Type, @[scope(args)] value : tp)
  : Command => "def " name args "=" value ";";

// Now that we have binders, introduce quantifiers
fn forall_expr (args : ArgDecls, @[scope(args)] b : BoolType) : BoolType =>
  "forall " args ", " b;
fn exists_expr (args : ArgDecls, @[scope(args)] b : BoolType) : BoolType =>
  "exists " args ", " b;

With these command extensions, we are now ready to use the dialects in programs:

program AssertLang;

assert forall (a : Int), exists (b : Int), b > a;
// Assert Fermat's last theorem
assert forall (a : Int, b : Int, c : Int, n : Int),
         a > 0 && b > 0 && c > 0 && n > 2 ==> a^n + b^n != c^n;

// Introduce function
def addMul(a : Int, b : Int, c : Int) = a * b + c;

assert forall (a : Int, b : Int, c : Int),
        b >= c ==> addMul(a, b, b) >= addMul(a, c, c);

2.1. Importing dialects🔗

Imports bring declarations of another dialect into the current dialect being declared. This includes transitive imports of the dialect being imported.

2.2. Syntactic Categories🔗

Syntactic categories are introduced by the category declaration:

2.3. Operators🔗

Operators extend syntactic categories with additional constructors for data. Each Strata operator has a name that is distinct from other names in the dialect, a list of arguments to the operator, the syntactic category being extended, and a syntax definition describing how to pretty-print the operator.

op assert (b : BoolType) : Statement => "assert" b ";";

op assign (tp : Type, v : Ident, e : tp) : Statement => v " := " e ";";

@[scope(b)]
op const (b : Binding) : Command => @[prec(10)] "const " b ";";

2.4. Types and Expressions🔗

As mentioned, the builtin Init.Type and Init.Expr categories are not extended using the op declaration. Instead one introduces new types with the type declaration and extends the expression language with new functions using the fn declaration. The builtin Init.Type and Init.Expr categories have some special support to simplify the creation of typed IRs in Strata.

• Strata supports type polymorphic functions and operations and has a support for type inference that allows it to automatically infer type arguments as long as an expression argument uses that type.

• Unlike categories, user types may contain parameters and parameters may themselves be variables. This allows more general functions than can be supported by operators such as a polymorphic length function over lists.

• Types use a standardized syntax that do not require syntax definitions for each type.

• After parsing, expressions are type checked to ensure that the syntax is well formed.

type BoolType;
type Map (dom : Type, range : Type);  -- Ex. Map Nat BoolType

fn if (tp : Type, c : BoolType, t : tp, f : tp) : tp =>
   "if " c " then " t "else " f;

2.5. Metadata🔗

The Strata Init dialect provides a builtin Init.Metadata category that allows metadata to be declared and attached to other declarations in dialects. Predefined metadata attributes are used in dialect definitions for defining precedence and type checking, but additional metadata attributes can be declared in dialects to build new capabilities on top of Strata. The goal of this is to provide a user-controllable extension mechanism to Strata dialects so that dialects themselves may be repurposed to new use cases.

metadata name (id1 : tp1, id2 : tp2, ... );

Declares a new metadata operation with the given name.

The type annotations in tp1 are currently restricted to Ident (for referencing arguments), natural numbers (Num) and optional versions of each (Option Ident and Option Num). More general support for metadata will be added in a future release.

metadata prec(p : Nat); -- Controls the precedence of the outermost operator
metadata leftassoc; -- Indicates operator is left-associative
metadata rightassoc; -- Indicates operator is right associative.

fn implies (p : Pred, q : Pred) : Pred => @[prec(20), rightassoc] p " ==> " q;

fn implies (p : Pred, q : Pred) : Pred => @[prec(20)] p:20 " ==> " q:19;

2.6. Parsing, Type Checking and Pretty Printings🔗

When parsing an operation or expression from source, there is an implicit variable context that contains bindings for variables in scope. Operators may transform this context while expressions are evaluated within a context. The changes to the context are controlled via metadata, and the Strata dialect makes three declarations for affecting this.

-- Specify result scope of argument used to evaluate
-- argument or following code.
metadata scope(name : Ident);
-- Declares a new variable in the resulting scope.
metadata declare(name : Ident, type : TypeOrCat);
-- Declares a function in the resulting scope with name,
-- arguments, and return type determined by the given arguments.
metadata declareFn(name : Ident, args : Ident, type : Ident);
-- Marks a list argument as requiring at least one element.
metadata nonempty;

As an example, Strata Core's variable declaration syntax can be defined in Strata using the following code:

category Decl;
-- Decl represents a single variable declaration that extends the context.
@[declare(v, tp)]
op var (v : Ident, tp : Type) : Decl => v ":" tp;

category DeclList;
@[scope(d)]
op declAtom (d : Decl) : DeclList => d;
@[scope(d)]
op declPush (dl : DeclList, @[scope(dl)] d : Decl) : DeclList => dl "," d;

category Statement;
@[scope(dl)]
op varStatement (dl : DeclList) : Statement => "var " dl ";";

category TypeVar;
@[declareTVar(name)]
op type_var (name : Ident) : TypeVar => name;

category TypeArgs;
@[scope(args)]
op type_args (args : CommaSepBy TypeVar) : TypeArgs => "<" args ">";

@[declareFn(name, b, r)]
op command_fndecl (name : Ident,
                   typeArgs : Option TypeArgs,
                   @[scope(typeArgs)] b : Bindings,
                   @[scope(typeArgs)] r : Type) : Command =>
  "function " name typeArgs b ":" r ";";

2.7. The Init dialect🔗

The Init dialect introduces a few syntactic categories that cannot currently be defined in user definable dialects.

• Init.Type and Init.Expr represent types and expressions in Strata. Unlike other categories, these are extended through the specialized type and fn commands rather than op declarations so that expressions can be type checked after parsing. See Types and Expressions for more details.

• Syntactic categories that in dialects other than Init currently cannot take additional parameters. This support will be added in a future update, but to help users, the Init declares a few builtin parametric categories:

  • Init.Option c denotes an optional value of c. Syntactically, either c may be read in or the empty string.

  • Init.Seq c denotes a sequence of values with category c. Each value of c is separated by whitespace. When formatted, values are concatenated with no separator.

  • Init.CommaSepBy c denotes a comma-separated list of values of type c. When formatted, values are separated by , (comma followed by space).

  • Init.SpaceSepBy c denotes a space-separated list of values of type c. Parsing is identical to Init.Seq, but when formatted, values are separated by a single space.

  • Init.SpacePrefixSepBy c denotes a space-prefix-separated list of values of type c. Parsing is identical to Init.Seq, but when formatted, each value is prefixed with a space.

  All list categories (CommaSepBy, SpaceSepBy, SpacePrefixSepBy, Seq) can be marked with the @[nonempty] metadata attribute to require at least one element during parsing. For example: @[nonempty] items : SpaceSepBy Item will reject empty lists with a parse error.

• Parsing for primitive literals and identifiers cannot be directly in syntax definitions. To accommodate this, the Init dialect introduces the syntactic categories for this:

  • Init.Ident represents identifiers. These are alphanumeric sequences that start with a letter that are not otherwise used as keywords in a dialect.

  • Init.Str represents string literals. These are delimited by double quotes and use escaping for special characters.

  • Init.Num represents numeric natural number literals.

2.8. Datatypes🔗

The DDM has special support for defining dialects with algebraic datatypes (ADTs) similar to those found in functional programming languages. Datatypes allow one to define custom types with multiple constructors, each of which can have zero or more fields (constructor arguments).

Datatypes differ from other language constructs (e.g. types, operators), since they define several operations simultaneously. For example, an SMT datatype declaration defines (in addition to the type itself and the constructors) tester functions to identify to which constructor an instance belongs and accessor functions to extract the fields of a constructor. Dafny datatypes additionally produce an ordering relation, while Lean inductive types produce eliminator instances defining induction principles. The DDM enables automatic creation of (a subset of) these auxiliary functions via a configurable function template system.

datatype IntList {
  Nil(),
  Cons(head: int, tail: IntList)
};

category Constructor;
category ConstructorList;

@[constructor(name, fields)]
op constructor_mk (name : Ident, fields : Option (CommaSepBy Binding)) : Constructor =>
  name "(" fields ")";

@[constructorListAtom(c)]
op constructorListAtom (c : Constructor) : ConstructorList => c;

@[constructorListPush(cl, c)]
op constructorListPush (cl : ConstructorList, c : Constructor) : ConstructorList =>
  cl "," c;

@[declareDatatype(name, typeParams, constructors,
    perConstructor([.datatype, .literal "..is", .constructor], [.datatype], .builtin "bool"),
    perField([.field], [.datatype], .fieldType))]
op command_datatype (name : Ident,
                     typeParams : Option Bindings,
                     @[scopeDatatype(name, typeParams)] constructors : ConstructorList)
  : Command =>
  "datatype " name typeParams " {" constructors "}" ";\n";

perConstructor([.datatype, .literal "..is", .constructor], [.datatype], .builtin "bool")

perField([.field], [.datatype], .fieldType)

perConstructor([.datatype, .literal "$idx$", .constructor], [.datatype], .builtin "int")

3.1. The Generic AST🔗

The generic AST is defined in Strata.DDM.AST. All types are parameterized by an annotation type α (typically SourceRange for source locations).

The core types are listed below in the same order as the dialect concepts they represent:

• SyntaxCatF α — a reference to a syntactic category, identified by its qualified name.

• OperationF α — an application of a dialect operator. Contains the operator's qualified name and an array of arguments.

• ArgF α — a single argument to an operation. This is a sum type whose variants cover all the kinds of data an operator can receive: nested operations, expressions, types, identifiers, numeric literals, string literals, decimal literals, byte arrays, category references, optional values, and sequences.

• TypeExprF α — a type expression. Variants cover dialect-defined types (ident), bound and polymorphic type variables (bvar, tvar), global type references (fvar), and function types (arrow).

• ExprF α — a typed expression. Expressions are represented in curried form: a head (fn for a named dialect function, bvar for a bound variable, or fvar for a free variable) applied to arguments via app. Type arguments found bound and free variables are implicit and omitted.

For the common case where annotations are source locations, Strata defines abbreviations:

abbrev SyntaxCat := SyntaxCatF SourceRange
abbrev Operation := OperationF SourceRange
abbrev Arg       := ArgF SourceRange
abbrev TypeExpr  := TypeExprF SourceRange
abbrev Expr      := ExprF SourceRange

3.2. The #strata_gen Command🔗

The #strata_gen command bridges Strata dialect definitions and Lean by automatically generating Lean inductive types and conversion functions from a dialect definition. This lets developers work with dialect ASTs as ordinary Lean values — constructing, pattern matching, and transforming them — while retaining the ability to convert back to the generic AST representation for serialization, pretty-printing, and cross-dialect interoperability.

import Strata.DDM.Integration.Lean

namespace MyDialect
#strata_gen MyDialect
end MyDialect

set_option trace.Strata.generator true in
#strata_gen MyDialect

[Strata.generator] Generating AssertLangType
[Strata.generator] Generating AssertLangType.toAst
[Strata.generator] Generating AssertLangType.ofAst
[Strata.generator] Generating ArgDecl
[Strata.generator] Generating ArgDecl.toAst
[Strata.generator] Generating ArgDecl.ofAst
[Strata.generator] Generating ArgDecls
[Strata.generator] Generating ArgDecls.toAst
[Strata.generator] Generating ArgDecls.ofAst
[Strata.generator] Generating Expr
[Strata.generator] Generating Expr.toAst
[Strata.generator] Generating Expr.ofAst
[Strata.generator] Generating Command
[Strata.generator] Generating Command.toAst
[Strata.generator] Generating Command.ofAst
[Strata.generator] Declarations group: [Init.Type]
[Strata.generator] Declarations group: [AssertLang.ArgDecl]
[Strata.generator] Declarations group: [AssertLang.ArgDecls]
[Strata.generator] Declarations group: [Init.Expr]
[Strata.generator] Declarations group: [Init.Command]

category MutA;
category MutB;
op opA (b : MutB) : MutA => "opA " b;
op opB (a : MutA) : MutB => "opB " a;

dialect SQL;

op create (name : Ident, c : CommaSepBy Ident) : Command =>
  "CREATE " name "(" c ")" ";\n";

op drop (name : Ident) : Command =>
  "DROP " name ";\n";

category Columns;
op colStar : Columns => "*";
op colList (c : CommaSepBy Ident) : Columns => c;

op select (col : Columns, table : Ident) : Command =>
  "SELECT " col " FROM " table ";\n";

inductive Command (α : Type) : Type where
  | create (ann : α) (name : Ann String α) (c : Ann (Array String) α) : Command α
  | drop   (ann : α) (name : Ann String α) : Command α
  | select (ann : α) (col : Columns α) (table : Ann String α) : Command α
  deriving Repr

inductive Columns (α : Type) : Type where
  | colStar (ann : α) : Columns α
  | colList (ann : α) (c : Ann (Array String) α) : Columns α
  deriving Repr

-- Convert generated type → generic AST
Command.toAst : {α : Type} → [Inhabited α] → Command α → OperationF α

-- Convert generic AST → generated type
Command.ofAst : {α : Type} → [Inhabited α] → [Repr α]
  → OperationF α → OfAstM (Command α)

inductive Expr (α : Type) : Type where
  -- Builtin constructors (always present for Init.Expr)
  | fvar  (ann : α) (idx : Nat) : Expr α
  | bvar  (ann : α) (idx : Nat) : Expr α
  | app   (ann : α) (fn : Expr α) (arg : Expr α) : Expr α
  -- Dialect-defined constructors
  | btrue   (ann : α) : Expr α
  | bfalse  (ann : α) : Expr α
  | intLit  (ann : α) (n : Ann Nat α) : Expr α
  | add     (ann : α) (x : Expr α) (y : Expr α) : Expr α
  | mul     (ann : α) (x : Expr α) (y : Expr α) : Expr α
  -- ... (additional constructors omitted)
  deriving Repr

deriving instance BEq for Command, Columns

deriving instance BEq for
  SpecConstant, QualifiedIdent, Symbol,
  SMTSort, Term, Command

#print Command    -- Shows inductive definition and constructors
#print Columns
#check Columns.colStar  -- Columns.colStar : {α : Type} → α → Columns α

def testRoundTrip (e : Expr Unit) : Bool :=
  match e |> Expr.toAst |> Expr.ofAst with
  | .error _ => false
  | .ok g => e == g

#guard testRoundTrip <| Expr.btrue ()
#guard testRoundTrip <| Expr.app () (.fvar () 0) (.btrue ())

namespace Arith
#strata_gen Arith      -- Generates Arith.Expr, Arith.ArithType, ...
end Arith

namespace ArithChecker
#strata_gen ArithChecker  -- Generates ArithChecker.Expr, ArithChecker.Command, ...
end ArithChecker
-- ArithChecker.Expr is isomorphic to Arith.Expr (same constructors)
-- but they are separate types.