------------------------------------------------------------------------
-- The Agda standard library
--
-- Environments (heterogeneous collections)
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.Star.Environment {} (Ty : Set ) where

open import Level
open import Data.Star.List
open import Data.Star.Decoration
open import Data.Star.Pointer as Pointer hiding (lookup)
open import Data.Unit
open import Function.Base hiding (_∋_)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Construct.Closure.ReflexiveTransitive

-- 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 (Lift  )) (σ ≡_) Γ

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 Pointer.lookup ρ i
... | result refl x = x