@@ -10,15 +10,18 @@ module Tix.Types
1010 (=>>),
1111 (//),
1212 Preds (..),
13− foldNTypeM,
14− foldNType,
15− NTypeFolder (..),
13+ traverseNTypesWith,
14+ traverseNTypes,
15+ TerminalNType (..),
1616 )
1717where
1818
19−import Control.Applicative
19+import Control.Lens hiding (List)
20+import Data.Bifunctor
21+import Data.Data (Data)
22+import Data.Data.Lens
2023import Data.Foldable
21−import Data.Functor.Identity
24+import Data.Generics.Sum.Subtype
2225import qualified Data.List as L
2326import Data.Map (Map)
2427import qualified Data.Map as M
@@ -30,6 +33,7 @@ import qualified Data.Text.Lazy.Builder as T
3033import GHC.Exts
3134import Generic.Data
3235import Prettyprinter
36+import Type.Reflection
3337
3438data Pred
3539 = -- | '(x // y) ~ z'
@@ -41,17 +45,18 @@ data Pred
4145 !NType
4246 -- ^ z
4347 | !NType `HasField` !(Text, Scheme)
44− deriving stock (Eq, Ord, Show)
48+ deriving stock (Eq, Ord, Show, Data, Generic)
4549
4650-- this seems bad. It should not drop constraints.
4751(//) :: Scheme -> Scheme -> Scheme -> Pred
4852(//) (_ :=> x) (_ :=> y) (_ :=> z) = Update x y z
4953
5054data Scheme = Preds :=> !NType
51− deriving stock (Eq, Ord, Show)
55+ deriving stock (Eq, Ord, Show, Data, Generic)
5256
5357newtype Preds = Preds {unPreds :: [Pred]}
5458 deriving newtype (Show, Eq, Ord, Semigroup, Monoid, IsList)
59+ deriving stock (Data, Generic)
5560
5661(=>>) :: Preds -> Scheme -> Scheme
5762[] =>> x = x
@@ -60,52 +65,34 @@ xs =>> (ys :=> u) = (xs <> ys) :=> u
6065scheme :: NType -> Scheme
6166scheme t = [] :=> t
6267
63−data NTypeFolder a = NTypeFolder
64− { variableFolder :: TypeVariable -> a,
65− deBruijnFolder :: DeBruijn -> a,
66− atomicFolder :: AtomicType -> a,
67− compositeFolder :: a -> a
68− }
69− deriving stock (Generic)
70− deriving (Semigroup, Monoid) via Generically (NTypeFolder a)
71−
72−class TypeFoldable t where
73− foldNTypeM :: (Applicative m, Monoid a) => NTypeFolder (m a) -> t -> m a
74−
75−instance TypeFoldable Scheme where
76− foldNTypeM tf (Preds ps :=> t) = foldA [foldAType tf ps, foldNTypeM tf t]
77−
78−instance TypeFoldable a => TypeFoldable [a] where
79− foldNTypeM tf = foldAType tf
80−
81−instance TypeFoldable Pred where
82− foldNTypeM tf (Update x y z) = foldAType tf [x, y, z]
83− foldNTypeM tf (HasField x (_, z)) = foldA [foldNTypeM tf x, foldNTypeM tf z]
84−
85−instance TypeFoldable NType where
86− foldNTypeM NTypeFolder {variableFolder = f} (NTypeVariable x) = f x
87− foldNTypeM NTypeFolder {deBruijnFolder = f} (NBruijn x) = f x
88− foldNTypeM NTypeFolder {atomicFolder = f} (NAtomic x) = f x
89− foldNTypeM tf@NTypeFolder {compositeFolder = f} (x :-> y) = f $ foldAType tf [x, y]
90− foldNTypeM tf@NTypeFolder {compositeFolder = f} (List x) = f $ foldNTypeM tf x
91− foldNTypeM tf@NTypeFolder {compositeFolder = f} (NAttrSet x) = f $ foldAType tf $ M.elems x
92−
93−foldNType :: (Monoid a, TypeFoldable x) => NTypeFolder a -> x -> a
94−foldNType NTypeFolder {..} = runIdentity . foldNTypeM tf
95− where
96− tf =
97− NTypeFolder
98− { variableFolder = Identity . variableFolder,
99− deBruijnFolder = Identity . deBruijnFolder,
100− atomicFolder = Identity . atomicFolder,
101− compositeFolder = Identity . compositeFolder . runIdentity
102− }
103−
104−foldAType :: (Monoid a, Applicative f, TypeFoldable t) => NTypeFolder (f a) -> [t] -> f a
105−foldAType tf ne = foldA $ fmap (foldNTypeM tf) ne
106−
107−foldA :: (Monoid a, Applicative f) => [f a] -> f a
108−foldA = foldr (liftA2 (<>)) (pure mempty)
68+data TerminalNType
69+ = TAtomic !AtomicType
70+ | TTypeVariable !TypeVariable
71+ | TBruijn !DeBruijn
72+ deriving stock (Show, Generic)
73+
74+traverseNTypesWith ::
75+ (Data s, Applicative f) => (forall x. f x -> f x) -> (TerminalNType -> f TerminalNType) -> s -> f s
76+traverseNTypesWith ctx f s = case eqTypeRep (typeOf s) (typeRep @NType) of
77+ Just HRefl | Just _ <- projectSub @TerminalNType s -> _Sub @TerminalNType f s
78+ Just HRefl -> ctx $ (template @_ @NType . traverseNTypesWith ctx) f s
79+ _ -> (template @_ @NType . traverseNTypesWith ctx) f s
80+{-# SPECIALIZE traverseNTypesWith ::
81+ Applicative f => (forall x. f x -> f x) -> (TerminalNType -> f TerminalNType) -> NType -> f NType
82+ #-}
83+{-# SPECIALIZE traverseNTypesWith ::
84+ Applicative f => (forall x. f x -> f x) -> (TerminalNType -> f TerminalNType) -> Scheme -> f Scheme
85+ #-}
86+{-# SPECIALIZE traverseNTypesWith ::
87+ Monoid r => (forall x. Const r x -> Const r x) -> (TerminalNType -> Const r TerminalNType) -> NType -> Const r NType
88+ #-}
89+{-# SPECIALIZE traverseNTypesWith ::
90+ Monoid r => (forall x. Const r x -> Const r x) -> (TerminalNType -> Const r TerminalNType) -> Scheme -> Const r Scheme
91+ #-}
92+
93+traverseNTypes :: Data s => Traversal' s TerminalNType
94+traverseNTypes = traverseNTypesWith id
95+{-# INLINE traverseNTypes #-}
10996
11097data NType
11198 = NTypeVariable !TypeVariable
@@ -114,7 +101,7 @@ data NType
114101 | !Scheme :-> !Scheme
115102 | List !Scheme
116103 | NAttrSet !(Map Text Scheme)
117− deriving stock (Eq, Ord, Show)
104+ deriving stock (Eq, Ord, Show, Data, Generic)
118105
119106data AtomicType
120107 = Integer
@@ -124,13 +111,14 @@ data AtomicType
124111 | Path
125112 | Null
126113 | URI
127− deriving stock (Eq, Ord, Show)
114+ deriving stock (Eq, Ord, Show, Data, Generic)
128115
129116data DeBruijn = DeBruijn !Int !Int
130− deriving stock (Show, Eq, Ord)
117+ deriving stock (Show, Eq, Ord, Data)
131118
132119newtype TypeVariable = TypeVariable Int
133120 deriving newtype (Eq, Ord, Enum, Bounded)
121+ deriving stock (Data)
134122
135123instance Show TypeVariable where
136124 show (TypeVariable n) = "〚" <> show n <> "〛"
@@ -177,15 +165,16 @@ showNType t = TL.toStrict . T.toLazyText $ showNType' 0 t
177165-- (current) binding context.
178166-- So variables that are bound in one of the inner contexts will have a negative
179167-- binding context number.
180−getAllDeBurjins :: TypeFoldable x => x -> Set DeBruijn
168+getAllDeBurjins :: Data x => x -> Set DeBruijn
181169getAllDeBurjins =
182− foldNType
183− NTypeFolder
184− { variableFolder = const S.empty,
185− deBruijnFolder = S.singleton,
186− atomicFolder = const S.empty,
187− compositeFolder = S.mapMonotonic (\(DeBruijn i j) -> DeBruijn (i - 1) j)
188− }
170+ view $
171+ traverseNTypesWith (first $ S.mapMonotonic (\(DeBruijn i j) -> DeBruijn (i - 1) j))
172+ . to
173+ ( \case
174+ TAtomic _ -> S.empty
175+ TBruijn b -> S.singleton b
176+ TTypeVariable _ -> S.empty
177+ )
189178
190179-- | Get all De Bruijn type variables that were bound in the the outermost
191180-- (current) binding context.
@@ -195,17 +184,19 @@ getDeBurjins t = getDeBurjins' t 0
195184
196185-- | Gets all De Bruijn variables with the given binding context offset.
197186-- Only returns the second indexes.
198−getDeBurjins' :: TypeFoldable x => x -> Int -> Set Int
187+getDeBurjins' :: Data x => x -> Int -> Set Int
199188getDeBurjins' =
200− foldNType
201− NTypeFolder
202− { variableFolder = \_ _ -> S.empty,
203− deBruijnFolder = \t n -> case t of
204− DeBruijn m j | m == n -> S.singleton j
205− _ -> S.empty,
206− atomicFolder = \_ _ -> S.empty,
207− compositeFolder = \f n -> f (n + 1)
208− }
189+ view $
190+ traverseNTypesWith (\(Const f) -> Const (\n -> f (n + 1)))
191+ . to
192+ ( \case
193+ TAtomic _ -> const S.empty
194+ TBruijn (DeBruijn m j) -> \n ->
195+ if m == n
196+ then S.singleton j
197+ else S.empty
198+ TTypeVariable _ -> const S.empty
199+ )
209200
210201showAtomicType :: AtomicType -> T.Builder
211202showAtomicType Integer = "Integer"