Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
- class PatternFrom t a b where
- patternFrom :: Relevance -> Int -> t -> a -> TCM b
- type NLM = ExceptT Blocked_ (StateT NLMState ReduceM)
- data NLMState = NLMState {}
- nlmSub :: Lens' Sub NLMState
- nlmEqs :: Lens' PostponedEquations NLMState
- runNLM :: MonadReduce m => NLM () -> m (Either Blocked_ NLMState)
- matchingBlocked :: Blocked_ -> NLM ()
- tellSub :: Relevance -> Int -> Term -> NLM ()
- tellEq :: Telescope -> Telescope -> Term -> Term -> NLM ()
- type Sub = IntMap (Relevance, Term)
- data PostponedEquation = PostponedEquation {}
- type PostponedEquations = [PostponedEquation]
- class Match t a b where
- reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a) => IntSet -> a -> m (Either Blocked_ (Maybe a))
- makeSubstitution :: Telescope -> Sub -> Substitution
- checkPostponedEquations :: (MonadReduce m, HasConstInfo m, MonadDebug m) => Substitution -> PostponedEquations -> m (Maybe Blocked_)
- nonLinMatch :: (MonadReduce m, HasConstInfo m, MonadDebug m, Match t a b) => Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)
- equal :: (MonadReduce m, HasConstInfo m) => Term -> Term -> m (Maybe Blocked_)
Documentation
class PatternFrom t a b where Source #
Turn a term into a non-linear pattern, treating the free variables as pattern variables. The first argument indicates the relevance we are working under: if this is Irrelevant, then we construct a pattern that never fails to match. The second argument is the number of bound variables (from pattern lambdas). The third argument is the type of the term.
Instances
PatternFrom () Sort NLPat Source # | |
Defined in Agda.TypeChecking.Rewriting.NonLinMatch | |
PatternFrom () Type NLPType Source # | |
Defined in Agda.TypeChecking.Rewriting.NonLinMatch | |
PatternFrom Type Term NLPat Source # | |
Defined in Agda.TypeChecking.Rewriting.NonLinMatch | |
PatternFrom t a b => PatternFrom t (Dom a) (Dom b) Source # | |
Defined in Agda.TypeChecking.Rewriting.NonLinMatch | |
PatternFrom t a b => PatternFrom (Dom t) (Arg a) (Arg b) Source # | |
Defined in Agda.TypeChecking.Rewriting.NonLinMatch | |
PatternFrom (Type, Term) Elims [Elim' NLPat] Source # | |
matchingBlocked :: Blocked_ -> NLM () Source #
tellSub :: Relevance -> Int -> Term -> NLM () Source #
Add substitution i |-> v
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.
type PostponedEquations = [PostponedEquation] Source #
class Match t a b where Source #
Match a non-linear pattern against a neutral term, returning a substitution.
reallyFree :: (MonadReduce m, Reduce a, ForceNotFree a) => IntSet -> a -> m (Either Blocked_ (Maybe a)) Source #
makeSubstitution :: Telescope -> Sub -> Substitution Source #
checkPostponedEquations :: (MonadReduce m, HasConstInfo m, MonadDebug m) => Substitution -> PostponedEquations -> m (Maybe Blocked_) Source #
nonLinMatch :: (MonadReduce m, HasConstInfo m, MonadDebug m, Match t a b) => Telescope -> t -> a -> b -> m (Either Blocked_ Substitution) Source #
equal :: (MonadReduce m, HasConstInfo m) => Term -> Term -> m (Maybe Blocked_) Source #
Untyped βη-equality, does not handle things like 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)