[ fixed agda#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 agda#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.

UPDATE: only switch to TopLevelInteraction when NotInScope error.

Catch not-in-scope errors in top-level interaction commands such as

  C-c C-d  infer
  C-c C-n  evaluate
  C-c C-o  module contents
  C-c C-w  why in scope

and try to handle by reloading file in TopLevelInteraction mode that
preserves the private declarations.

Caveat: commands that do not throw scope errors such as

  C-c C-z  search about

will by default (RegularInteraction) not include the private
declarations, only if some other top-level command switches to
TopLevelInteraction, then the private declarations will also be listed.

Note: Top-level commands that lead to a reload have to be used
with care in interaction tests.
Solutions given to metas by interaction commands get lost by reloads,
since they are not incorporated into the source file (naturally).  The
situation is now similar to why case splits do no update the state of
the interaction.

Instructions how to revert ...
------------------------------

... the changes introduced in interaction that are introduced by this
patch:

A simple `git revert` won't do since there are code improvements
contained in this patch that should not be reverted.

However, a manual revert is: remove data type

  Agda.Interaction.Base.InteractionMode

and go with the flow.  Any choices that use this bit should collapsed
as if there was only the value

  RegularInteraction

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

@@ -40,11 +40,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
@@ -56,6 +55,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
@@ -70,6 +73,7 @@ initCommandState commandQueue =
     , optionsOnReload      = defaultOptions
     , oldInteractionScopes = Map.empty
     , commandQueue         = commandQueue
+    , interactionMode      = RegularInteraction
     }
 
 -- | Monad for computing answers to interactive commands.
@@ -78,6 +82,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/BasicOps.hs

@@ -1246,6 +1246,8 @@ whyInScope :: String -> TCM (Maybe LocalVar, [AbstractName], [AbstractModule])
 whyInScope s = do
   x     <- parseName noRange s
   scope <- getScope
-  return ( lookup x $ map (first C.QName) $ scope ^. scopeLocals
+  ifNull ( lookup x $ map (first C.QName) $ scope ^. scopeLocals
          , scopeLookup x scope
          , scopeLookup x scope )
+    {-then-} (notInScopeError x)  -- Andreas, 2020-05-15, issue #4647 throw error to trigger TopLevelInteraction
+    {-else-} return

src/full/Agda/Interaction/Imports.hs

@@ -52,7 +52,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