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
- 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 {}
- data HasGoalSln = HasGoalSln {}
- data DelayedCt = DelayedCt {}
- data ConstraintSource
- 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
|
Instances
Show SolverConfig Source # | |
Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> SolverConfig -> ShowS show :: SolverConfig -> String showList :: [SolverConfig] -> ShowS | |
Generic SolverConfig Source # | |
Defined in Cryptol.TypeCheck.InferTypes Associated Types type Rep SolverConfig :: Type -> Type | |
NFData SolverConfig Source # | |
Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: SolverConfig -> () | |
type Rep SolverConfig Source # | |
Defined in Cryptol.TypeCheck.InferTypes type Rep SolverConfig = D1 ('MetaData "SolverConfig" "Cryptol.TypeCheck.InferTypes" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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])))) |
The types of variables in the environment.
Constructors
Goals | |
Fields
|
emptyGoals :: Goals Source #
goalsFromList :: [Goal] -> Goals Source #
Something that we need to find evidence for.
Constructors
Goal | |
Fields
|
Instances
Eq Goal Source # | |
Ord Goal Source # | |
Show Goal Source # | |
Generic Goal Source # | |
NFData Goal Source # | |
Defined in Cryptol.TypeCheck.InferTypes | |
FVS Goal Source # | |
TVars Goal Source # | |
PP (WithNames Goal) Source # | |
type Rep Goal Source # | |
Defined in Cryptol.TypeCheck.InferTypes type Rep Goal = D1 ('MetaData "Goal" "Cryptol.TypeCheck.InferTypes" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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)))) |
Delayed implication constraints, arising from user-specified type sigs.
Constructors
DelayedCt | |
Instances
Show DelayedCt Source # | |
Generic DelayedCt Source # | |
NFData DelayedCt Source # | |
Defined in Cryptol.TypeCheck.InferTypes | |
FVS DelayedCt Source # | |
TVars DelayedCt Source # | |
PP (WithNames DelayedCt) Source # | |
type Rep DelayedCt Source # | |
Defined in Cryptol.TypeCheck.InferTypes type Rep DelayedCt = D1 ('MetaData "DelayedCt" "Cryptol.TypeCheck.InferTypes" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 Doc | Constraints arising from type-checking patterns |
CtModuleInstance ModName | Instantiating a parametrized module |
Instances
Show ConstraintSource Source # | |
Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> ConstraintSource -> ShowS show :: ConstraintSource -> String showList :: [ConstraintSource] -> ShowS | |
Generic ConstraintSource Source # | |
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 # | |
Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: ConstraintSource -> () | |
PP ConstraintSource Source # | |
Defined in Cryptol.TypeCheck.InferTypes Methods ppPrec :: Int -> ConstraintSource -> Doc Source # | |
TVars ConstraintSource Source # | |
Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> ConstraintSource -> ConstraintSource Source # | |
type Rep ConstraintSource Source # | |
Defined in Cryptol.TypeCheck.InferTypes type Rep ConstraintSource = D1 ('MetaData "ConstraintSource" "Cryptol.TypeCheck.InferTypes" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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 Doc)) :+: C1 ('MetaCons "CtModuleInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModName)))))) |