git.iko.soy/tix
on master help sign in
Optimized yet more things
6db2184iko
src/Data/Map/Extra.hsnew file+14
compare with master
unifiedsplit
@@ -0,0 +1,14 @@
1+module Data.Map.Extra
2+ ( restrictKeysToRange,
3+ )
4+where
5+
6+import qualified Data.Map as M
7+import Data.Map.Strict (Map)
8+import Data.Range (Range (..))
9+import qualified Data.Range as R
10+
11+restrictKeysToRange :: Ord k => Range k -> Map k v -> Map k v
12+restrictKeysToRange range =
13+ M.takeWhileAntitone (`R.member` range)
14+ . M.dropWhileAntitone (`R.notMember` range)
src/Data/Range.hs+2−2
@@ -5,7 +5,7 @@ module Data.Range
5 )
5 )
6where
6where
7
7
8−-- | Includes both ends included
8+-- | Left included, right excluded
9data Range a
9data Range a
10 = Range' !a !a
10 = Range' !a !a
11 | InfiniteRange
11 | InfiniteRange
@@ -14,7 +14,7 @@ data Range a
14member :: Ord a => a -> Range a -> Bool
14member :: Ord a => a -> Range a -> Bool
15member _ InfiniteRange = True
15member _ InfiniteRange = True
16member _ EmptyRange = False
16member _ EmptyRange = False
17−member a (Range' l r) = a >= l && a <= r
17+member a (Range' l r) = a >= l && a < r
18{-# INLINE member #-}
18{-# INLINE member #-}
19
19
20notMember :: Ord a => a -> Range a -> Bool
20notMember :: Ord a => a -> Range a -> Bool
src/Tix/Typechecker.hs+38−34
@@ -23,6 +23,7 @@ import Data.Functor.Classes
23import Data.Group
23import Data.Group
24import Data.List.NonEmpty (NonEmpty (..))
24import Data.List.NonEmpty (NonEmpty (..))
25import qualified Data.List.NonEmpty as NE
25import qualified Data.List.NonEmpty as NE
26+import qualified Data.Map.Extra as M
26import Data.Map.Shifted.Strict (ShiftedMap (..))
27import Data.Map.Shifted.Strict (ShiftedMap (..))
27import qualified Data.Map.Shifted.Strict as SM
28import qualified Data.Map.Shifted.Strict as SM
28import Data.Map.Strict (Map)
29import Data.Map.Strict (Map)
@@ -94,31 +95,35 @@ variableNames =
94showNType :: NType -> Text
95showNType :: NType -> Text
95showNType t = TL.toStrict . T.toLazyText $ showNType' 0 t
96showNType t = TL.toStrict . T.toLazyText $ showNType' 0 t
96 where
97 where
97− greekVars = M.fromList . traceShowId $ zip (S.toList $ getAllDeBurjins t) variableNames
98+ greekVars = M.fromList $ zip (S.toList $ getAllDeBurjins t) variableNames
98 showNType' :: Int -> NType -> T.Builder
99 showNType' :: Int -> NType -> T.Builder
99 showNType' depth u =
100 showNType' depth u =
100 foralls <> case u of
101 foralls <> case u of
101 (NAtomic a) -> showAtomicType a
102 (NAtomic a) -> showAtomicType a
102 (NBrujin (DeBrujin i j)) -> greekVars M.! (DeBrujin (i - depth) j)
103 (NBrujin (DeBrujin i j)) -> greekVars M.! (DeBrujin (i - depth) j)
103 (NTypeVariable _) -> error "should not have free type variables at this point"
104 (NTypeVariable _) -> error "should not have free type variables at this point"
104− (x :-> y) -> showNType' (depth + 1) x <> " -> " <> showNType' (depth + 1) y
105+ (x :-> y) -> showNextNType' x <> " -> " <> showNextNType' y
105− (List x) -> "[" <> showNType' (depth + 1) x <> "]"
106+ (List x) -> "[" <> showNextNType' x <> "]"
106 (NAttrSet x) ->
107 (NAttrSet x) ->
107 "{ "
108 "{ "
108 <> ( mconcat
109 <> ( mconcat
109 . intersperse "; "
110 . intersperse "; "
110− . fmap (\(k, v) -> T.fromText k <> " = " <> showNType' (depth + 1) v)
111+ . fmap (\(k, v) -> T.fromText k <> " = " <> showNextNType' v)
111 $ M.toList x
112 $ M.toList x
112 )
113 )
113 <> " }"
114 <> " }"
114 where
115 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
116 foralls =
121 foralls =
117− if S.null currBurjins
122+ if M.null currBurjins
118 then ""
123 then ""
119 else
124 else
120 "∀ "
125 "∀ "
121− <> (mconcat . intersperse " " . M.elems $ M.restrictKeys greekVars currBurjins)
126+ <> (mconcat . intersperse " " . M.elems $ currBurjins)
122 <> ". "
127 <> ". "
123
128
124showAtomicType :: AtomicType -> T.Builder
129showAtomicType :: AtomicType -> T.Builder
@@ -150,34 +155,38 @@ data AtomicType
150 | URI
155 | URI
151 deriving stock (Eq, Ord, Show)
156 deriving stock (Eq, Ord, Show)
152
157
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.
153−getDeBurjins :: Int -> NType -> Set Int
166+getDeBurjins' :: Int -> NType -> Set Int
154−getDeBurjins _ (NTypeVariable _) = S.empty
167+getDeBurjins' _ (NTypeVariable _) = S.empty
155−getDeBurjins _ (NAtomic _) = S.empty
168+getDeBurjins' _ (NAtomic _) = S.empty
156−getDeBurjins n (NBrujin (DeBrujin m j)) | m == n = S.singleton j
169+getDeBurjins' n (NBrujin (DeBrujin m j)) | m == n = S.singleton j
157−getDeBurjins _ (NBrujin _) = S.empty
170+getDeBurjins' _ (NBrujin _) = S.empty
158−getDeBurjins n (x :-> y) = getDeBurjins (n + 1) x <> getDeBurjins (n + 1) y
171+getDeBurjins' n (x :-> y) = getDeBurjins' (n + 1) x <> getDeBurjins' (n + 1) y
159−getDeBurjins n (List x) = getDeBurjins (n + 1) x
172+getDeBurjins' n (List x) = getDeBurjins' (n + 1) x
160−getDeBurjins n (NAttrSet xs) = foldMap (getDeBurjins (n + 1)) . M.elems $ xs
173+getDeBurjins' n (NAttrSet xs) = foldMap (getDeBurjins' (n + 1)) . M.elems $ xs
161−
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.
162getAllDeBurjins :: NType -> Set DeBrujin
179getAllDeBurjins :: NType -> Set DeBrujin
163getAllDeBurjins =
180getAllDeBurjins =
164 traceShowId . \case
181 traceShowId . \case
165 (NTypeVariable _) -> S.empty
182 (NTypeVariable _) -> S.empty
166 (NAtomic _) -> S.empty
183 (NAtomic _) -> S.empty
167 (NBrujin x) -> S.singleton x
184 (NBrujin x) -> S.singleton x
168− (x :-> y) -> bncCtx $ getAllDeBurjins x <> getAllDeBurjins y
185+ (x :-> y) -> bndCtx $ getAllDeBurjins x <> getAllDeBurjins y
169− (List x) -> bncCtx $ getAllDeBurjins x
186+ (List x) -> bndCtx $ getAllDeBurjins x
170− (NAttrSet xs) -> bncCtx . foldMap getAllDeBurjins . M.elems $ xs
187+ (NAttrSet xs) -> bndCtx . foldMap getAllDeBurjins . M.elems $ xs
171 where
188 where
172− bncCtx = S.mapMonotonic (\(DeBrujin i j) -> DeBrujin (i - 1) j)
189+ bndCtx = 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
181
190
182newtype DeBrujinContext = DeBrujinContext (Sum Int)
191newtype DeBrujinContext = DeBrujinContext (Sum Int)
183 deriving newtype (Eq, Ord, Show, Semigroup, Monoid, Group, Num)
192 deriving newtype (Eq, Ord, Show, Semigroup, Monoid, Group, Num)
@@ -331,8 +340,6 @@ data Fresh x where
331 Fresh :: Fresh TypeVariable
340 Fresh :: Fresh TypeVariable
332 -- | Inclusive
341 -- | Inclusive
333 MinFreshFromNow :: Fresh TypeVariable
342 MinFreshFromNow :: Fresh TypeVariable
334− -- | Inclusive
335− MaxFreshUntilNow :: Fresh TypeVariable
336
343
337data ResumableExceptions x
344data ResumableExceptions x
338
345
@@ -348,16 +355,13 @@ runFresh =
348 put (TypeVariable $ x + 1)
355 put (TypeVariable $ x + 1)
349 return (TypeVariable x)
356 return (TypeVariable x)
350 MinFreshFromNow -> get
357 MinFreshFromNow -> get
351− MaxFreshUntilNow -> do
352− (TypeVariable new) <- get
353− return $ TypeVariable (new - 1)
354 )
358 )
355
359
356registerTypeVariables :: Member Fresh r => Eff r a -> Eff r (a, Range TypeVariable)
360registerTypeVariables :: Member Fresh r => Eff r a -> Eff r (a, Range TypeVariable)
357registerTypeVariables m = do
361registerTypeVariables m = do
358 l <- send MinFreshFromNow
362 l <- send MinFreshFromNow
359 a <- m
363 a <- m
360− r <- send MaxFreshUntilNow
364+ r <- send MinFreshFromNow
361 return (a, Range l r)
365 return (a, Range l r)
362
366
363freshSrc ::
367freshSrc ::