module Schema where

open import Data.Bool
open import Data.String
open import Data.Nat
open import Data.List
open import Data.Pair
open import Data.Vec

TableName = String
FieldName = String

-- Exercise: The Haskell library supports date and time values. Add those here.

data FieldType : Set where
  string : Nat -> FieldType
  number : FieldType

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

Field : FieldType -> Set
Field (string n) = Vec Char n
Field number     = Nat

data Row : TableType -> Set where
  []   : Row []
  _::_ : forall {name ft tt} ->
         Field ft -> Row tt -> Row ((name , ft) :: tt)

-- Converting a string to a vector
vString : (s : String) -> Vec Char (strLen s)
vString s = listToVec (stringToList s)

padString : {n : Nat}(s : String){p : isTrue (strLen s ≤ n)} -> Vec Char n
padString s {p} = padListToVec ' ' (stringToList s) {p}