[ fixed #4647 ] top-level interaction: access to private decls.

This commit addresses the problem that interaction commands that run
in the top-level, like C-c C-n, do not have access to private decls of
the main module.  These are deleted from the scope before
serialization, for reasons of performance (see #1806).

The solution implemented here is that interaction gets two modes:

1. RegularInteraction: Initial mode after C-c C-l.  The internal
representation of the top module, hence its insideScope, is loaded
from the interface file and thus has no knowledge of private
declarations.

2. TopLevelInteraction: Top-level interaction commands switch to this
mode, leading to a reload of the current top module in a way that
private declarations are preserved in the insideScope.  The module is
not serialized.

When a new file is loaded, we switch back to RegularInteraction.

The emacs mode had to be changed to switch on highlighting for
top-level commands, which was off because no highlighting would
happen.  Now, highlighting can happen due to a reload.

src/data/emacs-mode/agda2-mode.el

@@ -1193,7 +1193,7 @@ The form of the result depends on the prefix argument:
             (`(fromgoal ,want)
              `(agda2-goal-cmd (concat ,cmd " " ,eval) nil ,want))
             (`(global ,prompt)
-             `(agda2-go nil nil 'busy t
+             `(agda2-go nil t 'busy t
                         (concat ,cmd " "
                                 ,eval " "
                                 (if ,prompt
@@ -1269,7 +1269,7 @@ top-level scope."
 (defun agda2-why-in-scope-toplevel (name)
   "Explain why something is in scope at the top level."
   (interactive "MName: ")
-  (agda2-go nil nil 'busy t
+  (agda2-go nil t 'busy t
             "Cmd_why_in_scope_toplevel"
             (agda2-string-quote name)))
 
@@ -1426,7 +1426,7 @@ computation."
                      (cond ((equal arg nil) " DefaultCompute")
                             ((equal arg '(4)) " IgnoreAbstract")
                             (" UseShowInstance")) " ")))
-    (agda2-go nil nil 'busy t
+    (agda2-go nil t 'busy t
               (concat cmd (agda2-string-quote expr)))))
 
 (defun agda2-compute-normalised-maybe-toplevel ()

src/full/Agda/Interaction/Base.hs

@@ -41,11 +41,10 @@ data CommandState = CommandState
     --   recorded in 'theTCState', but when new interaction points are
     --   added by give or refine Agda does not ensure that the ranges
     --   of later interaction points are updated.
-  , theCurrentFile       :: Maybe (AbsolutePath, ClockTime)
+  , theCurrentFile       :: Maybe CurrentFile
     -- ^ The file which the state applies to. Only stored if the
     -- module was successfully type checked (potentially with
-    -- warnings). The 'ClockTime' is the modification time stamp of
-    -- the file when it was last loaded.
+    -- warnings).
   , optionsOnReload      :: CommandLineOptions
     -- ^ Reset the options on each reload to these.
   , oldInteractionScopes :: !OldInteractionScopes
@@ -57,6 +56,10 @@ data CommandState = CommandState
     --
     -- This queue should only be manipulated by
     -- 'initialiseCommandQueue' and 'maybeAbort'.
+  , interactionMode      :: !InteractionMode
+    -- ^ For top-level commands, we switch into a mode
+    --   where the interface contains also the private definitions.
+    --   See issues #4647 and #1804.
   }
 
 type OldInteractionScopes = Map InteractionId ScopeInfo
@@ -71,6 +74,7 @@ initCommandState commandQueue =
     , optionsOnReload      = defaultOptions
     , oldInteractionScopes = Map.empty
     , commandQueue         = commandQueue
+    , interactionMode      = RegularInteraction
     }
 
 -- | Monad for computing answers to interactive commands.
@@ -79,6 +83,36 @@ initCommandState commandQueue =
 
 type CommandM = StateT CommandState TCM
 
+-- | Information about the current main module.
+data CurrentFile = CurrentFile
+  { currentFilePath  :: AbsolutePath
+      -- ^ The file currently loaded into interaction.
+  , currentFileArgs  :: [String]
+      -- ^ The arguments to Agda used for loading the file.
+  , currentFileStamp :: ClockTime
+      -- ^ The modification time stamp of the file when it was loaded.
+  } deriving (Show)
+
+------------------------------------------------------------------------
+-- Interaction modes (issue #4647)
+
+-- | When a command is invoked at top-level, we wish to be the scope
+--   of the top-level module but also have access to the private
+--   declaration that are removed during serialization.
+--
+--   Thus, top-level commands switch to mode 'TopLevelInteraction'
+--   which initially reloads the current module to restore the
+--   private declarations into the scope.
+--
+--   Switching to a new file will fall back to 'RegularInteraction'.
+
+data InteractionMode
+  = RegularInteraction
+      -- ^ Initial mode. Use deserialized interface.
+  | TopLevelInteraction
+      -- ^ Mode for top-level commands.  Use original interface
+      --   that also contains the private declarations.
+  deriving (Show, Eq)
 
 ------------------------------------------------------------------------
 -- Command queues

src/full/Agda/Interaction/Imports.hs

@@ -51,7 +51,8 @@ import qualified Agda.TypeChecking.Monad.Benchmark as Bench
 
 import Agda.TheTypeChecker
 
-import Agda.Interaction.BasicOps (getGoals, showGoals)
+import Agda.Interaction.Base     ( InteractionMode(..) )
+import Agda.Interaction.BasicOps ( getGoals, showGoals )
 import Agda.Interaction.FindFile
 import Agda.Interaction.Highlighting.Generate
 import Agda.Interaction.Highlighting.Precise  ( compress )
@@ -105,7 +106,9 @@ sourceInfo (SourceFile f) = Bench.billTo [Bench.Parsing] $ do
 
 data Mode
   = ScopeCheck
-  | TypeCheck
+  | TypeCheck 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
@@ -231,9 +234,19 @@ alreadyVisited :: C.TopLevelModuleName ->
                   PragmaOptions ->
                   TCM (Interface, MaybeWarnings) ->
                   TCM (Interface, MaybeWarnings)
-alreadyVisited x isMain currentOptions getIface = do
-    mm <- getVisitedModule x
-    case mm of
+alreadyVisited x isMain currentOptions getIface =
+  case isMain of
+
+    -- Andreas, 2020-05-13, issue 4647:
+    -- For top-level interaction commands, we may not able to reuse
+    -- the existing interface, since it does not contain the private
+    -- declarations.  Thus, we always recheck.
+    MainInterface (TypeCheck TopLevelInteraction) -> fallback
+
+    _ -> getVisitedModule x >>= \case
+
+        -- Case: already visited.
+        --
         -- A module with warnings should never be allowed to be
         -- imported from another module.
         Just (ModuleInfo i hasWarn isPrim) | not hasWarn -> do
@@ -248,7 +261,13 @@ alreadyVisited x isMain currentOptions getIface = do
           if optsCompat then return (i , NoWarnings) else do
             wt <- getMaybeWarnings' isMain ErrorWarnings
             return (i, wt)
-        _ -> do
+
+        -- Case: Not visited already.
+        --
+        _ -> fallback
+
+  where
+  fallback = do
           reportSLn "import.visit" 5 $ "  Getting interface for " ++ prettyShow x
           r@(i, wt) <- getIface
           reportSLn "import.visit" 5 $ "  Now we've looked at " ++ prettyShow x
@@ -412,7 +431,8 @@ getInterface' x isMain msi =
         -- -- which is no longer serialized.
         -- let maySkip = isMain == NotMainInterface
         -- Andreas, 2015-07-13: Serialize iInsideScope again.
-        let maySkip = True
+        -- Andreas, 2020-05-13 issue #4647: don't skip if reload because of top-level command
+        let maySkip = isMain /= MainInterface (TypeCheck TopLevelInteraction)
 
         if uptodate && maySkip
           then getStoredInterface x file isMain msi
@@ -778,10 +798,12 @@ writeInterface file i = let fp = filePath file in do
     -- i <- return $
     --   i { iInsideScope  = emptyScopeInfo
     --     }
-    -- Andreas, 2016-02-02 this causes issue #1804, so don't do it:
-    -- i <- return $
-    --   i { iInsideScope  = removePrivates $ iInsideScope i
-    --     }
+    -- [Old: Andreas, 2016-02-02 this causes issue #1804, so don't do it:]
+    -- Andreas, 2020-05-13, #1804, #4647: removed private declarations
+    -- only when we actually write the interface.
+    i <- return $
+      i { iInsideScope  = removePrivates $ iInsideScope i
+        }
     reportSLn "import.iface.write" 50 $
       "Writing interface file with hash " ++ show (iFullHash i) ++ "."
     i' <- encodeFile fp i
@@ -801,7 +823,9 @@ writeInterface file i = let fp = filePath file in do
     throwError e
 
 removePrivates :: ScopeInfo -> ScopeInfo
-removePrivates = over scopeModules $ fmap restrictPrivate
+removePrivates scope = over scopeModules (fmap $ restrictLocalPrivate m) scope
+  where
+  m = scope ^. scopeCurrent
 
 concreteOptionsToOptionPragmas :: [C.Pragma] -> TCM [OptionsPragma]
 concreteOptionsToOptionPragmas p = do
@@ -1010,6 +1034,9 @@ createInterface file mname isMain msi =
       (_, MainInterface ScopeCheck) -> do
         reportSLn "import.iface.create" 7 "We are just scope-checking, skipping writing interface file."
         return i
+      (_, MainInterface (TypeCheck TopLevelInteraction)) -> do
+        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
         reportSLn "import.iface.create" 7 "Actually calling writeInterface."
         -- The file was successfully type-checked (and no warnings were