Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell2010 |
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 {}
- 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 #
SolverConfig | |
|
Instances
The types of variables in the environment.
Goals | |
|
emptyGoals :: Goals Source #
goalsFromList :: [Goal] -> Goals Source #
Something that we need to find evidence for.
Goal | |
|
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-Jl4xQKR0B4Q8VTNDfmeSo7" 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.
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-Jl4xQKR0B4Q8VTNDfmeSo7" 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.
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 |