Agda.TypeChecking.Substitute

Documentation

class Apply t where

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

Methods

apply :: t -> Args -> t

Instances

Apply Permutation

Apply ClauseBody

Apply Clause

Apply Sort

Apply Type

Apply Term

Apply CompiledClauses

Apply FunctionInverse

Apply PrimFun

Apply Defn

Apply Definition

Apply DisplayTerm

Apply t => Apply [t]

Apply [Occurrence]

Apply [Polarity]

Apply t => Apply (Maybe t)

Apply a => Apply (Ptr a)

Apply t => Apply (Blocked t)

Subst a => Apply (Tele a)

Apply a => Apply (Case a)

Apply a => Apply (WithArity a)

(Apply a, Apply b) => Apply (a, b)

Apply v => Apply (Map k v)

(Apply a, Apply b, Apply c) => Apply (a, b, c)

piApply :: Type -> Args -> Type

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

class Abstract t where

(abstract args v) args --> v[args].

Methods

abstract :: Telescope -> t -> t

Instances

Abstract Permutation

Abstract ClauseBody

Abstract Clause

Abstract Sort

Abstract Telescope

Abstract Type

Abstract Term

Abstract CompiledClauses

Abstract FunctionInverse

Abstract PrimFun

Abstract Defn

Abstract Definition

Abstract t => Abstract [t]

Abstract [Occurrence]

Abstract [Polarity]

Abstract t => Abstract (Maybe t)

Abstract a => Abstract (Case a)

Abstract a => Abstract (WithArity a)

Abstract v => Abstract (Map k v)

telVars :: Telescope -> [Arg Pattern]

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

data Substitution

Substitutions.

Constructors

IdS

EmptyS

Wk !Int Substitution

Term :# Substitution

Lift !Int Substitution

Instances

Eq Substitution

Ord Substitution

Show Substitution

Sized Substitution

KillRange Substitution

Subst Substitution

idS :: Substitution

wkS :: Int -> Substitution -> Substitution

raiseS :: Int -> Substitution

singletonS :: Term -> Substitution

liftS :: Int -> Substitution -> Substitution

dropS :: Int -> Substitution -> Substitution

composeS :: Substitution -> Substitution -> Substitution

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

splitS :: Int -> Substitution -> (Substitution, Substitution)

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

parallelS :: [Term] -> Substitution

lookupS :: Substitution -> Nat -> Term

class Subst t where

Apply a substitution.

Methods

applySubst :: Substitution -> t -> t

Instances

Subst ()

Subst Pattern

Subst ClauseBody

Subst LevelAtom

Subst PlusLevel

Subst Level

Subst Sort

Subst Type

Subst Elim

Subst Term

Subst DisplayTerm

Subst DisplayForm

Subst Constraint

Subst Substitution

Subst AsBinding

Subst DotPatternInst

Subst ProblemRest

Subst Equality

Subst a => Subst [a]

Subst a => Subst (Maybe a)

Subst a => Subst (Ptr a)

Subst a => Subst (Arg a)

Subst a => Subst (Dom a)

Subst t => Subst (Blocked t)

Subst a => Subst (Tele a)

Subst a => Subst (Abs a)

Subst (Problem' p)

Subst a => Subst (HomHet a)

(Subst a, Subst b) => Subst (a, b)

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

data TelV a

Constructors

TelV (Tele (Dom a)) a

Instances

Functor TelV

Typeable1 TelV

(Eq a, Subst a) => Eq (TelV a)

(Ord a, Subst a) => Ord (TelV a)

Show a => Show (TelV a)

type TelView = TelV Type

telFromList :: [Dom (String, Type)] -> Telescope

telToList :: Telescope -> [Dom (String, Type)]

telView' :: Type -> TelView

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

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

telePi :: Telescope -> Type -> Type

telePi_ :: Telescope -> Type -> Type

Everything will be a pi.

teleLam :: Telescope -> 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.

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

Instantiate an abstraction

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

mkAbs :: (Subst a, Free a) => String -> 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.

sLub :: Sort -> Sort -> Sort

lvlView :: Term -> Level

levelMax :: [PlusLevel] -> Level

sortTm :: Sort -> Term

levelSort :: Level -> Sort

levelTm :: Level -> Term

unLevelAtom :: LevelAtom -> Term