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 = FFIFunType {
- ffiTParams :: [TParam]
- ffiArgTypes :: [FFIType]
- ffiRetType :: FFIType
}
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 Source #

Type of a foreign function.

Constructors

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

Instances

Instances details

Generic FFIFunType Source #
Instance details Defined in Cryptol.TypeCheck.FFI.FFIType Associated Types type Rep FFIFunType :: Type -> Type # Methods from :: FFIFunType -> Rep FFIFunType x # to :: Rep FFIFunType x -> FFIFunType #
Show FFIFunType Source #
Instance details Defined in Cryptol.TypeCheck.FFI.FFIType Methods showsPrec :: Int -> FFIFunType -> ShowS # show :: FFIFunType -> String # showList :: [FFIFunType] -> ShowS #
TraverseNames FFIFunType Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => FFIFunType -> f FFIFunType Source #
NFData FFIFunType Source #
Instance details Defined in Cryptol.TypeCheck.FFI.FFIType Methods rnf :: FFIFunType -> () #
type Rep FFIFunType Source #
Instance details Defined in Cryptol.TypeCheck.FFI.FFIType type Rep FFIFunType = D1 ('MetaData "FFIFunType" "Cryptol.TypeCheck.FFI.FFIType" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "FFIFunType" 'PrefixI 'True) (S1 ('MetaSel ('Just "ffiTParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam]) :: (S1 ('MetaSel ('Just "ffiArgTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FFIType]) :: S1 ('MetaSel ('Just "ffiRetType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FFIType))))

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 :: Type -> Type # 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.1.0-276efOa9Q2aIFSEzDdp2Mp" '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 :: Type -> Type # 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.1.0-276efOa9Q2aIFSEzDdp2Mp" '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 :: Type -> Type # 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.1.0-276efOa9Q2aIFSEzDdp2Mp" '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 :: 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.1.0-276efOa9Q2aIFSEzDdp2Mp" '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 :: 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.1.0-276efOa9Q2aIFSEzDdp2Mp" '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

FFIInteger (Maybe Type)	Modulus (Just for Z, Nothing for Integer)
FFIRational

Instances

Instances details

Generic FFIBasicRefType Source #
Instance details Defined in Cryptol.TypeCheck.FFI.FFIType Associated Types type Rep FFIBasicRefType :: Type -> Type # Methods from :: FFIBasicRefType -> Rep FFIBasicRefType x # to :: Rep FFIBasicRefType x -> FFIBasicRefType #
Show FFIBasicRefType Source #
Instance details Defined in Cryptol.TypeCheck.FFI.FFIType Methods showsPrec :: Int -> FFIBasicRefType -> ShowS # show :: FFIBasicRefType -> String # showList :: [FFIBasicRefType] -> ShowS #
NFData FFIBasicRefType Source #
Instance details Defined in Cryptol.TypeCheck.FFI.FFIType Methods rnf :: FFIBasicRefType -> () #
type Rep FFIBasicRefType Source #
Instance details Defined in Cryptol.TypeCheck.FFI.FFIType type Rep FFIBasicRefType = D1 ('MetaData "FFIBasicRefType" "Cryptol.TypeCheck.FFI.FFIType" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "FFIInteger" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Type))) :+: C1 ('MetaCons "FFIRational" 'PrefixI 'False) (U1 :: Type -> Type))