git.iko.soy/tix
on master help sign in
optimized colsing
c00466diko
package.yaml+3
compare with master
unifiedsplit
@@ -28,6 +28,8 @@ dependencies:
28 - lens
28 - lens
29 - data-fix
29 - data-fix
30 - mono-traversable
30 - mono-traversable
31+ - acts
32+ - groups
31library:
33library:
32 source-dirs: src
34 source-dirs: src
33
35
@@ -70,3 +72,4 @@ default-extensions:
70 - PatternSynonyms
72 - PatternSynonyms
71 - ViewPatterns
73 - ViewPatterns
72 - KindSignatures
74 - KindSignatures
75+ - MultiParamTypeClasses
src/Data/Map/Shifted/Strict.hsnew file+39
@@ -0,0 +1,39 @@
1+module Data.Map.Shifted.Strict
2+ ( ShiftedMap (..),
3+ Data.Map.Shifted.Strict.lookup,
4+ insert,
5+ shift,
6+ liftMap,
7+ unshift,
8+ )
9+where
10+
11+import Data.Act
12+import Data.Group
13+import Data.Map.Strict (Map)
14+import qualified Data.Map.Strict as M
15+
16+data ShiftedMap d k v = ShiftedMap d (Map k v)
17+ deriving stock (Eq, Ord, Show)
18+
19+instance (Act d v, Group d, Ord k) => Semigroup (ShiftedMap d k v) where
20+ (ShiftedMap d m) <> (ShiftedMap d' m') =
21+ ShiftedMap d $ m <> (act (invert d <> d') <$> m')
22+
23+instance (Monoid d, Semigroup (ShiftedMap d k v)) => Monoid (ShiftedMap d k v) where
24+ mempty = ShiftedMap mempty M.empty
25+
26+lookup :: (Ord k, Act d v) => k -> ShiftedMap d k v -> Maybe v
27+lookup k (ShiftedMap d m) = act d <$> M.lookup k m
28+
29+insert :: (Ord k, Act d v, Group d) => k -> v -> ShiftedMap d k v -> ShiftedMap d k v
30+insert k v (ShiftedMap d m) = ShiftedMap d $ M.insert k ((act . invert) d v) m
31+
32+shift :: (Semigroup d) => d -> ShiftedMap d k v -> ShiftedMap d k v
33+shift d' (ShiftedMap d m) = ShiftedMap (d <> d') m
34+
35+liftMap :: Monoid d => Map k v -> ShiftedMap d k v
36+liftMap m = ShiftedMap mempty m
37+
38+unshift :: Act d v => ShiftedMap d k v -> Map k v
39+unshift (ShiftedMap d m) = act d <$> m
src/Tix/Typechecker.hs+17−6
@@ -15,15 +15,20 @@ import Control.Monad.Freer.Internal (handleRelayS)
15import Control.Monad.Freer.Reader
15import Control.Monad.Freer.Reader
16import Control.Monad.Freer.State
16import Control.Monad.Freer.State
17import Control.Monad.Freer.Writer
17import Control.Monad.Freer.Writer
18+import Data.Act
18import Data.Fix
19import Data.Fix
19import Data.Foldable
20import Data.Foldable
20import Data.Functor
21import Data.Functor
21import Data.Functor.Classes
22import Data.Functor.Classes
23+import Data.Group
22import Data.List.NonEmpty (NonEmpty (..))
24import Data.List.NonEmpty (NonEmpty (..))
23import qualified Data.List.NonEmpty as NE
25import qualified Data.List.NonEmpty as NE
26+import Data.Map.Shifted.Strict (ShiftedMap (..))
27+import qualified Data.Map.Shifted.Strict as SM
24import Data.Map.Strict (Map)
28import Data.Map.Strict (Map)
25import qualified Data.Map.Strict as M
29import qualified Data.Map.Strict as M
26import Data.MonoTraversable
30import Data.MonoTraversable
31+import Data.Monoid
27import Data.Range (Range (..))
32import Data.Range (Range (..))
28import qualified Data.Range as R
33import qualified Data.Range as R
29import Data.Sequence (Seq (..))
34import Data.Sequence (Seq (..))
@@ -174,16 +179,22 @@ isClosed (x :-> y) = isClosed x && isClosed y
174isClosed (List x) = isClosed x
179isClosed (List x) = isClosed x
175isClosed (NAttrSet xs) = all isClosed . M.elems $ xs
180isClosed (NAttrSet xs) = all isClosed . M.elems $ xs
176
181
182+newtype DeBrujinContext = DeBrujinContext (Sum Int)
183+ deriving newtype (Eq, Ord, Show, Semigroup, Monoid, Group, Num)
184+
185+instance Act DeBrujinContext DeBrujin where
186+ act (DeBrujinContext (Sum n)) (DeBrujin i j) = DeBrujin (i + n) j
187+
177close :: Range TypeVariable -> NType -> NType
188close :: Range TypeVariable -> NType -> NType
178close range =
189close range =
179 run
190 run
180− . evalState @(Map TypeVariable DeBrujin) M.empty
191+ . evalState @(ShiftedMap DeBrujinContext TypeVariable DeBrujin) mempty
181 . runReader @Int 0
192 . runReader @Int 0
182 . evalState @Int 0
193 . evalState @Int 0
183 . close'
194 . close'
184 where
195 where
185 -- State is the sequential number, Reader is the binding context number
196 -- State is the sequential number, Reader is the binding context number
186− close' :: NType -> Eff '[State Int, Reader Int, State (Map TypeVariable DeBrujin)] NType
197+ close' :: NType -> Eff '[State Int, Reader Int, State (ShiftedMap DeBrujinContext TypeVariable DeBrujin)] NType
187 close' x@(NAtomic _) = return x
198 close' x@(NAtomic _) = return x
188 close' x@(NBrujin _) = return x
199 close' x@(NBrujin _) = return x
189 close' (NTypeVariable tv) | tv `R.member` range = NBrujin <$> newbrujin tv
200 close' (NTypeVariable tv) | tv `R.member` range = NBrujin <$> newbrujin tv
@@ -192,18 +203,18 @@ close range =
192 close' (NAttrSet x) = bndCtx $ NAttrSet <$> traverse close' x
203 close' (NAttrSet x) = bndCtx $ NAttrSet <$> traverse close' x
193
204
194 bndCtx m = do
205 bndCtx m = do
195− modify @(Map TypeVariable DeBrujin) (fmap (\(DeBrujin i j) -> DeBrujin (i + 1) j))
206+ modify @(ShiftedMap DeBrujinContext TypeVariable DeBrujin) (SM.shift 1)
196 x <- local @Int (+ 1) m
207 x <- local @Int (+ 1) m
197− modify @(Map TypeVariable DeBrujin) (fmap (\(DeBrujin i j) -> DeBrujin (i - 1) j))
208+ modify @(ShiftedMap DeBrujinContext TypeVariable DeBrujin) (SM.shift (-1))
198 return x
209 return x
199 newbrujin t = do
210 newbrujin t = do
200− get @(Map TypeVariable DeBrujin) <&> M.lookup t >>= \case
211+ get @(ShiftedMap DeBrujinContext TypeVariable DeBrujin) <&> SM.lookup t >>= \case
201 Nothing -> do
212 Nothing -> do
202 i <- ask
213 i <- ask
203 j <- get
214 j <- get
204 modify @Int (+ 1)
215 modify @Int (+ 1)
205 let x = DeBrujin i j
216 let x = DeBrujin i j
206− modify @(Map TypeVariable DeBrujin) (M.insert t x)
217+ modify @(ShiftedMap DeBrujinContext TypeVariable DeBrujin) (SM.insert t x)
207 return x
218 return x
208 Just x -> return x
219 Just x -> return x
209
220
stack.yaml+8
@@ -37,6 +37,14 @@ packages:
37extra-deps:
37extra-deps:
38 - hnix-0.10.1
38 - hnix-0.10.1
39 - prettyprinter-1.7.0
39 - prettyprinter-1.7.0
40+ - acts-0.3.1.0
41+ - finitary-2.0.0.0
42+ - groups-0.4.1.0
43+ - typelits-witnesses-0.4.0.0
44+ - dependent-sum-0.7.1.0
45+ - constraints-extras-0.3.0.2
46+
47+allow-newer: true
40# - acme-missiles-0.3
48# - acme-missiles-0.3
41# - git: https://github.com/commercialhaskell/stack.git
49# - git: https://github.com/commercialhaskell/stack.git
42# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
50# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a