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)]))

patternToTerm :: Nat -> Pattern -> Term

nrBinds :: Num i => Pattern -> i

substForDot :: [NamedArg Pattern] -> Substitution

isInjectiveHere

Arguments

:: QName

Name of the function being tested

-> Int

The current argument

-> Clause

-> Compile TCM InjConstraints

litToCon :: Literal -> TCM Term

Turn NATURAL literal n into suc^n zero.

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

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...

Methods

(<:) :: a -> a -> ReaderT (QName :-> InjectiveFun) (Compile TCM) InjConstraints

Instances

Injectible Term

Injectible a => Injectible [a]

Injectible a => Injectible (Elim' a)

Injectible a => Injectible (Arg a)

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