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
- literalGoals :: Map TVar LitGoal
}
type LitGoal = Goal
litGoalToGoal :: (TVar, LitGoal) -> Goal
goalToLitGoal :: 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 TyFunName
- | CtImprovement
- | CtPattern Doc
- | CtModuleInstance ModName
data TyFunName
- = UserTyFun Name
- | BuiltInTyFun TFun
- | BuiltInTC TC
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

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.7.0-6VD9sMh08R1JPrYSq7DH8b" 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`. literalGoals :: Map TVar LitGoal An entry `(a,t)` corresponds to `Literal t a`.

Instances

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 #

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

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.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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

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.7.0-6VD9sMh08R1JPrYSq7DH8b" 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 TyFunName	Use of a partial type function.
CtImprovement
CtPattern Doc	Constraints arising from type-checking patterns
CtModuleInstance ModName	Instantiating a parametrized module

Instances

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.7.0-6VD9sMh08R1JPrYSq7DH8b" 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 TyFunName)))) :+: (C1 (MetaCons "CtImprovement" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "CtPattern" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Doc)) :+: C1 (MetaCons "CtModuleInstance" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ModName))))))

data TyFunName Source #

Constructors

UserTyFun Name
BuiltInTyFun TFun
BuiltInTC TC

Instances

Show TyFunName Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> TyFunName -> ShowS # show :: TyFunName -> String # showList :: [TyFunName] -> ShowS #
Generic TyFunName Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Associated Types type Rep TyFunName :: Type -> Type # Methods from :: TyFunName -> Rep TyFunName x # to :: Rep TyFunName x -> TyFunName #
NFData TyFunName Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: TyFunName -> () #
PP TyFunName Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods ppPrec :: Int -> TyFunName -> Doc Source #
type Rep TyFunName Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes type Rep TyFunName = D1 (MetaData "TyFunName" "Cryptol.TypeCheck.InferTypes" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (C1 (MetaCons "UserTyFun" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: (C1 (MetaCons "BuiltInTyFun" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TFun)) :+: C1 (MetaCons "BuiltInTC" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TC))))

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 #