[ WIP #4959 ] clarify cmd_load' interface

src/full/Agda/Interaction/Imports.hs

@@ -4,7 +4,7 @@
     interface files.
 -}
 module Agda.Interaction.Imports
-  ( Mode(ScopeCheck, TypeCheck)
+  ( Mode, Mode', pattern ScopeCheck, pattern TypeCheck
 
   , CheckResult (CheckResult)
   , crModuleInfo
@@ -161,12 +161,14 @@ setOptionsFromSourcePragmas src =
 -- | Is the aim to type-check the top-level module, or only to
 -- scope-check it?
 
-data Mode
+data Mode' a
   = ScopeCheck
-  | TypeCheck InteractionMode
+  | TypeCheck a
+  deriving (Eq, Show, Functor, Foldable)
+
+type Mode = Mode' InteractionMode
       -- ^ Depending on the 'InteractionMode' private declaration may be retained
       --   in the interface.
-  deriving (Eq, Show)
 
 -- | Are we loading the interface for the user-loaded file
 --   or for an import?
@@ -1096,6 +1098,13 @@ createInterface mname file isMain msrc = do
         reportSLn "import.iface.create" 7 "We are just scope-checking, skipping writing interface file."
         return i
       ([], MainInterface (TypeCheck TopLevelInteraction)) -> do
+        -- -- suggested by unclebetty at https://github.com/agda/agda/issues/4959#issuecomment-706179266
+        -- reportSLn "import.iface.create" 7 $ unlines
+        --   [ "We are in top-level interaction mode and want to retain private declarations."
+        --   , "We write the interface file but retain the private declarations."
+        --   ]
+        -- ifile <- toIFile file
+        -- _serializedIface <- writeInterface ifile i
         reportSLn "import.iface.create" 7 "We are in top-level interaction mode and want to retain private declarations, skipping writing interface file."
         return i
       ([], _) -> Bench.billTo [Bench.Serialization] $ do

src/full/Agda/Interaction/InteractionTop.hs

@@ -60,7 +60,7 @@ import Agda.Interaction.Response hiding (Function, ExtendedLambda)
 import qualified Agda.Interaction.Response as R
 import qualified Agda.Interaction.BasicOps as B
 import Agda.Interaction.Highlighting.Precise hiding (Error, Postulate, singleton)
-import Agda.Interaction.Imports  ( Mode(..) )
+import Agda.Interaction.Imports  ( Mode, Mode', pattern ScopeCheck, pattern TypeCheck )
 import qualified Agda.Interaction.Imports as Imp
 import Agda.Interaction.Highlighting.Generate
 
@@ -283,7 +283,7 @@ runInteraction (IOTCM current highlighting highlightingMethod cmd) =
     -- loaded.
     cf <- gets theCurrentFile
     when (not (independent cmd) && Just currentAbs /= (currentFilePath <$> cf)) $ do
-        let mode = Imp.TypeCheck TopLevelInteraction
+        let mode = TypeCheck Nothing
         cmd_load' current [] True mode $ \_ -> return ()
 
     withCurrentFile $ interpret cmd
@@ -496,7 +496,7 @@ interpret :: Interaction -> CommandM ()
 interpret (Cmd_load m argv) =
   cmd_load' m argv True mode $ \_ -> interpret $ Cmd_metas AsIs
   where
-  mode = Imp.TypeCheck TopLevelInteraction -- do not reset InteractionMode
+  mode = TypeCheck Nothing -- do not reset InteractionMode
 
 interpret (Cmd_compile backend file argv) =
   cmd_load' file argv allowUnsolved mode $ \ checkResult -> do
@@ -512,8 +512,8 @@ interpret (Cmd_compile backend file argv) =
       w@(_:_) -> display_info $ Info_Error $ Info_CompilationError w
   where
   allowUnsolved = backend `elem` [LaTeX, QuickLaTeX]
-  mode | QuickLaTeX <- backend = Imp.ScopeCheck
-       | otherwise             = Imp.TypeCheck RegularInteraction  -- reset InteractionMode
+  mode | QuickLaTeX <- backend = ScopeCheck
+       | otherwise             = TypeCheck $ Just RegularInteraction  -- reset InteractionMode
 
 interpret Cmd_constraints =
     display_info . Info_Constraints =<< lift B.getConstraints
@@ -869,27 +869,35 @@ cmd_load'
   :: FilePath  -- ^ File to load into interaction.
   -> [String]  -- ^ Arguments to Agda for loading this file
   -> Bool      -- ^ Allow unsolved meta-variables?
-  -> Imp.Mode  -- ^ Full type-checking, or only scope-checking?
-               --   Providing 'TypeCheck RegularInteraction' here
+  -> Mode' (Maybe InteractionMode)
+               -- ^ Full type-checking, or only scope-checking?
+               --   Providing 'TypeCheck (Just mode)' here
                --   will reset 'InteractionMode' accordingly.
-               --   Otherwise, only if different file from last time.
+               --   Otherwise, reset to 'RegularInteraction'
+               --   only if different file from last time.
   -> (CheckResult -> CommandM a)
                -- ^ Continuation after successful loading.
   -> CommandM a
-cmd_load' file argv unsolvedOK mode cmd = do
+cmd_load' file argv unsolvedOK modeChange cmd = do
     fp <- liftIO $ absolute file
     ex <- liftIO $ doesFileExist $ filePath fp
     unless ex $ typeError $ GenericError $
       "The file " ++ file ++ " was not found."
 
-    -- When switching to a new file, or @mode@ indicates such a reset,
+    -- When switching to a new file, or @modeChange@ indicates such a reset,
     -- fall back to RegularInteraction.
-    mode <- gets theCurrentFile >>= \case
-      Just CurrentFile{ currentFilePath = fp' }
-        | mode /= TypeCheck RegularInteraction
-        , fp == fp'
-        -> pure mode  -- keep InteractionMode
-      _ -> regularMode mode <$ setInteractionMode RegularInteraction  -- reset
+    mode <- do
+      let typeCheckMode m = TypeCheck m <$ setInteractionMode m
+      case modeChange of
+        ScopeCheck               -> pure ScopeCheck
+        TypeCheck (Just newmode) -> typeCheckMode newmode
+        TypeCheck Nothing        -> do
+          -- If the file has not changed, keep the existing mode, otherwise
+          -- use 'RegularInteraction' mode.
+          gets theCurrentFile >>= \case
+            Just CurrentFile{ currentFilePath = fp' } | fp == fp'
+              -> TypeCheck <$> gets interactionMode
+            _ -> typeCheckMode RegularInteraction
 
     -- Forget the previous "current file" and interaction points.
     modify $ \ st -> st { theInteractionPoints = []
@@ -973,13 +981,12 @@ atTopLevel cmd = do
     TopLevelInteraction -> continue  -- Already in the correct mode.
     RegularInteraction  -> continue `handleNotInScope` do
       -- Have to switch mode.
-      setInteractionMode TopLevelInteraction
       CurrentFile file argv _stamp <- gets $ fromMaybe __IMPOSSIBLE__ . theCurrentFile
+      let allowUnsolved = True
+          mode          = TypeCheck $ Just TopLevelInteraction
       cmd_load' (filePath file) argv allowUnsolved mode $ \ _ -> continue
   where
   continue      = liftCommandMT B.atTopLevel cmd
-  allowUnsolved = True
-  mode          = Imp.TypeCheck TopLevelInteraction
 
 setInteractionMode :: InteractionMode -> CommandM ()
 setInteractionMode mode = modify $ \ st -> st { interactionMode = mode }

test/interaction/Issue4959.out

@@ -16,7 +16,6 @@
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)
 (agda2-info-action "*Type-checking*" "Checking Issue4959 (Issue4959.agda). " t)
-(agda2-info-action "*Type-checking*" " Checking Issue4959-2 (Issue4959-2.agda). " t)
 (agda2-status-action "Checked")
 (agda2-info-action "*All Done*" "" nil)
 ((last . 1) . (agda2-goals-action '()))

test/interaction/TopScope.agda

@@ -12,3 +12,14 @@ private
   not-in-scope = true
 
 in-scope = used
+
+-- History:
+--
+-- * Ulf, 2015-20-12 c823aa9a0e84816d3e36ea86e04e9f9caa536c4a
+--   [ deadcode ] local private things are not in scope at top-level
+--                but imported things should be
+--   The previous restriction of the top level scope (7f47d51c) was a
+--   bit draconian and removed not only local private definitions but
+--   all imported things from the scope. This is fixed by this commit.
+--
+-- * Andreas, 2021-05-18, used as testcase for issue #4647

test/interaction/TopScope.in

@@ -1,6 +1,6 @@
 top_command (cmd_load currentFile ["-i.", "-i.."])
 top_command (cmd_load currentFile ["-i.", "-i.."])
--- These should give not in scope errors:
+-- Issue #4647: These should no longer give in scope errors:
 top_command (cmd_infer_toplevel Normalised "unused")
 top_command (cmd_infer_toplevel Normalised "used")
 top_command (cmd_infer_toplevel Normalised "Private.not-in-scope")

test/interaction/TopScope.out

@@ -10,10 +10,19 @@
 (agda2-status-action "Checked")
 (agda2-info-action "*All Done*" "" nil)
 ((last . 1) . (agda2-goals-action '()))
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
 (agda2-status-action "Checked")
 (agda2-info-action "*Inferred Type*" "Bool" nil)
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
 (agda2-status-action "Checked")
 (agda2-info-action "*Inferred Type*" "Bool" nil)
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
 (agda2-status-action "Checked")
 (agda2-info-action "*Inferred Type*" "Bool" nil)
 (agda2-status-action "Checked")