cryptol-3.0.0: Cryptol: The Language of Cryptography

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

- data Type
  - = TCon !TCon ![Type]
  - | TVar TVar
  - | TUser !Name ![Type] !Type
  - | TRec !(RecordMap Ident Type)
  - | TNewtype !Newtype ![Type]
- data TVar
  - = TVFree !Int Kind (Set TParam) TVarInfo
  - | TVBound !TParam
- data ArgDescr = ArgDescr {
  - argDescrFun :: Maybe Name
  - argDescrNumber :: Maybe Int
  }
- data Schema = Forall {
  - sVars :: [TParam]
  - sProps :: [Prop]
  - sType :: Type
  }
- data TParam = TParam {
  - tpUnique :: !Int
  - tpKind :: Kind
  - tpFlav :: TPFlavor
  - tpInfo :: !TVarInfo
  }
- type Prop = Type
- data TySyn = TySyn {
  - tsName :: Name
  - tsParams :: [TParam]
  - tsConstraints :: [Prop]
  - tsDef :: Type
  - tsDoc :: !(Maybe Text)
  }
- data Newtype = Newtype {
  - ntName :: Name
  - ntParams :: [TParam]
  - ntConstraints :: [Prop]
  - ntConName :: !Name
  - ntFields :: RecordMap Ident Type
  - ntDoc :: Maybe Text
  }
- data ModParam = ModParam {
  - mpName :: Ident
  - mpQual :: !(Maybe ModName)
  - mpIface :: ImpName Name
  - mpParameters :: ModParamNames
  }
- data ModParamNames = ModParamNames {
  - mpnTypes :: Map Name ModTParam
  - mpnTySyn :: !(Map Name TySyn)
  - mpnConstraints :: [Located Prop]
  - mpnFuns :: Map Name ModVParam
  - mpnDoc :: !(Maybe Text)
  }
- class FVS t where
  - fvs :: t -> Set TVar
- type FunctorParams = Map Ident ModParam
- data ModTParam = ModTParam {
  - mtpName :: Name
  - mtpKind :: Kind
  - mtpDoc :: Maybe Text
  }
- data ModVParam = ModVParam {
  - mvpName :: Name
  - mvpType :: Schema
  - mvpDoc :: Maybe Text
  - mvpFixity :: Maybe Fixity
  }
- data TVarInfo = TVarInfo {
  - tvarSource :: !Range
  - tvarDesc :: !TypeSource
  }
- data TPFlavor
  - = TPModParam Name
  - | TPUnifyVar
  - | TPSchemaParam Name
  - | TPTySynParam Name
  - | TPPropSynParam Name
  - | TPNewtypeParam Name
  - | TPPrimParam Name
- 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 TypeWithSource = WithSource {
  - twsType :: Type
  - twsSource :: TypeSource
  - twsRange :: !(Maybe Range)
  }
- data AbstractType = AbstractType {
  - atName :: Name
  - atKind :: Kind
  - atCtrs :: ([TParam], [Prop])
  - atFixitiy :: Maybe Fixity
  - atDoc :: Maybe Text
  }
- type SType = Type
- class FreeAbstract t where
  - freeAbstract :: t -> Set UserTC
- tArray :: 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
- tpName :: TParam -> Maybe Name
- (=#=) :: Type -> Type -> Prop
- (>==) :: Type -> Type -> Prop
- tFun :: Type -> Type -> Type
- 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
- 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
- pFin :: Type -> Prop
- tTwo :: Type
- newtypeConType :: Newtype -> Schema
- abstractTypeTC :: AbstractType -> TCon
- isFreeTV :: TVar -> Bool
- isBoundTV :: TVar -> Bool
- tIsError :: Type -> Maybe Type
- tNoUser :: Type -> 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
- 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
- tWord :: Type -> Type
- tSeq :: Type -> Type -> Type
- tChar :: Type
- tString :: Int -> Type
- tRec :: RecordMap Ident Type -> Type
- tTuple :: [Type] -> Type
- tError :: Type -> Type
- tf1 :: TFun -> Type -> Type
- tf2 :: TFun -> Type -> Type -> Type
- tf3 :: TFun -> Type -> Type -> Type -> Type
- (=/=) :: 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
- pHas :: Selector -> Type -> Type -> Prop
- pTrue :: Prop
- pAnd :: [Prop] -> Prop
- pSplitAnd :: Prop -> [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

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 Source # Methods from :: Type -> Rep Type x Source # to :: Rep Type x -> Type Source #
Show Type Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> Type -> ShowS Source # show :: Type -> String Source # showList :: [Type] -> ShowS Source #
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 -> () Source #
Eq Type Source # | Syntactic equality, ignoring type synonyms and record order.
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: Type -> Type -> Bool Source # (/=) :: Type -> Type -> Bool Source #
Ord Type Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods compare :: Type -> Type -> Ordering Source # (<) :: Type -> Type -> Bool Source # (<=) :: Type -> Type -> Bool Source # (>) :: Type -> Type -> Bool Source # (>=) :: Type -> Type -> Bool Source # max :: Type -> Type -> Type Source # min :: Type -> Type -> Type 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: `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-DBVDUAjB1JeD0WzkHH4ckn" '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 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 Source # Methods from :: TVar -> Rep TVar x Source # to :: Rep TVar x -> TVar Source #
Show TVar Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TVar -> ShowS Source # show :: TVar -> String Source # showList :: [TVar] -> ShowS Source #
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 -> () Source #
Eq TVar Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: TVar -> TVar -> Bool Source # (/=) :: TVar -> TVar -> Bool Source #
Ord TVar Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods compare :: TVar -> TVar -> Ordering Source # (<) :: TVar -> TVar -> Bool Source # (<=) :: TVar -> TVar -> Bool Source # (>) :: TVar -> TVar -> Bool Source # (>=) :: TVar -> TVar -> Bool Source # max :: TVar -> TVar -> TVar Source # min :: TVar -> TVar -> TVar 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

type Rep TVar = D1 ('MetaData "TVar" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 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 Source # Methods from :: ArgDescr -> Rep ArgDescr x Source # to :: Rep ArgDescr x -> ArgDescr Source #
Show ArgDescr Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> ArgDescr -> ShowS Source # show :: ArgDescr -> String Source # showList :: [ArgDescr] -> ShowS Source #
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 -> () Source #
type Rep ArgDescr Source # |

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep ArgDescr = D1 ('MetaData "ArgDescr" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 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 Source # Methods from :: Schema -> Rep Schema x Source # to :: Rep Schema x -> Schema Source #
Show Schema Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> Schema -> ShowS Source # show :: Schema -> String Source # showList :: [Schema] -> ShowS Source #
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 -> () Source #
Eq Schema Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: Schema -> Schema -> Bool Source # (/=) :: Schema -> Schema -> Bool Source #
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-DBVDUAjB1JeD0WzkHH4ckn" '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 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 Source # Methods from :: TParam -> Rep TParam x Source # to :: Rep TParam x -> TParam Source #
Show TParam Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TParam -> ShowS Source # show :: TParam -> String Source # showList :: [TParam] -> ShowS Source #
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 -> () Source #
Eq TParam Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: TParam -> TParam -> Bool Source # (/=) :: TParam -> TParam -> Bool Source #
Ord TParam Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods compare :: TParam -> TParam -> Ordering Source # (<) :: TParam -> TParam -> Bool Source # (<=) :: TParam -> TParam -> Bool Source # (>) :: TParam -> TParam -> Bool Source # (>=) :: TParam -> TParam -> Bool Source # max :: TParam -> TParam -> TParam Source # min :: TParam -> TParam -> TParam Source #
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-DBVDUAjB1JeD0WzkHH4ckn" '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))))

type Prop = Type Source #

The type is supposed to be of kind `KProp`.

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 Source # Methods from :: TySyn -> Rep TySyn x Source # to :: Rep TySyn x -> TySyn Source #
Show TySyn Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TySyn -> ShowS Source # show :: TySyn -> String Source # showList :: [TySyn] -> ShowS Source #
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 -> () 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 Rep TySyn = D1 ('MetaData "TySyn" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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))))))

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 Source # Methods from :: Newtype -> Rep Newtype x Source # to :: Rep Newtype x -> Newtype Source #
Show Newtype Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> Newtype -> ShowS Source # show :: Newtype -> String Source # showList :: [Newtype] -> ShowS Source #
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 -> () Source #
Eq Newtype Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: Newtype -> Newtype -> Bool Source # (/=) :: Newtype -> Newtype -> Bool Source #
Ord Newtype Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods compare :: Newtype -> Newtype -> Ordering Source # (<) :: Newtype -> Newtype -> Bool Source # (<=) :: Newtype -> Newtype -> Bool Source # (>) :: Newtype -> Newtype -> Bool Source # (>=) :: Newtype -> Newtype -> Bool Source # max :: Newtype -> Newtype -> Newtype Source # min :: Newtype -> Newtype -> Newtype Source #
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-DBVDUAjB1JeD0WzkHH4ckn" '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 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 Source # Methods from :: ModParam -> Rep ModParam x Source # to :: Rep ModParam x -> ModParam Source #
Show ModParam Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> ModParam -> ShowS Source # show :: ModParam -> String Source # showList :: [ModParam] -> ShowS Source #
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 -> () Source #
type Rep ModParam Source # |

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep ModParam = D1 ('MetaData "ModParam" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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))))

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 Source # Methods from :: ModParamNames -> Rep ModParamNames x Source # to :: Rep ModParamNames x -> ModParamNames Source #
Show ModParamNames Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> ModParamNames -> ShowS Source # show :: ModParamNames -> String Source # showList :: [ModParamNames] -> ShowS Source #
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 -> () Source #
type Rep ModParamNames Source # |

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep ModParamNames = D1 ('MetaData "ModParamNames" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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))))))

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 FunctorParams = Map Ident ModParam Source #

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 Source # Methods from :: ModTParam -> Rep ModTParam x Source # to :: Rep ModTParam x -> ModTParam Source #
Show ModTParam Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> ModTParam -> ShowS Source # show :: ModTParam -> String Source # showList :: [ModTParam] -> ShowS Source #
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 -> () Source #
type Rep ModTParam Source # |

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep ModTParam = D1 ('MetaData "ModTParam" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 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 Source # Methods from :: ModVParam -> Rep ModVParam x Source # to :: Rep ModVParam x -> ModVParam Source #
Show ModVParam Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> ModVParam -> ShowS Source # show :: ModVParam -> String Source # showList :: [ModVParam] -> ShowS Source #
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 -> () Source #
type Rep ModVParam Source # |

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep ModVParam = D1 ('MetaData "ModVParam" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 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 Source # Methods from :: TVarInfo -> Rep TVarInfo x Source # to :: Rep TVarInfo x -> TVarInfo Source #
Show TVarInfo Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TVarInfo -> ShowS Source # show :: TVarInfo -> String Source # showList :: [TVarInfo] -> ShowS Source #
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 -> () Source #
type Rep TVarInfo Source # |

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TVarInfo = D1 ('MetaData "TVarInfo" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 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 Source # Methods from :: TPFlavor -> Rep TPFlavor x Source # to :: Rep TPFlavor x -> TPFlavor Source #
Show TPFlavor Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TPFlavor -> ShowS Source # show :: TPFlavor -> String Source # showList :: [TPFlavor] -> ShowS Source #
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 -> () Source #
type Rep TPFlavor Source # |

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TPFlavor = D1 ('MetaData "TPFlavor" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 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 Source # Methods from :: TypeSource -> Rep TypeSource x Source # to :: Rep TypeSource x -> TypeSource Source #
Show TypeSource Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TypeSource -> ShowS Source # show :: TypeSource -> String Source # showList :: [TypeSource] -> ShowS Source #
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 -> () Source #
type Rep TypeSource Source # |

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TypeSource = D1 ('MetaData "TypeSource" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 TypeWithSource Source #

A type annotated with information on how it came about.

Constructors

WithSource |

Fields

- twsType :: Type
- twsSource :: TypeSource
- twsRange :: !(Maybe Range)

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 Source # Methods from :: AbstractType -> Rep AbstractType x Source # to :: Rep AbstractType x -> AbstractType Source #
Show AbstractType Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> AbstractType -> ShowS Source # show :: AbstractType -> String Source # showList :: [AbstractType] -> ShowS Source #
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 -> () Source #
type Rep AbstractType Source # |

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep AbstractType = D1 ('MetaData "AbstractType" "Cryptol.TypeCheck.Type" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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))))))

type SType = Type Source #

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

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 #

tArray :: Type -> Type -> Type Source #

tSub :: Type -> Type -> Type Source #

tMul :: Type -> Type -> Type Source #

tDiv :: Type -> Type -> Type Source #

tMod :: Type -> Type -> Type Source #

tExp :: Type -> Type -> Type Source #

tMin :: Type -> Type -> Type Source #

tCeilDiv :: Type -> Type -> Type Source #

tCeilMod :: Type -> Type -> Type Source #

tLenFromThenTo :: Type -> Type -> Type -> Type Source #

tpName :: TParam -> Maybe Name 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.

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

Make a function type.

allParamNames :: FunctorParams -> ModParamNames Source #

Compute the names from all functor parameters

mtpParam :: ModTParam -> TParam Source #

This is how module parameters appear in actual types.

tMono :: Type -> Schema Source #

isMono :: Schema -> Maybe Type Source #

schemaParam :: Name -> TPFlavor Source #

tySynParam :: Name -> TPFlavor Source #

propSynParam :: Name -> TPFlavor Source #

newtypeParam :: Name -> TPFlavor Source #

modTyParam :: Name -> TPFlavor Source #

tpfName :: TPFlavor -> Maybe Name Source #

tvInfo :: TVar -> TVarInfo Source #

tvUnique :: TVar -> Int Source #

noArgDescr :: ArgDescr Source #

tvSourceName :: TypeSource -> Maybe Name Source #

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

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

kindResult :: Kind -> Kind Source #

tpVar :: TParam -> TVar Source #

superclassSet :: Prop -> Set Prop Source #

Compute the set of all `Prop`s that are implied by the given prop via superclass constraints.

pFin :: Type -> Prop Source #

tTwo :: Type Source #

newtypeConType :: Newtype -> Schema Source #

abstractTypeTC :: AbstractType -> TCon Source #

isFreeTV :: TVar -> Bool Source #

isBoundTV :: TVar -> Bool Source #

tIsError :: Type -> Maybe Type Source #

tNoUser :: Type -> Type Source #

Eliminate outermost type synonyms.

tHasErrors :: Type -> Bool Source #

tIsNat' :: Type -> Maybe Nat' Source #

tIsNum :: Type -> Maybe Integer Source #

tIsInf :: Type -> Bool Source #

tIsVar :: Type -> Maybe TVar Source #

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

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

tIsBit :: Type -> Bool Source #

tIsInteger :: Type -> Bool Source #

tIsIntMod :: Type -> Maybe Type Source #

tIsRational :: Type -> Bool Source #

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

tIsTuple :: Type -> Maybe [Type] Source #

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

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

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

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

pIsFin :: Prop -> Maybe Type Source #

pIsPrime :: Prop -> Maybe Type Source #

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

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

pIsZero :: Prop -> Maybe Type Source #

pIsLogic :: Prop -> Maybe Type Source #

pIsRing :: Prop -> Maybe Type Source #

pIsField :: Prop -> Maybe Type Source #

pIsIntegral :: Prop -> Maybe Type Source #

pIsRound :: Prop -> Maybe Type Source #

pIsEq :: Prop -> Maybe Type Source #

pIsCmp :: Prop -> Maybe Type Source #

pIsSignedCmp :: Prop -> Maybe Type Source #

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

pIsLiteralLessThan :: Prop -> Maybe (Type, Type) Source #

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

pIsTrue :: Prop -> Bool Source #

pIsWidth :: Prop -> Maybe Type Source #

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

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

tZero :: Type Source #

tOne :: Type Source #

tInf :: Type Source #

tNat' :: Nat' -> Type Source #

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

tNewtype :: Newtype -> [Type] -> Type Source #

tBit :: Type Source #

tInteger :: Type Source #

tRational :: Type Source #

tFloat :: Type -> Type -> Type Source #

tIntMod :: Type -> Type Source #

tWord :: Type -> Type Source #

tSeq :: Type -> Type -> Type Source #

tChar :: Type Source #

tString :: Int -> Type Source #

tRec :: RecordMap Ident Type -> Type Source #

tTuple :: [Type] -> Type Source #

tError :: Type -> Type Source #

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

tf1 :: TFun -> Type -> Type Source #

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

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

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

pZero :: Type -> Prop Source #

pLogic :: Type -> Prop Source #

pRing :: Type -> Prop Source #

pIntegral :: Type -> Prop Source #

pField :: Type -> Prop Source #

pRound :: Type -> Prop Source #

pEq :: Type -> Prop Source #

pCmp :: Type -> Prop Source #

pSignedCmp :: Type -> Prop Source #

pLiteral :: Type -> Type -> Prop Source #

pLiteralLessThan :: Type -> Type -> Prop Source #

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

A `Has` constraint, used for tuple and record selection.

pTrue :: Prop Source #

pAnd :: [Prop] -> Prop Source #

pSplitAnd :: Prop -> [Prop] Source #

pValidFloat :: Type -> Type -> Type Source #

pPrime :: Type -> Prop Source #

pNegNumeric :: Prop -> [Prop] Source #

`pNegNumeric` negates a simple (i.e., not And, not prime, etc) prop over numeric type vars. The result is a conjunction of properties.

noFreeVariables :: FVS t => t -> Bool Source #

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

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

ppNewtypeShort :: Newtype -> Doc Source #

ppNewtypeFull :: Newtype -> Doc Source #

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

module Cryptol.TypeCheck.TCon