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

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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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

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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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

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

Generic DelayedCt Source # 
Instance details

Defined in Cryptol.TypeCheck.InferTypes

Associated Types

type Rep DelayedCt :: Type -> Type #

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

type Rep DelayedCt Source # 
Instance details

Defined in Cryptol.TypeCheck.InferTypes

type Rep DelayedCt = D1 ('MetaData "DelayedCt" "Cryptol.TypeCheck.InferTypes" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" '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 TypeSource

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

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

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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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 TypeSource)) :+: C1 ('MetaCons "CtModuleInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModName))))))

cppKind :: Kind -> Doc Source #

For use in error messages