def MeTTaIL.distinct {α : Type} [BEq α] (xs : List α) : List α

Keep the first occurrence of each element, dropping later duplicates. The analogue of Scala List.distinct.

Equations

• MeTTaIL.distinct xs = List.foldl (fun (acc : List α) (x : α) => if acc.contains x = true then acc else acc ++ [x]) [] xs

def MeTTaIL.Item.isTerminal : Item → Bool

Whether an item is a terminal (a literal token).

Equations

• (MeTTaIL.Item.terminal s).isTerminal = true
• x✝.isTerminal = false

def MeTTaIL.Rule.nonTerminalItems (r : Rule) : List Item

The non-terminal items of a rule: everything that is not a literal token, so plain non-terminals and the two binder forms. Mirrors Scala AddEqRwHelpers.nonTerminals, used for the arity and category-alignment checks on replacements.

Equations

• r.nonTerminalItems = List.filter (fun (i : MeTTaIL.Item) => !i.isTerminal) r.items

def MeTTaIL.Item.cats : Item → List Cat

The sort of a plain non-terminal item, and nothing for a terminal or a binder. This is the category Scala collects with collect { case nt: NTerminal => nt.cat_ } in handleConj, handleSubtract, and checkAddTerms; binder items are deliberately not counted, matching Scala.

Equations

• (MeTTaIL.Item.nterminal c).cats = [c]
• x✝.cats = []

def MeTTaIL.Rule.mentionedCats (r : Rule) : List Cat

The categories a function symbol mentions for the intersection and difference filters and the unknown-category check: its output sort and the sorts of its plain non-terminal items. Mirrors the set Set(rule.cat_) ++ {nterminal item cats} Scala builds in handleConj, handleSubtract, and checkAddTerms.

Equations

• r.mentionedCats = r.cat :: List.flatMap MeTTaIL.Item.cats r.items

def MeTTaIL.AST.topLabels : AST → List Label

The head label of a term, if it is an applied constructor; nothing for a variable or a substitution.

Equations

• (MeTTaIL.AST.var path).topLabels = []
• (MeTTaIL.AST.sexp l args).topLabels = [l]
• (body.subst repl v).topLabels = []

def MeTTaIL.Equation.labels : Equation → List Label

The (top-level) labels appearing in an equation. Mirrors Scala labelsInEquation: it recurses through a freshness guard, and on each side takes only the head label (Scala's per-term labelsInAST is non-recursive).

Equations

• (MeTTaIL.Equation.impl l r).labels = l.topLabels ++ r.topLabels
• (MeTTaIL.Equation.fresh x_1 y e).labels = e.labels

def MeTTaIL.Rewrite.conclusion : Rewrite → AST × AST

Strip the premises (let h in ...) of a rewrite to its conclusion lhs ~> rhs. Mirrors ASTHelpers.rewriteBase.

Equations

• (MeTTaIL.Rewrite.base l r).conclusion = (l, r)
• (MeTTaIL.Rewrite.ctx h r).conclusion = r.conclusion

def MeTTaIL.RewriteDecl.labels (rd : RewriteDecl) : List Label

The (top-level) labels appearing in a rewrite's conclusion.

Equations

• rd.labels = match rd.rw.conclusion with | (l, r) => l.topLabels ++ r.topLabels

def MeTTaIL.Presentation.union (pa pb : Presentation) : Presentation

Union of two presentations: concatenate each component and keep first occurrences. Mirrors handleDisj (the \/ operator), which builds a fresh presentation with empty references (as the intersection and difference operators do).

Equations

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

def MeTTaIL.Presentation.inter (pa pb : Presentation) : Presentation

Intersection of two presentations, filtered to common sorts and surviving labels. Mirrors handleConj (the /\ operator): keep sorts in both; keep defs in both whose mentioned categories are all common; keep equations/rewrites in both whose labels all survive.

Equations

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

def MeTTaIL.Presentation.diff (pa pb : Presentation) : Presentation

Difference of two presentations. Mirrors handleSubtract (the \ operator): remove pb's sorts; drop defs that are in pb or that mention a removed sort; keep equations/rewrites not in pb whose labels all survive.

Equations

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

def MeTTaIL.DottedPath.baseName : DottedPath → String

The base identifier of a dotted path: the variable name it heads. A premise src ~> tgt binds tgt's base identifier.

Equations

• (MeTTaIL.DottedPath.base n).baseName = n
• (MeTTaIL.DottedPath.qualified n rest).baseName = n

def MeTTaIL.Rewrite.premises : Rewrite → List Hyp

The premises (the let h in ... hypotheses) of a rewrite, outermost first.

Equations

• (MeTTaIL.Rewrite.base l r).premises = []
• (MeTTaIL.Rewrite.ctx h r).premises = h :: r.premises