{-# OPTIONS --universe-polymorphism #-}
module NaPa.Interface where

open import Function
open import Level
open import Data.Nat
open import Data.Maybe using (Maybe; nothing; just)
open import Data.Unit using (⊤)
open import Data.Fin using (Fin; zero; suc)
open import Data.Sum
open import Data.Bool
open import NaPa.Worlds
open import NaPa.Subtyping
open import Relation.Nullary

record DataKit {ℓ} : Set (suc ℓ) where
  constructor mkKit
  field
    {World} : Set ℓ
    Name    : World → Set
    _↑1     : World → World

rawKit : DataKit
rawKit = mkKit {World = ⊤} (const ℕ) _

finKit : DataKit
finKit = mkKit Fin suc

mayKit : DataKit
mayKit = mkKit id Maybe

record Types (World : Set) : Set₁ where
  field
    Name : World → Set
    _⊆_ : World → World → Set
  infix  _⊆_

record Primitives {World}
                  (worldSym : WorldSymantics World)
                  (types : Types World)
                  (⊆-Sym : ⊆-Symantics worldSym (Types._⊆_ types)) : Set where
  open Types types
  open WorldSymantics worldSym
  open WorldOps worldSym
  open ⊆-Symantics ⊆-Sym
  field
    _==nm_   : ∀ {α} → Name α → Name α → Bool
    fromFin  : ∀ {α n} → Fin n → Name (α ↑ n)
    add      : ∀ {α} k → Name α → Name (α +[ k ])
    subtract : ∀ {α} k → Name (α +[ k ]) → Name α
    coe      : ∀ {α β} → α ⊆ β → Name α → Name β
    >nm      : ∀ {α} k → Name (α ↑ k) → Name (ø ↑ k) ⊎ Name (α +[ k ])
    ¬Name    : ∀ {α} → α ⊆ ø → ¬(Name α)

  infixl  add subtract
  infix  >nm
  syntax subtract k x = x ∸nm k
  syntax add k x = x +nm k
  syntax >nm k x = x <nm k

module Derived {World}
               {worldSym : WorldSymantics World}
               (types : Types World)
               (⊆-Sym : ⊆-Symantics worldSym (Types._⊆_ types))
               (prims : Primitives worldSym types ⊆-Sym) where
  open Types types
  open WorldSymantics worldSym
  open WorldOps worldSym
  open ⊆-Symantics ⊆-Sym
  open Primitives prims

  naPaKit : DataKit
  naPaKit = mkKit Name _↑1

  ze : ∀ {α} → Name (α ↑1)
  ze {α} = fromFin {α} {} zero

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

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

  su↑ : ∀ {α} → Name α → Name (α ↑1)
  su↑ = coe ⊆-+1↑1 ∘ su

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

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

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

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