module Uniform.InitialPleasingAgda where

open import Prelude.Basic
open import Prelude.Fam

open import Uniform.IR

-- formation and introduction rules


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

  mutual

    -- specialised variants so that Agda can see that U is strictly
    -- positive and T terminating
    ⟦_⟧Uni' : (G : Uni D)-> Set
    ⟦ ι ⟧Uni' = ⊤
    ⟦ σ G S ⟧Uni' = Σ (⟦ G ⟧Uni') (S ∘ ⟦ G ⟧Info')
    ⟦ δ G S ⟧Uni' = Σ[ x ∈ (⟦ G ⟧Uni')] (S (⟦ G ⟧Info' x) -> U)

    ⟦_⟧Info' : (c : Uni D)-> ⟦ c ⟧Uni' -> Info c
    ⟦ ι ⟧Info' _ = lift tt
    ⟦ σ G S ⟧Info' (x , a) = (⟦ G ⟧Info' x , a)
    ⟦ δ G S ⟧Info' (x , g) = (⟦ G ⟧Info' x , (λ x → T (g x)))

    data U  : Set where
      intro : ⟦ (proj₁ c) ⟧Uni' -> U

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

-- Elimination rules

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

  IH : ∀ {a} -> (c' : Uni D) ->
       (P : U {c = c} -> Set a) -> ⟦_⟧Uni' {c = c} c' -> Set a
  IH ι P _ = Lift ⊤
  IH (σ d A) P (x , a) = IH d P x
  IH (δ d A) P (x , h)
     = Σ[ y ∈ (IH d P x) ] ((a : A (⟦ d ⟧Info' x)) -> P (h a))

  mutual

    elim : ∀ {a}(P : U -> Set a) ->
           (step : (x : ⟦ proj₁ c ⟧Uni') -> 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)

    -- specialised version of mapIH to make Agda see that elim is
    -- terminating
    mapIH' : ∀ {a}(c' : Uni D) ->
            (P : U -> Set a)  ->
            (step : (x : ⟦ proj₁ c ⟧Uni') -> IH (proj₁ c) P x -> P (intro x)) ->
            (x : ⟦ c' ⟧Uni') -> IH c' P x
    mapIH' ι P step _ = lift tt
    mapIH' (σ c A) P step (x , a) = mapIH' c P step x
    mapIH' (δ c A) P step (x , h)
       = (mapIH' c P step x , (λ a → elim P step (h a)))