module Schema where

open import Data.Nat
open import Data.Bool
open import Data.List
open import Data.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 20)
      ("Time"  , time)
      ("Wet"   , number)
      []

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

infixr 40 _∷_
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 0 1 18 400
       0
       []