module Polynomial.InitialPleasingAgda where

open import Function
open import Data.Product
open import Data.Unit
open import Level

open import Prelude.Fam
open import Polynomial.IR

-- formation and introduction rules

module _ {D : Set1}{c : IR D D} where

  mutual

    -- specialised variants so that Agda can see that U is strictly
    -- positive and T terminating
    Node' : Poly D -> Set
    Node' idPN = U
    Node' (con A) = A
    Node' (sigma S T) = Σ[ s ∈ Node' S ] Node' (T (info' S s))
    Node' (pi A T) = (x : A) -> Node' (T x)

    info' : (T : Poly D) -> Node' T -> Info T
    info' idPN x = T x
    info' (con A) a = lift a
    info' (sigma S T) (s , x) = info' S s , info' (T (info' S s)) x
    info' (pi A T) g = λ a → info' (T a) (g a)

    data U  : Set where
      intro : Node' (proj₁ c) -> U

    T : U -> D
    T (intro x) = (proj₂ c) (info' (proj₁ c) x)

-- Elimination rules

module _ {D : Set1}{c : IR D D} where

  IH : ∀ {a}(c' : Poly D) ->
       (P : U {c = c} -> Set a) -> Node' {c = c} c' -> Set a
  IH idPN P x = P x
  IH (con A) P a = Lift ⊤
  IH (sigma S T) P (x , y) = (IH S P x) × IH (T (info' S x)) P y
  IH (pi A T) P f = (a : A) -> IH (T a) P (f a)

  mutual

    elim : ∀ {a}(P : U {c = c} -> Set a) ->
           (step : (x : Node' (proj₁ c)) -> IH (proj₁ c) P x -> P (intro x)) ->
           (x : U) -> P x
    elim P step (intro x) = step x (mapIH (proj₁ c) P step x)


    mapIH : ∀ {a}(c' : Poly D) ->
            (P : U {c = c} -> Set a) ->
            (step : (x : Node' (proj₁ c)) -> IH (proj₁ c) P x -> P (intro x)) ->
            (x : Node' {c = c} c') -> IH c' P x
    mapIH idPN P step x = elim P step x
    mapIH (con A) P step a = lift tt
    mapIH (sigma S T) P step (x , y) = mapIH S P step x , mapIH (T _) P step y
    mapIH (pi A T) P step f = λ a → mapIH (T a) P step (f a)