cryptol-2.11.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Cryptol.TypeCheck.Subst

Description

 
Synopsis

Documentation

data Subst Source #

A Subst value represents a substitution that maps each TVar 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 TVar 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 TVar in the substitution must map to a Type of the same kind.

Instances

Instances details
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 #

data SubstError Source #

Reasons to reject a single-variable substitution.

Constructors

SubstRecursive

TVar maps to a type containing the same variable.

SubstEscaped [TParam]

TVar maps to a type containing one or more out-of-scope bound variables.

SubstKindMismatch Kind Kind

TVar maps to a type with a different kind.

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.

class FVS t where Source #

Methods

fvs :: t -> Set TVar Source #

Instances

Instances details
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 :: Subst -> t -> t Source #

Replaces free variables. To prevent space leaks when used with large Subst values, every instance of apSubst should satisfy a strictness property: Forcing evaluation of apSubst s x should also force the evaluation of all recursive calls to apSubst s. This ensures that unevaluated thunks will not cause Subst values to be retained on the heap.

Instances

Instances details
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

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

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

TVars DelayedCt Source # 
Instance details

Defined in Cryptol.TypeCheck.InferTypes

TVars HasGoal Source # 
Instance details

Defined in Cryptol.TypeCheck.InferTypes

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

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 #

(Traversable 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.

fmap' :: Traversable t => (a -> b) -> t a -> t b Source #

Strict variant of fmap.

(!$) :: (a -> b) -> a -> b infixl 0 Source #

Left-associative variant of the strict application operator $!.

(.$) :: (a -> b) -> a -> b infixl 0 Source #

Left-associative variant of the application operator $.