From 34f516d570bece8a1ebf450a89857370d4f68ad6 Mon Sep 17 00:00:00 2001 From: David Raymond Christiansen Date: Mon, 8 Jun 2015 16:56:58 +0200 Subject: [PATCH] Canonicalize paths in internalapp Otherwise, equal pathnames would not show up as equal, leading to problems in interactive editing if Idris's notion of a relative path didn't agree with the user's notion. For example, loading a file as "Foo/Bar.idr" would break interactive editing, because Idris would remember the name as "./Foo/Bar.idr". --- src/Idris/AbsSyntax.hs | 23 ++++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs index f6cfe95b5..b8b95a025 100644 --- a/src/Idris/AbsSyntax.hs +++ b/src/Idris/AbsSyntax.hs @@ -16,6 +16,7 @@ import Util.DynamicLinker import System.Console.Haskeline import System.IO +import System.Directory (canonicalizePath, doesFileExist) import Control.Applicative import Control.Monad (liftM3) @@ -516,14 +517,26 @@ getName = do i <- getIState; addInternalApp :: FilePath -> Int -> PTerm -> Idris () addInternalApp fp l t = do i <- getIState - putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i }) + -- We canonicalise the path to make "./Test/Module.idr" equal + -- to "Test/Module.idr" + exists <- runIO $ doesFileExist fp + when exists $ + do fp' <- runIO $ canonicalizePath fp + putIState (i { idris_lineapps = ((fp', l), t) : idris_lineapps i }) getInternalApp :: FilePath -> Int -> Idris PTerm getInternalApp fp l = do i <- getIState - case lookup (fp, l) (idris_lineapps i) of - Just n' -> return n' - Nothing -> return Placeholder - -- TODO: What if it's not there? + -- We canonicalise the path to make + -- "./Test/Module.idr" equal to + -- "Test/Module.idr" + exists <- runIO $ doesFileExist fp + if exists + then do fp' <- runIO $ canonicalizePath fp + case lookup (fp', l) (idris_lineapps i) of + Just n' -> return n' + Nothing -> return Placeholder + -- TODO: What if it's not there? + else return Placeholder -- Pattern definitions are only used for coverage checking, so erase them -- when we're done