{-# OPTIONS --universe-polymorphism #-}
-- vim: iskeyword=a-z,A-Z,48-57,-,+,',#,/,~,],[,=,_,`,⊆
module NaPa where

open import Level
open import Irrelevance
import Relation.Binary.PropositionalEquality.NP as ≡
open ≡ using (_≡_; _≢_; _≗_; module ≗-Reasoning; module ≡-Reasoning)
open import Data.Nat.NP as Nat using (ℕ; zero; suc; s≤s; z≤n; ≤-pred; pred; _<=_; module <=)
                            renaming (_+_ to _+ℕ_ ; _∸_ to _∸ℕ_ ; _==_ to _==ℕ_; ¬≤ to ¬≤ℕ;
                                      _<_ to _<ℕ_ ; _≤_ to _≤ℕ_; _≥_ to _≥ℕ_; _≤?_ to _≤?ℕ_)
open import Data.Nat.Logical using (⟦ℕ⟧; zero; suc; ⟦ℕ⟧-setoid; ⟦ℕ⟧-equality; ⟦ℕ⟧-cong)
                          renaming (_≟_ to _≟⟦ℕ⟧_)
import Data.Nat.Properties as Nat
open import Function
open import Function.Equality as ⟶≡ using (_⟶_; _⟨$⟩_)
open import Data.Sum.NP as Sum using (_⊎_; inj₁; inj₂; [_,_]′) renaming (map to ⊎-map)
open import Data.Bool.Extras using (Bool; true; false; if_then_else_; T; not; T'not'¬)
open import Data.Unit using (⊤)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product.Extras using (_,_)
open import Data.Maybe.NP using (Maybe; nothing; just; maybe)
open import Relation.Binary.Extras as Bin
open import Relation.Nullary
open import Relation.Nullary.Decidable
import Relation.Binary.On.NP as On
open import NaPa.Worlds
open import NaPa.Subtyping
open ListBoolWorlds public
import Category.Monad as Cat
open Cat.RawMonad Data.Maybe.NP.monad
open Data.Maybe.NP.FunctorLemmas

private
  module ℕs = Setoid ⟦ℕ⟧-setoid
  module ℕe = Equality ⟦ℕ⟧-equality

infixr  _,_
record Name α : Set where
  constructor
    _,_
  field
    name    : ℕ
    name∈α : name ∈ α

open Name public

mkName : ∀ {α} (x : ℕ) → x ∈ α → Name α
mkName x pf = x , pf

infix  _≡nm_ _≟nm_ _==nm_

-- prim
_≡nm_ : ∀ {α} (x y : Name α) → Set
_≡nm_ = ⟦ℕ⟧ on name

-- prim
_≟nm_ : ∀ {α} → Decidable (_≡nm_ {α})
x ≟nm y = name x ≟⟦ℕ⟧ name y

-- prim
_==nm_ : ∀ {α} (x y : Name α) → Bool
_==nm_ x y = name x ==ℕ name y

name-injective : ∀ {α} {x y : Name α} → name x ≡ name y → x ≡ y
name-injective {α} {_ , p₁} {a , p₂} eq rewrite eq
--= ≡.refl {_} {_} {a , p₂}
  = ≡.cong (_,_ a) (∈-uniq α p₁ p₂)

Nm : World → Setoid zero zero
Nm α = On.setoid (name {α}) ℕs.isEquivalence

nm-equality : ∀ {α} → Equality (_≡nm_ {α})
nm-equality {α}
   = record { isEquivalence = Setoid.isEquivalence (Nm α)
            ; subst = λ P → ≡.subst P ∘ name-injective ∘ Equality.to-propositional ⟦ℕ⟧-equality }

module NmEq {α} = Equality (nm-equality {α})

≡nm⇒≡ : ∀ {α} → _≡nm_ {α} ⇒ _≡_
≡nm⇒≡ = NmEq.to-propositional

≡nm-cong : ∀ {α β} (f : Name α → Name β) → _≡nm_ =[ f ]⇒ _≡nm_
≡nm-cong f = NmEq.reflexive ∘ ≡.cong f ∘ ≡nm⇒≡

≡nm-⟦ℕ⟧-cong : ∀ {α} (f : Name α → ℕ) → _≡nm_ =[ f ]⇒ ⟦ℕ⟧
≡nm-⟦ℕ⟧-cong f = ℕe.reflexive ∘ ≡.cong f ∘ ≡nm⇒≡

≡-⟦ℕ⟧-cong : ∀ {a} {A : Set a} (f : A → ℕ) → _≡_ =[ f ]⇒ ⟦ℕ⟧
≡-⟦ℕ⟧-cong f = ℕe.reflexive ∘ ≡.cong f

≡nm-≡-cong : ∀ {a α} {A : Set a} (f : Name α → A) → _≡nm_ =[ f ]⇒ _≡_
≡nm-≡-cong f = ≡.cong f ∘ ≡nm⇒≡

⟦ℕ⟧-≡nm-cong : ∀ {α} (f : ℕ → Name α) → ⟦ℕ⟧ =[ f ]⇒ _≡nm_
⟦ℕ⟧-≡nm-cong f = NmEq.reflexive ∘ ≡.cong f ∘ ℕe.to-propositional

⟦ℕ⟧-≡-cong : ∀ {a} {A : Set a} (f : ℕ → A) → ⟦ℕ⟧ =[ f ]⇒ _≡_
⟦ℕ⟧-≡-cong f = ≡.cong f ∘ ℕe.to-propositional

module ≡nm-Reasoning {α} = Bin.Setoid-Reasoning (Nm α)

open WorldSymantics listBoolWorlds public
open WorldOps listBoolWorlds public
open WorldOps listBoolWorlds using () renaming (_+[_] to _+_)
open NaPa.Subtyping.⊆-Pack `⊆`-pack public
open NaPa.Subtyping.SyntacticOnBools ⊆ᵇ-pack public hiding (minimalSymantics)

-- Here is a first set of core primitives easy to define

-- prim
ze : ∀ {α} → Name (α ↑1)
ze =  , _

-- prim
¬Nameø : ¬(Name ø)
¬Nameø (_ , ())

-- prim
_+nm_ : ∀ {α} (x : Name α) k → Name (α + k)
_+nm_ {α} x k = k +ℕ name x , proof k where
  proof : ∀ k → k +ℕ name x ∈ α + k
  proof zero    = name∈α x
  proof (suc k) = proof k

infixl  _+nm_

-- prim
subtract : ∀ {α} k (x : Name (α + k)) → Name α
subtract k x = name x ∸ℕ k , proof (name x) k (name∈α x) where
  proof : ∀ {α} x k → (x ∈ α + k) → (x ∸ℕ k ∈ α)
  proof x       zero = id
  proof zero    (suc k) = λ()
  proof (suc x) (suc k) = proof x k

infixl  subtract
syntax subtract k x = x ∸nm k

-- prim
coe : ∀ {α β} → α ⊆ β → Name α → Name β
coe α⊆β x = name x , `⊆`-sound α⊆β (name x) (name∈α x)

-- Then we define some convenience functions on top of them.

infix  _because⟨_⟩
_because⟨_⟩ : ∀ {α β} → Name α → α ⊆ β → Name β
_because⟨_⟩ n pf = coe pf n

add : ∀ {α} k → Name α → Name (α + k)
add k x = x +nm k

add↑ : ∀ {α} k → Name α → Name (α ↑ k)
add↑ k x = x +nm k  because⟨ ⊆-+-↑ k ⟩

su : ∀ {α} → Name α → Name (α +1)
su x = x +nm 

su↑ : ∀ {α} → Name α → Name (α ↑1)
su↑ = add↑ 

-- Then comes <nm and the necessary intermediate definitions

private
  lem-<k : ∀ {α β x k} → x ≤ℕ k → x ∈ (α ↑ suc k) → x ∈ (β ↑ suc k)
  lem-<k z≤n       = _
  lem-<k (s≤s m≤n) = lem-<k m≤n

  lem-≥k : ∀ {α x k} → x ≥ℕ k → x ∈ α ↑ k → x ∈ α + k
  lem-≥k z≤n        = id
  lem-≥k (s≤s m≤n)  = lem-≥k m≤n

  lem-<k? : ∀ {α β n} k → n ∈ β ↑ k → n ∈ (if suc n <= k then α ↑ k else β + k)
  lem-<k? {n = n} k with suc n <= k | <=.sound (suc n) k | <=.complete {suc n} {k}
  ... | true  | n<k | _    = lem-<k (n<k _)
  ... | false | _   | ¬n<k = lem-≥k (¬≤ℕ ¬n<k)

-- prim
>nm-bool : ∀ {α} k → Name (α ↑ k) → Bool
>nm-bool k x = suc (name x) <= k

syntax >nm-bool k x = x <nm-bool k

-- prim
>nm-name : ∀ {α} k (x : Name (α ↑ k)) → Name (if >nm-bool k x then ø ↑ k else α + k)
>nm-name k x = name x , lem-<k? k (name∈α x)

syntax >nm-name k x = x <nm-name k

-- prim
>nm-name∈α : ∀ {α} k (x : Name (α ↑ k)) → name x ∈ (if >nm-bool k x then ø ↑ k else α + k)
>nm-name∈α k x = lem-<k? k (name∈α x)

syntax >nm-name∈α k x = x <nm-name∈α k

-- prim
>nm : ∀ {α} k → Name (α ↑ k) → Name (ø ↑ k) ⊎ Name (α + k)
>nm k x with >nm-bool k x | >nm-name∈α k x
... | true  | pf = inj₁ (name x , pf)
... | false | pf = inj₂ (name x , pf)

infix  >nm
syntax >nm k x = x <nm k

>nm-ind : ∀ {ℓ α} k (x : Name (α ↑ k))
            (P : (Name (ø ↑ k) ⊎ Name (α + k)) → Set ℓ)
            (Pinj₁ : T (>nm-bool k x) → ∀ pf → P (inj₁ (name x , pf)))
            (Pinj₂ : T (not (>nm-bool k x)) → ∀ pf → P (inj₂ (name x , pf)))
          → P (>nm k x)
>nm-ind k x P p₁ p₂
 with >nm-bool k x | >nm-name∈α k x
... | true         | pf = p₁ _ pf
... | false        | pf = p₂ _ pf

easy->nm : ∀ {α} k → Name (α ↑ k) → Name (ø ↑ k) ⊎ Name (α + k)
easy->nm zero x               = inj₂ x
easy->nm (suc _) (zero , _)   = inj₁ (zero , _)
easy->nm (suc k) (suc x , pf) = ⊎-map su↑ su (easy->nm k (x , pf))

syntax easy->nm k x = x <nm-easy k

easy->nm≗>nm : ∀ {α} k → easy->nm {α} k ≗ >nm k
easy->nm≗>nm zero x = ≡.cong inj₂ (name-injective ≡.refl)
easy->nm≗>nm (suc n) (zero , _) = ≡.refl
easy->nm≗>nm {α} (suc n) (suc x , pf) rewrite easy->nm≗>nm n (x , pf) = helper n x pf
  where
    helper : ∀ k x pf → ⊎-map su↑ su (>nm {α} k (x , pf)) ≡ >nm (suc k) (suc x , pf)
    helper k x pf = >nm-ind k (x , pf) (λ r → ⊎-map su↑ su r ≡ >nm (suc k) (suc x , pf))
                      (λ h pf' → >nm-ind (suc k) (suc x , pf) (λ r → inj₁ (suc x , pf') ≡ r)
                                         (λ _ _ → ≡.cong inj₁ (name-injective ≡.refl))
                                         (λ h' → ⊥-elim (T'not'¬ h' h)))
                      (λ h pf' → >nm-ind (suc k) (suc x , pf) (λ r → inj₂ (suc x , pf') ≡ r)
                                         (λ h' → ⊥-elim (T'not'¬ h h'))
                                         (λ _ _ → ≡.cong inj₂ (name-injective ≡.refl)))

-- prim (could be defined with (>nm 1)
lift↑1 : ∀ {α β} → (Name α → Name β) → Name (α ↑1) → Name (β ↑1)
lift↑1 f x with name x | name∈α x
... | zero  | _  = zero , _
... | suc m | pf = su↑ (f (m , pf))

-- mkName; _,_; name; name∈α are forbidden from now on (except in proofs).

ze↑1+ : ∀ {α} k → Name (α ↑ ( +ℕ k))
ze↑1+ _ = ze

infix  #_
#_ : ∀ {α} k → Name (α ↑ suc k)
#_ {α} k = ze +nm k because⟨ α ↑1 +[ k ]  ⊆⟨ ⊆-+-↑ k ⟩
                              α ↑1 ↑ k     ⊆⟨ ⊆-exch-↑-↑ ⊆-refl  k ⟩∎
                              α ↑ suc k ∎ ⟩
   where open ⊆-Reasoning

private
 module CoeExamples where
  nmα+→nmα↑ : ∀ {α} k → Name (α + k) → Name (α ↑ k)
  nmα+→nmα↑ k = coe (⊆-ctx-+↑ ⊆-refl k)
 module Unused where
  open import Data.List using ([]; _∷_; replicate; _++_)
  n∈trueⁿ⁺¹ : ∀ {α} n → n ∈ replicate (suc n) true ++ α
  n∈trueⁿ⁺¹ zero    = _
  n∈trueⁿ⁺¹ (suc n) = n∈trueⁿ⁺¹ n

predNm : ∀ {α} → Name (α +1) → Name α
predNm = subtract 

Name→-to-Nm⟶ : ∀ {b₁ b₂ α} {B : Setoid b₁ b₂} →
                 (Name α → Setoid.Carrier B) → Nm α ⟶ B
Name→-to-Nm⟶ {α = α} {B} f = record { _⟨$⟩_ = f; cong = cong′ }
  where
  open Setoid B renaming (_≈_ to _≈B_)

  cong≡ : ∀ {x y} → x ≡ y → f x ≈B f y
  cong≡ ≡.refl = Setoid.refl B

  cong′ : ∀ {x y} → x ≡nm y → f x ≈B f y
  cong′ = cong≡ ∘ Equality.to-propositional nm-equality

¬Name : ∀ {α} → α ⊆ ø → ¬(Name α)
¬Name α⊆ø = ¬Nameø ∘ coe α⊆ø

Name-elim : ∀ {a} {A : Set a} {α} (α⊆ø : α ⊆ ø) (x : Name α) → A
Name-elim x y with ¬Name x y
... | ()

Nameø-elim : ∀ {a} {A : Set a} → Name ø → A
Nameø-elim = Name-elim ⊆-refl

¬Nameø+ : ∀ k → ¬(Name (ø + k))
¬Nameø+ = ¬Name ∘ α⊆ø→α+⊆ø ⊆-ø-bottom

Nameø+-elim : ∀ {a} {A : Set a} k → Name (ø + k) → A
Nameø+-elim = Name-elim ∘ α⊆ø→α+⊆ø ⊆-ø-bottom

Nameø↑→Nameα↑ : ∀ {k} → Name (ø ↑ k) → ∀ {α} → Name (α ↑ k)
Nameø↑→Nameα↑ {k} x = coe (⊆-cong-↑ ⊆-ø-bottom k) x

exportName : ∀ {α} k → Name (α ↑ k) → Maybe (Name α)
exportName k x = [ const nothing , just ∘′ subtract k ]′ (x <nm k)

impNm : ∀ (ℓ k n : ℕ) → ℕ
impNm ℓ k n = if suc n <= ℓ then n else n +ℕ k

importName : ∀ {α β} ℓ k → α + k ⊆ β → Name (α ↑ ℓ) → Name (β ↑ ℓ)
importName ℓ k pf n
  with n <nm ℓ
...  | inj₁ n′ = n′        because⟨ ⊆-cong-↑ ø-bottom ℓ ⟩
...  | inj₂ n′ = n′ +nm k  because⟨ ⊆-trans (⊆-exch-+-+ ⊆-refl ℓ k) (⊆-ctx-+↑ pf ℓ) ⟩

module Singletons where

  SWorld : ℕ → World
  SWorld n = ø ↑1 + n

  SName : ℕ → Set
  SName = Name ∘ SWorld

  sName : ∀ n → SName n
  sName n = ze +nm n

  _+sn_ : ∀ {n} → SName n → ∀ k → SName (k +ℕ n)
  _+sn_ {n} x k = x +nm k  because⟨ ⊆-assoc-+ ⊆-refl n k ⟩

  subtract-sn : ∀ {n} k → SName (k +ℕ n) → SName n
  subtract-sn {n} k x = x′ ∸nm k
    where x′ = x  because⟨ ⊆-assoc-+′ ⊆-refl n k ⟩

  infixl  subtract-sn
  syntax subtract-sn k x = x ∸sn k

-- Properties

coe-names : ∀ {α β} (α⊆β : α ⊆ β) → name ∘ coe α⊆β ≗ name
coe-names = λ _ _ → ≡.refl

<nm-names : ∀ {α k} {x : Name (α ↑ k)} → [ name , name ]′ (x <nm k) ≡ name x
<nm-names {α} {k} {x} with x <nm-bool k | x <nm-name∈α k
... | true  | _ = ≡.refl
... | false | _ = ≡.refl

Dec-≡nm→≡ : ∀ {α} → Decidable (_≡nm_ {α}) → Decidable _≡_
Dec-≡nm→≡ _≟_ x y with x ≟ y
... | yes x≡y = yes (≡nm⇒≡ x≡y)
... | no  x≢y = no  (x≢y ∘′ ℕs.reflexive ∘′ ≡.cong name)

importName-ℓ-0≡coe : ∀ {α β} ℓ (pf : α ⊆ β) n → name (importName ℓ  pf n) ≡ name n
importName-ℓ-0≡coe ℓ pf x with x <nm-bool ℓ | x <nm-name∈α ℓ
... | true  | _ = ≡.refl
... | false | _ = ≡.refl

pred-impNm-comm : ∀ k x → pred (impNm  k (suc x)) ≡ x +ℕ k
pred-impNm-comm k x = ≡.refl

.import11-export1-comm :
  ∀ {α β} (pf : α +1 ⊆ β) (x : Name (α ↑1)) →
  exportName  (importName   pf x) ≡ coe pf ∘ su <$> exportName  x
import11-export1-comm {α} pf x
   = <$>-injective₁ name-injective (≡.trans (helper (name x) {name∈α x} (suc (name x) ≤?ℕ )) (<$>-assoc (exportName  x)))
  where
    -- getting the name unpacked (and the Dec), works around an Agda bug in 2.2.8.
    .helper : ∀ n {pn : n ∈ α ↑1} → Dec (n <ℕ ) → let x = n , pn in
             name <$> (exportName  (importName   pf x)) ≡ name ∘ (coe pf ∘ su) <$> exportName  x
    helper zero    (no ¬p)         = ⊥-elim (¬p (s≤s z≤n))
    helper .      (yes (s≤s z≤n)) = ≡.refl
    helper (suc _) (no _)          = ≡.refl

1+ : ∀ {α} → Name α → Name (α +1)
1+ x = x +nm 

module Name↑⇔Fin where
  open import Data.Fin as Fin

  ⇒ : ∀ n → Name (ø ↑ n) → Fin n
  ⇒ zero    = Nameø-elim
  ⇒ (suc n) = maybe (suc ∘′ ⇒ n) zero ∘ exportName 

  ⇐ : ∀ {α n} → Fin n → Name (α ↑ n)
  ⇐ (zero {n})  = ze↑1+ n
  ⇐ (suc i)     = su↑ (⇐ i)

module WorldSyntax where
  data `World` : Set where
    _`↑1`  _`+1` : (`α` : `World`) → `World`
    `ø` : `World`

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

  _`+`_ : (`α` : `World`) (k : ℕ) → `World`
  `α` `+` zero = `α`
  `α` `+` suc n = (`α` `+` n) `+1`

  El : `World` → World
  El (`α` `↑1`)  = El `α` ↑1
  El (`α` `+1`)  = El `α` +1
  El `ø`     = ø

  -- A second way to see bnd is to say that it loose the distinction
  -- between ↑1 and +1.
  bnd : `World` → ℕ
  bnd (`α` `↑1`)  = suc (bnd `α`)
  bnd (`α` `+1`)  = suc (bnd `α`)
  bnd `ø`         = 

  empty? : `World` → Set
  empty? (`α` `↑1`) = ⊥
  empty? (`α` `+1`) = empty? `α`
  empty? `ø`        = ⊤

  _`∈`_ : ℕ → `World` → Set
  _      `∈` `ø`        = ⊥
  zero   `∈` (`α` `↑1`) = ⊤
  suc n  `∈` (`α` `↑1`) = n `∈` `α`
  zero   `∈` (`α` `+1`) = ⊥
  suc n  `∈` (`α` `+1`) = n `∈` `α`

module WorldSyntaxProps where
  open WorldSyntax
  comm-El-↑ : ∀ `α` n → El `α` ↑ n ≡ El (`α` `↑` n)
  comm-El-↑ `α` zero                            = ≡.refl
  comm-El-↑ `α` (suc n) rewrite comm-El-↑ `α` n = ≡.refl

module ℕ⇒Name`α` where
  open WorldSyntax
  ⇒ : ∀ `α` x → x ∈ El `α` → Name (El `α`)
  ⇒ (`α` `↑1`) zero    _     = zero , _
  ⇒ (`α` `↑1`) (suc i) pf    = su↑ (⇒ `α` i pf)
  ⇒ (`α` `+1`) zero    ()
  ⇒ (`α` `+1`) (suc i) pf    = su (⇒ `α` i pf)
  ⇒ `ø`        _       ()

module Name`α`⇔Fin where
  open import Data.Fin as F renaming (_+_ to _+F_)
  open WorldSyntax
  open WorldSyntaxProps
  mutual

    ⇒+1 : ∀ `α` → Name (El `α` +1) → Fin (suc (bnd `α`))
    ⇒+1 `α` = F.raise  ∘ ⇒ `α` ∘ predNm

    ⇒ : ∀ `α` → Name (El `α`) → Fin (bnd `α`)
    ⇒ (`α` `↑1`)  = [ inject+ _ ∘ Name↑⇔Fin.⇒  , ⇒+1 `α` ]′ ∘ >nm 
    ⇒ (`α` `+1`)  = ⇒+1 `α`
    ⇒ `ø`         = Nameø-elim

  ⇐₁ : ∀ {n} `α` → (x : Fin n) → toℕ x ∈ El `α` → Name (El `α`)
  ⇐₁ `α` = ℕ⇒Name`α`.⇒ `α` ∘ toℕ

  x∈ø↑x : ∀ {n} (x : Fin n) → toℕ x ∈ (ø ↑ n)
  x∈ø↑x zero    = _
  x∈ø↑x (suc n) = x∈ø↑x n

  ⇐₂ : ∀ {n} → (x : Fin n) → Name (ø ↑ n)
  ⇐₂ {n} x with x∈ø↑x x
  ...         | y       rewrite comm-El-↑ `ø` n = ⇐₁ (`ø` `↑` n) x y

module WellFormedWorld where
  data WF : World → Set where
    `ø : WF ø
    _`+_ : ∀ {α} (`α : WF α) k → WF (α + k)
    _`↑_ : ∀ {α} (`α : WF α) k → WF (α ↑ k)

_+↑nm_ : ∀ {α} → Name α → ∀ k → Name (α ↑ k)
_+↑nm_ x k = coe (⊆-ctx-+↑ ⊆-refl k) (x +nm k)

subtract↑ : ∀ {α} k → Name (α ↑ k) → Name (ø ↑ k) ⊎ Name α
subtract↑ k x with x <nm k
... | inj₁ x′ = inj₁ x′
... | inj₂ x′ = inj₂ (x′ ∸nm k)

infixl  subtract↑
syntax subtract↑ k x = x -↑nm k

data WithLim (R : (α β : World) → Set) : (α β : World) → Set where
  mkWithLim : ∀ {α₀ β₀} ℓ (Rα₀β₀ : R α₀ β₀) → WithLim R (α₀ ↑ ℓ) (β₀ ↑ ℓ)

withLim : ∀ {R α β} → R α β → WithLim R α β
withLim = mkWithLim 

-- functions known to be ``bad'' and that we don't want to export
private
 module Bad where
  -- `name' alone is "bad"
  bad₁ : ∀ {α} → Name α → Bool
  bad₁ (zero  , _) = true
  bad₁ (suc _ , _) = false