-- See Polynomial.InitialPleasingAgda for a version of this file not bypassing
-- the positivity and termination checkers

module Polynomial.Initial 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

    {-# NO_POSITIVITY_CHECK #-}
    data U  : Set where
      intro : ⟦ c ⟧₀ (U , T) -> U

    {-# TERMINATING #-}
    T : U -> D
    T (intro x) = ⟦ c ⟧₁ (U , T) x

-- Elimination rules

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

mapIH : ∀ {a}{D : Set1}(c : Poly D){Z : Fam D} ->
        (P : ind Z -> Set a) -> (g : (x : ind Z) -> P x) ->
        (x : Node c Z) -> IH c P x
mapIH idPN P g x = g x
mapIH (con A) P g a = lift tt
mapIH (sigma S T) P g (x , y) = mapIH S P g x , mapIH (T _) P g y
mapIH (pi A T) P g f = λ a → mapIH (T a) P g (f a)

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

  {-# TERMINATING #-}
  elim : ∀ {a}(P : U {D} {c} -> Set a) ->
         (step : (x : ⟦ c ⟧₀ (U , T)) -> IH (proj₁ c) P x -> P (intro x)) ->
         (x : U) -> P x
  elim P step (intro x) = step x (mapIH (proj₁ c) P (elim P step) x)