Instantly share code, notes, and snippets.

# vituscze/SOTrie.agda Last active Aug 29, 2015

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 σ)