cryptol-2.8.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
- 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 `TVar` 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

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 #

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

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

Arguments

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

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