| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Compiler.Epic.Injection
- findInjection :: [(QName, Definition)] -> Compile TCM [(QName, Definition)]
- replaceFunCC :: QName -> CompiledClauses -> Compile TCM ()
- type InjConstraints = Maybe [(QName, QName)]
- isInjective :: QName -> [Clause] -> Compile TCM (Maybe ((QName, InjectiveFun), [(QName, QName)]))
- patternToTerm :: Nat -> Pattern -> Term
- nrBinds :: Num i => Pattern -> i
- substForDot :: [NamedArg (Pattern' a)] -> Substitution
- isInjectiveHere :: QName -> Int -> Clause -> Compile TCM InjConstraints
- litToCon :: Literal -> TCM Term
- litInt :: Literal -> Bool
- insertAt :: (Nat, Term) -> Term -> Term
- solve :: [QName] -> [((QName, InjectiveFun), [(QName, QName)])] -> Compile TCM [(QName, InjectiveFun)]
- emptyC :: InjConstraints
- addConstraint :: QName -> QName -> InjConstraints -> InjConstraints
- unionConstraints :: [InjConstraints] -> InjConstraints
- class Injectible a where
- data TagEq
- data Tags = Tags {}
- initialTags :: Map QName Tag -> [QName] -> Tags
- unify :: QName -> QName -> Tags -> Compile TCM (Maybe Tags)
- setTag :: Int -> Tag -> Tags -> Compile TCM (Maybe Tags)
- mergeGroups :: Int -> Int -> Tags -> Compile TCM (Maybe Tags)
- unifiable :: QName -> QName -> Compile TCM Bool
- (!!!!) :: Ord k => Map k v -> k -> v
Documentation
findInjection :: [(QName, Definition)] -> Compile TCM [(QName, Definition)] Source #
Find potentially injective functions, solve constraints to fix some constructor tags and make functions whose constraints are fulfilled injections
replaceFunCC :: QName -> CompiledClauses -> Compile TCM () Source #
type InjConstraints = Maybe [(QName, QName)] Source #
If the pairs of constructor names have the same tags, the function is injective. If Nothing, the function is not injective.
substForDot :: [NamedArg (Pattern' a)] -> Substitution Source #
solve :: [QName] -> [((QName, InjectiveFun), [(QName, QName)])] -> Compile TCM [(QName, InjectiveFun)] Source #
addConstraint :: QName -> QName -> InjConstraints -> InjConstraints Source #
class Injectible a where Source #
Are two terms injectible? Tries to find a mapping between constructors that equates the terms.
Precondition: t1 is normalised, t2 is in WHNF When reducing t2, it may become a literal, which makes this not work in some cases...
Minimal complete definition
Methods
(<:) :: a -> a -> ReaderT (Map QName InjectiveFun) (Compile TCM) InjConstraints Source #
Instances
| Injectible Term Source # | |
| Injectible a => Injectible [a] Source # | |
| Injectible a => Injectible (Arg a) Source # | |
| Injectible a => Injectible (Elim' a) Source # | |