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

Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.Epic.Injection

Synopsis

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

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

nrBinds :: Num i => Pattern -> i #

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.

insertAt :: (Nat, Term) -> Term -> Term #

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

Minimal complete definition

(<:)

data TagEq #

Constructors

Same Int 
IsTag Tag 

Instances

Eq TagEq # 

Methods

(==) :: TagEq -> TagEq -> Bool #

(/=) :: TagEq -> TagEq -> Bool #

data Tags #

Constructors

Tags 

(!!!!) :: Ord k => Map k v -> k -> v #