Agda.Compiler.Epic.Injection

Documentation

findInjection :: [(QName, Definition)] -> Compile TCM [(QName, Definition)]

Find potentially injective functions, solve constraints to fix some constructor tags and make functions whose constraints are fulfilled injections

replaceFunCC :: QName -> CompiledClauses -> Compile TCM ()

type InjConstraints = Maybe [(QName, QName)]

If the pairs of constructor names have the same tags, the function is injective. If Nothing, the function is not injective.

isInjective

Arguments

:: QName

Name of the function being tested

-> [Clause]

The function's clauses

-> Compile TCM (Maybe ((QName, InjectiveFun), [(QName, QName)]))

remAbs :: ClauseBody -> Term

isNoBody :: ClauseBody -> Bool

patternToTerm :: Nat -> Pattern -> Term

nrBinds :: Num i => Pattern -> i

substForDot :: [Arg Pattern] -> Substitution

isInjectiveHere

Arguments

:: QName

Name of the function being tested

-> Int

The current argument

-> Clause

-> Compile TCM InjConstraints

litToCon :: Literal -> TCM Term

litCon :: 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

(<:) :: Term -> Term -> (QName :-> InjectiveFun) -> Compile TCM InjConstraints

Are two terms injectible? Precondition: t1 is normalised, t2 is in WHNF When reducing t2, it may become a literal, which makes this not work in some cases...

data TagEq

Constructors

Same Int

IsTag Tag

Instances

Eq TagEq

data Tags

Constructors

Tags

Fields

eqGroups :: Int :-> Set QName

constrGroup :: QName :-> TagEq

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 => (k :-> v) -> k -> v