module Query where

open import Data.Function
open import Data.Bool renaming (T to isTrue)
open import Data.Unit
open import Data.List hiding (and)
open import Data.Product hiding (map)
import IO.Primitive as IO
open IO using (IO)
open import Data.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 0 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 25 _⊗_

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 0 SELECT_FROM_WHERE_

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

infixr 40 _&_
_&_ = 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 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