@[reducible, inline]

abbrev StrataDDM.DialectName : Type

Equations

• StrataDDM.DialectName = String

structure StrataDDM.QualifiedIdent : Type

• dialect : DialectName
• name : String

def StrataDDM.instDecidableEqQualifiedIdent.decEq (x✝ x✝¹ : QualifiedIdent) : Decidable (x✝ = x✝¹)

Equations

• StrataDDM.instDecidableEqQualifiedIdent.decEq { dialect := a, name := a_1 } { dialect := b, name := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance StrataDDM.instDecidableEqQualifiedIdent : DecidableEq QualifiedIdent

Equations

• StrataDDM.instDecidableEqQualifiedIdent = StrataDDM.instDecidableEqQualifiedIdent.decEq

@[implicit_reducible]

instance StrataDDM.instHashableQualifiedIdent : Hashable QualifiedIdent

Equations

• StrataDDM.instHashableQualifiedIdent = { hash := StrataDDM.instHashableQualifiedIdent.hash }

def StrataDDM.instHashableQualifiedIdent.hash : QualifiedIdent → UInt64

Equations

• StrataDDM.instHashableQualifiedIdent.hash { dialect := a, name := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

def StrataDDM.instInhabitedQualifiedIdent.default : QualifiedIdent

Equations

• StrataDDM.instInhabitedQualifiedIdent.default = { dialect := default, name := default }

@[implicit_reducible]

instance StrataDDM.instInhabitedQualifiedIdent : Inhabited QualifiedIdent

Equations

• StrataDDM.instInhabitedQualifiedIdent = { default := StrataDDM.instInhabitedQualifiedIdent.default }

def StrataDDM.instReprQualifiedIdent.repr : QualifiedIdent → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprQualifiedIdent : Repr QualifiedIdent

Equations

• StrataDDM.instReprQualifiedIdent = { reprPrec := StrataDDM.instReprQualifiedIdent.repr }

def StrataDDM.QualifiedIdent.fullName (i : QualifiedIdent) : String

Equations

• i.fullName = toString i.dialect ++ toString "." ++ toString i.name

@[implicit_reducible]

instance StrataDDM.QualifiedIdent.instToString : ToString QualifiedIdent

Equations

• StrataDDM.QualifiedIdent.instToString = { toString := StrataDDM.QualifiedIdent.fullName }

def StrataDDM.QualifiedIdent.ofString (fullname : String) : Option QualifiedIdent

Equations

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

def StrataDDM.QualifiedIdent.quote (i : QualifiedIdent) : Lean.Term

Equations

• i.quote = Lean.Syntax.mkCApp `StrataDDM.QualifiedIdent.mk #[Lean.quote `term i.dialect, Lean.quote `term i.name]

@[implicit_reducible]

instance StrataDDM.QualifiedIdent.instQuoteMkStr1 : Lean.Quote QualifiedIdent

Equations

• StrataDDM.QualifiedIdent.instQuoteMkStr1 = { quote := StrataDDM.QualifiedIdent.quote }

def StrataDDM.QualifiedIdent.quoteIdent : Lean.ParserDescr

Equations

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

def StrataDDM.QualifiedIdent.quoteIdentImpl : Lean.Macro

Equations

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

structure StrataDDM.SyntaxCatF (α : Type) : Type

Denotes a fully specified syntax category in the Strata dialect.

• ann : α
• name : QualifiedIdent
• args : Array (SyntaxCatF α)

partial def StrataDDM.instBEqSyntaxCatF.beq {α✝ : Type} [BEq α✝] : SyntaxCatF α✝ → SyntaxCatF α✝ → Bool

@[implicit_reducible]

instance StrataDDM.instBEqSyntaxCatF {α✝ : Type} [BEq α✝] : BEq (SyntaxCatF α✝)

Equations

• StrataDDM.instBEqSyntaxCatF = { beq := StrataDDM.instBEqSyntaxCatF.beq }

@[implicit_reducible]

instance StrataDDM.instInhabitedSyntaxCatF {a✝ : Type} [Inhabited a✝] : Inhabited (SyntaxCatF a✝)

Equations

• StrataDDM.instInhabitedSyntaxCatF = { default := StrataDDM.instInhabitedSyntaxCatF.default }

def StrataDDM.instInhabitedSyntaxCatF.default {a✝ : Type} [Inhabited a✝] : SyntaxCatF a✝

Equations

• StrataDDM.instInhabitedSyntaxCatF.default = { ann := default, name := default, args := default }

@[implicit_reducible]

instance StrataDDM.instReprSyntaxCatF {α✝ : Type} [Repr α✝] : Repr (SyntaxCatF α✝)

Equations

• StrataDDM.instReprSyntaxCatF = { reprPrec := StrataDDM.instReprSyntaxCatF.repr }

partial def StrataDDM.instReprSyntaxCatF.repr {α✝ : Type} [Repr α✝] : SyntaxCatF α✝ → Nat → Std.Format

def StrataDDM.SyntaxCatF.atom {α : Type} (ann : α) (ident : QualifiedIdent) : SyntaxCatF α

Equations

• StrataDDM.SyntaxCatF.atom ann ident = { ann := ann, name := ident, args := #[] }

def StrataDDM.SyntaxCatF.isType {α : Type} (c : SyntaxCatF α) : Bool

Return true if this corresponds to builtin category Init.Type

Equations

• c.isType = (c.name == { dialect := "Init", name := "Type" })

def StrataDDM.SyntaxCatF.sizeOf_spec {α : Type} [SizeOf α] (op : SyntaxCatF α) : sizeOf op = 1 + sizeOf op.ann + sizeOf op.name + sizeOf op.args

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev StrataDDM.FreeVarIndex : Type

This refers to a value introduced in the program.

Equations

• StrataDDM.FreeVarIndex = Nat

inductive StrataDDM.TypeExprF (α : Type) : Type

An expression that denotes a type.

• ident {α : Type} (ann : α) (name : QualifiedIdent) (args : Array (TypeExprF α)) : TypeExprF α

  A dialect defined type.

• bvar {α : Type} (ann : α) (index : Nat) : TypeExprF α

  A bound type variable at the given deBruijn index in the context.

• tvar {α : Type} (ann : α) (name : String) : TypeExprF α

  A polymorphic type variable (universally quantified). Used for polymorphic function type parameters

• fvar {α : Type} (ann : α) (fvar : FreeVarIndex) (args : Array (TypeExprF α)) : TypeExprF α

  A reference to a global variable along with any arguments to ensure it is well-typed.

• arrow {α : Type} (ann : α) (arg res : TypeExprF α) : TypeExprF α

  A function type.

partial def StrataDDM.instBEqTypeExprF.beq {α✝ : Type} [BEq α✝] : TypeExprF α✝ → TypeExprF α✝ → Bool

@[implicit_reducible]

instance StrataDDM.instBEqTypeExprF {α✝ : Type} [BEq α✝] : BEq (TypeExprF α✝)

Equations

• StrataDDM.instBEqTypeExprF = { beq := StrataDDM.instBEqTypeExprF.beq }

def StrataDDM.instInhabitedTypeExprF.default {a✝ : Type} [Inhabited a✝] : TypeExprF a✝

Equations

• StrataDDM.instInhabitedTypeExprF.default = StrataDDM.TypeExprF.ident default default default

@[implicit_reducible]

instance StrataDDM.instInhabitedTypeExprF {a✝ : Type} [Inhabited a✝] : Inhabited (TypeExprF a✝)

Equations

• StrataDDM.instInhabitedTypeExprF = { default := StrataDDM.instInhabitedTypeExprF.default }

@[implicit_reducible]

instance StrataDDM.instReprTypeExprF {α✝ : Type} [Repr α✝] : Repr (TypeExprF α✝)

Equations

• StrataDDM.instReprTypeExprF = { reprPrec := StrataDDM.instReprTypeExprF.repr }

partial def StrataDDM.instReprTypeExprF.repr {α✝ : Type} [Repr α✝] : TypeExprF α✝ → Nat → Std.Format

def StrataDDM.TypeExprF.placeholder {α : Type} (loc : α) : TypeExprF α

An anonymous type placeholder.

Equations

• StrataDDM.TypeExprF.placeholder loc = StrataDDM.TypeExprF.tvar loc ""

def StrataDDM.TypeExprF.ann {α : Type} : TypeExprF α → α

Equations

• (StrataDDM.TypeExprF.ident a a_1 a_2).ann = a
• (StrataDDM.TypeExprF.bvar a a_1).ann = a
• (StrataDDM.TypeExprF.tvar a a_1).ann = a
• (StrataDDM.TypeExprF.fvar a a_1 a_2).ann = a
• (StrataDDM.TypeExprF.arrow a a_1 a_2).ann = a

def StrataDDM.TypeExprF.mkFunType {α : Type} (n : α) (bindings : Array (String × TypeExprF α)) (res : TypeExprF α) : TypeExprF α

Equations

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

@[irreducible]

def StrataDDM.TypeExprF.incIndices {α : Type} (tp : TypeExprF α) (count : Nat) : TypeExprF α

Equations

• One or more equations did not get rendered due to their size.
• (StrataDDM.TypeExprF.bvar n idx).incIndices count = StrataDDM.TypeExprF.bvar n (idx + count)
• (StrataDDM.TypeExprF.tvar n name).incIndices count = StrataDDM.TypeExprF.tvar n name
• (StrataDDM.TypeExprF.arrow n a r).incIndices count = StrataDDM.TypeExprF.arrow n (a.incIndices count) (r.incIndices count)

@[irreducible]

def StrataDDM.TypeExprF.hasUnboundVar {α : Type} (bindingCount : Nat := 0) : TypeExprF α → Bool

Return true if type expression has a bound variable.

Equations

• One or more equations did not get rendered due to their size.
• StrataDDM.TypeExprF.hasUnboundVar bindingCount (StrataDDM.TypeExprF.bvar n idx) = decide (idx ≥ bindingCount)
• StrataDDM.TypeExprF.hasUnboundVar bindingCount (StrataDDM.TypeExprF.tvar n name) = true
• StrataDDM.TypeExprF.hasUnboundVar bindingCount (StrataDDM.TypeExprF.arrow n a r) = (StrataDDM.TypeExprF.hasUnboundVar bindingCount a || StrataDDM.TypeExprF.hasUnboundVar bindingCount r)

def StrataDDM.TypeExprF.isGround {α : Type} (tp : TypeExprF α) : Bool

Return true if type expression has no free variables.

Equations

• tp.isGround = !StrataDDM.TypeExprF.hasUnboundVar 0 tp

@[irreducible]

def StrataDDM.TypeExprF.instTypeM {m : Type → Type u_1} {α : Type} [Monad m] (d : TypeExprF α) (bindings : α → Nat → m (TypeExprF α)) : m (TypeExprF α)

Applies a transformation to each bound variable in a type expression.

Free type alias variables bound to alias

Equations

• One or more equations did not get rendered due to their size.
• (StrataDDM.TypeExprF.bvar a a_1).instTypeM bindings = bindings a a_1
• (StrataDDM.TypeExprF.tvar a a_1).instTypeM bindings = pure (StrataDDM.TypeExprF.tvar a a_1)
• (StrataDDM.TypeExprF.arrow a a_1 a_2).instTypeM bindings = StrataDDM.TypeExprF.arrow a <$> a_1.instTypeM bindings <*> a_2.instTypeM bindings

@[irreducible, specialize #[]]

def StrataDDM.TypeExprF.mapAnnM {α β : Type} {m : Type → Type u_1} [Monad m] (t : TypeExprF α) (f : α → m β) : m (TypeExprF β)

Monadic map over all annotations in a type expression.

Equations

• One or more equations did not get rendered due to their size.
• (StrataDDM.TypeExprF.bvar a a_1).mapAnnM f = do let __do_lift ← f a pure (StrataDDM.TypeExprF.bvar __do_lift a_1)
• (StrataDDM.TypeExprF.tvar a a_1).mapAnnM f = do let __do_lift ← f a pure (StrataDDM.TypeExprF.tvar __do_lift a_1)

@[specialize #[]]

def StrataDDM.TypeExprF.mapAnn {α β : Type} (t : TypeExprF α) (f : α → β) : TypeExprF β

Map over all annotations in a type expression.

Equations

• t.mapAnn f = t.mapAnnM f

inductive StrataDDM.SepFormat : Type

Separator format for sequence formatting

• none : SepFormat
• comma : SepFormat
• space : SepFormat
• spacePrefix : SepFormat
• newline : SepFormat
• semicolonNewline : SepFormat

@[implicit_reducible]

instance StrataDDM.instInhabitedSepFormat : Inhabited SepFormat

Equations

• StrataDDM.instInhabitedSepFormat = { default := StrataDDM.instInhabitedSepFormat.default }

def StrataDDM.instInhabitedSepFormat.default : SepFormat

Equations

• StrataDDM.instInhabitedSepFormat.default = StrataDDM.SepFormat.none

@[implicit_reducible]

instance StrataDDM.instReprSepFormat : Repr SepFormat

Equations

• StrataDDM.instReprSepFormat = { reprPrec := StrataDDM.instReprSepFormat.repr }

def StrataDDM.instReprSepFormat.repr : SepFormat → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• StrataDDM.instReprSepFormat.repr StrataDDM.SepFormat.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "StrataDDM.SepFormat.none")).group prec✝
• StrataDDM.instReprSepFormat.repr StrataDDM.SepFormat.comma prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "StrataDDM.SepFormat.comma")).group prec✝
• StrataDDM.instReprSepFormat.repr StrataDDM.SepFormat.space prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "StrataDDM.SepFormat.space")).group prec✝

@[implicit_reducible]

instance StrataDDM.instBEqSepFormat : BEq SepFormat

Equations

• StrataDDM.instBEqSepFormat = { beq := StrataDDM.instBEqSepFormat.beq }

def StrataDDM.instBEqSepFormat.beq : SepFormat → SepFormat → Bool

Equations

• StrataDDM.instBEqSepFormat.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def StrataDDM.SepFormat.toString : SepFormat → String

Equations

• StrataDDM.SepFormat.none.toString = "seq"
• StrataDDM.SepFormat.comma.toString = "commaSepBy"
• StrataDDM.SepFormat.space.toString = "spaceSepBy"
• StrataDDM.SepFormat.spacePrefix.toString = "spacePrefixSepBy"
• StrataDDM.SepFormat.newline.toString = "newlineSepBy"
• StrataDDM.SepFormat.semicolonNewline.toString = "semicolonSepBy"

def StrataDDM.SepFormat.fromCategoryName? : QualifiedIdent → Option SepFormat

Equations

• StrataDDM.SepFormat.fromCategoryName? { dialect := "Init", name := "Seq" } = some StrataDDM.SepFormat.none
• StrataDDM.SepFormat.fromCategoryName? { dialect := "Init", name := "CommaSepBy" } = some StrataDDM.SepFormat.comma
• StrataDDM.SepFormat.fromCategoryName? { dialect := "Init", name := "SpaceSepBy" } = some StrataDDM.SepFormat.space
• StrataDDM.SepFormat.fromCategoryName? { dialect := "Init", name := "SpacePrefixSepBy" } = some StrataDDM.SepFormat.spacePrefix
• StrataDDM.SepFormat.fromCategoryName? { dialect := "Init", name := "NewlineSepBy" } = some StrataDDM.SepFormat.newline
• StrataDDM.SepFormat.fromCategoryName? { dialect := "Init", name := "SemicolonSepBy" } = some StrataDDM.SepFormat.semicolonNewline
• StrataDDM.SepFormat.fromCategoryName? x✝ = none

def StrataDDM.SepFormat.isParametricCategory (name : QualifiedIdent) : Bool

Returns true if the category name is a parametric (single-argument) built-in category: any separator format or Init.Option.

Equations

• StrataDDM.SepFormat.isParametricCategory name = ((StrataDDM.SepFormat.fromCategoryName? name).isSome || name == { dialect := "Init", name := "Option" })

@[implicit_reducible]

instance StrataDDM.SepFormat.instToString : ToString SepFormat

Equations

• StrataDDM.SepFormat.instToString = { toString := StrataDDM.SepFormat.toString }

inductive StrataDDM.ExprF (α : Type) : Type

• bvar {α : Type} (ann : α) (idx : Nat) : ExprF α

  A bound variable reference (de Bruijn index).

  If this is a function, then the arguments are always value-level; type arguments are omitted.

• fvar {α : Type} (ann : α) (idx : FreeVarIndex) : ExprF α

  A free variable reference.

  If this is a function, then the arguments are always value-level; type arguments are omitted.

• fn {α : Type} (ann : α) (ident : QualifiedIdent) : ExprF α

  A named dialect function.

• app {α : Type} (ann : α) (e : ExprF α) (a : ArgF α) : ExprF α

  Function application.

@[implicit_reducible]

instance StrataDDM.instInhabitedOperationF {a✝ : Type} [Inhabited a✝] : Inhabited (OperationF a✝)

Equations

• StrataDDM.instInhabitedOperationF = { default := StrataDDM.instInhabitedOperationF.default_1 }

@[implicit_reducible]

instance StrataDDM.instInhabitedArgF {a✝ : Type} [Inhabited a✝] : Inhabited (ArgF a✝)

Equations

• StrataDDM.instInhabitedArgF = { default := StrataDDM.instInhabitedArgF.default_1 }

def StrataDDM.instInhabitedArgF.default_1 {a✝ : Type} [Inhabited a✝] : ArgF a✝

Equations

• StrataDDM.instInhabitedArgF.default_1 = StrataDDM.ArgF.op default

def StrataDDM.instInhabitedExprF.default_1 {a✝ : Type} [Inhabited a✝] : ExprF a✝

Equations

• StrataDDM.instInhabitedExprF.default_1 = StrataDDM.ExprF.bvar default default

@[implicit_reducible]

instance StrataDDM.instInhabitedExprF {a✝ : Type} [Inhabited a✝] : Inhabited (ExprF a✝)

Equations

• StrataDDM.instInhabitedExprF = { default := StrataDDM.instInhabitedExprF.default_1 }

def StrataDDM.instInhabitedOperationF.default_1 {a✝ : Type} [Inhabited a✝] : OperationF a✝

Equations

• StrataDDM.instInhabitedOperationF.default_1 = { ann := default, name := default, args := default }

partial def StrataDDM.instReprArgF.repr_3 {α✝ : Type} [Repr α✝] : ArgF α✝ → Nat → Std.Format

partial def StrataDDM.instReprArgF.repr_1 {α✝ : Type} [Repr α✝] : ExprF α✝ → Nat → Std.Format

partial def StrataDDM.instReprOperationF.repr_2 {α✝ : Type} [Repr α✝] : OperationF α✝ → Nat → Std.Format

partial def StrataDDM.instReprArgF.repr_2 {α✝ : Type} [Repr α✝] : OperationF α✝ → Nat → Std.Format

partial def StrataDDM.instReprExprF.repr_3 {α✝ : Type} [Repr α✝] : ArgF α✝ → Nat → Std.Format

@[implicit_reducible]

instance StrataDDM.instReprOperationF {α✝ : Type} [Repr α✝] : Repr (OperationF α✝)

Equations

• StrataDDM.instReprOperationF = { reprPrec := StrataDDM.instReprOperationF.repr_2 }

@[implicit_reducible]

instance StrataDDM.instReprArgF {α✝ : Type} [Repr α✝] : Repr (ArgF α✝)

Equations

• StrataDDM.instReprArgF = { reprPrec := StrataDDM.instReprArgF.repr_3 }

partial def StrataDDM.instReprOperationF.repr_3 {α✝ : Type} [Repr α✝] : ArgF α✝ → Nat → Std.Format

@[implicit_reducible]

instance StrataDDM.instReprExprF {α✝ : Type} [Repr α✝] : Repr (ExprF α✝)

Equations

• StrataDDM.instReprExprF = { reprPrec := StrataDDM.instReprExprF.repr_1 }

partial def StrataDDM.instReprExprF.repr_1 {α✝ : Type} [Repr α✝] : ExprF α✝ → Nat → Std.Format

partial def StrataDDM.instReprOperationF.repr_1 {α✝ : Type} [Repr α✝] : ExprF α✝ → Nat → Std.Format

partial def StrataDDM.instReprExprF.repr_2 {α✝ : Type} [Repr α✝] : OperationF α✝ → Nat → Std.Format

structure StrataDDM.OperationF (α : Type) : Type

• ann : α
• name : QualifiedIdent
• args : Array (ArgF α)

inductive StrataDDM.ArgF (α : Type) : Type

• op {α : Type} (o : OperationF α) : ArgF α
• cat {α : Type} (c : SyntaxCatF α) : ArgF α
• expr {α : Type} (e : ExprF α) : ArgF α
• type {α : Type} (e : TypeExprF α) : ArgF α
• ident {α : Type} (ann : α) (i : String) : ArgF α
• num {α : Type} (ann : α) (v : Nat) : ArgF α
• decimal {α : Type} (ann : α) (v : Decimal) : ArgF α
• strlit {α : Type} (ann : α) (i : String) : ArgF α
• bytes {α : Type} (ann : α) (a : ByteArray) : ArgF α
• option {α : Type} (ann : α) (l : Option (ArgF α)) : ArgF α
• seq {α : Type} (ann : α) (sep : SepFormat) (l : Array (ArgF α)) : ArgF α

def StrataDDM.ExprF.ann {α : Type} : ExprF α → α

Equations

• (StrataDDM.ExprF.bvar a a_1).ann = a
• (StrataDDM.ExprF.fvar a a_1).ann = a
• (StrataDDM.ExprF.fn a a_1).ann = a
• (StrataDDM.ExprF.app a a_1 a_2).ann = a

def StrataDDM.ArgF.ann {α : Type} : ArgF α → α

Equations

• (StrataDDM.ArgF.op o).ann = o.ann
• (StrataDDM.ArgF.cat c).ann = c.ann
• (StrataDDM.ArgF.expr e).ann = e.ann
• (StrataDDM.ArgF.type t).ann = t.ann
• (StrataDDM.ArgF.ident ann i).ann = ann
• (StrataDDM.ArgF.num ann v).ann = ann
• (StrataDDM.ArgF.decimal ann v).ann = ann
• (StrataDDM.ArgF.bytes ann a).ann = ann
• (StrataDDM.ArgF.strlit ann i).ann = ann
• (StrataDDM.ArgF.option ann l).ann = ann
• (StrataDDM.ArgF.seq ann sep l).ann = ann

theorem StrataDDM.OperationF.sizeOf_spec {α : Type} [SizeOf α] (op : OperationF α) : sizeOf op = 1 + sizeOf op.ann + sizeOf op.name + sizeOf op.args

def StrataDDM.ExprF.flatten {α : Type} (e : ExprF α) (prev : List (ArgF α) := []) : ExprF α × List (ArgF α)

Flattens a curried application expression into its head and list of arguments. For example, ((f a) b) c becomes (f, [a, b, c]).

Equations

• (StrataDDM.ExprF.app ann f e_2).flatten prev = f.flatten (e_2 :: prev)
• e.flatten prev = (e, prev)

@[irreducible, specialize #[]]

def StrataDDM.SyntaxCatF.mapAnnM {α β : Type} {m : Type → Type u_1} [Monad m] (c : SyntaxCatF α) (f : α → m β) : m (SyntaxCatF β)

Monadic map over all annotations in a syntax category.

Equations

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

@[specialize #[]]

def StrataDDM.SyntaxCatF.mapAnn {α β : Type} (c : SyntaxCatF α) (f : α → β) : SyntaxCatF β

Map over all annotations in a syntax category.

Equations

• c.mapAnn f = c.mapAnnM f

@[irreducible, specialize #[]]

def StrataDDM.ExprF.mapAnnM {α β : Type} {m : Type → Type u_1} [Monad m] (e : ExprF α) (f : α → m β) : m (ExprF β)

Monadic map over all annotations in an expression.

Equations

• (StrataDDM.ExprF.bvar a a_1).mapAnnM f = do let __do_lift ← f a pure (StrataDDM.ExprF.bvar __do_lift a_1)
• (StrataDDM.ExprF.fvar a a_1).mapAnnM f = do let __do_lift ← f a pure (StrataDDM.ExprF.fvar __do_lift a_1)
• (StrataDDM.ExprF.fn a a_1).mapAnnM f = do let __do_lift ← f a pure (StrataDDM.ExprF.fn __do_lift a_1)
• (StrataDDM.ExprF.app a a_1 a_2).mapAnnM f = do let __do_lift ← f a let __do_lift_1 ← a_1.mapAnnM f let __do_lift_2 ← a_2.mapAnnM f pure (StrataDDM.ExprF.app __do_lift __do_lift_1 __do_lift_2)

@[irreducible, specialize #[]]

def StrataDDM.ArgF.mapAnnM {α β : Type} {m : Type → Type u_1} [Monad m] (a : ArgF α) (f : α → m β) : m (ArgF β)

Monadic map over all annotations in an argument.

Equations

• One or more equations did not get rendered due to their size.
• (StrataDDM.ArgF.op o).mapAnnM f = do let __do_lift ← o.mapAnnM f pure (StrataDDM.ArgF.op __do_lift)
• (StrataDDM.ArgF.cat c).mapAnnM f = do let __do_lift ← c.mapAnnM f pure (StrataDDM.ArgF.cat __do_lift)
• (StrataDDM.ArgF.expr e).mapAnnM f = do let __do_lift ← e.mapAnnM f pure (StrataDDM.ArgF.expr __do_lift)
• (StrataDDM.ArgF.type t).mapAnnM f = do let __do_lift ← t.mapAnnM f pure (StrataDDM.ArgF.type __do_lift)
• (StrataDDM.ArgF.ident ann i).mapAnnM f = do let __do_lift ← f ann pure (StrataDDM.ArgF.ident __do_lift i)
• (StrataDDM.ArgF.num ann v).mapAnnM f = do let __do_lift ← f ann pure (StrataDDM.ArgF.num __do_lift v)
• (StrataDDM.ArgF.decimal ann v).mapAnnM f = do let __do_lift ← f ann pure (StrataDDM.ArgF.decimal __do_lift v)
• (StrataDDM.ArgF.strlit ann i).mapAnnM f = do let __do_lift ← f ann pure (StrataDDM.ArgF.strlit __do_lift i)
• (StrataDDM.ArgF.bytes ann b).mapAnnM f = do let __do_lift ← f ann pure (StrataDDM.ArgF.bytes __do_lift b)
• (StrataDDM.ArgF.option ann none).mapAnnM f = do let __do_lift ← f ann pure (StrataDDM.ArgF.option __do_lift none)
• (StrataDDM.ArgF.option ann (some a_2)).mapAnnM f = do let __do_lift ← f ann let __do_lift_1 ← a_2.mapAnnM f pure (StrataDDM.ArgF.option __do_lift (some __do_lift_1))

@[irreducible, specialize #[]]

def StrataDDM.OperationF.mapAnnM {α β : Type} {m : Type → Type u_1} [Monad m] (op : OperationF α) (f : α → m β) : m (OperationF β)

Map a monadic function over all annotations in an operation.

Equations

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

@[specialize #[]]

def StrataDDM.ExprF.mapAnn {α β : Type} (e : ExprF α) (f : α → β) : ExprF β

Map a pure function over all annotations in an expression.

Equations

• e.mapAnn f = e.mapAnnM f

@[specialize #[]]

def StrataDDM.ArgF.mapAnn {α β : Type} (a : ArgF α) (f : α → β) : ArgF β

Map a pure function over all annotations in an argument.

Equations

• a.mapAnn f = a.mapAnnM f

@[specialize #[]]

def StrataDDM.OperationF.mapAnn {α β : Type} (op : OperationF α) (f : α → β) : OperationF β

Map a pure function over all annotations in an operation.

Equations

• op.mapAnn f = op.mapAnnM f

@[reducible, inline]

abbrev StrataDDM.Arg : Type

Equations

• StrataDDM.Arg = StrataDDM.ArgF StrataDDM.SourceRange

@[reducible, inline]

abbrev StrataDDM.Expr : Type

Equations

• StrataDDM.Expr = StrataDDM.ExprF StrataDDM.SourceRange

@[reducible, inline]

abbrev StrataDDM.Operation : Type

Equations

• StrataDDM.Operation = StrataDDM.OperationF StrataDDM.SourceRange

@[reducible, inline]

abbrev StrataDDM.SyntaxCat : Type

Equations

• StrataDDM.SyntaxCat = StrataDDM.SyntaxCatF StrataDDM.SourceRange

@[reducible, inline]

abbrev StrataDDM.TypeExpr : Type

Equations

• StrataDDM.TypeExpr = StrataDDM.TypeExprF StrataDDM.SourceRange

@[implicit_reducible]

instance StrataDDM.instBEqExprF {α : Type} [BEq α] : BEq (ExprF α)

Equations

• StrataDDM.instBEqExprF = { beq := StrataDDM.instBEqExprF._private_1 }

@[implicit_reducible]

instance StrataDDM.instBEqOperationF {α : Type} [BEq α] : BEq (OperationF α)

Equations

• StrataDDM.instBEqOperationF = { beq := StrataDDM.instBEqOperationF._private_1 }

@[implicit_reducible]

instance StrataDDM.instBEqArgF {α : Type} [BEq α] : BEq (ArgF α)

Equations

• StrataDDM.instBEqArgF = { beq := StrataDDM.instBEqArgF._private_1 }

inductive StrataDDM.MetadataArg : Type

• bool (e : Bool) : MetadataArg
• catbvar (index : Nat) : MetadataArg
• num (e : Nat) : MetadataArg
• option (a : Option MetadataArg) : MetadataArg
• functionTemplate (t : FunctionTemplate) : MetadataArg

@[implicit_reducible]

instance StrataDDM.instBEqMetadataArg : BEq MetadataArg

Equations

• StrataDDM.instBEqMetadataArg = { beq := StrataDDM.instBEqMetadataArg.beq }

partial def StrataDDM.instBEqMetadataArg.beq : MetadataArg → MetadataArg → Bool

@[implicit_reducible]

instance StrataDDM.instInhabitedMetadataArg : Inhabited MetadataArg

Equations

• StrataDDM.instInhabitedMetadataArg = { default := StrataDDM.instInhabitedMetadataArg.default }

def StrataDDM.instInhabitedMetadataArg.default : MetadataArg

Equations

• StrataDDM.instInhabitedMetadataArg.default = StrataDDM.MetadataArg.bool default

partial def StrataDDM.instReprMetadataArg.repr : MetadataArg → Nat → Std.Format

@[implicit_reducible]

instance StrataDDM.instReprMetadataArg : Repr MetadataArg

Equations

• StrataDDM.instReprMetadataArg = { reprPrec := StrataDDM.instReprMetadataArg.repr }

def StrataDDM.MetadataArg.instDecidableEq (x y : MetadataArg) : Decidable (x = y)

Equations

• (StrataDDM.MetadataArg.bool a).instDecidableEq (StrataDDM.MetadataArg.bool a_1) = if p : a = a_1 then isTrue ⋯ else isFalse ⋯
• (StrataDDM.MetadataArg.bool a).instDecidableEq (StrataDDM.MetadataArg.catbvar a_1) = isFalse ⋯
• (StrataDDM.MetadataArg.bool a).instDecidableEq (StrataDDM.MetadataArg.num a_1) = isFalse ⋯
• (StrataDDM.MetadataArg.bool a).instDecidableEq (StrataDDM.MetadataArg.option a_1) = isFalse ⋯
• (StrataDDM.MetadataArg.bool a).instDecidableEq (StrataDDM.MetadataArg.functionTemplate a_1) = isFalse ⋯
• (StrataDDM.MetadataArg.catbvar a).instDecidableEq (StrataDDM.MetadataArg.catbvar y_2) = if p : a = y_2 then isTrue ⋯ else isFalse ⋯
• (StrataDDM.MetadataArg.catbvar a).instDecidableEq (StrataDDM.MetadataArg.bool e) = isFalse ⋯
• (StrataDDM.MetadataArg.catbvar a).instDecidableEq (StrataDDM.MetadataArg.num e) = isFalse ⋯
• (StrataDDM.MetadataArg.catbvar a).instDecidableEq (StrataDDM.MetadataArg.option a_1) = isFalse ⋯
• (StrataDDM.MetadataArg.catbvar a).instDecidableEq (StrataDDM.MetadataArg.functionTemplate t) = isFalse ⋯
• (StrataDDM.MetadataArg.num a).instDecidableEq (StrataDDM.MetadataArg.num y_2) = if p : a = y_2 then isTrue ⋯ else isFalse ⋯
• (StrataDDM.MetadataArg.num a).instDecidableEq (StrataDDM.MetadataArg.bool e) = isFalse ⋯
• (StrataDDM.MetadataArg.num a).instDecidableEq (StrataDDM.MetadataArg.catbvar index) = isFalse ⋯
• (StrataDDM.MetadataArg.num a).instDecidableEq (StrataDDM.MetadataArg.option a_1) = isFalse ⋯
• (StrataDDM.MetadataArg.num a).instDecidableEq (StrataDDM.MetadataArg.functionTemplate t) = isFalse ⋯
• (StrataDDM.MetadataArg.option none).instDecidableEq (StrataDDM.MetadataArg.option none) = isTrue StrataDDM.MetadataArg.instDecidableEq._proof_28✝
• (StrataDDM.MetadataArg.option (some x_2)).instDecidableEq (StrataDDM.MetadataArg.option (some y_3)) = match x_2.instDecidableEq y_3 with | isTrue p => isTrue ⋯ | isFalse p => isFalse ⋯
• (StrataDDM.MetadataArg.option none).instDecidableEq (StrataDDM.MetadataArg.option (some val)) = isFalse ⋯
• (StrataDDM.MetadataArg.option (some val)).instDecidableEq (StrataDDM.MetadataArg.option none) = isFalse ⋯
• (StrataDDM.MetadataArg.option a).instDecidableEq (StrataDDM.MetadataArg.bool e) = isFalse ⋯
• (StrataDDM.MetadataArg.option a).instDecidableEq (StrataDDM.MetadataArg.catbvar index) = isFalse ⋯
• (StrataDDM.MetadataArg.option a).instDecidableEq (StrataDDM.MetadataArg.num e) = isFalse ⋯
• (StrataDDM.MetadataArg.option a).instDecidableEq (StrataDDM.MetadataArg.functionTemplate t) = isFalse ⋯
• (StrataDDM.MetadataArg.functionTemplate a).instDecidableEq (StrataDDM.MetadataArg.functionTemplate y_2) = if p : a = y_2 then isTrue ⋯ else isFalse ⋯
• (StrataDDM.MetadataArg.functionTemplate a).instDecidableEq (StrataDDM.MetadataArg.bool e) = isFalse ⋯
• (StrataDDM.MetadataArg.functionTemplate a).instDecidableEq (StrataDDM.MetadataArg.catbvar index) = isFalse ⋯
• (StrataDDM.MetadataArg.functionTemplate a).instDecidableEq (StrataDDM.MetadataArg.num e) = isFalse ⋯
• (StrataDDM.MetadataArg.functionTemplate a).instDecidableEq (StrataDDM.MetadataArg.option a_1) = isFalse ⋯

@[implicit_reducible]

instance StrataDDM.MetadataArg.instDecidableEq_1 : DecidableEq MetadataArg

Equations

• StrataDDM.MetadataArg.instDecidableEq_1 = StrataDDM.MetadataArg.instDecidableEq

structure StrataDDM.MetadataAttr : Type

• ident : QualifiedIdent
• args : Array MetadataArg

def StrataDDM.instDecidableEqMetadataAttr.decEq (x✝ x✝¹ : MetadataAttr) : Decidable (x✝ = x✝¹)

Equations

• StrataDDM.instDecidableEqMetadataAttr.decEq { ident := a, args := a_1 } { ident := b, args := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance StrataDDM.instDecidableEqMetadataAttr : DecidableEq MetadataAttr

Equations

• StrataDDM.instDecidableEqMetadataAttr = StrataDDM.instDecidableEqMetadataAttr.decEq

def StrataDDM.instInhabitedMetadataAttr.default : MetadataAttr

Equations

• StrataDDM.instInhabitedMetadataAttr.default = { ident := default, args := default }

@[implicit_reducible]

instance StrataDDM.instInhabitedMetadataAttr : Inhabited MetadataAttr

Equations

• StrataDDM.instInhabitedMetadataAttr = { default := StrataDDM.instInhabitedMetadataAttr.default }

@[implicit_reducible]

instance StrataDDM.instReprMetadataAttr : Repr MetadataAttr

Equations

• StrataDDM.instReprMetadataAttr = { reprPrec := StrataDDM.instReprMetadataAttr.repr }

def StrataDDM.instReprMetadataAttr.repr : MetadataAttr → Nat → Std.Format

Equations

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

def StrataDDM.MetadataAttr.scope (idx : Nat) : MetadataAttr

Create scope using deBrujin index of environment.

Equations

• StrataDDM.MetadataAttr.scope idx = { ident := StrataDDM.MetadataAttr.scopeName✝, args := #[StrataDDM.MetadataArg.catbvar idx] }

structure StrataDDM.Metadata : Type

• ofArray :: (
• toArray : Array MetadataAttr
• )

def StrataDDM.instDecidableEqMetadata.decEq (x✝ x✝¹ : Metadata) : Decidable (x✝ = x✝¹)

Equations

• StrataDDM.instDecidableEqMetadata.decEq { toArray := a } { toArray := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance StrataDDM.instDecidableEqMetadata : DecidableEq Metadata

Equations

• StrataDDM.instDecidableEqMetadata = StrataDDM.instDecidableEqMetadata.decEq

@[implicit_reducible]

instance StrataDDM.instReprMetadata : Repr Metadata

Equations

• StrataDDM.instReprMetadata = { reprPrec := StrataDDM.instReprMetadata.repr }

def StrataDDM.instReprMetadata.repr : Metadata → Nat → Std.Format

Equations

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

def StrataDDM.Metadata.emptyWithCapacity (c : Nat) : Metadata

Equations

• StrataDDM.Metadata.emptyWithCapacity c = { toArray := Array.emptyWithCapacity c }

def StrataDDM.Metadata.empty : Metadata

Equations

• StrataDDM.Metadata.empty = StrataDDM.Metadata.emptyWithCapacity 0

@[implicit_reducible]

instance StrataDDM.Metadata.instEmptyCollection : EmptyCollection Metadata

Equations

• StrataDDM.Metadata.instEmptyCollection = { emptyCollection := StrataDDM.Metadata.empty }

def StrataDDM.Metadata.push (md : Metadata) (attr : MetadataAttr) : Metadata

Equations

• md.push attr = { toArray := md.toArray.push attr }

@[implicit_reducible]

instance StrataDDM.Metadata.instInhabited : Inhabited Metadata

Equations

• StrataDDM.Metadata.instInhabited = { default := ∅ }

def StrataDDM.Metadata.isEmpty (md : Metadata) : Bool

Equations

• md.isEmpty = md.toArray.isEmpty

def StrataDDM.Metadata.toList (m : Metadata) : List MetadataAttr

Equations

• m.toList = m.toArray.toList

@[implicit_reducible]

instance StrataDDM.Metadata.instMembershipQualifiedIdent : Membership QualifiedIdent Metadata

Equations

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

@[implicit_reducible]

instance StrataDDM.Metadata.instDecidableMem (x : QualifiedIdent) (md : Metadata) : Decidable (x ∈ md)

Equations

• StrataDDM.Metadata.instDecidableMem x md = inferInstance

@[implicit_reducible]

instance StrataDDM.Metadata.instGetElem?QualifiedIdentArrayMetadataArgMem : GetElem? Metadata QualifiedIdent (Array MetadataArg) fun (md : Metadata) (i : QualifiedIdent) => i ∈ md

Equations

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

def StrataDDM.Metadata.scopeTVarIndex (metadata : Metadata) : Except String (Option Nat)

Returns the typeParams index if @[scopeTVar] is present. Converts .type bindings from typeParams into .tvar bindings for constructor elaboration.

Equations

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

def StrataDDM.Metadata.declareTVarIndex (metadata : Metadata) : Except String (Option Nat)

Returns the name index if @[declareTVar] is present. Used for operations that introduce a type variable (creates .tvar binding in result context).

Equations

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

def StrataDDM.Metadata.resultLevel (varCount : Nat) (metadata : Metadata) : Except String (Option (Fin varCount))

Returns the index of the value in the binding for the given variable of the scope to use.

Equations

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

def StrataDDM.Metadata.preRegisterTypesIndex (metadata : Metadata) : Except String (Option Nat)

Returns the argument index from @[preRegisterTypes] metadata, if present.

Equations

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

def StrataDDM.Metadata.preRegisterTypesLevel (varCount : Nat) (metadata : Metadata) : Except String (Option (Fin varCount))

Returns the level for @[preRegisterTypes] metadata, if present.

Equations

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

def StrataDDM.Metadata.preRegisterFunctionsIndex (metadata : Metadata) : Except String (Option Nat)

Returns the argument index from @[preRegisterFunctions] metadata, if present.

Equations

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

def StrataDDM.Metadata.preRegisterFunctionsLevel (varCount : Nat) (metadata : Metadata) : Except String (Option (Fin varCount))

Returns the level for @[preRegisterFunctions] metadata, if present.

Equations

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

@[reducible, inline]

abbrev StrataDDM.Var : Type

Equations

• StrataDDM.Var = String

inductive StrataDDM.PreType : Type

PreTypes are partially resolved types that may depend on values applied to other arguments. These need to be resolved to generate types.

• ident (ann : SourceRange) (name : QualifiedIdent) (args : Array PreType) : PreType

  A dialect defined type.

• bvar (ann : SourceRange) (index : Nat) : PreType

  A bound type variable at the given deBruijn index in the context. Used for type alias parameters

• tvar (ann : SourceRange) (name : String) : PreType

  A polymorphic type variable (universally quantified). Used for polymorphic function type parameters

• arrow (ann : SourceRange) (arg res : PreType) : PreType

  A function type.

• funMacro (ann : SourceRange) (bindingsIndex : Nat) (res : PreType) : PreType

  A function created from a reference to bindings and a result type.

@[implicit_reducible]

instance StrataDDM.instBEqPreType : BEq PreType

Equations

• StrataDDM.instBEqPreType = { beq := StrataDDM.instBEqPreType.beq }

partial def StrataDDM.instBEqPreType.beq : PreType → PreType → Bool

def StrataDDM.instInhabitedPreType.default : PreType

Equations

• StrataDDM.instInhabitedPreType.default = StrataDDM.PreType.ident default default default

@[implicit_reducible]

instance StrataDDM.instInhabitedPreType : Inhabited PreType

Equations

• StrataDDM.instInhabitedPreType = { default := StrataDDM.instInhabitedPreType.default }

@[implicit_reducible]

instance StrataDDM.instReprPreType : Repr PreType

Equations

• StrataDDM.instReprPreType = { reprPrec := StrataDDM.instReprPreType.repr }

partial def StrataDDM.instReprPreType.repr : PreType → Nat → Std.Format

def StrataDDM.PreType.ann : PreType → SourceRange

Return annotation on pretype.

Equations

• (StrataDDM.PreType.ident a a_1 a_2).ann = a
• (StrataDDM.PreType.bvar a a_1).ann = a
• (StrataDDM.PreType.tvar a a_1).ann = a
• (StrataDDM.PreType.arrow a a_1 a_2).ann = a
• (StrataDDM.PreType.funMacro a a_1 a_2).ann = a

def StrataDDM.maxPrec : Nat

Equations

• StrataDDM.maxPrec = 1024

def StrataDDM.callPrec : Nat

Precedence of an explicit function call f(..).

This specifically addresses the priority between f and the open paren.

Equations

• StrataDDM.callPrec = 200

def StrataDDM.appPrec : Nat

Precedence of the empty application operator f x in expressions and types.

Equations

• StrataDDM.appPrec = 20

def StrataDDM.arrowPrec : Nat

Precedence of the arrow operator t -> u in types.

Equations

• StrataDDM.arrowPrec = 17

inductive StrataDDM.SyntaxDefAtom : Type

A token in a syntax definition.

• ident (level prec : Nat) : SyntaxDefAtom

  Argument reference. Parenthesizes when the argument's precedence is ≤ prec; prec = 0 disables parenthesization.

• str (lit : String) : SyntaxDefAtom

  Literal string token.

• indent (n : Nat) (args : Array SyntaxDefAtom) : SyntaxDefAtom

  Indented block of tokens.

@[implicit_reducible]

instance StrataDDM.instBEqSyntaxDefAtom : BEq SyntaxDefAtom

Equations

• StrataDDM.instBEqSyntaxDefAtom = { beq := StrataDDM.instBEqSyntaxDefAtom.beq }

partial def StrataDDM.instBEqSyntaxDefAtom.beq : SyntaxDefAtom → SyntaxDefAtom → Bool

@[implicit_reducible]

instance StrataDDM.instInhabitedSyntaxDefAtom : Inhabited SyntaxDefAtom

Equations

• StrataDDM.instInhabitedSyntaxDefAtom = { default := StrataDDM.instInhabitedSyntaxDefAtom.default }

def StrataDDM.instInhabitedSyntaxDefAtom.default : SyntaxDefAtom

Equations

• StrataDDM.instInhabitedSyntaxDefAtom.default = StrataDDM.SyntaxDefAtom.ident default default

@[implicit_reducible]

instance StrataDDM.instReprSyntaxDefAtom : Repr SyntaxDefAtom

Equations

• StrataDDM.instReprSyntaxDefAtom = { reprPrec := StrataDDM.instReprSyntaxDefAtom.repr }

partial def StrataDDM.instReprSyntaxDefAtom.repr : SyntaxDefAtom → Nat → Std.Format

inductive StrataDDM.SyntaxDef : Type

Syntax definition for an operator or function.

• std (atoms : Array SyntaxDefAtom) (prec : Nat) : SyntaxDef

  Standard syntax with explicit atoms and precedence.

• passthrough : SyntaxDef

  Single-argument syntax that inherits the argument's precedence.

def StrataDDM.instBEqSyntaxDef.beq : SyntaxDef → SyntaxDef → Bool

Equations

• StrataDDM.instBEqSyntaxDef.beq (StrataDDM.SyntaxDef.std a a_1) (StrataDDM.SyntaxDef.std b b_1) = (a == b && a_1 == b_1)
• StrataDDM.instBEqSyntaxDef.beq StrataDDM.SyntaxDef.passthrough StrataDDM.SyntaxDef.passthrough = true
• StrataDDM.instBEqSyntaxDef.beq x✝¹ x✝ = false

@[implicit_reducible]

instance StrataDDM.instBEqSyntaxDef : BEq SyntaxDef

Equations

• StrataDDM.instBEqSyntaxDef = { beq := StrataDDM.instBEqSyntaxDef.beq }

@[implicit_reducible]

instance StrataDDM.instReprSyntaxDef : Repr SyntaxDef

Equations

• StrataDDM.instReprSyntaxDef = { reprPrec := StrataDDM.instReprSyntaxDef.repr }

def StrataDDM.instReprSyntaxDef.repr : SyntaxDef → Nat → Std.Format

Equations

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

def StrataDDM.instInhabitedSyntaxDef.default : SyntaxDef

Equations

• StrataDDM.instInhabitedSyntaxDef.default = StrataDDM.SyntaxDef.std default default

@[implicit_reducible]

instance StrataDDM.instInhabitedSyntaxDef : Inhabited SyntaxDef

Equations

• StrataDDM.instInhabitedSyntaxDef = { default := StrataDDM.instInhabitedSyntaxDef.default }

def StrataDDM.SyntaxDef.mkFunApp (name : String) (n : Nat) : SyntaxDef

Creates syntax of the form name(arg1, ..., argn).

If n is 0, then this is just name.

Equations

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

def StrataDDM.SyntaxDef.ofList (atoms : List SyntaxDefAtom) (prec : Nat := maxPrec) : SyntaxDef

Equations

• StrataDDM.SyntaxDef.ofList atoms prec = StrataDDM.SyntaxDef.std atoms.toArray prec

structure StrataDDM.DebruijnIndex (n : Nat) : Type

• val : Nat
• isLt : self.val < n

def StrataDDM.instReprDebruijnIndex.repr {n✝ : Nat} : DebruijnIndex n✝ → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprDebruijnIndex {n✝ : Nat} : Repr (DebruijnIndex n✝)

Equations

• StrataDDM.instReprDebruijnIndex = { reprPrec := StrataDDM.instReprDebruijnIndex.repr }

def StrataDDM.DebruijnIndex.toLevel {n : Nat} : DebruijnIndex n → Fin n

Equations

• { val := v, isLt := lt }.toLevel = ⟨n - (v + 1), ⋯⟩

def StrataDDM.DebruijnIndex.ofNat {n : Nat} [NeZero n] (a : Nat) : DebruijnIndex n

Equations

• StrataDDM.DebruijnIndex.ofNat a = { val := a % n, isLt := ⋯ }

inductive StrataDDM.ArgDeclKind : Type

This is the type information for an operator or function declaration.

• type (tp : PreType) : ArgDeclKind

  Variable is an expression with the given type.

• cat (k : SyntaxCat) : ArgDeclKind

  Variable belongs to the particular category

def StrataDDM.instBEqArgDeclKind.beq : ArgDeclKind → ArgDeclKind → Bool

Equations

• StrataDDM.instBEqArgDeclKind.beq (StrataDDM.ArgDeclKind.type a) (StrataDDM.ArgDeclKind.type b) = (a == b)
• StrataDDM.instBEqArgDeclKind.beq (StrataDDM.ArgDeclKind.cat a) (StrataDDM.ArgDeclKind.cat b) = (a == b)
• StrataDDM.instBEqArgDeclKind.beq x✝¹ x✝ = false

@[implicit_reducible]

instance StrataDDM.instBEqArgDeclKind : BEq ArgDeclKind

Equations

• StrataDDM.instBEqArgDeclKind = { beq := StrataDDM.instBEqArgDeclKind.beq }

def StrataDDM.instInhabitedArgDeclKind.default : ArgDeclKind

Equations

• StrataDDM.instInhabitedArgDeclKind.default = StrataDDM.ArgDeclKind.type default

@[implicit_reducible]

instance StrataDDM.instInhabitedArgDeclKind : Inhabited ArgDeclKind

Equations

• StrataDDM.instInhabitedArgDeclKind = { default := StrataDDM.instInhabitedArgDeclKind.default }

def StrataDDM.instReprArgDeclKind.repr : ArgDeclKind → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprArgDeclKind : Repr ArgDeclKind

Equations

• StrataDDM.instReprArgDeclKind = { reprPrec := StrataDDM.instReprArgDeclKind.repr }

def StrataDDM.ArgDeclKind.categoryOf : ArgDeclKind → SyntaxCat

Equations

• (StrataDDM.ArgDeclKind.type a).categoryOf = StrataDDM.SyntaxCatF.atom a.ann { dialect := "Init", name := "Expr" }
• (StrataDDM.ArgDeclKind.cat a).categoryOf = a

def StrataDDM.ArgDeclKind.isType (k : ArgDeclKind) : Bool

Return true if this corresponds to builtin category Init.Type

Equations

• (StrataDDM.ArgDeclKind.cat c).isType = StrataDDM.SyntaxCatF.isType c
• k.isType = false

structure StrataDDM.ArgDecl : Type

An argument declaration in an operator or function.

• ident : Var
• kind : ArgDeclKind
• metadata : Metadata

def StrataDDM.instBEqArgDecl.beq : ArgDecl → ArgDecl → Bool

Equations

• StrataDDM.instBEqArgDecl.beq { ident := a, kind := a_1, metadata := a_2 } { ident := b, kind := b_1, metadata := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• StrataDDM.instBEqArgDecl.beq x✝¹ x✝ = false

@[implicit_reducible]

instance StrataDDM.instBEqArgDecl : BEq ArgDecl

Equations

• StrataDDM.instBEqArgDecl = { beq := StrataDDM.instBEqArgDecl.beq }

@[implicit_reducible]

instance StrataDDM.instInhabitedArgDecl : Inhabited ArgDecl

Equations

• StrataDDM.instInhabitedArgDecl = { default := StrataDDM.instInhabitedArgDecl.default }

def StrataDDM.instInhabitedArgDecl.default : ArgDecl

Equations

• StrataDDM.instInhabitedArgDecl.default = { ident := default, kind := default, metadata := default }

def StrataDDM.instReprArgDecl.repr : ArgDecl → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprArgDecl : Repr ArgDecl

Equations

• StrataDDM.instReprArgDecl = { reprPrec := StrataDDM.instReprArgDecl.repr }

structure StrataDDM.ArgDecls : Type

• ofArray :: (
• toArray : Array ArgDecl
• )

def StrataDDM.instBEqArgDecls.beq : ArgDecls → ArgDecls → Bool

Equations

• StrataDDM.instBEqArgDecls.beq { toArray := a } { toArray := b } = (a == b)
• StrataDDM.instBEqArgDecls.beq x✝¹ x✝ = false

@[implicit_reducible]

instance StrataDDM.instBEqArgDecls : BEq ArgDecls

Equations

• StrataDDM.instBEqArgDecls = { beq := StrataDDM.instBEqArgDecls.beq }

def StrataDDM.instInhabitedArgDecls.default : ArgDecls

Equations

• StrataDDM.instInhabitedArgDecls.default = { toArray := default }

@[implicit_reducible]

instance StrataDDM.instInhabitedArgDecls : Inhabited ArgDecls

Equations

• StrataDDM.instInhabitedArgDecls = { default := StrataDDM.instInhabitedArgDecls.default }

@[implicit_reducible]

instance StrataDDM.instReprArgDecls : Repr ArgDecls

Equations

• StrataDDM.instReprArgDecls = { reprPrec := StrataDDM.instReprArgDecls.repr }

def StrataDDM.instReprArgDecls.repr : ArgDecls → Nat → Std.Format

Equations

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

def StrataDDM.ArgDecls.empty : ArgDecls

Equations

• StrataDDM.ArgDecls.empty = { toArray := #[] }

@[implicit_reducible]

instance StrataDDM.ArgDecls.instEmptyCollection : EmptyCollection ArgDecls

Equations

• StrataDDM.ArgDecls.instEmptyCollection = { emptyCollection := StrataDDM.ArgDecls.empty }

def StrataDDM.ArgDecls.size (a : ArgDecls) : Nat

Equations

• a.size = a.toArray.size

def StrataDDM.ArgDecls.isEmpty (a : ArgDecls) : Bool

Equations

• a.isEmpty = a.toArray.isEmpty

@[implicit_reducible]

instance StrataDDM.ArgDecls.instGetElemNatArgDeclLtSize : GetElem ArgDecls Nat ArgDecl fun (a : ArgDecls) (i : Nat) => i < a.size

Equations

• StrataDDM.ArgDecls.instGetElemNatArgDeclLtSize = { getElem := fun (a : StrataDDM.ArgDecls) (i : Nat) (p : i < a.size) => StrataDDM.ArgDecls.instGetElemNatArgDeclLtSize._private_1 a i p }

def StrataDDM.ArgDecls.foldl {α : Type u_1} (a : ArgDecls) (f : α → ArgDecl → α) (init : α) : α

Equations

• a.foldl f init = Array.foldl f init a.toArray

def StrataDDM.ArgDecls.argScopeLevel (argDecls : ArgDecls) (level : Fin argDecls.size) : Except String (Option (Fin ↑level))

Returns the index of the value in the binding for the given variable of the scope to use.

Equations

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

def StrataDDM.ArgDecls.argScopeTVarLevel (argDecls : ArgDecls) (level : Fin argDecls.size) : Except String (Option (Fin ↑level))

Returns the typeParams level if @[scopeTVar] is present.

Equations

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

structure StrataDDM.ValueBindingSpec (argDecls : ArgDecls) : Type

Indices for introducing a new expression or operation.

• nameIndex : DebruijnIndex argDecls.size
• argsIndex : Option (DebruijnIndex argDecls.size)
• typeIndex : DebruijnIndex argDecls.size
• allowCat : Bool

@[implicit_reducible]

instance StrataDDM.instReprValueBindingSpec {argDecls✝ : ArgDecls} : Repr (ValueBindingSpec argDecls✝)

Equations

• StrataDDM.instReprValueBindingSpec = { reprPrec := StrataDDM.instReprValueBindingSpec.repr }

def StrataDDM.instReprValueBindingSpec.repr {argDecls✝ : ArgDecls} : ValueBindingSpec argDecls✝ → Nat → Std.Format

Equations

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

structure StrataDDM.TypeBindingSpec (argDecls : ArgDecls) : Type

Indices for introducing a new type binding.

• nameIndex : DebruijnIndex argDecls.size
• argsIndex : Option (DebruijnIndex argDecls.size)
• defIndex : Option (DebruijnIndex argDecls.size)

def StrataDDM.instReprTypeBindingSpec.repr {argDecls✝ : ArgDecls} : TypeBindingSpec argDecls✝ → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprTypeBindingSpec {argDecls✝ : ArgDecls} : Repr (TypeBindingSpec argDecls✝)

Equations

• StrataDDM.instReprTypeBindingSpec = { reprPrec := StrataDDM.instReprTypeBindingSpec.repr }

Datatype Type Building Functions

def StrataDDM.resolveTypeRef (ref : TypeRef) (datatypeType : TypeExpr) (fieldType : Option TypeExpr := none) (dialectName : String) : Except String TypeExpr

Resolve a type reference to a concrete TypeExpr. A type reference is either a datatype, field type (within perField/perConstructor scope), or a built-in (e.g. "bool")

Equations

• StrataDDM.resolveTypeRef StrataDDM.TypeRef.datatype datatypeType fieldType dialectName = Except.ok datatypeType
• StrataDDM.resolveTypeRef StrataDDM.TypeRef.fieldType datatypeType (some ft) dialectName = Except.ok ft
• StrataDDM.resolveTypeRef StrataDDM.TypeRef.fieldType datatypeType none dialectName = Except.error "TypeRef.fieldType is only valid in perField scope"
• StrataDDM.resolveTypeRef (StrataDDM.TypeRef.builtin name) datatypeType fieldType dialectName = Except.ok (StrataDDM.TypeExprF.ident default { dialect := dialectName, name := name } #[])

structure StrataDDM.ConstructorInfo : Type

Information about a single constructor in a datatype.

• name : String

  Constructor name

• fields : Array (String × TypeExpr)

  Fields as (fieldName, fieldType) pairs

def StrataDDM.instReprConstructorInfo.repr : ConstructorInfo → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprConstructorInfo : Repr ConstructorInfo

Equations

• StrataDDM.instReprConstructorInfo = { reprPrec := StrataDDM.instReprConstructorInfo.repr }

def StrataDDM.mkDatatypeTypeRef (ann : SourceRange) (datatypeIndex : FreeVarIndex) (typeParams : Array String) : TypeExpr

Build a TypeExpr reference to the datatype with type parameters, using .fvar for the datatype's GlobalContext index and .tvar for type parameters.

Equations

• StrataDDM.mkDatatypeTypeRef ann datatypeIndex typeParams = StrataDDM.TypeExprF.fvar ann datatypeIndex (Array.map (fun (name : String) => StrataDDM.TypeExprF.tvar ann name) typeParams)

def StrataDDM.mkConstructorType (ann : SourceRange) (datatypeType : TypeExpr) (fields : Array (String × TypeExpr)) : TypeExpr

Build an arrow type from field types to the datatype type. E.g. for cons, creates a -> List a -> List a.

Equations

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

def StrataDDM.buildFunctionType (template : FunctionTemplate) (datatypeType : TypeExpr) (fieldType : Option TypeExpr) (dialectName : String) : Except String TypeExpr

Build a function type from parameter types and return type. Returns an arrow type: param1 -> param2 -> ... -> returnType

Equations

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

structure StrataDDM.DatatypeBindingSpec (argDecls : ArgDecls) : Type

Specification for datatype declarations. Includes indices for extracting datatype information and optional function templates.

• nameIndex : DebruijnIndex argDecls.size

  deBrujin index of datatype name

• typeParamsIndex : DebruijnIndex argDecls.size

  deBrujin index of type parameters

• constructorsIndex : DebruijnIndex argDecls.size

  deBrujin index of constructors

• functionTemplates : Array FunctionTemplate

  Optional list of function templates to expand

@[implicit_reducible]

instance StrataDDM.instReprDatatypeBindingSpec {argDecls✝ : ArgDecls} : Repr (DatatypeBindingSpec argDecls✝)

Equations

• StrataDDM.instReprDatatypeBindingSpec = { reprPrec := StrataDDM.instReprDatatypeBindingSpec.repr }

def StrataDDM.instReprDatatypeBindingSpec.repr {argDecls✝ : ArgDecls} : DatatypeBindingSpec argDecls✝ → Nat → Std.Format

Equations

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

structure StrataDDM.TvarBindingSpec (argDecls : ArgDecls) : Type

Specification for declaring a single type variable. Creates a .tvar binding in the result context.

• nameIndex : DebruijnIndex argDecls.size

  deBrujin index of the identifier to become a type variable

def StrataDDM.instReprTvarBindingSpec.repr {argDecls✝ : ArgDecls} : TvarBindingSpec argDecls✝ → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprTvarBindingSpec {argDecls✝ : ArgDecls} : Repr (TvarBindingSpec argDecls✝)

Equations

• StrataDDM.instReprTvarBindingSpec = { reprPrec := StrataDDM.instReprTvarBindingSpec.repr }

inductive StrataDDM.BindingSpec (argDecls : ArgDecls) : Type

• value {argDecls : ArgDecls} : ValueBindingSpec argDecls → BindingSpec argDecls
• type {argDecls : ArgDecls} : TypeBindingSpec argDecls → BindingSpec argDecls
• scopedType {argDecls : ArgDecls} : TypeBindingSpec argDecls → BindingSpec argDecls
• datatype {argDecls : ArgDecls} : DatatypeBindingSpec argDecls → BindingSpec argDecls
• tvar {argDecls : ArgDecls} : TvarBindingSpec argDecls → BindingSpec argDecls

@[implicit_reducible]

instance StrataDDM.instReprBindingSpec {argDecls✝ : ArgDecls} : Repr (BindingSpec argDecls✝)

Equations

• StrataDDM.instReprBindingSpec = { reprPrec := StrataDDM.instReprBindingSpec.repr }

def StrataDDM.instReprBindingSpec.repr {argDecls✝ : ArgDecls} : BindingSpec argDecls✝ → Nat → Std.Format

Equations

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

def StrataDDM.BindingSpec.nameIndex {argDecls : ArgDecls} : BindingSpec argDecls → DebruijnIndex argDecls.size

Equations

• (StrataDDM.BindingSpec.value a).nameIndex = a.nameIndex
• (StrataDDM.BindingSpec.type a).nameIndex = a.nameIndex
• (StrataDDM.BindingSpec.scopedType a).nameIndex = a.nameIndex
• (StrataDDM.BindingSpec.datatype a).nameIndex = a.nameIndex
• (StrataDDM.BindingSpec.tvar a).nameIndex = a.nameIndex

def StrataDDM.parseNewBindings (md : Metadata) (argDecls : ArgDecls) : Array (BindingSpec argDecls) × Array String

Equations

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

def StrataDDM.parseNewBindings! (md : Metadata) (argDecls : ArgDecls) : Array (BindingSpec argDecls)

Equations

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

structure StrataDDM.SynCatDecl : Type

• name : String
• argNames : Array String

def StrataDDM.instReprSynCatDecl.repr : SynCatDecl → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprSynCatDecl : Repr SynCatDecl

Equations

• StrataDDM.instReprSynCatDecl = { reprPrec := StrataDDM.instReprSynCatDecl.repr }

def StrataDDM.instDecidableEqSynCatDecl.decEq (x✝ x✝¹ : SynCatDecl) : Decidable (x✝ = x✝¹)

Equations

• StrataDDM.instDecidableEqSynCatDecl.decEq { name := a, argNames := a_1 } { name := b, argNames := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance StrataDDM.instDecidableEqSynCatDecl : DecidableEq SynCatDecl

Equations

• StrataDDM.instDecidableEqSynCatDecl = StrataDDM.instDecidableEqSynCatDecl.decEq

@[implicit_reducible]

instance StrataDDM.instInhabitedSynCatDecl : Inhabited SynCatDecl

Equations

• StrataDDM.instInhabitedSynCatDecl = { default := StrataDDM.instInhabitedSynCatDecl.default }

def StrataDDM.instInhabitedSynCatDecl.default : SynCatDecl

Equations

• StrataDDM.instInhabitedSynCatDecl.default = { name := default, argNames := default }

structure StrataDDM.Ann (Base α : Type) : Type

• ann : α
• val : Base

def StrataDDM.instBEqAnn.beq {Base✝ α✝ : Type} [BEq Base✝] [BEq α✝] : Ann Base✝ α✝ → Ann Base✝ α✝ → Bool

Equations

• StrataDDM.instBEqAnn.beq { ann := a, val := a_1 } { ann := b, val := b_1 } = (a == b && a_1 == b_1)
• StrataDDM.instBEqAnn.beq x✝¹ x✝ = false

@[implicit_reducible]

instance StrataDDM.instBEqAnn {Base✝ α✝ : Type} [BEq Base✝] [BEq α✝] : BEq (Ann Base✝ α✝)

Equations

• StrataDDM.instBEqAnn = { beq := StrataDDM.instBEqAnn.beq }

def StrataDDM.instDecidableEqAnn.decEq {Base✝ α✝ : Type} [DecidableEq Base✝] [DecidableEq α✝] (x✝ x✝¹ : Ann Base✝ α✝) : Decidable (x✝ = x✝¹)

Equations

• StrataDDM.instDecidableEqAnn.decEq { ann := a, val := a_1 } { ann := b, val := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance StrataDDM.instDecidableEqAnn {Base✝ α✝ : Type} [DecidableEq Base✝] [DecidableEq α✝] : DecidableEq (Ann Base✝ α✝)

Equations

• StrataDDM.instDecidableEqAnn = StrataDDM.instDecidableEqAnn.decEq

@[implicit_reducible]

instance StrataDDM.instInhabitedAnn {a✝ : Type} [Inhabited a✝] {a✝¹ : Type} [Inhabited a✝¹] : Inhabited (Ann a✝ a✝¹)

Equations

• StrataDDM.instInhabitedAnn = { default := StrataDDM.instInhabitedAnn.default }

def StrataDDM.instInhabitedAnn.default {a✝ : Type} [Inhabited a✝] {a✝¹ : Type} [Inhabited a✝¹] : Ann a✝ a✝¹

Equations

• StrataDDM.instInhabitedAnn.default = { ann := default, val := default }

def StrataDDM.instReprAnn.repr {Base✝ α✝ : Type} [Repr Base✝] [Repr α✝] : Ann Base✝ α✝ → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprAnn {Base✝ α✝ : Type} [Repr Base✝] [Repr α✝] : Repr (Ann Base✝ α✝)

Equations

• StrataDDM.instReprAnn = { reprPrec := StrataDDM.instReprAnn.repr }

structure StrataDDM.TypeDecl : Type

A declaration of an algebraic data type.

• name : String
• argNames : Array (Ann String SourceRange)

@[implicit_reducible]

instance StrataDDM.instBEqTypeDecl : BEq TypeDecl

Equations

• StrataDDM.instBEqTypeDecl = { beq := StrataDDM.instBEqTypeDecl.beq }

def StrataDDM.instBEqTypeDecl.beq : TypeDecl → TypeDecl → Bool

Equations

• StrataDDM.instBEqTypeDecl.beq { name := a, argNames := a_1 } { name := b, argNames := b_1 } = (a == b && a_1 == b_1)
• StrataDDM.instBEqTypeDecl.beq x✝¹ x✝ = false

@[implicit_reducible]

instance StrataDDM.instInhabitedTypeDecl : Inhabited TypeDecl

Equations

• StrataDDM.instInhabitedTypeDecl = { default := StrataDDM.instInhabitedTypeDecl.default }

def StrataDDM.instInhabitedTypeDecl.default : TypeDecl

Equations

• StrataDDM.instInhabitedTypeDecl.default = { name := default, argNames := default }

def StrataDDM.instReprTypeDecl.repr : TypeDecl → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprTypeDecl : Repr TypeDecl

Equations

• StrataDDM.instReprTypeDecl = { reprPrec := StrataDDM.instReprTypeDecl.repr }

structure StrataDDM.OpDecl : Type

Operator declaration

• name : String

  Name of operator

• argDecls : ArgDecls

  Arguments to operator.

• category : QualifiedIdent

  Syntactic category of operator

• syntaxDef : SyntaxDef

  Schema for operator

• metadata : Metadata

  Metadata for operator.

• newBindings : Array (BindingSpec self.argDecls)

  New bindings

@[implicit_reducible]

instance StrataDDM.instInhabitedOpDecl : Inhabited OpDecl

Equations

• StrataDDM.instInhabitedOpDecl = { default := StrataDDM.instInhabitedOpDecl.default }

def StrataDDM.instInhabitedOpDecl.default : OpDecl

Equations

• StrataDDM.instInhabitedOpDecl.default = { name := default, argDecls := default, category := default, syntaxDef := default, metadata := default, newBindings := default }

def StrataDDM.instReprOpDecl.repr : OpDecl → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprOpDecl : Repr OpDecl

Equations

• StrataDDM.instReprOpDecl = { reprPrec := StrataDDM.instReprOpDecl.repr }

@[implicit_reducible]

instance StrataDDM.OpDecl.instBEq : BEq OpDecl

Equations

• StrataDDM.OpDecl.instBEq = { beq := fun (x y : StrataDDM.OpDecl) => StrataDDM.OpDecl.instBEq._private_1 x y }

@[reducible, inline]

abbrev StrataDDM.FnName : Type

Equations

• StrataDDM.FnName = String

structure StrataDDM.FunctionDecl : Type

• name : FnName
• argDecls : ArgDecls
• result : PreType
• syntaxDef : SyntaxDef
• metadata : Metadata

def StrataDDM.instBEqFunctionDecl.beq : FunctionDecl → FunctionDecl → Bool

Equations

• One or more equations did not get rendered due to their size.
• StrataDDM.instBEqFunctionDecl.beq x✝¹ x✝ = false

@[implicit_reducible]

instance StrataDDM.instBEqFunctionDecl : BEq FunctionDecl

Equations

• StrataDDM.instBEqFunctionDecl = { beq := StrataDDM.instBEqFunctionDecl.beq }

@[implicit_reducible]

instance StrataDDM.instInhabitedFunctionDecl : Inhabited FunctionDecl

Equations

• StrataDDM.instInhabitedFunctionDecl = { default := StrataDDM.instInhabitedFunctionDecl.default }

def StrataDDM.instInhabitedFunctionDecl.default : FunctionDecl

Equations

• StrataDDM.instInhabitedFunctionDecl.default = { name := default, argDecls := default, result := default, syntaxDef := default, metadata := default }

def StrataDDM.instReprFunctionDecl.repr : FunctionDecl → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprFunctionDecl : Repr FunctionDecl

Equations

• StrataDDM.instReprFunctionDecl = { reprPrec := StrataDDM.instReprFunctionDecl.repr }

inductive StrataDDM.MetadataArgType : Type

• num : MetadataArgType
• ident : MetadataArgType
• bool : MetadataArgType
• opt (tp : MetadataArgType) : MetadataArgType
• functionTemplate : MetadataArgType

def StrataDDM.instDecidableEqMetadataArgType.decEq (x✝ x✝¹ : MetadataArgType) : Decidable (x✝ = x✝¹)

Equations

• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.num StrataDDM.MetadataArgType.num = isTrue ⋯
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.num StrataDDM.MetadataArgType.ident = isFalse StrataDDM.instDecidableEqMetadataArgType.decEq._proof_1✝
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.num StrataDDM.MetadataArgType.bool = isFalse StrataDDM.instDecidableEqMetadataArgType.decEq._proof_2✝
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.num tp.opt = isFalse ⋯
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.num StrataDDM.MetadataArgType.functionTemplate = isFalse StrataDDM.instDecidableEqMetadataArgType.decEq._proof_4✝
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.ident StrataDDM.MetadataArgType.num = isFalse StrataDDM.instDecidableEqMetadataArgType.decEq._proof_5✝
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.ident StrataDDM.MetadataArgType.ident = isTrue ⋯
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.ident StrataDDM.MetadataArgType.bool = isFalse StrataDDM.instDecidableEqMetadataArgType.decEq._proof_6✝
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.ident tp.opt = isFalse ⋯
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.ident StrataDDM.MetadataArgType.functionTemplate = isFalse StrataDDM.instDecidableEqMetadataArgType.decEq._proof_8✝
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.bool StrataDDM.MetadataArgType.num = isFalse StrataDDM.instDecidableEqMetadataArgType.decEq._proof_9✝
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.bool StrataDDM.MetadataArgType.ident = isFalse StrataDDM.instDecidableEqMetadataArgType.decEq._proof_10✝
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.bool StrataDDM.MetadataArgType.bool = isTrue ⋯
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.bool tp.opt = isFalse ⋯
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.bool StrataDDM.MetadataArgType.functionTemplate = isFalse StrataDDM.instDecidableEqMetadataArgType.decEq._proof_12✝
• StrataDDM.instDecidableEqMetadataArgType.decEq tp.opt StrataDDM.MetadataArgType.num = isFalse ⋯
• StrataDDM.instDecidableEqMetadataArgType.decEq tp.opt StrataDDM.MetadataArgType.ident = isFalse ⋯
• StrataDDM.instDecidableEqMetadataArgType.decEq tp.opt StrataDDM.MetadataArgType.bool = isFalse ⋯
• StrataDDM.instDecidableEqMetadataArgType.decEq a.opt b.opt = if h : a = b then h ▸ have inst := StrataDDM.instDecidableEqMetadataArgType.decEq a a; isTrue ⋯ else isFalse ⋯
• StrataDDM.instDecidableEqMetadataArgType.decEq tp.opt StrataDDM.MetadataArgType.functionTemplate = isFalse ⋯
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.functionTemplate StrataDDM.MetadataArgType.num = isFalse StrataDDM.instDecidableEqMetadataArgType.decEq._proof_19✝
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.functionTemplate StrataDDM.MetadataArgType.ident = isFalse StrataDDM.instDecidableEqMetadataArgType.decEq._proof_20✝
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.functionTemplate StrataDDM.MetadataArgType.bool = isFalse StrataDDM.instDecidableEqMetadataArgType.decEq._proof_21✝
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.functionTemplate tp.opt = isFalse ⋯
• StrataDDM.instDecidableEqMetadataArgType.decEq StrataDDM.MetadataArgType.functionTemplate StrataDDM.MetadataArgType.functionTemplate = isTrue ⋯

@[implicit_reducible]

instance StrataDDM.instDecidableEqMetadataArgType : DecidableEq MetadataArgType

Equations

• StrataDDM.instDecidableEqMetadataArgType = StrataDDM.instDecidableEqMetadataArgType.decEq

@[implicit_reducible]

instance StrataDDM.instInhabitedMetadataArgType : Inhabited MetadataArgType

Equations

• StrataDDM.instInhabitedMetadataArgType = { default := StrataDDM.instInhabitedMetadataArgType.default }

def StrataDDM.instInhabitedMetadataArgType.default : MetadataArgType

Equations

• StrataDDM.instInhabitedMetadataArgType.default = StrataDDM.MetadataArgType.num

def StrataDDM.instReprMetadataArgType.repr : MetadataArgType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprMetadataArgType : Repr MetadataArgType

Equations

• StrataDDM.instReprMetadataArgType = { reprPrec := StrataDDM.instReprMetadataArgType.repr }

structure StrataDDM.MetadataArgDecl : Type

• ident : String
• type : MetadataArgType

def StrataDDM.instDecidableEqMetadataArgDecl.decEq (x✝ x✝¹ : MetadataArgDecl) : Decidable (x✝ = x✝¹)

Equations

• StrataDDM.instDecidableEqMetadataArgDecl.decEq { ident := a, type := a_1 } { ident := b, type := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance StrataDDM.instDecidableEqMetadataArgDecl : DecidableEq MetadataArgDecl

Equations

• StrataDDM.instDecidableEqMetadataArgDecl = StrataDDM.instDecidableEqMetadataArgDecl.decEq

@[implicit_reducible]

instance StrataDDM.instInhabitedMetadataArgDecl : Inhabited MetadataArgDecl

Equations

• StrataDDM.instInhabitedMetadataArgDecl = { default := StrataDDM.instInhabitedMetadataArgDecl.default }

def StrataDDM.instInhabitedMetadataArgDecl.default : MetadataArgDecl

Equations

• StrataDDM.instInhabitedMetadataArgDecl.default = { ident := default, type := default }

def StrataDDM.instReprMetadataArgDecl.repr : MetadataArgDecl → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprMetadataArgDecl : Repr MetadataArgDecl

Equations

• StrataDDM.instReprMetadataArgDecl = { reprPrec := StrataDDM.instReprMetadataArgDecl.repr }

structure StrataDDM.MetadataDecl : Type

Declaration of a metadata tag in a dialect.

Metadata has an optional argument that must have the specified type.

N.B. We may want to further restrict where metadata can appear.

• name : String
• args : Array MetadataArgDecl

def StrataDDM.instDecidableEqMetadataDecl.decEq (x✝ x✝¹ : MetadataDecl) : Decidable (x✝ = x✝¹)

Equations

• StrataDDM.instDecidableEqMetadataDecl.decEq { name := a, args := a_1 } { name := b, args := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance StrataDDM.instDecidableEqMetadataDecl : DecidableEq MetadataDecl

Equations

• StrataDDM.instDecidableEqMetadataDecl = StrataDDM.instDecidableEqMetadataDecl.decEq

@[implicit_reducible]

instance StrataDDM.instInhabitedMetadataDecl : Inhabited MetadataDecl

Equations

• StrataDDM.instInhabitedMetadataDecl = { default := StrataDDM.instInhabitedMetadataDecl.default }

def StrataDDM.instInhabitedMetadataDecl.default : MetadataDecl

Equations

• StrataDDM.instInhabitedMetadataDecl.default = { name := default, args := default }

@[implicit_reducible]

instance StrataDDM.instReprMetadataDecl : Repr MetadataDecl

Equations

• StrataDDM.instReprMetadataDecl = { reprPrec := StrataDDM.instReprMetadataDecl.repr }

def StrataDDM.instReprMetadataDecl.repr : MetadataDecl → Nat → Std.Format

Equations

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

inductive StrataDDM.Decl : Type

• syncat (d : SynCatDecl) : Decl
• op (d : OpDecl) : Decl
• type (d : TypeDecl) : Decl
• function (d : FunctionDecl) : Decl
• metadata (d : MetadataDecl) : Decl

@[implicit_reducible]

instance StrataDDM.instBEqDecl : BEq Decl

Equations

• StrataDDM.instBEqDecl = { beq := StrataDDM.instBEqDecl.beq }

def StrataDDM.instBEqDecl.beq : Decl → Decl → Bool

Equations

• StrataDDM.instBEqDecl.beq (StrataDDM.Decl.syncat a) (StrataDDM.Decl.syncat b) = (a == b)
• StrataDDM.instBEqDecl.beq (StrataDDM.Decl.op a) (StrataDDM.Decl.op b) = (a == b)
• StrataDDM.instBEqDecl.beq (StrataDDM.Decl.type a) (StrataDDM.Decl.type b) = (a == b)
• StrataDDM.instBEqDecl.beq (StrataDDM.Decl.function a) (StrataDDM.Decl.function b) = (a == b)
• StrataDDM.instBEqDecl.beq (StrataDDM.Decl.metadata a) (StrataDDM.Decl.metadata b) = (a == b)
• StrataDDM.instBEqDecl.beq x✝¹ x✝ = false

@[implicit_reducible]

instance StrataDDM.instInhabitedDecl : Inhabited Decl

Equations

• StrataDDM.instInhabitedDecl = { default := StrataDDM.instInhabitedDecl.default }

def StrataDDM.instInhabitedDecl.default : Decl

Equations

• StrataDDM.instInhabitedDecl.default = StrataDDM.Decl.syncat default

@[implicit_reducible]

instance StrataDDM.instReprDecl : Repr Decl

Equations

• StrataDDM.instReprDecl = { reprPrec := StrataDDM.instReprDecl.repr }

def StrataDDM.instReprDecl.repr : Decl → Nat → Std.Format

Equations

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

def StrataDDM.Decl.name : Decl → String

Equations

• (StrataDDM.Decl.syncat a).name = a.name
• (StrataDDM.Decl.op a).name = a.name
• (StrataDDM.Decl.type a).name = a.name
• (StrataDDM.Decl.function a).name = a.name
• (StrataDDM.Decl.metadata a).name = a.name

structure StrataDDM.Collection (α : Type) : Type

• declarations : Array Decl
• cache : Std.HashMap String Decl
• proj : Decl → Option α
• pretty : α → String

@[implicit_reducible]

instance StrataDDM.Collection.instForInOfMonad {m : Type u_1 → Type u_2} {α : Type} [Monad m] : ForIn m (Collection α) α

Equations

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

def StrataDDM.Collection.fold {α : Type} {β : Type u_1} (f : β → α → β) (init : β) (c : Collection α) : β

Equations

• StrataDDM.Collection.fold f init c = Array.foldl (fun (b : β) (d : StrataDDM.Decl) => match c.proj d with | some v => f b v | none => b) init c.declarations

@[implicit_reducible]

instance StrataDDM.Collection.instToString {α : Type} : ToString (Collection α)

Equations

• StrataDDM.Collection.instToString = { toString := fun (c : StrataDDM.Collection α) => StrataDDM.Collection.instToString._private_1 c }

@[implicit_reducible]

instance StrataDDM.Collection.instMembershipString {α : Type} : Membership String (Collection α)

Equations

• StrataDDM.Collection.instMembershipString = { mem := StrataDDM.Collection.instMembershipString._private_1 }

def StrataDDM.Collection.instDecidableMem {α : Type} (nm : String) (c : Collection α) : Decidable (nm ∈ c)

Equations

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

@[implicit_reducible]

instance StrataDDM.Collection.instDecidableMemString {α : Type} (nm : String) (c : Collection α) : Decidable (nm ∈ c)

Equations

• StrataDDM.Collection.instDecidableMemString nm c = StrataDDM.Collection.instDecidableMem nm c

@[implicit_reducible]

instance StrataDDM.Collection.instGetElem?StringMem {α : Type} : GetElem? (Collection α) String α fun (c : Collection α) (nm : String) => nm ∈ c

Equations

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

structure StrataDDM.Dialect : Type

A dialect definition.

• name : DialectName
• imports : Array DialectName
• declarations : Array Decl
• typecheck : Bool

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

• cache : Std.HashMap String Decl

@[implicit_reducible]

instance StrataDDM.Dialect.instInhabited : Inhabited Dialect

Equations

• StrataDDM.Dialect.instInhabited = { default := { name := default, imports := #[] } }

@[implicit_reducible]

instance StrataDDM.Dialect.instBEq : BEq Dialect

Equations

• StrataDDM.Dialect.instBEq = { beq := fun (x y : StrataDDM.Dialect) => decide (x.name = y.name) && decide (x.imports = y.imports) && x.declarations == y.declarations }

def StrataDDM.Dialect.syncats (d : Dialect) : Collection SynCatDecl

Equations

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

def StrataDDM.Dialect.ops (d : Dialect) : Collection OpDecl

Equations

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

def StrataDDM.Dialect.types (d : Dialect) : Collection TypeDecl

Equations

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

def StrataDDM.Dialect.functions (d : Dialect) : Collection FunctionDecl

Equations

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

def StrataDDM.Dialect.metadata (d : Dialect) : Collection MetadataDecl

Equations

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

def StrataDDM.Dialect.ofArray (name : DialectName) (importDialects : Array DialectName) (a : Array Decl) : Dialect

Equations

• StrataDDM.Dialect.ofArray name importDialects a = { name := name, imports := importDialects, declarations := a }

def StrataDDM.Dialect.addDecl (d : Dialect) (decl : Decl) : Dialect

Equations

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

def StrataDDM.Dialect.mem (d : Dialect) (name : String) : Bool

Equations

• d.mem name = decide (name ∈ d.cache)

@[implicit_reducible]

instance StrataDDM.Dialect.instMembershipString : Membership String Dialect

Equations

• StrataDDM.Dialect.instMembershipString = { mem := fun (d : StrataDDM.Dialect) (nm : String) => d.mem nm = true }

@[implicit_reducible]

instance StrataDDM.Dialect.instDecidableMem (nm : String) (d : Dialect) : Decidable (nm ∈ d)

Equations

• StrataDDM.Dialect.instDecidableMem nm d = inferInstance

def StrataDDM.DialectMap.Closed (map : Std.HashMap DialectName Dialect) : Prop

Equations

• StrataDDM.DialectMap.Closed map = ∀ (d : StrataDDM.DialectName) (p : d ∈ map), (map[d].imports.all fun (x : StrataDDM.DialectName) => decide (x ∈ map)) = true

structure StrataDDM.DialectMap : Type

• map : Std.HashMap StrataDDM.DialectName StrataDDM.Dialect
• closed : StrataDDM.DialectMap.Closed (StrataDDM.DialectMap.map✝ self)

def StrataDDM.DialectMap.empty : DialectMap

Equations

• StrataDDM.DialectMap.empty = { map := ∅, closed := StrataDDM.DialectMap.empty._proof_1✝ }

@[implicit_reducible]

instance StrataDDM.DialectMap.instEmptyCollection : EmptyCollection DialectMap

Equations

• StrataDDM.DialectMap.instEmptyCollection = { emptyCollection := StrataDDM.DialectMap.empty }

@[implicit_reducible]

instance StrataDDM.DialectMap.instInhabited : Inhabited DialectMap

Equations

• StrataDDM.DialectMap.instInhabited = { default := StrataDDM.DialectMap.instInhabited._private_1 }

def StrataDDM.DialectMap.mem (m : DialectMap) (name : DialectName) : Bool

Equations

• m.mem name = decide (name ∈ StrataDDM.DialectMap.map✝ m)

@[implicit_reducible]

instance StrataDDM.DialectMap.instMembership : Membership DialectName DialectMap

Equations

• StrataDDM.DialectMap.instMembership = { mem := fun (m : StrataDDM.DialectMap) (name : StrataDDM.DialectName) => m.mem name = true }

@[implicit_reducible]

instance StrataDDM.DialectMap.instDecidableMembership (d : DialectName) (m : DialectMap) : Decidable (d ∈ m)

Equations

• StrataDDM.DialectMap.instDecidableMembership d m = inferInstance

@[implicit_reducible]

instance StrataDDM.DialectMap.instGetElem?DialectNameDialectMem : GetElem? DialectMap DialectName Dialect fun (m : DialectMap) (d : DialectName) => d ∈ m

Equations

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

opaque StrataDDM.DialectMap.insert (m : DialectMap) (d : Dialect) (_d_new : ¬d.name ∈ m) (d_imports_ok : (d.imports.all fun (x : DialectName) => decide (x ∈ m)) = true) : DialectMap

This inserts a new dialect into the dialect map.

This requires propositions to ensure we do not change the semantics of dialects and imports are already in dialect.

def StrataDDM.DialectMap.insert! (m : DialectMap) (d : Dialect) : DialectMap

This inserts a dialect in to the dialect map.

It panics if a dialect with the same name is already in the map or if the dialect imports a dialect not already in the map.

Equations

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

def StrataDDM.DialectMap.ofList! (l : List Dialect) : DialectMap

Equations

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

def StrataDDM.DialectMap.toList (m : DialectMap) : List Dialect

Return dialects in map.

Note that no specific ordering is made on dialects returned.

Equations

• m.toList = (StrataDDM.DialectMap.map✝ m).values

def StrataDDM.DialectMap.decl! (dm : DialectMap) (ident : QualifiedIdent) : Decl

Equations

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

def StrataDDM.DialectMap.importedDialects (dm : DialectMap) (dialect : DialectName) (p : dialect ∈ dm) : DialectMap

Return set of all dialects that are imported by dialect.

This includes transitive imports.

Equations

• dm.importedDialects dialect p = StrataDDM.DialectMap.importedDialectsAux✝ (StrataDDM.DialectMap.map✝ dm) ⋯ dialect ⋯

def StrataDDM.DialectMap.lookupOpDecl (dialects : DialectMap) (opName : QualifiedIdent) : Option OpDecl

Look up an operation's metadata in the dialect. Returns the OpDecl if found, or none if the operation is not in the dialect.

Equations

• dialects.lookupOpDecl opName = match dialects[opName.dialect]? with | none => none | some dialect => dialect.ops[opName.name]?

partial def StrataDDM.foldOverArgBindingSpecs {α : Type} {β : Type u_1} (m : DialectMap) (f : β → α → (argDecls : ArgDecls) → BindingSpec argDecls → Vector (ArgF α) argDecls.size → β) (init : β) (a : ArgF α) : β

Recursively folds over all binding specifications declared within an argument. Used to collect type bindings, value bindings, and other declarations that appear nested within operation arguments.

partial def StrataDDM.OperationF.foldBindingSpecs {α : Type} {β : Type u_1} (m : DialectMap) (f : β → α → {argDecls : ArgDecls} → BindingSpec argDecls → Vector (ArgF α) argDecls.size → β) (init : β) (op : OperationF α) : β

Invoke a function f over each of the declaration specifications for an operator.

inductive StrataDDM.GlobalKind : Type

• expr (tp : TypeExpr) : GlobalKind
• type (params : List String) (definition : Option TypeExpr) : GlobalKind

def StrataDDM.instBEqGlobalKind.beq : GlobalKind → GlobalKind → Bool

Equations

• StrataDDM.instBEqGlobalKind.beq (StrataDDM.GlobalKind.expr a) (StrataDDM.GlobalKind.expr b) = (a == b)
• StrataDDM.instBEqGlobalKind.beq (StrataDDM.GlobalKind.type a a_1) (StrataDDM.GlobalKind.type b b_1) = (a == b && a_1 == b_1)
• StrataDDM.instBEqGlobalKind.beq x✝¹ x✝ = false

@[implicit_reducible]

instance StrataDDM.instBEqGlobalKind : BEq GlobalKind

Equations

• StrataDDM.instBEqGlobalKind = { beq := StrataDDM.instBEqGlobalKind.beq }

@[implicit_reducible]

instance StrataDDM.instInhabitedGlobalKind : Inhabited GlobalKind

Equations

• StrataDDM.instInhabitedGlobalKind = { default := StrataDDM.instInhabitedGlobalKind.default }

def StrataDDM.instInhabitedGlobalKind.default : GlobalKind

Equations

• StrataDDM.instInhabitedGlobalKind.default = StrataDDM.GlobalKind.expr default

@[implicit_reducible]

instance StrataDDM.instReprGlobalKind : Repr GlobalKind

Equations

• StrataDDM.instReprGlobalKind = { reprPrec := StrataDDM.instReprGlobalKind.repr }

def StrataDDM.instReprGlobalKind.repr : GlobalKind → Nat → Std.Format

Equations

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

partial def StrataDDM.resolveBindingIndices {argDecls : ArgDecls} (m : DialectMap) (src : SourceRange) (b : BindingSpec argDecls) (args : Vector Arg argDecls.size) : Option GlobalKind

Resolves a binding spec into a global kind.

Annotation-based Constructor Info Extraction

The following functions implement constructor info extraction using @[constructor(name, fields)] and @[field(name, tp)] annotations.

The annotation-based approach:

1. Looks up the operation in the dialect's operation declarations
2. Checks if the operation has the appropriate metadata annotation
3. Uses the indices from the annotation to extract the relevant arguments

@[irreducible]

def StrataDDM.extractConstructorInfo (dialects : DialectMap) (arg : Arg) : Except String (Array ConstructorInfo)

This function traverses a constructor list AST node and extracts structured information about each constructor, including its name and fields using the dialect annotations @[constructor], @[constructorListAtom], @[constructorListPush].

Example: For { None(), Some(value: T) }, returns:

#[
  { name := "None", fields := #[] },
  { name := "Some", fields := #[("value", <TypeExpr for T>)] }
]

Equations

• One or more equations did not get rendered due to their size.
• StrataDDM.extractConstructorInfo dialects arg = throw (toString "Expected op for constructor list, got " ++ toString (repr arg))

structure StrataDDM.GlobalContext : Type

Typing environment created from declarations in an environment.

• nameMap : Std.HashMap Var FreeVarIndex
• vars : Array (Var × GlobalKind)

def StrataDDM.instReprGlobalContext.repr : GlobalContext → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprGlobalContext : Repr GlobalContext

Equations

• StrataDDM.instReprGlobalContext = { reprPrec := StrataDDM.instReprGlobalContext.repr }

@[implicit_reducible]

instance StrataDDM.GlobalContext.instEmptyCollection : EmptyCollection GlobalContext

Equations

• StrataDDM.GlobalContext.instEmptyCollection = { emptyCollection := StrataDDM.GlobalContext.instEmptyCollection._private_1 }

@[implicit_reducible]

instance StrataDDM.GlobalContext.instInhabited : Inhabited GlobalContext

Equations

• StrataDDM.GlobalContext.instInhabited = { default := ∅ }

@[implicit_reducible]

instance StrataDDM.GlobalContext.instMembershipVar : Membership Var GlobalContext

Equations

• StrataDDM.GlobalContext.instMembershipVar = { mem := fun (ctx : StrataDDM.GlobalContext) (v : StrataDDM.Var) => v ∈ ctx.nameMap }

@[implicit_reducible]

instance StrataDDM.GlobalContext.instDecidableMem (v : Var) (ctx : GlobalContext) : Decidable (v ∈ ctx)

Equations

• StrataDDM.GlobalContext.instDecidableMem v ctx = inferInstance

def StrataDDM.GlobalContext.define (ctx : GlobalContext) (v : Var) (k : GlobalKind) : ¬v ∈ ctx → GlobalContext

Define a symbol. Caller must prove v ∉ ctx.

Equations

• ctx.define v k x✝ = { nameMap := ctx.nameMap.insert v ctx.vars.size, vars := ctx.vars.push (v, k) }

def StrataDDM.GlobalContext.ensureDefined (ctx : GlobalContext) (v : Var) (k : GlobalKind) : GlobalContext

Define a symbol if not already present. No-op if already defined.

Equations

• ctx.ensureDefined v k = if h : v ∈ ctx then ctx else ctx.define v k h

def StrataDDM.GlobalContext.defineChecked (ctx : GlobalContext) (v : Var) (k : GlobalKind) (preRegistered : Bool) : Except String GlobalContext

Define a symbol, with behavior controlled by preRegistered:

• preRegistered = true: the name is expected to already exist (was pre-registered). Returns the context unchanged, or an error if missing.
• preRegistered = false: the name must be fresh. Defines it, or returns an error if already present.

Equations

• ctx.defineChecked v k true = Except.ok ctx
• ctx.defineChecked v k false = Except.error (toString "'" ++ toString v ++ toString "' already defined")
• ctx.defineChecked v k false = Except.ok (ctx.define v k h)
• ctx.defineChecked v k true = Except.error (toString "pre-registered '" ++ toString v ++ toString "' not found")

def StrataDDM.GlobalContext.findIndex? (ctx : GlobalContext) (v : Var) : Option FreeVarIndex

Return the index of the variable with the given name.

Equations

• ctx.findIndex? v = ctx.nameMap.get? v

def StrataDDM.GlobalContext.nameOf? (ctx : GlobalContext) (idx : FreeVarIndex) : Option String

Equations

• ctx.nameOf? idx = Option.map (fun (x : StrataDDM.Var × StrataDDM.GlobalKind) => x.fst) ctx.vars[idx]?

def StrataDDM.GlobalContext.kindOf! (ctx : GlobalContext) (idx : FreeVarIndex) : GlobalKind

Equations

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

def StrataDDM.GlobalContext.expandFunctionTemplates (dialectName : String) (src : SourceRange) (datatypeName : String) (datatypeType : TypeExpr) (constructorInfo : Array ConstructorInfo) (templates : Array FunctionTemplate) (gctx : GlobalContext) : GlobalContext × Array String

Register constructor signatures and expand function templates for a datatype, returning the updated GlobalContext and any error messages.

dialectName is the dialect that owns the @[declareDatatype]-annotated operator. It is used to qualify builtin type references in templates (e.g., .builtin "bool" resolves to ⟨dialectName, "bool"⟩).

Equations

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

def StrataDDM.GlobalContext.addCommand (dialects : DialectMap) (gctx : GlobalContext) (op : Operation) : Except String GlobalContext

Equations

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

def StrataDDM.computeGlobalContext (dialects : DialectMap) (commands : Array Operation) : Except String GlobalContext

Equations

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

structure StrataDDM.Program : Type

• dialects : DialectMap

  Map from dialect names to the dialect definition.

• dialect : DialectName

  Main dialect for program.

• commands : Array Operation

  Top level commands in file.

• globalContext : GlobalContext

  Final global context for program.

@[implicit_reducible]

instance StrataDDM.Program.instBEq : BEq Program

Equations

• StrataDDM.Program.instBEq = { beq := fun (x y : StrataDDM.Program) => x.dialect == y.dialect && x.commands == y.commands }

@[implicit_reducible]

instance StrataDDM.Program.instInhabited : Inhabited Program

Equations

• StrataDDM.Program.instInhabited = { default := StrataDDM.Program.instInhabited._private_1 }

def StrataDDM.Program.addCommand (env : Program) (cmd : Operation) : Program

Equations

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

def StrataDDM.Program.create (dialects : DialectMap) (dialect : DialectName) (commands : Array Operation) : Program

This creates a program. It is added in addition to Program.mk to simplify the ToExpr Program instance.

Equations

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

def StrataDDM.tacticSizeOf_op_arg_dec : Lean.ParserDescr

This tactic, added to the decreasing_trivial toolbox, proves that sizeOf a < sizeOf as when a ∈ as, which is useful for well founded recursions over a nested inductive like inductive T | mk : List T → T.

Equations

• StrataDDM.tacticSizeOf_op_arg_dec = Lean.ParserDescr.node `StrataDDM.tacticSizeOf_op_arg_dec 1024 (Lean.ParserDescr.nonReservedSymbol "sizeOf_op_arg_dec" false)