| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe |
| Language | Haskell2010 |
Cryptol.TypeCheck.Subst
Description
Synopsis
- data Subst
- emptySubst :: Subst
- data SubstError
- singleSubst :: TVar -> Type -> Either SubstError Subst
- singleTParamSubst :: TParam -> Type -> Subst
- uncheckedSingleSubst :: TVar -> Type -> Subst
- (@@) :: Subst -> Subst -> Subst
- defaultingSubst :: Subst -> Subst
- listSubst :: [(TVar, Type)] -> Subst
- listParamSubst :: [(TParam, 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
A Subst value represents a substitution that maps each Type
to a Type.
Invariant 1: If there is a mapping from TVFree _ _ tps _ to a
type t, then t must not mention (directly or indirectly) any
type parameter that is not in tps. In particular, if t contains
a variable TVFree _ _ tps2 _, then tps2 must be a subset of
tps. This ensures that applying the substitution will not permit
any type parameter to escape from its scope.
Invariant 2: The substitution must be idempotent, in that applying
a substitution to any Type in the map should leave that Type
unchanged. In other words, Type values in the range of a Subst
should not mention any Type in the domain of the Subst. In
particular, this implies that a substitution must not contain any
recursive variable mappings.
Invariant 3: The substitution must be kind correct: Each Type in
the substitution must map to a Type of the same kind.
emptySubst :: Subst Source #
data SubstError Source #
Reasons to reject a single-variable substitution.
Constructors
| SubstRecursive |
|
| SubstEscaped [TParam] |
|
| SubstKindMismatch Kind Kind |
|
singleSubst :: TVar -> Type -> Either SubstError Subst Source #
defaultingSubst :: Subst -> Subst Source #
A defaulting substitution maps all otherwise-unmapped free
variables to a kind-appropriate default type (Bit for value types
and 0 for numeric types).
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.
listParamSubst :: [(TParam, 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.
Instances
| TVars Type Source # | |
| TVars Schema Source # | This instance does not need to worry about bound variable
capture, because we rely on the |
| TVars DeclDef Source # | |
| TVars Decl Source # | |
| TVars DeclGroup Source # | |
| TVars Match Source # | |
| TVars Expr Source # | |
| TVars Module Source # | |
| TVars ConstraintSource Source # | |
Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> ConstraintSource -> ConstraintSource Source # | |
| TVars DelayedCt Source # | |
| TVars HasGoal Source # | |
| TVars Goal Source # | |
| TVars Goals Source # | |
| TVars Error Source # | |
| TVars Warning Source # | |
| TVars t => TVars [t] Source # | |
Defined in Cryptol.TypeCheck.Subst | |
| TVars t => TVars (Maybe t) Source # | |
| TVars a => TVars (TypeMap a) Source # | |
| (TVars s, TVars t) => TVars (s, t) Source # | |
Defined in Cryptol.TypeCheck.Subst | |
| (Functor m, TVars a) => TVars (List m a) Source # | |