module Database where

-- Shamelessly ripped from David Christiansen's Talk @CurryOn'15
-- "Coding for Types: The Universe Pattern in Idris"

open import Data.List hiding (_++_)
open import Data.Nat
open import Data.Nat.Show renaming (show to showℕ)
open import Data.Product hiding (map)
open import Data.String

open import Function

-- cf. http://jozefg.bitbucket.org/posts/2013-12-24-favorite-dependent-types.html
data HList : List Set → Set₁ where
  [] : HList []
  _⟪_ : {A : Set}{xs : List Set} → A → HList xs → HList (A ∷ xs)

infixr 60 _⟪_

data Column : Set where
  TEXT : Column
  NAT : Column
 
⟦_⟧ : Column → Set
⟦ TEXT ⟧ = String
⟦ NAT ⟧ = ℕ

Schema : Set
Schema = List (String × Column)

⟦_⟧ₛ : Schema → Set₁
⟦ s ⟧ₛ = HList (map (⟦_⟧ ∘ proj₂) s)

ScoreSchema : Schema
ScoreSchema = ("Name" , TEXT) ∷ ("Score" , NAT) ∷ []

ScoreSchema' : Schema
ScoreSchema' = ("fst" , TEXT) ∷ ("snd" , NAT) ∷ []

DB : Schema → Set₁
DB = List ∘ ⟦_⟧ₛ

Highscores : DB ScoreSchema
Highscores = ("Ingo" ⟪ 15 ⟪ []) ∷ ("Cai" ⟪ 9001 ⟪ []) ∷ []

Highscores' : DB ScoreSchema'
Highscores' = Highscores

totalScore : DB ScoreSchema → ℕ
totalScore [] = 0
totalScore (_ ⟪ score ⟪ [] ∷ xs) = score + totalScore xs

header : Schema → String
header [] = ""
header ((label , _) ∷ t) = label ++ "\t" ++ header t

showCol : {c : Column} → ⟦ c ⟧ → String
showCol {TEXT} s = s
showCol {NAT} n = showℕ n

showRow : {s : Schema} → ⟦ s ⟧ₛ → String
showRow {[]} x = "\n"
showRow {_ ∷ _} (x ⟪ xs) = showCol x ++ "\t" ++ showRow xs

showDatabase : {s : Schema} → DB s → String
showDatabase {s} xs = header s ++ "\n" ++ foldr _++_ "" (map showRow xs)

dumpSchema : {s : Schema} → DB s → Schema
dumpSchema {s} db = s