Support go to definition for the standard library (#1592)

* Remove ParserParams

ParserParams is only used to record the root of the project, which is
used to prefix source file paths. However source file paths are always
absolute so this is not required.

* Add GetAbsPath to Files effect

The Files effect is not responsible for resolving a relative module
path into an absolute path on disk. This will allow us to resolve
relative module paths to alternative paths, for example to point to the
standard library on disk.

* Files effect getAbsPath returns paths within the registered standard
library

This means that the standard library can exist on disk at a different
location to the Juvix project.

A command line flag --stdlib-path can be specified to point to a
standard library, otherwise the embedded standard library is written to
disk at $PROJ_DIR/.juvix-build/stdlib and this is used instead.

* Recreate stdlib dir only when juvix version changes

* Add UpdateStdlib to the Files effect

* Add comment for stdlibOrFile

* Remove spurious import

app/App.hs

@@ -61,6 +61,7 @@ getEntryPoint' opts root pkg inputFile = do
         _entryPointNoTermination = opts ^. globalNoTermination,
         _entryPointNoPositivity = opts ^. globalNoPositivity,
         _entryPointNoStdlib = opts ^. globalNoStdlib,
+        _entryPointStdlibPath = opts ^. globalStdlibPath,
         _entryPointPackage = pkg,
         _entryPointModulePaths = pure (inputFile ^. pathPath),
         _entryPointGenericOptions = project opts,

app/Commands/Compile.hs

@@ -6,6 +6,7 @@ import Data.ByteString qualified as BS
 import Data.FileEmbed qualified as FE
 import Data.Text.IO qualified as TIO
 import Juvix.Compiler.Backend.C.Translation.FromInternal qualified as MiniC
+import Juvix.Extra.Paths
 import System.Environment
 import System.Process qualified as P
 
@@ -19,9 +20,6 @@ runCommand opts@CompileOptions {..} = do
     Left err -> printFailureExit err
     _ -> return ()
 
-juvixBuildDir :: FilePath
-juvixBuildDir = ".juvix-build"
-
 inputCFile :: FilePath -> FilePath -> FilePath
 inputCFile projRoot inputFileCompile =
   projRoot </> juvixBuildDir </> outputMiniCFile

app/Commands/Dev/Asm/Run.hs

@@ -12,7 +12,7 @@ import Juvix.Compiler.Asm.Translation.FromSource qualified as Asm
 runCommand :: forall r. Members '[Embed IO, App] r => AsmRunOptions -> Sem r ()
 runCommand opts = do
   s <- embed (readFile file)
-  case Asm.runParser "" file s of
+  case Asm.runParser file s of
     Left err -> exitJuvixError (JuvixError err)
     Right tab ->
       let v = if opts ^. asmRunNoValidate then Nothing else Asm.validate tab

app/Commands/Dev/Asm/Validate.hs

@@ -8,7 +8,7 @@ import Juvix.Compiler.Asm.Translation.FromSource qualified as Asm
 runCommand :: forall r. Members '[Embed IO, App] r => AsmValidateOptions -> Sem r ()
 runCommand opts = do
   s <- embed (readFile file)
-  case Asm.runParser "" file s of
+  case Asm.runParser file s of
     Left err -> exitJuvixError (JuvixError err)
     Right tab -> do
       case Asm.validate tab of

app/Commands/Dev/Core/Eval.hs

@@ -28,7 +28,7 @@ doEval noIO loc tab node
 runCommand :: forall r. Members '[Embed IO, App] r => CoreEvalOptions -> Sem r ()
 runCommand opts = do
   s <- embed (readFile f)
-  case Core.runParser "" f Core.emptyInfoTable s of
+  case Core.runParser f Core.emptyInfoTable s of
     Left err -> exitJuvixError (JuvixError err)
     Right (tab, Just node) -> do
       r <- doEval (opts ^. coreEvalNoIO) defaultLoc tab node
@@ -43,6 +43,6 @@ runCommand opts = do
     Right (_, Nothing) -> return ()
   where
     defaultLoc :: Interval
-    defaultLoc = singletonInterval (mkLoc f 0 (M.initialPos f))
+    defaultLoc = singletonInterval (mkLoc 0 (M.initialPos f))
     f :: FilePath
     f = opts ^. coreEvalInputFile . pathPath

app/Commands/Dev/Core/Read.hs

@@ -9,7 +9,7 @@ import Juvix.Compiler.Core.Translation.FromSource qualified as Core
 runCommand :: forall r. Members '[Embed IO, App] r => CoreReadOptions -> Sem r ()
 runCommand opts = do
   s' <- embed (readFile f)
-  tab <- getRight (fst <$> mapLeft JuvixError (Core.runParser "" f Core.emptyInfoTable s'))
+  tab <- getRight (fst <$> mapLeft JuvixError (Core.runParser f Core.emptyInfoTable s'))
   let tab' = Core.applyTransformations (opts ^. coreReadTransformations) tab
   renderStdOut (Core.ppOut opts tab')
   where

app/Commands/Dev/Core/Repl.hs

@@ -51,7 +51,7 @@ runRepl opts tab = do
             runRepl opts tab'
       ':' : 'l' : ' ' : f -> do
         s' <- embed (readFile f)
-        case Core.runParser "" f Core.emptyInfoTable s' of
+        case Core.runParser f Core.emptyInfoTable s' of
           Left err -> do
             printJuvixError (JuvixError err)
             runRepl opts tab
@@ -84,7 +84,7 @@ runRepl opts tab = do
               embed (putStrLn "")
               runRepl opts tab'
       where
-        defaultLoc = singletonInterval (mkLoc "stdin" 0 (M.initialPos "stdin"))
+        defaultLoc = singletonInterval (mkLoc 0 (M.initialPos "stdin"))
 
 showReplWelcome :: Members '[Embed IO, App] r => Sem r ()
 showReplWelcome = embed $ do

app/GlobalOptions.hs

@@ -17,7 +17,8 @@ data GlobalOptions = GlobalOptions
     _globalStdin :: Bool,
     _globalNoTermination :: Bool,
     _globalNoPositivity :: Bool,
-    _globalNoStdlib :: Bool
+    _globalNoStdlib :: Bool,
+    _globalStdlibPath :: Maybe FilePath
   }
   deriving stock (Eq, Show, Data)
 
@@ -52,7 +53,8 @@ defaultGlobalOptions =
       _globalNoTermination = False,
       _globalStdin = False,
       _globalNoPositivity = False,
-      _globalNoStdlib = False
+      _globalNoStdlib = False,
+      _globalStdlibPath = Nothing
     }
 
 -- | Get a parser for global flags which can be hidden or not depending on
@@ -99,4 +101,14 @@ parseGlobalFlags = do
       ( long "no-stdlib"
           <> help "Do not use the standard library"
       )
+  _globalStdlibPath <-
+    optional
+      ( strOption
+          ( long "stdlib-path"
+              <> metavar "PATH"
+              <> help "Specify path to the standard library"
+              <> action "directory"
+          )
+      )
+
   return GlobalOptions {..}

juvix-mode/flycheck-juvix.el

@@ -9,8 +9,10 @@
 
 (flycheck-define-checker juvix
   "A Juvix syntax checker."
-  :command ("juvix" "--only-errors" "--no-colors" "--stdin" "typecheck"
+  :command ("juvix" "--only-errors" "--no-colors" "--stdin"
             (option-flag "--no-stdlib" juvix-disable-embedded-stdlib)
+            (option "--stdlib-path" juvix-stdlib-path)
+            "typecheck"
             source-original)
   :standard-input t
   :error-patterns

juvix-mode/juvix-customize.el

@@ -9,4 +9,9 @@
   :type 'boolean
   :group 'juvix)
 
+(defcustom juvix-stdlib-path nil
+  "Specify the path to the standard library."
+  :type 'directory
+  :group 'juvix)
+
 (provide 'juvix-customize)

juvix-mode/juvix-mode.el

@@ -53,7 +53,7 @@
   (save-buffer)
   (juvix-clear-annotations)
   (eval (read (shell-command-to-string
-               (concat "juvix " (if juvix-disable-embedded-stdlib "--no-stdlib " "") "dev highlight "
+               (concat "juvix " (if juvix-disable-embedded-stdlib "--no-stdlib " "") (if juvix-stdlib-path (concat "--stdlib-path " juvix-stdlib-path " ") "") "dev highlight "
                        (buffer-file-name)))))
   (save-buffer))
 

package.yaml

@@ -36,6 +36,8 @@ dependencies:
 - megaparsec == 9.2.*
 - microlens-platform == 0.4.*
 - parser-combinators == 1.3.*
+- path == 0.9.*
+- path-io == 1.7.*
 - polysemy == 1.7.*
 - polysemy-plugin == 0.4.*
 - prettyprinter == 1.7.*

src/Juvix/Compiler/Asm/Error.hs

@@ -37,4 +37,4 @@ instance Show AsmError where
 instance HasLoc AsmError where
   getLoc (AsmError {..}) = fromMaybe defaultLoc _asmErrorLoc
     where
-      defaultLoc = singletonInterval (mkLoc "" 0 (M.initialPos ""))
+      defaultLoc = singletonInterval (mkLoc 0 (M.initialPos ""))