Sqlite3.Marshall

Reexports

Definitions

0 LAll : (0 _ : (k -> Type)) -> List k -> Type

Totality: total
Visibility: public export

interface FromCell : Type -> Type

  Inteface for converting an Idris value to a single cell in a table row.

Parameters: a
Constructor: 

MkFromCell

Methods:

fromCellType : SqliteType

fromCell : Maybe (IdrisType fromCellType) -> Either SqlError a

Implementations:

FromCell a => FromCell (Maybe a)

FromCell Integer

FromCell Nat

FromCell Int64

FromCell Int32

FromCell Int16

FromCell Int8

FromCell Bits64

FromCell Bits32

FromCell Bits16

FromCell Bits8

FromCell String

FromCell ByteString

FromCell Double

FromCell Bool

fromCellType : FromCell a => SqliteType

Totality: total
Visibility: public export

fromCell : {auto __con : FromCell a} -> Maybe (IdrisType fromCellType) -> Either SqlError a

Totality: total
Visibility: public export

FromCellType : (0 a : Type) -> FromCell a => SqliteType

  Utility alias for `fromCellType` with an explicit erased type argument.

Totality: total
Visibility: public export

decodeJust : String -> (t -> Either SqlError a) -> Maybe t -> Either SqlError a

  Utility for implementing `fromCell` for non-nullable data types.
  
  In case of a `Nothing` (corresponding to `NULL` in SQL land),
  this fails with a `NullPointer` error that wraps the type name
  to display, what kind of data we tried to convert.

Totality: total
Visibility: export

interface ToCell : Type -> Type

  Inteface for converting an Idris value to a single cell in a table row.

Parameters: a
Constructor: 

MkToCell

Methods:

toCellType : SqliteType

toCell : a -> Maybe (IdrisType toCellType)

Implementations:

ToCell a => ToCell (Maybe a)

ToCell Int64

ToCell Int32

ToCell Int16

ToCell Int8

ToCell Bits64

ToCell Bits32

ToCell Bits16

ToCell Bits8

ToCell String

ToCell ByteString

ToCell Double

ToCell Bool

toCellType : ToCell a => SqliteType

Totality: total
Visibility: public export

toCell : {auto __con : ToCell a} -> a -> Maybe (IdrisType toCellType)

Totality: total
Visibility: public export

ToCellType : (0 a : Type) -> ToCell a => SqliteType

  Utility alias for `toCellType` with an explicit erased type argument.

Totality: total
Visibility: public export

interface FromRow : Type -> Type

  Inteface for converting an Idris value from a row in a table.

Parameters: a
Constructor: 

MkFromRow

Methods:

fromRowTypes : List SqliteType

fromRow : LAll (Maybe . IdrisType) fromRowTypes -> Either SqlError a

Implementations:

Query t => FromRow t

FromCell a => FromRow a

LAll (FromRow . f) ts => FromRow (LAll f ts)

FromRow a => FromRow (Vect n a)

fromRowTypes : FromRow a => List SqliteType

Totality: total
Visibility: public export

fromRow : {auto __con : FromRow a} -> LAll (Maybe . IdrisType) fromRowTypes -> Either SqlError a

Totality: total
Visibility: public export

FromRowTypes : (0 a : Type) -> FromRow a => List SqliteType

  Utility alias for `fromRowTypes` with an explicit erased type argument.

Totality: total
Visibility: public export

FromRowsTypes : LAll (FromRow . f) ts -> List SqliteType

  List of SQLite types we require to read a sequence of
  several values with a `FromRow` implementation.

Totality: total
Visibility: public export

FromRowsTypesN : Nat -> FromRow a -> List SqliteType

  We can also convert a row of values to a vector of values.
  
  This function computes the types we need.

Totality: total
Visibility: public export

interface ToRow : Type -> Type

  Inteface for converting an Idris value from a row in a table.

Parameters: a
Constructor: 

MkToRow

Methods:

toRowTypes : List SqliteType

toRow : a -> LAll (Maybe . IdrisType) toRowTypes

Implementations:

ToCell a => ToRow a

LAll (ToRow . f) ts => ToRow (LAll f ts)

ToRow a => ToRow (Vect n a)

toRowTypes : ToRow a => List SqliteType

Totality: total
Visibility: public export

toRow : {auto __con : ToRow a} -> a -> LAll (Maybe . IdrisType) toRowTypes

Totality: total
Visibility: public export

ToRowTypes : (0 a : Type) -> ToRow a => List SqliteType

  Utility alias for `fromRowTypes` with an explicit erased type argument.

Totality: total
Visibility: public export

ToRowsTypes : LAll (ToRow . f) ts -> List SqliteType

  List of SQLite types we require to read a sequence of
  several values with a `ToRow` implementation.

Totality: total
Visibility: public export

ToRowsTypesN : Nat -> ToRow a -> List SqliteType

  We can also convert a vector of values to a (flat) row of values.
  
  This function computes the types we need.

Totality: total
Visibility: public export

Concat : List (List a) -> List a

  List concatenation specialized to behave nicely during unification.

Totality: total
Visibility: public export

splitAll : (v : List (List a)) -> LAll f (Concat v) -> LAll (LAll f) v

  Generalization of `Data.List.Quantifiers.splitAt`, to split a
  heterogeneous list based on a list of lists of its indices.

Totality: total
Visibility: public export