cryptol-3.0.0: Cryptol: The Language of Cryptography

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

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

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

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

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

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

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

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

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

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

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

Instance details

Defined in Cryptol.TypeCheck.FFI.FFIType

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