cryptol-2.6.0: Cryptol: The Language of Cryptography

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 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
- addTVarsDescs :: 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 Source # show :: SolverConfig -> String Source # showList :: [SolverConfig] -> ShowS Source #
Generic SolverConfig Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Associated Types type Rep SolverConfig :: Type -> Type Source # Methods from :: SolverConfig -> Rep SolverConfig x Source # to :: Rep SolverConfig x -> SolverConfig Source #
NFData SolverConfig Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: SolverConfig -> () Source #
type Rep SolverConfig Source # |

Instance details

Defined in Cryptol.TypeCheck.InferTypes

type Rep SolverConfig = D1 (MetaData "SolverConfig" "Cryptol.TypeCheck.InferTypes" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" 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 Source # show :: Goals -> String Source # showList :: [Goals] -> ShowS Source #
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 Source # (/=) :: Goal -> Goal -> Bool Source #
Ord Goal Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods compare :: Goal -> Goal -> Ordering Source # (<) :: Goal -> Goal -> Bool Source # (<=) :: Goal -> Goal -> Bool Source # (>) :: Goal -> Goal -> Bool Source # (>=) :: Goal -> Goal -> Bool Source # max :: Goal -> Goal -> Goal Source # min :: Goal -> Goal -> Goal Source #
Show Goal Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> Goal -> ShowS Source # show :: Goal -> String Source # showList :: [Goal] -> ShowS Source #
Generic Goal Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Associated Types type Rep Goal :: Type -> Type Source # Methods from :: Goal -> Rep Goal x Source # to :: Rep Goal x -> Goal Source #
NFData Goal Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: Goal -> () Source #
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.6.0-FO78l5UWBYr51eDL1ksQpO" 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 Source # show :: HasGoal -> String Source # showList :: [HasGoal] -> ShowS Source #
TVars HasGoal Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods apSubst :: Subst -> HasGoal -> HasGoal Source #

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 Source # show :: DelayedCt -> String Source # showList :: [DelayedCt] -> ShowS Source #
Generic DelayedCt Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Associated Types type Rep DelayedCt :: Type -> Type Source # Methods from :: DelayedCt -> Rep DelayedCt x Source # to :: Rep DelayedCt x -> DelayedCt Source #
NFData DelayedCt Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: DelayedCt -> () Source #
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.6.0-FO78l5UWBYr51eDL1ksQpO" 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 Source # show :: ConstraintSource -> String Source # showList :: [ConstraintSource] -> ShowS Source #
Generic ConstraintSource Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Associated Types type Rep ConstraintSource :: Type -> Type Source # Methods from :: ConstraintSource -> Rep ConstraintSource x Source # to :: Rep ConstraintSource x -> ConstraintSource Source #
NFData ConstraintSource Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: ConstraintSource -> () Source #
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.6.0-FO78l5UWBYr51eDL1ksQpO" 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 Source # show :: TyFunName -> String Source # showList :: [TyFunName] -> ShowS Source #
Generic TyFunName Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Associated Types type Rep TyFunName :: Type -> Type Source # Methods from :: TyFunName -> Rep TyFunName x Source # to :: Rep TyFunName x -> TyFunName Source #
NFData TyFunName Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: TyFunName -> () Source #
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.6.0-FO78l5UWBYr51eDL1ksQpO" 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

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

ppUse :: Expr -> Doc Source #