From c1ed3c2fc8aa601950d885ee9df83e9a543e3ed1 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sat, 4 Jul 2020 21:25:41 +0100 Subject: [PATCH] Don't reload hints on import as We only need to reload the defined names so that we can set up the aliases - everything else is already loaded, and in particular adding hints twice will break implicit search. --- src/Core/Binary.idr | 21 ++++++++++++--------- src/Idris/ProcessIdr.idr | 11 +++++------ 2 files changed, 17 insertions(+), 15 deletions(-) diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 9ce7e9d08..68fa05a54 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -431,16 +431,19 @@ readFromTTC nestedns loc reexp fname modNS importAs traverse_ addUserHole (userHoles ttc) setNS (currentNS ttc) when nestedns $ setNestedNS (nestedNS ttc) + -- Only do the next batch if the module hasn't been loaded + -- in any form + when (not (modNS `elem` map (fst . getNSas) (allImported defs))) $ -- Set up typeHints and autoHints based on the loaded data - traverse_ (addTypeHint loc) (typeHints ttc) - traverse_ addAutoHint (autoHints ttc) - -- Set up pair/rewrite etc names - updatePair (pairnames ttc) - updateRewrite (rewritenames ttc) - updatePrims (primnames ttc) - updateNameDirectives (reverse (namedirectives ttc)) - updateCGDirectives (cgdirectives ttc) - updateTransforms (transforms ttc) + do traverse_ (addTypeHint loc) (typeHints ttc) + traverse_ addAutoHint (autoHints ttc) + -- Set up pair/rewrite etc names + updatePair (pairnames ttc) + updateRewrite (rewritenames ttc) + updatePrims (primnames ttc) + updateNameDirectives (reverse (namedirectives ttc)) + updateCGDirectives (cgdirectives ttc) + updateTransforms (transforms ttc) when (not reexp) clearSavedHints resetFirstEntry diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index afd513631..0e38e007c 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -62,11 +62,10 @@ readModule : {auto c : Ref Ctxt Defs} -> (full : Bool) -> -- load everything transitively (needed for REPL and compiling) FC -> (visible : Bool) -> -- Is import visible to top level module? - (reexp : Bool) -> -- Should the module be reexported? (imp : List String) -> -- Module name to import (as : List String) -> -- Namespace to import into Core () -readModule full loc vis reexp imp as +readModule full loc vis imp as = do defs <- get Ctxt let False = (imp, vis, as) `elem` map snd (allImported defs) | True => when vis (setVisible imp) @@ -84,7 +83,7 @@ readModule full loc vis reexp imp as do let m = fst mimp let reexp = fst (snd mimp) let as = snd (snd mimp) - when (reexp || full) $ readModule full loc (vis && reexp) reexp m as) more + when (reexp || full) $ readModule full loc reexp m as) more setNS modNS readImport : {auto c : Ref Ctxt Defs} -> @@ -92,7 +91,7 @@ readImport : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> Bool -> Import -> Core () readImport full imp - = do readModule full (loc imp) True (reexport imp) (path imp) (nameAs imp) + = do readModule full (loc imp) True (path imp) (nameAs imp) addImported (path imp, reexport imp, nameAs imp) ||| Adds new import to the namespace without changing the current top-level namespace @@ -148,13 +147,13 @@ readAsMain fname traverse_ (\ mimp => do let m = fst mimp let as = snd (snd mimp) - readModule True emptyFC True True m as + readModule True emptyFC True m as addImported (m, True, as)) more -- also load the prelude, if required, so that we have access to it -- at the REPL. when (not (noprelude !getSession)) $ - readModule True emptyFC True True ["Prelude"] ["Prelude"] + readModule True emptyFC True ["Prelude"] ["Prelude"] -- We're in the namespace from the first TTC, so use the next name -- from that for the fresh metavariable name generation