2018-04-14 05:29:18 +03:00
|
|
|
{-# LANGUAGE FlexibleContexts #-}
|
2018-04-06 07:10:06 +03:00
|
|
|
{-# LANGUAGE LambdaCase #-}
|
2018-04-12 07:31:48 +03:00
|
|
|
{-# LANGUAGE OverloadedStrings #-}
|
2018-04-14 05:29:18 +03:00
|
|
|
{-# LANGUAGE ScopedTypeVariables #-}
|
2018-04-30 20:41:21 +03:00
|
|
|
{-# LANGUAGE TupleSections #-}
|
2018-04-25 23:00:41 +03:00
|
|
|
{-# LANGUAGE TypeApplications #-}
|
2018-03-30 01:35:12 +03:00
|
|
|
|
2015-06-24 00:53:07 +03:00
|
|
|
module Main where
|
|
|
|
|
2018-04-14 19:44:55 +03:00
|
|
|
import qualified Control.DeepSeq as Deep
|
2018-04-10 18:34:21 +03:00
|
|
|
import qualified Control.Exception as Exc
|
2018-04-04 00:21:33 +03:00
|
|
|
import Control.Monad
|
2018-04-21 08:36:40 +03:00
|
|
|
import Control.Monad.Catch
|
2018-04-14 05:29:18 +03:00
|
|
|
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 03:35:13 +03:00
|
|
|
-- import Control.Monad.ST
|
2018-04-18 00:24:52 +03:00
|
|
|
import qualified Data.Aeson.Encoding as A
|
|
|
|
import qualified Data.Aeson.Text as A
|
2018-04-30 20:41:21 +03:00
|
|
|
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 03:35:13 +03:00
|
|
|
import qualified Data.Map as Map
|
2018-04-30 20:41:21 +03:00
|
|
|
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 03:35:13 +03:00
|
|
|
import Data.Maybe (fromJust)
|
2018-05-03 07:32:00 +03:00
|
|
|
import Data.Time
|
2018-04-30 20:41:21 +03:00
|
|
|
import qualified Data.Text as Text
|
2018-04-10 03:12:16 +03:00
|
|
|
import qualified Data.Text.IO as Text
|
2018-04-18 00:24:52 +03:00
|
|
|
import qualified Data.Text.Lazy.Encoding as TL
|
|
|
|
import qualified Data.Text.Lazy.IO as TL
|
2018-04-14 19:44:55 +03:00
|
|
|
import Nix
|
2018-04-18 00:24:52 +03:00
|
|
|
import Nix.Convert
|
2018-04-21 20:10:22 +03:00
|
|
|
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 03:35:13 +03:00
|
|
|
-- import Nix.Lint
|
2018-05-09 02:40:56 +03:00
|
|
|
import Nix.Options.Parser
|
2018-05-01 04:47:58 +03:00
|
|
|
import qualified Nix.Type.Env as Env
|
|
|
|
import qualified Nix.Type.Infer as HM
|
2018-04-18 00:24:52 +03:00
|
|
|
import Nix.Utils
|
2018-04-04 00:21:33 +03:00
|
|
|
import Options.Applicative hiding (ParserResult(..))
|
2018-04-18 00:24:52 +03:00
|
|
|
import qualified Repl
|
2018-04-12 00:35:17 +03:00
|
|
|
import System.FilePath
|
2018-04-18 00:24:52 +03:00
|
|
|
import System.IO
|
2018-04-04 00:21:33 +03:00
|
|
|
import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
|
2018-05-01 04:47:58 +03:00
|
|
|
import qualified Text.Show.Pretty as PS
|
2015-06-24 00:53:07 +03:00
|
|
|
|
|
|
|
main :: IO ()
|
|
|
|
main = do
|
2018-05-03 07:32:00 +03:00
|
|
|
time <- liftIO getCurrentTime
|
|
|
|
opts <- execParser (nixOptionsInfo time)
|
2018-04-24 22:25:40 +03:00
|
|
|
runLazyM opts $ case readFrom opts of
|
2018-04-12 00:35:17 +03:00
|
|
|
Just path -> do
|
2018-04-12 06:19:59 +03:00
|
|
|
let file = addExtension (dropExtension path) "nix"
|
2018-04-24 22:25:40 +03:00
|
|
|
process opts (Just file) =<< liftIO (readCache path)
|
2018-04-12 00:35:17 +03:00
|
|
|
Nothing -> case expression opts of
|
|
|
|
Just s -> handleResult opts Nothing (parseNixTextLoc s)
|
|
|
|
Nothing -> case fromFile opts of
|
|
|
|
Just "-" ->
|
2018-04-24 22:25:40 +03:00
|
|
|
mapM_ (processFile opts)
|
|
|
|
=<< (lines <$> liftIO getContents)
|
2018-04-12 00:35:17 +03:00
|
|
|
Just path ->
|
2018-04-24 22:25:40 +03:00
|
|
|
mapM_ (processFile opts)
|
|
|
|
=<< (lines <$> liftIO (readFile path))
|
2018-04-12 00:35:17 +03:00
|
|
|
Nothing -> case filePaths opts of
|
2018-04-29 02:13:24 +03:00
|
|
|
[] -> Repl.shell (pure ())
|
2018-04-12 00:35:17 +03:00
|
|
|
["-"] ->
|
|
|
|
handleResult opts Nothing . parseNixTextLoc
|
2018-04-24 22:25:40 +03:00
|
|
|
=<< liftIO Text.getContents
|
2018-04-12 00:35:17 +03:00
|
|
|
paths ->
|
|
|
|
mapM_ (processFile opts) paths
|
2018-04-06 06:43:13 +03:00
|
|
|
where
|
|
|
|
processFile opts path = do
|
|
|
|
eres <- parseNixFileLoc path
|
|
|
|
handleResult opts (Just path) eres
|
2018-03-28 07:59:27 +03:00
|
|
|
|
2018-04-06 06:43:13 +03:00
|
|
|
handleResult opts mpath = \case
|
2018-04-10 07:35:46 +03:00
|
|
|
Failure err ->
|
2018-04-10 19:02:02 +03:00
|
|
|
(if ignoreErrors opts
|
2018-04-24 22:25:40 +03:00
|
|
|
then liftIO . hPutStrLn stderr
|
2018-04-10 19:02:02 +03:00
|
|
|
else errorWithoutStackTrace) $ "Parse failed: " ++ show err
|
2018-04-10 07:35:46 +03:00
|
|
|
|
2018-04-24 22:25:40 +03:00
|
|
|
Success expr -> do
|
2018-05-01 04:47:58 +03:00
|
|
|
when (check opts) $ do
|
2018-05-03 01:07:30 +03:00
|
|
|
expr' <- liftIO (reduceExpr mpath expr)
|
|
|
|
case HM.inferTop Env.empty [("it", stripAnnotation expr')] of
|
2018-05-01 04:47:58 +03:00
|
|
|
Left err ->
|
2018-05-02 03:35:01 +03:00
|
|
|
errorWithoutStackTrace $ "Type error: " ++ PS.ppShow err
|
2018-05-01 04:47:58 +03:00
|
|
|
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 03:35:13 +03:00
|
|
|
liftIO $ putStrLn $ "Type of expression: "
|
|
|
|
++ PS.ppShow (fromJust (Map.lookup "it" (Env.types ty)))
|
2018-05-01 04:47:58 +03:00
|
|
|
|
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 03:35:13 +03:00
|
|
|
-- liftIO $ putStrLn $ runST $
|
|
|
|
-- runLintM opts . renderSymbolic =<< lint opts expr
|
2018-04-09 12:07:40 +03:00
|
|
|
|
2018-04-24 22:25:40 +03:00
|
|
|
catch (process opts mpath expr) $ \case
|
|
|
|
NixException frames ->
|
|
|
|
errorWithoutStackTrace . show
|
2018-04-25 23:00:41 +03:00
|
|
|
=<< renderFrames @(NThunk (Lazy IO)) frames
|
2018-04-24 22:25:40 +03:00
|
|
|
|
2018-04-29 02:13:24 +03:00
|
|
|
when (repl opts) $ Repl.shell (pure ())
|
2018-04-04 23:33:53 +03:00
|
|
|
|
2018-04-30 20:41:21 +03:00
|
|
|
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 =
|
2018-05-07 08:13:44 +03:00
|
|
|
liftIO $ putStr $ PS.ppShow $ stripAnnotation expr
|
2018-04-30 20:41:21 +03:00
|
|
|
|
|
|
|
| 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
|
2018-04-13 02:46:34 +03:00
|
|
|
|
2018-04-21 10:43:52 +03:00
|
|
|
reduction path mp x = do
|
|
|
|
eres <- Nix.withNixContext mp $
|
2018-04-21 20:10:22 +03:00
|
|
|
Nix.reducingEvalExpr (Eval.eval . annotated . getCompose) mp x
|
2018-04-21 10:43:52 +03:00
|
|
|
handleReduced path eres
|
|
|
|
|
2018-04-21 08:36:40 +03:00
|
|
|
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
|