Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
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