← Back to branch summary

~ubuntu-branches/ubuntu/lucid/agda-stdlib/lucid

« back to all changes in this revision

Viewing changes to src/Data/Star/Environment.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-08 23:35:09 UTC
  • Revision ID: james.westby@ubuntu.com-20100108233509-l6ejt9xji64xysfb
Import upstream version 0.3

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Star/Environment.agda
 
1
------------------------------------------------------------------------
 
2
-- Environments (heterogeneous collections)
 
3
------------------------------------------------------------------------
 
4
 
 
5
module Data.Star.Environment (Ty : Set) where
 
6
 
 
7
open import Data.Star
 
8
open import Data.Star.List
 
9
open import Data.Star.Decoration
 
10
open import Data.Star.Pointer as Pointer hiding (lookup)
 
11
open import Data.Unit
 
12
open import Relation.Binary.PropositionalEquality
 
13
 
 
14
-- Contexts, listing the types of all the elements in an environment.
 
15
 
 
16
Ctxt : Set
 
17
Ctxt = List Ty
 
18
 
 
19
-- Variables (de Bruijn indices); pointers into environments.
 
20
 
 
21
infix 4 _∋_
 
22
 
 
23
_∋_ : Ctxt → Ty → Set
 
24
Γ ∋ σ = Any (λ _ → ⊤) (_≡_ σ) Γ
 
25
 
 
26
vz : ∀ {Γ σ} → Γ ▻ σ ∋ σ
 
27
vz = this refl
 
28
 
 
29
vs : ∀ {Γ σ τ} → Γ ∋ τ → Γ ▻ σ ∋ τ
 
30
vs = that tt
 
31
 
 
32
-- Environments. The T function maps types to element types.
 
33
 
 
34
Env : (Ty → Set) → Ctxt → Set
 
35
Env T Γ = All T Γ
 
36
 
 
37
-- A safe lookup function for environments.
 
38
 
 
39
lookup : ∀ {Γ σ} {T : Ty → Set} → Γ ∋ σ → Env T Γ → T σ
 
40
lookup i ρ with Pointer.lookup i ρ
 
41
... | result refl x = x