@@ -3,7 +3,6 @@ module Tix.Types
33 AtomicType (..),
44 DeBruijn (..),
55 TypeVariable (..),
6− showNType,
76 Scheme (..),
87 scheme,
98 Pred (..),
@@ -17,20 +16,20 @@ module Tix.Types
1716where
1817
1918import Control.Lens hiding (List)
19+import Control.Monad.Freer
20+import Control.Monad.Freer.Reader
2021import Data.Bifunctor
2122import Data.Data (Data)
2223import Data.Data.Lens
23−import Data.Foldable
2424import Data.Generics.Sum.Subtype
25−import qualified Data.List as L
2625import Data.Map (Map)
2726import qualified Data.Map as M
2827import qualified Data.Map.MultiKey.Strict as MKM
2928import Data.Set (Set)
3029import qualified Data.Set as S
3130import Data.Text (Text)
32−import qualified Data.Text.Lazy as TL
33−import qualified Data.Text.Lazy.Builder as T
31+import qualified Data.Text as T
32+import Debug.Trace
3433import GHC.Exts
3534import Generic.Data
3635import Prettyprinter
@@ -118,6 +117,9 @@ data AtomicType
118117 | URI
119118 deriving stock (Eq, Ord, Show, Data, Generic)
120119
120+instance Pretty AtomicType where
121+ pretty = viaShow
122+
121123data DeBruijn = DeBruijn !Int !Int
122124 deriving stock (Show, Eq, Ord, Data)
123125
@@ -128,43 +130,92 @@ newtype TypeVariable = TypeVariable Int
128130instance Show TypeVariable where
129131 show (TypeVariable n) = "〚" <> show n <> "〛"
130132
131−-- | Show a type which has already been closed over.
132−--
133−-- TODO: This should be a Prettyprinter
134−showNType :: Scheme -> Text
135−showNType t = TL.toStrict . T.toLazyText $ showNType' 0 t
133+instance Pretty TypeVariable where
134+ pretty (TypeVariable n) = "〚" <> pretty n <> "〛"
135+
136+instance Pretty DeBruijn where
137+ pretty (DeBruijn i j) = "〚" <> pretty i <+> pretty j <> "〛"
138+
139+instance Pretty NType where
140+ pretty t = greekifyWith t $ prettyNType t
141+
142+instance Pretty Scheme where
143+ pretty t = greekifyWith t $ prettyScheme t
144+
145+greekifyWith :: Data t => t -> Eff '[Reader (Map DeBruijn Text), Reader Depth] x -> x
146+greekifyWith t =
147+ run
148+ . runReader (Depth 0)
149+ . runReader (M.fromList $ zip (S.toList $ getAllDeBurjins t) variableNames)
150+
151+newtype Depth = Depth Int
152+
153+descend :: Member (Reader Depth) eff => Eff eff x -> Eff eff x
154+descend = local (\(Depth n) -> Depth $ n + 1)
155+
156+getDepthedDeBurjins :: (Data x, Member (Reader Depth) eff) => x -> Eff eff (Set DeBruijn)
157+getDepthedDeBurjins x = do
158+ Depth depth <- ask
159+ return $ S.mapMonotonic (DeBruijn (- depth)) $ getDeBurjins x
160+
161+getDeBurjin :: (Members '[Reader Depth, Reader (Map DeBruijn Text)] eff) => DeBruijn -> Eff eff (Maybe Text)
162+getDeBurjin (DeBruijn i j) = do
163+ Depth depth <- ask
164+ M.lookup (DeBruijn (i - depth) j) <$> ask
165+
166+type PrettyM a = forall eff. Members '[Reader Depth, Reader (Map DeBruijn Text)] eff => Eff eff a
167+
168+prettyNType :: NType -> PrettyM (Doc ann)
169+prettyNType (NTypeVariable x) = return $ pretty x
170+prettyNType (NBruijn x) =
171+ getDeBurjin x <&> \case
172+ Nothing -> pretty x
173+ Just t -> pretty t
174+prettyNType (NAtomic x) = return $ pretty x
175+prettyNType (x :-> y) = descend $ do
176+ x' <- prettyNType x
177+ y' <- prettyNType y
178+ return $ group $ x' <+> "->" <> line <> y'
179+prettyNType (List x) = descend $ do
180+ x' <- prettyNType x
181+ return $ group $ bracketed "[" "]" x'
182+prettyNType (NAttrSet m) = descend $ do
183+ decls <- prettyDecl `traverse` M.toAscList m
184+ return $ group $ bracketed "{" "}" $ vsep decls
185+ where
186+ prettyDecl :: (Text, Scheme) -> PrettyM (Doc ann)
187+ prettyDecl (name, sch) = do
188+ sch' <- prettyScheme sch
189+ return $ group $ pretty name <+> "=" <> nest 2 (line <> sch' <> ";")
190+
191+bracketed :: Doc ann -> Doc ann -> Doc ann -> Doc ann
192+bracketed l r d = flatAlt (l <> " ") l <> nest 2 d <> line' <> r
193+
194+prettyScheme :: Scheme -> PrettyM (Doc ann)
195+prettyScheme u@(Preds cs :=> t) = do
196+ greekVars <- ask @(Map DeBruijn Text)
197+ foralls <-
198+ getDepthedDeBurjins (traceShowId u) <&> \s -> case M.elems . M.restrictKeys greekVars $ traceShowId s of
199+ [] -> mempty
200+ 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'
136207 where
137− greekVars = M.fromList $ zip (S.toList $ getAllDeBurjins t) variableNames
138− showNType' :: Int -> Scheme -> T.Builder
139− showNType' depth (Preds ps :=> u) =
140− foralls <> predicates <> case u of
141− (NAtomic a) -> showAtomicType a
142− (NBruijn (DeBruijn i j)) -> greekVars M.! DeBruijn (i - depth) j
143− (NTypeVariable _) -> error "should not have free type variables at this point"
144− (x :-> y) -> showNextNType' (scheme x) <> " -> " <> showNextNType' (scheme y)
145− (List x) -> "[" <> showNextNType' (scheme x) <> "]"
146− (NAttrSet x) ->
147− "{ "
148− <> ( mconcat
149− . L.intersperse "; "
150− . fmap (\(k, v) -> T.fromText k <> " = " <> showNextNType' v)
151− $ M.toList x
152− )
153− <> " }"
154− where
155− showNextNType' = showNType' $ depth + 1
156− currBurjins = S.mapMonotonic (DeBruijn (- depth)) $ getDeBurjins u
157− foralls =
158− if S.null currBurjins
159− then ""
160− else
161− "∀ "
162− <> (mconcat . L.intersperse " " . M.elems $ M.restrictKeys greekVars currBurjins)
163− <> ". "
164− predicates =
165− if null ps
166− then mempty
167− else "(" <> (fold . L.intersperse ", " $ T.fromString . show <$> ps) <> ") => "
208+ prettyPred :: Pred -> PrettyM (Doc ann)
209+ prettyPred (h `HasField` (k, v)) = do
210+ h' <- prettyNType h
211+ v' <- prettyScheme v
212+ return $ group $ group (h' <> nest 2 (line' <> "." <> pretty k <+> "=")) <> nest 2 (line <> v')
213+ prettyPred (Update x y z) = do
214+ x' <- prettyNType x
215+ y' <- prettyNType y
216+ z' <- prettyNType z
217+ return $ group $ paren x' <+> "//" <> line <> paren y' <+> "~" <> line <> paren z'
218+ paren = bracketed "(" ")"
168219
169220-- | Returns the set of all De Bruijn type variables relative to the outermost
170221-- (current) binding context.
@@ -184,7 +235,7 @@ getAllDeBurjins =
184235-- | Get all De Bruijn type variables that were bound in the the outermost
185236-- (current) binding context.
186237-- Only returns the second indexes.
187−getDeBurjins :: NType -> Set Int
238+getDeBurjins :: Data x => x -> Set Int
188239getDeBurjins t = getDeBurjins' t 0
189240
190241-- | Gets all De Bruijn variables with the given binding context offset.
@@ -203,39 +254,9 @@ getDeBurjins' =
203254 TTypeVariable _ -> const S.empty
204255 )
205256
206−showAtomicType :: AtomicType -> T.Builder
207−showAtomicType Integer = "Integer"
208−showAtomicType Float = "Float"
209−showAtomicType Bool = "Bool"
210−showAtomicType String = "String"
211−showAtomicType Path = "Path"
212−showAtomicType Null = "Null"
213−showAtomicType URI = "URI"
214−
215−greek :: [T.Builder]
257+greek :: [Text]
216258greek = ["α", "β", "γ", "δ", "ε", "ζ", "η", "θ", "ι", "κ", "λ", "μ", "ν", "ξ", "ο", "π", "ρ", "σ", "τ", "υ", "φ", "χ", "ψ", "ω"]
217259
218−variableNames :: [T.Builder]
260+variableNames :: [Text]
219261variableNames =
220− greek <> fmap (\(n, g) -> g <> T.fromString (show n)) (zip [1 :: Int ..] greek)
221−
222−instance Pretty NType where
223− pretty (NAtomic a) = viaShow a
224− pretty (NTypeVariable t) = viaShow t
225− pretty (NBruijn (DeBruijn i j)) = "⟦" <> pretty i <+> pretty j <> "⟧"
226− pretty (x :-> y) = sep [pretty x, "->" <+> pretty y]
227− pretty (List x) = "[" <> align (pretty x) <> "]"
228− pretty (NAttrSet x) =
229− sep
230− [ flatAlt "{ " "{"
231− <+> align
232− ( sep . zipWith (<+>) ("" : repeat ";")
233− . map (\(k, v) -> pretty k <+> "=" <+> align (pretty v))
234− $ M.toList x
235− ),
236− "}"
237− ]
238−
239−instance Pretty Scheme where
240− pretty ([] :=> t) = pretty t
241− pretty (cs :=> t) = viaShow cs <+> "=>" <+> pretty t
262+ greek <> fmap (\(n, g) -> g <> T.pack (show n)) (zip [1 :: Int ..] greek)