-- The bookstore example (Figure 2).

module BiGUL.Bookstore where

open import BiGUL.Utilities
open import BiGUL.Partiality
open import BiGUL.Lens
open import BiGUL.Universe
open import BiGUL.BiGUL
open import BiGUL.ViewRearrangement

open import Function
open import Data.Product
open import Data.Sum
open import Data.Bool
open import Data.Maybe
open import Data.Nat
open import Data.Fin
open import Data.List
open import Data.String
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Binary.PropositionalEquality


kString : {n : ℕ} → U n
kString = k String Data.String._≟_

-- title, author, year, price, in stock
SBookU : {n : ℕ} → U n
SBookU = kString ⊗ (kString ⊗ (k ℕ Data.Nat._≟_ ⊗ (k ℕ Data.Nat._≟_ ⊗ k Bool Data.Bool._≟_)))

-- title, price
VBookU : {n : ℕ} → U n
VBookU = kString ⊗ k ℕ Data.Nat._≟_

emptyF : Functor 0
emptyF ()

emptyTEnv : Fin 0 → Set
emptyTEnv ()

bookstore : BiGUL emptyF (list SBookU) (list VBookU)
bookstore =
  align ((String × String × ℕ × ℕ × Bool → Par Bool) ∋
           (λ { (_ , _ , year , _ , instock) → return (⌊ year Data.Nat.≟ 2016 ⌋ ∧ instock) }))
        ((String × String × ℕ × ℕ × Bool → String × ℕ → Par Bool) ∋
           (λ { (stitle , _) (vtitle , _) → return (stitle == vtitle) }))
        (rearr (prod var var) (prod var (prod (k tt) (prod (k tt) (prod var (k tt))))) (inj₁ refl , tt , tt , inj₂ refl , tt)
               (update (prod var (prod var (prod var (prod var var))))
                       ((, replace) , (, skip) , (, skip) , (, replace) , (, skip))))
        (const (return ("" , "(to be updated)" , 2016 , 0 , true)))
        (λ { (title , author , year , price , instock) → return (just (title , author , year , price , false)) })

bookstore-CompleteExpr : BiGULCompleteExpr emptyF bookstore
bookstore-CompleteExpr = (return refl >>= return refl) , tt , tt , tt , tt , tt

sbooks : ⟦ list SBookU ⟧ emptyTEnv
sbooks = ("Harry Potter"             , "J. K. Rowling"     , 2016 , 950 , true) ∷
         ("The Lord of the Rings"    , "J. R. R. Tolkien"  , 1954 , 450 , true) ∷
         ("The Chronicles of Narnia" , "C. S. Lewis"       , 2016 , 650 , true) ∷ []

vbooks : ⟦ list VBookU ⟧ emptyTEnv
vbooks = ("Harry Potter" , 950) ∷ ("The Chronicles of Narnia" , 650) ∷ []

vbooks' : ⟦ list VBookU ⟧ emptyTEnv
vbooks' = ("Harry Potter" , 850) ∷ ("The Hitchhiker's Guide to the Galaxy" , 550) ∷ []

test-get : Maybe (⟦ list VBookU ⟧ emptyTEnv)
test-get = runPar (Lens.get (interp emptyF bookstore bookstore-CompleteExpr) sbooks)

test-put : Maybe (⟦ list SBookU ⟧ emptyTEnv)
test-put = runPar (Lens.put (interp emptyF bookstore bookstore-CompleteExpr) sbooks vbooks)

test-put' : Maybe (⟦ list SBookU ⟧ emptyTEnv)
test-put' = runPar (Lens.put (interp emptyF bookstore bookstore-CompleteExpr) sbooks vbooks')