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 t a b where

Turn a term into a non-linear pattern, treating the free variables as pattern variables. The first argument indicates the relevance we are working under: if this is Irrelevant, then we construct a pattern that never fails to match. The second argument is the number of bound variables (from pattern lambdas). The third argument is the type of the term.

Methods

patternFrom :: Relevance -> Int -> t -> a -> TCM b

Instances

PatternFrom () Sort NLPat

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> () -> Sort -> TCM NLPat

PatternFrom () Type NLPType

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> () -> Type -> TCM NLPType

PatternFrom Type Term NLPat

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> Type -> Term -> TCM NLPat

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> t -> Dom a -> TCM (Dom b)

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> Dom t -> Arg a -> TCM (Arg b)

PatternFrom (Type, Term) Elims [Elim' NLPat]

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternFrom :: Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat]

type NLM = ExceptT Blocked_ (StateT NLMState ReduceM)

Monad for non-linear matching.

data NLMState

Constructors

NLMState

Fields

• _nlmSub :: Sub
• _nlmEqs :: PostponedEquations

Instances

Null NLMState

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

empty :: NLMState

null :: NLMState -> Bool

nlmSub :: Lens' Sub NLMState

nlmEqs :: Lens' PostponedEquations NLMState

runNLM :: MonadReduce m => NLM () -> m (Either Blocked_ NLMState)

matchingBlocked :: Blocked_ -> NLM ()

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

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

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

type Sub = IntMap (Relevance, 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 :: Telescope

  Telescope 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.

type PostponedEquations = [PostponedEquation]

class Match t a b where

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

Methods

match

Arguments

:: Relevance

Are we currently matching in an irrelevant context?

-> Telescope

The telescope of pattern variables

-> Telescope

The telescope of lambda-bound variables

-> t

The type of the pattern

-> a

The pattern to match

-> b

The term to be matched against the pattern

-> NLM ()

Instances

Match () NLPType Type

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPType -> Type -> NLM ()

Match () NLPat Level

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPat -> Level -> NLM ()

Match () NLPat Sort

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPat -> Sort -> NLM ()

Match Type NLPat Term

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM ()

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> t -> Dom a -> Dom b -> NLM ()

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Dom t -> Arg a -> Arg b -> NLM ()

Match (Type, Term) [Elim' NLPat] Elims

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> (Type, Term) -> [Elim' NLPat] -> Elims -> NLM ()

reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a) => IntSet -> a -> m (Either Blocked_ (Maybe a))

makeSubstitution :: Telescope -> Sub -> Substitution

checkPostponedEquations :: (MonadReduce m, HasConstInfo m, MonadDebug m) => Substitution -> PostponedEquations -> m (Maybe Blocked_)

nonLinMatch :: (MonadReduce m, HasConstInfo m, MonadDebug m, Match t a b) => Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)

equal :: (MonadReduce m, HasConstInfo m) => Term -> Term -> m (Maybe Blocked_)

Untyped βη-equality, does not handle things like empty record types. Returns Nothing if the terms are equal, or `Just b` if the terms are not (where b contains information about possible metas blocking the comparison)