commit 0d9ba56d82d9a5993d54fb79f38c4e39af7f1b8e
parent eadfc1b82c261148bc2028ad639c22764fe5421a
Author: Robert Russell <robert@rr3.xyz>
Date: Sat, 26 Jul 2025 18:35:14 -0700
Uncomment and simplify environments
Diffstat:
4 files changed, 68 insertions(+), 63 deletions(-)
diff --git a/package.yaml b/package.yaml
@@ -18,6 +18,7 @@ default-extensions:
- MagicHash
- OverloadedStrings
- PartialTypeSignatures
+ - PatternSynonyms
- QuantifiedConstraints
- RecursiveDo
- TypeData
diff --git a/src/PlUtils/DeBruijn.hs b/src/PlUtils/DeBruijn.hs
@@ -1,24 +1,54 @@
module PlUtils.DeBruijn (
+ Depth (..),
Index (..),
Level (..),
+ descend,
+ idxInBounds,
+ lvlInBounds,
+ assertIdxInBounds,
+ assertLvlInBounds,
idxToLvl,
lvlToIdx,
) where
-import Data.Coerce
-import Naturals
+import Naturals.Nat
+
+import PlUtils.Util
--------------------------------------------------------------------------------
-- Indices and levels
-newtype Index n = Index (Finat n)
-newtype Level n = Level (Finat n)
+-- | A @Nat@ representing the number of free variables in some context.
+newtype Depth = Depth {unDepth :: Nat} deriving (Show, Eq)
+
+-- | A de Bruijn index represented as a @Nat@, that is, an index into a context
+-- "from the right", such that the innermost free variable gets index 0.
+newtype Index = Index {unIndex :: Nat} deriving (Show, Eq)
+
+-- | A de Bruijn level represented as a @Nat@, that is, an index into a context
+-- "from the left", such that the outermost free variable gets index 0.
+newtype Level = Level {unLevel :: Nat} deriving (Show, Eq)
+
+descend :: Depth -> (Level, Depth)
+descend (Depth d) = assert (d < maxBound) "PlUtils: depth overflow" (Level d, Depth (d + 1))
+
+idxInBounds :: Depth -> Index -> Bool
+idxInBounds (Depth d) (Index i) = i < d
+
+lvlInBounds :: Depth -> Level -> Bool
+lvlInBounds (Depth d) (Level l) = l < d
+
+assertIdxInBounds :: Depth -> Index -> a -> a
+assertIdxInBounds d i = assert (idxInBounds d i) "PlUtils: index out of bounds"
+
+assertLvlInBounds :: Depth -> Level -> a -> a
+assertLvlInBounds d l = assert (lvlInBounds d l) "PlUtils: level out of bounds"
-idxToLvl :: Snat n -> Index n -> Level n
-idxToLvl = coerce finatMirror
+idxToLvl :: Depth -> Index -> Level
+idxToLvl d i = assertIdxInBounds d i $ Level (unDepth d - unIndex i - 1)
-lvlToIdx :: Snat n -> Level n -> Index n
-lvlToIdx = coerce finatMirror
+lvlToIdx :: Depth -> Level -> Index
+lvlToIdx d l = assertLvlInBounds d l $ Index (unDepth d - unLevel l - 1)
--------------------------------------------------------------------------------
-- TODO
diff --git a/src/PlUtils/Environment.hs b/src/PlUtils/Environment.hs
@@ -1,82 +1,48 @@
-module PlUtils.Environment where
-
-{-
module PlUtils.Environment (
Environment,
empty,
depth,
bind,
- idxToLvl,
- lvlToIdx,
assign,
lookup,
define,
- eval,
) where
-import Control.Exception hiding (assert)
-import Data.IntMap.Strict (IntMap)
-import Data.IntMap.Strict qualified as IntMap
-import Data.Maybe (fromMaybe)
+import Naturals.NatMap (NatMap)
+import Naturals.NatMap qualified as NatMap
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)
+-- 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 v = Environment Depth (NatMap v) deriving (Show)
-empty :: (IsIndex idx, SemValue val) => Environment idx val
-empty = Environment 0 IntMap.empty
+empty :: Environment v
+empty = Environment (Depth 0) NatMap.empty
-depth :: (IsIndex idx, SemValue val) => Environment idx val -> Int
+depth :: Environment v -> Depth
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)
+bind :: Environment v -> (Level, Environment v)
+bind (Environment d s) =
+ let (l, d') = descend d
+ in (l, Environment d' s)
-- | 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)
+assign :: Level -> v -> Environment v -> Environment v
+assign l v (Environment d s) = assertLvlInBounds d l $ Environment d (NatMap.insert (unLevel l) v 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
+lookup :: Level -> Environment v -> Maybe v
+lookup l (Environment d s) = assertLvlInBounds d l $ NatMap.lookup (unLevel 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 :: (Level -> v) -> Environment v -> Environment v
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)
--}
+ let (l, env') = bind env
+ in assign l (makeVal l) env'
diff --git a/src/PlUtils/Util.hs b/src/PlUtils/Util.hs
@@ -0,0 +1,8 @@
+module PlUtils.Util (
+ assert,
+) where
+
+import Control.Exception hiding (assert)
+
+assert :: Bool -> String -> a -> a
+assert b s a = if b then a else throw (AssertionFailed s)
