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
singleSubst :: TVar -> Type -> Subst
(@@) :: Subst -> Subst -> Subst
defaultingSubst :: Subst -> Subst
listSubst :: [(TVar, Type)] -> Subst
listParamSubst :: [(TParam, Type)] -> Subst
isEmptySubst :: Subst -> Bool
class FVS t where
- fvs :: t -> Set TVar
apSubstMaybe :: Subst -> Type -> Maybe Type
class TVars t where
- apSubst :: Subst -> t -> t
apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a
substBinds :: Subst -> Set TVar
applySubstToVar :: Subst -> TVar -> Maybe Type
substToList :: Subst -> [(TVar, Type)]

Documentation

data Subst Source #

A Subst value represents a substitution that maps each Type to a Type.

Invariant: 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.

Instances

Show Subst Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods showsPrec :: Int -> Subst -> ShowS # show :: Subst -> String # showList :: [Subst] -> ShowS #
PP Subst Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods ppPrec :: Int -> Subst -> Doc Source #
PP (WithNames Subst) Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods ppPrec :: Int -> WithNames Subst -> Doc Source #

emptySubst :: Subst Source #

singleSubst :: TVar -> Type -> Subst Source #

(@@) :: Subst -> Subst -> 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 #

class FVS t where Source #

Methods

fvs :: t -> Set TVar Source #

Instances

FVS Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Type -> Set TVar Source #
FVS Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Schema -> Set TVar Source #
FVS DelayedCt Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods fvs :: DelayedCt -> Set TVar Source #
FVS Goal Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods fvs :: Goal -> Set TVar Source #
FVS Error Source #
Instance details Defined in Cryptol.TypeCheck.Error Methods fvs :: Error -> Set TVar Source #
FVS Warning Source #
Instance details Defined in Cryptol.TypeCheck.Error Methods fvs :: Warning -> Set TVar Source #
FVS a => FVS [a] Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: [a] -> Set TVar Source #
FVS a => FVS (Maybe a) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Maybe a -> Set TVar Source #
(FVS a, FVS b) => FVS (a, b) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: (a, b) -> Set TVar Source #

apSubstMaybe :: Subst -> Type -> Maybe Type Source #

Apply a substitution. Returns Nothing if nothing changed.

class TVars t where Source #

Methods

apSubst Source #

Arguments

:: Subst
-> t
-> t	replaces free vars

Instances

TVars Type Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Type -> Type Source #
TVars Schema Source #	This instance does not need to worry about bound variable capture, because we rely on the `Subst` datatype invariant to ensure that variable scopes will be properly preserved.
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Schema -> Schema Source #
TVars DeclDef Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> DeclDef -> DeclDef Source #
TVars Decl Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Decl -> Decl Source #
TVars DeclGroup Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> DeclGroup -> DeclGroup Source #
TVars Match Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Match -> Match Source #
TVars Expr Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Expr -> Expr Source #
TVars Module Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Module -> Module Source #
TVars ConstraintSource Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> ConstraintSource -> ConstraintSource Source #
TVars DelayedCt Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> DelayedCt -> DelayedCt Source #
TVars HasGoal Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> HasGoal -> HasGoal Source #
TVars Goal Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> Goal -> Goal Source #
TVars Goals Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> Goals -> Goals Source #
TVars Error Source #
Instance details Defined in Cryptol.TypeCheck.Error Methods apSubst :: Subst -> Error -> Error Source #
TVars Warning Source #
Instance details Defined in Cryptol.TypeCheck.Error Methods apSubst :: Subst -> Warning -> Warning Source #
TVars t => TVars [t] Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> [t] -> [t] Source #
TVars t => TVars (Maybe t) Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Maybe t -> Maybe t Source #
TVars a => TVars (TypeMap a) Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> TypeMap a -> TypeMap a Source #
(TVars s, TVars t) => TVars (s, t) Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> (s, t) -> (s, t) Source #
(Functor m, TVars a) => TVars (List m a) Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> List m a -> List m a Source #

apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a Source #

Apply the substitution to the keys of a type map.

substBinds :: Subst -> Set TVar Source #

applySubstToVar :: Subst -> TVar -> Maybe Type Source #

substToList :: Subst -> [(TVar, Type)] Source #