Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



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



class PatternFrom a b where Source

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


patternFrom :: Int -> a -> TCM b Source

type NLM = ExceptT Blocked_ (StateT NLMState ReduceM) Source

Monad for non-linear matching.

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

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

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

data PostponedEquation Source

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




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.


class Match a b where Source

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


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


Match NLPat Term Source 
Match a b => Match [a] [b] Source 
Match a b => Match (Type' a) (Type' b) Source 
(Match a b, Subst b, Free b, PrettyTCM a, PrettyTCM b) => Match (Abs a) (Abs b) Source 
Match a b => Match (Elim' a) (Elim' b) Source 
Match a b => Match (Dom a) (Dom b) Source 
Match a b => Match (Arg a) (Arg b) Source 

equal :: Term -> Term -> ReduceM Bool Source

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