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
- class PatternFrom a b where
- type NLM = ExceptT Blocked_ (StateT NLMState ReduceM)
- data NLMState = NLMState {}
- nlmSub :: Lens' Sub NLMState
- nlmEqs :: Lens' PostponedEquations NLMState
- liftRed :: ReduceM a -> NLM a
- runNLM :: NLM () -> ReduceM (Either Blocked_ NLMState)
- traceSDocNLM :: VerboseKey -> Int -> TCM Doc -> NLM a -> NLM a
- 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 a b where
- reallyFree :: (Reduce a, Normalise a, Free' a FreeVars) => (Int -> Bool) -> a -> ReduceM (Either Blocked_ (Maybe a))
- makeSubstitution :: Telescope -> Sub -> Substitution
- checkPostponedEquations :: Substitution -> PostponedEquations -> ReduceM (Maybe Blocked_)
- nonLinMatch :: Match a b => Telescope -> a -> b -> ReduceM (Either Blocked_ Substitution)
- equal :: Term -> Term -> ReduceM (Maybe Blocked_)
- normaliseB' :: (Reduce t, Normalise t) => t -> ReduceM (Blocked t)
- class RaiseNLP a where
Documentation
class PatternFrom a b where #
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).
Minimal complete definition
Methods
patternFrom :: Relevance -> Int -> a -> TCM b #
Instances
PatternFrom Sort NLPat # | |
PatternFrom Type NLPType # | |
PatternFrom Term NLPat # | |
PatternFrom a b => PatternFrom [a] [b] # | |
PatternFrom a b => PatternFrom (Dom a) (Dom b) # | |
PatternFrom a b => PatternFrom (Arg a) (Arg b) # | |
PatternFrom a b => PatternFrom (Abs a) (Abs b) # | |
PatternFrom a NLPat => PatternFrom (Elim' a) (Elim' NLPat) # | |
Constructors
NLMState | |
Fields
|
traceSDocNLM :: VerboseKey -> Int -> TCM Doc -> NLM a -> NLM a #
matchingBlocked :: Blocked_ -> NLM () #
data PostponedEquation #
Matching against a term produces a constraint which we have to verify after applying the substitution computed by matching.
Constructors
PostponedEquation | |
type PostponedEquations = [PostponedEquation] #
Match a non-linear pattern against a neutral term, returning a substitution.
Minimal complete definition
reallyFree :: (Reduce a, Normalise a, Free' a FreeVars) => (Int -> Bool) -> a -> ReduceM (Either Blocked_ (Maybe a)) #
makeSubstitution :: Telescope -> Sub -> Substitution #
nonLinMatch :: Match a b => Telescope -> a -> b -> ReduceM (Either Blocked_ Substitution) #
equal :: Term -> Term -> ReduceM (Maybe Blocked_) #
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)
normaliseB' :: (Reduce t, Normalise t) => t -> ReduceM (Blocked t) #
Normalise the given term but also preserve blocking tags TODO: implement a more efficient version of this.
Raise (bound) variables in a NLPat
Minimal complete definition