cryptol-2.9.0: Cryptol: The Language of Cryptography

Safe HaskellSafe
LanguageHaskell2010

Cryptol.TypeCheck.Type

Synopsis

Documentation

class FVS t where Source #

Methods

fvs :: t -> Set TVar Source #

Instances
FVS Type Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Type -> Set TVar Source #

FVS Schema Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Schema -> Set TVar Source #

FVS DelayedCt Source # 
Instance details

Defined in Cryptol.TypeCheck.InferTypes

Methods

fvs :: DelayedCt -> Set TVar Source #

FVS Goal Source # 
Instance details

Defined in Cryptol.TypeCheck.InferTypes

Methods

fvs :: Goal -> Set TVar Source #

FVS Error Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

Methods

fvs :: Error -> Set TVar Source #

FVS Warning Source # 
Instance details

Defined in Cryptol.TypeCheck.Error

Methods

fvs :: Warning -> Set TVar Source #

FVS a => FVS [a] Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: [a] -> Set TVar Source #

FVS a => FVS (Maybe a) Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Maybe a -> Set TVar Source #

(FVS a, FVS b) => FVS (a, b) Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: (a, b) -> Set TVar Source #

type SType = Type Source #

The type is "simple" (i.e., it contains no type functions).

data AbstractType Source #

Information about an abstract type.

Constructors

AbstractType 

data Newtype Source #

Named records

Constructors

Newtype 
Instances
Show Newtype Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Generic Newtype Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Associated Types

type Rep Newtype :: Type -> Type #

Methods

from :: Newtype -> Rep Newtype x #

to :: Rep Newtype x -> Newtype #

NFData Newtype Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: Newtype -> () #

PP Newtype Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> Newtype -> Doc Source #

HasKind Newtype Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: Newtype -> Kind Source #

FreeVars Newtype Source # 
Instance details

Defined in Cryptol.IR.FreeVars

PP (WithNames Newtype) Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

type Rep Newtype Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

data TySyn Source #

Type synonym.

Constructors

TySyn 

Fields

Instances
Show TySyn Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> TySyn -> ShowS #

show :: TySyn -> String #

showList :: [TySyn] -> ShowS #

Generic TySyn Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Associated Types

type Rep TySyn :: Type -> Type #

Methods

from :: TySyn -> Rep TySyn x #

to :: Rep TySyn x -> TySyn #

NFData TySyn Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TySyn -> () #

PP TySyn Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> TySyn -> Doc Source #

HasKind TySyn Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: TySyn -> Kind Source #

PP (WithNames TySyn) Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> WithNames TySyn -> Doc Source #

type Rep TySyn Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

type Prop = Type Source #

The type is supposed to be of kind KProp.

data TVarSource Source #

Instances
Show TVarSource Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Generic TVarSource Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Associated Types

type Rep TVarSource :: Type -> Type #

NFData TVarSource Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TVarSource -> () #

PP TVarSource Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> TVarSource -> Doc Source #

type Rep TVarSource Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TVarSource = D1 (MetaData "TVarSource" "Cryptol.TypeCheck.Type" "cryptol-2.9.0-4aSi1YZNBynFQwh9aOpllR" False) (((C1 (MetaCons "TVFromModParam" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: (C1 (MetaCons "TVFromSignature" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: C1 (MetaCons "TypeWildCard" PrefixI False) (U1 :: Type -> Type))) :+: ((C1 (MetaCons "TypeOfRecordField" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Ident)) :+: C1 (MetaCons "TypeOfTupleField" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int))) :+: (C1 (MetaCons "TypeOfSeqElement" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "LenOfSeq" PrefixI False) (U1 :: Type -> Type)))) :+: ((C1 (MetaCons "TypeParamInstNamed" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Ident)) :+: (C1 (MetaCons "TypeParamInstPos" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) :+: C1 (MetaCons "DefinitionOf" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)))) :+: ((C1 (MetaCons "LenOfCompGen" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "TypeOfArg" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Int)))) :+: (C1 (MetaCons "TypeOfRes" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "TypeErrorPlaceHolder" PrefixI False) (U1 :: Type -> Type)))))

data TVarInfo Source #

Constructors

TVarInfo 

Fields

Instances
Show TVarInfo Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Generic TVarInfo Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Associated Types

type Rep TVarInfo :: Type -> Type #

Methods

from :: TVarInfo -> Rep TVarInfo x #

to :: Rep TVarInfo x -> TVarInfo #

NFData TVarInfo Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TVarInfo -> () #

PP TVarInfo Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> TVarInfo -> Doc Source #

type Rep TVarInfo Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TVarInfo = D1 (MetaData "TVarInfo" "Cryptol.TypeCheck.Type" "cryptol-2.9.0-4aSi1YZNBynFQwh9aOpllR" False) (C1 (MetaCons "TVarInfo" PrefixI True) (S1 (MetaSel (Just "tvarSource") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Range) :*: S1 (MetaSel (Just "tvarDesc") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TVarSource)))

data TVar Source #

Type variables.

Constructors

TVFree !Int Kind (Set TParam) TVarInfo

Unique, kind, ids of bound type variables that are in scope The last field gives us some infor for nicer warnings/errors.

TVBound !TParam 
Instances
Eq TVar Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

(==) :: TVar -> TVar -> Bool #

(/=) :: TVar -> TVar -> Bool #

Ord TVar Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

compare :: TVar -> TVar -> Ordering #

(<) :: TVar -> TVar -> Bool #

(<=) :: TVar -> TVar -> Bool #

(>) :: TVar -> TVar -> Bool #

(>=) :: TVar -> TVar -> Bool #

max :: TVar -> TVar -> TVar #

min :: TVar -> TVar -> TVar #

Show TVar Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> TVar -> ShowS #

show :: TVar -> String #

showList :: [TVar] -> ShowS #

Generic TVar Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Associated Types

type Rep TVar :: Type -> Type #

Methods

from :: TVar -> Rep TVar x #

to :: Rep TVar x -> TVar #

NFData TVar Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TVar -> () #

PP TVar Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> TVar -> Doc Source #

HasKind TVar Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: TVar -> Kind Source #

FreeVars TVar Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: TVar -> Deps Source #

PP (WithNames TVar) Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> WithNames TVar -> Doc Source #

type Rep TVar Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

data Type Source #

The internal representation of types. These are assumed to be kind correct.

Constructors

TCon !TCon ![Type]

Type constant with args

TVar TVar

Type variable (free or bound)

TUser !Name ![Type] !Type

This is just a type annotation, for a type that was written as a type synonym. It is useful so that we can use it to report nicer errors. Example: TUser T ts t is really just the type t that was written as T ts by the user.

TRec !(RecordMap Ident Type)

Record type

Instances
Eq Type Source #

Syntactic equality, ignoring type synonyms and record order.

Instance details

Defined in Cryptol.TypeCheck.Type

Methods

(==) :: Type -> Type -> Bool #

(/=) :: Type -> Type -> Bool #

Ord Type Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

compare :: Type -> Type -> Ordering #

(<) :: Type -> Type -> Bool #

(<=) :: Type -> Type -> Bool #

(>) :: Type -> Type -> Bool #

(>=) :: Type -> Type -> Bool #

max :: Type -> Type -> Type #

min :: Type -> Type -> Type #

Show Type Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> Type -> ShowS #

show :: Type -> String #

showList :: [Type] -> ShowS #

Generic Type Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Associated Types

type Rep Type :: Type -> Type #

Methods

from :: Type -> Rep Type x #

to :: Rep Type x -> Type #

NFData Type Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: Type -> () #

PP Type Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> Type -> Doc Source #

HasKind Type Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: Type -> Kind Source #

FVS Type Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Type -> Set TVar Source #

TVars Type Source # 
Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Type -> Type Source #

ShowParseable Type Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

FreeVars Type Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Type -> Deps Source #

TrieMap TypeMap Type Source # 
Instance details

Defined in Cryptol.TypeCheck.TypeMap

Methods

emptyTM :: TypeMap a Source #

nullTM :: TypeMap a -> Bool Source #

lookupTM :: Type -> TypeMap a -> Maybe a Source #

alterTM :: Type -> (Maybe a -> Maybe a) -> TypeMap a -> TypeMap a Source #

unionTM :: (a -> a -> a) -> TypeMap a -> TypeMap a -> TypeMap a Source #

toListTM :: TypeMap a -> [(Type, a)] Source #

mapMaybeWithKeyTM :: (Type -> a -> Maybe b) -> TypeMap a -> TypeMap b Source #

PP (WithNames Type) Source #

The precedence levels used by this pretty-printing instance correspond with parser non-terminals as follows:

  • 0-1: type
  • 2: infix_type
  • 3: app_type
  • 4: atype
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> WithNames Type -> Doc Source #

type Rep Type Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

data TPFlavor Source #

Constructors

TPModParam Name 
TPOther (Maybe Name) 
Instances
Show TPFlavor Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Generic TPFlavor Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Associated Types

type Rep TPFlavor :: Type -> Type #

Methods

from :: TPFlavor -> Rep TPFlavor x #

to :: Rep TPFlavor x -> TPFlavor #

NFData TPFlavor Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TPFlavor -> () #

type Rep TPFlavor Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TPFlavor = D1 (MetaData "TPFlavor" "Cryptol.TypeCheck.Type" "cryptol-2.9.0-4aSi1YZNBynFQwh9aOpllR" False) (C1 (MetaCons "TPModParam" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: C1 (MetaCons "TPOther" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Name))))

data TParam Source #

Type parameters.

Constructors

TParam 

Fields

Instances
Eq TParam Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

(==) :: TParam -> TParam -> Bool #

(/=) :: TParam -> TParam -> Bool #

Ord TParam Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Show TParam Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Generic TParam Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Associated Types

type Rep TParam :: Type -> Type #

Methods

from :: TParam -> Rep TParam x #

to :: Rep TParam x -> TParam #

NFData TParam Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TParam -> () #

PP TParam Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> TParam -> Doc Source #

HasKind TParam Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: TParam -> Kind Source #

ShowParseable TParam Source # 
Instance details

Defined in Cryptol.TypeCheck.Parseable

PP (WithNames TParam) Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TParam Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

data Schema Source #

The types of polymorphic values.

Constructors

Forall 

Fields

Instances
Eq Schema Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

(==) :: Schema -> Schema -> Bool #

(/=) :: Schema -> Schema -> Bool #

Show Schema Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Generic Schema Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Associated Types

type Rep Schema :: Type -> Type #

Methods

from :: Schema -> Rep Schema x #

to :: Rep Schema x -> Schema #

NFData Schema Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: Schema -> () #

PP Schema Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> Schema -> Doc Source #

FVS Schema Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Schema -> Set TVar Source #

TVars Schema Source #

This instance does not need to worry about bound variable capture, because we rely on the Subst datatype invariant to ensure that variable scopes will be properly preserved.

Instance details

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Schema -> Schema Source #

FreeVars Schema Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Schema -> Deps Source #

PP (WithNames Schema) Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

type Rep Schema Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

type Rep Schema = D1 (MetaData "Schema" "Cryptol.TypeCheck.Type" "cryptol-2.9.0-4aSi1YZNBynFQwh9aOpllR" False) (C1 (MetaCons "Forall" PrefixI True) (S1 (MetaSel (Just "sVars") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TParam]) :*: (S1 (MetaSel (Just "sProps") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Prop]) :*: S1 (MetaSel (Just "sType") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type))))

tvSourceName :: TVarSource -> Maybe Name Source #

Get the names of something that is related to the tvar.

quickApply :: Kind -> [a] -> Kind Source #

superclassSet :: Prop -> Set Prop Source #

Compute the set of all Props that are implied by the given prop via superclass constraints.

tSplitFun :: TFun -> Type -> [Type] Source #

Split up repeated occurances of the given binary type-level function.

tNum :: Integral a => a -> Type Source #

tFun :: Type -> Type -> Type infixr 5 Source #

Make a function type.

tNoUser :: Type -> Type Source #

Eliminate outermost type synonyms.

tError :: Type -> String -> Type Source #

Make an error value of the given type to replace the given malformed type (the argument to the error function)

tf2 :: TFun -> Type -> Type -> Type Source #

tf3 :: TFun -> Type -> Type -> Type -> Type Source #

(=#=) :: Type -> Type -> Prop infix 4 Source #

Equality for numeric types.

(>==) :: Type -> Type -> Prop infix 4 Source #

Make a greater-than-or-equal-to constraint.

pHas :: Selector -> Type -> Type -> Prop Source #

A Has constraint, used for tuple and record selection.