inductive MeTTaIL.DottedPath : Type

A dotted path of identifiers, e.g. a.b.c. Mirrors BNFC DottedPath (BaseDottedPath Ident | QualifiedDottedPath Ident DottedPath).

• base (ident : String) : DottedPath
• qualified (ident : String) (rest : DottedPath) : DottedPath

@[implicit_reducible]

instance MeTTaIL.instInhabitedDottedPath : Inhabited DottedPath

Equations

• MeTTaIL.instInhabitedDottedPath = { default := MeTTaIL.instInhabitedDottedPath.default }

def MeTTaIL.instBEqDottedPath.beq : DottedPath → DottedPath → Bool

Equations

• MeTTaIL.instBEqDottedPath.beq (MeTTaIL.DottedPath.base a) (MeTTaIL.DottedPath.base b) = (a == b)
• MeTTaIL.instBEqDottedPath.beq (MeTTaIL.DottedPath.qualified a a_1) (MeTTaIL.DottedPath.qualified b b_1) = (a == b && MeTTaIL.instBEqDottedPath.beq a_1 b_1)
• MeTTaIL.instBEqDottedPath.beq x✝¹ x✝ = false

@[implicit_reducible]

instance MeTTaIL.instBEqDottedPath : BEq DottedPath

Equations

• MeTTaIL.instBEqDottedPath = { beq := MeTTaIL.instBEqDottedPath.beq }

@[implicit_reducible]

instance MeTTaIL.instDecidableEqDottedPath : DecidableEq DottedPath

Equations

• MeTTaIL.instDecidableEqDottedPath = MeTTaIL.instDecidableEqDottedPath.decEq

def MeTTaIL.instDecidableEqDottedPath.decEq (x✝ x✝¹ : DottedPath) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• MeTTaIL.instDecidableEqDottedPath.decEq (MeTTaIL.DottedPath.base a) (MeTTaIL.DottedPath.base b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• MeTTaIL.instDecidableEqDottedPath.decEq (MeTTaIL.DottedPath.base ident) (MeTTaIL.DottedPath.qualified ident_1 rest) = isFalse ⋯
• MeTTaIL.instDecidableEqDottedPath.decEq (MeTTaIL.DottedPath.qualified ident rest) (MeTTaIL.DottedPath.base ident_1) = isFalse ⋯

def MeTTaIL.instReprDottedPath.repr : DottedPath → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance MeTTaIL.instReprDottedPath : Repr DottedPath

Equations

• MeTTaIL.instReprDottedPath = { reprPrec := MeTTaIL.instReprDottedPath.repr }

inductive MeTTaIL.Cat : Type

A sort / category, i.e. an arity expression. The arity language is the generating shapes closed under lists, exponentials (arrow), and products. Mirrors BNFC Cat (IdCat | ListOfCat | ArrowCat | ProdCat).

• idCat (name : String) : Cat
• listOf (c : Cat) : Cat
• arrow (dom cod : Cat) : Cat
• prod (cs : List Cat) : Cat

@[implicit_reducible]

instance MeTTaIL.instInhabitedCat : Inhabited Cat

Equations

• MeTTaIL.instInhabitedCat = { default := MeTTaIL.instInhabitedCat.default }

def MeTTaIL.Cat.beq : Cat → Cat → Bool

Structural equality on categories, the analogue of the Scala Cat.equals. Hand-written because Cat nests through List Cat in prod, which deriving BEq does not support.

Equations

• (MeTTaIL.Cat.idCat a).beq (MeTTaIL.Cat.idCat b) = (a == b)
• a.listOf.beq b.listOf = a.beq b
• (a.arrow b).beq (c.arrow d) = (a.beq c && b.beq d)
• (MeTTaIL.Cat.prod cs).beq (MeTTaIL.Cat.prod ds) = MeTTaIL.Cat.beqList cs ds
• x✝¹.beq x✝ = false

def MeTTaIL.Cat.beqList : List Cat → List Cat → Bool

Pointwise structural equality on category lists (the prod arguments).

Equations

• MeTTaIL.Cat.beqList [] [] = true
• MeTTaIL.Cat.beqList (c :: cs) (d :: ds) = (c.beq d && MeTTaIL.Cat.beqList cs ds)
• MeTTaIL.Cat.beqList x✝¹ x✝ = false

@[implicit_reducible]

instance MeTTaIL.instBEqCat : BEq Cat

Equations

• MeTTaIL.instBEqCat = { beq := MeTTaIL.Cat.beq }

inductive MeTTaIL.Label : Type

A constructor label. Mirrors BNFC Label (Id | Wild | ListE | ListCons | ListOne). The list labels carry the element category of the list sort they construct.

• id (name : String) : Label
• wild : Label
• listE (c : Cat) : Label
• listCons (c : Cat) : Label
• listOne (c : Cat) : Label

@[implicit_reducible]

instance MeTTaIL.instInhabitedLabel : Inhabited Label

Equations

• MeTTaIL.instInhabitedLabel = { default := MeTTaIL.instInhabitedLabel.default }

@[implicit_reducible]

instance MeTTaIL.instBEqLabel : BEq Label

Equations

• MeTTaIL.instBEqLabel = { beq := MeTTaIL.instBEqLabel.beq }

def MeTTaIL.instBEqLabel.beq : Label → Label → Bool

Equations

• MeTTaIL.instBEqLabel.beq (MeTTaIL.Label.id a) (MeTTaIL.Label.id b) = (a == b)
• MeTTaIL.instBEqLabel.beq MeTTaIL.Label.wild MeTTaIL.Label.wild = true
• MeTTaIL.instBEqLabel.beq (MeTTaIL.Label.listE a) (MeTTaIL.Label.listE b) = (a == b)
• MeTTaIL.instBEqLabel.beq (MeTTaIL.Label.listCons a) (MeTTaIL.Label.listCons b) = (a == b)
• MeTTaIL.instBEqLabel.beq (MeTTaIL.Label.listOne a) (MeTTaIL.Label.listOne b) = (a == b)
• MeTTaIL.instBEqLabel.beq x✝¹ x✝ = false

inductive MeTTaIL.Item : Type

One item in a function symbol's concrete syntax. Mirrors BNFC Item. terminal is a literal; nterminal is a sort argument; absNTerminal x it is the abstraction (x) it with x bound in it; bindNTerminal x c is (Bind x c). The absNTerminal/bindNTerminal pair encodes a higher-order (exponential) argument.

• terminal (s : String) : Item
• nterminal (c : Cat) : Item
• absNTerminal (x : String) (it : Item) : Item
• bindNTerminal (x : String) (c : Cat) : Item

@[implicit_reducible]

instance MeTTaIL.instInhabitedItem : Inhabited Item

Equations

• MeTTaIL.instInhabitedItem = { default := MeTTaIL.instInhabitedItem.default }

def MeTTaIL.instBEqItem.beq : Item → Item → Bool

Equations

• MeTTaIL.instBEqItem.beq (MeTTaIL.Item.terminal a) (MeTTaIL.Item.terminal b) = (a == b)
• MeTTaIL.instBEqItem.beq (MeTTaIL.Item.nterminal a) (MeTTaIL.Item.nterminal b) = (a == b)
• MeTTaIL.instBEqItem.beq (MeTTaIL.Item.absNTerminal a a_1) (MeTTaIL.Item.absNTerminal b b_1) = (a == b && MeTTaIL.instBEqItem.beq a_1 b_1)
• MeTTaIL.instBEqItem.beq (MeTTaIL.Item.bindNTerminal a a_1) (MeTTaIL.Item.bindNTerminal b b_1) = (a == b && a_1 == b_1)
• MeTTaIL.instBEqItem.beq x✝¹ x✝ = false

@[implicit_reducible]

instance MeTTaIL.instBEqItem : BEq Item

Equations

• MeTTaIL.instBEqItem = { beq := MeTTaIL.instBEqItem.beq }

structure MeTTaIL.Rule : Type

A function symbol, written as a grammar rule label . cat ::= items. cat is the output arity; the input arity is read off the non-terminal items. Mirrors BNFC Rule . Def.

• label : Label
• cat : Cat
• items : List Item

@[implicit_reducible]

instance MeTTaIL.instInhabitedRule : Inhabited Rule

Equations

• MeTTaIL.instInhabitedRule = { default := MeTTaIL.instInhabitedRule.default }

@[implicit_reducible]

instance MeTTaIL.instBEqRule : BEq Rule

Equations

• MeTTaIL.instBEqRule = { beq := MeTTaIL.instBEqRule.beq }

def MeTTaIL.instBEqRule.beq : Rule → Rule → Bool

Equations

• MeTTaIL.instBEqRule.beq { label := a, cat := a_1, items := a_2 } { label := b, cat := b_1, items := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• MeTTaIL.instBEqRule.beq x✝¹ x✝ = false

inductive MeTTaIL.AST : Type

A term. Mirrors BNFC AST: var is a (possibly qualified) variable, sexp label args is an applied constructor (label args...), and subst body repl v is the built-in capture-avoiding substitution (Subst body repl v) that drives the COMM rule.

• var (path : DottedPath) : AST
• sexp (label : Label) (args : List AST) : AST
• subst (body repl : AST) (v : DottedPath) : AST

@[implicit_reducible]

instance MeTTaIL.instInhabitedAST : Inhabited AST

Equations

• MeTTaIL.instInhabitedAST = { default := MeTTaIL.instInhabitedAST.default }

def MeTTaIL.AST.beq : AST → AST → Bool

Structural equality on terms, the analogue of the Scala AST.equals. Hand-written because AST nests through List AST in sexp.

Equations

• (MeTTaIL.AST.var p).beq (MeTTaIL.AST.var q) = (p == q)
• (MeTTaIL.AST.sexp l cs).beq (MeTTaIL.AST.sexp m ds) = (l == m && MeTTaIL.AST.beqList cs ds)
• (b.subst r v).beq (b'.subst r' v') = (b.beq b' && r.beq r' && v == v')
• x✝¹.beq x✝ = false

def MeTTaIL.AST.beqList : List AST → List AST → Bool

Pointwise structural equality on term lists (the sexp arguments).

Equations

• MeTTaIL.AST.beqList [] [] = true
• MeTTaIL.AST.beqList (c :: cs) (d :: ds) = (c.beq d && MeTTaIL.AST.beqList cs ds)
• MeTTaIL.AST.beqList x✝¹ x✝ = false

@[implicit_reducible]

instance MeTTaIL.instBEqAST : BEq AST

Equations

• MeTTaIL.instBEqAST = { beq := MeTTaIL.AST.beq }

inductive MeTTaIL.Equation : Type

An equation, optionally guarded by a freshness side condition if x # y then .... Mirrors BNFC Equation (EquationImpl | EquationFresh).

• impl (lhs rhs : AST) : Equation
• fresh (x y : String) (e : Equation) : Equation

@[implicit_reducible]

instance MeTTaIL.instInhabitedEquation : Inhabited Equation

Equations

• MeTTaIL.instInhabitedEquation = { default := MeTTaIL.instInhabitedEquation.default }

def MeTTaIL.instBEqEquation.beq : Equation → Equation → Bool

Equations

• MeTTaIL.instBEqEquation.beq (MeTTaIL.Equation.impl a a_1) (MeTTaIL.Equation.impl b b_1) = (a == b && a_1 == b_1)
• MeTTaIL.instBEqEquation.beq (MeTTaIL.Equation.fresh a a_1 a_2) (MeTTaIL.Equation.fresh b b_1 b_2) = (a == b && (a_1 == b_1 && MeTTaIL.instBEqEquation.beq a_2 b_2))
• MeTTaIL.instBEqEquation.beq x✝¹ x✝ = false

@[implicit_reducible]

instance MeTTaIL.instBEqEquation : BEq Equation

Equations

• MeTTaIL.instBEqEquation = { beq := MeTTaIL.instBEqEquation.beq }

structure MeTTaIL.Hyp : Type

A rewrite premise src ~> tgt over dotted-path variables. Mirrors BNFC Hyp . Hypothesis.

• src : DottedPath
• tgt : DottedPath

@[implicit_reducible]

instance MeTTaIL.instInhabitedHyp : Inhabited Hyp

Equations

• MeTTaIL.instInhabitedHyp = { default := MeTTaIL.instInhabitedHyp.default }

def MeTTaIL.instBEqHyp.beq : Hyp → Hyp → Bool

Equations

• MeTTaIL.instBEqHyp.beq { src := a, tgt := a_1 } { src := b, tgt := b_1 } = (a == b && a_1 == b_1)
• MeTTaIL.instBEqHyp.beq x✝¹ x✝ = false

@[implicit_reducible]

instance MeTTaIL.instBEqHyp : BEq Hyp

Equations

• MeTTaIL.instBEqHyp = { beq := MeTTaIL.instBEqHyp.beq }

inductive MeTTaIL.Rewrite : Type

A rewrite rule: a conclusion lhs ~> rhs, optionally under premises let h in .... Mirrors BNFC Rewrite (RewriteBase | RewriteContext).

• base (lhs rhs : AST) : Rewrite
• ctx (h : Hyp) (r : Rewrite) : Rewrite

@[implicit_reducible]

instance MeTTaIL.instInhabitedRewrite : Inhabited Rewrite

Equations

• MeTTaIL.instInhabitedRewrite = { default := MeTTaIL.instInhabitedRewrite.default }

@[implicit_reducible]

instance MeTTaIL.instBEqRewrite : BEq Rewrite

Equations

• MeTTaIL.instBEqRewrite = { beq := MeTTaIL.instBEqRewrite.beq }

def MeTTaIL.instBEqRewrite.beq : Rewrite → Rewrite → Bool

Equations

• MeTTaIL.instBEqRewrite.beq (MeTTaIL.Rewrite.base a a_1) (MeTTaIL.Rewrite.base b b_1) = (a == b && a_1 == b_1)
• MeTTaIL.instBEqRewrite.beq (MeTTaIL.Rewrite.ctx a a_1) (MeTTaIL.Rewrite.ctx b b_1) = (a == b && MeTTaIL.instBEqRewrite.beq a_1 b_1)
• MeTTaIL.instBEqRewrite.beq x✝¹ x✝ = false

structure MeTTaIL.RewriteDecl : Type

A named rewrite declaration name : rw. Mirrors BNFC RDecl . RewriteDecl.

• name : String
• rw : Rewrite

@[implicit_reducible]

instance MeTTaIL.instInhabitedRewriteDecl : Inhabited RewriteDecl

Equations

• MeTTaIL.instInhabitedRewriteDecl = { default := MeTTaIL.instInhabitedRewriteDecl.default }

def MeTTaIL.instBEqRewriteDecl.beq : RewriteDecl → RewriteDecl → Bool

Equations

• MeTTaIL.instBEqRewriteDecl.beq { name := a, rw := a_1 } { name := b, rw := b_1 } = (a == b && a_1 == b_1)
• MeTTaIL.instBEqRewriteDecl.beq x✝¹ x✝ = false

@[implicit_reducible]

instance MeTTaIL.instBEqRewriteDecl : BEq RewriteDecl

Equations

• MeTTaIL.instBEqRewriteDecl = { beq := MeTTaIL.instBEqRewriteDecl.beq }

inductive MeTTaIL.Presentation : Type

A theory presentation, the in-memory BasePres: exported sorts, function symbols (terms), equations, rewrites, and a references map (declared prefix to sub-presentation) used to validate dotted-path prefixes in rewrites.

The references field makes the type recursive, exactly as BasePres.listmapentry_ does (MakeMapEntry . MapEntry ::= Ident "=>" Pres). Our elaborate never populates it, so every presentation this development produces has empty references; the field is kept to mirror BasePres faithfully, where a literal presentation can carry references. The type is an inductive rather than a structure because Lean structures may not be recursive; named accessors are defined just below.

• mk (exports : List Cat) (terms : List Rule) (equations : List Equation) (rewrites : List RewriteDecl) (references : List (String × Presentation)) : Presentation

@[implicit_reducible]

instance MeTTaIL.instInhabitedPresentation : Inhabited Presentation

Equations

• MeTTaIL.instInhabitedPresentation = { default := MeTTaIL.instInhabitedPresentation.default }

def MeTTaIL.Presentation.beq : Presentation → Presentation → Bool

Structural equality on presentations. Hand-written because Presentation nests through List (String × Presentation) in references.

Equations

• (MeTTaIL.Presentation.mk e₁ t₁ q₁ r₁ m₁).beq (MeTTaIL.Presentation.mk e₂ t₂ q₂ r₂ m₂) = (e₁ == e₂ && t₁ == t₂ && q₁ == q₂ && r₁ == r₂ && MeTTaIL.Presentation.beqRefs m₁ m₂)

def MeTTaIL.Presentation.beqRefs : List (String × Presentation) → List (String × Presentation) → Bool

Pointwise structural equality on reference maps.

Equations

• MeTTaIL.Presentation.beqRefs [] [] = true
• MeTTaIL.Presentation.beqRefs ((s, p) :: m₁) ((t, q) :: m₂) = (s == t && p.beq q && MeTTaIL.Presentation.beqRefs m₁ m₂)
• MeTTaIL.Presentation.beqRefs x✝¹ x✝ = false

@[implicit_reducible]

instance MeTTaIL.instBEqPresentation : BEq Presentation

Equations

• MeTTaIL.instBEqPresentation = { beq := MeTTaIL.Presentation.beq }

def MeTTaIL.Presentation.exports : Presentation → List Cat

The exported sorts of a presentation (the generating shapes S).

Equations

• (MeTTaIL.Presentation.mk e terms equations rewrites references).exports = e

def MeTTaIL.Presentation.terms : Presentation → List Rule

The function symbols of a presentation (the set F, written as grammar rules).

Equations

• (MeTTaIL.Presentation.mk e terms equations rewrites references).terms = terms

def MeTTaIL.Presentation.equations : Presentation → List Equation

The equations of a presentation (the set E).

Equations

• (MeTTaIL.Presentation.mk e terms equations rewrites references).equations = equations

def MeTTaIL.Presentation.rewrites : Presentation → List RewriteDecl

The named rewrite rules of a presentation (the GSLT reduction rules).

Equations

• (MeTTaIL.Presentation.mk e terms equations rewrites references).rewrites = rewrites

def MeTTaIL.Presentation.references : Presentation → List (String × Presentation)

The references map of a presentation (declared prefix to sub-presentation).

Equations

• (MeTTaIL.Presentation.mk e terms equations rewrites references).references = references

def MeTTaIL.Presentation.empty : Presentation

The empty presentation: no exports, terms, equations, rewrites, or references. Mirrors BasePresOps.empty.

Equations

• MeTTaIL.Presentation.empty = MeTTaIL.Presentation.mk [] [] [] [] []