| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
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
- patternFrom :: a -> TCM b
- type NLM = MaybeT (WriterT NLMOut ReduceM)
- type NLMOut = (AmbSubst, PostponedEquations)
- liftRed :: ReduceM a -> NLM a
- runNLM :: NLM () -> ReduceM (Maybe NLMOut)
- traceSDocNLM :: VerboseKey -> Int -> TCM Doc -> NLM a -> NLM a
- tellSubst :: Int -> Term -> NLM ()
- tellEq :: Term -> Term -> NLM ()
- newtype AmbSubst = AmbSubst {}
- data PostponedEquation = PostponedEquation {}
- type PostponedEquations = [PostponedEquation]
- class AmbMatch a b where
- makeSubstitution :: IntMap Term -> Substitution
- disambiguateSubstitution :: AmbSubst -> ReduceM (Maybe Substitution)
- checkPostponedEquations :: Substitution -> PostponedEquations -> ReduceM Bool
- nonLinMatch :: AmbMatch a b => a -> b -> ReduceM (Maybe Substitution)
- equal :: Term -> Term -> ReduceM Bool
Documentation
class PatternFrom a b where Source
Turn a term into a non-linear pattern, treating the free variables as pattern variables.
Methods
patternFrom :: a -> TCM b Source
Instances
| PatternFrom Term NLPat Source | |
| (Traversable f, PatternFrom a b) => PatternFrom (f a) (f b) Source |
type NLMOut = (AmbSubst, PostponedEquations) Source
traceSDocNLM :: VerboseKey -> Int -> TCM Doc -> NLM a -> NLM a Source
Non-linear matching returns first an ambiguous substitution, mapping one de Bruijn index to possibly several terms.
data PostponedEquation Source
Matching against a term produces a constraint which we have to verify after applying the substitution computed by matching.
Constructors
| PostponedEquation | |
Instances
type PostponedEquations = [PostponedEquation] Source
class AmbMatch a b where Source
Match a non-linear pattern against a neutral term, returning a substitution.
nonLinMatch :: AmbMatch a b => a -> b -> ReduceM (Maybe Substitution) Source