@@ -10,10 +10,15 @@ module Tix.Types
1010 (=>>),
1111 (//),
1212 Preds (..),
13+ foldNTypeM,
14+ foldNType,
15+ NTypeFolder (..),
1316 )
1417where
1518
19+import Control.Applicative
1620import Data.Foldable
21+import Data.Functor.Identity
1722import qualified Data.List as L
1823import Data.Map (Map)
1924import qualified Data.Map as M
@@ -23,6 +28,7 @@ import Data.Text (Text)
2328import qualified Data.Text.Lazy as TL
2429import qualified Data.Text.Lazy.Builder as T
2530import GHC.Exts
31+import Generic.Data
2632import Prettyprinter
2733
2834data Pred
@@ -37,13 +43,11 @@ data Pred
3743 | !NType `HasField` !(Text, Scheme)
3844 deriving stock (Eq, Ord, Show)
3945
46+-- this seems bad. It should not drop constraints.
4047(//) :: Scheme -> Scheme -> Scheme -> Pred
4148(//) (_ :=> x) (_ :=> y) (_ :=> z) = Update x y z
42−(//) _ _ _ = error "Bad update operator" -- This should not be an 'error'
4349
44−data Scheme
45− = Preds :=> !NType
46− | NAtomic !AtomicType
50+data Scheme = Preds :=> !NType
4751 deriving stock (Eq, Ord, Show)
4852
4953newtype Preds = Preds {unPreds :: [Pred]}
@@ -52,14 +56,61 @@ newtype Preds = Preds {unPreds :: [Pred]}
5256(=>>) :: Preds -> Scheme -> Scheme
5357[] =>> x = x
5458xs =>> (ys :=> u) = (xs <> ys) :=> u
55−_ =>> (NAtomic _) = error "Can not constrain atomic type"
5659
5760scheme :: NType -> Scheme
5861scheme t = [] :=> t
5962
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)
109+
60110data NType
61111 = NTypeVariable !TypeVariable
62112 | NBruijn !DeBruijn
113+ | NAtomic !AtomicType
63114 | !Scheme :-> !Scheme
64115 | List !Scheme
65116 | NAttrSet !(Map Text Scheme)
@@ -92,9 +143,9 @@ showNType t = TL.toStrict . T.toLazyText $ showNType' 0 t
92143 where
93144 greekVars = M.fromList $ zip (S.toList $ getAllDeBurjins t) variableNames
94145 showNType' :: Int -> Scheme -> T.Builder
95− showNType' _ (NAtomic a) = showAtomicType a
96146 showNType' depth (Preds ps :=> u) =
97147 foralls <> predicates <> case u of
148+ (NAtomic a) -> showAtomicType a
98149 (NBruijn (DeBruijn i j)) -> greekVars M.! DeBruijn (i - depth) j
99150 (NTypeVariable _) -> error "should not have free type variables at this point"
100151 (x :-> y) -> showNextNType' x <> " -> " <> showNextNType' y
@@ -126,55 +177,35 @@ showNType t = TL.toStrict . T.toLazyText $ showNType' 0 t
126177-- (current) binding context.
127178-- So variables that are bound in one of the inner contexts will have a negative
128179-- binding context number.
129−getAllDeBurjins :: Scheme -> Set DeBruijn
130−getAllDeBurjins (NAtomic _) = S.empty
131−getAllDeBurjins (Preds ps :=> t) =
132− foldMap
133− ( \case
134− (Update x y z) ->
135− bndCtx $
136− getAllTypeDeBurjins x <> getAllTypeDeBurjins y <> getAllTypeDeBurjins z
137− (HasField x (_, y)) -> bndCtx $ getAllTypeDeBurjins x <> getAllDeBurjins y
138− )
139− ps
140− <> case t of
141− (NTypeVariable _) -> S.empty
142− (NBruijn x) -> S.singleton x
143− (x :-> y) -> bndCtx $ getAllDeBurjins x <> getAllDeBurjins y
144− (List x) -> bndCtx $ getAllDeBurjins x
145− (NAttrSet xs) -> bndCtx . foldMap getAllDeBurjins . M.elems $ xs
146− where
147− bndCtx = S.mapMonotonic (\(DeBruijn i j) -> DeBruijn (i - 1) j)
148−
149−getAllTypeDeBurjins :: NType -> Set DeBruijn
150−getAllTypeDeBurjins = getAllDeBurjins . scheme
180+getAllDeBurjins :: TypeFoldable x => x -> Set DeBruijn
181+getAllDeBurjins =
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+ }
151189
152190-- | Get all De Bruijn type variables that were bound in the the outermost
153191-- (current) binding context.
154192-- Only returns the second indexes.
155193getDeBurjins :: NType -> Set Int
156−getDeBurjins = getDeBurjins' 0
194+getDeBurjins t = getDeBurjins' t 0
157195
158196-- | Gets all De Bruijn variables with the given binding context offset.
159197-- Only returns the second indexes.
160−getDeBurjins' :: Int -> NType -> Set Int
161−getDeBurjins' _ (NTypeVariable _) = S.empty
162−getDeBurjins' n (NBruijn (DeBruijn m j)) | m == n = S.singleton j
163−getDeBurjins' _ (NBruijn _) = S.empty
164−getDeBurjins' n (x :-> y) = getSchemeDeBurjins' (n + 1) x <> getSchemeDeBurjins' (n + 1) y
165−getDeBurjins' n (List x) = getSchemeDeBurjins' (n + 1) x
166−getDeBurjins' n (NAttrSet xs) = foldMap (getSchemeDeBurjins' (n + 1)) . M.elems $ xs
167−
168−getSchemeDeBurjins' :: Int -> Scheme -> Set Int
169−getSchemeDeBurjins' _ (NAtomic _) = S.empty
170−getSchemeDeBurjins' n (Preds ps :=> t) =
171− getDeBurjins' n t
172− <> foldMap
173− ( \case
174− Update x y z -> getDeBurjins' n x <> getDeBurjins' n y <> getDeBurjins' n z
175− HasField u (_, v) -> getDeBurjins' n u <> getSchemeDeBurjins' n v
176− )
177− ps
198+getDeBurjins' :: TypeFoldable x => x -> Int -> Set Int
199+getDeBurjins' =
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+ }
178209
179210showAtomicType :: AtomicType -> T.Builder
180211showAtomicType Integer = "Integer"
@@ -193,6 +224,7 @@ variableNames =
193224 greek <> fmap (\(n, g) -> g <> T.fromString (show n)) (zip [1 :: Int ..] greek)
194225
195226instance Pretty NType where
227+ pretty (NAtomic a) = viaShow a
196228 pretty (NTypeVariable t) = viaShow t
197229 pretty (NBruijn (DeBruijn i j)) = "⟦" <> pretty i <+> pretty j <> "⟧"
198230 pretty (x :-> y) = sep [pretty x, "->" <+> pretty y]
@@ -209,6 +241,5 @@ instance Pretty NType where
209241 ]
210242
211243instance Pretty Scheme where
212− pretty (NAtomic a) = viaShow a
213244 pretty ([] :=> t) = pretty t
214245 pretty (cs :=> t) = viaShow cs <+> "=>" <+> pretty t