module Query where

open import Function
open import Data.Bool renaming (T to isTrue)
open import Data.Unit
open import List hiding (and)
open import Data.Product hiding (map)
import IO.Primitive as IO
open IO using (IO)
open import Maybe
import Data.String as String
open String using (String)
open import Relation.Binary.PropositionalEquality
open import Category.Monad.Indexed
open import Category.Monad

open import Eq
open import Schema
open import Util
open import BString
open import Database

open RawIMonad MonadDb hiding (_⊗_)
open RawMonad MonadIO using () renaming (_>>_ to _>>′_)

{-# IMPORT Database.Firebird #-}

infix  found_expectedOneOf_ theFields_appearInBoth_and_

data ErrorMsg : Set where
  found_expectedOneOf_        : String → List String → ErrorMsg
  theFields_appearInBoth_and_ : List String → List String → List String → ErrorMsg
  noError                     : ErrorMsg

Constraint = Bool × ErrorMsg

trivial : Constraint
trivial = true , noError

_&&_ : Constraint → Constraint → Constraint
(true  , _) && c = c
(false , e) && _ = false , e

_hasField_ : TableType → FieldName → Constraint
t hasField x = haskey x t , (found x expectedOneOf map proj₁ t)

_hasTable_ : Schema → TableName → Constraint
s hasTable t = haskey t s , (found t expectedOneOf map proj₁ s)

_hasFields_ : TableType → List FieldName → Constraint
t hasFields xs = foldr _&&_ trivial (map (_hasField_ t) xs)

disjoint : TableType → TableType → Constraint
disjoint s s' = all (λ x → not (elem x names')) names
              , (theFields filter (λ x → elem x names') names appearInBoth names and names')
  where
    names  = map proj₁ s
    names' = map proj₁ s'

data Error (e : ErrorMsg) : Set where

sat : Constraint → Set
sat (true  , _) = ⊤
sat (false , e) = Error e

trueConstr : ∀ {c} → sat c → isTrue (proj₁ c)
trueConstr {true  , _} p = p
trueConstr {false , _} ()

lookupField : (x : FieldName)(t : TableType) → sat (t hasField x) → FieldType
lookupField x t p = lookup' x t (trueConstr p)

lookupTable : (t : TableName)(s : Schema) → sat (s hasTable t) → TableType
lookupTable t s p = lookup' t s (trueConstr p)

{-
subschema : TableType → TableType → Bool
subschema [] s' = true
subschema ((name , ft) ∷ s) s' with lookup name s'
... | nothing  = false
... | just ft' = ft =FT= ft'
-}

sat-and₁ : ∀ {a b} → sat (a && b) → sat a
sat-and₁ {true  , _} p = _
sat-and₁ {false , _} ()

sat-and₂ : ∀ {a b} → sat (a && b) → sat b
sat-and₂ {true  , _} p = p
sat-and₂ {false , _} ()

subTable : (xs : List FieldName)(t : TableType) → sat (t hasFields xs) → TableType
subTable [] t _ = []
subTable (x ∷ xs) t p = (x , lookupField x t (sat-and₁ p)) ∷
                         subTable xs t (sat-and₂ {t hasField x} p)

data EType : Set where
  bool  : EType
  ftype : FieldType → EType

data Expr (t : TableType) : EType → Set where
  _===_ : ∀ {a} → Expr t a → Expr t a → Expr t bool
  !_    : ∀ x {p : sat (t hasField x)} → Expr t (ftype (lookupField x t p))
  K     : ∀ {a} → Field a → Expr t (ftype a)

infixr  _⊗_

data Query (s : Schema) : TableType → Set where
  read : ∀ (x : TableName){p : sat (s hasTable x)} →
         Query s (lookupTable x s p)
  _⊗_  : ∀ {t t'}{p : sat (disjoint t t')} →
         Query s t → Query s t' → Query s (t ++ t')
  proj : ∀ {t} xs {p : sat (t hasFields xs)} →
         Query s t → Query s (subTable xs t p)
  select : ∀ {t} → Expr t bool → Query s t → Query s t

infix  SELECT_FROM_WHERE_

data SQL : Set where
  SELECT_FROM_WHERE_ : List FieldName → List TableName → List String → SQL

infixr  _&_
_&_ = primStringAppend

sepBy : String → List String → String
sepBy _ [] = ""
sepBy _ (x ∷ []) = x
sepBy i (x ∷ xs) = x & i & sepBy i xs

showField : ∀ {a} → Field a → String
showField {string _} s = "'" & trim ' ' (unBString s) & "'"  -- TODO: escaping
showField {number} n = showNat n
showField {date} d = sepBy "-" (map showNat (Date.year d ∷ Date.month d ∷ Date.day d ∷ []))
showField {time} t = sepBy ":" (map showNat (Time.hour t ∷ Time.minute t ∷ Time.second t ∷ []))
                     & "." & showNat (Time.millisecond t)

showRow : ∀ {t} → Row t → String
showRow []        = ""
showRow (_∷_ {name = name} x []) = name & " = " & showField x
showRow (_∷_ {name = name} x xs) = name & " = " & showField x & ", " & showRow xs

showExpr : ∀ {t a} → Expr t a → String
showExpr (e₁ === e₂) = showExpr e₁ & " = " & showExpr e₂ 
showExpr (! x) = x
showExpr (K c) = showField c

showSQL : SQL → String
showSQL (SELECT as FROM ts WHERE cs) =
  "SELECT " & sepBy ", " as & " FROM " & sepBy ", " ts & whereClause cs
  where
    whereClause : List String → String
    whereClause [] = ""
    whereClause cs = " WHERE " & sepBy " AND " cs

toSQL : ∀ {s t} → Query s t → SQL
toSQL {s} (read x {p}) = SELECT (map proj₁ (lookup' x s (trueConstr p))) FROM x ∷ [] WHERE []
toSQL (q₁ ⊗ q₂) with toSQL q₁ | toSQL q₂
... | SELECT as₁ FROM ts₁ WHERE cs₁
    | SELECT as₂ FROM ts₂ WHERE cs₂ = SELECT as₁ ++ as₂ FROM nub (ts₁ ++ ts₂) WHERE cs₁ ++ cs₂ 
toSQL (proj as q) with toSQL q
... | SELECT _ FROM ts WHERE cs = SELECT as FROM ts WHERE cs
toSQL (select c q) with toSQL q
... | SELECT as FROM ts WHERE cs = SELECT as FROM ts WHERE showExpr c ∷ cs 

data HsField : Set where
  string : String → HsField
  number : Integer → HsField
  date   : (year month day : Integer) → HsField
  time   : (hour minute second millisecond : Integer) → HsField

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

HsRow = List HsField

postulate
  hs_query : RawHandle → String → IO (List HsRow)

{-# COMPILED hs_query sqlQuery #-}

parseHsField : ∀ {t} → HsField → Maybe (Field t)
parseHsField {string n} (string s) with inspect (strLen s =< n)
... | true  with-≡ p = just (bString s {istrue (sym p)})
... | false with-≡ _ = nothing
parseHsField {number} (number n)    = just (primIntegerAbs n)
parseHsField {date} (date y m d)    = just (mkDate (primIntegerAbs y)
                                                   (primIntegerAbs m)
                                                   (primIntegerAbs d)
                                           )
parseHsField {time} (time h m s ms) = just (mkTime (primIntegerAbs h)
                                                   (primIntegerAbs m)
                                                   (primIntegerAbs s)
                                                   (primIntegerAbs ms)
                                           )
parseHsField _ = nothing

parseHsRow : ∀ {t} → HsRow → Maybe (Row t)
parseHsRow {[]}            []        = just []
parseHsRow {(_ , t) ∷ ts} (x ∷ xs) =
  bindMaybe (parseHsField x) λ y →
  bindMaybe (parseHsRow xs) λ ys →
  just (y ∷ ys)
parseHsRow _ = nothing

parseHsRows : ∀ {t} → List HsRow → Maybe (List (Row t))
parseHsRows = mapMaybe parseHsRow

showHsField : HsField → String
showHsField (string s) = "'" & s & "'"
showHsField (number n) = showInteger n
showHsField (date y m d) = sepBy "-" (map showInteger (y ∷ m ∷ d ∷ []))
showHsField (time h m s ms) =
  sepBy ":" (map showInteger (h ∷ m ∷ s ∷ [])) & "." & showInteger ms

printHsRow = putStrLn ∘ sepBy ", " ∘ map showHsField
printHsRows = mapM₋ printHsRow

query : ∀ {s t} → Query s t → Db s s (List (Row t))
query q = withRawHandle λ h →
  let sql = showSQL (toSQL q) in
  liftIO (putStrLn ("query: " & sql)) >>
  liftIO (hs_query h sql) >>= λ hrows →
  withMaybe (parseHsRows hrows)
    (liftIO (putStrLn "Bad rows:" >>′ printHsRows hrows >>′ ioError "Bad rows")) 
      λ rows → return rows