{-# 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 2 _⊆_

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 6 add subtract
  infix 4 >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 {α} {1} zero

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

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

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

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

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

  infix 0 _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 )