module Main where

open import Data.Function
open import Data.List
open import Data.Pair
open import Data.Unit
open import Data.Maybe
open import Foreign.IO
import Control.Monad
open Control.Monad returnIO bindIO

open import Database
open import Query
open import Schema
open import Universe
open import ExampleDatabase

queryType : forall {s t} -> Query s t -> TableType
queryType {t = t} _ = t

-- Query to find the computing science students.
q : Query universitySchema _
q =
  proj ("SNAME" :: [])
       (select (! "BPROGRAM" === val (padString "Computing Science"))
       (select (! "BID" === ! "SBRANCH")
               (read "Students" ⊗ read "Branches")
       ))

-- Exercise: write some more interesting queries.

main : IO Unit
main =
  connect "university.fdb" "sysdba" "masterkey" universitySchema >>= \mh ->
  withMaybe mh (putStrLn "Connection failed") \h ->
  putStrLn "Ok" >>
  query h q >>= \rows ->
  putStrLn "Query result:" >>
  mapM₋ (putStrLn ∘ showRow) rows >>
  disconnect h