cryptol-2.8.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Cryptol.TypeCheck.InferTypes

Description

This module contains types used during type inference.

Synopsis

Documentation

data SolverConfig Source #

Constructors

SolverConfig 

Fields

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

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.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]))))

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

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

nullGoals :: Goals -> Bool Source #

data Goal Source #

Something that we need to find evidence for.

Constructors

Goal 

Fields

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.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))))

data HasGoal Source #

Constructors

HasGoal 

Fields

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

data HasGoalSln Source #

A solution for a HasGoal

Constructors

HasGoalSln 

Fields

data DelayedCt Source #

Delayed implication constraints, arising from user-specified type sigs.

Constructors

DelayedCt 

Fields

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

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.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

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

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

type Rep ConstraintSource Source # 
Instance details

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))))))

cppKind :: Kind -> Doc Source #

For use in error messages