Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Compiler.Epic.Injection

Synopsis

- 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)]))
- remAbs :: ClauseBody -> Term
- isNoBody :: ClauseBody -> Bool
- patternToTerm :: Nat -> Pattern -> Term
- nrBinds :: Num i => Pattern -> i
- substForDot :: [Arg Pattern] -> Substitution
- isInjectiveHere :: QName -> Int -> 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
- data TagEq
  - = Same Int
  - | IsTag Tag
- data Tags = Tags {
  - 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

# 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