cryptol-2.7.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
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.7.0-6VD9sMh08R1JPrYSq7DH8b" 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
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
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.7.0-6VD9sMh08R1JPrYSq7DH8b" 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
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
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.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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.7.0-6VD9sMh08R1JPrYSq7DH8b" 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 #

Instances
Show TyFunName Source # 
Instance details

Defined in Cryptol.TypeCheck.InferTypes

Generic TyFunName Source # 
Instance details

Defined in Cryptol.TypeCheck.InferTypes

Associated Types

type Rep TyFunName :: Type -> Type #

NFData TyFunName Source # 
Instance details

Defined in Cryptol.TypeCheck.InferTypes

Methods

rnf :: TyFunName -> () #

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

cppKind :: Kind -> Doc Source #

For use in error messages