-- Two fun examples of generic programming using univalence

module Cubical.Experiments.Generic where

open import Agda.Builtin.String
open import Agda.Builtin.List

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence

open import Cubical.Data.Nat
open import Cubical.Data.Int
open import Cubical.Data.Prod

----------------------------------------------------------------------------
--
-- Dan Licata's example from slide 47 of:
-- http://dlicata.web.wesleyan.edu/pubs/l13jobtalk/l13jobtalk.pdf

There : Type₀ → Type₀
There X = List (ℕ × String × (X × ℕ))

Database : Type₀
Database = There (ℕ × ℕ)

us : Database
us = (  , "John"  , ( ,  ) , )
   ∷ (  , "Hugo"  , ( , ) , )
   ∷ ( , "James" , (  ,  ) , )
   ∷ ( , "Sayid" , (  , ) , )
   ∷ ( , "Jack"  , (  , ) , )
   ∷ ( , "Sun"   , ( ,  ) , )
   ∷ []

convert : Database → Database
convert d = transport (λ i → There (swapEq ℕ ℕ i)) d

-- Swap the dates of the American database to get the European format
eu : Database
eu = convert us

-- A sanity check
_ : us ≡ convert eu
_ = refl


----------------------------------------------------------------------------
--
-- Example inspired by:
--
-- Scrap Your Boilerplate: A Practical Design Pattern for Generic Programming
-- Ralf Lämmel & Simon Peyton Jones, TLDI'03

Address : Type₀
Address = String

Name : Type₀
Name = String

data Person : Type₀ where
  P : Name → Address → Person

data Salary (A : Type₀) : Type₀ where
  S : A → Salary A

data Employee (A : Type₀) : Type₀ where
  E : Person → Salary A → Employee A

Manager : Type₀ → Type₀
Manager A = Employee A

-- First test of "mutual"
mutual
  data Dept (A : Type₀) : Type₀ where
    D : Name → Manager A → List (SubUnit A) → Dept A

  data SubUnit (A : Type₀) : Type₀ where
    PU : Employee A → SubUnit A
    DU : Dept A → SubUnit A

data Company (A : Type₀) : Type₀ where
  C : List (Dept A) → Company A


-- A small example

anders : Employee ℤ
anders = E (P "Anders" "Pittsburgh") (S (pos ))

andrea : Employee ℤ
andrea = E (P "Andrea" "Copenhagen") (S (pos ))

andreas : Employee ℤ
andreas = E (P "Andreas" "Gothenburg") (S (pos ))

-- For now we have a small company
genCom : Company ℤ
genCom =
  C ( D "Research" andreas (PU anders ∷ PU andrea ∷ [])
    ∷ [])

-- Increase the salary for everyone by 1
incSalary : Company ℤ → Company ℤ
incSalary c = transport (λ i → Company (sucPathℤ i)) c

genCom1 : Company ℤ
genCom1 = incSalary genCom


-- Increase the salary more
incSalaryℕ : ℕ → Company ℤ → Company ℤ
incSalaryℕ n c = transport (λ i → Company (addEq n i)) c

genCom2 : Company ℤ
genCom2 = incSalaryℕ  genCom

genCom10 : Company ℤ
genCom10 = incSalaryℕ  genCom