module Orn.Ornament.Examples.Vec where

open import Function

open import Data.Empty
open import Data.Unit
open import Data.Nat
open import Data.Fin hiding (lift)
open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Logic.Logic


open import IDesc.IDesc
open import IDesc.Fixpoint


open import Orn.Ornament

u : ℕ → ⊤
u _ = tt

ListD : Set → func ⊤ ⊤
ListD A = func.mk λ _ → `Σ (Fin ) (λ { zero → `1 
                                      ; (suc zero) → `Σ A λ _ → `var tt 
                                      ; (suc (suc ())) })

module Constraint {A : Set} where

  VecO : orn (ListD A) u u
  VecO = orn.mk λ n → 
         `Σ {S = Fin }
             λ { zero → insert ( ≡ n) λ _ → 
                        `1
               ; (suc zero) → insert ℕ λ m → 
                              insert (suc m ≡ n) λ _ → 
                              `Σ λ _ →
                              `var (inv m) 
               ; (suc (suc ())) }

  Vec : ℕ → Set
  Vec = μ ⟦ VecO ⟧orn 
  
  nil : Vec 
  nil = ⟨ zero , refl , tt ⟩
  
  cons : ∀{n} → A → Vec n → Vec (suc n)
  cons {n} a xs = ⟨ suc zero , n , refl , a , xs  ⟩

module Compute {A : Set} where

  VecO : orn (ListD A) u u
  VecO = orn.mk λ { zero → insert (Fin ) λ { zero → deleteΣ zero `1
                                            ; (suc ()) }
                  ; (suc n) → insert (Fin ) λ { zero → deleteΣ (suc zero) (`Σ λ _ → `var (inv n)) 
                                               ; (suc ()) } }

  Vec : ℕ → Set
  Vec = μ ⟦ VecO ⟧orn 
  
  nil : Vec 
  nil = ⟨ zero , tt ⟩

  cons : ∀{n} → A → Vec n → Vec (suc n)
  cons a xs = ⟨ zero , a , xs ⟩