Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	Safe
Language	Haskell2010

Cryptol.TypeCheck.InferTypes

Description

This module contains types used during type inference.

Synopsis

data SolverConfig = SolverConfig {
- solverPath :: FilePath
- solverArgs :: [String]
- solverVerbose :: Int
- solverPreludePath :: [FilePath]
}
defaultSolverConfig :: [FilePath] -> SolverConfig
data VarType
- = ExtVar Schema
- | CurSCC Expr Type
data Goals = Goals {
- goalSet :: Set Goal
- saturatedPropSet :: Set Prop
- literalGoals :: Map TVar LitGoal
- literalLessThanGoals :: Map TVar LitGoal
}
type LitGoal = Goal
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 = Goal {
- goalSource :: ConstraintSource
- goalRange :: Range
- goal :: Prop
}
data HasGoal = HasGoal {
- hasName :: !Int
- hasGoal :: Goal
}
data HasGoalSln = HasGoalSln {
- hasDoSelect :: Expr -> Expr
- hasDoSet :: Expr -> Expr -> Expr
}
data DelayedCt = DelayedCt {
- dctSource :: Maybe Name
- dctForall :: [TParam]
- dctAsmps :: [Prop]
- dctGoals :: [Goal]
}
data ConstraintSource
- = CtComprehension
- | CtSplitPat
- | CtTypeSig
- | CtInst Expr
- | CtSelector
- | CtExactType
- | CtEnumeration
- | CtDefaulting
- | CtPartialTypeFun Name
- | CtImprovement
- | CtPattern TypeSource
- | CtModuleInstance Range
- | CtPropGuardsExhaustive Name
- | CtFFI Name
selSrc :: Selector -> TypeSource
cppKind :: Kind -> Doc
addTVarsDescsAfter :: FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsBefore :: FVS t => NameMap -> t -> Doc -> Doc
ppUse :: Expr -> Doc

Documentation

data SolverConfig Source #

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

Instances details

Generic SolverConfig Source #
Instance details 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 Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> SolverConfig -> ShowS # show :: SolverConfig -> String # showList :: [SolverConfig] -> ShowS #
NFData SolverConfig Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: SolverConfig -> () #
type Rep SolverConfig Source #
Instance details 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 Source #

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

data VarType Source #

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 Source #

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

Instances details

Show Goals Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> Goals -> ShowS # show :: Goals -> String # showList :: [Goals] -> ShowS #
TVars Goals Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> Goals -> Goals Source #

type LitGoal = Goal Source #

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 Source #

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

litLessThanGoalToGoal :: (TVar, LitGoal) -> Goal Source #

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

emptyGoals :: Goals Source #

nullGoals :: Goals -> Bool Source #

fromGoals :: Goals -> [Goal] Source #

goalsFromList :: [Goal] -> Goals Source #

insertGoal :: Goal -> Goals -> Goals Source #

data Goal Source #

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

Instances details

Generic Goal Source #
Instance details 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 Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> Goal -> ShowS # show :: Goal -> String # showList :: [Goal] -> ShowS #
TVars Goal Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> Goal -> Goal Source #
FVS Goal Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods fvs :: Goal -> Set TVar Source #
NFData Goal Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: Goal -> () #
Eq Goal Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods (==) :: Goal -> Goal -> Bool # (/=) :: Goal -> Goal -> Bool #
Ord Goal Source #
Instance details 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) Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods ppPrec :: Int -> WithNames Goal -> Doc Source #
type Rep Goal Source #
Instance details 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 Source #

Constructors

HasGoal
Fields hasName :: !Int This is the "name" of the constraint, used to find the solution for ellaboration. hasGoal :: Goal

Instances

Instances details

Show HasGoal Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> HasGoal -> ShowS # show :: HasGoal -> String # showList :: [HasGoal] -> ShowS #
TVars HasGoal Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> HasGoal -> HasGoal Source #

data HasGoalSln Source #

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 Source #

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

Instances details

Generic DelayedCt Source #
Instance details 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 Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> DelayedCt -> ShowS # show :: DelayedCt -> String # showList :: [DelayedCt] -> ShowS #
TVars DelayedCt Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> DelayedCt -> DelayedCt Source #
FVS DelayedCt Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods fvs :: DelayedCt -> Set TVar Source #
NFData DelayedCt Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: DelayedCt -> () #
PP (WithNames DelayedCt) Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods ppPrec :: Int -> WithNames DelayedCt -> Doc Source #
type Rep DelayedCt Source #
Instance details 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 Source #

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

Instances details

Generic ConstraintSource Source #
Instance details 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 Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> ConstraintSource -> ShowS # show :: ConstraintSource -> String # showList :: [ConstraintSource] -> ShowS #
TVars ConstraintSource Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> ConstraintSource -> ConstraintSource Source #
PP ConstraintSource Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods ppPrec :: Int -> ConstraintSource -> Doc Source #
NFData ConstraintSource Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: ConstraintSource -> () #
type Rep ConstraintSource Source #
Instance details 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 Source #

cppKind :: Kind -> Doc Source #

For use in error messages

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

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

ppUse :: Expr -> Doc Source #