Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell98 |
- data Subst
- emptySubst :: Subst
- singleSubst :: TVar -> Type -> Subst
- (@@) :: Subst -> Subst -> Subst
- defaultingSubst :: Subst -> Subst
- listSubst :: [(TVar, Type)] -> Subst
- isEmptySubst :: Subst -> Bool
- class FVS t where
- apSubstMaybe :: Subst -> Type -> Maybe Type
- class TVars t where
- apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a
- substBinds :: Subst -> Set TVar
- applySubstToVar :: Subst -> TVar -> Maybe Type
- substToList :: Subst -> [(TVar, Type)]
Documentation
emptySubst :: Subst Source #
defaultingSubst :: Subst -> Subst Source #
listSubst :: [(TVar, Type)] -> Subst Source #
Makes a substitution out of a list. WARNING: We do not validate the list in any way, so the caller should ensure that we end up with a valid (e.g., idempotent) substitution.
isEmptySubst :: Subst -> Bool Source #
apSubstMaybe :: Subst -> Type -> Maybe Type Source #
Apply a substitution. Returns Nothing
if nothing changed.
TVars Type Source # | |
TVars Schema Source # | WARNING: This instance assumes that the quantified variables in the types in the substitution will not get captured by the quantified variables. This is reasonable because there should be no shadowing of quantified variables but, just in case, we make a sanity check and panic if somehow capture did occur. |
TVars DeclDef Source # | |
TVars Decl Source # | |
TVars DeclGroup Source # | |
TVars Match Source # | |
TVars Expr Source # | |
TVars Module Source # | |
TVars ConstraintSource Source # | |
TVars Error Source # | |
TVars Warning Source # | |
TVars DelayedCt Source # | |
TVars HasGoal Source # | |
TVars Goal Source # | |
TVars Goals Source # | |
TVars t => TVars [t] Source # | |
TVars t => TVars (Maybe t) Source # | |
TVars a => TVars (TypeMap a) Source # | |
(TVars s, TVars t) => TVars (s, t) Source # | |
(Functor m, TVars a) => TVars (List m a) Source # | |