cryptol-3.0.0: Cryptol: The Language of Cryptography

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
  - = SubstRecursive
  - | SubstEscaped [TParam]
  - | SubstKindMismatch Kind Kind
- 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
  - 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)]
- fmap' :: Traversable t => (a -> b) -> t a -> t b
- (!$) :: (a -> b) -> a -> b
- (.$) :: (a -> b) -> a -> b
- mergeDistinctSubst :: [Subst] -> Subst

# Documentation

data Subst Source #

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

Instances details

Show Subst Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods showsPrec :: Int -> Subst -> ShowS Source # show :: Subst -> String Source # showList :: [Subst] -> ShowS Source #
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 #

data SubstError Source #

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 Source #

singleTParamSubst :: TParam -> Type -> Subst Source #

uncheckedSingleSubst :: 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

Instances details

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 FFITypeError Source # |
Instance details Defined in Cryptol.TypeCheck.FFI.Error Methods fvs :: FFITypeError -> Set TVar Source #
FVS FFITypeErrorReason Source # |
Instance details Defined in Cryptol.TypeCheck.FFI.Error Methods fvs :: FFITypeErrorReason -> 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 Schema Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Schema -> Set TVar Source #
FVS Type Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Type -> 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 [a] Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: [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 Decl Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Decl -> Decl Source #
TVars DeclDef Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> DeclDef -> DeclDef Source #
TVars DeclGroup Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> DeclGroup -> DeclGroup Source #
TVars Expr Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Expr -> Expr Source #
TVars Match Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Match -> Match Source #
TVars TCTopEntity Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> TCTopEntity -> TCTopEntity 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 FFITypeError Source # |
Instance details Defined in Cryptol.TypeCheck.FFI.Error Methods apSubst :: Subst -> FFITypeError -> FFITypeError Source #
TVars FFITypeErrorReason Source # |
Instance details Defined in Cryptol.TypeCheck.FFI.Error Methods apSubst :: Subst -> FFITypeErrorReason -> FFITypeErrorReason 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 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 HasGoal Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> HasGoal -> HasGoal 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 TySyn Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> TySyn -> TySyn Source #
TVars Type Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Type -> Type Source #
TVars (ModuleG names) Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> ModuleG names -> ModuleG names Source #
TVars a => TVars (TypeMap a) Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> TypeMap a -> TypeMap a Source #
TVars t => TVars (Maybe t) Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Maybe t -> Maybe t Source #
TVars t => TVars [t] Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> [t] -> [t] Source #
TVars a => TVars (Map k a) Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Map k a -> Map k a 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 #
(TVars s, TVars t) => TVars (s, t) Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> (s, t) -> (s, t) 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 #

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 `$`.

mergeDistinctSubst :: [Subst] -> Subst Source #