def MeTTaIL.AST.matchPat : AST → AST → List (String × AST) → Option (List (String × AST))

First-order matching of a pattern against a term, threading the variable bindings. A pattern variable matches any subterm (and must match consistently if it recurs); constructors match structurally; everything else matches only itself.

Equations

• One or more equations did not get rendered due to their size.
• (MeTTaIL.AST.sexp l ps).matchPat (MeTTaIL.AST.sexp m ts) x✝ = if (l == m) = true then MeTTaIL.AST.matchPatList ps ts x✝ else none
• (pb.subst pr pv).matchPat (tb.subst tr tv) x✝ = if (pv == tv) = true then (pb.matchPat tb x✝).bind (pr.matchPat tr) else none
• x✝².matchPat x✝¹ x✝ = if (x✝² == x✝¹) = true then some x✝ else none

def MeTTaIL.AST.matchPatList : List AST → List AST → List (String × AST) → Option (List (String × AST))

Match a list of patterns against a list of terms, pointwise.

Equations

• MeTTaIL.AST.matchPatList [] [] x✝ = some x✝
• MeTTaIL.AST.matchPatList (p :: ps) (t :: ts) x✝ = (p.matchPat t x✝).bind (MeTTaIL.AST.matchPatList ps ts)
• MeTTaIL.AST.matchPatList x✝² x✝¹ x✝ = none

def MeTTaIL.AST.subst1 (v : DottedPath) (repl : AST) : AST → AST

Substitute repl for the variable v in a term. The Subst node's own variable is not a binder in the term tree (binders live in the grammar, not the AST), so this is plain replacement.

Equations

• MeTTaIL.AST.subst1 v repl (MeTTaIL.AST.var p) = if (p == v) = true then repl else MeTTaIL.AST.var p
• MeTTaIL.AST.subst1 v repl (MeTTaIL.AST.sexp l args) = MeTTaIL.AST.sexp l (MeTTaIL.AST.subst1List v repl args)
• MeTTaIL.AST.subst1 v repl (b.subst r w) = (MeTTaIL.AST.subst1 v repl b).subst (MeTTaIL.AST.subst1 v repl r) w

def MeTTaIL.AST.subst1List (v : DottedPath) (repl : AST) : List AST → List AST

Substitute through a list of terms.

Equations

• MeTTaIL.AST.subst1List v repl [] = []
• MeTTaIL.AST.subst1List v repl (a :: as) = MeTTaIL.AST.subst1 v repl a :: MeTTaIL.AST.subst1List v repl as

def MeTTaIL.AST.inst (bnds : List (String × AST)) : AST → AST

Instantiate a term with variable bindings, resolving any Subst node. For Subst body repl w, if the pattern variable w is bound to a term variable, substitution targets that variable's path (the bound name); otherwise it targets w directly.

Equations

• One or more equations did not get rendered due to their size.
• MeTTaIL.AST.inst bnds (MeTTaIL.AST.var p) = MeTTaIL.AST.var p
• MeTTaIL.AST.inst bnds (MeTTaIL.AST.sexp l args) = MeTTaIL.AST.sexp l (MeTTaIL.AST.instList bnds args)
• MeTTaIL.AST.inst bnds (b.subst r w) = MeTTaIL.AST.subst1 w (MeTTaIL.AST.inst bnds r) (MeTTaIL.AST.inst bnds b)

def MeTTaIL.AST.instList (bnds : List (String × AST)) : List AST → List AST

Instantiate a list of terms.

Equations

• MeTTaIL.AST.instList bnds [] = []
• MeTTaIL.AST.instList bnds (a :: as) = MeTTaIL.AST.inst bnds a :: MeTTaIL.AST.instList bnds as

def MeTTaIL.applyBaseRewrite (rd : RewriteDecl) (t : AST) : Option AST

Apply a base rewrite (one with no premises) to a term: match its left-hand side, then instantiate its right-hand side. Returns none if the rewrite has premises or does not match.

Equations

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

def MeTTaIL.baseReducts (p : Presentation) (t : AST) : List AST

The base-rewrite reducts of a term in a presentation: every result of applying a premise-free rewrite whose left-hand side matches at the top level.

Equations

• MeTTaIL.baseReducts p t = List.filterMap (fun (rd : MeTTaIL.RewriteDecl) => MeTTaIL.applyBaseRewrite rd t) p.rewrites