Cryptol.TypeCheck.Subst

Documentation

data Subst

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.

Instances

Show Subst

Defined in Cryptol.TypeCheck.Subst

Methods

showsPrec :: Int -> Subst -> ShowS

show :: Subst -> String

showList :: [Subst] -> ShowS

PP Subst

Defined in Cryptol.TypeCheck.Subst

Methods

ppPrec :: Int -> Subst -> Doc

PP (WithNames Subst)

Defined in Cryptol.TypeCheck.Subst

Methods

ppPrec :: Int -> WithNames Subst -> Doc

emptySubst :: Subst

data SubstError

Reasons to reject a single-variable substitution.

Constructors

SubstRecursive

Type maps to a type containing the same variable.

SubstEscaped [TParam]

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

SubstKindMismatch Kind Kind

Type maps to a type with a different kind.

singleSubst :: TVar -> Type -> Either SubstError Subst

singleTParamSubst :: TParam -> Type -> Subst

uncheckedSingleSubst :: TVar -> Type -> Subst

(@@) :: Subst -> Subst -> Subst

defaultingSubst :: Subst -> Subst

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

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

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

class FVS t where

Methods

fvs :: t -> Set TVar

Instances

FVS Type

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Type -> Set TVar

FVS Schema

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Schema -> Set TVar

FVS DelayedCt

Defined in Cryptol.TypeCheck.InferTypes

Methods

fvs :: DelayedCt -> Set TVar

FVS Goal

Defined in Cryptol.TypeCheck.InferTypes

Methods

fvs :: Goal -> Set TVar

FVS Error

Defined in Cryptol.TypeCheck.Error

Methods

fvs :: Error -> Set TVar

FVS Warning

Defined in Cryptol.TypeCheck.Error

Methods

fvs :: Warning -> Set TVar

FVS a => FVS [a]

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: [a] -> Set TVar

FVS a => FVS (Maybe a)

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Maybe a -> Set TVar

(FVS a, FVS b) => FVS (a, b)

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: (a, b) -> Set TVar

apSubstMaybe :: Subst -> Type -> Maybe Type

Apply a substitution. Returns Nothing if nothing changed.

class TVars t where

Methods

apSubst

Arguments

:: Subst

-> t

-> t

replaces free vars

Instances

TVars Type

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Type -> Type

TVars Schema

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.

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Schema -> Schema

TVars DeclDef

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> DeclDef -> DeclDef

TVars Decl

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Decl -> Decl

TVars DeclGroup

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> DeclGroup -> DeclGroup

TVars Match

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Match -> Match

TVars Expr

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Expr -> Expr

TVars Module

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Module -> Module

TVars ConstraintSource

Defined in Cryptol.TypeCheck.InferTypes

Methods

apSubst :: Subst -> ConstraintSource -> ConstraintSource

TVars DelayedCt

Defined in Cryptol.TypeCheck.InferTypes

Methods

apSubst :: Subst -> DelayedCt -> DelayedCt

TVars HasGoal

Defined in Cryptol.TypeCheck.InferTypes

Methods

apSubst :: Subst -> HasGoal -> HasGoal

TVars Goal

Defined in Cryptol.TypeCheck.InferTypes

Methods

apSubst :: Subst -> Goal -> Goal

TVars Goals

Defined in Cryptol.TypeCheck.InferTypes

Methods

apSubst :: Subst -> Goals -> Goals

TVars Error

Defined in Cryptol.TypeCheck.Error

Methods

apSubst :: Subst -> Error -> Error

TVars Warning

Defined in Cryptol.TypeCheck.Error

Methods

apSubst :: Subst -> Warning -> Warning

TVars t => TVars [t]

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> [t] -> [t]

TVars t => TVars (Maybe t)

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Maybe t -> Maybe t

TVars a => TVars (TypeMap a)

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> TypeMap a -> TypeMap a

(TVars s, TVars t) => TVars (s, t)

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> (s, t) -> (s, t)

(Functor m, TVars a) => TVars (List m a)

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> List m a -> List m a

apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a

Apply the substitution to the keys of a type map.

substBinds :: Subst -> Set TVar

applySubstToVar :: Subst -> TVar -> Maybe Type

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