hnix/main/Main.hs

219 lines
8.9 KiB
Haskell
Raw Normal View History

{-# LANGUAGE FlexibleContexts #-}
2018-04-06 06:10:06 +02:00
{-# LANGUAGE LambdaCase #-}
2018-04-12 06:31:48 +02:00
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
module Main where
2018-04-14 18:44:55 +02:00
import qualified Control.DeepSeq as Deep
2018-04-10 17:34:21 +02:00
import qualified Control.Exception as Exc
import Control.Monad
import Control.Monad.Catch
import Control.Monad.IO.Class
Much more work on type inference; report multiple possible types This is needed because of a function like this: x: y: x + y This is polymorphic, but over exactly four possibilities: int -> int int -> float float -> int float -> float The "type" is really the combination of the four, since we don't yet have a mechanism like type classes, which could have rendered this as a single type: (Num a, Num b) => (x :: a): (y :: b): x + y Going this route will require that we manage an implicit type classes hierarchy, and perform unification on constraints as well as types. In the interim, I just lifted the unification algorithm into the LogicT monad, and use back-tracking search to find all the possible types an expression could be. The main problem with using LogicT, however, is that there are many types it *couldn't* be, and in the case of a unification failure, it not yet clear what the type should have been. For example: "foo" + 2 Should the string have been a float or an integer or a path? Or should the integer have been a string? So for now we report all the possibilities, since it's not obvious which part of the expression is in error: hnix: Type error: TypeInferenceErrors [ UnificationFail (TCon "integer") (TCon "string") , UnificationFail (TCon "string") (TCon "path") , UnificationFail (TCon "string") (TCon "float") , UnificationFail (TCon "string") (TCon "integer") ] This is a case where enumerating types rather than trying to make them compact using type classes might actually be an improvement, since the errors here would have been only slightly less numerous: string != Num a => a string != path integer != string Clearly a better reporting mechanism is needed to clarify these problems. I can imagine that in an IDE, there would be a squiggly under both sides of the expression, each suggesting the type that was expected for that argument under the assumption that the other argument (the one not be inspected) was the correct one.
2018-05-02 02:35:13 +02:00
-- import Control.Monad.ST
import qualified Data.Aeson.Encoding as A
import qualified Data.Aeson.Text as A
import qualified Data.HashMap.Lazy as M
Much more work on type inference; report multiple possible types This is needed because of a function like this: x: y: x + y This is polymorphic, but over exactly four possibilities: int -> int int -> float float -> int float -> float The "type" is really the combination of the four, since we don't yet have a mechanism like type classes, which could have rendered this as a single type: (Num a, Num b) => (x :: a): (y :: b): x + y Going this route will require that we manage an implicit type classes hierarchy, and perform unification on constraints as well as types. In the interim, I just lifted the unification algorithm into the LogicT monad, and use back-tracking search to find all the possible types an expression could be. The main problem with using LogicT, however, is that there are many types it *couldn't* be, and in the case of a unification failure, it not yet clear what the type should have been. For example: "foo" + 2 Should the string have been a float or an integer or a path? Or should the integer have been a string? So for now we report all the possibilities, since it's not obvious which part of the expression is in error: hnix: Type error: TypeInferenceErrors [ UnificationFail (TCon "integer") (TCon "string") , UnificationFail (TCon "string") (TCon "path") , UnificationFail (TCon "string") (TCon "float") , UnificationFail (TCon "string") (TCon "integer") ] This is a case where enumerating types rather than trying to make them compact using type classes might actually be an improvement, since the errors here would have been only slightly less numerous: string != Num a => a string != path integer != string Clearly a better reporting mechanism is needed to clarify these problems. I can imagine that in an IDE, there would be a squiggly under both sides of the expression, each suggesting the type that was expected for that argument under the assumption that the other argument (the one not be inspected) was the correct one.
2018-05-02 02:35:13 +02:00
import qualified Data.Map as Map
import Data.List (sortOn)
Much more work on type inference; report multiple possible types This is needed because of a function like this: x: y: x + y This is polymorphic, but over exactly four possibilities: int -> int int -> float float -> int float -> float The "type" is really the combination of the four, since we don't yet have a mechanism like type classes, which could have rendered this as a single type: (Num a, Num b) => (x :: a): (y :: b): x + y Going this route will require that we manage an implicit type classes hierarchy, and perform unification on constraints as well as types. In the interim, I just lifted the unification algorithm into the LogicT monad, and use back-tracking search to find all the possible types an expression could be. The main problem with using LogicT, however, is that there are many types it *couldn't* be, and in the case of a unification failure, it not yet clear what the type should have been. For example: "foo" + 2 Should the string have been a float or an integer or a path? Or should the integer have been a string? So for now we report all the possibilities, since it's not obvious which part of the expression is in error: hnix: Type error: TypeInferenceErrors [ UnificationFail (TCon "integer") (TCon "string") , UnificationFail (TCon "string") (TCon "path") , UnificationFail (TCon "string") (TCon "float") , UnificationFail (TCon "string") (TCon "integer") ] This is a case where enumerating types rather than trying to make them compact using type classes might actually be an improvement, since the errors here would have been only slightly less numerous: string != Num a => a string != path integer != string Clearly a better reporting mechanism is needed to clarify these problems. I can imagine that in an IDE, there would be a squiggly under both sides of the expression, each suggesting the type that was expected for that argument under the assumption that the other argument (the one not be inspected) was the correct one.
2018-05-02 02:35:13 +02:00
import Data.Maybe (fromJust)
import qualified Data.Text as Text
import qualified Data.Text.IO as Text
import qualified Data.Text.Lazy.Encoding as TL
import qualified Data.Text.Lazy.IO as TL
2018-04-14 18:44:55 +02:00
import Nix
import Nix.Convert
import qualified Nix.Eval as Eval
Much more work on type inference; report multiple possible types This is needed because of a function like this: x: y: x + y This is polymorphic, but over exactly four possibilities: int -> int int -> float float -> int float -> float The "type" is really the combination of the four, since we don't yet have a mechanism like type classes, which could have rendered this as a single type: (Num a, Num b) => (x :: a): (y :: b): x + y Going this route will require that we manage an implicit type classes hierarchy, and perform unification on constraints as well as types. In the interim, I just lifted the unification algorithm into the LogicT monad, and use back-tracking search to find all the possible types an expression could be. The main problem with using LogicT, however, is that there are many types it *couldn't* be, and in the case of a unification failure, it not yet clear what the type should have been. For example: "foo" + 2 Should the string have been a float or an integer or a path? Or should the integer have been a string? So for now we report all the possibilities, since it's not obvious which part of the expression is in error: hnix: Type error: TypeInferenceErrors [ UnificationFail (TCon "integer") (TCon "string") , UnificationFail (TCon "string") (TCon "path") , UnificationFail (TCon "string") (TCon "float") , UnificationFail (TCon "string") (TCon "integer") ] This is a case where enumerating types rather than trying to make them compact using type classes might actually be an improvement, since the errors here would have been only slightly less numerous: string != Num a => a string != path integer != string Clearly a better reporting mechanism is needed to clarify these problems. I can imagine that in an IDE, there would be a squiggly under both sides of the expression, each suggesting the type that was expected for that argument under the assumption that the other argument (the one not be inspected) was the correct one.
2018-05-02 02:35:13 +02:00
-- import Nix.Lint
import qualified Nix.Type.Env as Env
import qualified Nix.Type.Infer as HM
import Nix.Utils
import Options.Applicative hiding (ParserResult(..))
import qualified Repl
import System.FilePath
import System.IO
import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
import qualified Text.Show.Pretty as PS
main :: IO ()
main = do
opts <- execParser nixOptionsInfo
2018-04-24 21:25:40 +02:00
runLazyM opts $ case readFrom opts of
Just path -> do
let file = addExtension (dropExtension path) "nix"
2018-04-24 21:25:40 +02:00
process opts (Just file) =<< liftIO (readCache path)
Nothing -> case expression opts of
Just s -> handleResult opts Nothing (parseNixTextLoc s)
Nothing -> case fromFile opts of
Just "-" ->
2018-04-24 21:25:40 +02:00
mapM_ (processFile opts)
=<< (lines <$> liftIO getContents)
Just path ->
2018-04-24 21:25:40 +02:00
mapM_ (processFile opts)
=<< (lines <$> liftIO (readFile path))
Nothing -> case filePaths opts of
[] -> Repl.shell (pure ())
["-"] ->
handleResult opts Nothing . parseNixTextLoc
2018-04-24 21:25:40 +02:00
=<< liftIO Text.getContents
paths ->
mapM_ (processFile opts) paths
where
processFile opts path = do
eres <- parseNixFileLoc path
handleResult opts (Just path) eres
handleResult opts mpath = \case
Failure err ->
(if ignoreErrors opts
2018-04-24 21:25:40 +02:00
then liftIO . hPutStrLn stderr
else errorWithoutStackTrace) $ "Parse failed: " ++ show err
2018-04-24 21:25:40 +02:00
Success expr -> do
when (check opts) $ do
2018-05-03 00:07:30 +02:00
expr' <- liftIO (reduceExpr mpath expr)
case HM.inferTop Env.empty [("it", stripAnnotation expr')] of
Left err ->
errorWithoutStackTrace $ "Type error: " ++ PS.ppShow err
Right ty ->
Much more work on type inference; report multiple possible types This is needed because of a function like this: x: y: x + y This is polymorphic, but over exactly four possibilities: int -> int int -> float float -> int float -> float The "type" is really the combination of the four, since we don't yet have a mechanism like type classes, which could have rendered this as a single type: (Num a, Num b) => (x :: a): (y :: b): x + y Going this route will require that we manage an implicit type classes hierarchy, and perform unification on constraints as well as types. In the interim, I just lifted the unification algorithm into the LogicT monad, and use back-tracking search to find all the possible types an expression could be. The main problem with using LogicT, however, is that there are many types it *couldn't* be, and in the case of a unification failure, it not yet clear what the type should have been. For example: "foo" + 2 Should the string have been a float or an integer or a path? Or should the integer have been a string? So for now we report all the possibilities, since it's not obvious which part of the expression is in error: hnix: Type error: TypeInferenceErrors [ UnificationFail (TCon "integer") (TCon "string") , UnificationFail (TCon "string") (TCon "path") , UnificationFail (TCon "string") (TCon "float") , UnificationFail (TCon "string") (TCon "integer") ] This is a case where enumerating types rather than trying to make them compact using type classes might actually be an improvement, since the errors here would have been only slightly less numerous: string != Num a => a string != path integer != string Clearly a better reporting mechanism is needed to clarify these problems. I can imagine that in an IDE, there would be a squiggly under both sides of the expression, each suggesting the type that was expected for that argument under the assumption that the other argument (the one not be inspected) was the correct one.
2018-05-02 02:35:13 +02:00
liftIO $ putStrLn $ "Type of expression: "
++ PS.ppShow (fromJust (Map.lookup "it" (Env.types ty)))
Much more work on type inference; report multiple possible types This is needed because of a function like this: x: y: x + y This is polymorphic, but over exactly four possibilities: int -> int int -> float float -> int float -> float The "type" is really the combination of the four, since we don't yet have a mechanism like type classes, which could have rendered this as a single type: (Num a, Num b) => (x :: a): (y :: b): x + y Going this route will require that we manage an implicit type classes hierarchy, and perform unification on constraints as well as types. In the interim, I just lifted the unification algorithm into the LogicT monad, and use back-tracking search to find all the possible types an expression could be. The main problem with using LogicT, however, is that there are many types it *couldn't* be, and in the case of a unification failure, it not yet clear what the type should have been. For example: "foo" + 2 Should the string have been a float or an integer or a path? Or should the integer have been a string? So for now we report all the possibilities, since it's not obvious which part of the expression is in error: hnix: Type error: TypeInferenceErrors [ UnificationFail (TCon "integer") (TCon "string") , UnificationFail (TCon "string") (TCon "path") , UnificationFail (TCon "string") (TCon "float") , UnificationFail (TCon "string") (TCon "integer") ] This is a case where enumerating types rather than trying to make them compact using type classes might actually be an improvement, since the errors here would have been only slightly less numerous: string != Num a => a string != path integer != string Clearly a better reporting mechanism is needed to clarify these problems. I can imagine that in an IDE, there would be a squiggly under both sides of the expression, each suggesting the type that was expected for that argument under the assumption that the other argument (the one not be inspected) was the correct one.
2018-05-02 02:35:13 +02:00
-- liftIO $ putStrLn $ runST $
-- runLintM opts . renderSymbolic =<< lint opts expr
2018-04-09 11:07:40 +02:00
2018-04-24 21:25:40 +02:00
catch (process opts mpath expr) $ \case
NixException frames ->
errorWithoutStackTrace . show
=<< renderFrames @(NThunk (Lazy IO)) frames
2018-04-24 21:25:40 +02:00
when (repl opts) $ Repl.shell (pure ())
process opts mpath expr
| evaluate opts, tracing opts =
evaluateExpression mpath
Nix.nixTracingEvalExprLoc printer expr
| evaluate opts, Just path <- reduce opts =
evaluateExpression mpath (reduction path) printer expr
| evaluate opts, not (null (arg opts) && null (argstr opts)) =
evaluateExpression mpath
Nix.nixEvalExprLoc printer expr
| evaluate opts =
processResult printer =<< Nix.nixEvalExprLoc mpath expr
| xml opts =
error "Rendering expression trees to XML is not yet implemented"
| json opts =
liftIO $ TL.putStrLn $
A.encodeToLazyText (stripAnnotation expr)
| verbose opts >= DebugInfo =
liftIO $ print $ stripAnnotation expr
| cache opts, Just path <- mpath =
liftIO $ writeCache (addExtension (dropExtension path) "nixc") expr
| parseOnly opts =
void $ liftIO $ Exc.evaluate $ Deep.force expr
| otherwise =
liftIO $ displayIO stdout
. renderPretty 0.4 80
. prettyNix
. stripAnnotation $ expr
where
printer :: forall e m. (MonadNix e m, MonadIO m, Typeable m)
=> NValue m -> m ()
printer
| finder opts =
fromValue @(AttrSet (NThunk m)) >=> findAttrs
| xml opts =
liftIO . putStrLn . toXML <=< normalForm
| json opts =
liftIO . TL.putStrLn
. TL.decodeUtf8
. A.encodingToLazyByteString
. toEncodingSorted
<=< fromNix
| normalize opts =
liftIO . print . prettyNValueNF <=< normalForm
| values opts =
liftIO . print <=< prettyNValueProv
| otherwise =
liftIO . print <=< prettyNValue
where
findAttrs = go ""
where
go prefix s = do
xs <- forM (sortOn fst (M.toList s))
$ \(k, nv@(NThunk _ t)) -> case t of
Value v -> pure (k, Just v)
Thunk _ _ ref -> do
let path = prefix ++ Text.unpack k
(_, descend) = filterEntry path k
val <- readVar ref
case val of
Computed _ -> pure (k, Nothing)
_ | descend -> (k,) <$> forceEntry path nv
| otherwise -> pure (k, Nothing)
forM_ xs $ \(k, mv) -> do
let path = prefix ++ Text.unpack k
(report, descend) = filterEntry path k
when report $ do
liftIO $ putStrLn path
when descend $ case mv of
Nothing -> return ()
Just v -> case v of
NVSet s' _ -> go (path ++ ".") s'
_ -> return ()
where
filterEntry path k = case (path, k) of
("stdenv", "stdenv") -> (True, True)
(_, "stdenv") -> (False, False)
(_, "out") -> (True, False)
(_, "src") -> (True, False)
(_, "mirrorsFile") -> (True, False)
(_, "buildPhase") -> (True, False)
(_, "builder") -> (False, False)
(_, "drvPath") -> (False, False)
(_, "outPath") -> (False, False)
(_, "__impureHostDeps") -> (False, False)
(_, "__sandboxProfile") -> (False, False)
("pkgs", "pkgs") -> (True, True)
(_, "pkgs") -> (False, False)
(_, "drvAttrs") -> (False, False)
_ -> (True, True)
forceEntry k v = catch (Just <$> force v pure)
$ \(NixException frames) -> do
liftIO . putStrLn
. ("Exception forcing " ++)
. (k ++)
. (": " ++) . show
=<< renderFrames @(NThunk (Lazy IO)) frames
return Nothing
reduction path mp x = do
eres <- Nix.withNixContext mp $
Nix.reducingEvalExpr (Eval.eval . annotated . getCompose) mp x
handleReduced path eres
handleReduced :: (MonadThrow m, MonadIO m)
=> FilePath
-> (NExprLoc, Either SomeException (NValue m))
-> m (NValue m)
handleReduced path (expr', eres) = do
liftIO $ do
putStrLn $ "Wrote winnowed expression tree to " ++ path
writeFile path $ show $ prettyNix (stripAnnotation expr')
case eres of
Left err -> throwM err
Right v -> return v