SyntaxDesc.agda

{-# OPTIONS --safe --without-K #-}

module SyntaxDesc (I : Set) where

open import Agda.Primitive using () renaming (Set to Type)
open import Data.Nat.Base
open import Data.Fin.Base
open import Data.List.Base using (List; []; _∷_; _++_)

data Desc : Type₀ where
  ‵σ : (n : ℕ) (d : Fin n → Desc) → Desc
  ‵r : I → Desc → Desc
  ‵λ : List I → Desc → Desc
  ‵■ : I → Desc

module _ (X : I → List I → Type₀) where

  data Meaning : Desc → I → List I → Type₀ where
    _,_   : ∀ {n d i Γ} (k : Fin n) → Meaning (d k) i Γ → Meaning (‵σ n d) i Γ
    [_],_ : ∀ {j d i Γ} → X j Γ → Meaning d i Γ → Meaning (‵r j d) i Γ
    [_]   : ∀ {Δ d i Γ} → Meaning d i (Δ ++ Γ) → Meaning (‵λ Δ d) i Γ
    refl  : ∀ {i Γ} → Meaning (‵■ i) i Γ

⟦_⟧ : Desc → (I → List I → Type₀) → I → List I → Type₀
⟦ d ⟧ X i Γ = Meaning X d i Γ


data Var (i : I) : List I → Type₀ where
  Z : ∀ {Γ} → Var i (i ∷ Γ)
  S_ : ∀ {Γ j} → Var i Γ → Var i (j ∷ Γ)

data Tm (d : Desc) (i : I) (Γ : List I) : Type₀ where
  ‵var : Var i Γ → Tm d i Γ
  ‵tm  : ⟦ d ⟧ (Tm d) i Γ → Tm d i Γ

ext : ∀ {Γ Δ}
    → (∀ {i} → Var i Γ → Var i Δ)
    → (∀ {i} Θ → Var i (Θ ++ Γ) → Var i (Θ ++ Δ))
ext ρ []      x     = ρ x
ext ρ (_ ∷ Θ) Z     = Z
ext ρ (_ ∷ Θ) (S x) = S (ext ρ Θ x)

module _ (d : Desc) where

  rename : ∀ {Γ Δ}
         → (∀ {i} → Var i Γ → Var i Δ)
         → (∀ {i} → Tm d i Γ → Tm d i Δ)
  rename⟦_⟧ : ∀ e {Γ Δ}
           → (∀ {i} → Var i Γ → Var i Δ)
           → (∀ {i} → ⟦ e ⟧ (Tm d) i Γ → ⟦ e ⟧ (Tm d) i Δ)

  rename⟦ ‵σ A e ⟧ ρ (a , t)    = a , rename⟦ e a ⟧ ρ t
  rename⟦ ‵r j e ⟧ ρ ([ r ], t) = [ rename ρ r ], rename⟦ e ⟧ ρ t
  rename⟦ ‵λ Δ e ⟧ ρ [ t ]      = [ rename⟦ e ⟧ (ext ρ Δ) t ]
  rename⟦ ‵■ i   ⟧ ρ refl       = refl

  rename ρ (‵var x) = ‵var (ρ x)
  rename ρ (‵tm x ) = ‵tm (rename⟦ d ⟧ ρ x)

SyntaxDescPar.agda

{-# OPTIONS --safe --without-K #-}

module SyntaxDescPar (I : Set) where

open import Agda.Primitive using () renaming (Set to Type)
open import Data.Nat.Base
open import Data.Fin.Base
open import Data.List.Base using (List; []; _∷_; _++_)

data Desc (n : ℕ) (As : Fin n → Type₀) : Type₀ where
  ‵σ : (k : Fin n) (d : As k → Desc n As) → Desc n As
  ‵r : I → Desc n As → Desc n As
  ‵λ : List I → Desc n As → Desc n As
  ‵■ : I → Desc n As

module _ {n : ℕ} {As : Fin n → Type₀} (X : I → List I → Type₀) where

  data Meaning : Desc n As → I → List I → Type₀ where
    _,_   : ∀ {k d i Γ} (a : As k) → Meaning (d a) i Γ → Meaning (‵σ k d) i Γ
    [_],_ : ∀ {j d i Γ} → X j Γ → Meaning d i Γ → Meaning (‵r j d) i Γ
    [_]   : ∀ {Δ d i Γ} → Meaning d i (Δ ++ Γ) → Meaning (‵λ Δ d) i Γ
    refl  : ∀ {i Γ} → Meaning (‵■ i) i Γ

⟦_⟧ : ∀ {n As} → Desc n As → (I → List I → Type₀) → I → List I → Type₀
⟦ d ⟧ X i Γ = Meaning X d i Γ


data Var (i : I) : List I → Type₀ where
  Z : ∀ {Γ} → Var i (i ∷ Γ)
  S_ : ∀ {Γ j} → Var i Γ → Var i (j ∷ Γ)

data Tm {n As} (d : Desc n As) (i : I) (Γ : List I) : Type₀ where
  ‵var : Var i Γ → Tm d i Γ
  ‵tm  : ⟦ d ⟧ (Tm d) i Γ → Tm d i Γ

ext : ∀ {Γ Δ}
    → (∀ {i} → Var i Γ → Var i Δ)
    → (∀ {i} Θ → Var i (Θ ++ Γ) → Var i (Θ ++ Δ))
ext ρ []      x     = ρ x
ext ρ (_ ∷ Θ) Z     = Z
ext ρ (_ ∷ Θ) (S x) = S (ext ρ Θ x)

module _ {n As} (d : Desc n As) where

  rename : ∀ {Γ Δ}
         → (∀ {i} → Var i Γ → Var i Δ)
         → (∀ {i} → Tm d i Γ → Tm d i Δ)
  rename⟦_⟧ : ∀ e {Γ Δ}
           → (∀ {i} → Var i Γ → Var i Δ)
           → (∀ {i} → ⟦ e ⟧ (Tm d) i Γ → ⟦ e ⟧ (Tm d) i Δ)

  rename⟦ ‵σ A e ⟧ ρ (a , t)    = a , rename⟦ e a ⟧ ρ t
  rename⟦ ‵r j e ⟧ ρ ([ r ], t) = [ rename ρ r ], rename⟦ e ⟧ ρ t
  rename⟦ ‵λ Δ e ⟧ ρ [ t ]      = [ rename⟦ e ⟧ (ext ρ Δ) t ]
  rename⟦ ‵■ i   ⟧ ρ refl       = refl

  rename ρ (‵var x) = ‵var (ρ x)
  rename ρ (‵tm x ) = ‵tm (rename⟦ d ⟧ ρ x)