This module implements a simple E-matching procedure as a backtracking search.
We represent an E-matching
problem as a list of constraints.
- match
(gen? : Option GenPatternInfo)
(pat e : Expr)
: Cnstr
Matches pattern
pat
with terme
- offset
(gen? : Option GenPatternInfo)
(pat : Expr)
(k : Nat)
(e : Expr)
: Cnstr
Matches offset pattern
pat+k
with terme
- continue
(pat : Expr)
: Cnstr
This constraint is used to encode multi-patterns.
Instances For
Choice point for the backtracking search. The state of the procedure contains a stack of choices.
Constraints to be processed.
- gen : Nat
Maximum term generation found so far.
Partial assignment so far. Recall that pattern variables are encoded as de-Bruijn variables.
Instances For
Context for the E-matching monad.
- useMT : Bool
useMT
istrue
if we are using the mod-time optimization. It is always set to false for newEMatchTheorem
s. - thm : EMatchTheorem
EMatchTheorem
being processed. - initApp : Expr
Initial application used to start E-matching
Instances For
State for the E-matching monad
Choices that still have to be processed.
Instances For
Equations
Instances For
Equations
Instances For
Performs one round of E-matching, and returns true
if new instances were generated.