| 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
- applySubst :: Substitution' t -> a -> a
- 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
- listS :: Subst a a => [(Int, a)] -> Substitution' 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).
Minimal complete definition
Instances
Abstraction
class Abstract t where Source #
(abstract args v) .apply args --> v[args]
Instances
Substitution and shifting/weakening/strengthening
class DeBruijn t => Subst t a | a -> t where Source #
Apply a substitution.
Minimal complete definition
Nothing
Methods
applySubst :: Substitution' t -> a -> a Source #
applySubst :: (a ~ f b, Functor f, Subst t b) => Substitution' t -> a -> a Source #
Instances
strengthen :: Subst t a => Empty -> a -> a Source #
substUnder :: Subst t a => Nat -> t -> a -> a Source #
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 Source #
wkS :: Int -> Substitution' a -> Substitution' a Source #
raiseS :: Int -> Substitution' a Source #
consS :: DeBruijn a => a -> Substitution' a -> Substitution' a Source #
singletonS :: DeBruijn a => Int -> a -> Substitution' a Source #
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 Source #
Single substitution without disturbing any deBruijn indices.
Γ, A, Δ ⊢ u : A
---------------------------------
Γ, A, Δ ⊢ inplace |Δ| u : Γ, A, Δ
liftS :: Int -> Substitution' a -> Substitution' a Source #
Lift a substitution under k binders.
dropS :: Int -> Substitution' a -> Substitution' a Source #
Γ ⊢ ρ : Δ, Ψ
-------------------
Γ ⊢ dropS |Ψ| ρ : Δ
composeS :: Subst a a => Substitution' a -> Substitution' a -> Substitution' a Source #
applySubst (ρ composeS σ) v == applySubst ρ (applySubst σ v)splitS :: Int -> Substitution' a -> (Substitution' a, Substitution' a) Source #
(++#) :: DeBruijn a => [a] -> Substitution' a -> Substitution' a infixr 4 Source #
prependS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a -> Substitution' a Source #
Γ ⊢ ρ : Δ Γ ⊢ reverse vs : Θ
----------------------------- (treating Nothing as having any type)
Γ ⊢ prependS vs ρ : Δ, Θ
parallelS :: DeBruijn a => [a] -> Substitution' a Source #
strengthenS :: Empty -> Int -> Substitution' a Source #
Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ
listS :: Subst a a => [(Int, a)] -> Substitution' a Source #
lookupS (listS [(x0,t0)..(xn,tn)]) xi = ti, assuming x0 < .. < xn.
Functions on abstractions
lazyAbsApp :: Subst t a => Abs a -> t -> a Source #
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 Source #
Instantiate an abstraction that doesn't use its argument.
underAbs :: Subst t a => (a -> b -> b) -> a -> Abs b -> Abs b Source #
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.