Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	Safe
Language	Haskell98

Cryptol.TypeCheck.Subst

Description

Synopsis

Documentation

data Subst Source #

Instances

Show Subst Source #
Methods showsPrec :: Int -> Subst -> ShowS # show :: Subst -> String # showList :: [Subst] -> ShowS #
PP Subst Source #
Methods ppPrec :: Int -> Subst -> Doc Source #
DebugLog Subst Source #
Methods debugLog :: Solver -> Subst -> IO () Source # debugLogList :: Solver -> [Subst] -> IO () Source #
PP (WithNames Subst) Source #
Methods ppPrec :: Int -> WithNames Subst -> Doc Source #

emptySubst :: Subst Source #

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

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

class FVS t where Source #

Minimal complete definition

fvs

Methods

fvs :: t -> Set TVar Source #

Instances

FVS Type Source #
Methods fvs :: Type -> Set TVar Source #
FVS Schema Source #
Methods fvs :: Schema -> Set TVar Source #
FVS Error Source #
Methods fvs :: Error -> Set TVar Source #
FVS Warning Source #
Methods fvs :: Warning -> Set TVar Source #
FVS DelayedCt Source #
Methods fvs :: DelayedCt -> Set TVar Source #
FVS Goal Source #
Methods fvs :: Goal -> Set TVar Source #
FVS a => FVS [a] Source #
Methods fvs :: [a] -> Set TVar Source #
FVS a => FVS (Maybe a) Source #
Methods fvs :: Maybe a -> Set TVar Source #
(FVS a, FVS b) => FVS (a, b) Source #
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 #

Minimal complete definition

apSubst

Methods

apSubst :: Subst -> t -> t Source #

Instances

TVars Type Source #
Methods apSubst :: Subst -> Type -> 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.
Methods apSubst :: Subst -> Schema -> Schema Source #
TVars DeclDef Source #
Methods apSubst :: Subst -> DeclDef -> DeclDef Source #
TVars Decl Source #
Methods apSubst :: Subst -> Decl -> Decl Source #
TVars DeclGroup Source #
Methods apSubst :: Subst -> DeclGroup -> DeclGroup Source #
TVars Match Source #
Methods apSubst :: Subst -> Match -> Match Source #
TVars Expr Source #
Methods apSubst :: Subst -> Expr -> Expr Source #
TVars Module Source #
Methods apSubst :: Subst -> Module -> Module Source #
TVars ConstraintSource Source #
Methods apSubst :: Subst -> ConstraintSource -> ConstraintSource Source #
TVars Error Source #
Methods apSubst :: Subst -> Error -> Error Source #
TVars Warning Source #
Methods apSubst :: Subst -> Warning -> Warning Source #
TVars DelayedCt Source #
Methods apSubst :: Subst -> DelayedCt -> DelayedCt Source #
TVars HasGoal Source #
Methods apSubst :: Subst -> HasGoal -> HasGoal Source #
TVars Goal Source #
Methods apSubst :: Subst -> Goal -> Goal Source #
TVars Goals Source #
Methods apSubst :: Subst -> Goals -> Goals Source #
TVars t => TVars [t] Source #
Methods apSubst :: Subst -> [t] -> [t] Source #
TVars t => TVars (Maybe t) Source #
Methods apSubst :: Subst -> Maybe t -> Maybe t Source #
TVars a => TVars (TypeMap a) Source #
Methods apSubst :: Subst -> TypeMap a -> TypeMap a Source #
(TVars s, TVars t) => TVars (s, t) Source #
Methods apSubst :: Subst -> (s, t) -> (s, t) Source #
(Functor m, TVars a) => TVars (List m a) Source #
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 #