-- The interface against the Haskell Firebird library.

module Firebird where

open import Data.List
open import Data.String
open import Data.Integer
open import Data.Maybe
open import Data.Unit
open import Foreign.IO

{-# IMPORT Database.Firebird #-}

data HsField : Set where
  fString : String -> HsField
  fNumber : Integer -> HsField
  fDate   : (y m d : Integer) -> HsField
  fTime   : (h m s ms : Integer) -> HsField

{-# COMPILED_DATA HsField Field FString FNumber FDate FTime #-}

data HsFieldType : Set where
  text    : Integer -> HsFieldType
  varText : Integer -> HsFieldType
  short   : HsFieldType
  long    : HsFieldType
  date    : HsFieldType
  time    : HsFieldType

{-# COMPILED_DATA HsFieldType FieldType Text VarText Short Long Date Time #-}

data HsColInfo : Set where
  hsColInfo : String -> HsFieldType -> HsColInfo

{-# COMPILED_DATA HsColInfo ColumnInfo ColInfo #-}

HsTableInfo = List HsColInfo
HsRow       = List HsField

private
  FileName = String
  UserName = String
  Password = String
  TableName = String

postulate
  RawHandle    : Set
  hsConnect    : FileName -> UserName -> Password -> IO (Maybe RawHandle)
  hsDisconnect : RawHandle -> IO Unit
  hsStatement  : RawHandle -> String -> IO Unit
  hsQuery      : RawHandle -> String -> IO (List HsRow)
  hsTableInfo  : RawHandle -> TableName -> IO HsTableInfo

{-# COMPILED_TYPE RawHandle DbHandle #-}

{-# COMPILED hsConnect dbConnect #-}
{-# COMPILED hsDisconnect dbDisconnect #-}
{-# COMPILED hsStatement sqlStatement #-}
{-# COMPILED hsQuery sqlQuery #-}
{-# COMPILED hsTableInfo tableInfo #-}