Safe Haskell	Safe
Language	Haskell2010

Cryptol.TypeCheck.Type

Description

This module contains types related to typechecking and the output of the typechecker. In particular, it should contain the types needed by interface files (see Interface), which are (kind of) the output of the typechker.

Synopsis

class FreeAbstract t where
- freeAbstract :: t -> Set UserTC
class FVS t where
- fvs :: t -> Set TVar
type SType = Type
data AbstractType = AbstractType {
- atName :: Name
- atKind :: Kind
- atCtrs :: ([TParam], [Prop])
- atFixitiy :: Maybe Fixity
- atDoc :: Maybe Text
}
data Newtype = Newtype {
- ntName :: Name
- ntParams :: [TParam]
- ntConstraints :: [Prop]
- ntConName :: !Name
- ntFields :: RecordMap Ident Type
- ntDoc :: Maybe Text
}
data TySyn = TySyn {
- tsName :: Name
- tsParams :: [TParam]
- tsConstraints :: [Prop]
- tsDef :: Type
- tsDoc :: !(Maybe Text)
}
type Prop = Type
data TypeWithSource = WithSource {
- twsType :: Type
- twsSource :: TypeSource
- twsRange :: !(Maybe Range)
}
data ArgDescr = ArgDescr {
- argDescrFun :: Maybe Name
- argDescrNumber :: Maybe Int
}
data TypeSource
- = TVFromModParam Name
- | TVFromSignature Name
- | TypeWildCard
- | TypeOfRecordField Ident
- | TypeOfTupleField Int
- | TypeOfSeqElement
- | LenOfSeq
- | TypeParamInstNamed Name Ident
- | TypeParamInstPos Name Int
- | DefinitionOf Name
- | LenOfCompGen
- | TypeOfArg ArgDescr
- | TypeOfRes
- | FunApp
- | TypeOfIfCondExpr
- | TypeFromUserAnnotation
- | GeneratorOfListComp
- | TypeErrorPlaceHolder
data TVarInfo = TVarInfo {
- tvarSource :: !Range
- tvarDesc :: !TypeSource
}
data TVar
- = TVFree !Int Kind (Set TParam) TVarInfo
- | TVBound !TParam
data Type
- = TCon !TCon ![Type]
- | TVar TVar
- | TUser !Name ![Type] !Type
- | TRec !(RecordMap Ident Type)
- | TNewtype !Newtype ![Type]
data TPFlavor
- = TPModParam Name
- | TPUnifyVar
- | TPSchemaParam Name
- | TPTySynParam Name
- | TPPropSynParam Name
- | TPNewtypeParam Name
- | TPPrimParam Name
data TParam = TParam {
- tpUnique :: !Int
- tpKind :: Kind
- tpFlav :: TPFlavor
- tpInfo :: !TVarInfo
}
data Schema = Forall {
- sVars :: [TParam]
- sProps :: [Prop]
- sType :: Type
}
data ModVParam = ModVParam {
- mvpName :: Name
- mvpType :: Schema
- mvpDoc :: Maybe Text
- mvpFixity :: Maybe Fixity
}
data ModTParam = ModTParam {
- mtpName :: Name
- mtpKind :: Kind
- mtpDoc :: Maybe Text
}
data ModParamNames = ModParamNames {
- mpnTypes :: Map Name ModTParam
- mpnTySyn :: !(Map Name TySyn)
- mpnConstraints :: [Located Prop]
- mpnFuns :: Map Name ModVParam
- mpnDoc :: !(Maybe Text)
}
data ModParam = ModParam {
- mpName :: Ident
- mpQual :: !(Maybe ModName)
- mpIface :: ImpName Name
- mpParameters :: ModParamNames
}
type FunctorParams = Map Ident ModParam
allParamNames :: FunctorParams -> ModParamNames
mtpParam :: ModTParam -> TParam
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
quickApply :: Kind -> [a] -> Kind
kindResult :: Kind -> Kind
tpVar :: TParam -> TVar
superclassSet :: Prop -> Set Prop
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]
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)
pIsLiteralLessThan :: 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
tNewtype :: Newtype -> [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
tFun :: Type -> Type -> Type
tNoUser :: Type -> Type
tError :: Type -> Type
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
(=/=) :: 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
pLiteralLessThan :: Type -> Type -> Prop
(>==) :: Type -> Type -> Prop
pHas :: Selector -> Type -> Type -> Prop
pTrue :: Prop
pAnd :: [Prop] -> Prop
pSplitAnd :: Prop -> [Prop]
pFin :: Type -> Prop
pValidFloat :: Type -> Type -> Type
pPrime :: Type -> Prop
pNegNumeric :: Prop -> [Prop]
noFreeVariables :: FVS t => t -> Bool
freeParams :: FVS t => t -> Set TParam
addTNames :: [TParam] -> NameMap -> NameMap
ppNewtypeShort :: Newtype -> Doc
ppNewtypeFull :: Newtype -> Doc
pickTVarName :: Kind -> TypeSource -> Int -> Doc
module Cryptol.TypeCheck.TCon

Documentation

class FreeAbstract t where Source #

Find the abstract types mentioned in a type.

Methods

freeAbstract :: t -> Set UserTC Source #

Instances

Instances details

FreeAbstract TCon Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods freeAbstract :: TCon -> Set UserTC Source #
FreeAbstract Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods freeAbstract :: Type -> Set UserTC Source #
FreeAbstract a => FreeAbstract [a] Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods freeAbstract :: [a] -> Set UserTC Source #
(FreeAbstract a, FreeAbstract b) => FreeAbstract (a, b) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods freeAbstract :: (a, b) -> Set UserTC Source #

class FVS t where Source #

Methods

fvs :: t -> Set TVar Source #

Instances

Instances details

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 FFITypeError Source #
Instance details Defined in Cryptol.TypeCheck.FFI.Error Methods fvs :: FFITypeError -> Set TVar Source #
FVS FFITypeErrorReason Source #
Instance details Defined in Cryptol.TypeCheck.FFI.Error Methods fvs :: FFITypeErrorReason -> 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 Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Schema -> Set TVar Source #
FVS Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Type -> 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 [a] Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: [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
Fields atName :: Name atKind :: Kind atCtrs :: ([TParam], [Prop]) atFixitiy :: Maybe Fixity atDoc :: Maybe Text

Instances

Instances details

Generic AbstractType Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep AbstractType :: Type -> Type # Methods from :: AbstractType -> Rep AbstractType x # to :: Rep AbstractType x -> AbstractType #
Show AbstractType Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> AbstractType -> ShowS # show :: AbstractType -> String # showList :: [AbstractType] -> ShowS #
ModuleInstance AbstractType Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: AbstractType -> AbstractType Source #
HasKind AbstractType Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: AbstractType -> Kind Source #
NFData AbstractType Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: AbstractType -> () #
type Rep AbstractType Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep AbstractType = D1 ('MetaData "AbstractType" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-CoAB0rhRDtyEduZtDlyHHM" '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 Source #

Named records

Constructors

Newtype
Fields ntName :: Name ntParams :: [TParam] ntConstraints :: [Prop] ntConName :: !Name ntFields :: RecordMap Ident Type ntDoc :: Maybe Text

Instances

Instances details

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 #
Show Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> Newtype -> ShowS # show :: Newtype -> String # showList :: [Newtype] -> ShowS #
FreeVars Newtype Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Newtype -> Deps Source #
TraverseNames Newtype Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => Newtype -> f Newtype Source #
ModuleInstance Newtype Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: Newtype -> Newtype Source #
HasKind Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: Newtype -> Kind Source #
PP Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> Newtype -> Doc Source #
NFData Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: Newtype -> () #
Eq Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: Newtype -> Newtype -> Bool # (/=) :: Newtype -> Newtype -> Bool #
Ord Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods compare :: Newtype -> Newtype -> Ordering # (<) :: Newtype -> Newtype -> Bool # (<=) :: Newtype -> Newtype -> Bool # (>) :: Newtype -> Newtype -> Bool # (>=) :: Newtype -> Newtype -> Bool # max :: Newtype -> Newtype -> Newtype # min :: Newtype -> Newtype -> Newtype #
PP (WithNames Newtype) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames Newtype -> Doc Source #
type Rep Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep Newtype = D1 ('MetaData "Newtype" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-CoAB0rhRDtyEduZtDlyHHM" '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 "ntConName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name) :: (S1 ('MetaSel ('Just "ntFields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RecordMap Ident Type)) :*: S1 ('MetaSel ('Just "ntDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text))))))

data TySyn Source #

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

Instances details

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 #
Show TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TySyn -> ShowS # show :: TySyn -> String # showList :: [TySyn] -> ShowS #
TraverseNames TySyn Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => TySyn -> f TySyn Source #
ModuleInstance TySyn Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: TySyn -> TySyn Source #
TVars TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> TySyn -> TySyn Source #
HasKind TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TySyn -> Kind Source #
PP TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TySyn -> Doc Source #
NFData TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TySyn -> () #
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 Rep TySyn = D1 ('MetaData "TySyn" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-CoAB0rhRDtyEduZtDlyHHM" '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 Source #

The type is supposed to be of kind KProp.

data TypeWithSource Source #

A type annotated with information on how it came about.

Constructors

WithSource
Fields twsType :: Type twsSource :: TypeSource twsRange :: !(Maybe Range)

data ArgDescr Source #

Constructors

ArgDescr
Fields argDescrFun :: Maybe Name argDescrNumber :: Maybe Int

Instances

Instances details

Generic ArgDescr Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep ArgDescr :: Type -> Type # Methods from :: ArgDescr -> Rep ArgDescr x # to :: Rep ArgDescr x -> ArgDescr #
Show ArgDescr Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> ArgDescr -> ShowS # show :: ArgDescr -> String # showList :: [ArgDescr] -> ShowS #
TraverseNames ArgDescr Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => ArgDescr -> f ArgDescr Source #
PP ArgDescr Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> ArgDescr -> Doc Source #
NFData ArgDescr Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: ArgDescr -> () #
type Rep ArgDescr Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep ArgDescr = D1 ('MetaData "ArgDescr" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-CoAB0rhRDtyEduZtDlyHHM" '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 Source #

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

Instances details

Generic TypeSource Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep TypeSource :: Type -> Type # Methods from :: TypeSource -> Rep TypeSource x # to :: Rep TypeSource x -> TypeSource #
Show TypeSource Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TypeSource -> ShowS # show :: TypeSource -> String # showList :: [TypeSource] -> ShowS #
TraverseNames TypeSource Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => TypeSource -> f TypeSource Source #
PP TypeSource Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TypeSource -> Doc Source #
NFData TypeSource Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TypeSource -> () #
type Rep TypeSource Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TypeSource = D1 ('MetaData "TypeSource" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-CoAB0rhRDtyEduZtDlyHHM" '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 Source #

Constructors

TVarInfo
Fields tvarSource :: !Range Source code that gave rise tvarDesc :: !TypeSource Description

Instances

Instances details

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 #
Show TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TVarInfo -> ShowS # show :: TVarInfo -> String # showList :: [TVarInfo] -> ShowS #
TraverseNames TVarInfo Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => TVarInfo -> f TVarInfo Source #
PP TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TVarInfo -> Doc Source #
NFData TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TVarInfo -> () #
type Rep TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TVarInfo = D1 ('MetaData "TVarInfo" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-CoAB0rhRDtyEduZtDlyHHM" '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 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 info for nicer warnings/errors.
TVBound !TParam

Instances

Instances details

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 #
Show TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TVar -> ShowS # show :: TVar -> String # showList :: [TVar] -> ShowS #
FreeVars TVar Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: TVar -> Deps Source #
TraverseNames TVar Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => TVar -> f TVar Source #
HasKind TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TVar -> Kind Source #
PP TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TVar -> Doc Source #
NFData TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TVar -> () #
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 #
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 type Rep TVar = D1 ('MetaData "TVar" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-CoAB0rhRDtyEduZtDlyHHM" '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 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
TNewtype !Newtype ![Type]	A newtype

Instances

Instances details

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 #
Show Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> Type -> ShowS # show :: Type -> String # showList :: [Type] -> ShowS #
FreeVars Type Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Type -> Deps Source #
TraverseNames Type Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => Type -> f Type Source #
ModuleInstance Type Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: Type -> Type Source #
ShowParseable Type Source #
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Type -> Doc Void Source #
TVars Type Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Type -> Type 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 #
FreeAbstract Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods freeAbstract :: Type -> Set UserTC Source #
PP Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> Type -> Doc Source #
NFData Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: Type -> () #
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 #
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: `dimensions atype` 5: `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 type Rep Type = D1 ('MetaData "Type" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-CoAB0rhRDtyEduZtDlyHHM" '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))) :+: C1 ('MetaCons "TNewtype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Newtype) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Type])))))

data TPFlavor Source #

Constructors

TPModParam Name
TPUnifyVar
TPSchemaParam Name
TPTySynParam Name
TPPropSynParam Name
TPNewtypeParam Name
TPPrimParam Name

Instances

Instances details

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 #
Show TPFlavor Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TPFlavor -> ShowS # show :: TPFlavor -> String # showList :: [TPFlavor] -> ShowS #
TraverseNames TPFlavor Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => TPFlavor -> f TPFlavor Source #
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-3.0.0-CoAB0rhRDtyEduZtDlyHHM" 'False) ((C1 ('MetaCons "TPModParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "TPUnifyVar" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TPSchemaParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)))) :+: ((C1 ('MetaCons "TPTySynParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "TPPropSynParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name))) :+: (C1 ('MetaCons "TPNewtypeParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "TPPrimParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)))))

data TParam Source #

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

Instances details

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 #
Show TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TParam -> ShowS # show :: TParam -> String # showList :: [TParam] -> ShowS #
TraverseNames TParam Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => TParam -> f TParam Source #
ShowParseable TParam Source #
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: TParam -> Doc Void Source #
HasKind TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TParam -> Kind Source #
PP TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TParam -> Doc Source #
NFData TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TParam -> () #
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 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 #
PP (WithNames TParam) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames TParam -> Doc Source #
type Rep TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TParam = D1 ('MetaData "TParam" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-CoAB0rhRDtyEduZtDlyHHM" '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 Source #

The types of polymorphic values.

Constructors

Forall
Fields sVars :: [TParam] sProps :: [Prop] sType :: Type

Instances

Instances details

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 #
Show Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> Schema -> ShowS # show :: Schema -> String # showList :: [Schema] -> ShowS #
FreeVars Schema Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Schema -> Deps Source #
TraverseNames Schema Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => Schema -> f Schema Source #
ModuleInstance Schema Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: Schema -> Schema 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 #
FVS Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Schema -> Set TVar Source #
PP Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> Schema -> Doc Source #
NFData Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: Schema -> () #
Eq Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: Schema -> Schema -> Bool # (/=) :: Schema -> Schema -> Bool #
PP (WithNames Schema) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames Schema -> Doc Source #
type Rep Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep Schema = D1 ('MetaData "Schema" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-CoAB0rhRDtyEduZtDlyHHM" '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))))

data ModVParam Source #

A value parameter of a module.

Constructors

ModVParam
Fields mvpName :: Name mvpType :: Schema mvpDoc :: Maybe Text mvpFixity :: Maybe Fixity

Instances

Instances details

Generic ModVParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep ModVParam :: Type -> Type # Methods from :: ModVParam -> Rep ModVParam x # to :: Rep ModVParam x -> ModVParam #
Show ModVParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> ModVParam -> ShowS # show :: ModVParam -> String # showList :: [ModVParam] -> ShowS #
TraverseNames ModVParam Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => ModVParam -> f ModVParam Source #
ModuleInstance ModVParam Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: ModVParam -> ModVParam Source #
PP ModVParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> ModVParam -> Doc Source #
NFData ModVParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: ModVParam -> () #
type Rep ModVParam Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep ModVParam = D1 ('MetaData "ModVParam" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-CoAB0rhRDtyEduZtDlyHHM" 'False) (C1 ('MetaCons "ModVParam" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mvpName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Just "mvpType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Schema)) :: (S1 ('MetaSel ('Just "mvpDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text)) :*: S1 ('MetaSel ('Just "mvpFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity)))))

data ModTParam Source #

A type parameter of a module.

Constructors

ModTParam
Fields mtpName :: Name mtpKind :: Kind mtpDoc :: Maybe Text

Instances

Instances details

Generic ModTParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep ModTParam :: Type -> Type # Methods from :: ModTParam -> Rep ModTParam x # to :: Rep ModTParam x -> ModTParam #
Show ModTParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> ModTParam -> ShowS # show :: ModTParam -> String # showList :: [ModTParam] -> ShowS #
TraverseNames ModTParam Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => ModTParam -> f ModTParam Source #
ModuleInstance ModTParam Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: ModTParam -> ModTParam Source #
PP ModTParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> ModTParam -> Doc Source #
NFData ModTParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: ModTParam -> () #
type Rep ModTParam Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep ModTParam = D1 ('MetaData "ModTParam" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-CoAB0rhRDtyEduZtDlyHHM" 'False) (C1 ('MetaCons "ModTParam" 'PrefixI 'True) (S1 ('MetaSel ('Just "mtpName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: (S1 ('MetaSel ('Just "mtpKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind) :: S1 ('MetaSel ('Just "mtpDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text)))))

data ModParamNames Source #

Information about the names brought in through an "interface import". This is also used to keep information about.

Constructors

ModParamNames
Fields mpnTypes :: Map Name ModTParam Type parameters mpnTySyn :: !(Map Name TySyn) Type synonyms mpnConstraints :: [Located Prop] Constraints on param. types mpnFuns :: Map Name ModVParam Value parameters mpnDoc :: !(Maybe Text) Documentation about the interface.

Instances

Instances details

Generic ModParamNames Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep ModParamNames :: Type -> Type # Methods from :: ModParamNames -> Rep ModParamNames x # to :: Rep ModParamNames x -> ModParamNames #
Show ModParamNames Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> ModParamNames -> ShowS # show :: ModParamNames -> String # showList :: [ModParamNames] -> ShowS #
ModuleInstance ModParamNames Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: ModParamNames -> ModParamNames Source #
PP ModParamNames Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> ModParamNames -> Doc Source #
NFData ModParamNames Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: ModParamNames -> () #
type Rep ModParamNames Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep ModParamNames = D1 ('MetaData "ModParamNames" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-CoAB0rhRDtyEduZtDlyHHM" 'False) (C1 ('MetaCons "ModParamNames" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mpnTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name ModTParam)) :: S1 ('MetaSel ('Just "mpnTySyn") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map Name TySyn))) :: (S1 ('MetaSel ('Just "mpnConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located Prop]) :: (S1 ('MetaSel ('Just "mpnFuns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name ModVParam)) :: S1 ('MetaSel ('Just "mpnDoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Text))))))

data ModParam Source #

A module parameter. Corresponds to a "signature import". A single module parameter can bring multiple things in scope.

Constructors

ModParam

Fields

mpName :: Ident
The name of a functor parameter.
mpQual :: !(Maybe ModName)
This is the qualifier for the parameter. We use it to derive parameter names when doing `_` imports.
mpIface :: ImpName Name
The interface corresponding to this parameter. This is thing in `import interface`
mpParameters :: ModParamNames
These are the actual parameters, not the ones in the interface For example if the same interface is used for multiple parameters the ifmpParameters would all be different.

Instances

Instances details

Generic ModParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep ModParam :: Type -> Type # Methods from :: ModParam -> Rep ModParam x # to :: Rep ModParam x -> ModParam #
Show ModParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> ModParam -> ShowS # show :: ModParam -> String # showList :: [ModParam] -> ShowS #
ModuleInstance ModParam Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: ModParam -> ModParam Source #
NFData ModParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: ModParam -> () #
type Rep ModParam Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep ModParam = D1 ('MetaData "ModParam" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-CoAB0rhRDtyEduZtDlyHHM" 'False) (C1 ('MetaCons "ModParam" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mpName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident) :: S1 ('MetaSel ('Just "mpQual") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe ModName))) :: (S1 ('MetaSel ('Just "mpIface") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ImpName Name)) :*: S1 ('MetaSel ('Just "mpParameters") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModParamNames))))