Merge pull request #256 from vilunov/repl-package

"--repl" command for opening a REPL in a package

src/Idris/Main.idr

@@ -131,7 +131,6 @@ stMain opts
          defs <- initDefs
          c <- newRef Ctxt defs
          s <- newRef Syn initSyntax
-         m <- newRef MD initMetadata
          addPrimitives
 
          setWorkingDir "."
@@ -157,6 +156,7 @@ stMain opts
                  when (checkVerbose opts) $ -- override Quiet if implicitly set
                      setOutput (REPL False)
                  u <- newRef UST initUState
+                 m <- newRef MD initMetadata
                  updateREPLOpts
                  session <- getSession
                  when (not $ nobanner session) $

src/Idris/Package.idr

@@ -444,15 +444,16 @@ getParseErrorLoc fname _ = replFC
 -- Just load the 'Main' module, if it exists, which will involve building
 -- it if necessary
 runRepl : {auto c : Ref Ctxt Defs} ->
+          {auto s : Ref Syn SyntaxInfo} ->
           {auto o : Ref ROpts REPLOpts} ->
           PkgDesc ->
           List CLOpt ->
           Core ()
-runRepl pkg opts
-    = do addDeps pkg
-         processOptions (options pkg)
-         preOptions opts
-         throw (InternalError "Not implemented")
+runRepl pkg opts = do
+  u <- newRef UST initUState
+  m <- newRef MD initMetadata
+  repl {u} {s}
+
 
 processPackage : {auto c : Ref Ctxt Defs} ->
                  {auto s : Ref Syn SyntaxInfo} ->
@@ -480,7 +481,10 @@ processPackage cmd file opts
                                        | errs => coreLift (exitWith (ExitFailure 1))
                                     install pkg opts
                       Clean => clean pkg opts
-                      REPL => runRepl pkg opts
+                      REPL => do
+                        [] <- build pkg opts
+                           | errs => coreLift (exitWith (ExitFailure 1))
+                        runRepl pkg opts
 
 record POptsFilterResult where
   constructor MkPFR

tests/Main.idr

@@ -80,7 +80,7 @@ idrisTests
        "perror001", "perror002", "perror003", "perror004", "perror005",
        "perror006",
        -- Packages and ipkg files
-       "pkg001", "pkg002", "pkg003",
+       "pkg001", "pkg002", "pkg003", "pkg004",
        -- Larger programs arising from real usage. Typically things with
        -- interesting interactions between features
        "real001", "real002",

tests/idris2/pkg004/Dummy.idr

@@ -0,0 +1,7 @@
+module Dummy
+
+something : String
+something = "Something something"
+
+data Proxy : Type -> Type where
+  MkProxy : Proxy a

tests/idris2/pkg004/dummy.ipkg

@@ -0,0 +1,9 @@
+package dummy
+
+authors = "Joe Bloggs"
+maintainers = "Joe Bloggs"
+license = "BSD3 but see LICENSE for more information"
+brief = "This is a dummy package."
+readme = "README.md"
+
+modules = Dummy

tests/idris2/pkg004/expected

@@ -0,0 +1,9 @@
+1/1: Building Dummy (Dummy.idr)
+Dummy> (interactive):1:4--1:13:Undefined name undefined
+Dummy> Dummy.something : String
+Dummy> "Something something"
+Dummy> Dummy.Proxy : Type -> Type
+Dummy> Proxy
+Dummy> Proxy String : Type
+Dummy> 
+Bye for now!

tests/idris2/pkg004/input

@@ -0,0 +1,6 @@
+:t undefined
+:t something
+something
+:t Proxy
+Proxy
+:t Proxy String

tests/idris2/pkg004/run

@@ -0,0 +1,3 @@
+$1 --repl dummy.ipkg < input
+
+rm -rf build