Agda.TypeChecking.Rewriting.NonLinMatch

Non-linear matching of the lhs of a rewrite rule against a neutral term.

Given a lhs

Δ ⊢ lhs : B

and a candidate term

Γ ⊢ t : A

we seek a substitution Γ ⊢ σ : Δ such that

Γ ⊢ B[σ] = A and Γ ⊢ lhs[σ] = t : A

Documentation

class PatternFrom a b where

Turn a term into a non-linear pattern, treating the free variables as pattern variables. The first argument is the number of bound variables.

Methods

patternFrom :: Int -> a -> TCM b

Instances

PatternFrom Term NLPat

PatternFrom a b => PatternFrom [a] [b]

PatternFrom a b => PatternFrom (Type' a) (Type' b)

PatternFrom a b => PatternFrom (Abs a) (Abs b)

PatternFrom a b => PatternFrom (Elim' a) (Elim' b)

PatternFrom a b => PatternFrom (Dom a) (Dom b)

PatternFrom a b => PatternFrom (Arg a) (Arg b)

type NLM = ExceptT Blocked_ (StateT NLMState ReduceM)

Monad for non-linear matching.

type NLMState = (Sub, PostponedEquations)

liftRed :: ReduceM a -> NLM a

runNLM :: NLM () -> ReduceM (Either Blocked_ NLMState)

traceSDocNLM :: VerboseKey -> Int -> TCM Doc -> NLM a -> NLM a

matchingBlocked :: Blocked_ -> NLM ()

tellSub :: Int -> Term -> NLM ()

Add substitution i |-> v to result of matching.

tellEq :: Int -> Term -> Term -> NLM ()

type Sub = IntMap Term

data PostponedEquation

Matching against a term produces a constraint which we have to verify after applying the substitution computed by matching.

Constructors

PostponedEquation

Fields

eqFreeVars :: Int

Number of free variables in the equation

eqLhs :: Term

Term from pattern, living in pattern context.

eqRhs :: Term

Term from scrutinee, living in context where matching was invoked.

Instances

HasOptions NLM

type PostponedEquations = [PostponedEquation]

class Match a b where

Match a non-linear pattern against a neutral term, returning a substitution.

Methods

match :: Int -> a -> b -> NLM ()

Instances

Match NLPat Term

Match a b => Match [a] [b]

Match a b => Match (Type' a) (Type' b)

(Match a b, Subst b, Free b, PrettyTCM a, PrettyTCM b) => Match (Abs a) (Abs b)

Match a b => Match (Elim' a) (Elim' b)

Match a b => Match (Dom a) (Dom b)

Match a b => Match (Arg a) (Arg b)

makeSubstitution :: Sub -> Substitution

checkPostponedEquations :: Substitution -> PostponedEquations -> ReduceM Bool

nonLinMatch :: Match a b => a -> b -> ReduceM (Either Blocked_ Substitution)

equal :: Term -> Term -> ReduceM Bool

Untyped βη-equality, does not handle things like empty record types.