Merge pull request #285 from jwiegley/pending

Further corrections to type checking functions that take sets
This commit is contained in:
John Wiegley 2018-05-02 14:24:05 -07:00 committed by GitHub
commit 555ce952ae
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 33 additions and 25 deletions

View File

@ -62,7 +62,9 @@ class (Show v, Monad m) => MonadEval v m | v -> m where
evalIf :: v -> m v -> m v -> m v
evalAssert :: v -> m v -> m v
evalApp :: v -> m v -> m v
evalAbs :: Params (m v) -> (m v -> m v) -> m v
evalAbs :: Params (m v)
-> (forall a. m v -> (AttrSet (m v) -> m v -> m (a, v)) -> m (a, v))
-> m v
{-
evalSelect :: v -> NonEmpty Text -> Maybe (m v) -> m v
@ -170,10 +172,10 @@ eval (NAbs params body) = do
-- we defer here so the present scope is restored when the parameters and
-- body are forced during application.
scope <- currentScopes @_ @t
evalAbs params $ \arg ->
evalAbs params $ \arg k ->
withScopes @t scope $ do
args <- buildArgument params arg
pushScope args body
pushScope args (k (M.map (`force` pure) args) body)
-- | If you know that the 'scope' action will result in an 'AttrSet t', then
-- this implementation may be used as an implementation for 'evalWith'.

View File

@ -209,10 +209,10 @@ instance MonadNix e m => MonadEval (NValue m) m where
evalAssert c body = fromValue c >>= \b -> do
span <- currentPos
if b
then do
scope <- currentScopes
addProvenance (\b -> Provenance scope (NAssert_ span (Just c) (Just b))) <$> body
else nverr $ Assertion span c
then do
scope <- currentScopes
addProvenance (\b -> Provenance scope (NAssert_ span (Just c) (Just b))) <$> body
else nverr $ Assertion span c
evalApp f x = do
scope <- currentScopes
@ -220,10 +220,11 @@ instance MonadNix e m => MonadEval (NValue m) m where
addProvenance (const $ Provenance scope (NBinary_ span NApp (Just f) Nothing))
<$> callFunc f x
evalAbs p b = do
evalAbs p k = do
scope <- currentScopes
span <- currentPos
pure $ nvClosureP (Provenance scope (NAbs_ span (Nothing <$ p) Nothing)) (void p) b
pure $ nvClosureP (Provenance scope (NAbs_ span (Nothing <$ p) Nothing))
(void p) (\arg -> snd <$> k arg (\_ b -> ((),) <$> b))
evalError = throwError

View File

@ -64,7 +64,7 @@ data NTypeF (m :: * -> *) r
| TStr
| TList r
| TSet (Maybe (HashMap Text r))
| TClosure (Params ()) (m (Symbolic m) -> m (Symbolic m))
| TClosure (Params ())
| TPath
| TBuiltin String (SThunk m -> m (Symbolic m))
deriving Functor
@ -140,7 +140,7 @@ renderSymbolic = unpackSymbolic >=> \case
TSet (Just s) -> do
x <- traverse (`force` renderSymbolic) s
return $ "{" ++ show x ++ "}"
f@(TClosure p _) -> do
f@(TClosure p) -> do
(args, sym) <- do
f' <- mkSymbolic [f]
lintApp (NAbs (void p) ()) f' everyPossible
@ -310,7 +310,7 @@ instance MonadLint e m => MonadEval (Symbolic m) m where
pure body'
evalApp = (fmap snd .) . lintApp (NBinary NApp () ())
evalAbs params body = mkSymbolic [TClosure (void params) body]
evalAbs params _ = mkSymbolic [TClosure (void params)]
evalError = throwError
@ -364,7 +364,7 @@ lintApp context fun arg = unpackSymbolic fun >>= \case
"Cannot apply something not known to be a function"
NMany xs -> do
(args:_, ys) <- fmap unzip $ forM xs $ \case
TClosure _params _f -> arg >>= unpackSymbolic >>= \case
TClosure _params -> arg >>= unpackSymbolic >>= \case
NAny -> do
error "NYI"

View File

@ -8,6 +8,7 @@
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}
@ -387,35 +388,39 @@ instance MonadEval (Judgment s) (Infer s) where
(cs1 ++ cs2 ++ [EqConst t1 (t2 `TArr` tv)])
tv
evalAbs (Param x) e = do
evalAbs (Param x) k = do
tv@(TVar a) <- fresh
Judgment as cs t <-
extendMSet a (e (pure (Judgment (As.singleton x tv) [] tv)))
((), Judgment as cs t) <-
extendMSet a (k (pure (Judgment (As.singleton x tv) [] tv))
(\_ b -> ((),) <$> b))
return $ Judgment
(as `As.remove` x)
(cs ++ [EqConst t' tv | t' <- As.lookup x as])
(tv `TArr` t)
evalAbs (ParamSet ps _variadic _mname) e = do
js <- fmap concat $ forM ps $ \(name, mdef) -> case mdef of
Just _ -> pure []
Nothing -> do
evalAbs (ParamSet ps variadic _mname) k = do
js <- fmap concat $ forM ps $ \(name, _) -> do
tv <- fresh
pure [(name, tv)]
let (env, tys) = (\f -> foldl' f (As.empty, M.empty) js)
$ \(as1, t1) (k, t) ->
(as1 `As.merge` As.singleton k t, M.insert k t t1)
arg = pure $ Judgment env [] (TSet True tys)
call = k arg $ \args b -> (args,) <$> b
names = map fst js
Judgment as cs t <-
(\f -> foldr f (e (pure (Judgment env [] (TSet True tys)))) js)
$ \(_, TVar a) rest -> extendMSet a rest
(args, Judgment as cs t) <-
foldr (\(_, TVar a) -> extendMSet a) call js
ty <- TSet variadic <$> traverse (inferredType <$>) args
return $ Judgment
(foldl' As.remove as names)
(cs ++ [ EqConst t' (tys M.! x)
| x <- names
, t' <- As.lookup x as])
-- jww (2018-05-01): How do we recover the actual args used?
(t `TArr` t)
(ty `TArr` t)
evalError = throwError . EvaluationError