cryptol-2.4.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 | Haskell98

Cryptol.TypeCheck.Subst

Description

Synopsis

- data Subst = S {
  - suMap :: !(Map TVar Type)
  - suDefaulting :: !Bool
  }
- emptySubst :: Subst
- singleSubst :: TVar -> Type -> Subst
- (@@) :: Subst -> Subst -> Subst
- defaultingSubst :: Subst -> Subst
- listSubst :: [(TVar, Type)] -> Subst
- isEmptySubst :: Subst -> Bool
- substToList :: Subst -> Maybe [(TVar, Type)]
- class FVS t where
- apSubstMaybe :: Subst -> Type -> Maybe Type
- class TVars t where
- defaultFreeVar :: TVar -> Type
- apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a

# Documentation

data Subst Source #

Constructors

S |

Fields

- suMap :: !(Map TVar Type)
- suDefaulting :: !Bool

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 #

substToList :: Subst -> Maybe [(TVar, Type)] 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 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 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 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 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 #

defaultFreeVar :: TVar -> Type Source #

Pick types for unconstrained unification variables.

apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a Source #

Apply the substitution to the keys of a type map.