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 (from pattern lambdas).

Minimal complete definition

patternFrom

Methods

patternFrom :: Int -> a -> TCM b

Instances

PatternFrom Term NLPat

Methods

patternFrom :: Int -> Term -> TCM NLPat

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

Methods

patternFrom :: Int -> [a] -> TCM [b]

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

Methods

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

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

Methods

patternFrom :: Int -> Arg a -> TCM (Arg b)

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

Methods

patternFrom :: Int -> Type' a -> TCM (Type' b)

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

Methods

patternFrom :: Int -> Abs a -> TCM (Abs b)

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

Methods

patternFrom :: Int -> Elim' a -> TCM (Elim' 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 :: Telescope -> Telescope -> 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 :: 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.

Instances

HasOptions NLM

Methods

pragmaOptions :: NLM PragmaOptions

commandLineOptions :: NLM CommandLineOptions

type PostponedEquations = [PostponedEquation]

class Match a b where

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

Minimal complete definition

match

Methods

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

Instances

Match NLPat Term

Methods

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

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

Methods

match :: Telescope -> Telescope -> [a] -> [b] -> NLM ()

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

Methods

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

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

Methods

match :: Telescope -> Telescope -> Arg a -> Arg b -> NLM ()

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

Methods

match :: Telescope -> Telescope -> Type' a -> Type' b -> NLM ()

(Match a b, Subst t1 a, Subst t2 b) => Match (Abs a) (Abs b)

Methods

match :: Telescope -> Telescope -> Abs a -> Abs b -> NLM ()

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

Methods

match :: Telescope -> Telescope -> Elim' a -> Elim' b -> NLM ()

makeSubstitution :: Telescope -> Sub -> Substitution

checkPostponedEquations :: Substitution -> PostponedEquations -> ReduceM Bool

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

equal :: Term -> Term -> ReduceM Bool

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

class RaiseNLP a where

Raise (bound) variables in a NLPat

Minimal complete definition

raiseNLPFrom

Methods

raiseNLPFrom :: Int -> Int -> a -> a

raiseNLP :: Int -> a -> a

Instances

RaiseNLP NLPat

Methods

raiseNLPFrom :: Int -> Int -> NLPat -> NLPat

raiseNLP :: Int -> NLPat -> NLPat

RaiseNLP a => RaiseNLP [a]

Methods

raiseNLPFrom :: Int -> Int -> [a] -> [a]

raiseNLP :: Int -> [a] -> [a]

RaiseNLP a => RaiseNLP (Dom a)

Methods

raiseNLPFrom :: Int -> Int -> Dom a -> Dom a

raiseNLP :: Int -> Dom a -> Dom a

RaiseNLP a => RaiseNLP (Arg a)

Methods

raiseNLPFrom :: Int -> Int -> Arg a -> Arg a

raiseNLP :: Int -> Arg a -> Arg a

RaiseNLP a => RaiseNLP (Type' a)

Methods

raiseNLPFrom :: Int -> Int -> Type' a -> Type' a

raiseNLP :: Int -> Type' a -> Type' a

RaiseNLP a => RaiseNLP (Abs a)

Methods

raiseNLPFrom :: Int -> Int -> Abs a -> Abs a

raiseNLP :: Int -> Abs a -> Abs a

RaiseNLP a => RaiseNLP (Elim' a)

Methods

raiseNLPFrom :: Int -> Int -> Elim' a -> Elim' a

raiseNLP :: Int -> Elim' a -> Elim' a