cryptol-2.4.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois, Inc.
Safe HaskellSafe






data InferInput Source #

Information needed for type inference.




data NameSeeds Source #

This is used for generating various names.





Show NameSeeds Source # 
Generic NameSeeds Source # 

Associated Types

type Rep NameSeeds :: * -> * #

NFData NameSeeds Source # 


rnf :: NameSeeds -> () #

type Rep NameSeeds Source # 
type Rep NameSeeds = D1 (MetaData "NameSeeds" "Cryptol.TypeCheck.Monad" "cryptol-2.4.0-AtabUoGsZJn8kSvO8P84NP" False) (C1 (MetaCons "NameSeeds" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "seedTVar") NoSourceUnpackedness SourceStrict DecidedUnpack) (Rec0 Int)) (S1 (MetaSel (Just Symbol "seedGoal") NoSourceUnpackedness SourceStrict DecidedUnpack) (Rec0 Int))))

nameSeeds :: NameSeeds Source #

The initial seeds, used when checking a fresh program.

data InferOutput a Source #

The results of type inference.


InferFailed [(Range, Warning)] [(Range, Error)]

We found some errors

InferOK [(Range, Warning)] NameSeeds Supply a

Type inference was successful.


newtype InferM a Source #





Monad InferM Source # 


(>>=) :: InferM a -> (a -> InferM b) -> InferM b #

(>>) :: InferM a -> InferM b -> InferM b #

return :: a -> InferM a #

fail :: String -> InferM a #

Functor InferM Source # 


fmap :: (a -> b) -> InferM a -> InferM b #

(<$) :: a -> InferM b -> InferM a #

MonadFix InferM Source # 


mfix :: (a -> InferM a) -> InferM a #

Applicative InferM Source # 


pure :: a -> InferM a #

(<*>) :: InferM (a -> b) -> InferM a -> InferM b #

(*>) :: InferM a -> InferM b -> InferM b #

(<*) :: InferM a -> InferM b -> InferM a #

FreshM InferM Source # 


liftSupply :: (Supply -> (a, Supply)) -> InferM a Source #

data DefLoc Source #



data RO Source #

Read-only component of the monad.




  • iRange :: Range

    Source code being analysed

  • iVars :: Map Name VarType

    Type of variable that are in scope

  • iTVars :: [TParam]

    Type variable that are in scope

  • iTSyns :: Map Name (DefLoc, TySyn)

    Type synonyms that are in scope

  • iNewtypes :: Map Name (DefLoc, Newtype)

    Newtype declarations in scope

    NOTE: type synonyms take precedence over newtype. The reason is that we can define local type synonyms, but not local newtypes. So, either a type-synonym shadows a newtype, or it was declared at the top-level, but then there can't be a newtype with the same name (this should be caught by the renamer).

  • iSolvedHasLazy :: Map Int (Expr -> Expr)

    NOTE: This field is lazy in an important way! It is the final version of iSolvedHas in RW, and the two are tied together through recursion. The field is here so that we can look thing up before they are defined, which is OK because we don't need to know the results until everything is done.

  • iMonoBinds :: Bool

    When this flag is set to true, bindings that lack signatures in where-blocks will never be generalized. Bindings with type signatures, and all bindings at top level are unaffected.

  • iSolver :: Solver
  • iPrimNames :: !PrimMap

data RW Source #

Read-write component of the monad.




  • iErrors :: ![(Range, Error)]

    Collected errors

  • iWarnings :: ![(Range, Warning)]

    Collected warnings

  • iSubst :: !Subst

    Accumulated substitution

  • iExistTVars :: [Map Name Type]

    These keeps track of what existential type variables are available. When we start checking a function, we push a new scope for its arguments, and we pop it when we are done checking the function body. The front element of the list is the current scope, which is the only thing that will be modified, as follows. When we encounter a existential type variable: 1. we look in all scopes to see if it is already defined. 2. if it was not defined, we create a fresh type variable, and we add it to the current scope. 3. it is an error if we encounter an existential variable but we have no current scope.

  • iSolvedHas :: Map Int (Expr -> Expr)

    Selector constraints that have been solved (ref. iSolvedSelectorsLazy)

  • iNameSeeds :: !NameSeeds
  • iCts :: !Goals

    Ordinary constraints

  • iHasCts :: ![HasGoal]

    Tuple/record projection constraints. The Int is the "name" of the constraint, used so that we can name it solution properly.

  • iSupply :: !Supply

io :: IO a -> InferM a Source #

inRange :: Range -> InferM a -> InferM a Source #

The monadic computation is about the given range of source code. This is useful for error reporting.

curRange :: InferM Range Source #

This is the current range that we are working on.

recordError :: Error -> InferM () Source #

Report an error.

getPrimMap :: InferM PrimMap Source #

Retrieve the mapping between identifiers and declarations in the prelude.

newGoals :: ConstraintSource -> [Prop] -> InferM () Source #

Record some constraints that need to be solved. The string explains where the constraints came from.

getGoals :: InferM [Goal] Source #

The constraints are removed, and returned to the caller. The substitution IS applied to them.

addGoals :: [Goal] -> InferM () Source #

Add a bunch of goals that need solving.

collectGoals :: InferM a -> InferM (a, [Goal]) Source #

Collect the goals emitted by the given sub-computation. Does not emit any new goals.

newHasGoal :: Selector -> Type -> Type -> InferM (Expr -> Expr) Source #

Record a constraint that when we select from the first type, we should get a value of the second type. The returned function should be used to wrap the expression from which we are selecting (i.e., the record or tuple). Plese note that the resulting expression should not be forced before the constraint is solved.

addHasGoal :: HasGoal -> InferM () Source #

Add a previously generate has constrained

getHasGoals :: InferM [HasGoal] Source #

Get the Has constraints. Each of this should either be solved, or added back using addHasGoal.

solveHasGoal :: Int -> (Expr -> Expr) -> InferM () Source #

Specify the solution (`Expr -> Expr`) for the given constraint (Int).

newGoalName :: InferM Int Source #

Generate a new name for a goal.

newTVar :: Doc -> Kind -> InferM TVar Source #

Generate a new free type variable.

newTVar' :: Doc -> Set TVar -> Kind -> InferM TVar Source #

Generate a new free type variable that depends on these additional type parameters.

newTParam :: Maybe Name -> Kind -> InferM TParam Source #

Generate a new free type variable.

newType :: Doc -> Kind -> InferM Type Source #

Generate an unknown type. The doc is a note about what is this type about.

unify :: Type -> Type -> InferM [Prop] Source #

Record that the two types should be syntactically equal.

applySubst :: TVars t => t -> InferM t Source #

Apply the accumulated substitution to something with free type variables.

getSubst :: InferM Subst Source #

Get the substitution that we have accumulated so far.

extendSubst :: Subst -> InferM () Source #

Add to the accumulated substitution.

varsWithAsmps :: InferM (Set TVar) Source #

Variables that are either mentioned in the environment or in a selector constraint.

lookupVar :: Name -> InferM VarType Source #

Lookup the type of a variable.

lookupTVar :: Name -> InferM (Maybe Type) Source #

Lookup a type variable. Return Nothing if there is no such variable in scope, in which case we must be dealing with a type constant.

lookupTSyn :: Name -> InferM (Maybe TySyn) Source #

Lookup the definition of a type synonym.

lookupNewtype :: Name -> InferM (Maybe Newtype) Source #

Lookup the definition of a newtype

existVar :: Name -> Kind -> InferM Type Source #

Check if we already have a name for this existential type variable and, if so, return the definition. If not, try to create a new definition, if this is allowed. If not, returns nothing.

getTSyns :: InferM (Map Name (DefLoc, TySyn)) Source #

Returns the type synonyms that are currently in scope.

getNewtypes :: InferM (Map Name (DefLoc, Newtype)) Source #

Returns the newtype declarations that are in scope.

getTVars :: InferM (Set Name) Source #

Get the set of bound type variables that are in scope.

getBoundInScope :: InferM (Set TVar) Source #

Return the keys of the bound variables that are in scope.

getMonoBinds :: InferM Bool Source #

Retrieve the value of the `mono-binds` option.

checkTShadowing :: String -> Name -> InferM () Source #

We disallow shadowing between type synonyms and type variables because it is confusing. As a bonus, in the implementation we don't need to worry about where we lookup things (i.e., in the variable or type synonym environment.

withTParam :: TParam -> InferM a -> InferM a Source #

The sub-computation is performed with the given type parameter in scope.

withTySyn :: TySyn -> InferM a -> InferM a Source #

The sub-computation is performed with the given type-synonym in scope.

withVarType :: Name -> VarType -> InferM a -> InferM a Source #

The sub-computation is performed with the given variable in scope.

withMonoType :: (Name, Located Type) -> InferM a -> InferM a Source #

The sub-computation is performed with the given variables in scope.

withMonoTypes :: Map Name (Located Type) -> InferM a -> InferM a Source #

The sub-computation is performed with the given variables in scope.

withDecls :: ([TySyn], Map Name Schema) -> InferM a -> InferM a Source #

The sub-computation is performed with the given type synonyms and variables in scope.

inNewScope :: InferM a -> InferM a Source #

Perform the given computation in a new scope (i.e., the subcomputation may use existential type variables).

newtype KindM a Source #





Monad KindM Source # 


(>>=) :: KindM a -> (a -> KindM b) -> KindM b #

(>>) :: KindM a -> KindM b -> KindM b #

return :: a -> KindM a #

fail :: String -> KindM a #

Functor KindM Source # 


fmap :: (a -> b) -> KindM a -> KindM b #

(<$) :: a -> KindM b -> KindM a #

Applicative KindM Source # 


pure :: a -> KindM a #

(<*>) :: KindM (a -> b) -> KindM a -> KindM b #

(*>) :: KindM a -> KindM b -> KindM b #

(<*) :: KindM a -> KindM b -> KindM a #

data KRO Source #




data KRW Source #




runKindM Source #


:: Bool 
-> [(Name, Maybe Kind, Type)]

See comment

-> KindM a 
-> InferM (a, Map Name Kind) 

The arguments to this function are as follows:

(type param. name, kind signature (opt.), a type representing the param)

The type representing the parameter is just a thunk that we should not force. The reason is that the type depnds on the kind of parameter, that we are in the process of computing.

As a result we return the value of the sub-computation and the computed kinds of the type parameters.

data LkpTyVar Source #

This is what's returned when we lookup variables during kind checking.


TLocalVar Type (Maybe Kind)

Locally bound variable.

TOuterVar Type

An outer binding.

kLookupTyVar :: Name -> KindM (Maybe LkpTyVar) Source #

Check if a name refers to a type variable.

kWildOK :: KindM Bool Source #

Are type wild-cards OK in this context?

kRecordError :: Error -> KindM () Source #

Reports an error.

kNewType :: Doc -> Kind -> KindM Type Source #

Generate a fresh unification variable of the given kind.

kLookupTSyn :: Name -> KindM (Maybe TySyn) Source #

Lookup the definition of a type synonym.

kLookupNewtype :: Name -> KindM (Maybe Newtype) Source #

Lookup the definition of a newtype.

kInstantiateT :: Type -> [(TParam, Type)] -> KindM Type Source #

Replace the given bound variables with concrete types.

kSetKind :: Name -> Kind -> KindM () Source #

Record the kind for a local type variable. This assumes that we already checked that there was no other valid kind for the variable (if there was one, it gets over-written).

kInRange :: Range -> KindM a -> KindM a Source #

The sub-computation is about the given range of the source code.