@@ -6,10 +6,9 @@ module Tix.Types
66 Scheme (..),
77 scheme,
88 Pred (..),
9− (=>>),
109 (//),
1110 Preds (..),
12− traverseNTypesWith,
11+ TraversableNTypes (..),
1312 traverseNTypes,
1413 TerminalNType (..),
1514 )
@@ -21,7 +20,6 @@ import Control.Monad.Freer.Reader
2120import Data.Bifunctor
2221import Data.Data (Data)
2322import Data.Data.Lens
24−import Data.Generics.Sum.Subtype
2523import Data.Map (Map)
2624import qualified Data.Map as M
2725import qualified Data.Map.MultiKey.Strict as MKM
@@ -33,7 +31,6 @@ import Debug.Trace
3331import GHC.Exts
3432import Generic.Data
3533import Prettyprinter
36−import Type.Reflection
3734
3835data Pred
3936 = -- | '(x // y) ~ z'
@@ -54,6 +51,7 @@ instance MKM.Keyable Pred where
5451-- this seems bad. It should not drop constraints.
5552(//) :: NType -> NType -> NType -> Pred
5653(//) = Update
54+{-# INLINE (//) #-}
5755
5856data Scheme = Preds :=> !NType
5957 deriving stock (Eq, Ord, Show, Data, Generic)
@@ -62,12 +60,9 @@ newtype Preds = Preds {unPreds :: [Pred]}
6260 deriving newtype (Show, Eq, Ord, Semigroup, Monoid, IsList)
6361 deriving stock (Data, Generic)
6462
65−(=>>) :: Preds -> Scheme -> Scheme
66−[] =>> x = x
67−xs =>> (ys :=> u) = (xs <> ys) :=> u
68−
6963scheme :: NType -> Scheme
7064scheme t = [] :=> t
65+{-# INLINE scheme #-}
7166
7267data TerminalNType
7368 = TAtomic !AtomicType
@@ -75,26 +70,50 @@ data TerminalNType
7570 | TBruijn !DeBruijn
7671 deriving stock (Show, Generic)
7772
78−traverseNTypesWith ::
79− (Data s, Applicative f) => (forall x. f x -> f x) -> (TerminalNType -> f TerminalNType) -> s -> f s
80−traverseNTypesWith ctx f s = case eqTypeRep (typeOf s) (typeRep @NType) of
81− Just HRefl | Just _ <- projectSub @TerminalNType s -> _Sub @TerminalNType f s
82− Just HRefl -> ctx $ (template @_ @NType . traverseNTypesWith ctx) f s
83− _ -> (template @_ @NType . traverseNTypesWith ctx) f s
84−{-# SPECIALIZE traverseNTypesWith ::
85− Applicative f => (forall x. f x -> f x) -> (TerminalNType -> f TerminalNType) -> NType -> f NType
86− #-}
87−{-# SPECIALIZE traverseNTypesWith ::
88− Applicative f => (forall x. f x -> f x) -> (TerminalNType -> f TerminalNType) -> Scheme -> f Scheme
89− #-}
90−{-# SPECIALIZE traverseNTypesWith ::
91− Monoid r => (forall x. Const r x -> Const r x) -> (TerminalNType -> Const r TerminalNType) -> NType -> Const r NType
92− #-}
93−{-# SPECIALIZE traverseNTypesWith ::
94− Monoid r => (forall x. Const r x -> Const r x) -> (TerminalNType -> Const r TerminalNType) -> Scheme -> Const r Scheme
95− #-}
96−
97−traverseNTypes :: Data s => Traversal' s TerminalNType
73+class TraversableNTypes s where
74+ traverseNTypesWith ::
75+ (Applicative f) => (forall x. f x -> f x) -> (TerminalNType -> f TerminalNType) -> s -> f s
76+
77+instance TraversableNTypes NType where
78+ traverseNTypesWith ctx f = \case
79+ NAtomic a -> f' $ TAtomic a
80+ NTypeVariable a -> f' $ TTypeVariable a
81+ NBruijn a -> f' $ TBruijn a
82+ x :-> y -> ctx $ (:->) <$> traverseNextType x <*> traverseNextType y
83+ List t -> ctx $ List <$> traverseNextType t
84+ NAttrSet m -> ctx $ NAttrSet <$> traverseNTypesWith ctx f `traverse` m
85+ where
86+ traverseNextType = traverseNTypesWith ctx f
87+ f' = fmap fromTerminalNType . f
88+ fromTerminalNType :: TerminalNType -> NType
89+ fromTerminalNType = \case
90+ TAtomic a -> NAtomic a
91+ TTypeVariable a -> NTypeVariable a
92+ TBruijn a -> NBruijn a
93+ {-# INLINE traverseNTypesWith #-}
94+
95+instance TraversableNTypes Scheme where
96+ traverseNTypesWith ctx f (cs :=> t) =
97+ ctx $
98+ (:=>) <$> traverseNTypesWith ctx f cs <*> traverseNTypesWith ctx f t
99+ {-# INLINE traverseNTypesWith #-}
100+
101+instance TraversableNTypes Preds where
102+ traverseNTypesWith ctx f (Preds ps) = Preds <$> traverseNTypesWith ctx f `traverse` ps
103+ {-# INLINE traverseNTypesWith #-}
104+
105+instance TraversableNTypes Pred where
106+ traverseNTypesWith ctx f = \case
107+ (HasField t (k, h)) ->
108+ HasField <$> traverseNTypesWith ctx f t <*> ((k,) <$> traverseNTypesWith ctx f h)
109+ (Update x y z) ->
110+ Update
111+ <$> traverseNTypesWith ctx f x
112+ <*> traverseNTypesWith ctx f y
113+ <*> traverseNTypesWith ctx f z
114+ {-# INLINE traverseNTypesWith #-}
115+
116+traverseNTypes :: TraversableNTypes s => Traversal' s TerminalNType
98117traverseNTypes = traverseNTypesWith id
99118{-# INLINE traverseNTypes #-}
100119
@@ -142,7 +161,7 @@ instance Pretty NType where
142161instance Pretty Scheme where
143162 pretty t = greekifyWith t $ prettyScheme t
144163
145−greekifyWith :: Data t => t -> Eff '[Reader (Map DeBruijn Text), Reader Depth] x -> x
164+greekifyWith :: TraversableNTypes t => t -> Eff '[Reader (Map DeBruijn Text), Reader Depth] x -> x
146165greekifyWith t =
147166 run
148167 . runReader (Depth 0)
@@ -153,7 +172,7 @@ newtype Depth = Depth Int
153172descend :: Member (Reader Depth) eff => Eff eff x -> Eff eff x
154173descend = local (\(Depth n) -> Depth $ n + 1)
155174
156−getDepthedDeBurjins :: (Data x, Member (Reader Depth) eff) => x -> Eff eff (Set DeBruijn)
175+getDepthedDeBurjins :: (TraversableNTypes x, Member (Reader Depth) eff) => x -> Eff eff (Set DeBruijn)
157176getDepthedDeBurjins x = do
158177 Depth depth <- ask
159178 return $ S.mapMonotonic (DeBruijn (- depth)) $ getDeBurjins x
@@ -198,12 +217,13 @@ prettyScheme u@(Preds cs :=> t) = do
198217 getDepthedDeBurjins (traceShowId u) <&> \s -> case M.elems . M.restrictKeys greekVars $ traceShowId s of
199218 [] -> mempty
200219 foralls -> "∀" <+> fillSep (pretty <$> foralls) <> "." <> line
201− cs' <-
202− prettyPred `traverse` cs <&> \case
203− [] -> mempty
204− cs' -> group (paren (vsep $ punctuate "," cs') <+> "=>" <> line)
205− t' <- prettyNType t
206− return $ group $ foralls <> cs' <> t'
220+ descend $ do
221+ cs' <-
222+ prettyPred `traverse` cs <&> \case
223+ [] -> mempty
224+ cs' -> group (paren (vsep $ punctuate "," cs') <+> "=>" <> line)
225+ t' <- prettyNType t
226+ return $ group $ foralls <> cs' <> t'
207227 where
208228 prettyPred :: Pred -> PrettyM (Doc ann)
209229 prettyPred (h `HasField` (k, v)) = do
@@ -221,7 +241,7 @@ prettyScheme u@(Preds cs :=> t) = do
221241-- (current) binding context.
222242-- So variables that are bound in one of the inner contexts will have a negative
223243-- binding context number.
224−getAllDeBurjins :: Data x => x -> Set DeBruijn
244+getAllDeBurjins :: TraversableNTypes x => x -> Set DeBruijn
225245getAllDeBurjins =
226246 view $
227247 traverseNTypesWith (first $ S.mapMonotonic (\(DeBruijn i j) -> DeBruijn (i - 1) j))
@@ -235,12 +255,12 @@ getAllDeBurjins =
235255-- | Get all De Bruijn type variables that were bound in the the outermost
236256-- (current) binding context.
237257-- Only returns the second indexes.
238−getDeBurjins :: Data x => x -> Set Int
258+getDeBurjins :: TraversableNTypes x => x -> Set Int
239259getDeBurjins t = getDeBurjins' t 0
240260
241261-- | Gets all De Bruijn variables with the given binding context offset.
242262-- Only returns the second indexes.
243−getDeBurjins' :: Data x => x -> Int -> Set Int
263+getDeBurjins' :: TraversableNTypes x => x -> Int -> Set Int
244264getDeBurjins' =
245265 view $
246266 traverseNTypesWith (\(Const f) -> Const (\n -> f (n + 1)))