open import Level
open import Data.Maybe
open import Data.Sum
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import Relation.Nullary
open import Relation.Nullary.Decidable


private
  isJust' :  {} {t : Set }  (x : t)  (Maybe.just x)  nothing  
  isJust' x ()

  isJust :  {} {t : Set }  (y : Maybe t)  Dec ( λ x  just x  y)
  isJust (just x) = yes (x , refl)
  isJust nothing = no λ k  isJust' _ (proj₂ k)

-- simple class to initiate search. nothing particularly interesting
record Search {ℓ₁ ℓ₂} (t₁ : Set ℓ₁) (t₂ : t₁  Set ℓ₂) : Set (ℓ₁  ℓ₂) where
  field
    try : (x : t₁)  Maybe (t₂ x)

  # :  x  {p : True (isJust (try x))}  (t₂ x)
  # x {p} = proj₁ (toWitness p)

open Search {{...}} using (#) public


-- Kabbalah
record Projection {ℓ₁ ℓ₂ ℓ'} {t : Set ℓ₁} {f : t  Set ℓ₂} (_●_ :  (x : t)  f x  Set ℓ') (x : t) (x' : f x) : Set ℓ' where
  field
    proj : x  x'

open Projection


infix 0 _⟫>_
_⟫>_ :  {ℓ₁ ℓ₂}  _
_⟫>_ {ℓ₁} {ℓ₂} = Projection λ (a : Set ℓ₁) (b : a  Set ℓ₂)  (x : _)  b x


instance
  -- by complete coincidence, there are 10 pieces that comprise our "projection" metastructure

  ×-Left :  {ℓ₁ ℓ₂} {t₁ : Set ℓ₁} {t₂ : t₁  Set ℓ₂}   t₂ ⟫> t₂  proj₁
  ×-Left = record { proj = proj₂ }

  ×-Right :  {ℓ₁ ℓ₂} {t₁ : Set ℓ₁} {t₂ : t₁  Set ℓ₂}   t₂ ⟫> const t₁
  ×-Right = record { proj = proj₁ }

  ×-RLeft :  {ℓ₁ ℓ₂ ℓ₃} {t₁ : Set ℓ₁} {t₂ : Set ℓ₂} {t : t₁  Set ℓ₃}  t₁ ⟫> t  t₁ × t₂ ⟫> t  proj₁
  ×-RLeft i = record { proj = proj i  proj₁ }

  ×-RRight :  {ℓ₁ ℓ₂ ℓ₃} {t₁ : Set ℓ₁} {t₂ : t₁  Set ℓ₂} {t :  {x}  t₂ x  Set ℓ₃}  (∀ {x}  t₂ x ⟫> t)   t₂ ⟫> t  proj₂
  ×-RRight i = record { proj = proj i  proj₂ }

  ×-build :  {ℓ₁ ℓ₂ } {t : Set } {t₁ : t  Set ℓ₁} {t₂ : t  Set ℓ₂}  t ⟫> t₁  t ⟫> t₂  t ⟫> λ x  t₁ x × t₂ x
  ×-build i j = record { proj = λ x  proj i x , proj j x }

  ⊎-Left :  {ℓ₁ ℓ₂} {t₁ : Set ℓ₁} {t₂ : Set ℓ₂}  t₁ ⟫> const (t₁  t₂)
  ⊎-Left = record { proj = inj₁ }

  ⊎-Right :  {ℓ₁ ℓ₂} {t₁ : Set ℓ₁} {t₂ : Set ℓ₂}  t₂ ⟫> const (t₁  t₂)
  ⊎-Right = record { proj = inj₂ }

  ⊎-RRight :  {ℓ₁ ℓ₂ } {t : Set } {t₁ : t  Set ℓ₁} {t₂ : Set ℓ₂}  t ⟫> t₁  t ⟫> λ x  t₁ x  t₂ -- overlaps with ⊎-Right
  ⊎-RRight i = record { proj = inj₁  proj i }

  ⊎-RLeft :  {ℓ₁ ℓ₂ } {t : Set } {t₁ : Set ℓ₁} {t₂ : t  Set ℓ₂}  t ⟫> t₂  t ⟫> λ x  t₁  t₂ x -- overlaps with ⊎-Left
  ⊎-RLeft i = record { proj = inj₂  proj i }

  ⊎-build :  {ℓ₁ ℓ₂ } {t₁ : Set ℓ₁} {t₂ : Set ℓ₂} {t : t₁  t₂  Set }  t₁ ⟫> t  inj₁  t₂ ⟫> t  inj₂  t₁  t₂ ⟫> t
  ⊎-build {t = t} i j = record { proj = λ where
      (inj₁ x)  proj i x
      (inj₂ x)  proj j x
    }



  projectionSearch :  {ℓ₁ ℓ₂} {t : Set ℓ₁} {t₂ : t  Set ℓ₂}  t ⟫> t₂  Search t t₂
  projectionSearch i = record { try = just  proj i }


------------------
--   Examples   --
------------------

-- universe polymorphism is fully supported, but it's
-- elided in all but the first example for visual clarify

private
  -- move a value into the left
  _ :  {ℓ₁ ℓ₂} {t₁ : Set ℓ₁} {t₂ : Set ℓ₂}  t₁  t₁  t₂
  _ = λ x  # x

  -- move a value into the right
  _ :  {a b : Set}  a  b  a
  _ = λ x  # x

  -- move a value into some exotic combination of sums
  _ :  {a b c d e f g : Set}  a  ((c  b)  f)  (g  a  d)  e
  _ = λ x  # x

  -- project a value from the left
  _ :  {a b : Set}  a × b  a
  _ = λ x  # x

  -- project a value from the right
  _ :  {a b : Set}  a × b  b
  _ = λ x  # x

  -- project a value from some exotic combination of products
  _ :  {a b c d e f g : Set}  ((c × b) × f) × (g × a × d) × e  a
  _ = λ x  # x

  -- project a value from a sum of products
  _ :  {a b c : Set}  a × c  c × b  c
  _ = λ x  # x

  -- project a value from an exotic combination of sums and products
  _ :  {a b c d e f g : Set}  e × a × (d × f)  g × d × b  d
  _ = λ x  # x

  -- project out multiple values
  _ :  {a b c d : Set}  (a × b) × (c × d)  b × c
  _ = λ x  # x

  -- project out a unique sum
  _ :  {a b c d : Set}  a × b  c × d  a  c
  _ = λ x  # x



-- food for further meditation...
instance
  equality :  {} {t : Set }  t ⟫> λ x  x  x
  equality = record { proj = λ _  refl }

_ :  {t : Set}  (x : t)  x  x
_ = λ x  # x


-- and DEFINITELY not possible.....
-- _ : ∀ {a b : Set} → (a → b) × a → b
-- _ = λ x → # x