{-# OPTIONS --rewriting #-}
open import Data.Product
open import Data.Unit.Polymorphic
open import Relation.Binary.PropositionalEquality

module small-IR-to-SPF
  (I : Set)
  where

  open import SPF I as SPF
  open import IR I as IR

  powfam : (I → Set) → Fam I
  powfam P = (Σ I P , proj₁)

  translate : IR → SPF
  translate (done d) = done d
  translate (non-ind A γ) = non-ind A λ x → translate (γ x)
  translate (ind A γ) = non-ind (A -> I) λ f → ind A f (translate (γ f))

  r : (γ : IR) → (P : I → Set) →
       Fam.idx (powfam (SPF.Arg (translate γ) P)) -> IR.Arg γ (powfam P)
  r (done d) P x = _
  r (non-ind A γ) P (j , a , x) = a , r (γ a) P (j , x)
  r (ind A γ) P (j , f , (g , x)) = (λ y → (f y , g y)) , r _ P (j , x)

  rT : (γ : IR) → (P : I → Set) →
       (x : Fam.idx (powfam (SPF.Arg (translate γ) P))) →
       Fam.fam (powfam (SPF.Arg (translate γ) P)) x ≡ Val γ (powfam P) (r γ P x)
  rT (done d) P (d , refl) = refl
  rT (non-ind A γ) P (j , a , x) = rT (γ a) P (j , x)
  rT (ind A γ) P (j , f , g , x) = rT _ P (j , x)

  r-morphism : (γ : IR) → (P : I → Set) →
                FamMorphism (powfam (SPF.Arg (translate γ) P))
                            (ArgVal γ (powfam P))
  r-morphism γ P = (r γ P , rT γ P)


  l : (γ : IR) → (P : I → Set) →
       IR.Arg γ (powfam P) → Fam.idx (powfam (SPF.Arg (translate γ) P))
  l (done d) P _ = (d , refl)
  l (non-ind A γ) P (a , x) = let (j , y) = l (γ a) P x in j , (a , y)
  l (ind A γ) P (g , x) = let (j , y) = l (γ _) P x
                           in j , (λ a → proj₁ (g a)) , (λ a → proj₂ (g a)) , y

  lT : (γ : IR) → (P : I → Set) → (x : IR.Arg γ (powfam P)) →
       Val γ (powfam P) x ≡ Fam.fam (powfam (SPF.Arg (translate γ) P)) (l γ P x)
  lT (done d) P x = refl
  lT (non-ind A γ) P (a , x) = lT (γ a) P x
  lT (ind A γ) P (g , x) = lT (γ _) P x

  l-morphism : (γ : IR) → (P : I → Set) →
                FamMorphism (ArgVal γ (powfam P))
                            (powfam (SPF.Arg (translate γ) P))
  l-morphism γ P = (l γ P , lT γ P)


  -- roundtrips
  lr : (γ : IR) → {P : I → Set} →
         (x : Fam.idx (powfam (SPF.Arg (translate γ) P))) →
         l γ P (r γ P x) ≡ x
  lr (done d) (d , refl) = refl
  lr (non-ind A γ) (j , a , x) rewrite lr (γ a) (j , x) = refl
  lr (ind A γ) (j , f , g , x) rewrite lr (γ _) (j , x) = refl

  rl : (γ : IR) → {P : I → Set} →
         (x : IR.Arg γ (powfam P)) →
         r γ P (l γ P x) ≡ x
  rl (done d) x = refl
  rl (non-ind A γ) (a , x) rewrite rl (γ a) x = refl
  rl (ind A γ) (g , x) rewrite rl (γ _) x = refl