Make pathToNS handle absolute path

src/Core/Directory.idr

@@ -87,12 +87,16 @@ nsToSource loc ns
 -- Given a filename in the working directory + source directory, return the correct
 -- namespace for it
 export
-pathToNS : String -> Maybe String -> String -> List String
+pathToNS : String -> Maybe String -> String -> Core (List String)
 pathToNS wdir sdir fname
-    = let sdir = fromMaybe "" sdir in
-        case stripPrefix sdir fname of
-             Nothing => []
-             Just p => map show $ reverse $ (parse (p <.> "")).body
+    = let sdir = fromMaybe "" sdir
+          base = if isAbsolute fname then wdir </> sdir else sdir
+        in
+          case stripPrefix base fname of
+               Nothing => throw (UserError ("Source file " ++ show fname 
+                                            ++ " is not in the source directory " 
+                                            ++ show (wdir </> sdir)))
+               Just p => pure $ map show $ reverse $ (parse (p <.> "")).body
 
 dirExists : String -> IO Bool
 dirExists dir = do Right d <- openDir dir
@@ -148,7 +152,7 @@ getTTCFileName inp ext
          d <- getDirs
          -- Get its namespace from the file relative to the working directory
          -- and generate the ttc file from that
-         let ns = pathToNS (working_dir d) (source_dir d) inp
+         ns <- pathToNS (working_dir d) (source_dir d) inp
          let fname = joinPath (reverse ns) <.> ext
          let bdir = build_dir d
          pure $ bdir </> "ttc" </> fname

src/Idris/Main.idr

@@ -122,13 +122,6 @@ checkVerbose [] = False
 checkVerbose (Verbose :: _) = True
 checkVerbose (_ :: xs) = checkVerbose xs
 
-checkRelative : Maybe String -> Core (Maybe String)
-checkRelative Nothing = pure Nothing
-checkRelative (Just str)
-    = if isAbsolute str
-         then throw (InternalError "Absolute paths only allowed with --find-ipkg")
-         else pure (Just str)
-
 stMain : List CLOpt -> Core ()
 stMain opts
     = do False <- tryYaffle opts
@@ -170,7 +163,7 @@ stMain opts
                    iputStrLn banner
                  fname <- if findipkg session
                              then findIpkg fname
-                             else checkRelative fname
+                             else pure fname
                  setMainFile fname
                  the (Core ()) $ case fname of
                       Nothing => logTime "Loading prelude" $

src/Idris/ModTree.idr

@@ -126,7 +126,7 @@ getBuildMods : {auto c : Ref Ctxt Defs} ->
 getBuildMods loc done fname
     = do a <- newRef AllMods []
          d <- getDirs
-         let fname_ns = pathToNS (working_dir d) (source_dir d) fname
+         fname_ns <- pathToNS (working_dir d) (source_dir d) fname
          if fname_ns `elem` map buildNS done
             then pure []
             else
@@ -158,7 +158,7 @@ buildMod loc num len mod
    = do clearCtxt; addPrimitives
         lazyActive True; setUnboundImplicits True
         let src = buildFile mod
-        mttc <- getTTCFileName src ".ttc"
+        mttc <- getTTCFileName src "ttc"
         -- We'd expect any errors in nsToPath to have been caught by now
         -- since the imports have been built! But we still have to check.
         depFilesE <- traverse (nsToPath loc) (imports mod)
@@ -230,12 +230,12 @@ buildDeps fname
               [] => do -- On success, reload the main ttc in a clean context
                        clearCtxt; addPrimitives
                        put MD initMetadata
-                       mainttc <- getTTCFileName fname ".ttc"
+                       mainttc <- getTTCFileName fname "ttc"
                        log 10 $ "Reloading " ++ show mainttc ++ " from " ++ fname
                        readAsMain mainttc
 
                        -- Load the associated metadata for interactive editing
-                       mainttm <- getTTCFileName fname ".ttm"
+                       mainttm <- getTTCFileName fname "ttm"
                        log 10 $ "Reloading " ++ show mainttm
                        readFromTTM mainttm
                        pure []

src/Idris/Package.idr

@@ -550,9 +550,7 @@ findIpkg : {auto c : Ref Ctxt Defs} ->
            Maybe String -> Core (Maybe String)
 findIpkg fname
    = do Just (dir, ipkgn, up) <- coreLift findIpkgFile
-             | Nothing => case fname of
-                               Nothing => pure Nothing
-                               Just srcpath => pure (fileName srcpath)
+             | Nothing => pure fname
         coreLift $ changeDir dir
         Right (pname, fs) <- coreLift $ parseFile ipkgn
                                  (do desc <- parsePkgDesc ipkgn
@@ -566,10 +564,8 @@ findIpkg fname
         loadDependencies (depends pkg)
         case fname of
              Nothing => pure Nothing
-             Just srcpath =>
-                do let Just src = fileName srcpath
-                       | _ => pure (Just srcpath)
-                   let src' = up </> src
+             Just srcpath  =>
+                do let src' = up </> srcpath 
                    setSource src'
                    opts <- get ROpts
                    put ROpts (record { mainfile = Just src' } opts)

src/Idris/ProcessIdr.idr

@@ -265,7 +265,8 @@ processMod srcf ttcf msg sourcecode
                 when (ns /= ["Main"]) $
                    do let MkFC fname _ _ = headerloc mod
                       d <- getDirs
-                      when (pathToNS (working_dir d) (source_dir d) fname /= ns) $
+                      ns' <- pathToNS (working_dir d) (source_dir d) fname
+                      when (ns /= ns') $
                           throw (GenericMsg (headerloc mod)
                                    ("Module name " ++ showSep "." (reverse ns) ++
                                     " does not match file name " ++ fname))
@@ -310,7 +311,7 @@ process : {auto c : Ref Ctxt Defs} ->
 process buildmsg file
     = do Right res <- coreLift (readFile file)
                | Left err => pure [FileErr file err]
-         catch (do ttcf <- getTTCFileName file ".ttc"
+         catch (do ttcf <- getTTCFileName file "ttc"
                    Just errs <- logTime ("Elaborating " ++ file) $
                                    processMod file ttcf buildmsg res
                         | Nothing => pure [] -- skipped it
@@ -318,9 +319,10 @@ process buildmsg file
                       then
                         do defs <- get Ctxt
                            d <- getDirs
-                           makeBuildDirectory (pathToNS (working_dir d) (source_dir d) file)
+                           ns <- pathToNS (working_dir d) (source_dir d) file
+                           makeBuildDirectory ns
                            writeToTTC !(get Syn) ttcf
-                           ttmf <- getTTCFileName file ".ttm"
+                           ttmf <- getTTCFileName file "ttm"
                            writeToTTM ttmf
                            pure []
                       else do pure errs)

src/Utils/Path.idr

@@ -217,6 +217,9 @@ parsePath = do vol <- optional parseVolume
                trailSep <- optional (some bodySeparator)
                let body = filter (\case Normal s => ltrim s /= ""
                                         _ => True) body
+               let body = case body of
+                               [] => []
+                               (x::xs) => x :: delete CurDir xs
                pure $ MkPath vol (isJust root) body (isJust trailSep)
 
 ||| Parse a String into Path component.
@@ -246,14 +249,9 @@ parsePath = do vol <- optional parseVolume
 ||| ```
 export
 parse : String -> Path
-parse str = let p = case parse parsePath (lexPath str) of
-                         Right (p, _) => p
-                         _ => emptyPath
-                body' = case p.body of
-                             [] => []
-                             (x::xs) => x :: delete CurDir xs
-              in
-                record { body = body' } p
+parse str = case parse parsePath (lexPath str) of
+                 Right (p, _) => p
+                 _ => emptyPath
 
 --------------------------------------------------------------------------------
 -- Utils

src/Yaffle/Main.idr

@@ -13,6 +13,7 @@ import Core.Normalise
 import Core.Options
 import Core.TT
 import Core.UnifyState
+import Utils.Path
 
 import TTImp.Parser
 import TTImp.ProcessDecls
@@ -52,15 +53,16 @@ yaffleMain fname args
          t <- processArgs args
          setLogTimings t
          addPrimitives
-         case span (/= '.') fname of
-              (_, ".ttc") => do coreLift $ putStrLn "Processing as TTC"
-                                readFromTTC {extra = ()} True emptyFC True fname [] []
-                                coreLift $ putStrLn "Read TTC"
+         case extension fname of
+              Just "ttc" => do coreLift $ putStrLn "Processing as TTC"
+                               readFromTTC {extra = ()} True emptyFC True fname [] []
+                               coreLift $ putStrLn "Read TTC"
               _ => do coreLift $ putStrLn "Processing as TTImp"
                       ok <- processTTImpFile fname
                       when ok $
-                         do makeBuildDirectory (pathToNS (working_dir d) (source_dir d) fname)
-                            writeToTTC () !(getTTCFileName fname ".ttc")
+                         do ns <- pathToNS (working_dir d) (source_dir d) fname
+                            makeBuildDirectory ns
+                            writeToTTC () !(getTTCFileName fname "ttc")
                             coreLift $ putStrLn "Written TTC"
          ust <- get UST