module Data.Environment where open import Data.Fin as Fin using (Fin; suc; zero) open import Data.List as List using (List; _∷_; []) open import Data.Product as Prod using (_×_; _,_; uncurry) open import Function using (const) open import Reflection private variable A : Set x : A xs xs′ : List A T T′ : A → List A → Set data Env (T : A → List A → Set) : List A → Set where [] : Env T [] _∷_ : T x xs → Env T xs → Env T (x ∷ xs) map : (f : ∀ {x xs} → T x xs → T′ x xs) → Env T xs → Env T′ xs map _f [] = [] map f (e ∷ env) = f e ∷ map f env head : Env T (x ∷ xs) → T x xs head (e ∷ _env) = e tail : Env T (x ∷ xs) → Env T xs tail (_e ∷ env) = env lookupRest : (xs : List A) (i : Fin (List.length xs)) → A × List A lookupRest (x ∷ xs) zero = x , xs lookupRest (x ∷ xs) (suc i) = lookupRest xs i lookup : (env : Env T xs) (i : Fin (List.length xs)) → uncurry T (lookupRest xs i) lookup [] () lookup ( e ∷ _env) zero = e lookup (_e ∷ env) (suc i) = lookup env i repeat : (f : ∀ x xs → T x xs) (xs : List A) → Env T xs repeat _f [] = [] repeat f (x ∷ xs) = f x xs ∷ repeat f xs module _ (inject : ∀ {x xs xs′} → T x xs → T x (xs List.++ xs′)) where append : (env : Env T xs) (env′ : Env T xs′) → Env T (xs List.++ xs′) append [] env′ = env′ append (x ∷ env) env′ = inject x ∷ (append env env′)