commit f4591f02060b35485616909048dfb4445c4fab69
parent 6f62012ba08c2013fa236187d9a7c6a887d0d088
Author: Robert Russell <robert@rr3.xyz>
Date: Sun, 22 Jun 2025 19:41:54 -0700
Rename Env to Environment
Diffstat:
2 files changed, 78 insertions(+), 78 deletions(-)
diff --git a/src/PlUtils/Env.hs b/src/PlUtils/Env.hs
@@ -1,78 +0,0 @@
-module PlUtils.Env (
- Env,
- empty,
- depth,
- bind,
- idxToLvl,
- lvlToIdx,
- assign,
- lookup,
- define,
- eval,
-) where
-
-import Control.Exception hiding (assert)
-import Data.IntMap (IntMap)
-import Data.IntMap qualified as IntMap
-import Data.Maybe (fromMaybe)
-import Prelude hiding (lookup)
-
-import PlUtils.DeBruijn
-
--- We really ought to use natural numbers here instead of integers, but Haskell
--- makes that difficult (e.g., fixed-precision natural number types are called
--- "WordXX" instead of "NatXX", and there's IntMap but not NatMap).
-
-assert :: Bool -> String -> a -> a
-assert b s a = if b then a else throw (AssertionFailed s)
-
--- | A collection of free variables and a substitution on them, intended for
--- semantic elaboration and evaluation with semantic variables represented as
--- de Bruijn levels (which are stable under weakening, so we don't need to
--- modify the environment when descending under a binder) and with syntactic
--- variables represented as de Bruijn indices.
-data Env idx val = Env Int (IntMap val) deriving (Show)
-
-empty :: (IsIndex idx, SemValue val) => Env idx val
-empty = Env 0 IntMap.empty
-
-depth :: (IsIndex idx, SemValue val) => Env idx val -> Int
-depth (Env d _) = d
-
--- | Bind a new variable (without introducing a substitution for it).
-bind :: (IsIndex idx, SemValue val) => Env idx val -> (Level val, Env idx val)
-bind (Env d s) = assert (d < maxBound) "PlUtils.Env.bind: depth overflow" (intToLvl d, Env (d + 1) s)
-
-idxToLvl :: (IsIndex idx, SemValue val) => idx -> Env idx val -> Level val
-idxToLvl idx (Env d _) =
- let i = idxToInt idx
- in assert (0 <= i && i < d) "PlUtils.Env.idxToLvl: index out of range" $ intToLvl (d - i - 1)
-
-lvlToIdx :: (IsIndex idx, SemValue val) => Level val -> Env idx val -> idx
-lvlToIdx lvl (Env d _) =
- let l = lvlToInt lvl
- in assert (0 <= l && l < d) "PlUtils.Env.lvlToIdx: level out of range" $ intToIdx (d - l - 1)
-
--- | Assign a value to an existing variable.
-assign :: (IsIndex idx, SemValue val) => Level val -> val -> Env idx val -> Env idx val
-assign lvl val (Env d s) =
- let l = lvlToInt lvl
- in assert (0 <= l && l < d) "PlUtils.Env.assign: level out of range" $ Env d (IntMap.insert l val s)
-
--- | Lookup the substitution for a variable.
-lookup :: (IsIndex idx, SemValue val) => Level val -> Env idx val -> Maybe val
-lookup lvl (Env d s) =
- let l = lvlToInt lvl
- in assert (0 <= l && l < d) "PlUtils.Env.lookup: level out of range" $ IntMap.lookup l s
-
--- | Bind and a new variable and assign a value to it.
-define :: (IsIndex idx, SemValue val) => (Level val -> val) -> Env idx val -> Env idx val
-define makeVal env =
- let (lvl, env') = bind env
- in assign lvl (makeVal lvl) env'
-
--- | Lookup the substitution for a variable.
-eval :: (IsIndex idx, SemValue val) => idx -> Env idx val -> val
-eval idx env =
- let lvl = idxToLvl idx env
- in fromMaybe (generic lvl) (lookup lvl env)
diff --git a/src/PlUtils/Environment.hs b/src/PlUtils/Environment.hs
@@ -0,0 +1,78 @@
+module PlUtils.Environment (
+ Environment,
+ empty,
+ depth,
+ bind,
+ idxToLvl,
+ lvlToIdx,
+ assign,
+ lookup,
+ define,
+ eval,
+) where
+
+import Control.Exception hiding (assert)
+import Data.IntMap (IntMap)
+import Data.IntMap qualified as IntMap
+import Data.Maybe (fromMaybe)
+import Prelude hiding (lookup)
+
+import PlUtils.DeBruijn
+
+-- We really ought to use natural numbers here instead of integers, but Haskell
+-- makes that difficult (e.g., fixed-precision natural number types are called
+-- "WordXX" instead of "NatXX", and there's IntMap but not NatMap).
+
+assert :: Bool -> String -> a -> a
+assert b s a = if b then a else throw (AssertionFailed s)
+
+-- | A collection of free variables and a substitution on them, intended for
+-- semantic elaboration and evaluation with semantic variables represented as
+-- de Bruijn levels (which are stable under weakening, so we don't need to
+-- modify the environment when descending under a binder) and with syntactic
+-- variables represented as de Bruijn indices.
+data Environment idx val = Environment Int (IntMap val) deriving (Show)
+
+empty :: (IsIndex idx, SemValue val) => Environment idx val
+empty = Environment 0 IntMap.empty
+
+depth :: (IsIndex idx, SemValue val) => Environment idx val -> Int
+depth (Environment d _) = d
+
+-- | Bind a new variable (without introducing a substitution for it).
+bind :: (IsIndex idx, SemValue val) => Environment idx val -> (Level val, Environment idx val)
+bind (Environment d s) = assert (d < maxBound) "PlUtils.Environment.bind: depth overflow" (intToLvl d, Environment (d + 1) s)
+
+idxToLvl :: (IsIndex idx, SemValue val) => idx -> Environment idx val -> Level val
+idxToLvl idx (Environment d _) =
+ let i = idxToInt idx
+ in assert (0 <= i && i < d) "PlUtils.Environment.idxToLvl: index out of range" $ intToLvl (d - i - 1)
+
+lvlToIdx :: (IsIndex idx, SemValue val) => Level val -> Environment idx val -> idx
+lvlToIdx lvl (Environment d _) =
+ let l = lvlToInt lvl
+ in assert (0 <= l && l < d) "PlUtils.Environment.lvlToIdx: level out of range" $ intToIdx (d - l - 1)
+
+-- | Assign a value to an existing variable.
+assign :: (IsIndex idx, SemValue val) => Level val -> val -> Environment idx val -> Environment idx val
+assign lvl val (Environment d s) =
+ let l = lvlToInt lvl
+ in assert (0 <= l && l < d) "PlUtils.Environment.assign: level out of range" $ Environment d (IntMap.insert l val s)
+
+-- | Lookup the substitution for a variable.
+lookup :: (IsIndex idx, SemValue val) => Level val -> Environment idx val -> Maybe val
+lookup lvl (Environment d s) =
+ let l = lvlToInt lvl
+ in assert (0 <= l && l < d) "PlUtils.Environment.lookup: level out of range" $ IntMap.lookup l s
+
+-- | Bind and a new variable and assign a value to it.
+define :: (IsIndex idx, SemValue val) => (Level val -> val) -> Environment idx val -> Environment idx val
+define makeVal env =
+ let (lvl, env') = bind env
+ in assign lvl (makeVal lvl) env'
+
+-- | Lookup the substitution for a variable.
+eval :: (IsIndex idx, SemValue val) => idx -> Environment idx val -> val
+eval idx env =
+ let lvl = idxToLvl idx env
+ in fromMaybe (generic lvl) (lookup lvl env)
