Copyright  (c) 20132016 Galois Inc. 

License  BSD3 
Maintainer  cryptol@galois.com 
Stability  provisional 
Portability  portable 
Safe Haskell  Safe 
Language  Haskell2010 
Synopsis
 data LkpTyVar
 data KRW = KRW {
 typeParams :: Map Name Kind
 kCtrs :: [(ConstraintSource, [Prop])]
 data AllowWildCards
 data KRO = KRO {}
 newtype KindM a = KM {}
 data RW = RW {}
 data RO = RO {
 iRange :: Range
 iVars :: Map Name VarType
 iTVars :: [TParam]
 iTSyns :: Map Name (DefLoc, TySyn)
 iNewtypes :: Map Name (DefLoc, Newtype)
 iParamTypes :: Map Name ModTParam
 iParamConstraints :: [Located Prop]
 iParamFuns :: Map Name ModVParam
 iSolvedHasLazy :: Map Int (Expr > Expr)
 iMonoBinds :: Bool
 iSolver :: Solver
 iPrimNames :: !PrimMap
 iSolveCounter :: !(IORef Int)
 data DefLoc
 newtype InferM a = IM {}
 data InferOutput a
 data NameSeeds = NameSeeds {}
 data InferInput = InferInput {
 inpRange :: Range
 inpVars :: Map Name Schema
 inpTSyns :: Map Name TySyn
 inpNewtypes :: Map Name Newtype
 inpParamTypes :: !(Map Name ModTParam)
 inpParamConstraints :: ![Located Prop]
 inpParamFuns :: !(Map Name ModVParam)
 inpNameSeeds :: NameSeeds
 inpMonoBinds :: Bool
 inpSolverConfig :: SolverConfig
 inpSearchPath :: [FilePath]
 inpPrimNames :: !PrimMap
 inpSupply :: !Supply
 nameSeeds :: NameSeeds
 bumpCounter :: InferM ()
 runInferM :: TVars a => InferInput > InferM a > IO (InferOutput a)
 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 ()
 getSolver :: InferM Solver
 getPrimMap :: InferM PrimMap
 newGoal :: ConstraintSource > Prop > InferM Goal
 newGoals :: ConstraintSource > [Prop] > InferM ()
 getGoals :: InferM [Goal]
 addGoals :: [Goal] > InferM ()
 collectGoals :: InferM a > InferM (a, [Goal])
 simpGoal :: Goal > InferM [Goal]
 simpGoals :: [Goal] > InferM [Goal]
 newHasGoal :: Selector > Type > Type > InferM (Expr > Expr)
 addHasGoal :: HasGoal > InferM ()
 getHasGoals :: InferM [HasGoal]
 solveHasGoal :: Int > (Expr > Expr) > InferM ()
 newParamName :: Ident > InferM Name
 newName :: (NameSeeds > (a, NameSeeds)) > InferM a
 newGoalName :: InferM Int
 newTVar :: TVarSource > Kind > InferM TVar
 newTVar' :: TVarSource > Set TParam > Kind > InferM TVar
 newTParam :: TParam Name > TPFlavor > Kind > InferM TParam
 newType :: TVarSource > Kind > InferM Type
 unify :: Type > Type > InferM [Prop]
 applySubst :: TVars t => t > InferM t
 applySubstPreds :: [Prop] > InferM [Prop]
 applySubstGoals :: [Goal] > InferM [Goal]
 getSubst :: InferM Subst
 extendSubst :: Subst > InferM ()
 varsWithAsmps :: InferM (Set TVar)
 lookupVar :: Name > InferM VarType
 lookupTParam :: Name > InferM (Maybe TParam)
 lookupTSyn :: Name > InferM (Maybe TySyn)
 lookupNewtype :: Name > InferM (Maybe Newtype)
 lookupParamType :: Name > InferM (Maybe ModTParam)
 lookupParamFun :: Name > InferM (Maybe ModVParam)
 existVar :: Name > Kind > InferM Type
 getTSyns :: InferM (Map Name (DefLoc, TySyn))
 getNewtypes :: InferM (Map Name (DefLoc, Newtype))
 getParamFuns :: InferM (Map Name ModVParam)
 getParamTypes :: InferM (Map Name ModTParam)
 getParamConstraints :: InferM [Located Prop]
 getTVars :: InferM (Set Name)
 getBoundInScope :: InferM (Set TParam)
 getMonoBinds :: InferM Bool
 checkTShadowing :: String > Name > 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
 withParamType :: ModTParam > InferM a > InferM a
 withVarType :: Name > VarType > InferM a > InferM a
 withVarTypes :: [(Name, VarType)] > InferM a > InferM a
 withVar :: Name > Schema > InferM a > InferM a
 withParamFuns :: [ModVParam] > InferM a > InferM a
 withParameterConstraints :: [Located Prop] > InferM a > InferM a
 withMonoType :: (Name, Located Type) > InferM a > InferM a
 withMonoTypes :: Map Name (Located Type) > InferM a > InferM a
 withDecls :: ([TySyn], Map Name Schema) > InferM a > InferM a
 inNewScope :: InferM a > InferM a
 runKindM :: AllowWildCards > [(Name, Maybe Kind, TParam)] > KindM a > InferM (a, Map Name Kind, [(ConstraintSource, [Prop])])
 kLookupTyVar :: Name > KindM (Maybe LkpTyVar)
 kWildOK :: KindM AllowWildCards
 kRecordError :: Error > KindM ()
 kRecordWarning :: Warning > KindM ()
 kNewType :: TVarSource > Kind > KindM Type
 kLookupTSyn :: Name > KindM (Maybe TySyn)
 kLookupNewtype :: Name > KindM (Maybe Newtype)
 kLookupParamType :: Name > KindM (Maybe ModTParam)
 kExistTVar :: Name > Kind > KindM Type
 kInstantiateT :: Type > [(TParam, Type)] > KindM Type
 kSetKind :: Name > Kind > KindM ()
 kInRange :: Range > KindM a > KindM a
 kNewGoals :: ConstraintSource > [Prop] > KindM ()
 kInInferM :: InferM a > KindM a
 module Cryptol.TypeCheck.InferTypes
Documentation
This is what's returned when we lookup variables during kind checking.
KRW  

KRO  

Readwrite component of the monad.
RW  

Readonly component of the monad.
RO  

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. 
Instances
Show a => Show (InferOutput a) Source #  
Defined in Cryptol.TypeCheck.Monad showsPrec :: Int > InferOutput a > ShowS # show :: InferOutput a > String # showList :: [InferOutput a] > ShowS # 
This is used for generating various names.
Instances
Show NameSeeds Source #  
Generic NameSeeds Source #  
NFData NameSeeds Source #  
Defined in Cryptol.TypeCheck.Monad  
type Rep NameSeeds Source #  
Defined in Cryptol.TypeCheck.Monad type Rep NameSeeds = D1 (MetaData "NameSeeds" "Cryptol.TypeCheck.Monad" "cryptol2.6.024w5HMDd2znGLrodkM4xJM" False) (C1 (MetaCons "NameSeeds" PrefixI True) (S1 (MetaSel (Just "seedTVar") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int) :*: S1 (MetaSel (Just "seedGoal") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int))) 
data InferInput Source #
Information needed for type inference.
InferInput  

Instances
Show InferInput Source #  
Defined in Cryptol.TypeCheck.Monad showsPrec :: Int > InferInput > ShowS # show :: InferInput > String # showList :: [InferInput] > ShowS # 
nameSeeds :: NameSeeds Source #
The initial seeds, used when checking a fresh program. XXX: why does this start at 10?
bumpCounter :: InferM () Source #
runInferM :: TVars a => InferInput > InferM a > IO (InferOutput 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.
recordError :: Error > InferM () Source #
Report an error.
recordWarning :: Warning > InferM () Source #
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.
collectGoals :: InferM a > InferM (a, [Goal]) Source #
Collect the goals emitted by the given subcomputation. 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
).
newParamName :: Ident > InferM Name Source #
Generate a fresh variable name to be used in a local binding.
newGoalName :: InferM Int Source #
Generate a new name for a goal.
newTVar' :: TVarSource > Set TParam > Kind > InferM TVar Source #
Generate a new free type variable that depends on these additional type parameters.
newTParam :: TParam Name > TPFlavor > Kind > InferM TParam Source #
Generate a new free type variable.
newType :: TVarSource > 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.
extendSubst :: Subst > InferM () Source #
Add to the accumulated substitution, checking that the datatype
invariant for Subst
is maintained.
varsWithAsmps :: InferM (Set TVar) Source #
Variables that are either mentioned in the environment or in a selector constraint.
lookupTParam :: Name > InferM (Maybe TParam) 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.
lookupParamFun :: Name > InferM (Maybe ModVParam) Source #
Lookup the schema for a parameter function.
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.
getBoundInScope :: InferM (Set TParam) Source #
Return the keys of the bound variables that are in scope.
getMonoBinds :: InferM Bool Source #
Retrieve the value of the `monobinds` 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 subcomputation is performed with the given type parameter in scope.
withTySyn :: TySyn > InferM a > InferM a Source #
The subcomputation is performed with the given typesynonym in scope.
withVarType :: Name > VarType > InferM a > InferM a Source #
The subcomputation is performed with the given variable in scope.
withParamFuns :: [ModVParam] > InferM a > InferM a Source #
The subcomputation is performed with the given abstract function in scope.
withParameterConstraints :: [Located Prop] > InferM a > InferM a Source #
Add some assumptions for an entire module
withMonoType :: (Name, Located Type) > InferM a > InferM a Source #
The subcomputation is performed with the given variables in scope.
withMonoTypes :: Map Name (Located Type) > InferM a > InferM a Source #
The subcomputation is performed with the given variables in scope.
withDecls :: ([TySyn], Map Name Schema) > InferM a > InferM a Source #
The subcomputation 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).
:: AllowWildCards  
> [(Name, Maybe Kind, TParam)]  See comment 
> KindM a  
> InferM (a, Map Name Kind, [(ConstraintSource, [Prop])]) 
The arguments to this function are as follows:
(type param. name, kind signature (opt.), type parameter)
The type parameter is just a thunk that we should not force. The reason is that the parameter depends on the kind that we are in the process of computing.
As a result we return the value of the subcomputation and the computed kinds of the type parameters.
kWildOK :: KindM AllowWildCards Source #
Are type wildcards OK in this context?
kRecordError :: Error > KindM () Source #
Reports an error.
kRecordWarning :: Warning > KindM () Source #
kNewType :: TVarSource > Kind > KindM Type Source #
Generate a fresh unification variable of the given kind.
NOTE: We do not simplify these, because we end up with bottom.
See hs
XXX: Perhaps we can avoid the recursion?
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 overwritten).
kInRange :: Range > KindM a > KindM a Source #
The subcomputation is about the given range of the source code.
module Cryptol.TypeCheck.InferTypes