Safe Haskell	Safe
Language	Haskell2010

Cryptol.TypeCheck.FFI.FFIType

Description

This module defines a nicer intermediate representation of Cryptol types allowed for the FFI, which the typechecker generates then stores in the AST. This way the FFI evaluation code does not have to examine the raw type signatures again.

Synopsis

data FFIFunType t = FFIFunType {
- ffiTParams :: [TParam]
- ffiArgTypes :: [t]
- ffiRetType :: t
}
data FFIType
- = FFIBool
- | FFIBasic FFIBasicType
- | FFIArray [Type] FFIBasicType
- | FFITuple [FFIType]
- | FFIRecord (RecordMap Ident FFIType)
data FFIBasicType
- = FFIBasicVal FFIBasicValType
- | FFIBasicRef FFIBasicRefType
data FFIBasicValType
- = FFIWord Integer FFIWordSize
- | FFIFloat Integer Integer FFIFloatSize
data FFIWordSize
- = FFIWord8
- | FFIWord16
- | FFIWord32
- | FFIWord64
data FFIFloatSize
- = FFIFloat32
- | FFIFloat64
data FFIBasicRefType
- = FFIInteger (Maybe Type)
- | FFIRational

Documentation

data FFIFunType t Source #

Type of a foreign function.

Constructors

FFIFunType
Fields ffiTParams :: [TParam] Note: any type variables within this function type must be bound here. ffiArgTypes :: [t] ffiRetType :: t

Instances

Instances details

Functor FFIFunType Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Methods

fmap :: (a -> b) -> FFIFunType a -> FFIFunType b #

(<$) :: a -> FFIFunType b -> FFIFunType a #

Generic (FFIFunType t) Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Associated Types

type Rep (FFIFunType t)

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

type Rep (FFIFunType t) = D1 ('MetaData "FFIFunType" "Cryptol.TypeCheck.FFI.FFIType" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "FFIFunType" 'PrefixI 'True) (S1 ('MetaSel ('Just "ffiTParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam]) :*: (S1 ('MetaSel ('Just "ffiArgTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [t]) :*: S1 ('MetaSel ('Just "ffiRetType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t))))

Methods

from :: FFIFunType t -> Rep (FFIFunType t) x #

to :: Rep (FFIFunType t) x -> FFIFunType t #

Show t => Show (FFIFunType t) Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Methods

showsPrec :: Int -> FFIFunType t -> ShowS #

show :: FFIFunType t -> String #

showList :: [FFIFunType t] -> ShowS #

TraverseNames t => TraverseNames (FFIFunType t) Source #

Instance details

Defined in Cryptol.IR.TraverseNames

Methods

traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => FFIFunType t -> f (FFIFunType t) Source #

NFData t => NFData (FFIFunType t) Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Methods

rnf :: FFIFunType t -> () #

type Rep (FFIFunType t) Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

type Rep (FFIFunType t) = D1 ('MetaData "FFIFunType" "Cryptol.TypeCheck.FFI.FFIType" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "FFIFunType" 'PrefixI 'True) (S1 ('MetaSel ('Just "ffiTParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam]) :*: (S1 ('MetaSel ('Just "ffiArgTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [t]) :*: S1 ('MetaSel ('Just "ffiRetType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 t))))

data FFIType Source #

Type of a value that can be passed to or returned from a foreign function.

Constructors

FFIBool
FFIBasic FFIBasicType
FFIArray [Type] FFIBasicType	n [m][p]T --> FFIArray [n, m, p] T
FFITuple [FFIType]
FFIRecord (RecordMap Ident FFIType)

Instances

Instances details

Generic FFIType Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Associated Types

type Rep FFIType

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

type Rep FFIType = D1 ('MetaData "FFIType" "Cryptol.TypeCheck.FFI.FFIType" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) ((C1 ('MetaCons "FFIBool" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FFIBasic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFIBasicType))) :+: (C1 ('MetaCons "FFIArray" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Type]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFIBasicType)) :+: (C1 ('MetaCons "FFITuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FFIType])) :+: C1 ('MetaCons "FFIRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RecordMap Ident FFIType))))))

Methods

from :: FFIType -> Rep FFIType x #

to :: Rep FFIType x -> FFIType #

Show FFIType Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Methods

showsPrec :: Int -> FFIType -> ShowS #

show :: FFIType -> String #

showList :: [FFIType] -> ShowS #

TraverseNames FFIType Source #

Instance details

Defined in Cryptol.IR.TraverseNames

Methods

traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => FFIType -> f FFIType Source #

NFData FFIType Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Methods

rnf :: FFIType -> () #

type Rep FFIType Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

type Rep FFIType = D1 ('MetaData "FFIType" "Cryptol.TypeCheck.FFI.FFIType" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) ((C1 ('MetaCons "FFIBool" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FFIBasic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFIBasicType))) :+: (C1 ('MetaCons "FFIArray" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Type]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFIBasicType)) :+: (C1 ('MetaCons "FFITuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FFIType])) :+: C1 ('MetaCons "FFIRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RecordMap Ident FFIType))))))

data FFIBasicType Source #

Types which can be elements of FFI arrays.

Constructors

FFIBasicVal FFIBasicValType
FFIBasicRef FFIBasicRefType

Instances

Instances details

Generic FFIBasicType Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Associated Types

type Rep FFIBasicType

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

type Rep FFIBasicType = D1 ('MetaData "FFIBasicType" "Cryptol.TypeCheck.FFI.FFIType" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "FFIBasicVal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFIBasicValType)) :+: C1 ('MetaCons "FFIBasicRef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFIBasicRefType)))

Methods

from :: FFIBasicType -> Rep FFIBasicType x #

to :: Rep FFIBasicType x -> FFIBasicType #

Show FFIBasicType Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Methods

showsPrec :: Int -> FFIBasicType -> ShowS #

show :: FFIBasicType -> String #

showList :: [FFIBasicType] -> ShowS #

NFData FFIBasicType Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Methods

rnf :: FFIBasicType -> () #

type Rep FFIBasicType Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

type Rep FFIBasicType = D1 ('MetaData "FFIBasicType" "Cryptol.TypeCheck.FFI.FFIType" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "FFIBasicVal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFIBasicValType)) :+: C1 ('MetaCons "FFIBasicRef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFIBasicRefType)))

data FFIBasicValType Source #

Basic type which is passed and returned directly by value.

Constructors

FFIWord
Fields Integer The size of the Cryptol type FFIWordSize The machine word size that it corresponds to
FFIFloat
Fields Integer Exponent Integer Precision FFIFloatSize The machine float size that it corresponds to

Instances

Instances details

Generic FFIBasicValType Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Associated Types

type Rep FFIBasicValType

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

type Rep FFIBasicValType = D1 ('MetaData "FFIBasicValType" "Cryptol.TypeCheck.FFI.FFIType" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "FFIWord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFIWordSize)) :+: C1 ('MetaCons "FFIFloat" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFIFloatSize))))

Methods

from :: FFIBasicValType -> Rep FFIBasicValType x #

to :: Rep FFIBasicValType x -> FFIBasicValType #

Show FFIBasicValType Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Methods

showsPrec :: Int -> FFIBasicValType -> ShowS #

show :: FFIBasicValType -> String #

showList :: [FFIBasicValType] -> ShowS #

NFData FFIBasicValType Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Methods

rnf :: FFIBasicValType -> () #

type Rep FFIBasicValType Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

type Rep FFIBasicValType = D1 ('MetaData "FFIBasicValType" "Cryptol.TypeCheck.FFI.FFIType" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "FFIWord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFIWordSize)) :+: C1 ('MetaCons "FFIFloat" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFIFloatSize))))

data FFIWordSize Source #

Constructors

FFIWord8
FFIWord16
FFIWord32
FFIWord64

Instances

Instances details

Generic FFIWordSize Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Associated Types

type Rep FFIWordSize

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

type Rep FFIWordSize = D1 ('MetaData "FFIWordSize" "Cryptol.TypeCheck.FFI.FFIType" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) ((C1 ('MetaCons "FFIWord8" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FFIWord16" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FFIWord32" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FFIWord64" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: FFIWordSize -> Rep FFIWordSize x #

to :: Rep FFIWordSize x -> FFIWordSize #

Show FFIWordSize Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Methods

showsPrec :: Int -> FFIWordSize -> ShowS #

show :: FFIWordSize -> String #

showList :: [FFIWordSize] -> ShowS #

NFData FFIWordSize Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Methods

rnf :: FFIWordSize -> () #

type Rep FFIWordSize Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

type Rep FFIWordSize = D1 ('MetaData "FFIWordSize" "Cryptol.TypeCheck.FFI.FFIType" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) ((C1 ('MetaCons "FFIWord8" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FFIWord16" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FFIWord32" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FFIWord64" 'PrefixI 'False) (U1 :: Type -> Type)))

data FFIFloatSize Source #

Constructors

FFIFloat32
FFIFloat64

Instances

Instances details

Generic FFIFloatSize Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Associated Types

type Rep FFIFloatSize
Instance details Defined in Cryptol.TypeCheck.FFI.FFIType type Rep FFIFloatSize = D1 ('MetaData "FFIFloatSize" "Cryptol.TypeCheck.FFI.FFIType" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "FFIFloat32" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FFIFloat64" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: FFIFloatSize -> Rep FFIFloatSize x #

to :: Rep FFIFloatSize x -> FFIFloatSize #

Show FFIFloatSize Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Methods

showsPrec :: Int -> FFIFloatSize -> ShowS #

show :: FFIFloatSize -> String #

showList :: [FFIFloatSize] -> ShowS #

NFData FFIFloatSize Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

Methods

rnf :: FFIFloatSize -> () #

type Rep FFIFloatSize Source #

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

type Rep FFIFloatSize = D1 ('MetaData "FFIFloatSize" "Cryptol.TypeCheck.FFI.FFIType" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "FFIFloat32" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FFIFloat64" 'PrefixI 'False) (U1 :: Type -> Type))

data FFIBasicRefType Source #

Basic type which is passed and returned by reference through a parameter.

Constructors