module Orn.Ornament.Examples.Fin where

open import Function

open import Data.Empty
open import Data.Unit
open import Data.Nat
open import Data.Fin hiding (lift) renaming (zero to zeF ; suc to suF )
open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Logic.Logic

open import IDesc.IDesc
open import IDesc.Fixpoint

open import IDesc.Examples.Nat

open import Orn.Ornament

u : ℕ → ⊤
u _ = tt

module Constraint where

  -- Paper: Example 4.8

  FinO : orn NatD u u
  FinO = orn.mk λ n → 
         `σ (λ { zeF → insert ℕ λ m →
                        insert (suc m ≡ n) λ _ → 
                        `1
               ; (suF zeF) → insert ℕ λ m → 
                              insert (suc m ≡ n) λ _ → 
                              `var (inv m) 
               ; (suF (suF ())) })

  Fin' : ℕ → Set
  Fin' = μ ⟦ FinO ⟧orn 
  
  fz : ∀{n} → Fin' (suc n)
  fz {n} = ⟨ zeF , n , refl , tt ⟩
  
  fs : ∀{n} → Fin' n → Fin' (suc n)
  fs {n} k = ⟨ suF zeF , n , refl , k ⟩

  -- Paper: Example 4.18
  forgetFin : ∀{n} → Fin' n → Nat
  forgetFin = forget
    where open import Orn.Ornament.Algebra FinO

module Compute where

  FinO : orn NatD u u
  FinO = orn.mk λ { zero → insert ⊥ ⊥-elim
                  ; (suc n) → 
                    `σ λ { zeF → `1
                  ; (suF zeF) → `var (inv n) 
                  ; (suF (suF ())) } }

  Fin' : ℕ → Set
  Fin' = μ ⟦ FinO ⟧orn 
  
  fz : ∀{n} → Fin' (suc n)
  fz {n} = ⟨ zeF , tt ⟩
  
  fs : ∀{n} → Fin' n → Fin' (suc n)
  fs {n} k = ⟨ suF zeF , k ⟩