module NaPa.Worlds where

open import Data.Nat          using (ℕ; zero; suc; pred) renaming (_+_ to _+ℕ_)
open import Data.List         using (List; []; _∷_; replicate; _++_)
open import Data.Bool         using (Bool; true; false)
open import Data.Empty        using (⊥)
open import Data.Unit         using (⊤)
open import Function          using (id)
open import Relation.Nullary  using (¬_)
open import Relation.Binary.PropositionalEquality as ≡

record WorldSymantics (W : Set) : Set where
  field
    ø : W
    _↑1 _+1 : (α : W) → W

  _^1 : (α : W) → W
  _^1 = _↑1

  Abs : (α : W) → W
  Abs = _↑1

module WorldOps {World} (Wsym : WorldSymantics World) where
  open WorldSymantics Wsym

  infixl  _↑_ _+[_]

  _+[_] : World → ℕ → World
  α +[      ] = α
  α +[ suc n ] = (α +[ n ])+1

  _↑_ : World → ℕ → World
  α ↑      = α
  α ↑ suc n = (α ↑ n)↑1

  _^[_] : World → ℕ → World
  _^[_] = _↑_

module ListBoolSpecialized where
  infixl  _↑_

  World : Set
  World = List Bool

  _+[_] : World → ℕ → World
  α +[ k ] = replicate k false ++ α
     -- {(i+k,j+k) | (i,j) ∈ α}

  _↑_ : World → ℕ → World
  α ↑ k = replicate k true ++ α
  -- {(i,i) | i ∈ 0 .. k-1 } ∪ α :+ k

module ListBoolWorlds where
  World : Set
  World = List Bool

  listBoolWorlds : WorldSymantics (List Bool)
  listBoolWorlds = record { ø = ø; _↑1 = _↑1; _+1 = _+1 }
   where
    ø : World
    ø = []

    _+1 : World → World
    α +1 = false ∷ α

    _↑1 : World → World
    α ↑1 = true ∷ α

  _∈_ : ℕ → World → Set
  _      ∈ []            = ⊥
  zero   ∈ (false ∷ _)   = ⊥
  zero   ∈ (true  ∷ _)   = ⊤
  suc n  ∈ (_     ∷ xs)  = n ∈ xs

  _∉_ : ℕ → World → Set
  x ∉ α = ¬(x ∈ α)
  infix  _∈_ _∉_

  ∈-uniq : ∀ {x} α (p q : x ∈ α) → p ≡ q
  ∈-uniq         []            ()  _
  ∈-uniq {zero}  (false ∷ xs)  ()  _
  ∈-uniq {zero}  (true ∷ xs)   _   _ = ≡.refl
  ∈-uniq {suc n} (_ ∷ xs)      p   q = ∈-uniq {n} xs p q

  private
   module Unused where
    open WorldSymantics listBoolWorlds
    open WorldOps listBoolWorlds
    x∉ø+ : ∀ x k → x ∉ (ø +[ k ])
    x∉ø+ zero    zero ()
    x∉ø+ (suc _) zero ()
    x∉ø+ zero (suc k) ()
    x∉ø+ (suc n) (suc k) pf = x∉ø+ n k pf

    ∈false∷ : ∀ x {xs} → x ∈ false ∷ xs → pred x ∈ xs
    ∈false∷ zero     = λ()
    ∈false∷ (suc n)  = id