{-# OPTIONS --universe-polymorphism #-}
module NaPa.TransKit where
import Category.Functor as Cat
open import Level
open import Function
open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin
open import Data.Maybe as Maybe
open import NaPa.Interface
open import NaPa using (Name; exportName; su↑; ze; _↑1)
record TransKit ℓ₁ ℓ₂ : Set (suc (ℓ₁ ⊔ ℓ₂)) where
constructor mkTransKit
field
k₁ : DataKit {ℓ₁}
k₂ : DataKit {ℓ₂}
open DataKit k₁ renaming (World to World₁; Name to Name₁; _↑1 to _↑1₁)
open DataKit k₂ renaming (World to World₂; Name to Name₂; _↑1 to _↑1₂)
field
Env : World₁ → World₂ → Set
_↑↑ : ∀ {α₁ α₂} → Env α₁ α₂ → Env (α₁ ↑1₁) (α₂ ↑1₂)
lookup : ∀ {α₁ α₂} → Env α₁ α₂ → Name₁ α₁ → Name₂ α₂
naPaKit : DataKit
naPaKit = mkKit Name _↑1
naPa-to-fin : TransKit _ _
naPa-to-fin = mkTransKit naPaKit finKit (λ α n → Name α → Fin n) _↑↑ id where
open import Data.Fin
_↑↑ : ∀ {α n} → (Name α → Fin n) → (Name (α ↑1) → Fin (suc n))
_↑↑ f = maybe (suc ∘′ f) zero ∘′ exportName 1
naPa-to-may : TransKit _ _
naPa-to-may = mkTransKit naPaKit mayKit (λ α A → Name α → A) _↑↑ id where
open Cat.RawFunctor Maybe.functor
_↑↑ : ∀ {α A} → (Name α → A) → (Name (α ↑1) → Maybe A)
_↑↑ f x = f <$> exportName 1 x
naPa-to-raw : TransKit _ _
naPa-to-raw = mkTransKit naPaKit rawKit (λ α _ → Name α → ℕ) _↑↑ id where
_↑↑ : ∀ {α} → (Name α → ℕ) → (Name (α ↑1) → ℕ)
_↑↑ f = maybe (suc ∘′ f) zero ∘′ exportName 1
raw-to-NaPa : TransKit _ _
raw-to-NaPa = mkTransKit rawKit naPaKit (λ _ α → ℕ → Name α) _↑↑ id where
_↑↑ : ∀ {α} → (ℕ → Name α) → (ℕ → Name (α ↑1))
_↑↑ _ zero = ze
_↑↑ f (suc n) = su↑ (f n)
fin-to-NaPa : TransKit _ _
fin-to-NaPa = mkTransKit finKit naPaKit (λ n α → Fin n → Name α) _↑↑ id where
open import Data.Fin
_↑↑ : ∀ {n α} → (Fin n → Name α) → (Fin (suc n) → Name (α ↑1))
_↑↑ _ zero = ze
_↑↑ f (suc n) = su↑ (f n)
may-to-NaPa : TransKit _ _
may-to-NaPa = mkTransKit mayKit naPaKit (λ A α → A → Name α) _↑↑ id where
_↑↑ : ∀ {A α} → (A → Name α) → (Maybe A → Name (α ↑1))
_↑↑ _ nothing = ze
_↑↑ f (just n) = su↑ (f n)