| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Substitute.Class
Contents
Synopsis
- class Apply t where
- applys :: Apply t => t -> [Term] -> t
- apply1 :: Apply t => t -> Term -> t
- class Abstract t where
- class DeBruijn t => Subst t a | a -> t where
- raise :: Subst t a => Nat -> a -> a
- raiseFrom :: Subst t a => Nat -> Nat -> a -> a
- subst :: Subst t a => Int -> t -> a -> a
- strengthen :: Subst t a => Empty -> a -> a
- substUnder :: Subst t a => Nat -> t -> a -> a
- 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
- inplaceS :: Subst a a => Int -> a -> Substitution' a
- liftS :: Int -> Substitution' a -> Substitution' a
- dropS :: Int -> Substitution' a -> Substitution' a
- composeS :: Subst a a => Substitution' a -> Substitution' a -> Substitution' a
- splitS :: Int -> Substitution' a -> (Substitution' a, Substitution' a)
- (++#) :: DeBruijn a => [a] -> Substitution' a -> Substitution' a
- prependS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a -> Substitution' a
- parallelS :: DeBruijn a => [a] -> Substitution' a
- compactS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a
- strengthenS :: Empty -> Int -> Substitution' a
- lookupS :: Subst a a => Substitution' a -> Nat -> a
- absApp :: Subst t a => Abs a -> t -> a
- lazyAbsApp :: Subst t a => Abs a -> t -> a
- noabsApp :: Subst t a => Empty -> Abs a -> a
- 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
- underLambdas :: Subst Term a => Int -> (a -> Term -> Term) -> a -> Term -> Term
Application
Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking).
Instances
Abstraction
(abstract args v) .apply args --> v[args]
Minimal complete definition
Instances
Substitution and raisingshiftingweakening
class DeBruijn t => Subst t a | a -> t where #
Apply a substitution.
Minimal complete definition
Methods
applySubst :: Substitution' t -> a -> a #
Instances
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).
Identity instances
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 #
strengthenS :: Empty -> Int -> Substitution' a #
Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ
lookupS :: Subst a a => Substitution' a -> Nat -> a #
Functions on abstractions
lazyAbsApp :: Subst t a => Abs a -> t -> a #
Instantiate an abstraction. Lazy in the term, which allow it to be
(throwImpossible (Impossible "srcfullAgdaTypeCheckingSubstitute/Class.hs" 233)) 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.
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.