module Query where

open import Data.Pair
open import Data.Bool
open import Data.String
open import Data.List
open import Data.Vec
open import Data.Function
import Data.Dictionary

open import Schema
open import Universe

open Data.Dictionary {String} _==_

data ExprType : Set where
  bool  : ExprType
  ftype : FieldType -> ExprType

-- Exercise: add more interesting expressions.
-- For instance, less than or greater than comparisons. Look at the SQL documentation for ideas.
data Expr (t : TableType) : ExprType -> Set where
  _===_ : forall {a} -> Expr t a -> Expr t a -> Expr t bool
  !_    : forall x {p : HasKey x t} -> Expr t (ftype (lookup x t {p}))
  val   : forall {a} -> Field a -> Expr t (ftype a)

-- Exercise: add more interesting queries. For instance,
-- 1. Make it possible to rename fields to allow combining tables with overlapping column names.
-- 2. SQL supports counting and ordering results. Add this to our queries.

data Query (s : Schema) : TableType -> Set where
  read   : (x : TableName){p : HasKey x s} -> Query s (lookup x s {p})
  _⊗_    : forall {t t'}{p : Disjoint t t'} ->
           Query s t -> Query s t' -> Query s (t ++ t')
  proj   : forall {t} xs {p : HasKeys xs t} ->
           Query s t -> Query s (project xs t {p})
  select : forall {t} -> Expr t bool -> Query s t -> Query s t

-- This might have to be changed when you add more interesting queries.

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

sepBy : String -> List String -> String
sepBy _ [] = ""
sepBy _ (x :: []) = x
sepBy i (x :: xs) = x +++ i +++ sepBy i xs

showField : forall {a} -> Field a -> String
showField {string _} s = "'" +++ listToString (vecToList s) +++ "'"  -- TODO: escaping
showField {number} n = show n

showRow : forall {t} -> Row t -> String
showRow []        = ""
showRow (_::_ {name = name} x []) = name +++ " = " +++ showField x
showRow (_::_ {name = name} x xs) = name +++ " = " +++ showField x +++ ", " +++ showRow xs

showExpr : forall {t a} -> Expr t a -> String
showExpr (e₁ === e₂) = showExpr e₁ +++ " = " +++ showExpr e₂ 
showExpr (! x) = x
showExpr (val c) = showField c

showSQL : SQL -> String
showSQL (SELECT as FROM ts WHERE cs) =
  "SELECT " +++ sepBy ", " as +++ " FROM " +++ sepBy ", " ts +++
  " WHERE " +++ sepBy " AND " cs

toSQL : forall {s t} -> Query s t -> SQL
toSQL {s} (read x {p}) = SELECT (map fst (lookup x s {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