@@ -9,8 +9,12 @@ module Tix.Typechecker
99 )
1010where
1111
12+import qualified Algebra.Graph.AdjacencyMap.Algorithm as AM
13+import qualified Algebra.Graph.Class as G
14+import qualified Algebra.Graph.NonEmpty.AdjacencyMap as AM
1215import Control.Lens hiding (Empty, List, cons, equality, set, set')
1316import Control.Monad
17+import qualified Control.Monad.Free as F
1418import Control.Monad.Freer
1519import Control.Monad.Freer.Fresh
1620import Control.Monad.Freer.Internal (handleRelayS)
@@ -25,6 +29,7 @@ import Data.Foldable
2529import Data.Functor.Contravariant
2630import Data.Group hiding ((~~))
2731import Data.List.NonEmpty (NonEmpty (..))
32+import qualified Data.List.NonEmpty as NE
2833import qualified Data.Map.MultiKey.Strict as MKM
2934import Data.Map.Shifted.Strict (ShiftedMap (..))
3035import qualified Data.Map.Shifted.Strict as SM
@@ -35,7 +40,7 @@ import Data.MonoTraversable
3540import Data.Monoid
3641import qualified Data.RangeSet.Map as RS
3742import Data.Sequence (Seq (..))
38−import Data.Sequences
43+import Data.Sequences hiding (catMaybes)
3944import Data.Set (Set)
4045import qualified Data.Set as S
4146import Data.Text (Text)
@@ -48,6 +53,7 @@ import Nix.Atoms
4853import Nix.Expr
4954import Nix.Pretty
5055import Tix.Types
56+import Prelude as P
5157
5258getType :: NExprLoc -> (Scheme, [(SrcSpan, Errors)], [InferError], [UnifyingError], [PredicateError], A.Object)
5359getType r =
@@ -210,6 +216,7 @@ unifySchemes :: Predicate TypeVariable -> [(Scheme, Scheme)] -> UnifyM Substitut
210216unifySchemes _ [] = pure mempty
211217unifySchemes f ((x, y) : rest) = do
212218 s <- unifyScheme f x y
219+ -- TODO: This should probably be (s <>)
213220 sub s <$> unifySchemes f (sub s rest)
214221
215222unifyScheme :: Predicate TypeVariable -> Scheme -> Scheme -> UnifyM Substitution
@@ -266,7 +273,7 @@ data PredicateError
266273 deriving stock (Eq, Show)
267274
268275data InferError
269− = ConflictingBindingDefinitions NormalizedBinding' NormalizedBinding'
276+ = ConflictingBindingDefinitions (NormalizedBinding' NExprLoc) (NormalizedBinding' NExprLoc)
270277 deriving stock (Show)
271278
272279type UnifyM x = forall r. Members '[Writer UnifyingError] r => Eff r x
@@ -438,6 +445,10 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
438445 defT ~~ resT
439446 return resT
440447 NSet NNonRecursive xs -> NAttrSet <$> inferBinding xs
448+ NSet NRecursive xs -> NAttrSet <$> inferRecBinding xs
449+ NLet bindings body -> do
450+ bindingsT <- inferRecBinding bindings
451+ withBindings bindingsT $ infer body
441452 NHasAttr attrSet path -> do
442453 setT <- infer attrSet
443454 -- this should infer optional type
@@ -460,9 +471,6 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
460471 return (setT, maybe M.empty (`M.singleton` scheme setT) binding <> setBindings)
461472 bodyT <- withBindings varMap $ infer body
462473 return $ paramT :-> bodyT
463− NLet bindings body -> do
464− bindingsT <- inferBinding bindings
465− withBindings bindingsT $ infer body
466474 NIf cond t f -> do
467475 condT <- infer cond
468476 condT ~~ NAtomic Bool
@@ -519,12 +527,11 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
519527 lhst ~~ NAtomic Bool
520528 return $ NAtomic Bool
521529
522−data NormalizedBinding' = NBType !NExprLoc | NBAttrSet !NormalizedBinding
523− deriving stock (Show)
530+type NormalizedBinding' = F.Free (Map VarName)
524531
525−type NormalizedBinding = Map VarName NormalizedBinding'
532+type NormalizedBinding x = Map VarName (NormalizedBinding' x)
526533
527−normalizeBindings :: Member (Writer InferError) eff => [Binding NExprLoc] -> Eff eff NormalizedBinding
534+normalizeBindings :: Member (Writer InferError) eff => [Binding NExprLoc] -> Eff eff (NormalizedBinding NExprLoc)
528535normalizeBindings bindings = case bindings' of
529536 [] -> return M.empty
530537 (x : xs) ->
@@ -532,18 +539,18 @@ normalizeBindings bindings = case bindings' of
532539 -- This is really sub-optimal
533540 foldl (\u -> M.unionWith (\i j -> i >>= \i' -> j >>= mergeBindings i') u . fmap pure) (fmap pure x) xs
534541 where
535− mergeBindings (NBAttrSet lhs) (NBAttrSet rhs) =
536− fmap NBAttrSet . sequence $
542+ mergeBindings (F.Free lhs) (F.Free rhs) =
543+ fmap F.Free . sequence $
537544 -- This is really sub-optimal
538545 M.unionWith (\x y -> x >>= \x' -> y >>= mergeBindings x') (pure <$> lhs) (pure <$> rhs)
539546 mergeBindings x y = do
540547 tell $ ConflictingBindingDefinitions x y
541548 return x
542− fromName :: NonEmpty VarName -> NExprLoc -> NormalizedBinding
543− fromName (n :| ns) x = M.singleton n $ foldr (\u t -> NBAttrSet $ M.singleton u t) (NBType x) ns
549+ fromName :: NonEmpty VarName -> x -> NormalizedBinding x
550+ fromName (n :| ns) x = M.singleton n $ foldr (\u t -> F.Free $ M.singleton u t) (F.Pure x) ns
544551 bindings' =
545552 bindings >>= \case
546− (NamedVar path r src) ->
553+ (NamedVar path r _src) ->
547554 case getPath path of
548555 Nothing -> [] -- TODO: This should be an error (?)
549556 Just name -> pure $ fromName name r
@@ -554,53 +561,188 @@ normalizeBindings bindings = case bindings' of
554561 Just set -> \v -> Fix $ Compose $ Ann (SrcSpan src src) $ NSelect set (pure $ StaticKey v) Nothing
555562 in (\v -> fromName (pure v) (f v)) <$> names
556563
557−inferNormalizedBindings' :: NormalizedBinding' -> InferM' Scheme
558−inferNormalizedBindings' (NBType expr) = inferGeneral expr
559−inferNormalizedBindings' (NBAttrSet m) = scheme . NAttrSet <$> inferNormalizedBindings' `traverse` m
560−
561−inferNormalizedBindings :: NormalizedBinding -> InferM' (Map VarName Scheme)
564+inferNormalizedBindings :: NormalizedBinding NExprLoc -> InferM' (Map VarName Scheme)
562565inferNormalizedBindings = traverse inferNormalizedBindings'
566+ where
567+ inferNormalizedBindings' :: NormalizedBinding' NExprLoc -> InferM' Scheme
568+ inferNormalizedBindings' (F.Pure expr) = inferGeneral expr
569+ inferNormalizedBindings' (F.Free m) = scheme . NAttrSet <$> inferNormalizedBindings' `traverse` m
570+
571+inferNormalizedBindingsRecursive :: NormalizedBinding NExprLoc -> InferM' (Map VarName Scheme)
572+inferNormalizedBindingsRecursive n = do
573+ let components = case AM.topSort . AM.scc $ bindingGraph n of
574+ Left x -> [foldMap AM.vertexSet x]
575+ Right x -> AM.vertexSet <$> P.reverse x
576+ fmap toScheme <$> inferComponents n components
577+ where
578+ toScheme :: NormalizedBinding' Scheme -> Scheme
579+ toScheme (F.Pure t) = t
580+ toScheme (F.Free m) = scheme $ NAttrSet $ fmap toScheme m
581+
582+inferComponents :: NormalizedBinding NExprLoc -> [Set (NonEmpty VarName)] -> InferM' (NormalizedBinding Scheme)
583+inferComponents _ [] = pure M.empty
584+inferComponents n ((S.toList -> paths) : otherComponents) = do
585+ let bindings = catMaybes $ paths <&> \path -> (path,) <$> lookupExpr path n
586+ (types, p, preds, s) <-
587+ traceSubtree (showExpr . bindingsToNExpr $ bindings)
588+ . inferGeneral' (NAttrSet . fmap toScheme)
589+ $ do
590+ tvsExprs <- for bindings (\(a, b) -> (a,b,) . NTypeVariable <$> freshSrc)
591+ let tvsExprs' =
592+ foldl' (M.unionWith mergeBindings) M.empty $
593+ fmap (\(a, b, c) -> normalize a (b, c)) tvsExprs
594+ tvs = toScheme . fmap snd <$> tvsExprs'
595+
596+ -- (type, tv)
597+ tvsTypes <-
598+ withBindings tvs $
599+ tvsExprs' & traverse . traverse . _1 %%~ infer
600+ for_ tvsTypes $ traverse (uncurry (~~))
601+ return $ fmap fst <$> tvsTypes
602+ -- TODO: There should probably be some smarter predicate filtering
603+ schemes <- types & traverse . traverse %%~ (\t -> solveAndClose p $ sub s $ preds :=> t)
604+ fmap (M.unionWith mergeBindings schemes) . withBindings (toScheme' <$> schemes) $
605+ inferComponents n otherComponents
606+ where
607+ bindingToNExpr :: NonEmpty VarName -> NExprLoc -> Binding NExpr
608+ bindingToNExpr name expr = NamedVar (StaticKey <$> name) (stripAnnotation expr) nullPos
609+
610+ bindingsToNExpr :: [(NonEmpty VarName, NExprLoc)] -> NExpr
611+ bindingsToNExpr bs = Fix $ NSet NNonRecursive $ fmap (uncurry bindingToNExpr) bs
612+
613+ normalize :: NonEmpty VarName -> x -> NormalizedBinding x
614+ normalize (NESingle x) t = M.singleton x (F.Pure t)
615+ normalize (x :|| xs) t = M.singleton x (F.Free $ normalize xs t)
616+
617+ mergeBindings :: NormalizedBinding' x -> NormalizedBinding' x -> NormalizedBinding' x
618+ mergeBindings (F.Free lhs) (F.Free rhs) = F.Free $ M.unionWith mergeBindings lhs rhs
619+ -- This should have been taken care of when constructing the structures.
620+ mergeBindings _ _ = error "not possible"
621+
622+ toScheme :: NormalizedBinding' NType -> Scheme
623+ toScheme (F.Pure t) = scheme t
624+ toScheme (F.Free m) = scheme $ NAttrSet $ fmap toScheme m
625+
626+ toScheme' :: NormalizedBinding' Scheme -> Scheme
627+ toScheme' (F.Pure t) = t
628+ toScheme' (F.Free m) = scheme $ NAttrSet $ fmap toScheme' m
629+
630+ -- Returns Just only if it is the tip.
631+ -- This is what we want because non-tip elements are also part of the call graph.
632+ lookupExpr :: NonEmpty VarName -> NormalizedBinding x -> Maybe x
633+ lookupExpr (NESingle x) m =
634+ M.lookup x m >>= \case
635+ F.Pure a -> Just a
636+ F.Free _ -> Nothing
637+ lookupExpr (x :|| xs) m =
638+ M.lookup x m >>= \case
639+ F.Pure _ -> Nothing
640+ F.Free a -> lookupExpr xs a
641+
642+bindingGraph :: forall g. (G.Graph g, G.Vertex g ~ NonEmpty VarName) => NormalizedBinding NExprLoc -> g
643+bindingGraph n = G.overlays . fmap (\(k, v) -> getGraph (pure k) v) . M.toList $ n
644+ where
645+ getGraph :: NonEmpty VarName -> NormalizedBinding' NExprLoc -> g
646+ getGraph p (F.Pure e) = G.star p (P.filter (elemBindingSet n) $ getReferences e)
647+ getGraph p (F.Free m) = G.star p (fmap fst attrs) `G.overlay` G.overlays (fmap (uncurry getGraph) attrs)
648+ where
649+ attrs = (\(k, v) -> (p <> pure k, v)) <$> M.toList m
650+ elemBindingSet :: NormalizedBinding x -> NonEmpty VarName -> Bool
651+ elemBindingSet m = elemBindingSet' m . NE.toList
652+ elemBindingSet' :: NormalizedBinding x -> [VarName] -> Bool
653+ elemBindingSet' _ [] = True
654+ elemBindingSet' m (x : xs) = case M.lookup x m of
655+ Nothing -> False
656+ Just (F.Free next) -> elemBindingSet' next xs
657+ Just (F.Pure _) -> case xs of
658+ [] -> True
659+ _ -> False
660+
661+getReferences :: NExprLoc -> [NonEmpty VarName]
662+getReferences expr@(Fix (Compose (Ann _ x))) = case x of
663+ NConstant _ -> []
664+ NLiteralPath _ -> []
665+ NEnvPath _ -> []
666+ NStr _ -> []
667+ NSym var -> [pure var]
668+ NList xs -> foldMap getReferences xs
669+ NUnary _ a -> getReferences a
670+ NBinary _ a b -> getReferences a <> getReferences b
671+ NSelect {} -> case processSelect expr of
672+ (Nothing, other) -> other
673+ (Just p, other) -> pure p <> other
674+ NSet _ xs -> foldMap getReferences $ xs >>= toList -- This is not strictly correct
675+ NHasAttr a _ -> getReferences a
676+ NAbs _ a -> getReferences a -- This is not strictly correct
677+ NLet a b -> foldMap getReferences (a >>= toList) <> getReferences b -- This is not strictly correct
678+ NIf a b c -> getReferences a <> getReferences b <> getReferences c -- This is not strictly correct
679+ NWith a b -> getReferences a <> getReferences b -- This is not strictly correct
680+ NAssert a b -> getReferences a <> getReferences b
681+ NSynHole _ -> []
682+ where
683+ processSelect :: NExprLoc -> (Maybe (NonEmpty VarName), [NonEmpty VarName])
684+ processSelect u@(Fix (Compose (Ann _ y))) = case y of
685+ NSym var -> (Just $ pure var, [])
686+ NSelect l h m -> fmap
687+ (join (maybeToList (getReferences <$> m)) <>)
688+ $ case getPath h of
689+ Nothing -> (Nothing, getReferences l)
690+ Just p -> case processSelect l of
691+ (Just path, other) -> (Just $ path <> p, other)
692+ (Nothing, other) -> (Nothing, other)
693+ _ -> (Nothing, getReferences u)
563694
564695inferBinding :: [Binding NExprLoc] -> InferM' (Map VarName Scheme)
565696inferBinding = normalizeBindings >=> inferNormalizedBindings
566697
698+inferRecBinding :: [Binding NExprLoc] -> InferM' (Map VarName Scheme)
699+inferRecBinding = normalizeBindings >=> inferNormalizedBindingsRecursive
700+
567701renderPretty :: Pretty x => x -> TL.Text
568702renderPretty = renderLazy . layoutPretty defaultLayoutOptions . pretty
569703
570−showExpr :: Fix NExprLocF -> Text
571−showExpr = TL.toStrict . renderLazy . layoutPretty defaultLayoutOptions . P.group . prettyNix . stripAnnotation
704+showExpr :: NExpr -> Text
705+showExpr = TL.toStrict . renderLazy . layoutPretty defaultLayoutOptions . P.group . prettyNix
572706
573707inferGeneral :: NExprLoc -> InferM Scheme
574−inferGeneral x@(Fix (Compose (Ann src _))) = runReader src $
575− traceSubtree (showExpr x) $ do
576− (((t, subs), cs), range) <-
577− traceSubtree "subexpressions" . registerTypeVariables . runConstraintEnv $ infer x
578− traceSubtree "received" $ do
579− traceValue "type" $ renderPretty t
580− traceValue "substitutions" $ prettySubstitution subs
581− traceValue "constraints" $ fmap renderPretty cs
582− traceValue "range" $ T.pack . show $ range
583− get @(MKM.Map Pred) >>= traceValue "preds" . showPreds
584− s' <- solveWithPriority (Predicate (`RS.member` range)) cs
585− traceValue "substitutions_after_solving" $ prettySubstitution s'
586− let s = subs <> s'
587− returnedS = Substitution . M.filterWithKey (\k _ -> k `RS.notMember` range) . unSubstitution $ s
588− traceSubtree "returned" $ do
589− traceValue "substitutions" $ prettySubstitution returnedS
590− -- Filter for optimization purposes
591− subEnv returnedS
592− preds <- get @(MKM.Map Pred)
593− traceValue "subbed_preds" $ showPreds preds
594− let p = Predicate (`RS.member` range) <> Predicate (`S.notMember` free returnedS)
595− (MKM.toList -> keep, toss) = MKM.partition (getPredicate p) preds
596− -- At this point the only predicates only contain type variables that are only used
597− -- in the expression. This means that all of the generated constraints and
598− -- substitutions can be safely restricted to this expression.
599− retT <- solveAndClose p $ sub s $ keep :=> t
600− traceValue "preds" $ showPreds toss
601− put toss
602− traceValue "type" $ renderPretty retT
603− return retT
708+inferGeneral x@(Fix (Compose (Ann src _))) = runReader src . traceSubtree (showExpr . stripAnnotation $ x) $ do
709+ (t, p, keep, s) <- inferGeneral' id $ infer x
710+ solveAndClose p $ sub s $ keep :=> t
711+
712+inferGeneral' ::
713+ (Members InferEffs r, Pretty y) =>
714+ (x -> y) ->
715+ Eff (SubstituteEnv : Writer Substitution : Writer Constraint : State (Seq Constraint) : r) x ->
716+ Eff r (x, Predicate TypeVariable, [Pred], Substitution)
717+inferGeneral' toPretty f = do
718+ (((x, subs), cs), range) <-
719+ traceSubtree "subexpressions" . registerTypeVariables . runConstraintEnv $ f
720+ traceSubtree "received" $ do
721+ traceValue "type" $ renderPretty $ toPretty x
722+ traceValue "substitutions" $ prettySubstitution subs
723+ traceValue "constraints" $ fmap renderPretty cs
724+ traceValue "range" $ T.pack . show $ range
725+ get @(MKM.Map Pred) >>= traceValue "preds" . showPreds
726+ s' <- solveWithPriority (Predicate (`RS.member` range)) cs
727+ traceValue "substitutions_after_solving" $ prettySubstitution s'
728+ let s = subs <> s'
729+ returnedS = Substitution . M.filterWithKey (\k _ -> k `RS.notMember` range) . unSubstitution $ s
730+ traceSubtree "returned" $ do
731+ traceValue "substitutions" $ prettySubstitution returnedS
732+ -- Filter for optimization purposes
733+ subEnv returnedS
734+ preds <- get @(MKM.Map Pred)
735+ traceValue "subbed_preds" $ showPreds preds
736+ let p = Predicate (`RS.member` range) <> Predicate (`S.notMember` free returnedS)
737+ (keep', toss) = MKM.partition (getPredicate p) preds
738+ keep = MKM.toList keep'
739+ -- At this point the only predicates only contain type variables that are only used
740+ -- in the expression. This means that all of the generated constraints and
741+ -- substitutions can be safely restricted to this expression.
742+ traceValue "preds" $ showPreds toss
743+ traceValue "keep_preds" $ showPreds keep'
744+ put toss
745+ return (x, p, keep, s)
604746 where
605747 showPreds :: MKM.Map Pred -> Map String String
606748 showPreds = M.mapKeys show . fmap show . MKM.toMap
@@ -746,13 +888,33 @@ lookupAttrSet ::
746888 r =>
747889 AttrSetPath ->
748890 Eff r (NType, TypeVariable)
749−lookupAttrSet (p :| []) = do
891+lookupAttrSet (NESingle p) = do
750892 set <- NTypeVariable <$> freshSrc
751893 var <- freshSrc
752894 tell (HasField set (p, scheme . NTypeVariable $ var))
753895 return (set, var)
754−lookupAttrSet (p :| (pp : ps)) = do
896+lookupAttrSet (p :|| ps) = do
755897 set <- NTypeVariable <$> freshSrc
756− (innerSet, var) <- lookupAttrSet (pp :| ps)
898+ (innerSet, var) <- lookupAttrSet ps
757899 tell $ HasField set (p, scheme innerSet)
758900 return (set, var)
901+
902+-- NonEmpty patterns
903+
904+pattern (:||) :: x -> NonEmpty x -> NonEmpty x
905+pattern (:||) x xs <-
906+ ( \case
907+ (a :| (aa : aaa)) -> Just (a, aa :| aaa)
908+ _ -> Nothing ->
909+ Just (x, xs)
910+ )
911+ where
912+ x :|| xs = NE.cons x xs
913+
914+pattern NESingle :: x -> NonEmpty x
915+pattern NESingle x <-
916+ x :| []
917+ where
918+ NESingle x = x :| []
919+
920+{-# COMPLETE (:||), NESingle #-}