Cryptol.TypeCheck.InferTypes

This module contains types used during type inference.

Documentation

data SolverConfig

Constructors

SolverConfig

Fields

• solverPath :: FilePath

  The SMT solver to invoke

• solverArgs :: [String]

  Additional arguments to pass to the solver

• solverVerbose :: Int

  How verbose to be when type-checking

• solverPreludePath :: [FilePath]

  Look for the solver prelude in these locations.

Instances

Generic SolverConfig

Defined in Cryptol.TypeCheck.InferTypes

Associated Types

type Rep SolverConfig :: Type -> Type

Methods

from :: SolverConfig -> Rep SolverConfig x

to :: Rep SolverConfig x -> SolverConfig

Show SolverConfig

Defined in Cryptol.TypeCheck.InferTypes

Methods

showsPrec :: Int -> SolverConfig -> ShowS

show :: SolverConfig -> String

showList :: [SolverConfig] -> ShowS

NFData SolverConfig

Defined in Cryptol.TypeCheck.InferTypes

Methods

rnf :: SolverConfig -> ()

type Rep SolverConfig

Defined in Cryptol.TypeCheck.InferTypes

type Rep SolverConfig = D1 ('MetaData "SolverConfig" "Cryptol.TypeCheck.InferTypes" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "SolverConfig" 'PrefixI 'True) ((S1 ('MetaSel ('Just "solverPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "solverArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :*: (S1 ('MetaSel ('Just "solverVerbose") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "solverPreludePath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]))))

defaultSolverConfig :: [FilePath] -> SolverConfig

A default configuration for using Z3, where the solver prelude is expected to be found in the given search path.

data VarType

The types of variables in the environment.

Constructors

ExtVar Schema

Known type

CurSCC Expr Type

Part of current SCC. The expression will replace the variable, after we are done with the SCC. In this way a variable that gets generalized is replaced with an appropriate instantiation of itself.

data Goals

Constructors

Goals

Fields

• goalSet :: Set Goal

  A bunch of goals, not including the ones in literalGoals.

• saturatedPropSet :: Set Prop

  The set of nonliteral goals, saturated by all superclass implications

• literalGoals :: Map TVar LitGoal

  An entry (a,t) corresponds to Literal t a.

• literalLessThanGoals :: Map TVar LitGoal

  An entry (a,t) corresponds to LiteralLessThan t a.

Instances

Show Goals

Defined in Cryptol.TypeCheck.InferTypes

Methods

showsPrec :: Int -> Goals -> ShowS

show :: Goals -> String

showList :: [Goals] -> ShowS

TVars Goals

Defined in Cryptol.TypeCheck.InferTypes

Methods

apSubst :: Subst -> Goals -> Goals

type LitGoal = Goal

This abuses the type Goal a bit. The goal field contains only the numeric part of the Literal constraint. For example, (a, Goal { goal = t }) representats the goal for Literal t a

litGoalToGoal :: (TVar, LitGoal) -> Goal

goalToLitGoal :: Goal -> Maybe (TVar, LitGoal)

litLessThanGoalToGoal :: (TVar, LitGoal) -> Goal

goalToLitLessThanGoal :: Goal -> Maybe (TVar, LitGoal)

emptyGoals :: Goals

nullGoals :: Goals -> Bool

fromGoals :: Goals -> [Goal]

goalsFromList :: [Goal] -> Goals

insertGoal :: Goal -> Goals -> Goals

data Goal

Something that we need to find evidence for.

Constructors

Goal

Fields

• goalSource :: ConstraintSource

  What it is about

• goalRange :: Range

  Part of source code that caused goal

• goal :: Prop

  What needs to be proved

Instances

Generic Goal

Defined in Cryptol.TypeCheck.InferTypes

Associated Types

type Rep Goal :: Type -> Type

Methods

from :: Goal -> Rep Goal x

to :: Rep Goal x -> Goal

Show Goal

Defined in Cryptol.TypeCheck.InferTypes

Methods

showsPrec :: Int -> Goal -> ShowS

show :: Goal -> String

showList :: [Goal] -> ShowS

TVars Goal

Defined in Cryptol.TypeCheck.InferTypes

Methods

apSubst :: Subst -> Goal -> Goal

FVS Goal

Defined in Cryptol.TypeCheck.InferTypes

Methods

fvs :: Goal -> Set TVar

NFData Goal

Defined in Cryptol.TypeCheck.InferTypes

Methods

rnf :: Goal -> ()

Eq Goal

Defined in Cryptol.TypeCheck.InferTypes

Methods

(==) :: Goal -> Goal -> Bool

(/=) :: Goal -> Goal -> Bool

Ord Goal

Defined in Cryptol.TypeCheck.InferTypes

Methods

compare :: Goal -> Goal -> Ordering

(<) :: Goal -> Goal -> Bool

(<=) :: Goal -> Goal -> Bool

(>) :: Goal -> Goal -> Bool

(>=) :: Goal -> Goal -> Bool

max :: Goal -> Goal -> Goal

min :: Goal -> Goal -> Goal

PP (WithNames Goal)

Defined in Cryptol.TypeCheck.InferTypes

Methods

ppPrec :: Int -> WithNames Goal -> Doc

type Rep Goal

Defined in Cryptol.TypeCheck.InferTypes

type Rep Goal = D1 ('MetaData "Goal" "Cryptol.TypeCheck.InferTypes" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "Goal" 'PrefixI 'True) (S1 ('MetaSel ('Just "goalSource") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ConstraintSource) :*: (S1 ('MetaSel ('Just "goalRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "goal") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Prop))))

data HasGoal

Constructors

HasGoal

Fields

• hasName :: !Int

  This is the "name" of the constraint, used to find the solution for ellaboration.

• hasGoal :: Goal

Instances

Show HasGoal

Defined in Cryptol.TypeCheck.InferTypes

Methods

showsPrec :: Int -> HasGoal -> ShowS

show :: HasGoal -> String

showList :: [HasGoal] -> ShowS

TVars HasGoal

Defined in Cryptol.TypeCheck.InferTypes

Methods

apSubst :: Subst -> HasGoal -> HasGoal

data HasGoalSln

A solution for a HasGoal

Constructors

HasGoalSln

Fields

• hasDoSelect :: Expr -> Expr

  Select a specific field from the input expsression.

• hasDoSet :: Expr -> Expr -> Expr

  Set a field of the first expression to the second expression

data DelayedCt

Delayed implication constraints, arising from user-specified type sigs.

Constructors

DelayedCt

Fields

• dctSource :: Maybe Name

  Signature that gave rise to this constraint Nothing means module top-level

• dctForall :: [TParam]
• dctAsmps :: [Prop]
• dctGoals :: [Goal]

Instances

Generic DelayedCt

Defined in Cryptol.TypeCheck.InferTypes

Associated Types

type Rep DelayedCt :: Type -> Type

Methods

from :: DelayedCt -> Rep DelayedCt x

to :: Rep DelayedCt x -> DelayedCt

Show DelayedCt

Defined in Cryptol.TypeCheck.InferTypes

Methods

showsPrec :: Int -> DelayedCt -> ShowS

show :: DelayedCt -> String

showList :: [DelayedCt] -> ShowS

TVars DelayedCt

Defined in Cryptol.TypeCheck.InferTypes

Methods

apSubst :: Subst -> DelayedCt -> DelayedCt

FVS DelayedCt

Defined in Cryptol.TypeCheck.InferTypes

Methods

fvs :: DelayedCt -> Set TVar

NFData DelayedCt

Defined in Cryptol.TypeCheck.InferTypes

Methods

rnf :: DelayedCt -> ()

PP (WithNames DelayedCt)

Defined in Cryptol.TypeCheck.InferTypes

Methods

ppPrec :: Int -> WithNames DelayedCt -> Doc

type Rep DelayedCt

Defined in Cryptol.TypeCheck.InferTypes

type Rep DelayedCt = D1 ('MetaData "DelayedCt" "Cryptol.TypeCheck.InferTypes" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "DelayedCt" 'PrefixI 'True) ((S1 ('MetaSel ('Just "dctSource") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Name)) :*: S1 ('MetaSel ('Just "dctForall") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam])) :*: (S1 ('MetaSel ('Just "dctAsmps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Prop]) :*: S1 ('MetaSel ('Just "dctGoals") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Goal]))))

data ConstraintSource

Information about how a constraint came to be, used in error reporting.

Constructors

CtComprehension

Computing shape of list comprehension

CtSplitPat

Use of a split pattern

CtTypeSig

A type signature in a pattern or expression

CtInst Expr

Instantiation of this expression

CtSelector

CtExactType

CtEnumeration

CtDefaulting

Just defaulting on the command line

CtPartialTypeFun Name

Use of a partial type function.

CtImprovement

CtPattern TypeSource

Constraints arising from type-checking patterns

CtModuleInstance Range

Instantiating a parametrized module

CtPropGuardsExhaustive Name

Checking that a use of prop guards is exhastive

CtFFI Name

Constraints on a foreign declaration required by the FFI (e.g. sequences must be finite)

Instances

Generic ConstraintSource

Defined in Cryptol.TypeCheck.InferTypes

Associated Types

type Rep ConstraintSource :: Type -> Type

Methods

from :: ConstraintSource -> Rep ConstraintSource x

to :: Rep ConstraintSource x -> ConstraintSource

Show ConstraintSource

Defined in Cryptol.TypeCheck.InferTypes

Methods

showsPrec :: Int -> ConstraintSource -> ShowS

show :: ConstraintSource -> String

showList :: [ConstraintSource] -> ShowS

TVars ConstraintSource

Defined in Cryptol.TypeCheck.InferTypes

Methods

apSubst :: Subst -> ConstraintSource -> ConstraintSource

PP ConstraintSource

Defined in Cryptol.TypeCheck.InferTypes

Methods

ppPrec :: Int -> ConstraintSource -> Doc

NFData ConstraintSource

Defined in Cryptol.TypeCheck.InferTypes

Methods

rnf :: ConstraintSource -> ()

type Rep ConstraintSource

Defined in Cryptol.TypeCheck.InferTypes

type Rep ConstraintSource = D1 ('MetaData "ConstraintSource" "Cryptol.TypeCheck.InferTypes" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (((C1 ('MetaCons "CtComprehension" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CtSplitPat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CtTypeSig" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "CtInst" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Expr)) :+: C1 ('MetaCons "CtSelector" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CtExactType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CtEnumeration" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "CtDefaulting" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CtPartialTypeFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "CtImprovement" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "CtPattern" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeSource)) :+: C1 ('MetaCons "CtModuleInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))) :+: (C1 ('MetaCons "CtPropGuardsExhaustive" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "CtFFI" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name))))))

selSrc :: Selector -> TypeSource

cppKind :: Kind -> Doc

For use in error messages

addTVarsDescsAfter :: FVS t => NameMap -> t -> Doc -> Doc

addTVarsDescsBefore :: FVS t => NameMap -> t -> Doc -> Doc

ppUse :: Expr -> Doc