Cryptol.TypeCheck.Type

Documentation

class FVS t where

Methods

fvs :: t -> Set TVar

Instances

FVS Type

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Type -> Set TVar

FVS Schema

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Schema -> Set TVar

FVS DelayedCt

Defined in Cryptol.TypeCheck.InferTypes

Methods

fvs :: DelayedCt -> Set TVar

FVS Goal

Defined in Cryptol.TypeCheck.InferTypes

Methods

fvs :: Goal -> Set TVar

FVS Error

Defined in Cryptol.TypeCheck.Error

Methods

fvs :: Error -> Set TVar

FVS Warning

Defined in Cryptol.TypeCheck.Error

Methods

fvs :: Warning -> Set TVar

FVS a => FVS [a]

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: [a] -> Set TVar

FVS a => FVS (Maybe a)

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Maybe a -> Set TVar

(FVS a, FVS b) => FVS (a, b)

Defined in Cryptol.TypeCheck.Type

Methods

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

type SType = Type

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

data AbstractType

Information about an abstract type.

Constructors

AbstractType

Fields

• atName :: Name
• atKind :: Kind
• atCtrs :: ([TParam], [Prop])
• atFixitiy :: Maybe Fixity
• atDoc :: Maybe Text

Instances

Show AbstractType

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> AbstractType -> ShowS

show :: AbstractType -> String

showList :: [AbstractType] -> ShowS

Generic AbstractType

Defined in Cryptol.TypeCheck.Type

Associated Types

type Rep AbstractType :: Type -> Type

Methods

from :: AbstractType -> Rep AbstractType x

to :: Rep AbstractType x -> AbstractType

NFData AbstractType

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: AbstractType -> ()

type Rep AbstractType

Defined in Cryptol.TypeCheck.Type

type Rep AbstractType = D1 ('MetaData "AbstractType" "Cryptol.TypeCheck.Type" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (C1 ('MetaCons "AbstractType" 'PrefixI 'True) ((S1 ('MetaSel ('Just "atName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "atKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :*: (S1 ('MetaSel ('Just "atCtrs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ([TParam], [Prop])) :*: (S1 ('MetaSel ('Just "atFixitiy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity)) :*: S1 ('MetaSel ('Just "atDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text))))))

data Newtype

Named records

Constructors

Newtype

Fields

• ntName :: Name
• ntParams :: [TParam]
• ntConstraints :: [Prop]
• ntFields :: [(Ident, Type)]
• ntDoc :: Maybe Text

Instances

Show Newtype

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> Newtype -> ShowS

show :: Newtype -> String

showList :: [Newtype] -> ShowS

Generic Newtype

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: Newtype -> ()

PP Newtype

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> Newtype -> Doc

HasKind Newtype

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: Newtype -> Kind

FreeVars Newtype

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Newtype -> Deps

PP (WithNames Newtype)

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> WithNames Newtype -> Doc

type Rep Newtype

Defined in Cryptol.TypeCheck.Type

type Rep Newtype = D1 ('MetaData "Newtype" "Cryptol.TypeCheck.Type" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (C1 ('MetaCons "Newtype" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ntName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "ntParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam])) :*: (S1 ('MetaSel ('Just "ntConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Prop]) :*: (S1 ('MetaSel ('Just "ntFields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Ident, Type)]) :*: S1 ('MetaSel ('Just "ntDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text))))))

data TySyn

Type synonym.

Constructors

TySyn

Fields

• tsName :: Name

  Name

• tsParams :: [TParam]

  Parameters

• tsConstraints :: [Prop]

  Ensure body is OK

• tsDef :: Type

  Definition

• tsDoc :: !(Maybe Text)

  Documentation

Instances

Show TySyn

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> TySyn -> ShowS

show :: TySyn -> String

showList :: [TySyn] -> ShowS

Generic TySyn

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TySyn -> ()

PP TySyn

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> TySyn -> Doc

HasKind TySyn

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: TySyn -> Kind

PP (WithNames TySyn)

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> WithNames TySyn -> Doc

type Rep TySyn

Defined in Cryptol.TypeCheck.Type

type Rep TySyn = D1 ('MetaData "TySyn" "Cryptol.TypeCheck.Type" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (C1 ('MetaCons "TySyn" 'PrefixI 'True) ((S1 ('MetaSel ('Just "tsName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "tsParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam])) :*: (S1 ('MetaSel ('Just "tsConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Prop]) :*: (S1 ('MetaSel ('Just "tsDef") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Just "tsDoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Text))))))

type Prop = Type

The type is supposed to be of kind KProp.

data TypeWithSource

A type annotated with information on how it came about.

Constructors

WithSource

Fields

• twsType :: Type
• twsSource :: TypeSource

data ArgDescr

Constructors

ArgDescr

Fields

• argDescrFun :: Maybe Name
• argDescrNumber :: Maybe Int

Instances

Show ArgDescr

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> ArgDescr -> ShowS

show :: ArgDescr -> String

showList :: [ArgDescr] -> ShowS

Generic ArgDescr

Defined in Cryptol.TypeCheck.Type

Associated Types

type Rep ArgDescr :: Type -> Type

Methods

from :: ArgDescr -> Rep ArgDescr x

to :: Rep ArgDescr x -> ArgDescr

NFData ArgDescr

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: ArgDescr -> ()

PP ArgDescr

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> ArgDescr -> Doc

type Rep ArgDescr

Defined in Cryptol.TypeCheck.Type

type Rep ArgDescr = D1 ('MetaData "ArgDescr" "Cryptol.TypeCheck.Type" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (C1 ('MetaCons "ArgDescr" 'PrefixI 'True) (S1 ('MetaSel ('Just "argDescrFun") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Name)) :*: S1 ('MetaSel ('Just "argDescrNumber") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int))))

data TypeSource

Explains how this type came to be, for better error messages.

Constructors

TVFromModParam Name

Name of module parameter

TVFromSignature Name

A variable in a signature

TypeWildCard

TypeOfRecordField Ident

TypeOfTupleField Int

TypeOfSeqElement

LenOfSeq

TypeParamInstNamed Name Ident

TypeParamInstPos Name Int

DefinitionOf Name

LenOfCompGen

TypeOfArg ArgDescr

TypeOfRes

FunApp

TypeOfIfCondExpr

TypeFromUserAnnotation

GeneratorOfListComp

TypeErrorPlaceHolder

Instances

Show TypeSource

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> TypeSource -> ShowS

show :: TypeSource -> String

showList :: [TypeSource] -> ShowS

Generic TypeSource

Defined in Cryptol.TypeCheck.Type

Associated Types

type Rep TypeSource :: Type -> Type

Methods

from :: TypeSource -> Rep TypeSource x

to :: Rep TypeSource x -> TypeSource

NFData TypeSource

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TypeSource -> ()

PP TypeSource

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> TypeSource -> Doc

type Rep TypeSource

Defined in Cryptol.TypeCheck.Type

type Rep TypeSource = D1 ('MetaData "TypeSource" "Cryptol.TypeCheck.Type" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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 ArgDescr)) :+: C1 ('MetaCons "TypeOfRes" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "FunApp" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TypeOfIfCondExpr" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TypeFromUserAnnotation" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "GeneratorOfListComp" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TypeErrorPlaceHolder" 'PrefixI 'False) (U1 :: Type -> Type))))))

data TVarInfo

Constructors

TVarInfo

Fields

• tvarSource :: !Range

  Source code that gave rise

• tvarDesc :: !TypeSource

  Description

Instances

Show TVarInfo

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> TVarInfo -> ShowS

show :: TVarInfo -> String

showList :: [TVarInfo] -> ShowS

Generic TVarInfo

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TVarInfo -> ()

PP TVarInfo

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> TVarInfo -> Doc

type Rep TVarInfo

Defined in Cryptol.TypeCheck.Type

type Rep TVarInfo = D1 ('MetaData "TVarInfo" "Cryptol.TypeCheck.Type" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (C1 ('MetaCons "TVarInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "tvarSource") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Range) :*: S1 ('MetaSel ('Just "tvarDesc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TypeSource)))

data TVar

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 info for nicer warnings/errors.

TVBound !TParam

Instances

Eq TVar

Defined in Cryptol.TypeCheck.Type

Methods

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

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

Ord TVar

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

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> TVar -> ShowS

show :: TVar -> String

showList :: [TVar] -> ShowS

Generic TVar

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TVar -> ()

PP TVar

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> TVar -> Doc

HasKind TVar

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: TVar -> Kind

FreeVars TVar

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: TVar -> Deps

PP (WithNames TVar)

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> WithNames TVar -> Doc

type Rep TVar

Defined in Cryptol.TypeCheck.Type

type Rep TVar = D1 ('MetaData "TVar" "Cryptol.TypeCheck.Type" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (C1 ('MetaCons "TVFree" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set TParam)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TVarInfo))) :+: C1 ('MetaCons "TVBound" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 TParam)))

data Type

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

Syntactic equality, ignoring type synonyms and record order.

Defined in Cryptol.TypeCheck.Type

Methods

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

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

Ord Type

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

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> Type -> ShowS

show :: Type -> String

showList :: [Type] -> ShowS

Generic Type

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: Type -> ()

PP Type

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> Type -> Doc

HasKind Type

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: Type -> Kind

FVS Type

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Type -> Set TVar

TVars Type

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Type -> Type

ShowParseable Type

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Type -> Doc

FreeVars Type

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Type -> Deps

TrieMap TypeMap Type

Defined in Cryptol.TypeCheck.TypeMap

Methods

emptyTM :: TypeMap a

nullTM :: TypeMap a -> Bool

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

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

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

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

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

PP (WithNames Type)

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: dimensions atype
• 5: atype

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> WithNames Type -> Doc

type Rep Type

Defined in Cryptol.TypeCheck.Type

type Rep Type = D1 ('MetaData "Type" "Cryptol.TypeCheck.Type" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) ((C1 ('MetaCons "TCon" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TCon) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Type])) :+: C1 ('MetaCons "TVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TVar))) :+: (C1 ('MetaCons "TUser" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Type]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Type))) :+: C1 ('MetaCons "TRec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (RecordMap Ident Type)))))

data TPFlavor

Constructors

TPModParam Name

TPOther (Maybe Name)

Instances

Show TPFlavor

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> TPFlavor -> ShowS

show :: TPFlavor -> String

showList :: [TPFlavor] -> ShowS

Generic TPFlavor

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TPFlavor -> ()

type Rep TPFlavor

Defined in Cryptol.TypeCheck.Type

type Rep TPFlavor = D1 ('MetaData "TPFlavor" "Cryptol.TypeCheck.Type" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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

Type parameters.

Constructors

TParam

Fields

• tpUnique :: !Int

  Parameter identifier

• tpKind :: Kind

  Kind of parameter

• tpFlav :: TPFlavor

  What sort of type parameter is this

• tpInfo :: !TVarInfo

  A description for better messages.

Instances

Eq TParam

Defined in Cryptol.TypeCheck.Type

Methods

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

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

Ord TParam

Defined in Cryptol.TypeCheck.Type

Methods

compare :: TParam -> TParam -> Ordering

(<) :: TParam -> TParam -> Bool

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

(>) :: TParam -> TParam -> Bool

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

max :: TParam -> TParam -> TParam

min :: TParam -> TParam -> TParam

Show TParam

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> TParam -> ShowS

show :: TParam -> String

showList :: [TParam] -> ShowS

Generic TParam

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: TParam -> ()

PP TParam

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> TParam -> Doc

HasKind TParam

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: TParam -> Kind

ShowParseable TParam

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: TParam -> Doc

PP (WithNames TParam)

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> WithNames TParam -> Doc

type Rep TParam

Defined in Cryptol.TypeCheck.Type

type Rep TParam = D1 ('MetaData "TParam" "Cryptol.TypeCheck.Type" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (C1 ('MetaCons "TParam" 'PrefixI 'True) ((S1 ('MetaSel ('Just "tpUnique") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "tpKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :*: (S1 ('MetaSel ('Just "tpFlav") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TPFlavor) :*: S1 ('MetaSel ('Just "tpInfo") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TVarInfo))))

data Schema

The types of polymorphic values.

Constructors

Forall

Fields

• sVars :: [TParam]
• sProps :: [Prop]
• sType :: Type

Instances

Eq Schema

Defined in Cryptol.TypeCheck.Type

Methods

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

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

Show Schema

Defined in Cryptol.TypeCheck.Type

Methods

showsPrec :: Int -> Schema -> ShowS

show :: Schema -> String

showList :: [Schema] -> ShowS

Generic Schema

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

Defined in Cryptol.TypeCheck.Type

Methods

rnf :: Schema -> ()

PP Schema

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> Schema -> Doc

FVS Schema

Defined in Cryptol.TypeCheck.Type

Methods

fvs :: Schema -> Set TVar

TVars Schema

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.

Defined in Cryptol.TypeCheck.Subst

Methods

apSubst :: Subst -> Schema -> Schema

FreeVars Schema

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: Schema -> Deps

PP (WithNames Schema)

Defined in Cryptol.TypeCheck.Type

Methods

ppPrec :: Int -> WithNames Schema -> Doc

type Rep Schema

Defined in Cryptol.TypeCheck.Type

type Rep Schema = D1 ('MetaData "Schema" "Cryptol.TypeCheck.Type" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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))))

tMono :: Type -> Schema

isMono :: Schema -> Maybe Type

schemaParam :: Name -> TPFlavor

tySynParam :: Name -> TPFlavor

propSynParam :: Name -> TPFlavor

newtypeParam :: Name -> TPFlavor

modTyParam :: Name -> TPFlavor

tpfName :: TPFlavor -> Maybe Name

tpName :: TParam -> Maybe Name

tvInfo :: TVar -> TVarInfo

tvUnique :: TVar -> Int

noArgDescr :: ArgDescr

tvSourceName :: TypeSource -> Maybe Name

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

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

kindResult :: Kind -> Kind

tpVar :: TParam -> TVar

superclassSet :: Prop -> Set Prop

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

newtypeConType :: Newtype -> Schema

abstractTypeTC :: AbstractType -> TCon

isFreeTV :: TVar -> Bool

isBoundTV :: TVar -> Bool

tIsError :: Type -> Maybe Type

tHasErrors :: Type -> Bool

tIsNat' :: Type -> Maybe Nat'

tIsNum :: Type -> Maybe Integer

tIsInf :: Type -> Bool

tIsVar :: Type -> Maybe TVar

tIsFun :: Type -> Maybe (Type, Type)

tIsSeq :: Type -> Maybe (Type, Type)

tIsBit :: Type -> Bool

tIsInteger :: Type -> Bool

tIsIntMod :: Type -> Maybe Type

tIsRational :: Type -> Bool

tIsFloat :: Type -> Maybe (Type, Type)

tIsTuple :: Type -> Maybe [Type]

tIsRec :: Type -> Maybe (RecordMap Ident Type)

tIsBinFun :: TFun -> Type -> Maybe (Type, Type)

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

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

pIsFin :: Prop -> Maybe Type

pIsPrime :: Prop -> Maybe Type

pIsGeq :: Prop -> Maybe (Type, Type)

pIsEqual :: Prop -> Maybe (Type, Type)

pIsZero :: Prop -> Maybe Type

pIsLogic :: Prop -> Maybe Type

pIsRing :: Prop -> Maybe Type

pIsField :: Prop -> Maybe Type

pIsIntegral :: Prop -> Maybe Type

pIsRound :: Prop -> Maybe Type

pIsEq :: Prop -> Maybe Type

pIsCmp :: Prop -> Maybe Type

pIsSignedCmp :: Prop -> Maybe Type

pIsLiteral :: Prop -> Maybe (Type, Type)

pIsFLiteral :: Prop -> Maybe (Type, Type, Type, Type)

pIsTrue :: Prop -> Bool

pIsWidth :: Prop -> Maybe Type

pIsValidFloat :: Prop -> Maybe (Type, Type)

tNum :: Integral a => a -> Type

tZero :: Type

tOne :: Type

tTwo :: Type

tInf :: Type

tNat' :: Nat' -> Type

tAbstract :: UserTC -> [Type] -> Type

tBit :: Type

tInteger :: Type

tRational :: Type

tFloat :: Type -> Type -> Type

tIntMod :: Type -> Type

tArray :: Type -> Type -> Type

tWord :: Type -> Type

tSeq :: Type -> Type -> Type

tChar :: Type

tString :: Int -> Type

tRec :: RecordMap Ident Type -> Type

tTuple :: [Type] -> Type

newtypeTyCon :: Newtype -> TCon

tFun :: Type -> Type -> Type infixr 5

Make a function type.

tNoUser :: Type -> Type

Eliminate outermost type synonyms.

tError :: Type -> Type

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

tf1 :: TFun -> Type -> Type

tf2 :: TFun -> Type -> Type -> Type

tf3 :: TFun -> Type -> Type -> Type -> Type

tSub :: Type -> Type -> Type

tMul :: Type -> Type -> Type

tDiv :: Type -> Type -> Type

tMod :: Type -> Type -> Type

tExp :: Type -> Type -> Type

tMin :: Type -> Type -> Type

tCeilDiv :: Type -> Type -> Type

tCeilMod :: Type -> Type -> Type

tLenFromThenTo :: Type -> Type -> Type -> Type

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

Equality for numeric types.

(=/=) :: Type -> Type -> Prop

pZero :: Type -> Prop

pLogic :: Type -> Prop

pRing :: Type -> Prop

pIntegral :: Type -> Prop

pField :: Type -> Prop

pRound :: Type -> Prop

pEq :: Type -> Prop

pCmp :: Type -> Prop

pSignedCmp :: Type -> Prop

pLiteral :: Type -> Type -> Prop

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

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

pHas :: Selector -> Type -> Type -> Prop

A Has constraint, used for tuple and record selection.

pTrue :: Prop

pAnd :: [Prop] -> Prop

pSplitAnd :: Prop -> [Prop]

pFin :: Type -> Prop

pValidFloat :: Type -> Type -> Type

pPrime :: Type -> Prop

noFreeVariables :: FVS t => t -> Bool

freeParams :: FVS t => t -> Set TParam

addTNames :: [TParam] -> NameMap -> NameMap

ppNewtypeShort :: Newtype -> Doc

pickTVarName :: Kind -> TypeSource -> Int -> Doc

module Cryptol.TypeCheck.TCon