Skip to content

Instantly share code, notes, and snippets.

@gallais
Last active Jun 22, 2020
Embed
What would you like to do?
{-# 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)
{-# 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment