| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Substitute.Class
Synopsis
- class Apply t where
- applys :: Apply t => t -> [Term] -> t
- apply1 :: Apply t => t -> Term -> t
- class Abstract t where
- class DeBruijn (SubstArg a) => Subst a where
- type SubstArg a
- applySubst :: Substitution' (SubstArg a) -> a -> a
- type SubstWith t a = (Subst a, SubstArg a ~ t)
- type EndoSubst a = SubstWith a a
- type TermSubst a = SubstWith Term a
- raise :: Subst a => Nat -> a -> a
- raiseFrom :: Subst a => Nat -> Nat -> a -> a
- subst :: Subst a => Int -> SubstArg a -> a -> a
- strengthen :: Subst a => Impossible -> a -> a
- substUnder :: Subst a => Nat -> SubstArg a -> a -> a
- isNoAbs :: (Free a, Subst a) => Abs a -> Maybe a
- newtype NoSubst t a = NoSubst {
- unNoSubst :: 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 :: EndoSubst a => Int -> a -> Substitution' a
- liftS :: Int -> Substitution' a -> Substitution' a
- dropS :: Int -> Substitution' a -> Substitution' a
- composeS :: EndoSubst 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 => Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
- parallelS :: DeBruijn a => [a] -> Substitution' a
- strengthenS :: Impossible -> Int -> Substitution' a
- strengthenS' :: Impossible -> Int -> Substitution' a -> Substitution' a
- lookupS :: EndoSubst a => Substitution' a -> Nat -> a
- listS :: EndoSubst a => [(Int, a)] -> Substitution' a
- raiseFromS :: Nat -> Nat -> Substitution' a
- absApp :: Subst a => Abs a -> SubstArg a -> a
- lazyAbsApp :: Subst a => Abs a -> SubstArg a -> a
- noabsApp :: Subst a => Impossible -> Abs a -> a
- absBody :: Subst a => Abs a -> a
- mkAbs :: (Subst a, Free a) => ArgName -> a -> Abs a
- reAbs :: (Subst a, Free a) => Abs a -> Abs a
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 (SubstArg a) => Subst a where Source #
Apply a substitution.
Minimal complete definition
Nothing
Methods
applySubst :: Substitution' (SubstArg a) -> a -> a Source #
default applySubst :: forall (f :: Type -> Type) b. (a ~ f b, Functor f, Subst b, SubstArg a ~ SubstArg b) => Substitution' (SubstArg a) -> a -> a Source #
Instances
type SubstWith t a = (Subst a, SubstArg a ~ t) Source #
Simple constraint alias for a Subst instance a with arg type t.
subst :: Subst a => Int -> SubstArg a -> a -> a Source #
Replace de Bruijn index i by a Term in something.
strengthen :: Subst a => Impossible -> a -> a Source #
substUnder :: Subst a => Nat -> SubstArg a -> a -> a Source #
Replace what is now de Bruijn index 0, but go under n binders.
substUnder n u == subst n (raise n u).
isNoAbs :: (Free a, Subst a) => Abs a -> Maybe a Source #
Checks whether the variable bound by the abstraction is actually
used, and, if not, returns the term within, strengthened to live in
the context outside the abstraction.
See also isBinderUsed.
Identity instances
Wrapper for types that do not contain variables (so applying a substitution is the identity). Useful if you have a structure of types that support substitution mixed with types that don't and need to apply a substitution to the full structure.
Instances
| Functor (NoSubst t) Source # | |||||
| DeBruijn t => Subst (NoSubst t a) Source # | |||||
Defined in Agda.TypeChecking.Substitute.Class Associated Types
Methods applySubst :: Substitution' (SubstArg (NoSubst t a)) -> NoSubst t a -> NoSubst t a Source # | |||||
| NFData a => NFData (NoSubst t a) Source # | |||||
Defined in Agda.TypeChecking.Substitute.Class | |||||
| Generic (NoSubst t a) Source # | |||||
Defined in Agda.TypeChecking.Substitute.Class Associated Types
| |||||
| type SubstArg (NoSubst t a) Source # | |||||
Defined in Agda.TypeChecking.Substitute.Class | |||||
| type Rep (NoSubst t a) Source # | |||||
Defined in Agda.TypeChecking.Substitute.Class | |||||
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 :: EndoSubst 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 :: EndoSubst 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 => Impossible -> [Maybe a] -> Substitution' a -> Substitution' a Source #
Γ ⊢ ρ : Δ Γ ⊢ reverse vs : Θ
----------------------------- (treating Nothing as having any type)
Γ ⊢ prependS vs ρ : Δ, Θ
parallelS :: DeBruijn a => [a] -> Substitution' a Source #
Γ ⊢ reverse vs : Δ
-----------------------------
Γ ⊢ parallelS vs ρ : Γ, Δ
Note the Γ in Γ, Δ.
strengthenS :: Impossible -> Int -> Substitution' a Source #
Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ
strengthenS' :: Impossible -> Int -> Substitution' a -> Substitution' a Source #
A "smart" variant of Strengthen. If strengthenS is applied
to a substitution with an outermost Strengthen constructor, then
the "error message" of that constructor is discarded in favour of
the Impossible argument of this function.
listS :: EndoSubst a => [(Int, a)] -> Substitution' a Source #
lookupS (listS [(x0,t0)..(xn,tn)]) xi = ti, assuming x0 < .. < xn.
raiseFromS :: Nat -> Nat -> Substitution' a Source #
Γ, Ξ, Δ ⊢ raiseFromS |Δ| |Ξ| : Γ, Δ
Functions on abstractions
absApp :: Subst a => Abs a -> SubstArg a -> a Source #
Instantiate an abstraction. Strict in the term.
lazyAbsApp :: Subst a => Abs a -> SubstArg a -> 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.