Skip to content

@vituscze /SOTrie.agda
Last active

Embed URL

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
module SOTrie where
open import Data.Unit
open import Category.Functor
open import Function
open import Level
open import Relation.Binary
-- A context is just a snoc-list.
data Cxt {𝒂} (A : Set 𝒂) : Set 𝒂 where
ε : Cxt A
_∷ᵣ_ : Cxt A A Cxt A
-- Context membership.
data _∈_ {𝒂} {A : Set 𝒂} (a : A) : Cxt A → Set 𝒂 where
here : {Δ} a ∈ Δ ∷ᵣ a
there : {Δ a′} a ∈ Δ a ∈ Δ ∷ᵣ a′
infix 3 _∈_
-- Well-formed types, using de Bruijn indices.
data _⊢ₜ (Δ : Cxt ⊤) : Set where
1ₜ : Δ ⊢ₜ
Varₜ : _ ∈ Δ Δ ⊢ₜ
_×ₜ_ : Δ ⊢ₜ Δ ⊢ₜ Δ ⊢ₜ
μₜ : Δ ∷ᵣ _ ⊢ₜ Δ ⊢ₜ
infix 3 _⊢ₜ
-- A closed type.
Type : Set
Type = ε ⊢ₜ
-- Type-level substitutions and renamings.
Sub Ren : Rel (Cxt ⊤) zero
Sub Δ Δ′ = _ ∈ Δ Δ′ ⊢ₜ
Ren Δ Δ′ = {x} x ∈ Δ x ∈ Δ′
-- Renaming extension.
extendᵣ : {Δ Δ′} Ren Δ Δ′ Ren (Δ ∷ᵣ _) (Δ′ ∷ᵣ _)
extendᵣ ρ here = here
extendᵣ ρ (there x) = there (ρ x)
-- Lift a type renaming to a type.
_*ᵣ_ : {Δ Δ′} Ren Δ Δ′ Δ ⊢ₜ Δ′ ⊢ₜ
_ *ᵣ 1= 1
ρ *ᵣ (Varₜ x) = Varₜ (ρ x)
ρ *ᵣ (τ₁ ×ₜ τ₂) = (ρ *ᵣ τ₁) ×ₜ (ρ *ᵣ τ₂)
ρ *ᵣ (μₜ τ) = μₜ (extendᵣ ρ *ᵣ τ)
-- Substitution extension.
extend : {Δ Δ′} Sub Δ Δ′ Sub (Δ ∷ᵣ _) (Δ′ ∷ᵣ _)
extend θ here = Varₜ here
extend θ (there x) = there *ᵣ (θ x)
-- Lift a type substitution to a type.
_*_ : {Δ Δ′} Sub Δ Δ′ Δ ⊢ₜ Δ′ ⊢ₜ
θ * 1= 1
θ * Varₜ x = θ x
θ * (τ₁ ×ₜ τ₂) = (θ * τ₁) ×ₜ (θ * τ₂)
θ * μₜ τ = μₜ (extend θ * τ)
data Trie {𝒂} (A : Set 𝒂) : Type → Set 𝒂 where
〈〉ₛ : A 1ₜ ▷ A
×ₛ : {τ₁ τ₂} τ₁ ▷ τ₂ ▷ A τ₁ ×ₜ τ₂ ▷ A
Rollₛ : {τ} (const (μₜ τ) * τ) ▷ A μₜ τ ▷ A
infixr 5 Trie
syntax Trie A τ = τ ▷ A
fmap fmap′ : {𝒂} {A B : Set 𝒂} {τ} (A B) τ ▷ A τ ▷ B
fmap f (〈〉ₛ x) = 〈〉ₛ (f x)
fmap f (×ₛ σ) = ×ₛ (fmap (fmap′ f) σ)
fmap f (Rollₛ σ) = Rollₛ (fmap f σ)
fmap′ f (〈〉ₛ x) = 〈〉ₛ (f x)
fmap′ f (×ₛ σ) = ×ₛ (fmap′ (fmap f) σ)
fmap′ f (Rollₛ σ) = Rollₛ (fmap′ f σ)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.