def StrataDDM.TypeExprF.instType {α : Type} (d : TypeExprF α) (bindings : Array (TypeExprF α)) : TypeExprF α

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.qualIdentKind (stx : Lean.Syntax) : Option QualifiedIdent

Get the kind as a qualified identifier.

Equations

• StrataDDM.qualIdentKind stx = match stx.getKind with | (Lean.Name.anonymous.str dialect).str name => some { dialect := dialect, name := name } | x => none

partial def StrataDDM.expandMacros (m : DialectMap) (f : PreType) (args : Nat → Option Arg) : Except Unit TypeExpr

partial def StrataDDM.Elab.TypingContext.hnf (tctx : TypingContext) (e : TypeExpr) : TypeExpr

This expands type aliases appearing at the head of the term so the head is in a normal form.

def StrataDDM.Elab.TypingContext.applyNArgs (tctx : TypingContext) (e : TypeExpr) (n : Nat) : Except (Array TypeExpr × TypeExpr) (Vector TypeExpr n × TypeExpr)

Attempt to interpret e as a n-ary function, and return the type of the arguments along with the return type if possible, or error (args, r) where args is an array with size args.size < n and r is the resulting type.

Equations

• tctx.applyNArgs e n = StrataDDM.Elab.TypingContext.applyNArgs.aux✝ tctx n #[] e

def StrataDDM.Elab.elabIdent (stx : Lean.Syntax) : String

Equations

• One or more equations did not get rendered due to their size.

structure StrataDDM.Elab.ElabContext : Type

• dialects : DialectMap
• openDialectSet : Std.HashSet DialectName
• typeOrCatDeclMap : TypeOrCatDeclMap

  Map for looking up types and categories by name.

• metadataDeclMap : MetadataDeclMap

  Map for looking up metadata by name.

• syntaxElabs : SyntaxElabMap

  Syntax elaboration functions.

• inputContext : Parser.InputContext
• globalContext : GlobalContext
• missingImport : Bool

  Flag to indicate we are missing an import (silences some warnings)

• typecheck : Bool

  When false, type inference and unification are skipped during elaboration.

structure StrataDDM.Elab.ElabState : Type

• errors : Array Lean.Message

@[reducible]

def StrataDDM.Elab.ElabM (α : Type) : Type

Equations

• StrataDDM.Elab.ElabM α = ReaderT StrataDDM.Elab.ElabContext (StateM StrataDDM.Elab.ElabState) α

@[implicit_reducible]

instance StrataDDM.Elab.instElabClassElabM : ElabClass ElabM

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev StrataDDM.Elab.FailureArray : Type

Equations

• StrataDDM.Elab.FailureArray = Array (Lean.Syntax × String)

inductive StrataDDM.Elab.MaybeQualifiedIdent : Type

• qid : QualifiedIdent → MaybeQualifiedIdent
• name : String → MaybeQualifiedIdent

def StrataDDM.Elab.instInhabitedMaybeQualifiedIdent.default : MaybeQualifiedIdent

Equations

• StrataDDM.Elab.instInhabitedMaybeQualifiedIdent.default = StrataDDM.Elab.MaybeQualifiedIdent.qid default

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedMaybeQualifiedIdent : Inhabited MaybeQualifiedIdent

Equations

• StrataDDM.Elab.instInhabitedMaybeQualifiedIdent = { default := StrataDDM.Elab.instInhabitedMaybeQualifiedIdent.default }

def StrataDDM.Elab.resolveTypeBinding (tctx : TypingContext) (loc : SourceRange) (name : String) (binding : TypingContext.VarBinding) (args : Array Tree) : ElabM Tree

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.resolveTypeOrCat (loc : SourceRange) (tpId : MaybeQualifiedIdent) : ElabM (Option (QualifiedIdent × TypeOrCatDecl))

This translate a possibly qualified identifier into a declaration in an open dialect.

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.translateQualifiedIdent (t : Tree) : MaybeQualifiedIdent

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.asTypeInfo (tree : Tree) : ElabM TypeInfo

Equations

• StrataDDM.Elab.asTypeInfo tree = match tree.info with | StrataDDM.Elab.Info.ofTypeInfo info => pure info | x => do StrataDDM.Elab.logError tree.info.loc "Expected type." pure default

def StrataDDM.Elab.checkArgSize {α : Type u_1} [ToStrataFormat α] (loc : SourceRange) (name : α) (expected : Nat) (args : Array Tree) : ElabM Unit

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.translateTypeIdent (elabInfo : ElabInfo) (qualIdentInfo : Tree) (args : Array Tree) : ElabM Tree

This resolves a type identifer using the name of the type (as name) and the arguments

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.withBindings (b : Bindings) (fmt : StrataFormat) : StrataFormat

Equations

• One or more equations did not get rendered due to their size.

partial def StrataDDM.Elab.headExpandTypeAlias (gctx : GlobalContext) (e : TypeExpr) : TypeExpr

This expands type aliases appearing at the head of the term so the root is in a normal for,.

N.B. This expects that macros have already been expanded in e.

partial def StrataDDM.Elab.checkExpressionType (tctx : TypingContext) (itype rtype : TypeExpr) : ElabM Bool

This checks that two types itype and rtype are equivalent.

In this context, itype refers to a type inferred from an operator argument at position stx and rtype refers to a type inferred or specifed by a previous argument.

partial def StrataDDM.Elab.unifyTypeVectors {argc : Nat} (isTypeP : Fin argc → Bool) (argLevel0 : Fin argc) (ea : Array TypeExpr) (tctx : TypingContext) (exprSyntax : Lean.Syntax) (ia : Array TypeExpr) (args : Vector (Option Tree) argc) : ElabM (Vector (Option Tree) argc)

partial def StrataDDM.Elab.unifyTypes {argc : Nat} (isTypeP : Fin argc → Bool) (argLevel0 : Fin argc) (expectedType : TypeExpr) (tctx : TypingContext) (exprSyntax : Lean.Syntax) (inferredType : TypeExpr) (args : Vector (Option Tree) argc) : ElabM (Vector (Option Tree) argc)

This compares the inferred type against the expected type for an argument to check if the argument value is well-typed and determine if additional type variables can be automatically inferred.

• isTypeP returns true if the argument at the given index is a type.
• argLevel refers to the index of the argument in args
• expectedType is the type of the argument for the operation/expression. Bound variables in it may refer to args in args less than argIndex.
• tctx is the typing context for inferredType.
• exprSyntax is the syntax of the expression/operator this is for. Used for positions in error reporting.
• inferredType is the type inferred from bottom up type inference. Bound variables in it may refere to bound variables in tctx.
• args is the current arguments. These may be refined by unifyTypes and the new arguments are returned.

@[reducible, inline]

abbrev StrataDDM.Elab.ElabArgFn : Type

Equations

• StrataDDM.Elab.ElabArgFn = (StrataDDM.Elab.TypingContext → Lean.Syntax → StrataDDM.Elab.ElabM StrataDDM.Elab.Tree)

def StrataDDM.Elab.elabOption (f : ElabArgFn) : ElabArgFn

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.evalBindingNameIndex {n : Nat} (trees : Vector Tree n) (idx : DebruijnIndex n) : String

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.collectNewBindingsM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (initialScope : Nat) (tree : Tree) (f : SourceRange → Binding → m α) : m (Array α)

This collects the results of applying a function f to the bindings added to the resulting context of tree after the initial number of bindings given by initialScope.

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.elabArgIndex {α : Type} {n : Nat} (initialScope : Nat) (trees : Vector Tree n) (argsIndex : Option (DebruijnIndex n)) (f : SourceRange → Binding → ElabM α) : ElabM (Array α)

Equations

• StrataDDM.Elab.elabArgIndex initialScope trees none f = pure #[]
• StrataDDM.Elab.elabArgIndex initialScope trees (some idx) f = StrataDDM.Elab.collectNewBindingsM initialScope trees[idx.toLevel] f

@[irreducible]

def StrataDDM.Elab.flattenTypeApp (arg : Tree) (args : Array Tree) : Tree × Array Tree

Parse TypeApp and TypeParen expressions to get Init.TypeExpr into head-format form.

Equations

• One or more equations did not get rendered due to their size.
• StrataDDM.Elab.flattenTypeApp arg args = (arg, args)

theorem StrataDDM.Elab.Array_size1 {α : Type u_1} [SizeOf α] {as : Array α} (szp : as.size = 1) : sizeOf as = sizeOf as[0] + 3

theorem StrataDDM.Elab.Array_size2 {α : Type u_1} [SizeOf α] {as : Array α} (szp : as.size = 2) : sizeOf as = sizeOf as[0] + sizeOf as[1] + 4

theorem StrataDDM.Elab.Pair_size {α : Type u_1} {β : Type u_2} [SizeOf α] [SizeOf β] (a : α) (b : β) : sizeOf (a, b) = 1 + sizeOf a + sizeOf b

@[irreducible]

theorem StrataDDM.Elab.flattenTypeApp_size (arg : Tree) (args : Array Tree) : sizeOf (flattenTypeApp arg args) ≤ sizeOf arg + sizeOf args + 1

def StrataDDM.Elab.logInternalError {m : Type → Type} [ElabClass m] (loc : SourceRange) (msg : String) : m Unit

Equations

• StrataDDM.Elab.logInternalError loc msg = StrataDDM.Elab.logError loc msg

partial def StrataDDM.Elab.translateSyntaxCat (tree : Tree) : ElabM SyntaxCat

Evaluate the tree as a type expression.

@[irreducible]

def StrataDDM.Elab.translateTypeExpr (tree : Tree) : ElabM TypeExpr

Evaluate the tree as a type expression.

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.translateBindingKind (tree : Tree) : ElabM BindingKind

Evaluate the tree as a type expression.

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.elabTypeParams {n : Nat} (initSize : Nat) (args : Vector Tree n) (idx : Option (DebruijnIndex n)) : ElabM (List String)

Extract type parameter names from a bindings argument.

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.evalBindingSpec {bindings : ArgDecls} (tctx : TypingContext) (loc : SourceRange) (initSize : Nat) (dialectName : DialectName) (b : BindingSpec bindings) (args : Vector Tree bindings.size) : ElabM TypingContext

Construct a binding from a binding spec and the arguments to an operation.

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.resultType! (tctx : TypingContext) (e : TypeExpr) (n : Nat) : TypeExpr

Given a type expression and a natural number, this returns a

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.inferType (tctx : TypingContext) (e : Expr) : ElabM TypeExpr

Returns the type of e in typing context tctx.

Equations

• One or more equations did not get rendered due to their size.

partial def StrataDDM.Elab.translateTypeTree (arg : Tree) : ElabM Tree

Given a tree from operations with category Init.TypeExpr, build a tree with the type or category successfully translated.

def StrataDDM.Elab.getSyntaxArgs (stx : Lean.Syntax) (ident : QualifiedIdent) (expected : Nat) : ElabM (Vector Lean.Syntax expected)

Return the arguments to the given syntax declaration.

This should alway succeeed, but captures an internal error if an invariant check fails.

Equations

• One or more equations did not get rendered due to their size.

inductive StrataDDM.Elab.ElabArgKind : Type

The kind of elaboration to perform for an argument in runSyntaxElaborator. Unlike ArgDeclKind, this distinguishes pre-types (which need macro expansion) from already-resolved type expressions.

• preType (tp : PreType) : ElabArgKind
• typeExpr (tp : TypeExpr) : ElabArgKind
• cat (k : SyntaxCat) : ElabArgKind

def StrataDDM.Elab.ElabArgKind.isType : ElabArgKind → Bool

Equations

• (StrataDDM.Elab.ElabArgKind.cat c).isType = StrataDDM.SyntaxCatF.isType c
• x✝.isType = false

def StrataDDM.Elab.ElabArgKind.ofArgDeclKind : ArgDeclKind → ElabArgKind

Equations

• StrataDDM.Elab.ElabArgKind.ofArgDeclKind (StrataDDM.ArgDeclKind.type tp) = StrataDDM.Elab.ElabArgKind.preType tp
• StrataDDM.Elab.ElabArgKind.ofArgDeclKind (StrataDDM.ArgDeclKind.cat c) = StrataDDM.Elab.ElabArgKind.cat c

partial def StrataDDM.Elab.elabOperation (tctx : TypingContext) (stx : Lean.Syntax) : ElabM Tree

partial def StrataDDM.Elab.elabSyntaxArg {argc : Nat} (getKind : Fin argc → ElabArgKind) (isTypeP : Fin argc → Bool) (tctx : TypingContext) (astx : Lean.Syntax) (argIdx : Fin argc) (trees : Vector (Option Tree) argc) : ElabM (Vector (Option Tree) argc)

Elaborate a single argument based on its ElabArgKind. Returns the updated trees vector with the result placed at argIdx.

partial def StrataDDM.Elab.runSyntaxElaborator {argc : Nat} (getKind : Fin argc → ElabArgKind) (se : SyntaxElaborator) (tctx0 : TypingContext) (args : Vector Lean.Syntax se.syntaxCount) : ElabM (Vector Tree argc)

Elaborate all syntax arguments for an operation according to the SyntaxElaborator's ordering. Iterates over se.argElaborators, computes the typing context for each argument (handling datatype scopes for recursive types), and delegates to elabSyntaxArg for the actual elaboration. Returns the elaborated Tree vector and the result TypingContext.

partial def StrataDDM.Elab.elaborateWithPreRegistrationCore {argc : Nat} (argDecls : Vector ArgDecl argc) (se : SyntaxElaborator) (tctx0 : TypingContext) (fallbackLoc : SourceRange) (stxArgs : Vector Lean.Syntax se.syntaxCount) (scopeArgLevel : Nat) (label : String) (extractInfo : GlobalContext → Lean.Syntax → ElabM GlobalContext) : ElabM (Vector Tree argc × TypingContext)

Two-phase elaboration for operations annotated with @[preRegisterTypes] or @[preRegisterFunctions].

• Phase 1: Resolve the scope argument, extract children, and fold extractInfo over them to pre-register names in the GlobalContext.
• Phase 2: Fully elaborate all args with the updated context.

label is used in error messages to identify the caller.

For @[preRegisterTypes]: pre-registers type-level bindings so mutual type references resolve. Known deviation: typeParams args are elaborated twice — once in Phase 1 (against tctx0) to extract param names, and again in Phase 2 (against the per-child context). Phase 1 typeParams trees cannot be reused because collectNewBindingsM requires tree.info.inputCtx.bindings.size ≥ initialScope, which fails when the Phase 1 context is smaller than the Phase 2 per-child context.

For @[preRegisterFunctions]: pre-registers expression-level bindings (function signatures) so mutual calls resolve.

partial def StrataDDM.Elab.extractFunctionInfo (gctx0 : GlobalContext) (child : Lean.Syntax) : ElabM GlobalContext

Phase 1 helper for a single child function in a mutual recursive block.

Partially elaborates the child's name, bindings, and return type to extract the function signature, then pre-registers it as an expression-level binding in the GlobalContext. This makes all sibling function names (including self) available when elaborating bodies in Phase 2.

partial def StrataDDM.Elab.extractDatatypeInfo (gctx0 : GlobalContext) (child : Lean.Syntax) : ElabM GlobalContext

Phase 1 helper for a single child operation in a mutual block.

Partially elaborates the child's name and typeParams args to extract the type name and parameter names, then pre-registers the type in the TypingContext's GlobalContext via preRegisterType. Returns the updated TypingContext with the new type registered.

partial def StrataDDM.Elab.elabType (tctx : TypingContext) (stx : Lean.Syntax) : ElabM Tree

partial def StrataDDM.Elab.catElaborator (c : SyntaxCat) : TypingContext → Lean.Syntax → ElabM Tree

partial def StrataDDM.Elab.elabExpr (tctx : TypingContext) (stx : Lean.Syntax) : ElabM Tree

def StrataDDM.Elab.runElab {α : Type} (action : ElabM α) : DeclM α

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Elab.elabCommand (leanEnv : Lean.Environment) : DeclM (Option Tree)

Equations

• One or more equations did not get rendered due to their size.