module Database where

open import Data.Function
import IO.Primitive as IO
open IO using (IO)
open import Data.Maybe
import Data.List as List
open List hiding (mapM; sequence)
open import Data.Bool
open import Data.String as String renaming (_++_ to _&_)
open import Data.Product
open import Foreign.Haskell
open import Category.Monad
open import Category.Monad.Indexed

open import Util hiding (_<$>_)
open import Schema

MonadIO : RawMonad IO
MonadIO = record { return = IO.return
                 ; _>>=_  = IO._>>=_
                 }

open RawMonad MonadIO

{-# IMPORT Database.Firebird #-}

ServerName = String
UserName   = String
Password   = String

postulate
  RawHandle     : Set
  hs_connect    : ServerName → UserName → Password → IO (Maybe RawHandle)
  hs_tableInfo  : RawHandle → TableName → IO (List HsColumnInfo)
  hs_disconnect : RawHandle → IO Unit

{-# COMPILED_TYPE RawHandle DbHandle #-}

{-# COMPILED hs_connect dbConnect #-}
{-# COMPILED hs_tableInfo tableInfo #-}
{-# COMPILED hs_disconnect dbDisconnect #-}

data Db (s₁ s₂ : Schema)(A : Set) : Set where
  mkDb : (RawHandle → IO A) → Db s₁ s₂ A

unDb : ∀ {A s₁ s₂} → Db s₁ s₂ A → RawHandle → IO A
unDb (mkDb f) = f

MonadDb : RawIMonad Db
MonadDb = record
  { return = λ x → mkDb λ _ → return x
  ; _>>=_  = λ m f → mkDb λ h → unDb m h >>= λ x → unDb (f x) h
  }

open RawIMonad MonadDb using () renaming (return to return′; _>>=_ to _>>=′_; _>>_ to _>>′_)

liftIO : ∀ {A s} → IO A → Db s s A
liftIO io = mkDb λ h → io

data Handle (s : Schema) : Set where
  handle : RawHandle → Handle s

showType : FieldType → String
showType (string n) = primStringAppend "STRING " (showInteger (primNatToInteger n))
showType number     = "NUMBER"
showType date       = "DATE"
showType time       = "TIME"

mapM : ∀ {A B} → (A → IO B) → List A → IO (List B)
mapM f []       = return []
mapM f (x ∷ xs) = f x >>= λ y → mapM f xs >>= λ ys → return (y ∷ ys)

mapM₋ : ∀ {A B} → (A → IO B) → List A → IO Unit
mapM₋ f xs = mapM f xs >> return unit

putStr : String → IO Unit
putStr = IO.putStr ∘ fromColist ∘ String.toCostring

putStrLn : String → IO Unit
putStrLn = IO.putStrLn ∘ fromColist ∘ String.toCostring

printCol : Attribute → IO Unit
printCol (name , type) =
  mapM₋ putStr (name ∷ " : " ∷ showType type ∷ "\n" ∷ [])

printTableInfo : TableType → IO Unit
printTableInfo = mapM₋ printCol

checkTable : RawHandle → TableName × TableType → IO Bool
checkTable h (name , type) =
  hs_tableInfo h name >>= λ info →
  if parseTableInfo info =TT= type
  then return true
  else putStrLn ("Schema mismatch for table " & name) >>
       putStrLn "Expected:" >>
       printTableInfo type >>
       putStrLn "Found:" >>
       printTableInfo (parseTableInfo info) >>
       return false

checkSchema : RawHandle → Schema → IO Bool
checkSchema h s = 
  putStrLn "Checking schema..." >>
  and <$> mapM (checkTable h) s

withDatabase : ∀ {s′ A} → ServerName → UserName → Password →
               (s : Schema) → Db s s′ A → IO (Maybe A)
withDatabase server user pass s action =
  putStrLn ("Connecting to " & server & "...") >>
  hs_connect server user pass >>= λ mh →
  withMaybe mh (return nothing) λ h →
  checkSchema h s >>= λ ok →
  if ok then just <$> unDb action h >>= (λ x → hs_disconnect h >> return x)
        else return nothing

withRawHandle : ∀ {A s₁ s₂} → (RawHandle → Db s₁ s₂ A) → Db s₁ s₂ A
withRawHandle f = mkDb λ h → unDb (f h) h