cryptol-2.6.0: Cryptol: The Language of Cryptography

Safe Haskell | Safe
Language | Haskell2010

Cryptol.TypeCheck.Type

Synopsis

- class FVS t where
  - fvs :: t -> Set TVar
- type SType = Type
- data Newtype = Newtype {
  - ntName :: Name
  - ntParams :: [TParam]
  - ntConstraints :: [Prop]
  - ntFields :: [(Ident, Type)]
  - ntDoc :: Maybe String
  }
- data TySyn = TySyn {
  - tsName :: Name
  - tsParams :: [TParam]
  - tsConstraints :: [Prop]
  - tsDef :: Type
  - tsDoc :: !(Maybe String)
  }
- type Prop = Type
- data TVarSource
  - = TVFromModParam Name
  - | TVFromSignature Name
  - | TypeWildCard
  - | TypeOfRecordField Ident
  - | TypeOfTupleField Int
  - | TypeOfSeqElement
  - | LenOfSeq
  - | TypeParamInstNamed Name Ident
  - | TypeParamInstPos Name Int
  - | DefinitionOf Name
  - | LenOfCompGen
  - | TypeOfArg (Maybe Int)
  - | TypeOfRes
  - | TypeErrorPlaceHolder
- data TVarInfo = TVarInfo {
  - tvarSource :: Range
  - tvarDesc :: TVarSource
  }
- data TVar
  - = TVFree !Int Kind (Set TParam) TVarInfo
  - | TVBound !TParam
- data Type
  - = TCon !TCon ![Type]
  - | TVar TVar
  - | TUser !Name ![Type] !Type
  - | TRec ![(Ident, Type)]
- data TPFlavor
  - = TPModParam Name
  - | TPOther (Maybe Name)
- data TParam = TParam {
  - tpUnique :: !Int
  - tpKind :: Kind
  - tpFlav :: TPFlavor
  - tpInfo :: !TVarInfo
  }
- data Schema = Forall {
  - sVars :: [TParam]
  - sProps :: [Prop]
  - sType :: Type
  }
- tMono :: Type -> Schema
- isMono :: Schema -> Maybe Type
- schemaParam :: Name -> TPFlavor
- tySynParam :: Name -> TPFlavor
- propSynParam :: Name -> TPFlavor
- newtypeParam :: Name -> TPFlavor
- modTyParam :: Name -> TPFlavor
- tpfName :: TPFlavor -> Maybe Name
- tpName :: TParam -> Maybe Name
- tvInfo :: TVar -> TVarInfo
- tvSourceName :: TVarSource -> Maybe Name
- quickApply :: Kind -> [a] -> Kind
- kindResult :: Kind -> Kind
- tpVar :: TParam -> TVar
- newtypeConType :: Newtype -> Schema
- isFreeTV :: TVar -> Bool
- isBoundTV :: TVar -> Bool
- tIsError :: Type -> Maybe TCErrorMessage
- 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
- tIsTuple :: Type -> Maybe [Type]
- tIsRec :: Type -> Maybe [(Ident, Type)]
- tIsBinFun :: TFun -> Type -> Maybe (Type, Type)
- tSplitFun :: TFun -> Type -> [Type]
- pIsFin :: Prop -> Maybe Type
- pIsGeq :: Prop -> Maybe (Type, Type)
- pIsEq :: Prop -> Maybe (Type, Type)
- pIsZero :: Prop -> Maybe Type
- pIsLogic :: Prop -> Maybe Type
- pIsArith :: Prop -> Maybe Type
- pIsCmp :: Prop -> Maybe Type
- pIsSignedCmp :: Prop -> Maybe Type
- pIsLiteral :: Prop -> Maybe (Type, Type)
- pIsTrue :: Prop -> Bool
- pIsWidth :: Prop -> Maybe Type
- tNum :: Integral a => a -> Type
- tZero :: Type
- tOne :: Type
- tTwo :: Type
- tInf :: Type
- tNat' :: Nat' -> Type
- tBit :: Type
- tInteger :: Type
- tIntMod :: Type -> Type
- tWord :: Type -> Type
- tSeq :: Type -> Type -> Type
- tChar :: Type
- tString :: Int -> Type
- tRec :: [(Ident, Type)] -> Type
- tTuple :: [Type] -> Type
- newtypeTyCon :: Newtype -> TCon
- tFun :: Type -> Type -> Type
- tNoUser :: Type -> Type
- tBadNumber :: TCErrorMessage -> 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
- tLenFromThen :: Type -> Type -> Type -> Type
- tLenFromThenTo :: Type -> Type -> Type -> Type
- (=#=) :: Type -> Type -> Prop
- (=/=) :: Type -> Type -> Prop
- pZero :: Type -> Prop
- pLogic :: Type -> Prop
- pArith :: Type -> Prop
- pCmp :: Type -> Prop
- pSignedCmp :: Type -> Prop
- pLiteral :: Type -> Type -> Prop
- (>==) :: Type -> Type -> Prop
- pHas :: Selector -> Type -> Type -> Prop
- pTrue :: Prop
- pAnd :: [Prop] -> Prop
- pSplitAnd :: Prop -> [Prop]
- pFin :: Type -> Prop
- pError :: TCErrorMessage -> Prop
- noFreeVariables :: FVS t => t -> Bool
- addTNames :: [TParam] -> NameMap -> NameMap
- ppNewtypeShort :: Newtype -> Doc
- pickTVarName :: Kind -> TVarSource -> Int -> Doc
- module Cryptol.Prims.Syntax

# Documentation

class FVS t where Source #

Methods

fvs :: t -> Set TVar Source #

Instances

FVS Type Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Type -> Set TVar Source #
FVS Schema Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Schema -> Set TVar Source #
FVS DelayedCt Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods fvs :: DelayedCt -> Set TVar Source #
FVS Goal Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods fvs :: Goal -> Set TVar Source #
FVS Error Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods fvs :: Error -> Set TVar Source #
FVS Warning Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods fvs :: Warning -> Set TVar Source #
FVS a => FVS [a] Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: [a] -> Set TVar Source #
FVS a => FVS (Maybe a) Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Maybe a -> Set TVar Source #
(FVS a, FVS b) => FVS (a, b) Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: (a, b) -> Set TVar Source #

type SType = Type Source #

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

data Newtype Source #

Named records

Constructors

Newtype |

Fields

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

Instances

Show Newtype Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> Newtype -> ShowS Source # show :: Newtype -> String Source # showList :: [Newtype] -> ShowS Source #
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 #
NFData Newtype Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: Newtype -> () Source #
PP Newtype Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> Newtype -> Doc Source #
HasKind Newtype Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: Newtype -> Kind Source #
FreeVars Newtype Source # |
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Newtype -> Deps 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-2.6.0-FO78l5UWBYr51eDL1ksQpO" False) (C1 (MetaCons "Newtype" PrefixI True) ((S1 (MetaSel (Just "ntName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Just "ntParams") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TParam])) :*: (S1 (MetaSel (Just "ntConstraints") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Prop]) :*: (S1 (MetaSel (Just "ntFields") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Ident, Type)]) :*: S1 (MetaSel (Just "ntDoc") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe String))))))

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 String)

  Documentation

Instances

Show TySyn Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TySyn -> ShowS Source # show :: TySyn -> String Source # showList :: [TySyn] -> ShowS Source #
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 #
NFData TySyn Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TySyn -> () Source #
PP TySyn Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TySyn -> Doc Source #
HasKind TySyn Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TySyn -> Kind Source #
PP (WithNames TySyn) Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames TySyn -> Doc Source #
type Rep TySyn Source # |

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TySyn = D1 (MetaData "TySyn" "Cryptol.TypeCheck.Type" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" 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 String))))))

type Prop = Type Source #

The type is supposed to be of kind `KProp`

data TVarSource Source #

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 (Maybe Int) |
TypeOfRes |
TypeErrorPlaceHolder |

Instances

Show TVarSource Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TVarSource -> ShowS Source # show :: TVarSource -> String Source # showList :: [TVarSource] -> ShowS Source #
Generic TVarSource Source # |
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep TVarSource :: Type -> Type Source # Methods from :: TVarSource -> Rep TVarSource x Source # to :: Rep TVarSource x -> TVarSource Source #
NFData TVarSource Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TVarSource -> () Source #
PP TVarSource Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TVarSource -> Doc Source #
type Rep TVarSource Source # |

Instance details

Defined in Cryptol.TypeCheck.Type

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

data TVarInfo Source #

Constructors

TVarInfo |

Fields

- tvarSource :: Range

  Source code that gave rise

- tvarDesc :: TVarSource

  Description

Instances

Show TVarInfo Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TVarInfo -> ShowS Source # show :: TVarInfo -> String Source # showList :: [TVarInfo] -> ShowS Source #
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 #
NFData TVarInfo Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TVarInfo -> () Source #
PP TVarInfo Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TVarInfo -> Doc Source #
type Rep TVarInfo Source # |

Instance details

Defined in Cryptol.TypeCheck.Type

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

data TVar Source #

Type variables.

Constructors

TVFree !Int Kind (Set TParam) TVarInfo | Unique, kind, ids of bound type variables that are in scope The last field gives us some infor for nicer warnings/errors.
TVBound !TParam |

Instances

Eq TVar Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: TVar -> TVar -> Bool 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 #
Show TVar Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TVar -> ShowS Source # show :: TVar -> String Source # showList :: [TVar] -> ShowS Source #
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 #
NFData TVar Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TVar -> () Source #
PP TVar Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TVar -> Doc Source #
HasKind TVar Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TVar -> Kind Source #
FreeVars TVar Source # |
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: TVar -> Deps Source #
PP (WithNames TVar) Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames TVar -> Doc Source #
type Rep TVar Source # |

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TVar = D1 (MetaData "TVar" "Cryptol.TypeCheck.Type" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" 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 ![(Ident, Type)] | Record type

Instances

Eq Type Source # |
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 #
Show Type Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> Type -> ShowS Source # show :: Type -> String Source # showList :: [Type] -> ShowS Source #
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 #
NFData Type Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: Type -> () Source #
PP Type Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> Type -> Doc Source #
HasKind Type Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: Type -> Kind Source #
FVS Type Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Type -> Set TVar Source #
ShowParseable Type Source # |
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Type -> Doc Source #
FreeVars Type Source # |
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Type -> Deps Source #
TVars Type Source # |
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> 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 # |
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-2.6.0-FO78l5UWBYr51eDL1ksQpO" 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 [(Ident, Type)]))))

data TPFlavor Source #

Constructors

TPModParam Name |
TPOther (Maybe Name) |

Instances

Show TPFlavor Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TPFlavor -> ShowS Source # show :: TPFlavor -> String Source # showList :: [TPFlavor] -> ShowS Source #
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 #
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-2.6.0-FO78l5UWBYr51eDL1ksQpO" False) (C1 (MetaCons "TPModParam" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: C1 (MetaCons "TPOther" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Name))))

data TParam Source #

Type parameters.

Constructors

TParam |

Fields

- tpUnique :: !Int

  Parameter identifier

- tpKind :: Kind

  Kind of parameter

- tpFlav :: TPFlavor

  What sort of type parameter is this

- tpInfo :: !TVarInfo

  A description for better messages.

Instances

Eq TParam 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 #
Show TParam Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TParam -> ShowS Source # show :: TParam -> String Source # showList :: [TParam] -> ShowS Source #
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 #
NFData TParam Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TParam -> () Source #
PP TParam Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TParam -> Doc Source #
HasKind TParam Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TParam -> Kind Source #
ShowParseable TParam Source # |
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: TParam -> Doc 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-2.6.0-FO78l5UWBYr51eDL1ksQpO" 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

Eq Schema Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: Schema -> Schema -> Bool Source # (/=) :: Schema -> Schema -> Bool 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 #
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 #
NFData Schema Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: Schema -> () Source #
PP Schema Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> Schema -> Doc Source #
FVS Schema Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Schema -> Set TVar Source #
FreeVars Schema Source # |
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Schema -> Deps 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 #
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-2.6.0-FO78l5UWBYr51eDL1ksQpO" False) (C1 (MetaCons "Forall" PrefixI True) (S1 (MetaSel (Just "sVars") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TParam]) :*: (S1 (MetaSel (Just "sProps") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Prop]) :*: S1 (MetaSel (Just "sType") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type))))

tMono :: Type -> Schema 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 #

tpName :: TParam -> Maybe Name Source #

tvInfo :: TVar -> TVarInfo Source #

tvSourceName :: TVarSource -> 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 #

newtypeConType :: Newtype -> Schema Source #

isFreeTV :: TVar -> Bool Source #

isBoundTV :: TVar -> Bool Source #

tIsError :: Type -> Maybe TCErrorMessage 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 #

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

tIsRec :: Type -> Maybe [(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 #

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

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

pIsZero :: Prop -> Maybe Type Source #

pIsLogic :: Prop -> Maybe Type Source #

pIsArith :: Prop -> Maybe Type Source #

pIsCmp :: Prop -> Maybe Type Source #

pIsSignedCmp :: Prop -> Maybe Type Source #

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

pIsTrue :: Prop -> Bool Source #

pIsWidth :: Prop -> Maybe Type Source #

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

tZero :: Type Source #

tOne :: Type Source #

tTwo :: Type Source #

tInf :: Type Source #

tNat' :: Nat' -> Type Source #

tBit :: Type Source #

tInteger :: Type Source #

tIntMod :: Type -> Type Source #

tWord :: Type -> Type Source #

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

tChar :: Type Source #

tString :: Int -> Type Source #

tRec :: [(Ident, Type)] -> Type Source #

tTuple :: [Type] -> Type Source #

newtypeTyCon :: Newtype -> TCon Source #

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

Make a function type.

tNoUser :: Type -> Type Source #

Eliminate outermost type synonyms.

tBadNumber :: TCErrorMessage -> Type Source #

Make a malformed numeric type.

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

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

tf3 :: TFun -> Type -> 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 #

tLenFromThen :: Type -> Type -> Type -> Type Source #

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

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

Equality for numeric types.

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

pZero :: Type -> Prop Source #

pLogic :: Type -> Prop Source #

pArith :: Type -> Prop Source #

pCmp :: Type -> Prop Source #

pSignedCmp :: Type -> Prop Source #

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

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

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

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

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

pTrue :: Prop Source #

pAnd :: [Prop] -> Prop Source #

pSplitAnd :: Prop -> [Prop] Source #

pFin :: Type -> Prop Source #

pError :: TCErrorMessage -> Prop Source #

Make a malformed property.

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

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

ppNewtypeShort :: Newtype -> Doc Source #

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

module Cryptol.Prims.Syntax