Agda.TypeChecking.Substitute.Class

Application

class Apply t where

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

Methods

apply :: t -> Args -> t

applyE :: t -> Elims -> t

applys :: Apply t => t -> [Term] -> t

Apply to some default arguments.

apply1 :: Apply t => t -> Term -> t

Apply to a single default argument.

Abstraction

class Abstract t where

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

Minimal complete definition

abstract

Methods

abstract :: Telescope -> t -> t

Substitution and raisingshiftingweakening

class DeBruijn t => Subst t a | a -> t where

Apply a substitution.

Minimal complete definition

applySubst

Methods

applySubst :: Substitution' t -> a -> a

Instances

Subst Term AsBinding

Methods

applySubst :: Substitution' Term -> AsBinding -> AsBinding

Subst Term DotPatternInst

Methods

applySubst :: Substitution' Term -> DotPatternInst -> DotPatternInst

Subst Term ProblemRest

Methods

applySubst :: Substitution' Term -> ProblemRest -> ProblemRest

Subst Term SizeConstraint

Methods

applySubst :: Substitution' Term -> SizeConstraint -> SizeConstraint

Subst Term SizeMeta

Methods

applySubst :: Substitution' Term -> SizeMeta -> SizeMeta

Subst Term (Problem' p)

Methods

applySubst :: Substitution' Term -> Problem' p -> Problem' p

Subst Term (SizeExpr' NamedRigid SizeMeta)

Only for raise.

Methods

applySubst :: Substitution' Term -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta

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

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

subst :: Subst t a => Int -> t -> a -> a

Replace de Bruijn index i by a Term in something.

strengthen :: Subst t a => Empty -> a -> a

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

Replace what is now de Bruijn index 0, but go under n binders. substUnder n u == subst n (raise n u).

Explicit substitutions

idS :: Substitution' a

wkS :: Int -> Substitution' a -> Substitution' a

raiseS :: Int -> Substitution' a

consS :: DeBruijn a => a -> Substitution' a -> Substitution' a

singletonS :: DeBruijn a => Int -> a -> Substitution' a

To replace index n by term u, do applySubst (singletonS n u). Γ, Δ ⊢ u : A --------------------------------- Γ, Δ ⊢ singletonS |Δ| u : Γ, A, Δ

inplaceS :: Subst a a => Int -> a -> Substitution' a

Single substitution without disturbing any deBruijn indices. Γ, A, Δ ⊢ u : A --------------------------------- Γ, A, Δ ⊢ inplace |Δ| u : Γ, A, Δ

liftS :: Int -> Substitution' a -> Substitution' a

Lift a substitution under k binders.

dropS :: Int -> Substitution' a -> Substitution' a

        Γ ⊢ ρ : Δ, Ψ
     -------------------
     Γ ⊢ dropS |Ψ| ρ : Δ
  

composeS :: Subst a a => Substitution' a -> Substitution' a -> Substitution' a

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

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

(++#) :: DeBruijn a => [a] -> Substitution' a -> Substitution' a infixr 4

prependS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a -> Substitution' a

     Γ ⊢ ρ : Δ  Γ ⊢ reverse vs : Θ
     ----------------------------- (treating Nothing as having any type)
       Γ ⊢ prependS vs ρ : Δ, Θ
  

parallelS :: DeBruijn a => [a] -> Substitution' a

compactS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a

strengthenS :: Empty -> Int -> Substitution' a

Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ

lookupS :: Subst a a => Substitution' a -> Nat -> a

Functions on abstractions

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

Instantiate an abstraction. Strict in the term.

lazyAbsApp :: Subst t a => Abs a -> t -> a

Instantiate an abstraction. Lazy in the term, which allow it to be IMPOSSIBLE in the case where the variable shouldn't be used but we cannot use noabsApp. Used in Apply.

noabsApp :: Subst t a => Empty -> Abs a -> a

Instantiate an abstraction that doesn't use its argument.

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

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

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

underAbs :: Subst t 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 Term 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.