module Orn.Reornament.Examples.Iterative (A B C : Set) where



open import Data.Unit
open import Data.Nat
open import Data.Bool
open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Level renaming (zero to zeroL ; suc to sucL)

open import Logic.Logic
open import Logic.IProp
open Logic.IProp.Applicative {zeroL}

open import IDesc.IDesc
open import IDesc.Fixpoint

open import Orn.Ornament
open import Orn.Reornament

-- Paper: Remark 4.33

test : func  
test = mk  x   A  a  
                  B λ b  
                  Bool λ x  
                 `var tt))

forget :   
forget n = tt

testO : orn test forget forget
testO = mk  n    a  
                  insert C  c  
                    b  
                  deleteΣ true 
                         (`var (inv (ℕ.suc n)))))))

postulate 
  a : A
  b : B
  c : C
  n : 
  x : Bool
  xs : μ test tt

reorn1 : orn  testO ⟧orn proj₁ proj₁
reorn1 =  testO 

reorn1O : Orn proj₁ (func.out  testO ⟧orn n)
reorn1O = orn.out reorn1 (n ,  a ,  _  x , xs) )

{-
 reorn1 (n , ⟨ a , (λ _ → x , xs) ⟩ )  ↝ 
     deleteΣ a
       (`Σ (λ c →
        `Π (λ b →
          insert (x ≡ true) (λ q →
          `var (inv (ℕ.suc n , xs))))))
-}

reorn2 : orn  reorn1 ⟧orn proj₁ proj₁
reorn2 =  reorn1 

postulate
  a' : A
  xs⁺ : μ  testO ⟧orn (ℕ.suc n)

reorn2O : Orn proj₁ (func.out  reorn1 ⟧orn (n ,  a ,  _  x , xs) ))
reorn2O = orn.out reorn2 ((n ,  a ,  _  x , xs) ) ,  a' , c ,  _  xs⁺) )

{-
 reorn2 ((n , ⟨ a , (λ _ → x , xs) ⟩) , ⟨ a , c , (λ _ → xs⁺) ⟩ ) ↝
     insert (a' ≡ a) (λ qa →
     deleteΣ c
       (`Π (λ b →
        `Σ (λ qx →
          `var (inv ((ℕ.suc n , xs) , xs⁺ b))))))
-}

reorn3 : orn  reorn2 ⟧orn proj₁ proj₁
reorn3 =  reorn2 

postulate 
  c' : C
  xs⁺⁺ : μ  reorn1 ⟧orn (ℕ.suc n , xs)

reorn3O : Orn proj₁  (func.out  reorn2 ⟧orn ((n ,  a ,  _  true , xs) ) ,  (a , (c ,  _  xs⁺))) ))
reorn3O = orn.out reorn3 (((n ,  a ,  _  true , xs) ) ,  a , c ,  _  xs⁺) ) ,  (c' ,  b  refl , xs⁺⁺)) )

{-
 reorn3 (((n , ⟨ a , (λ _ → true , xs) ⟩) , ⟨ a , c , (λ _ → xs⁺) ⟩ ) , ⟨ c' , λ b → refl , xs⁺⁺ ⟩ ) ↝
    `Σ (λ q₁ →
    insert (c' ≡ c) (λ q₂ →
    `Π (λ b →
    deleteΣ refl 
     (`var (inv (((ℕ.suc n , xs) , xs⁺ b , xs⁺⁺ b)))))))
-}


lemma : ∀{i₁ i₂ i₃ i₄}  (x y : μ  reorn3 ⟧orn (((i₁ , i₂) , i₃) , i₄))   x  y
lemma {i₂ =  i₂₁ , i₂₂ }
      { .i₂₁ , i₄₁ , i₃₃ } 
      { .i₄₁ , i₄₂ } 
       refl , refl , x  
       refl , refl , y  = cong  x   refl , refl , x ) <$>
                                 extensionality  b  lemma (x b) (y b))