{-# OPTIONS --cubical --safe #-}

module Data.Array.Skew where

open import Prelude
open import Data.Binary.Skew
open import Data.List
open import Data.Nat using (_+_)

private
  variable
    p : Level
    P : β„• β†’ Type p
    n : β„•
    ns : 𝔹

infixl 6 _βˆ”_
_βˆ”_ : β„• β†’ β„• β†’ β„•
zero  βˆ” m = m
suc n βˆ” m = n βˆ” suc m

infixl 4 _βŠ•_
_βŠ•_ : (β„• β†’ Type p) β†’ β„• β†’ β„• β†’ Type p
_βŠ•_ P n m = P (n βˆ” m)

data Spine⁺ {p} (P : β„• β†’ Type p) : 𝔹 β†’ Type p where
  nil : Spine⁺ P []
  conss : βˆ€ n β†’ P n β†’ Spine⁺ (P βŠ• suc n) ns β†’ Spine⁺ P (n ∷ ns)

data Spine {p} (P : β„• β†’ Type p) : 𝔹 β†’ Type p where
  nil : Spine P []
  conss : βˆ€ n β†’ P n β†’ Spine⁺ (P βŠ• n) ns β†’ Spine P (n ∷ ns)

-- cons : (βˆ€ {m} β†’ P m β†’ P m β†’ P (suc m)) β†’ P zero β†’ Spine P ns β†’ Spine P (inc ns)
-- cons _*_ x nil = conss zero x nil
-- cons _*_ x (conss n x₁ nil) = conss zero x (conss n x₁ nil)
-- cons _*_ x (conss n x₁ (conss zero xβ‚‚ xs)) = conss (suc n) (x₁ * x₁) xs
-- cons _*_ x (conss n x₁ (conss (suc m) xβ‚‚ xs)) = conss zero x (conss n x₁ (conss m xβ‚‚ {!!}))