module Main where
open import Data.Function
import IO.Primitive as IO
open IO using (IO)
open import Data.Maybe
open import Data.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")
q′ : Query universitySchema _
q′ = proj ("DNAME" ∷ []) (read "Departments")
badQ : Query universitySchema _
badQ = proj ("SNAME" ∷ [])
(select (! "SID" === K 0)
(read "Students")
)
main =
withDatabase "university.fdb" "sysdba" "masterkey" universitySchema $
query q >>= λ rows →
liftIO (putStrLn "Query result:") >>
liftIO (mapM₋ (putStrLn ∘ showRow) rows)