| Safe Haskell | Safe |
|---|---|
| Language | Haskell98 |
Cryptol.TypeCheck.Type
- data Kind
- data Schema = Forall {}
- data TParam = TParam {}
- data Type
- data TVar
- type Prop = Type
- data TCon
- data PC
- data TC
- data UserTC = UserTC Name Kind
- data TCErrorMessage = TCErrorMessage {
- tcErrorMessage :: !String
- data TySyn = TySyn {}
- data Newtype = Newtype {}
- class HasKind t where
- quickApply :: Kind -> [a] -> Kind
- kindResult :: Kind -> Kind
- tpVar :: TParam -> TVar
- type SType = Type
- 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
- tIsTuple :: Type -> Maybe [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)
- pIsArith :: Prop -> Maybe Type
- pIsCmp :: Prop -> Maybe 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
- 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
- tWidth :: Type -> Type
- tLenFromThen :: Type -> Type -> Type -> Type
- tLenFromThenTo :: Type -> Type -> Type -> Type
- (=#=) :: Type -> Type -> Prop
- (=/=) :: Type -> Type -> Prop
- pArith :: Type -> Prop
- pCmp :: Type -> Prop
- (>==) :: Type -> Type -> Prop
- pHas :: Selector -> Type -> Type -> Prop
- pTrue :: Prop
- pAnd :: [Prop] -> Prop
- pSplitAnd :: Prop -> [Prop]
- pFin :: Type -> Prop
- pError :: TCErrorMessage -> Prop
- class FVS t where
- addTNames :: [TParam] -> NameMap -> NameMap
- ppNewtypeShort :: Newtype -> Doc
- data TFun
Documentation
Kinds, classify types.
The types of polymorphic values.
Instances
| Eq Schema Source # | |
| Show Schema Source # | |
| Generic Schema Source # | |
| NFData Schema Source # | |
| PP Schema Source # | |
| FVS Schema Source # | |
| TVars Schema Source # | WARNING: This instance assumes that the quantified variables in the types in the substitution will not get captured by the quantified variables. This is reasonable because there should be no shadowing of quantified variables but, just in case, we make a sanity check and panic if somehow capture did occur. |
| PP (WithNames Schema) Source # | |
| type Rep Schema Source # | |
Type parameters.
Constructors
| TParam | |
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 |
| TRec ![(Ident, Type)] | Record type |
Type variables.
Type constants.
Predicate symbols.
1-1 constants.
data TCErrorMessage Source #
Constructors
| TCErrorMessage | |
Fields
| |
Type synonym.
Constructors
| TySyn | |
Named records
Constructors
| Newtype | |
quickApply :: Kind -> [a] -> Kind Source #
kindResult :: Kind -> Kind Source #
newtypeConType :: Newtype -> Schema Source #
tSplitFun :: TFun -> Type -> [Type] Source #
Split up repeated occurances of the given binary type-level function.
newtypeTyCon :: Newtype -> TCon Source #
tBadNumber :: TCErrorMessage -> Type Source #
Make a malformed numeric type.
pHas :: Selector -> Type -> Type -> Prop Source #
A Has constraint, used for tuple and record selection.
pError :: TCErrorMessage -> Prop Source #
Make a malformed property.
Minimal complete definition
ppNewtypeShort :: Newtype -> Doc Source #
Built-in types.
Constructors
| TCAdd | : Num -> Num -> Num |
| TCSub | : Num -> Num -> Num |
| TCMul | : Num -> Num -> Num |
| TCDiv | : Num -> Num -> Num |
| TCMod | : Num -> Num -> Num |
| TCExp | : Num -> Num -> Num |
| TCWidth | : Num -> Num |
| TCMin | : Num -> Num -> Num |
| TCMax | : Num -> Num -> Num |
| TCLenFromThen |
|
| TCLenFromThenTo |
|