cryptol-2.2.3: Cryptol: The Language of Cryptography

Copyright(c) 2013-2015 Galois, Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell98

Cryptol.TypeCheck.Subst

Description

 

Synopsis

Documentation

data Subst Source

Constructors

S 

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.

class FVS t where Source

Methods

fvs :: t -> Set TVar Source

Instances

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

class TVars t where Source

Methods

apSubst Source

Arguments

:: Subst 
-> t 
-> t

replaces free vars

Instances

TVars Decl 
TVars DeclGroup 
TVars Match 
TVars Expr 
TVars Type 
TVars Schema

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 
TVars ConstraintSource 
TVars Error 
TVars Warning 
TVars DelayedCt 
TVars HasGoal 
TVars Goal 
TVars Goals 
TVars t => TVars [t] 
TVars t => TVars (Maybe t) 
TVars a => TVars (TypeMap a) 
(TVars s, TVars t) => TVars (s, t) 
(Functor m, TVars a) => TVars (List m a) 

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.