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

newtype NLM a

Monad for non-linear matching.

Constructors

NLM

Fields

• unNLM :: ExceptT Blocked_ (StateT NLMState ReduceM) a

Instances

HasOptions NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

pragmaOptions :: NLM PragmaOptions

commandLineOptions :: NLM CommandLineOptions

MonadBlock NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

patternViolation :: Blocker -> NLM a

catchPatternErr :: (Blocker -> NLM a) -> NLM a -> NLM a

MonadReduce NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

liftReduce :: ReduceM a -> NLM a

MonadTCEnv NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

askTC :: NLM TCEnv

localTC :: (TCEnv -> TCEnv) -> NLM a -> NLM a

ReadTCState NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

getTCState :: NLM TCState

locallyTCState :: Lens' TCState a -> (a -> a) -> NLM b -> NLM b

withTCState :: (TCState -> TCState) -> NLM a -> NLM a

HasBuiltins NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

getBuiltinThing :: SomeBuiltin -> NLM (Maybe (Builtin PrimFun))

MonadAddContext NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

addCtx :: Name -> Dom Type -> NLM a -> NLM a

addLetBinding' :: Origin -> Name -> Term -> Dom Type -> NLM a -> NLM a

updateContext :: Substitution -> (Context -> Context) -> NLM a -> NLM a

withFreshName :: Range -> ArgName -> (Name -> NLM a) -> NLM a

MonadDebug NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> NLM String

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> NLM a -> NLM a

verboseBracket :: VerboseKey -> VerboseLevel -> String -> NLM a -> NLM a

getVerbosity :: NLM Verbosity

getProfileOptions :: NLM ProfileOptions

isDebugPrinting :: NLM Bool

nowDebugPrinting :: NLM a -> NLM a

PureTCM NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

HasConstInfo NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

getConstInfo :: QName -> NLM Definition

getConstInfo' :: QName -> NLM (Either SigError Definition)

getRewriteRulesFor :: QName -> NLM RewriteRules

MonadFail NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

fail :: String -> NLM a

Alternative NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

empty :: NLM a

(<|>) :: NLM a -> NLM a -> NLM a

some :: NLM a -> NLM [a]

many :: NLM a -> NLM [a]

Applicative NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

pure :: a -> NLM a

(<*>) :: NLM (a -> b) -> NLM a -> NLM b

liftA2 :: (a -> b -> c) -> NLM a -> NLM b -> NLM c

(*>) :: NLM a -> NLM b -> NLM b

(<*) :: NLM a -> NLM b -> NLM a

Functor NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

fmap :: (a -> b) -> NLM a -> NLM b

(<$) :: a -> NLM b -> NLM a

Monad NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

(>>=) :: NLM a -> (a -> NLM b) -> NLM b

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

return :: a -> NLM a

MonadPlus NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

mzero :: NLM a

mplus :: NLM a -> NLM a -> NLM a

MonadError Blocked_ NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

throwError :: Blocked_ -> NLM a

catchError :: NLM a -> (Blocked_ -> NLM a) -> NLM a

MonadState NLMState NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

get :: NLM NLMState

put :: NLMState -> NLM ()

state :: (NLMState -> (a, NLMState)) -> NLM a

data NLMState

Constructors

NLMState

Fields

• _nlmSub :: Sub
• _nlmEqs :: PostponedEquations

Instances

Null NLMState

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

empty :: NLMState

null :: NLMState -> Bool

MonadState NLMState NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

get :: NLM NLMState

put :: NLMState -> NLM ()

state :: (NLMState -> (a, NLMState)) -> NLM a

nlmSub :: Lens' NLMState Sub

nlmEqs :: Lens' NLMState PostponedEquations

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

matchingBlocked :: Blocked_ -> NLM ()

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

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

tellEq :: Telescope -> Telescope -> Type -> 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

• eqType :: Type

  Type of the equation, living in same context as the rhs.

• 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 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

-> TypeOf b

The type of the pattern

-> a

The pattern to match

-> b

The term to be matched against the pattern

-> NLM ()

Instances

Match NLPSort Sort

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> TypeOf Sort -> NLPSort -> Sort -> NLM ()

Match NLPType Type

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

Match NLPat Level

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

Match NLPat Term

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

Match [Elim' NLPat] Elims

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> TypeOf Elims -> [Elim' NLPat] -> Elims -> NLM ()

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

makeSubstitution :: Telescope -> Sub -> Maybe Substitution

checkPostponedEquations :: PureTCM m => Substitution -> PostponedEquations -> m (Maybe Blocked_)

nonLinMatch :: (PureTCM m, Match a b) => Telescope -> TypeOf b -> a -> b -> m (Either Blocked_ Substitution)

equal :: PureTCM m => Type -> Term -> Term -> m (Maybe Blocked_)

Typed βη-equality, also handles 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)

getTypedHead :: PureTCM m => Term -> m (Maybe (QName, Type))

Utility function for getting the name and type of a head term (i.e. a Def or Con with no arguments)