Cryptol.TypeCheck.Monad

Documentation

data LkpTyVar

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

Constructors

TLocalVar TParam (Maybe Kind)

Locally bound variable.

TOuterVar TParam

An outer binding.

data KRW

Constructors

KRW

Fields

• typeParams :: Map Name Kind

  kinds of (known) vars.

• kCtrs :: [(ConstraintSource, [Prop])]

data AllowWildCards

Do we allow wild cards in the given context.

Constructors

AllowWildCards

NoWildCards

data KRO

Constructors

KRO

Fields

• lazyTParams :: Map Name TParam

  lazy map, with tparams.

• allowWild :: AllowWildCards

  are type-wild cards allowed?

newtype KindM a

Constructors

KM

Fields

• unKM :: ReaderT KRO (StateT KRW InferM) a

Instances

Monad KindM

Defined in Cryptol.TypeCheck.Monad

Methods

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

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

return :: a -> KindM a

Functor KindM

Defined in Cryptol.TypeCheck.Monad

Methods

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

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

MonadFail KindM

Defined in Cryptol.TypeCheck.Monad

Methods

fail :: String -> KindM a

Applicative KindM

Defined in Cryptol.TypeCheck.Monad

Methods

pure :: a -> KindM a

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

liftA2 :: (a -> b -> c) -> KindM a -> KindM b -> KindM c

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

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

data RW

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 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 HasGoalSln

  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 its solution properly.

• iScope :: ![ModuleG ScopeName]

  Nested scopes we are currently checking, most nested first.

• iBindTypes :: !(Map Name Schema)

  Types of variables that we know about. We don't worry about scoping here because we assume the bindings all have different names.

• iSupply :: !Supply

data RO

Read-only component of the monad.

Constructors

RO

Fields

• iRange :: Range

  Source code being analysed

• iVars :: Map Name VarType

  Type of variable that are in scope These are only parameters vars that are in recursive component we are checking at the moment. If a var is not there, keep looking in the iScope

• iTVars :: [TParam]

  Type variable that are in scope

• iExtScope :: ModuleG ScopeName

  These are things we know about, but are not part of the modules we are currently constructing. XXX: this sould probably be an interface

• iSolvedHasLazy :: Map Int HasGoalSln

  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.

• iCallStacks :: Bool

  When this flag is true, retain source location information in typechecked terms

• iSolver :: Solver
• iPrimNames :: !PrimMap
• iSolveCounter :: !(IORef Int)

data ScopeName

Constructors

ExternalScope

LocalScope

SubModule Name

MTopModule ModName

newtype InferM a

Constructors

IM

Fields

• unIM :: ReaderT RO (StateT RW IO) a

Instances

Monad InferM

Defined in Cryptol.TypeCheck.Monad

Methods

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

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

return :: a -> InferM a

Functor InferM

Defined in Cryptol.TypeCheck.Monad

Methods

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

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

MonadFix InferM

Defined in Cryptol.TypeCheck.Monad

Methods

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

MonadFail InferM

Defined in Cryptol.TypeCheck.Monad

Methods

fail :: String -> InferM a

Applicative InferM

Defined in Cryptol.TypeCheck.Monad

Methods

pure :: a -> InferM a

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

liftA2 :: (a -> b -> c) -> InferM a -> InferM b -> InferM c

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

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

FreshM InferM

Defined in Cryptol.TypeCheck.Monad

Methods

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

data InferOutput a

The results of type inference.

Constructors

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

We found some errors

InferOK NameMap [(Range, Warning)] NameSeeds Supply a

Type inference was successful.

Instances

Show a => Show (InferOutput a)

Defined in Cryptol.TypeCheck.Monad

Methods

showsPrec :: Int -> InferOutput a -> ShowS

show :: InferOutput a -> String

showList :: [InferOutput a] -> ShowS

data NameSeeds

This is used for generating various names.

Constructors

NameSeeds

Fields

• seedTVar :: !Int
• seedGoal :: !Int

Instances

Show NameSeeds

Defined in Cryptol.TypeCheck.Monad

Methods

showsPrec :: Int -> NameSeeds -> ShowS

show :: NameSeeds -> String

showList :: [NameSeeds] -> ShowS

Generic NameSeeds

Defined in Cryptol.TypeCheck.Monad

Associated Types

type Rep NameSeeds :: Type -> Type

Methods

from :: NameSeeds -> Rep NameSeeds x

to :: Rep NameSeeds x -> NameSeeds

NFData NameSeeds

Defined in Cryptol.TypeCheck.Monad

Methods

rnf :: NameSeeds -> ()

type Rep NameSeeds

Defined in Cryptol.TypeCheck.Monad

type Rep NameSeeds = D1 ('MetaData "NameSeeds" "Cryptol.TypeCheck.Monad" "cryptol-2.12.0-1cEC2pVyc8sLwNRndAigau" '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

Information needed for type inference.

Constructors

InferInput

Fields

• inpRange :: Range

  Location of program source

• inpVars :: Map Name Schema

  Variables that are in scope

• inpTSyns :: Map Name TySyn

  Type synonyms that are in scope

• inpNewtypes :: Map Name Newtype

  Newtypes in scope

• inpAbstractTypes :: Map Name AbstractType

  Abstract types in scope

• inpParamTypes :: !(Map Name ModTParam)

  Type parameters

• inpParamConstraints :: ![Located Prop]

  Constraints on parameters

• inpParamFuns :: !(Map Name ModVParam)

  Value parameters

• inpNameSeeds :: NameSeeds

  Private state of type-checker

• inpMonoBinds :: Bool

  Should local bindings without signatures be monomorphized?

• inpCallStacks :: Bool

  Are we tracking call stacks?

• inpSearchPath :: [FilePath]

  Where to look for Cryptol theory file.

• inpPrimNames :: !PrimMap

  This is used when the type-checker needs to refer to a predefined identifier (e.g., number).

• inpSupply :: !Supply

  The supply for fresh name generation

• inpSolver :: Solver

  Solver connection for typechecking

nameSeeds :: NameSeeds

The initial seeds, used when checking a fresh program. XXX: why does this start at 10?

bumpCounter :: InferM ()

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

io :: IO a -> InferM a

inRange :: Range -> InferM a -> InferM a

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

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

curRange :: InferM Range

This is the current range that we are working on.

recordError :: Error -> InferM ()

Report an error.

recordWarning :: Warning -> InferM ()

getSolver :: InferM Solver

getPrimMap :: InferM PrimMap

Retrieve the mapping between identifiers and declarations in the prelude.

newGoal :: ConstraintSource -> Prop -> InferM Goal

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

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

getGoals :: InferM [Goal]

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

addGoals :: [Goal] -> InferM ()

Add a bunch of goals that need solving.

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

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

simpGoal :: Goal -> InferM [Goal]

simpGoals :: [Goal] -> InferM [Goal]

newHasGoal :: Selector -> Type -> Type -> InferM HasGoalSln

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 ()

Add a previously generate has constrained

getHasGoals :: InferM [HasGoal]

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

solveHasGoal :: Int -> HasGoalSln -> InferM ()

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

newParamName :: Namespace -> Ident -> InferM Name

Generate a fresh variable name to be used in a local binding.

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

newGoalName :: InferM Int

Generate a new name for a goal.

newTVar :: TypeSource -> Kind -> InferM TVar

Generate a new free type variable.

newTVar' :: TypeSource -> Set TParam -> Kind -> InferM TVar

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

checkParamKind :: TParam -> TPFlavor -> Kind -> InferM ()

Check that the given "flavor" of parameter is allowed to have the given type, and raise an error if not

newTParam :: TParam Name -> TPFlavor -> Kind -> InferM TParam

Generate a new free type variable.

newType :: TypeSource -> Kind -> InferM Type

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

unify :: TypeWithSource -> Type -> InferM [Prop]

Record that the two types should be syntactically equal.

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

Apply the accumulated substitution to something with free type variables.

applySubstPreds :: [Prop] -> InferM [Prop]

applySubstGoals :: [Goal] -> InferM [Goal]

getSubst :: InferM Subst

Get the substitution that we have accumulated so far.

extendSubst :: Subst -> InferM ()

Add to the accumulated substitution, checking that the datatype invariant for Subst is maintained.

varsWithAsmps :: InferM (Set TVar)

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

lookupVar :: Name -> InferM VarType

Lookup the type of a variable.

lookupTParam :: Name -> InferM (Maybe TParam)

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)

Lookup the definition of a type synonym.

lookupNewtype :: Name -> InferM (Maybe Newtype)

Lookup the definition of a newtype

lookupAbstractType :: Name -> InferM (Maybe AbstractType)

lookupParamType :: Name -> InferM (Maybe ModTParam)

Lookup the kind of a parameter type

lookupParamFun :: Name -> InferM (Maybe ModVParam)

Lookup the schema for a parameter function.

existVar :: Name -> Kind -> InferM Type

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 TySyn)

Returns the type synonyms that are currently in scope.

getNewtypes :: InferM (Map Name Newtype)

Returns the newtype declarations that are in scope.

getAbstractTypes :: InferM (Map Name AbstractType)

Returns the abstract type declarations that are in scope.

getParamFuns :: InferM (Map Name ModVParam)

Returns the parameter functions declarations

getParamTypes :: InferM (Map Name ModTParam)

Returns the abstract function declarations

getParamConstraints :: InferM [Located Prop]

Constraints on the module's parameters.

getTVars :: InferM (Set Name)

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

getBoundInScope :: InferM (Set TParam)

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

getMonoBinds :: InferM Bool

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

getCallStacks :: InferM Bool

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

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

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

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

newScope :: ScopeName -> InferM ()

Execute the given computation in a new top scope. The sub-computation would typically be validating a module.

newLocalScope :: InferM ()

newSubmoduleScope :: Name -> [Import] -> ExportSpec Name -> InferM ()

newModuleScope :: ModName -> [Import] -> ExportSpec Name -> InferM ()

updScope :: (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()

Update the current scope (first in the list). Assumes there is one.

endLocalScope :: InferM ([DeclGroup], Map Name TySyn)

endSubmodule :: InferM ()

endModule :: InferM Module

endModuleInstance :: InferM ()

getScope :: Semigroup a => (ModuleG ScopeName -> a) -> InferM a

Get an environment combining all nested scopes.

addDecls :: DeclGroup -> InferM ()

addTySyn :: TySyn -> InferM ()

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

addNewtype :: Newtype -> InferM ()

addPrimType :: AbstractType -> InferM ()

addParamType :: ModTParam -> InferM ()

addParamFun :: ModVParam -> InferM ()

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

addParameterConstraints :: [Located Prop] -> InferM ()

Add some assumptions for an entire module

inNewScope :: InferM a -> InferM a

Perform the given computation in a new scope (i.e., the subcomputation may use existential type variables). This is a different kind of scope from the nested modules one.

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

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

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

withVar :: Name -> Schema -> InferM a -> InferM a

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

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

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

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

runKindM

Arguments

:: 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 sub-computation and the computed kinds of the type parameters.

kLookupTyVar :: Name -> KindM (Maybe LkpTyVar)

Check if a name refers to a type variable.

kWildOK :: KindM AllowWildCards

Are type wild-cards OK in this context?

kRecordError :: Error -> KindM ()

Reports an error.

kRecordWarning :: Warning -> KindM ()

kIO :: IO a -> KindM a

kNewType :: TypeSource -> Kind -> KindM Type

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?

kLookupTSyn :: Name -> KindM (Maybe TySyn)

Lookup the definition of a type synonym.

kLookupNewtype :: Name -> KindM (Maybe Newtype)

Lookup the definition of a newtype.

kLookupParamType :: Name -> KindM (Maybe ModTParam)

kLookupAbstractType :: Name -> KindM (Maybe AbstractType)

kExistTVar :: Name -> Kind -> KindM Type

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

Replace the given bound variables with concrete types.

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

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

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

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

kInInferM :: InferM a -> KindM a

module Cryptol.TypeCheck.InferTypes