@@ -23,6 +23,7 @@ import Data.Functor.Classes
2323import Data.Group
2424import Data.List.NonEmpty (NonEmpty (..))
2525import qualified Data.List.NonEmpty as NE
26+import qualified Data.Map.Extra as M
2627import Data.Map.Shifted.Strict (ShiftedMap (..))
2728import qualified Data.Map.Shifted.Strict as SM
2829import Data.Map.Strict (Map)
@@ -94,31 +95,35 @@ variableNames =
9495showNType :: NType -> Text
9596showNType t = TL.toStrict . T.toLazyText $ showNType' 0 t
9697 where
97− greekVars = M.fromList . traceShowId $ zip (S.toList $ getAllDeBurjins t) variableNames
98+ greekVars = M.fromList $ zip (S.toList $ getAllDeBurjins t) variableNames
9899 showNType' :: Int -> NType -> T.Builder
99100 showNType' depth u =
100101 foralls <> case u of
101102 (NAtomic a) -> showAtomicType a
102103 (NBrujin (DeBrujin i j)) -> greekVars M.! (DeBrujin (i - depth) j)
103104 (NTypeVariable _) -> error "should not have free type variables at this point"
104− (x :-> y) -> showNType' (depth + 1) x <> " -> " <> showNType' (depth + 1) y
105− (List x) -> "[" <> showNType' (depth + 1) x <> "]"
105+ (x :-> y) -> showNextNType' x <> " -> " <> showNextNType' y
106+ (List x) -> "[" <> showNextNType' x <> "]"
106107 (NAttrSet x) ->
107108 "{ "
108109 <> ( mconcat
109110 . intersperse "; "
110− . fmap (\(k, v) -> T.fromText k <> " = " <> showNType' (depth + 1) v)
111+ . fmap (\(k, v) -> T.fromText k <> " = " <> showNextNType' v)
111112 $ M.toList x
112113 )
113114 <> " }"
114115 where
115− currBurjins = traceShowId . S.mapMonotonic (DeBrujin (- depth)) $ getDeBurjins 0 (traceShowId u)
116+ showNextNType' = showNType' $ depth + 1
117+ currBurjins =
118+ M.restrictKeysToRange
119+ (Range (DeBrujin (- depth) 0) (DeBrujin (- depth + 1) 0))
120+ greekVars
116121 foralls =
117− if S.null currBurjins
122+ if M.null currBurjins
118123 then ""
119124 else
120125 "∀ "
121− <> (mconcat . intersperse " " . M.elems $ M.restrictKeys greekVars currBurjins)
126+ <> (mconcat . intersperse " " . M.elems $ currBurjins)
122127 <> ". "
123128
124129showAtomicType :: AtomicType -> T.Builder
@@ -150,34 +155,38 @@ data AtomicType
150155 | URI
151156 deriving stock (Eq, Ord, Show)
152157
153−getDeBurjins :: Int -> NType -> Set Int
154−getDeBurjins _ (NTypeVariable _) = S.empty
155−getDeBurjins _ (NAtomic _) = S.empty
156−getDeBurjins n (NBrujin (DeBrujin m j)) | m == n = S.singleton j
157−getDeBurjins _ (NBrujin _) = S.empty
158−getDeBurjins n (x :-> y) = getDeBurjins (n + 1) x <> getDeBurjins (n + 1) y
159−getDeBurjins n (List x) = getDeBurjins (n + 1) x
160−getDeBurjins n (NAttrSet xs) = foldMap (getDeBurjins (n + 1)) . M.elems $ xs
161−
158+-- | Get all De Brujin type variables that were bound in the the outermost
159+-- (current) binding context.
160+-- Only returns the second indexes.
161+getDeBurjins :: NType -> Set Int
162+getDeBurjins = getDeBurjins' 0
163+
164+-- | Gets all De Brujin variables with the given binding context offset.
165+-- Only returns the second indexes.
166+getDeBurjins' :: Int -> NType -> Set Int
167+getDeBurjins' _ (NTypeVariable _) = S.empty
168+getDeBurjins' _ (NAtomic _) = S.empty
169+getDeBurjins' n (NBrujin (DeBrujin m j)) | m == n = S.singleton j
170+getDeBurjins' _ (NBrujin _) = S.empty
171+getDeBurjins' n (x :-> y) = getDeBurjins' (n + 1) x <> getDeBurjins' (n + 1) y
172+getDeBurjins' n (List x) = getDeBurjins' (n + 1) x
173+getDeBurjins' n (NAttrSet xs) = foldMap (getDeBurjins' (n + 1)) . M.elems $ xs
174+
175+-- | Returns the set of all De Brujin type variables relative to the outermost
176+-- (current) binding context.
177+-- So variables that are bound in one of the inner contexts will have a negative
178+-- binding context number.
162179getAllDeBurjins :: NType -> Set DeBrujin
163180getAllDeBurjins =
164181 traceShowId . \case
165182 (NTypeVariable _) -> S.empty
166183 (NAtomic _) -> S.empty
167184 (NBrujin x) -> S.singleton x
168− (x :-> y) -> bncCtx $ getAllDeBurjins x <> getAllDeBurjins y
169− (List x) -> bncCtx $ getAllDeBurjins x
170− (NAttrSet xs) -> bncCtx . foldMap getAllDeBurjins . M.elems $ xs
185+ (x :-> y) -> bndCtx $ getAllDeBurjins x <> getAllDeBurjins y
186+ (List x) -> bndCtx $ getAllDeBurjins x
187+ (NAttrSet xs) -> bndCtx . foldMap getAllDeBurjins . M.elems $ xs
171188 where
172− bncCtx = S.mapMonotonic (\(DeBrujin i j) -> DeBrujin (i - 1) j)
173−
174−isClosed :: NType -> Bool
175−isClosed (NTypeVariable _) = False
176−isClosed (NBrujin _) = True
177−isClosed (NAtomic _) = True
178−isClosed (x :-> y) = isClosed x && isClosed y
179−isClosed (List x) = isClosed x
180−isClosed (NAttrSet xs) = all isClosed . M.elems $ xs
189+ bndCtx = S.mapMonotonic (\(DeBrujin i j) -> DeBrujin (i - 1) j)
181190
182191newtype DeBrujinContext = DeBrujinContext (Sum Int)
183192 deriving newtype (Eq, Ord, Show, Semigroup, Monoid, Group, Num)
@@ -331,8 +340,6 @@ data Fresh x where
331340 Fresh :: Fresh TypeVariable
332341 -- | Inclusive
333342 MinFreshFromNow :: Fresh TypeVariable
334− -- | Inclusive
335− MaxFreshUntilNow :: Fresh TypeVariable
336343
337344data ResumableExceptions x
338345
@@ -348,16 +355,13 @@ runFresh =
348355 put (TypeVariable $ x + 1)
349356 return (TypeVariable x)
350357 MinFreshFromNow -> get
351− MaxFreshUntilNow -> do
352− (TypeVariable new) <- get
353− return $ TypeVariable (new - 1)
354358 )
355359
356360registerTypeVariables :: Member Fresh r => Eff r a -> Eff r (a, Range TypeVariable)
357361registerTypeVariables m = do
358362 l <- send MinFreshFromNow
359363 a <- m
360− r <- send MaxFreshUntilNow
364+ r <- send MinFreshFromNow
361365 return (a, Range l r)
362366
363367freshSrc ::