------------------------------------------------------------------------
-- The Agda standard library
--
-- Environments (heterogeneous collections)
------------------------------------------------------------------------
{-# OPTIONS --with-K --safe #-}
module Data.Star.Environment {ℓ} (Ty : Set ℓ) where
open import Level using (_⊔_)
open import Data.Star.List using (List)
open import Data.Star.Decoration using (All)
open import Data.Star.Pointer as Pointer using (Any; this; that; result)
open import Data.Unit.Polymorphic.Base using (⊤)
open import Function.Base using (const; case_of_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
using (_▻_)
-- Contexts, listing the types of all the elements in an environment.
Ctxt : Set ℓ
Ctxt = List Ty
-- Variables (de Bruijn indices); pointers into environments.
infix 4 _∋_
_∋_ : Ctxt → Ty → Set ℓ
Γ ∋ σ = Any (const (⊤ {ℓ})) (σ ≡_) Γ
vz : ∀ {Γ σ} → Γ ▻ σ ∋ σ
vz = this refl
vs : ∀ {Γ σ τ} → Γ ∋ τ → Γ ▻ σ ∋ τ
vs = that _
-- Environments. The T function maps types to element types.
Env : ∀ {e} → (Ty → Set e) → (Ctxt → Set (ℓ ⊔ e))
Env T Γ = All T Γ
-- A safe lookup function for environments.
lookup : ∀ {Γ σ} {T : Ty → Set} → Env T Γ → Γ ∋ σ → T σ
lookup ρ i with result refl x ← Pointer.lookup ρ i = x
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4