cryptol-2.2.6: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2015 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
  - fvs :: t -> Set TVar
- class TVars t where
  - apSubst :: Subst -> t -> t
- 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 |
PP Subst Source |
PP (WithNames Subst) 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

Methods

fvs :: t -> Set TVar Source

Instances

FVS Type Source |
FVS Schema Source |
FVS Error Source |
FVS Warning Source |
FVS DelayedCt Source |
FVS Goal Source |
FVS a => FVS [a] Source |
(FVS a, FVS b) => FVS (a, b) Source |

class TVars t where Source

Methods

apSubst Source

Arguments

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

Instances

TVars Decl Source |
TVars DeclGroup Source |
TVars Match Source |
TVars Expr Source |
TVars 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.
TVars Module Source |
TVars ConstraintSource Source |
TVars Error Source |
TVars Warning Source |
TVars DelayedCt Source |
TVars HasGoal Source |
TVars Goal Source |
TVars Goals Source |
TVars t => TVars [t] Source |
TVars t => TVars (Maybe t) Source |
TVars a => TVars (TypeMap a) Source |
(TVars s, TVars t) => TVars (s, t) Source |
(Functor m, TVars a) => TVars (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.