commit 6f62012ba08c2013fa236187d9a7c6a887d0d088
Author: Robert Russell <robert@rr3.xyz>
Date: Sun, 22 Jun 2025 19:32:24 -0700
Initial commit
Diffstat:
6 files changed, 184 insertions(+), 0 deletions(-)
diff --git a/.gitignore b/.gitignore
@@ -0,0 +1,3 @@
+*.cabal
+stack.yaml.lock
+.stack-work
diff --git a/package.yaml b/package.yaml
@@ -0,0 +1,35 @@
+name: plutils
+author: Robert Russell
+
+ghc-options:
+ - -Wall
+ - -Wno-name-shadowing
+ - -Wno-unused-top-binds
+
+language: GHC2021
+
+default-extensions:
+ - BlockArguments
+ - DataKinds
+ - DefaultSignatures
+ - FunctionalDependencies
+ - GADTs
+ - LambdaCase
+ - MagicHash
+ - OverloadedStrings
+ - PartialTypeSignatures
+ - QuantifiedConstraints
+ - RecursiveDo
+ - TypeData
+ - TypeFamilies
+ - UnboxedTuples
+ - UnicodeSyntax
+ - UnliftedNewtypes
+ - UnliftedDatatypes
+
+dependencies:
+ - base
+ - containers
+
+library:
+ source-dirs: src
diff --git a/src/PlUtils/DeBruijn.hs b/src/PlUtils/DeBruijn.hs
@@ -0,0 +1,40 @@
+module PlUtils.DeBruijn (
+ IsIndex,
+ intToIdx,
+ idxToInt,
+ IsLevel,
+ intToLvl,
+ lvlToInt,
+ SemValue (..),
+) where
+
+import Data.Coerce
+
+--------------------------------------------------------------------------------
+-- De Bruijn indices
+
+type IsIndex = Coercible Int
+
+intToIdx :: (IsIndex a) => Int -> a
+intToIdx = coerce
+
+idxToInt :: (IsIndex a) => a -> Int
+idxToInt = coerce
+
+--------------------------------------------------------------------------------
+-- De Bruijn levels
+
+type IsLevel = Coercible Int
+
+intToLvl :: (IsLevel a) => Int -> a
+intToLvl = coerce
+
+lvlToInt :: (IsLevel a) => a -> Int
+lvlToInt = coerce
+
+--------------------------------------------------------------------------------
+-- Semantic values with generic values represented as de Bruijn levels
+
+class (IsLevel (Level a)) => SemValue a where
+ type Level a
+ generic :: Level a -> a
diff --git a/src/PlUtils/Env.hs b/src/PlUtils/Env.hs
@@ -0,0 +1,78 @@
+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/ShadowMap.hs b/src/PlUtils/ShadowMap.hs
@@ -0,0 +1,27 @@
+module PlUtils.ShadowMap (
+ ShadowMap,
+ empty,
+ assign,
+ lookup,
+) where
+
+import Data.List ((!?))
+import Data.Map.Strict (Map)
+import Data.Map.Strict qualified as Map
+import Prelude hiding (lookup)
+
+insertOrAdjust :: (Ord k) => v -> (v -> v) -> k -> Map k v -> Map k v
+insertOrAdjust i a = Map.alter \case
+ Nothing -> Just i
+ Just v -> Just (a v)
+
+newtype ShadowMap k v = ShadowMap (Map k [v]) deriving (Show, Eq, Functor)
+
+empty :: (Ord k) => ShadowMap k v
+empty = ShadowMap Map.empty
+
+assign :: (Ord k) => k -> v -> ShadowMap k v -> ShadowMap k v
+assign k v (ShadowMap m) = ShadowMap (insertOrAdjust [v] (v :) k m)
+
+lookup :: (Ord k) => k -> Int -> ShadowMap k v -> Maybe v
+lookup k i (ShadowMap m) = Map.lookup k m >>= (!? i)
diff --git a/stack.yaml b/stack.yaml
@@ -0,0 +1 @@
+resolver: lts-23.23
