{-# 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 ℓ) ⟩