-- Two fun examples of generic programming using univalence

{-# OPTIONS --safe #-}
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