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]
}
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 ModName
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

Show SolverConfig Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> SolverConfig -> ShowS # show :: SolverConfig -> String # showList :: [SolverConfig] -> ShowS #
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 #
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-2.11.0-KBQWpCBm4GD4lGHyVVV39L" '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]))))

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

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 #
Show Goal Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> Goal -> ShowS # show :: Goal -> String # showList :: [Goal] -> ShowS #
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 #
NFData Goal Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: Goal -> () #
FVS Goal Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods fvs :: Goal -> Set TVar Source #
TVars Goal Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> Goal -> Goal Source #
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-2.11.0-KBQWpCBm4GD4lGHyVVV39L" '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 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

Show DelayedCt Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> DelayedCt -> ShowS # show :: DelayedCt -> String # showList :: [DelayedCt] -> ShowS #
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 #
NFData DelayedCt Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: DelayedCt -> () #
FVS DelayedCt Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods fvs :: DelayedCt -> Set TVar Source #
TVars DelayedCt Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> DelayedCt -> DelayedCt Source #
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-2.11.0-KBQWpCBm4GD4lGHyVVV39L" '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 ModName	Instantiating a parametrized module

Instances

Instances details

Show ConstraintSource Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> ConstraintSource -> ShowS # show :: ConstraintSource -> String # showList :: [ConstraintSource] -> ShowS #
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 #
NFData ConstraintSource Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: ConstraintSource -> () #
PP ConstraintSource Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods ppPrec :: Int -> ConstraintSource -> Doc Source #
TVars ConstraintSource Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> ConstraintSource -> ConstraintSource Source #
type Rep ConstraintSource Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes type Rep ConstraintSource = D1 ('MetaData "ConstraintSource" "Cryptol.TypeCheck.InferTypes" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" '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 ModName))))))

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 #