@@ -5,6 +5,7 @@ module Tix.Typechecker
55 runSeqWriter,
66 getType,
77 showNType,
8+ runNoTreeTracer,
89 )
910where
1011
@@ -15,13 +16,14 @@ import Control.Monad.Freer.Reader
1516import Control.Monad.Freer.State
1617import Control.Monad.Freer.Writer
1718import Data.Act
19+import qualified Data.Aeson as A
1820import Data.Fix
1921import Data.Foldable
2022import Data.Functor
2123import Data.Group hiding ((~~))
24+import qualified Data.HashMap.Strict as HM
2225import Data.List.NonEmpty (NonEmpty (..))
2326import qualified Data.List.NonEmpty as NE
24−import qualified Data.Map.Extra as M
2527import Data.Map.Shifted.Strict (ShiftedMap (..))
2628import qualified Data.Map.Shifted.Strict as SM
2729import Data.Map.Strict (Map)
@@ -37,9 +39,13 @@ import qualified Data.Set as S
3739import Data.Text (Text)
3840import qualified Data.Text.Lazy as TL
3941import qualified Data.Text.Lazy.Builder as T
42+import Data.Text.Prettyprint.Doc as P
43+import Data.Text.Prettyprint.Doc.Render.Text
4044import Data.Traversable
45+import qualified Data.Vector as V
4146import Nix.Atoms
4247import Nix.Expr
48+import Nix.Pretty
4349
4450runConstraintEnv ::
4551 Eff (SubstituteEnv : Writer Substitution : Writer Constraint : State (Seq Constraint) : effs) a ->
@@ -55,9 +61,9 @@ runConstraintEnv =
5561 return ()
5662 )
5763
58−getType :: NExprLoc -> (NType, [(SrcSpan, Errors)], [UnifyingError])
64+getType :: NExprLoc -> (NType, [(SrcSpan, Errors)], [UnifyingError], A.Object)
5965getType r =
60− let (((((t, unifying), errs), srcs), subs), _) =
66+ let ((((((t, traceTree), unifying), errs), srcs), subs), _) =
6167 run
6268 . runConstraintEnv
6369 . runState @[(TypeVariable, SrcSpan)] []
@@ -66,8 +72,9 @@ getType r =
6672 . runSeqWriter @[UnifyingError]
6773 . runReader (M.empty :: VariableMap)
6874 . runFresh
75+ . runTreeTracer
6976 $ inferGeneral r
70− in (sub subs t, errs, unifying)
77+ in (sub subs t, errs, unifying, traceTree)
7178
7279data SubstituteEnv a where
7380 SubstituteEnv :: Substitution -> SubstituteEnv ()
@@ -84,6 +91,9 @@ instance Show TypeVariable where
8491data Constraint = !NType :~ !NType
8592 deriving stock (Eq, Ord, Show)
8693
94+instance Pretty Constraint where
95+ pretty (x :~ y) = pretty x <+> "~" <+> pretty y
96+
8797data DeBrujin = DeBrujin !Int !Int
8898 deriving stock (Show, Eq, Ord)
8999
@@ -240,9 +250,32 @@ instance Free NType where
240250 free (NAttrSet attrs) = foldMap free . M.elems $ attrs
241251 free (x :-> y) = free x <> free y
242252
253+instance Pretty NType where
254+ pretty (NTypeVariable t) = pretty $ prettyTypeVariable t
255+ pretty (NBrujin (DeBrujin i j)) = "⟦" <> pretty i <+> pretty j <> "⟧"
256+ pretty (NAtomic a) = viaShow a
257+ pretty (x :-> y) = sep [pretty x, "->" <+> pretty y]
258+ pretty (List x) = "[" <> align (pretty x) <> "]"
259+ pretty (NAttrSet x) =
260+ sep
261+ [ flatAlt "{ " "{"
262+ <+> align
263+ ( sep . zipWith (<+>) ("" : repeat ";")
264+ . map (\(k, v) -> pretty k <+> "=" <+> align (pretty v))
265+ $ M.toList x
266+ ),
267+ "}"
268+ ]
269+
243270newtype Substitution = Substitution {unSubstitution :: Map TypeVariable NType}
244271 deriving newtype (Eq, Ord, Show)
245272
273+prettyTypeVariable :: TypeVariable -> TL.Text
274+prettyTypeVariable (TypeVariable n) = "⟦" <> (TL.pack . show) n <> "⟧"
275+
276+prettySubstitution :: Substitution -> A.Value
277+prettySubstitution = A.toJSON . M.mapKeysMonotonic prettyTypeVariable . fmap renderPretty . unSubstitution
278+
246279-- | Prefers the left
247280instance Semigroup Substitution where
248281 x'@(Substitution x) <> (Substitution y) = Substitution (x <> fmap (sub x') y)
@@ -375,7 +408,8 @@ type InferEffs =
375408 Writer (SrcSpan, Errors),
376409 Reader VariableMap,
377410 Writer UnifyingError,
378− SubstituteEnv
411+ SubstituteEnv,
412+ TreeTracer
379413 ]
380414
381415type InferM x = forall r. Members InferEffs r => Eff r x
@@ -580,15 +614,29 @@ inferBinding bindings = do
580614-- (_ : (x, _) : _) -> traceM $ x <> " " <> s <> " \t" <> show a
581615-- _ -> traceM $ s <> " \t" <> show a
582616
617+renderPretty :: Pretty x => x -> TL.Text
618+renderPretty = renderLazy . layoutPretty defaultLayoutOptions . pretty
619+
620+showExpr :: Fix NExprLocF -> Text
621+showExpr = TL.toStrict . renderLazy . layoutPretty defaultLayoutOptions . P.group . prettyNix . stripAnnotation
622+
583623inferGeneral :: NExprLoc -> InferM NType
584−inferGeneral x = do
585− (((t, subs), cs), range) <- registerTypeVariables . runConstraintEnv $ infer x
624+inferGeneral x = traceSubtree (showExpr x) $ do
625+ (((t, subs), cs), range) <-
626+ traceSubtree "subexpressions" . registerTypeVariables . runConstraintEnv $ infer x
627+ traceValue "received_type" $ renderPretty t
628+ traceValue "received_substitutions" $ prettySubstitution subs
629+ traceValue "received_constraints" $ fmap renderPretty cs
586630 s' <- solveWithPriority range cs
631+ traceValue "substitutions_after_solving" $ prettySubstitution s'
587632 let s = subs <> s'
588633 returnedS = Substitution . M.filterWithKey (\k _ -> k `R.notMember` range) . unSubstitution $ s
634+ traceValue "returned_substitutions" $ prettySubstitution returnedS
589635 -- Filter for optimization purposes
590636 subEnv returnedS
591− return . close range $ sub s t
637+ let retT = close range $ sub s t
638+ traceValue "returned_type" $ renderPretty retT
639+ return retT
592640
593641expectAttrSet :: Members '[Reader SrcSpan, Writer (SrcSpan, Errors)] r => NType -> Eff r VariableMap
594642expectAttrSet (NAttrSet x) = return x
@@ -676,3 +724,26 @@ lookupAttrSet path = go (NE.toList path)
676724 expectAttrSet x <&> M.lookup p >>= \case
677725 Nothing -> NTypeVariable <$> throwSrcTV (KeyNotPresent p)
678726 Just t -> go ps t
727+
728+data TreeTracer a where
729+ TraceTree :: A.Object -> TreeTracer ()
730+
731+traceValue :: (A.ToJSON v, Member TreeTracer eff) => Text -> v -> Eff eff ()
732+traceValue k v = send $ TraceTree $ k A..= v
733+
734+traceSubtree :: Member TreeTracer eff => Text -> Eff eff a -> Eff eff a
735+traceSubtree k = interpose (\(TraceTree o) -> send $ TraceTree (k A..= o))
736+
737+runTreeTracer :: Eff (TreeTracer ': eff) a -> Eff eff (a, A.Object)
738+runTreeTracer = handleRelayS HM.empty (\s x -> pure (x, s)) $ \s (TraceTree o) k ->
739+ k (HM.unionWith unionToList s o) ()
740+ where
741+ unionToList :: A.Value -> A.Value -> A.Value
742+ unionToList (A.Array x) (A.Array y) = A.Array $ x <> y
743+ unionToList (A.Array x) y = A.Array $ V.snoc x y
744+ unionToList x (A.Array y) = A.Array $ V.cons x y
745+ unionToList (A.Object x) (A.Object y) = A.Object $ HM.unionWith unionToList x y
746+ unionToList x y = A.Array $ V.fromList [x, y]
747+
748+runNoTreeTracer :: Eff (TreeTracer ': eff) a -> Eff eff a
749+runNoTreeTracer = interpret (\(TraceTree _) -> return ())