commit 3baa91b7a8cc580469fb6e0c15673ea36998ceb2
parent f844d389f0a9897b15b65d8a07a2f2dd7bc9195d
Author: Robert Russell <robert@rr3.xyz>
Date: Sun, 24 May 2026 19:39:34 -0700
Add topLevel
Diffstat:
2 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/PlUtils/DeBruijn.hs b/src/PlUtils/DeBruijn.hs
@@ -2,6 +2,7 @@ module PlUtils.DeBruijn (
Depth (..),
Index (..),
Level (..),
+ topLevel,
descend,
idxInBounds,
lvlInBounds,
@@ -35,6 +36,9 @@ newtype Index syn = Index {unIndex :: Nat} deriving (Show, Eq)
-- The @syn@ phantom type parameter separates levels for different syntaxes.
newtype Level syn = Level {unLevel :: Nat} deriving (Show, Eq)
+topLevel :: Depth syn
+topLevel = Depth 0
+
descend :: Depth syn -> (Level syn, Depth syn)
descend (Depth d) = assert (d < maxBound) "PlUtils: depth overflow" (Level d, Depth (d + 1))
diff --git a/src/PlUtils/Environment.hs b/src/PlUtils/Environment.hs
@@ -24,7 +24,7 @@ import PlUtils.DeBruijn
data Environment syn v = Environment (Depth syn) (NatMap v) deriving (Show)
empty :: Environment syn v
-empty = Environment (Depth 0) NatMap.empty
+empty = Environment topLevel NatMap.empty
depth :: Environment syn v -> Depth syn
depth (Environment d _) = d