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.Monad

Description

Synopsis

- data InferInput = InferInput {
  - inpRange :: Range
  - inpVars :: Map QName Schema
  - inpTSyns :: Map QName TySyn
  - inpNewtypes :: Map QName Newtype
  - inpNameSeeds :: NameSeeds
  - inpMonoBinds :: Bool
  }
- data NameSeeds = NameSeeds {
  - seedTVar :: !Int
  - seedGoal :: !Int
  }
- nameSeeds :: NameSeeds
- data InferOutput a
  - = InferFailed [(Range, Warning)] [(Range, Error)]
  - | InferOK [(Range, Warning)] NameSeeds a
- runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
- newtype InferM a = IM {
  - unIM :: ReaderT RO (StateT RW IO) a
  }
- data DefLoc
  - = IsLocal
  - | IsExternal
- data RO = RO {
  - iRange :: Range
  - iVars :: Map QName VarType
  - iTVars :: [TParam]
  - iTSyns :: Map QName (DefLoc, TySyn)
  - iNewtypes :: Map QName (DefLoc, Newtype)
  - iSolvedHasLazy :: Map Int (Expr -> Expr)
  - iMonoBinds :: Bool
  }
- data RW = RW {
  - iErrors :: ![(Range, Error)]
  - iWarnings :: ![(Range, Warning)]
  - iSubst :: !Subst
  - iExistTVars :: [Map QName Type]
  - iSolvedHas :: Map Int (Expr -> Expr)
  - iNameSeeds :: !NameSeeds
  - iCts :: !Goals
  - iHasCts :: ![HasGoal]
  }
- io :: IO a -> InferM a
- inRange :: Range -> InferM a -> InferM a
- inRangeMb :: Maybe Range -> InferM a -> InferM a
- curRange :: InferM Range
- recordError :: Error -> InferM ()
- recordWarning :: Warning -> InferM ()
- newGoal :: ConstraintSource -> Prop -> InferM Goal
- newGoals :: ConstraintSource -> [Prop] -> InferM ()
- getGoals :: InferM [Goal]
- addGoals :: [Goal] -> InferM ()
- collectGoals :: InferM a -> InferM (a, [Goal])
- newHasGoal :: Selector -> Type -> Type -> InferM (Expr -> Expr)
- addHasGoal :: HasGoal -> InferM ()
- getHasGoals :: InferM [HasGoal]
- solveHasGoal :: Int -> (Expr -> Expr) -> InferM ()
- newName :: (NameSeeds -> (a, NameSeeds)) -> InferM a
- newGoalName :: InferM Int
- newTVar :: Doc -> Kind -> InferM TVar
- newTVar' :: Doc -> Set TVar -> Kind -> InferM TVar
- newTParam :: Maybe QName -> Kind -> InferM TParam
- newType :: Doc -> Kind -> InferM Type
- unify :: Type -> Type -> InferM [Prop]
- applySubst :: TVars t => t -> InferM t
- getSubst :: InferM Subst
- extendSubst :: Subst -> InferM ()
- varsWithAsmps :: InferM (Set TVar)
- lookupVar :: QName -> InferM VarType
- lookupTVar :: QName -> InferM (Maybe Type)
- lookupTSyn :: QName -> InferM (Maybe TySyn)
- lookupNewtype :: QName -> InferM (Maybe Newtype)
- existVar :: QName -> Kind -> InferM Type
- getTSyns :: InferM (Map QName (DefLoc, TySyn))
- getNewtypes :: InferM (Map QName (DefLoc, Newtype))
- getTVars :: InferM (Set QName)
- getBoundInScope :: InferM (Set TVar)
- getMonoBinds :: InferM Bool
- checkTShadowing :: String -> QName -> InferM ()
- withTParam :: TParam -> InferM a -> InferM a
- withTParams :: [TParam] -> InferM a -> InferM a
- withTySyn :: TySyn -> InferM a -> InferM a
- withNewtype :: Newtype -> InferM a -> InferM a
- withVarType :: QName -> VarType -> InferM a -> InferM a
- withVarTypes :: [(QName, VarType)] -> InferM a -> InferM a
- withVar :: QName -> Schema -> InferM a -> InferM a
- withMonoType :: (QName, Located Type) -> InferM a -> InferM a
- withMonoTypes :: Map QName (Located Type) -> InferM a -> InferM a
- withDecls :: ([TySyn], Map QName Schema) -> InferM a -> InferM a
- inNewScope :: InferM a -> InferM a
- newtype KindM a = KM {
  - unKM :: ReaderT KRO (StateT KRW InferM) a
  }
- data KRO = KRO {
  - lazyTVars :: Map QName Type
  - allowWild :: Bool
  }
- data KRW = KRW {
  - typeParams :: Map QName Kind
  }
- runKindM :: Bool -> [(QName, Maybe Kind, Type)] -> KindM a -> InferM (a, Map QName Kind)
- data LkpTyVar
  - = TLocalVar Type (Maybe Kind)
  - | TOuterVar Type
- kLookupTyVar :: QName -> KindM (Maybe LkpTyVar)
- kWildOK :: KindM Bool
- kRecordError :: Error -> KindM ()
- kRecordWarning :: Warning -> KindM ()
- kNewType :: Doc -> Kind -> KindM Type
- kLookupTSyn :: QName -> KindM (Maybe TySyn)
- kLookupNewtype :: QName -> KindM (Maybe Newtype)
- kExistTVar :: QName -> Kind -> KindM Type
- kInstantiateT :: Type -> [(TParam, Type)] -> KindM Type
- kSetKind :: QName -> Kind -> KindM ()
- kInRange :: Range -> KindM a -> KindM a
- kNewGoals :: ConstraintSource -> [Prop] -> KindM ()
- kInInferM :: InferM a -> KindM a
- module Cryptol.TypeCheck.InferTypes

# Documentation

data InferInput Source

Information needed for type inference.

Constructors

InferInput |

Fields

inpRange :: Range

  Location of program source

inpVars :: Map QName Schema

  Variables that are in scope

inpTSyns :: Map QName TySyn

  Type synonyms that are in scope

inpNewtypes :: Map QName Newtype

  Newtypes in scope

inpNameSeeds :: NameSeeds

  Private state of type-checker

inpMonoBinds :: Bool

  Should local bindings without signatures be monomorphized?

Instances

Show InferInput Source |

data NameSeeds Source

This is used for generating various names.

Constructors

NameSeeds |

Fields

seedTVar :: !Int
seedGoal :: !Int

Instances

Show NameSeeds Source |

nameSeeds :: NameSeeds Source

The initial seeds, used when checking a fresh program.

data InferOutput a Source

The results of type inference.

Constructors

InferFailed [(Range, Warning)] [(Range, Error)] | We found some errors
InferOK [(Range, Warning)] NameSeeds a | Type inference was successful.

Instances

Show a => Show (InferOutput a) Source |

runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a) Source

newtype InferM a Source

Constructors

IM |

Fields

unIM :: ReaderT RO (StateT RW IO) a

Instances

Monad InferM Source |
Functor InferM Source |
MonadFix InferM Source |
Applicative InferM Source |

data DefLoc Source

Constructors

IsLocal |
IsExternal |

data RO Source

Read-only component of the monad.

Constructors

RO |

Fields

iRange :: Range

  Source code being analysed

iVars :: Map QName VarType

  Type of variable that are in scope

iTVars :: [TParam]

  Type variable that are in scope

iTSyns :: Map QName (DefLoc, TySyn)

  Type synonyms that are in scope

iNewtypes :: Map QName (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.

data RW Source

Read-write component of the monad.

Constructors

RW |

Fields

iErrors :: ![(Range, Error)]

  Collected errors

iWarnings :: ![(Range, Warning)]

  Collected warnings

iSubst :: !Subst

  Accumulated substitution

iExistTVars :: [Map QName 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.

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.

inRangeMb :: Maybe Range -> InferM a -> InferM a Source

curRange :: InferM Range Source

This is the current range that we are working on.

recordError :: Error -> InferM () Source

Report an error.

recordWarning :: Warning -> InferM () Source

newGoal :: ConstraintSource -> Prop -> InferM Goal Source

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`).

newName :: (NameSeeds -> (a, NameSeeds)) -> InferM a Source

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 QName -> 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 :: QName -> InferM VarType Source

Lookup the type of a variable.

lookupTVar :: QName -> 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 :: QName -> InferM (Maybe TySyn) Source

Lookup the definition of a type synonym.

lookupNewtype :: QName -> InferM (Maybe Newtype) Source

Lookup the definition of a newtype

existVar :: QName -> 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 QName (DefLoc, TySyn)) Source

Returns the type synonyms that are currently in scope.

getNewtypes :: InferM (Map QName (DefLoc, Newtype)) Source

Returns the newtype declarations that are in scope.

getTVars :: InferM (Set QName) 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 -> QName -> 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.

withTParams :: [TParam] -> InferM a -> InferM a Source

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

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

withNewtype :: Newtype -> InferM a -> InferM a Source

withVarType :: QName -> VarType -> InferM a -> InferM a Source

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

withVarTypes :: [(QName, VarType)] -> InferM a -> InferM a Source

withVar :: QName -> Schema -> InferM a -> InferM a Source

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

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

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

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

withDecls :: ([TySyn], Map QName 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

Constructors

KM |

Fields

unKM :: ReaderT KRO (StateT KRW InferM) a

Instances

Monad KindM Source |
Functor KindM Source |
Applicative KindM Source |

data KRO Source

Constructors

KRO |

Fields

lazyTVars :: Map QName Type

  lazy map, with tyvars.

allowWild :: Bool

  are type-wild cards allowed?

data KRW Source

Constructors

KRW |

Fields

typeParams :: Map QName Kind

  kinds of (known) vars.

runKindM Source

Arguments

:: Bool |
-> [(QName, Maybe Kind, Type)] | See comment
-> KindM a |
-> InferM (a, Map QName 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.

Constructors

TLocalVar Type (Maybe Kind) | Locally bound variable.
TOuterVar Type | An outer binding.

kLookupTyVar :: QName -> 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.

kRecordWarning :: Warning -> KindM () Source

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

Generate a fresh unification variable of the given kind.

kLookupTSyn :: QName -> KindM (Maybe TySyn) Source

Lookup the definition of a type synonym.

kLookupNewtype :: QName -> KindM (Maybe Newtype) Source

Lookup the definition of a newtype.

kExistTVar :: QName -> Kind -> KindM Type Source

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

Replace the given bound variables with concrete types.

kSetKind :: QName -> 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.

kNewGoals :: ConstraintSource -> [Prop] -> KindM () Source

kInInferM :: InferM a -> KindM a Source

module Cryptol.TypeCheck.InferTypes