add load targets to search path

Fixes a bug pointed out by @weaversa:
#127 (comment)

In addition to the other search path changes in #127, we now will add
the directory containing files to be loaded to the search path. This
applies to:

- files loaded with a command line argument, like in the original
  comment
- arguments to `:l`, so for example `:l examples/DES.cry` would work
- batch file arguments, so for example running `cryptol -b
  /some/path/bar.cry` adds `/some/path` to the search path.

cryptol/Main.hs

@@ -26,7 +26,7 @@ import Cryptol.Utils.PP(pp)
 import Data.Monoid (mconcat)
 import System.Environment (getArgs, getProgName, lookupEnv)
 import System.Exit (exitFailure)
-import System.FilePath (splitSearchPath)
+import System.FilePath (splitSearchPath, takeDirectory)
 import System.Console.GetOpt
     (OptDescr(..),ArgOrder(..),ArgDescr(..),getOpt,usageInfo)
 
@@ -156,6 +156,10 @@ setupREPL opts = do
 #else
       where path' = splitSearchPath path
 #endif
+  case optBatch opts of
+    Nothing -> return ()
+    -- add the directory containing the batch file to the module search path
+    Just file -> prependSearchPath [ takeDirectory file ]
   case optLoad opts of
     []  -> loadPrelude `REPL.catch` \x -> io $ print $ pp x
     [l] -> loadCmd l `REPL.catch` \x -> io $ print $ pp x

src/Cryptol/ModuleSystem/Base.hs

@@ -36,10 +36,15 @@ import Data.List (nubBy)
 import Data.Maybe (mapMaybe,fromMaybe)
 import Data.Monoid ((<>))
 import System.Directory (doesFileExist)
-import System.FilePath (addExtension,joinPath,(</>))
+import System.FilePath ( addExtension
+                       , isAbsolute
+                       , joinPath
+                       , (</>)
+                       , takeDirectory
+                       , takeFileName
+                       )
 import qualified Data.Map as Map
 
-
 -- Renaming --------------------------------------------------------------------
 
 rename :: R.Rename a => R.NamingEnv -> a -> ModuleM a
@@ -112,18 +117,21 @@ parseModule path = do
 
 -- | Load a module by its path.
 loadModuleByPath :: FilePath -> ModuleM T.Module
-loadModuleByPath path = do
-  pm <- parseModule path
+loadModuleByPath path = withPrependedSearchPath [ takeDirectory path ] $ do
+  let fileName = takeFileName path
+  -- path' is the resolved, absolute path
+  path' <- findFile fileName
+  pm <- parseModule path'
   let n = thing (P.mName pm)
 
   -- Check whether this module name has already been loaded from a different file
   env <- getModuleEnv
   case lookupModule n env of
-    Nothing -> loadingModule n (loadModule path pm)
+    Nothing -> loadingModule n (loadModule path' pm)
     Just lm
-      | path == path' -> return (lmModule lm)
-      | otherwise     -> duplicateModuleName n path path'
-      where path' = lmFilePath lm
+      | path' == loaded -> return (lmModule lm)
+      | otherwise       -> duplicateModuleName n path' loaded
+      where loaded = lmFilePath lm
 
 
 -- | Load the module specified by an import.
@@ -202,6 +210,24 @@ findModule n = do
     ext  <- P.knownExts
     return (path </> moduleFile n ext)
 
+-- | Discover a file. This is distinct from 'findModule' in that we
+-- assume we've already been given a particular file name.
+findFile :: FilePath -> ModuleM FilePath
+findFile path | isAbsolute path = do
+  -- No search path checking for absolute paths
+  b <- io (doesFileExist path)
+  if b then return path else cantFindFile path
+findFile path = do
+  paths <- getSearchPath
+  loop (possibleFiles paths)
+  where
+  loop paths = case paths of
+    path':rest -> do
+      b <- io (doesFileExist path')
+      if b then return path' else loop rest
+    [] -> cantFindFile path
+  possibleFiles paths = map (</> path) paths
+
 preludeName :: P.ModName
 preludeName  = P.ModName ["Cryptol"]
 

src/Cryptol/ModuleSystem/Monad.hs

@@ -351,6 +351,19 @@ setFocusedModule n = ModuleT $ do
 getSearchPath :: ModuleM [FilePath]
 getSearchPath  = ModuleT (meSearchPath `fmap` get)
 
+-- | Run a 'ModuleM' action in a context with a prepended search
+-- path. Useful for temporarily looking in other places while
+-- resolving imports, for example.
+withPrependedSearchPath :: [FilePath] -> ModuleM a -> ModuleM a
+withPrependedSearchPath fps m = ModuleT $ do
+  env0 <- get
+  let fps0 = meSearchPath env0
+  set $! env0 { meSearchPath = fps ++ fps0 }
+  x <- unModuleT m
+  env <- get
+  set $! env { meSearchPath = fps0 }
+  return x
+
 -- XXX improve error handling here
 getFocusedEnv :: ModuleM IfaceDecls
 getFocusedEnv  = ModuleT (focusedEnv `fmap` get)

tests/issues/issue058.icry.stdout

@@ -2,29 +2,29 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 
-[error] at issue058.cry:10:1--10:17:
+[error] at ./issue058.cry:10:1--10:17:
   Failed to validate user-specified signature.
-    In the definition of 'Main::pad', at issue058.cry:10:1--10:4:
+    In the definition of 'Main::pad', at ./issue058.cry:10:1--10:4:
       for any type n
       fin n
         arising from
         use of expression (#)
-        at issue058.cry:10:11--10:12
-[error] at issue058.cry:7:1--7:17:
+        at ./issue058.cry:10:11--10:12
+[error] at ./issue058.cry:7:1--7:17:
   Failed to validate user-specified signature.
-    In the definition of 'Main::last', at issue058.cry:7:1--7:5:
+    In the definition of 'Main::last', at ./issue058.cry:7:1--7:5:
       for any type n, a
         n >= 1
       =>
       fin n
         arising from
         use of expression (!)
-        at issue058.cry:7:14--7:15
-[error] at issue058.cry:4:1--4:16:
+        at ./issue058.cry:7:14--7:15
+[error] at ./issue058.cry:4:1--4:16:
   Failed to validate user-specified signature.
-    In the definition of 'Main::some', at issue058.cry:4:1--4:5:
+    In the definition of 'Main::some', at ./issue058.cry:4:1--4:5:
       for any type n
       fin n
         arising from
         use of literal or demoted expression
-        at issue058.cry:4:15--4:16
+        at ./issue058.cry:4:15--4:16

tests/issues/issue127.icry

@@ -0,0 +1 @@
+:l issue127/issue127.cry

tests/issues/issue127.icry.stdout

@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Foo
+Loading module issue127

tests/issues/issue127/Foo.cry

@@ -0,0 +1,3 @@
+module Foo where
+
+x = 5

tests/issues/issue127/issue127.cry

@@ -0,0 +1,3 @@
+module issue127 where
+
+import Foo

tests/issues/issue198.icry.stdout

@@ -1,19 +1,19 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-[warning] at simon.cry2:83:1--92:15:
+[warning] at ./simon.cry2:83:1--92:15:
   Defaulting type parameter 'bits'
              of literal or demoted expression
-             at simon.cry2:87:34--87:35
+             at ./simon.cry2:87:34--87:35
   to max (width a`450) 3
-[warning] at simon.cry2:83:1--92:15:
+[warning] at ./simon.cry2:83:1--92:15:
   Defaulting type parameter 'bits'
              of literal or demoted expression
-             at simon.cry2:90:29--90:31
+             at ./simon.cry2:90:29--90:31
   to width a`452
-[warning] at simon.cry2:83:1--92:15:
+[warning] at ./simon.cry2:83:1--92:15:
   Defaulting type parameter 'bits'
              of literal or demoted expression
-             at simon.cry2:89:36--89:38
+             at ./simon.cry2:89:36--89:38
   to max (width (a`451 - 1)) (max (width a`450) 6)
 True

tests/mono-binds/test04.icry.stdout

@@ -16,17 +16,17 @@ test04::test = \{a, b} (b >= 4, fin b) (a : a) ->
 
 Loading module Cryptol
 Loading module test04
-[warning] at test04.cry:1:1--5:14:
+[warning] at ./test04.cry:1:1--5:14:
   Defaulting type parameter 'bits'
              of literal or demoted expression
-             at test04.cry:3:19--3:21
+             at ./test04.cry:3:19--3:21
   to 4
 
-[error] at test04.cry:3:19--3:21:
+[error] at ./test04.cry:3:19--3:21:
   Type mismatch:
     Expected type: ()
     Inferred type: [?k3]
   where
   ?k3 is type parameter 'bits'
          of literal or demoted expression
-         at test04.cry:3:19--3:21
+         at ./test04.cry:3:19--3:21

tests/mono-binds/test05.icry.stdout

@@ -1,12 +1,12 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module test05
-[warning] at test05.cry:9:3--9:6
+[warning] at ./test05.cry:9:3--9:6
     This binding for foo shadows the existing binding from
-    (at test05.cry:4:1--4:4, test05::foo)
-[warning] at test05.cry:13:5--13:8
+    (at ./test05.cry:4:1--4:4, test05::foo)
+[warning] at ./test05.cry:13:5--13:8
     This binding for foo shadows the existing binding from
-    (at test05.cry:9:3--9:6, foo)
+    (at ./test05.cry:9:3--9:6, foo)
 module test05
 import Cryptol
 /* Not recursive */
@@ -41,16 +41,16 @@ test05::test = \{a, b, c} (c >= 4, fin c) (a : [a]b) ->
 
 Loading module Cryptol
 Loading module test05
-[warning] at test05.cry:9:3--9:6
+[warning] at ./test05.cry:9:3--9:6
     This binding for foo shadows the existing binding from
-    (at test05.cry:4:1--4:4, test05::foo)
-[warning] at test05.cry:13:5--13:8
+    (at ./test05.cry:4:1--4:4, test05::foo)
+[warning] at ./test05.cry:13:5--13:8
     This binding for foo shadows the existing binding from
-    (at test05.cry:9:3--9:6, foo)
-[warning] at test05.cry:1:1--14:21:
+    (at ./test05.cry:9:3--9:6, foo)
+[warning] at ./test05.cry:1:1--14:21:
   Defaulting 1st type parameter
              of expression (#)
-             at test05.cry:14:16--14:17
+             at ./test05.cry:14:16--14:17
   to 0
 module test05
 import Cryptol

tests/regression/AES.icry.stdout

@@ -1,30 +1,30 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module AES
-[warning] at AES.cry:147:1--150:39:
+[warning] at ./AES.cry:147:1--150:39:
   Defaulting type parameter 'bits'
              of finite enumeration
-             at AES.cry:147:36--147:51
+             at ./AES.cry:147:36--147:51
   to 4
-[warning] at AES.cry:147:1--150:39:
+[warning] at ./AES.cry:147:1--150:39:
   Defaulting type parameter 'bits'
              of literal or demoted expression
-             at AES.cry:147:60--147:63
+             at ./AES.cry:147:60--147:63
   to 4
-[warning] at AES.cry:124:1--124:9:
+[warning] at ./AES.cry:124:1--124:9:
   Defaulting type parameter 'bits'
              of literal or demoted expression
-             at AES.cry:127:32--127:33
+             at ./AES.cry:127:32--127:33
   to 3
-[warning] at AES.cry:91:1--93:23:
+[warning] at ./AES.cry:91:1--93:23:
   Defaulting type parameter 'bits'
              of finite enumeration
-             at AES.cry:92:61--92:69
+             at ./AES.cry:92:61--92:69
   to 2
-[warning] at AES.cry:86:1--88:20:
+[warning] at ./AES.cry:86:1--88:20:
   Defaulting type parameter 'bits'
              of finite enumeration
-             at AES.cry:87:58--87:66
+             at ./AES.cry:87:58--87:66
   to 2
 True
 True

tests/regression/check01.icry.stdout

@@ -1,10 +1,10 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-[warning] at check01.cry:2:1--2:27:
+[warning] at ./check01.cry:2:1--2:27:
   Defaulting type parameter 'bits'
              of literal or demoted expression
-             at check01.cry:2:24--2:26
+             at ./check01.cry:2:24--2:26
   to 5
 [0x00000007, 0x00000014]
 True

tests/regression/check02.icry.stdout

@@ -4,7 +4,7 @@ Loading module Main
 [warning] at :1:1--3:25:
   Defaulting type parameter 'bits'
              of literal or demoted expression
-             at check02.cry:3:24--3:25
+             at ./check02.cry:3:24--3:25
   to 1
 [warning] at <interactive>:1:1--1:18:
   Defaulting type parameter 'bits'

tests/regression/check04.icry.stdout

@@ -4,12 +4,12 @@ Loading module Main
 [warning] at :1:1--4:45:
   Defaulting type parameter 'bits'
              of finite enumeration
-             at check04.cry:4:21--4:29
+             at ./check04.cry:4:21--4:29
   to 2
 [warning] at :1:1--4:45:
   Defaulting type parameter 'bits'
              of literal or demoted expression
-             at check04.cry:4:43--4:44
+             at ./check04.cry:4:43--4:44
   to 2
 [warning] at <interactive>:1:1--1:21:
   Defaulting type parameter 'bits'

tests/regression/check05.icry.stdout

@@ -4,12 +4,12 @@ Loading module Main
 [warning] at :1:1--4:45:
   Defaulting type parameter 'bits'
              of finite enumeration
-             at check05.cry:4:21--4:29
+             at ./check05.cry:4:21--4:29
   to 2
 [warning] at :1:1--4:45:
   Defaulting type parameter 'bits'
              of literal or demoted expression
-             at check05.cry:4:43--4:44
+             at ./check05.cry:4:43--4:44
   to 2
 [warning] at <interactive>:1:1--1:21:
   Defaulting type parameter 'bits'

tests/regression/check06.icry.stdout

@@ -4,12 +4,12 @@ Loading module Main
 [warning] at :1:1--5:70:
   Defaulting type parameter 'bits'
              of finite enumeration
-             at check06.cry:5:24--5:32
+             at ./check06.cry:5:24--5:32
   to 2
 [warning] at :1:1--5:70:
   Defaulting type parameter 'bits'
              of literal or demoted expression
-             at check06.cry:5:66--5:67
+             at ./check06.cry:5:66--5:67
   to 2
 [warning] at <interactive>:1:1--1:24:
   Defaulting type parameter 'bits'