commit eadfc1b82c261148bc2028ad639c22764fe5421a
parent 3e370f2e237e83f47900aa225b53243bf737fb5a
Author: Robert Russell <robert@rr3.xyz>
Date: Sun, 6 Jul 2025 14:12:06 -0700
Start using naturals library, and temporarily comment out a bunch of stuff
Diffstat:
7 files changed, 57 insertions(+), 29 deletions(-)
diff --git a/.gitmodules b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "naturals"]
+ path = naturals
+ url = git://git.rr3.xyz/naturals
diff --git a/naturals b/naturals
@@ -0,0 +1 @@
+Subproject commit db6d10b99f3a092cb6b2ddc16c0aa166bf5c083d
diff --git a/package.yaml b/package.yaml
@@ -30,6 +30,7 @@ default-extensions:
dependencies:
- base
- containers
+ - naturals
library:
source-dirs: src
diff --git a/src/PlUtils/DeBruijn.hs b/src/PlUtils/DeBruijn.hs
@@ -1,40 +1,53 @@
module PlUtils.DeBruijn (
- IsIndex,
- intToIdx,
- idxToInt,
- IsLevel,
- intToLvl,
- lvlToInt,
- SemValue (..),
+ Index (..),
+ Level (..),
+ idxToLvl,
+ lvlToIdx,
) where
import Data.Coerce
+import Naturals
--------------------------------------------------------------------------------
--- De Bruijn indices
+-- Indices and levels
-type IsIndex = Coercible Int
+newtype Index n = Index (Finat n)
+newtype Level n = Level (Finat n)
-intToIdx :: (IsIndex a) => Int -> a
-intToIdx = coerce
+idxToLvl :: Snat n -> Index n -> Level n
+idxToLvl = coerce finatMirror
-idxToInt :: (IsIndex a) => a -> Int
-idxToInt = coerce
+lvlToIdx :: Snat n -> Level n -> Index n
+lvlToIdx = coerce finatMirror
--------------------------------------------------------------------------------
--- 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
+-- TODO
+
+{-
+Data structures required for elaboration of surface (shadowing names) to
+core (de Bruijn indices):
+
+ULC (standard):
+ Depth: `Nat` (Peano-indexed?)
+ VarMap: `ShadowMap Name Level` OR `ShadowMap Name Value`
+ The latter provides a convenient way to implement predeclared names.
+STLC (no type variables):
+ Depth: `Nat`
+ DVarMap: `ShadowMap DName (DLevel, Type)` OR `ShadowMap DName (DValue, Type)`
+STLC/PLC (type variables but no higher kinds):
+ Depth: `Nat`
+ DVarMap: `ShadowMap DName (DLevel, Type)` OR `ShadowMap DName (DValue, Type)`
+ SVarMap: `ShadowMap SName SLevel` OR `ShadowMap SName SValue`
+STLC/HOPLC (type variables and higher kinds):
+ Depth: `Nat`
+ DVarMap: `ShadowMap DName (DLevel, Type)` OR `ShadowMap DName (DValue, Type)`
+ SVarMap: `ShadowMap SName (SLevel, Kind)` OR `ShadowMap SName (SValue, Kind)`
+-}
+
+{-
+TODO: Do same thing but with evaluation.
+TODO: Do we need to carry a substitution on static variables during elaboration?
+This is what I've done in the past, but I don't think it's necessary. At times
+when we need to evaluate during elaboration, we can just convert the elaboration
+context to an evaluation environment with an empty substitution.
+-}
diff --git a/src/PlUtils/Environment.hs b/src/PlUtils/Environment.hs
@@ -1,3 +1,6 @@
+module PlUtils.Environment where
+
+{-
module PlUtils.Environment (
Environment,
empty,
@@ -76,3 +79,4 @@ 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)
+-}
diff --git a/src/PlUtils/ShadowMap.hs b/src/PlUtils/ShadowMap.hs
@@ -15,6 +15,8 @@ insertOrAdjust i a = Map.alter \case
Nothing -> Just i
Just v -> Just (a v)
+-- | A @ShadowMap@ is a (strict) @Map@ that supports shadowing values without
+-- overwriting them.
newtype ShadowMap k v = ShadowMap (Map k [v]) deriving (Show, Eq, Functor)
empty :: (Ord k) => ShadowMap k v
diff --git a/stack.yaml b/stack.yaml
@@ -1 +1,5 @@
resolver: lts-23.23
+
+packages:
+ - .
+ - naturals
