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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Substitute

Contents

Synopsis

Application

class Apply t where

Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking).

Minimal complete definition

Nothing

Methods

apply :: t -> Args -> t

applyE :: t -> Elims -> t

canProject :: QName -> Term -> Maybe (Arg Term)

If $v$ is a record value, canProject f v returns its field f.

conApp :: ConHead -> Args -> Elims -> Term

Eliminate a constructed term.

defApp :: QName -> Elims -> Elims -> Term

defApp f us vs applies Def f us to further arguments vs, eliminating top projection redexes. If us is not empty, we cannot have a projection redex, since the record argument is the first one.

piApply :: Type -> Args -> Type

The type must contain the right number of pis without have to perform any reduction.

Abstraction

abstractArgs :: Abstract a => Args -> a -> a

Explicit substitutions

composeS :: Substitution -> Substitution -> Substitution

applySubst (ρ composeS σ) v == applySubst ρ (applySubst σ v)

(++#) :: [Term] -> Substitution -> Substitution infixr 4

Substitution and raisingshiftingweakening

class Subst t where

Apply a substitution.

Methods

applySubst :: Substitution -> t -> t

raise :: Subst t => Nat -> t -> t

raiseFrom :: Subst t => Nat -> Nat -> t -> t

subst :: Subst t => Term -> t -> t

substUnder :: Subst t => Nat -> Term -> t -> t

Telescopes

data TelV a

Constructors

TelV 

Fields

theTel :: Tele (Dom a)
 
theCore :: a
 

Instances

Functor TelV 
(Eq a, Subst a) => Eq (TelV a) 
(Ord a, Subst a) => Ord (TelV a) 
Show a => Show (TelV a) 
Typeable (* -> *) TelV 

type ListTel' a = [Dom (a, Type)]

bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a

Turn a typed binding (x1 .. xn : A) into a telescope.

mkPi :: Dom (ArgName, Type) -> Type -> Type

mkPi dom t = telePi (telFromList [dom]) t

telePi :: Telescope -> Type -> Type

Uses free variable analysis to introduce noAbs bindings.

telePi_ :: Telescope -> Type -> Type

Everything will be a Abs.

class TeleNoAbs a where

Performs void (noAbs) abstraction over telescope.

Methods

teleNoAbs :: a -> Term -> Term

dLub :: Sort -> Abs Sort -> Sort

Dependent least upper bound, to assign a level to expressions like forall i -> Set i.

dLub s1 i.s2 = omega if i appears in the rigid variables of s2.

Functions on abstractions

absApp :: Subst t => Abs t -> Term -> t

Instantiate an abstraction

absBody :: Subst t => Abs t -> t

mkAbs :: (Subst a, Free a) => ArgName -> a -> Abs a

reAbs :: (Subst a, Free a) => Abs a -> Abs a

underAbs :: Subst a => (a -> b -> b) -> a -> Abs b -> Abs b

underAbs k a b applies k to a and the content of abstraction b and puts the abstraction back. a is raised if abstraction was proper such that at point of application of k and the content of b are at the same context. Precondition: a and b are at the same context at call time.

underLambdas :: Subst a => Int -> (a -> Term -> Term) -> a -> Term -> Term

underLambdas n k a b drops n initial Lams from b, performs operation k on a and the body of b, and puts the Lams back. a is raised correctly according to the number of abstractions.

class GetBody a where

getBody returns the properly raised clause Body, and Nothing if NoBody.

getBodyUnraised just grabs the body, without raising the de Bruijn indices. This is useful if you want to consider the body in context clauseTel.

Methods

getBody :: a -> Maybe Term

getBodyUnraised :: a -> Maybe Term

Syntactic equality and order

Level stuff

sLub :: Sort -> Sort -> Sort

Boring instances