structure StrataDDM.Elab.ArgDeclWithLoc : Type

An argument declaration with annotations for the source location of name and type.

• nameLoc : SourceRange
• typeLoc : SourceRange
• val : ArgDecl

@[implicit_reducible]

instance StrataDDM.Elab.instInhabitedArgDeclWithLoc : Inhabited ArgDeclWithLoc

Equations

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

def StrataDDM.Elab.instInhabitedArgDeclWithLoc.default : ArgDeclWithLoc

Equations

• StrataDDM.Elab.instInhabitedArgDeclWithLoc.default = { nameLoc := default, typeLoc := default, val := default }

structure StrataDDM.Elab.ArgDeclsMap (argc : Nat) : Type

Map for arg declarations.

• argIndexMap : Std.HashMap String Nat
• decls : Vector ArgDeclWithLoc argc
• argIndexMapSize : self.argIndexMap.size = argc
• mapIndicesValid (v : String) (p : v ∈ self.argIndexMap) : self.argIndexMap[v] < argc

def StrataDDM.Elab.ArgDeclsMap.isType {argc : Nat} (m : ArgDeclsMap argc) (lvl : Fin argc) : Bool

Equations

• m.isType lvl = m.decls[lvl].val.kind.isType

def StrataDDM.Elab.ArgDeclsMap.empty (capacity : Nat := 0) : ArgDeclsMap 0

Equations

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

def StrataDDM.Elab.ArgDeclsMap.push {n : Nat} (m : ArgDeclsMap n) (d : ArgDeclWithLoc) (isUnused : ¬d.val.ident ∈ m.argIndexMap) : ArgDeclsMap (n + 1)

Adds an additional declaration to the list of arguments.

Requires proof the name is new.

Equations

• m.push d isUnused = { argIndexMap := m.argIndexMap.insert d.val.ident m.decls.size, decls := m.decls.push d, argIndexMapSize := ⋯, mapIndicesValid := ⋯ }

def StrataDDM.Elab.ArgDeclsMap.argLevel? {argc : Nat} (argDecls : ArgDeclsMap argc) (name : String) : Option (Fin argc)

Equations

• argDecls.argLevel? name = match r : argDecls.argIndexMap[name]? with | none => none | some lvl => have lvlP := ⋯; some ⟨lvl, lvlP⟩

def StrataDDM.Elab.asTypeVar {argc : Nat} (argDecls : ArgDeclsMap argc) (loc : SourceRange) (tpId : MaybeQualifiedIdent) (argChildren : Array Tree) : ElabM (Option PreType)

Equations

• One or more equations did not get rendered due to their size.
• StrataDDM.Elab.asTypeVar argDecls loc tpId argChildren = do let y ← pure PUnit.unit (fun (y : PUnit) => pure none) y

def StrataDDM.Elab.translateFunMacro {argc : Nat} (argDecls : ArgDeclsMap argc) (loc : SourceRange) (bindingsTree : Tree) (rType : PreType) : ElabM PreType

Equations

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

@[irreducible]

def StrataDDM.Elab.translatePreType {argc : Nat} (argDecls : ArgDeclsMap argc) (tree : Tree) : ElabM PreType

Evaluate the tree as a type expression.

Equations

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

def StrataDDM.Elab.translateArgDeclKind {argc : Nat} (argDecls : ArgDeclsMap argc) (tree : Tree) : ElabM ArgDeclKind

Evaluate the tree as a type expression.

Equations

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

def StrataDDM.Elab.elabMetadataName (loc : SourceRange) (mi : MaybeQualifiedIdent) : ElabM (QualifiedIdent × MetadataDecl)

Equations

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

def StrataDDM.Elab.translateFunctionIterScope (tree : Tree) : ElabM FunctionIterScope

Translate a FunctionIterScope syntax tree to the AST type

Equations

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

def StrataDDM.Elab.translateNamePatternPart (tree : Tree) : ElabM NamePatternPart

Translate a NamePatternPart syntax tree to the AST type

Equations

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

def StrataDDM.Elab.translateNamePattern (tree : Tree) : ElabM (Array NamePatternPart)

Translate a NamePattern syntax tree (array of NamePatternPart)

Equations

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

def StrataDDM.Elab.translateTypeRef (tree : Tree) : ElabM TypeRef

Translate a TypeRef syntax tree to the AST type

Equations

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

def StrataDDM.Elab.translateTypeRefList (tree : Tree) : ElabM (Array TypeRef)

Translate a TypeRefList syntax tree (array of TypeRef)

Equations

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

def StrataDDM.Elab.translateFunctionTemplate (tree : Tree) : ElabM FunctionTemplate

Translate a FunctionTemplate syntax tree to the AST type

Equations

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

partial def StrataDDM.Elab.translateMetadataArg {argc : Nat} (args : ArgDeclsMap argc) (argName : String) (expected : MetadataArgType) (tree : Tree) : ElabM MetadataArg

def StrataDDM.Elab.translateMetadataArgs {argc : Nat} (argDecls : ArgDeclsMap argc) (decl : MetadataDecl) (op : Tree) : ElabM (Array MetadataArg)

Equations

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

def StrataDDM.Elab.translateMetadataAttr {argc : Nat} (args : ArgDeclsMap argc) (t : Tree) : ElabM MetadataAttr

Equations

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

def StrataDDM.Elab.translateMetadata {argc : Nat} (argDecls : ArgDeclsMap argc) (tree : Tree) : ElabM Metadata

This parses an optional metadata

Equations

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

def StrataDDM.Elab.translateOptMetadata {argc : Nat} (argDecls : ArgDeclsMap argc) (tree : Option Tree) : ElabM Metadata

Translate metadata if it is optional.

Equations

• StrataDDM.Elab.translateOptMetadata argDecls none = pure StrataDDM.Metadata.empty
• StrataDDM.Elab.translateOptMetadata argDecls (some tree_2) = StrataDDM.Elab.translateMetadata argDecls tree_2

def StrataDDM.Elab.translateOptMetadata! {argc : Nat} (argDecls : ArgDeclsMap argc) (tree : Tree) : ElabM Metadata

Translate metadata if it is optional.

Equations

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

def StrataDDM.Elab.translateArgDecl {argc : Nat} (argDecls : ArgDeclsMap argc) (t : Tree) : ElabM ArgDeclWithLoc

Equations

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

def StrataDDM.Elab.translateArgDecls (tree : Tree) : ElabM ((argc : Nat) × ArgDeclsMap argc)

Equations

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

partial def StrataDDM.Elab.elabMetadataArgCatType (loc : SourceRange) (cat : SyntaxCat) : DeclM MetadataArgType

inductive StrataDDM.Elab.ArgSetStatus : Type

• implicit : ArgSetStatus
• explicit : ArgSetStatus

def StrataDDM.Elab.checkIdentUsedArgs {argc : Nat} (argDecls : Vector ArgDeclWithLoc argc) (argLevel : Fin argc) : StateT (Std.HashMap Nat ArgSetStatus) ElabM Unit

Equations

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

partial def StrataDDM.Elab.elabSyntaxDefAtom {argc : Nat} (argDecls : ArgDeclsMap argc) (defaultPrec : Nat) (arg : Tree) : StateT (Std.HashMap Nat ArgSetStatus) ElabM SyntaxDefAtom

def StrataDDM.Elab.translateSyntaxDef {argc : Nat} (argDecls : ArgDeclsMap argc) (mdTree tree : Tree) : ElabM SyntaxDef

Equations

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

structure StrataDDM.Elab.DialectContext : Type

• loadDialect : LoadDialectCallback

  Callback to load dialects dynamically upon demand.

• loadedRef : IO.Ref LoadedDialects

  Mutable reference for syncing loaded dialects after callbacks.

• inputContext : Parser.InputContext
• stopPos : String.Pos.Raw

structure StrataDDM.Elab.DialectState : Type

• declState : DeclState
• dialect : Dialect
• missingImport : Bool

  Flag to indicate dialect is missing an import. Missing declarations will be silenced.

@[reducible, inline]

abbrev StrataDDM.Elab.DialectM (α : Type) : Type

Equations

• StrataDDM.Elab.DialectM = ReaderT StrataDDM.Elab.DialectContext (StateRefT' IO.RealWorld StrataDDM.Elab.DialectState BaseIO)

def StrataDDM.Elab.getCurrentDialect : DialectM Dialect

Equations

• StrataDDM.Elab.getCurrentDialect = do let __do_lift ← get pure __do_lift.dialect

def StrataDDM.Elab.getLoadedDialects : DialectM LoadedDialects

Read the current loaded dialects from the IO.Ref.

Equations

• StrataDDM.Elab.getLoadedDialects = do let __do_lift ← read ST.Ref.get __do_lift.loadedRef

@[implicit_reducible]

instance StrataDDM.Elab.instMonadStateDialectStateDialectM : MonadState DialectState DialectM

Equations

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

@[implicit_reducible]

instance StrataDDM.Elab.instMonadLiftDeclMDialectM : MonadLift DeclM DialectM

Equations

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

def StrataDDM.Elab.getDeclState : DialectM DeclState

Equations

• StrataDDM.Elab.getDeclState x✝ = StrataDDM.Elab.DialectState.declState <$> get

def StrataDDM.Elab.modifyDeclState (f : DeclState → DeclState) : DialectM Unit

Equations

• StrataDDM.Elab.modifyDeclState f = modify fun (s : StrataDDM.Elab.DialectState) => { declState := f s.declState, dialect := s.dialect, missingImport := s.missingImport }

def StrataDDM.Elab.modifyDialect (f : Dialect → Dialect) : DialectM Unit

Equations

• StrataDDM.Elab.modifyDialect f x✝ = modify fun (s : StrataDDM.Elab.DialectState) => { declState := s.declState, dialect := f s.dialect, missingImport := s.missingImport }

def StrataDDM.Elab.addDeclToDialect (decl : Decl) : DialectM Unit

Equations

• StrataDDM.Elab.addDeclToDialect decl = StrataDDM.Elab.modifyDialect fun (d : StrataDDM.Dialect) => d.addDecl decl

@[implicit_reducible]

instance StrataDDM.Elab.instElabClassDialectM : ElabClass DialectM

Equations

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

def StrataDDM.Elab.checkTreeSize (tree : Tree) (size : Nat) : Decidable (tree.children.size = size)

Equations

• StrataDDM.Elab.checkTreeSize tree size = inferInstance

@[reducible, inline]

abbrev StrataDDM.Elab.DialectElab : Type

Equations

• StrataDDM.Elab.DialectElab = (StrataDDM.Elab.Tree → StrataDDM.Elab.DialectM Unit)

def StrataDDM.Elab.elabDialectImportCommand : DialectElab

Equations

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

def StrataDDM.Elab.elabOpCommand : DialectElab

Equations

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

def StrataDDM.Elab.elabFnCommand : DialectElab

Equations

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

def StrataDDM.Elab.elabMdCommand : DialectElab

Equations

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

def StrataDDM.Elab.elabSetOptionCommand : DialectElab

Equations

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

def StrataDDM.Elab.dialectElabs : Std.HashMap QualifiedIdent DialectElab

Equations

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

def StrataDDM.Elab.runDialectCommand (leanEnv : Lean.Environment) : DialectM Bool

Equations

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