def MeTTaIL.AST.vars : AST → List String

The variables occurring in a term, including the substitution target. Mirrors Scala ASTHelpers.varsInAST, which adds the target dotted-path to the variables of the body and the replacement.

Equations

• (MeTTaIL.AST.var (MeTTaIL.DottedPath.base n)).vars = [n]
• (MeTTaIL.AST.var (MeTTaIL.DottedPath.qualified n rest)).vars = [n]
• (MeTTaIL.AST.sexp label args).vars = MeTTaIL.AST.varsList args
• (b.subst r t).vars = b.vars ++ r.vars ++ [t.baseName]

def MeTTaIL.AST.varsList : List AST → List String

The variables occurring in a list of terms.

Equations

• MeTTaIL.AST.varsList [] = []
• MeTTaIL.AST.varsList (a :: as) = a.vars ++ MeTTaIL.AST.varsList as

def MeTTaIL.AST.headCat (defs : List Rule) : AST → Option Cat

The top-level category of a term given the function symbols: the labelled rule's output sort for an application, the body's category through a substitution, and none (undetermined) for a variable or a head label that names no rule.

Equations

• MeTTaIL.AST.headCat defs (MeTTaIL.AST.var path) = none
• MeTTaIL.AST.headCat defs (MeTTaIL.AST.sexp l args) = Option.map (fun (x : MeTTaIL.Rule) => x.cat) (List.find? (fun (r : MeTTaIL.Rule) => r.label == l) defs)
• MeTTaIL.AST.headCat defs (b.subst repl v) = MeTTaIL.AST.headCat defs b

def MeTTaIL.catCompatible : Option Cat → Option Cat → Bool

Two top-level categories are compatible: an undetermined side (none) matches anything, and two determined sides must be equal. A more permissive version of AddEqRwHelpers.sameCategory (see the note at the top of the file on the two cases Scala additionally rejects).

Equations

• MeTTaIL.catCompatible none x✝ = true
• MeTTaIL.catCompatible x✝ none = true
• MeTTaIL.catCompatible (some c1) (some c2) = (c1 == c2)

def MeTTaIL.checkEquation (defs : List Rule) : Equation → Option String

Check an equation: its two sides have compatible top-level categories (recursing through a freshness guard).

Equations

• One or more equations did not get rendered due to their size.
• MeTTaIL.checkEquation defs (MeTTaIL.Equation.fresh x_1 y e) = MeTTaIL.checkEquation defs e

def MeTTaIL.checkRewrite (defs : List Rule) (rd : RewriteDecl) : Option String

Check a rewrite: its two conclusion sides have compatible categories, and every right-hand-side variable is bound on the left-hand side or by a premise.

Equations

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