| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe |
| Language | Haskell98 |
Cryptol.TypeCheck.Monad
Description
- data InferInput = InferInput {
- inpRange :: Range
- inpVars :: Map Name Schema
- inpTSyns :: Map Name TySyn
- inpNewtypes :: Map Name Newtype
- inpNameSeeds :: NameSeeds
- inpMonoBinds :: Bool
- inpSolverConfig :: SolverConfig
- inpSearchPath :: [FilePath]
- inpPrimNames :: !PrimMap
- inpSupply :: !Supply
- data NameSeeds = NameSeeds {}
- nameSeeds :: NameSeeds
- data InferOutput a
- bumpCounter :: InferM ()
- runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
- newtype InferM a = IM {}
- data DefLoc
- data RO = RO {}
- data RW = RW {}
- 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 ()
- newName :: (NameSeeds -> (a, NameSeeds)) -> InferM a
- newGoalName :: InferM Int
- newTVar :: Doc -> Kind -> InferM TVar
- newTVar' :: Doc -> Set TVar -> Kind -> InferM TVar
- newTParam :: Maybe Name -> 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 :: Name -> InferM VarType
- lookupTVar :: Name -> InferM (Maybe Type)
- lookupTSyn :: Name -> InferM (Maybe TySyn)
- lookupNewtype :: Name -> InferM (Maybe Newtype)
- existVar :: Name -> Kind -> InferM Type
- getTSyns :: InferM (Map Name (DefLoc, TySyn))
- getNewtypes :: InferM (Map Name (DefLoc, Newtype))
- getTVars :: InferM (Set Name)
- getBoundInScope :: InferM (Set TVar)
- 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
- withVarType :: Name -> VarType -> InferM a -> InferM a
- withVarTypes :: [(Name, VarType)] -> InferM a -> InferM a
- withVar :: Name -> Schema -> 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
- newtype KindM a = KM {}
- data KRO = KRO {}
- data KRW = KRW {
- typeParams :: Map Name Kind
- kCtrs :: [(ConstraintSource, [Prop])]
- runKindM :: Bool -> [(Name, Maybe Kind, Type)] -> KindM a -> InferM (a, Map Name Kind, [(ConstraintSource, [Prop])])
- data LkpTyVar
- kLookupTyVar :: Name -> KindM (Maybe LkpTyVar)
- kWildOK :: KindM Bool
- kRecordError :: Error -> KindM ()
- kRecordWarning :: Warning -> KindM ()
- kNewType :: Doc -> Kind -> KindM Type
- kLookupTSyn :: Name -> KindM (Maybe TySyn)
- kLookupNewtype :: Name -> KindM (Maybe Newtype)
- 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
data InferInput Source #
Information needed for type inference.
Constructors
| InferInput | |
Fields
| |
Instances
This is used for generating various names.
data InferOutput a Source #
The results of type inference.
Constructors
| 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 # | |
bumpCounter :: InferM () Source #
runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a) Source #
Constructors
| IsLocal | |
| IsExternal |
Read-only component of the monad.
Constructors
| RO | |
Fields
| |
Read-write component of the monad.
Constructors
| RW | |
Fields
| |
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 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 -> Set TVar -> Kind -> InferM TVar Source #
Generate a new free type variable that depends on these additional type parameters.
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.
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.
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.
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 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).
Constructors
| KRW | |
Fields
| |
Arguments
| :: Bool | |
| -> [(Name, Maybe Kind, Type)] | 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.), 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.
This is what's returned when we lookup variables during kind checking.
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.
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 over-written).
kInRange :: Range -> KindM a -> KindM a Source #
The sub-computation is about the given range of the source code.
module Cryptol.TypeCheck.InferTypes