From 18547332435c0e33106763daa9d8532c9df09115 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 14 Aug 2024 15:06:30 +0100
Subject: Define environments over worlds.

---
 src/Inky/Env.idr | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)
 create mode 100644 src/Inky/Env.idr

(limited to 'src/Inky/Env.idr')

diff --git a/src/Inky/Env.idr b/src/Inky/Env.idr
new file mode 100644
index 0000000..174b681
--- /dev/null
+++ b/src/Inky/Env.idr
@@ -0,0 +1,30 @@
+module Inky.Env
+
+import Control.Relation
+import Inky.Binding
+
+infix 2 :~
+
+public export
+record Assoc (0 a : Type) where
+  constructor (:~)
+  binder : Binder
+  value : a
+
+public export
+data PartialEnv : Type -> World -> World -> Type where
+  Lin : PartialEnv a w w
+  (:<) : PartialEnv a w v -> (x : Assoc a) -> PartialEnv a (w :< x.binder) v
+
+public export
+Env : Type -> World -> Type
+Env a w = PartialEnv a w [<]
+
+public export
+partialLookup : PartialEnv a w v -> Name w -> Either (Name v) a
+partialLookup [<] = Left
+partialLookup (env :< (x :~ v)) = stripWith (Right v) (partialLookup env)
+
+public export
+lookup : Env a w -> Name w -> a
+lookup = either absurd id .: partialLookup
-- 
cgit v1.2.3