module Main where

open import Function
import IO.Primitive as IO
open IO using (IO)
open import Maybe
open import List
open import Data.Bool
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Category.Monad.Indexed

open import Schema
open import Database
open import Query
open import Util
open import BString

open import ExampleDatabase

open RawIMonad MonadDb hiding (_⊗_)

{-# IMPORT Database.Firebird #-}

queryType : ∀ {s t} → Query s t → TableType
queryType {t = t} _ = t

departmentPrograms : Query universitySchema _
departmentPrograms =
  proj ("PNAME" ∷ "ABBR" ∷ "DNAME" ∷ [])
  ( select (! "DPDEPARTMENT" === ! "DNAME")
  ( select (! "DPPROGRAM" === ! "PNAME")
    (read "Departments" ⊗ read "Programs" ⊗ read "DepartmentsPrograms")
  ))

studentsInDepartment : BString _ → Query universitySchema _
studentsInDepartment p =
  proj ("SNAME" ∷ "PNAME" ∷ [])
    ( select (! "SBRANCH"  === ! "BID")
    ( select (! "DNAME"    === K p)
    ( select (! "BPROGRAM" === ! "PNAME")
             (read "Students" ⊗ read "Branches" ⊗ departmentPrograms)
    )))

q : Query universitySchema _
q = studentsInDepartment (bString "Applied Mechanics")
  -- "Computer Science and Engineering")

q′ : Query universitySchema _
q′ = proj ("DNAME" ∷ []) (read "Departments")

badQ : Query universitySchema _
badQ = proj ("SNAME" ∷ [])
       (select (! "SID" === K )
         (read "Students")
       )

main =
  withDatabase "university.fdb" "sysdba" "masterkey" universitySchema $
    query q >>= λ rows →
    liftIO (putStrLn "Query result:") >>
    liftIO (mapM₋ (putStrLn ∘ showRow) rows)