module Conversion where

open import Data.String
open import Data.Pair
open import Data.List
open import Data.Nat
open import Data.Maybe
open import Data.Integer
open import Logic.Id

open import Schema
open import Firebird

open MonadMaybe

{-# IMPORT Database.Firebird #-}

P = Maybe

fail : {A : Set} -> P A
fail = nothing

-- Exercise: use the Either monad (Data.Either) instead of Maybe to get error messages.

-- Converting the Haskell representation to our representation

parseFieldType : HsFieldType -> P FieldType
parseFieldType (text n)    = return (string (intToNat n))
parseFieldType (varText n) = return (string (intToNat n))
parseFieldType short = return number
parseFieldType long = return number
parseFieldType date = fail 
parseFieldType time = fail 

parseColInfo : HsColInfo -> P Attribute
parseColInfo (hsColInfo name t) = parseFieldType t >>= \t -> return (name , t)

parseTableInfo : HsTableInfo -> P TableType
parseTableInfo xs = mapM parseColInfo xs

compareNat : (n m : Nat) -> Maybe (n == m)
compareNat zero zero = just refl
compareNat zero (suc n) = nothing
compareNat (suc n) zero = nothing 
compareNat (suc n) (suc m) with compareNat n m
compareNat (suc n) (suc m) | nothing = nothing
compareNat (suc .m) (suc m) | just refl = just refl 

parseField : {t : FieldType} -> HsField -> P (Field t)
parseField {string n} (fString s) with compareNat n (strLen s)
parseField {string n} (fString s)  | nothing   = fail
parseField {string ._} (fString s) | just refl = return (vString s) 
parseField {string n} (fNumber m) = fail
parseField {string n} (fDate y m d) = fail 
parseField {string n} (fTime h m s ms) = fail 
parseField {number} (fString _) = fail 
parseField {number} (fNumber n) = return (intToNat n)
parseField {number} (fDate _ _ _) = fail
parseField {number} (fTime _ _ _ _) = fail

parseRow : {t : TableType} -> HsRow -> P (Row t)
parseRow {[]} [] = return []
parseRow {(_ , t) :: ts} (x :: xs) =
  parseField x >>= \y ->
  parseRow xs  >>= \ys ->
  return (y :: ys)
parseRow _ = fail

parseRows : {t : TableType} -> List HsRow -> P (List (Row t))
parseRows xs = mapM parseRow xs