ModuleAgda-2.7.0.1Haskell2010

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

5 types
1 class
12 values

PackageAgda-2.7.0.1
Exports18
LanguageHaskell2010
LicenceMIT
SourceNonLinMatch.hs

newtypenewtype NLM a

Monad for non-linear matching.

Constructors

NLM
- unNLM :: ExceptT Blocked_ (StateT NLMState ReduceM) a

Instances18Monad, Functor, MonadFail, Applicative, Alternative, MonadPlus, …

Monad NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
Functor NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
MonadFail NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
Applicative NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
Alternative NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
MonadPlus NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
HasOptions NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
MonadBlock NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
MonadReduce NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
MonadTCEnv NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
ReadTCState NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
HasBuiltins NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
MonadAddContext NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
MonadDebug NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
PureTCM NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
HasConstInfo NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
MonadError Blocked_ NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
MonadState NLMState NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch

datadata NLMState

Constructors

NLMState
- _nlmSub :: Sub
- _nlmEqs :: PostponedEquations

Instances2Null, MonadState

Null NLMStateDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
MonadState NLMState NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch

valuenlmSub :: Lens' NLMState Sub

valuenlmEqs :: Lens' NLMState PostponedEquations

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

valuematchingBlocked :: Blocked_ -> NLM ()

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

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

valuetellEq :: Telescope -> Context -> Type -> Term -> Term -> NLM ()

typetype Sub = IntMap (Relevance, Term)

datadata PostponedEquation

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

Constructors

PostponedEquation
- eqFreeVars :: Context
  Context 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.

typetype PostponedEquations = [PostponedEquation]

classclass Match a b where

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

Methods

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

Instances7Match, …

Match NLPSort SortDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
Match NLPType TypeDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
Match NLPat LevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
Match NLPat TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
Match [Elim' NLPat] ElimsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
Match a b => Match (Arg a) (Arg b)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
Match a b => Match (Dom a) (Dom b)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch

valueextendContext

:: MonadAddContext m
=> Context
-> ArgName
-> Dom Type
-> m Context

valuemakeSubstitution :: Telescope -> Sub -> Maybe Substitution

valuecheckPostponedEquations

valuenonLinMatch

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

valueequal :: 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)

valuegetTypedHead :: 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)