Safe Haskell	None
Language	Haskell2010

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

type NLM = ExceptT Blocked_ (StateT NLMState ReduceM)
data NLMState = NLMState {
- _nlmSub :: Sub
- _nlmEqs :: PostponedEquations
}
nlmSub :: Lens' Sub NLMState
nlmEqs :: Lens' PostponedEquations NLMState
runNLM :: MonadReduce m => NLM () -> m (Either Blocked_ NLMState)
matchingBlocked :: Blocked_ -> NLM ()
tellSub :: Relevance -> Int -> Type -> Term -> NLM ()
tellEq :: Telescope -> Telescope -> Type -> Term -> Term -> NLM ()
type Sub = IntMap (Relevance, Term)
data PostponedEquation = PostponedEquation {
- eqFreeVars :: Telescope
- eqType :: Type
- eqLhs :: Term
- eqRhs :: Term
}
type PostponedEquations = [PostponedEquation]
class Match t a b where
- match :: Relevance -> Telescope -> Telescope -> t -> a -> b -> NLM ()
reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a) => IntSet -> a -> m (Either Blocked_ (Maybe a))
makeSubstitution :: Telescope -> Sub -> Substitution
checkPostponedEquations :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, MonadDebug m) => Substitution -> PostponedEquations -> m (Maybe Blocked_)
nonLinMatch :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, MonadDebug m, Match t a b) => Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)
equal :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m) => Type -> Term -> Term -> m (Maybe Blocked_)

Documentation

type NLM = ExceptT Blocked_ (StateT NLMState ReduceM) Source #

Monad for non-linear matching.

data NLMState Source #

Constructors

NLMState
Fields _nlmSub :: Sub _nlmEqs :: PostponedEquations

Instances

Instances details

Null NLMState Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods empty :: NLMState Source # null :: NLMState -> Bool Source #

nlmSub :: Lens' Sub NLMState Source #

nlmEqs :: Lens' PostponedEquations NLMState Source #

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

matchingBlocked :: Blocked_ -> NLM () Source #

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

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

tellEq :: Telescope -> Telescope -> Type -> Term -> Term -> NLM () Source #

type Sub = IntMap (Relevance, Term) Source #

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.

type PostponedEquations = [PostponedEquation] Source #

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 () 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 Type NLPat Term Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> Type -> NLPat -> Term -> 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, Term) [Elim' NLPat] Elims Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods match :: Relevance -> Telescope -> Telescope -> (Type, Term) -> [Elim' NLPat] -> Elims -> NLM () Source #

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

makeSubstitution :: Telescope -> Sub -> Substitution Source #

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

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

equal :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins 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)