module Schema where

open import Data.Nat
open import Data.Bool
open import List
open import Maybe
open import Data.Product hiding (map)
import Data.String as String
open String using (String)
open import Data.Char hiding (_==_)
open import Relation.Binary.PropositionalEquality

open import BString
open import Util
open import Eq

data FieldType : Set where
  string : ℕ → FieldType
  number : FieldType
  date   : FieldType
  time   : FieldType

TableName = String
FieldName = String
Attribute = FieldName × FieldType
TableType = List Attribute
Schema    = List (TableName × TableType)

_=FT=_ : FieldType → FieldType → Bool
string n =FT= string m = n == m
number   =FT= number   = true
date     =FT= date     = true
time     =FT= time     = true
_        =FT= _        = false

_=TT=_ : TableType → TableType → Bool
[]                 =TT= [] = true
((f₁ , t₁) ∷ tt₁)  =TT= ((f₂ , t₂) ∷ tt₂) =
  (f₁ == f₂) ∧ (t₁ =FT= t₂) ∧ (tt₁ =TT= tt₂) 
_ =TT= _ = false

record Date : Set where
  field
    year  : ℕ
    month : ℕ
    day   : ℕ

record Time : Set where
  field
    hour        : ℕ
    minute      : ℕ
    second      : ℕ
    millisecond : ℕ

mkDate : ℕ → ℕ → ℕ → Date
mkDate y m d = record { year = y; month = m; day = d }

mkTime : ℕ → ℕ → ℕ → ℕ → Time
mkTime h m s ms = record { hour = h; minute = m; second = s; millisecond = ms }

Field : FieldType → Set
Field (string n) = BList Char n
Field number     = ℕ
Field date       = Date
Field time       = Time

-- Haskell interface

{-# IMPORT Database.Firebird #-}

data HsFieldType : Set where
  text    : Integer → HsFieldType
  vartext : Integer → HsFieldType
  short   : HsFieldType
  long    : HsFieldType
  date    : HsFieldType
  time    : HsFieldType

{-# COMPILED_DATA HsFieldType FieldType Text VarText Short Long Date Time #-}

data HsColumnInfo : Set where
  colInfo : String → HsFieldType → HsColumnInfo

{-# COMPILED_DATA HsColumnInfo ColumnInfo ColInfo #-}

parseHsFieldType : HsFieldType → FieldType
parseHsFieldType (text n)    = string (primIntegerAbs n)
parseHsFieldType (vartext n) = string (primIntegerAbs n)
parseHsFieldType short       = number
parseHsFieldType long        = number
parseHsFieldType date        = date
parseHsFieldType time        = time

parseHsColumnInfo : HsColumnInfo → Attribute
parseHsColumnInfo (colInfo name type) = name , parseHsFieldType type

parseTableInfo : List HsColumnInfo → TableType
parseTableInfo = map parseHsColumnInfo

-- Example schema
Cars : TableType
Cars =  ("Model" , string )
     ∷ ("Time"  , time)
     ∷ ("Wet"   , number)
     ∷ []

Students : TableType
Students =
     ("Name"   , string )
  ∷ ("Passed" , number)
  ∷ []

infixr  _∷_
data Row : TableType → Set where
  []  : Row []
  _∷_ : forall {name ft schema} →
         Field ft → Row schema → Row ((name , ft) ∷ schema)

zonda : Row Cars
zonda = bString "Pagani Zonda C122 F"
      ∷ mkTime    
      ∷ 
      ∷ []