Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Rewriting.NonLinMatch

Description

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

Synopsis

Documentation

newtype NLM a Source #

Monad for non-linear matching.

Constructors

NLM 

Fields

Instances

Instances details
HasOptions NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

MonadBlock NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

MonadReduce NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

liftReduce :: ReduceM a -> NLM a Source #

MonadTCEnv NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

askTC :: NLM TCEnv Source #

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

ReadTCState NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

getTCState :: NLM TCState Source #

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

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

HasBuiltins NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

MonadAddContext NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

addLetBinding' :: Name -> Term -> Dom Type -> NLM a -> NLM a Source #

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

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

MonadDebug NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

PureTCM NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

HasConstInfo NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

MonadFail NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

fail :: String -> NLM a #

Alternative NLM Source # 
Instance details

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 Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

Monad NLM Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

mzero :: NLM a #

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

MonadError Blocked_ NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

throwError :: Blocked_ -> NLM a

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

MonadState NLMState NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

get :: NLM NLMState

put :: NLMState -> NLM ()

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

data NLMState Source #

Constructors

NLMState 

Instances

Instances details
Null NLMState Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

MonadState NLMState NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

get :: NLM NLMState

put :: NLMState -> NLM ()

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

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

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

data PostponedEquation Source #

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.

class Match t a b where Source #

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

Methods

match Source #

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

Instances details
Match Type NLPat Term Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

Match () NLPSort Sort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPSort -> Sort -> NLM () Source #

Match () NLPType Type Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

Match () NLPat Level Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

Match t a b => Match t (Dom a) (Dom b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

Match t a b => Match (Dom t) (Arg a) (Arg b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

Match (Type, Elims -> Term) [Elim' NLPat] Elims Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

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

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

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

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)) Source #

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