on master help sign in
Normalized bindings
commita8834431fe64dd6d6cfd7df79bc9d21b949d07aa authoriko <ilyakooo0@gmail.com> dateSun 11 Apr 2021, 14:23 (6 years ago) parentb71b0eb
4 files changed+66−46
app/Main.hs+2−1 package.yaml+1 src/Tix/Typechecker.hs+61−43 test/src/Main.hs+2−2
app/Main.hs+2−1
@@ -13,9 +13,10 @@ main = do
1313 case parseNixTextLoc inp of
1414 Failure err -> error $ show err
1515 Success r -> do
16− let (t, errs, uErrs, pErrs, o) = getType r
16+ let (t, errs, infErr, uErrs, pErrs, o) = getType r
1717 BSC.putStrLn . YAML.encode $
1818 o <> "errors" .= fmap show errs
1919 <> "unifying_errors" .= fmap show uErrs
2020 <> "resulting_type" .= renderPretty t
2121 <> "predicate_errors" .= fmap show pErrs
22+ <> "infer_errors" .= fmap show infErr
package.yaml+1
@@ -99,3 +99,4 @@ default-extensions:
9999 - TypeFamilies
100100 - FlexibleInstances
101101 - DeriveAnyClass
102+ - ConstraintKinds
src/Tix/Typechecker.hs+61−43
@@ -30,6 +30,7 @@ import Data.Map.Shifted.Strict (ShiftedMap (..))
3030import qualified Data.Map.Shifted.Strict as SM
3131import Data.Map.Strict (Map)
3232import qualified Data.Map.Strict as M
33+import Data.Maybe
3334import Data.MonoTraversable
3435import Data.Monoid
3536import qualified Data.RangeSet.Map as RS
@@ -48,9 +49,9 @@ import Nix.Expr
4849import Nix.Pretty
4950import Tix.Types
5051
51−getType :: NExprLoc -> (Scheme, [(SrcSpan, Errors)], [UnifyingError], [PredicateError], A.Object)
52+getType :: NExprLoc -> (Scheme, [(SrcSpan, Errors)], [InferError], [UnifyingError], [PredicateError], A.Object)
5253getType r =
53− let (((((((t, traceTree), predicate), unifying), errs), _srcs), subs), _) =
54+ let ((((((((t, traceTree), inf), predicate), unifying), errs), _srcs), subs), _) =
5455 run
5556 . evalState @(MKM.Map Pred) mempty
5657 . interpret @(Writer Pred) (\(Tell x) -> modify (<> MKM.singleton x))
@@ -61,10 +62,11 @@ getType r =
6162 . runSeqWriter @[(SrcSpan, Errors)]
6263 . runSeqWriter @[UnifyingError]
6364 . runSeqWriter @[PredicateError]
65+ . runSeqWriter @[InferError]
6466 . runFresh
6567 . runTreeTracer
6668 $ inferGeneral r
67− in (sub subs t, errs, unifying, predicate, traceTree)
69+ in (sub subs t, errs, inf, unifying, predicate, traceTree)
6870
6971runConstraintEnv ::
7072 Members '[State VariableMap, State (MKM.Map Pred)] effs =>
@@ -197,7 +199,7 @@ unifyWithPriority f (lhs :~ rhs) =
197199 (NTypeVariable t, x) -> t <<- x
198200 (x, NTypeVariable t) -> t <<- x
199201 (List x, List y) -> unifyWithPriority f $ x :~ y
200− (NAttrSet _x, NAttrSet _y) -> error "TODO: This should be handled in a special way"
202+ (NAttrSet _x, NAttrSet _y) -> error $ "TODO: This should be handled in a special way " <> show _x <> show _y
201203 -- foldr (\c s -> s >>= \s' -> (<> s') <$> unifyWithPriority f (sub s' c)) (pure mempty)
202204 -- . M.elems
203205 -- $ M.intersectionWith (:~) x y
@@ -246,6 +248,10 @@ data PredicateError
246248 | NotAnAttributeSet NType
247249 deriving stock (Eq, Show)
248250
251+data InferError
252+ = ConflictingBindingDefinitions NormalizedBinding' NormalizedBinding'
253+ deriving stock (Show)
254+
249255type UnifyM x = forall r. Members '[Writer UnifyingError] r => Eff r x
250256
251257type InferEffs =
@@ -258,6 +264,7 @@ type InferEffs =
258264 State (MKM.Map Pred),
259265 State VariableMap,
260266 Writer UnifyingError,
267+ Writer InferError,
261268 SubstituteEnv,
262269 TreeTracer
263270 ]
@@ -398,7 +405,7 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
398405 NBinary NImpl lhs rhs -> logic lhs rhs
399406 NSelect r path' def -> do
400407 setT <- infer r
401− path <- getPath path'
408+ let path = getPath path'
402409 resT <-
403410 NTypeVariable <$> case path of
404411 Just p -> do
@@ -495,39 +502,50 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
495502 lhst ~~ NAtomic Bool
496503 return $ NAtomic Bool
497504
498−inferBinding :: [Binding (Fix NExprLocF)] -> InferM' (Map VarName Scheme)
499−inferBinding bindings = do
500− bindings' <-
501− bindings >>.= \case
502− (NamedVar path r src) -> do
503− getPath path >>= \case
504− Nothing -> return []
505− Just name -> do
506− t <- inferGeneral r
507− return [stack ((,) <$> name) (scheme . NAttrSet . uncurry M.singleton) t]
508− Inherit attrSet keys src -> do
509− names <- catMaybes <$> traverse getKeyName keys
510− attrSet' <- infer `traverse` attrSet
511− names' <- for names $ \name ->
512− fmap (name,) <$> do
513− case attrSet' of
514− Just t -> do
515− (s', var) <- lookupAttrSet (pure name)
516− s' ~~ t
517− return $ Just . scheme . NTypeVariable $ var
518− Nothing -> do
519− vars <- get @VariableMap
520− return $ case M.lookup name vars of
521− Nothing -> Nothing
522− Just r -> Just r
523− return $ catMaybes names'
524− return $ M.fromListWith mergeSetTypes bindings'
505+data NormalizedBinding' = NBType !NExprLoc | NBAttrSet !NormalizedBinding
506+ deriving stock (Show)
507+
508+type NormalizedBinding = Map VarName NormalizedBinding'
509+
510+normalizeBindings :: Member (Writer InferError) eff => [Binding NExprLoc] -> Eff eff NormalizedBinding
511+normalizeBindings bindings = case bindings' of
512+ [] -> return M.empty
513+ (x : xs) ->
514+ sequence $
515+ -- This is really sub-optimal
516+ foldl (\u -> M.unionWith (\i j -> i >>= \i' -> j >>= mergeBindings i') u . fmap pure) (fmap pure x) xs
525517 where
526− -- This seems fishy
527− mergeSetTypes :: Scheme -> Scheme -> Scheme
528− mergeSetTypes (xcs :=> NAttrSet ks) (ycs :=> NAttrSet ks') =
529− (xcs <> ycs) :=> NAttrSet (M.unionWith mergeSetTypes ks ks')
530− mergeSetTypes _ x = x
518+ mergeBindings (NBAttrSet lhs) (NBAttrSet rhs) =
519+ fmap NBAttrSet . sequence $
520+ -- This is really sub-optimal
521+ M.unionWith (\x y -> x >>= \x' -> y >>= mergeBindings x') (pure <$> lhs) (pure <$> rhs)
522+ mergeBindings x y = do
523+ tell $ ConflictingBindingDefinitions x y
524+ return x
525+ fromName :: NonEmpty VarName -> NExprLoc -> NormalizedBinding
526+ fromName (n :| ns) x = M.singleton n $ foldr (\u t -> NBAttrSet $ M.singleton u t) (NBType x) ns
527+ bindings' =
528+ bindings >>= \case
529+ (NamedVar path r src) ->
530+ case getPath path of
531+ Nothing -> [] -- TODO: This should be an error (?)
532+ Just name -> pure $ fromName name r
533+ (Inherit attrSet keys src) ->
534+ let names :: [VarName] = mapMaybe getKeyName keys
535+ f :: VarName -> NExprLoc = case attrSet of
536+ Nothing -> \v -> Fix $ Compose $ Ann (SrcSpan src src) $ NSym v
537+ Just set -> \v -> Fix $ Compose $ Ann (SrcSpan src src) $ NSelect set (pure $ StaticKey v) Nothing
538+ in (\v -> fromName (pure v) (f v)) <$> names
539+
540+inferNormalizedBindings' :: NormalizedBinding' -> InferM' Scheme
541+inferNormalizedBindings' (NBType expr) = inferGeneral expr
542+inferNormalizedBindings' (NBAttrSet m) = scheme . NAttrSet <$> inferNormalizedBindings' `traverse` m
543+
544+inferNormalizedBindings :: NormalizedBinding -> InferM' (Map VarName Scheme)
545+inferNormalizedBindings = traverse inferNormalizedBindings'
546+
547+inferBinding :: [Binding NExprLoc] -> InferM' (Map VarName Scheme)
548+inferBinding = normalizeBindings >=> inferNormalizedBindings
531549
532550renderPretty :: Pretty x => x -> TL.Text
533551renderPretty = renderLazy . layoutPretty defaultLayoutOptions . pretty
@@ -702,15 +720,15 @@ unNString :: NString r -> Maybe Text
702720unNString (DoubleQuoted ss) = foldMap antiAntiQuoteText ss
703721unNString (Indented _ ss) = foldMap antiAntiQuoteText ss
704722
705−getKeyName :: Monad m => NKeyName r -> m (Maybe VarName)
706−getKeyName (StaticKey k) = return $ Just k
707−getKeyName (DynamicKey k) = return $ antiAntiQuote k
723+getKeyName :: NKeyName r -> (Maybe VarName)
724+getKeyName (StaticKey k) = Just k
725+getKeyName (DynamicKey k) = antiAntiQuote k
708726
709727getPath ::
710− (Traversable t, Monad f) =>
728+ (Traversable t) =>
711729 t (NKeyName r) ->
712− f (Maybe (t Text))
713−getPath path = sequence <$> traverse getKeyName path
730+ Maybe (t Text)
731+getPath = mapM getKeyName
714732
715733type AttrSetPath = NonEmpty Text
716734
test/src/Main.hs+2−2
@@ -30,8 +30,8 @@ tests = do
3030 Failure err -> error $ show err
3131 Success r -> do
3232 case getType r of
33− (t, [], [], [], _) ->
33+ (t, [], [], [], [], _) ->
3434 return $ (TL.encodeUtf8 . renderPretty) t
35− (_, errors, unifyingErrors, predicateErrors, _) -> error . show $ (errors, unifyingErrors, predicateErrors)
35+ (_, errors, inferError, unifyingErrors, predicateErrors, _) -> error . show $ (errors, inferError, unifyingErrors, predicateErrors)
3636 )
3737 )