Support go to definition for the standard library

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 ""))