module Container where

open import Lib.Sigma
open import Lib.Nat

record Container : Set₁ where
  constructor _◃_
  field Sh   : Set
        Pos  : Sh → Set

⟦_⟧c : Container → Set → Set
⟦ Sh ◃ Pos ⟧c X = Σ Sh λ sh → Pos sh → X

ListC : Container
ListC = Nat ◃ Fin

List : (A : Set) → Set
List A = ⟦ ListC ⟧c A

record IxCon (M : Set) : Set₁ where
  constructor _◃_
  field Sh   : Set
        Pos  : Sh → M → Set

⟦_⟧ : {M : Set} → IxCon M → (M → Set) → M → Set
⟦_⟧ (Sh ◃ Pos) X m = Σ Sh λ sh → Pos sh m → X m

module GraphContainer where

  open import Lib.Star as L
  open IxCon

  data Edge {E : Set} : L.List E → L.List E → Set where
       push : ∀ {es} → (e : E) → Edge es (e ,- es)
       pop : ∀ {es} →  (e : E) → Edge (e ,- es) es
       span : ∀ {es} → Edge es es

  data NStar {X : Set}(R : X → X → Set)(x : X) : X → Nat → Set where
    nil′  : NStar R x x zero
    cons′ : {y z : X}{n : Nat} → R x y →  NStar R y z n
          → NStar  R x z (suc n)

  GraphC : {E : Set} → IxCon (L.List E × L.List E)
  Sh  (GraphC {E = E}) = Σ Nat \ n → NStar (Edge {E}) [] [] n
  Pos GraphC (n , _) (es , es') = Fin n

  Graph : {E : Set} → (C : Set) → Set
  Graph {E} C = ⟦ GraphC {E} ⟧ (λ _ → C) ([] , [])


  exampleG : {C E : Set}(c1 c2 : C)(e1 e2 : E) → Graph {E} C
  exampleG c1 c2 e1 e2
    = ( , cons′ (push e1) (cons′ (pop e1) nil′))
      , λ { zero → c1
          ; (suc zero) → c2}