fix #7212: Mimer respects C-u modifiers

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

@@ -1378,15 +1378,17 @@ Either only one if point is a goal, or all of them."
                           'agda2-mimerAll))
 )
 
-(defun agda2-mimer ()
+(agda2-maybe-normalised-asis
+  agda2-mimer
   "Run proof search on a goal."
-  (interactive)
-  (agda2-goal-cmd "Cmd_autoOne" 'save 'goal))
+  "Cmd_autoOne"
+  nil
+)
 
-(defun agda2-mimerAll ()
+(agda2-maybe-normalised-toplevel-asis-noprompt
+  agda2-mimerAll
   "Solves all goals by simple proof search."
-  (interactive)
-  (agda2-go nil nil 'busy t "Cmd_autoAll")
+  "Cmd_autoAll"
 )
 
 (agda2-maybe-normalised-toplevel-asis-noprompt

src/full/Agda/Interaction/Base.hs

@@ -169,8 +169,8 @@ data Interaction' range
   | Cmd_solveOne Rewrite InteractionId range String
 
     -- | Solve (all goals / the goal at point) by using Mimer proof search.
-  | Cmd_autoOne            InteractionId range String
-  | Cmd_autoAll
+  | Cmd_autoOne  Rewrite   InteractionId range String
+  | Cmd_autoAll  Rewrite
 
     -- | Parse the given expression (as if it were defined at the
     -- top-level of the current module) and infer its type.

src/full/Agda/Interaction/InteractionTop.hs

@@ -695,9 +695,9 @@ interpret (Cmd_refine_or_intro pmLambda ii r s) = interpret $
   let s' = trim s
   in (if null s' then Cmd_intro pmLambda else Cmd_refine) ii r s'
 
-interpret (Cmd_autoOne ii rng str) = do
+interpret (Cmd_autoOne norm ii rng str) = do
   iscope <- getInteractionScope ii
-  (time, result) <- maybeTimed $ Mimer.mimer ii rng str
+  (time, result) <- maybeTimed $ Mimer.mimer norm ii rng str
   case result of
     MimerNoResult -> display_info $ Info_Auto "No solution found"
     MimerExpr str -> do
@@ -711,7 +711,7 @@ interpret (Cmd_autoOne ii rng str) = do
         [ "  " ++ show i ++ ". " ++ s | (i, s) <- sols ]
     MimerClauses{} -> __IMPOSSIBLE__    -- Mimer can't do case splitting yet
 
-interpret Cmd_autoAll = do
+interpret (Cmd_autoAll norm) = do
   iis <- getInteractionPoints
   getOldScope <- do
     st <- getTC
@@ -721,7 +721,7 @@ interpret Cmd_autoAll = do
     st <- getTC
     solved <- fmap concat $ forM iis $ \ ii -> do
       rng <- getInteractionRange ii
-      res <- Mimer.mimer ii rng ("-t " ++ show time ++ "ms")
+      res <- Mimer.mimer norm ii rng ("-t " ++ show time ++ "ms")
       case res of
         MimerNoResult -> pure []
         MimerExpr str -> do

src/full/Agda/Mimer/Mimer.hs

@@ -77,6 +77,8 @@ import Data.IORef (IORef, writeIORef, readIORef, newIORef, modifyIORef')
 -- Temporary (used for custom cost verbosity hack)
 import qualified Agda.Utils.Maybe.Strict as Strict
 import qualified Agda.Utils.Trie as Trie
+import Agda.Interaction.Base (Rewrite(..))
+import Agda.Interaction.BasicOps (normalForm)
 import Agda.Interaction.Options.Base (parseVerboseKey)
 import Agda.Utils.List (lastWithDefault)
 
@@ -90,11 +92,12 @@ data MimerResult
 instance NFData MimerResult
 
 mimer :: MonadTCM tcm
-  => InteractionId
+  => Rewrite
+  -> InteractionId
   -> Range
   -> String
   -> tcm MimerResult
-mimer ii rng argStr = liftTCM $ do
+mimer norm ii rng argStr = liftTCM $ do
     reportSDoc "mimer.top" 10 ("Running Mimer on interaction point" <+> pretty ii <+> "with argument string" <+> text (show argStr))
 
     start <- liftIO $ getCPUTime
@@ -104,7 +107,7 @@ mimer ii rng argStr = liftTCM $ do
 
     oldState <- getTC
 
-    sols <- runSearch opts ii rng
+    sols <- runSearch norm opts ii rng
     putTC oldState
 
     sol <- case drop (optSkip opts) $ zip [0..] sols of
@@ -237,6 +240,7 @@ data SearchOptions = SearchOptions
   , searchFnName :: Maybe QName
   , searchCosts :: Costs
   , searchStats :: IORef MimerStats
+  , searchRewrite :: Rewrite
   }
 
 type Cost = Int
@@ -691,8 +695,8 @@ updateStat f = verboseS "mimer.stats" 10 $ do
 -- * Core algorithm
 ------------------------------------------------------------------------------
 
-runSearch :: Options -> InteractionId -> Range -> TCM [MimerResult]
-runSearch options ii rng = withInteractionId ii $ do
+runSearch :: Rewrite -> Options -> InteractionId -> Range -> TCM [MimerResult]
+runSearch norm options ii rng = withInteractionId ii $ do
   (mTheFunctionQName, whereNames) <- fmap ipClause (lookupInteractionPoint ii) <&> \case
     clause@IPClause{} -> ( Just $ ipcQName clause
                          , case A.whereDecls $ A.clauseWhereDecls $ ipcClause clause of
@@ -752,7 +756,7 @@ runSearch options ii rng = withInteractionId ii $ do
         InstV inst -> do
           expr <- withInteractionId ii $ do
             metaArgs <- getMetaContextArgs metaVar
-            instantiateFull (apply (MetaV metaId []) metaArgs) >>= reify
+            instantiateFull (apply (MetaV metaId []) metaArgs) >>= normalForm norm >>= reify
           str <- P.render <$> prettyTCM expr
           let sol = MimerExpr str
           reportSDoc "mimer.init" 10 $ "Goal already solved. Solution:" <+> text str
@@ -795,6 +799,7 @@ runSearch options ii rng = withInteractionId ii $ do
             , searchFnName = mTheFunctionQName
             , searchCosts = costs
             , searchStats = statsRef
+            , searchRewrite = norm
             }
 
       reportSDoc "mimer.init" 20 $ "Using search options:" $$ nest 2 (prettyTCM searchOptions)
@@ -1374,6 +1379,10 @@ applyToMetas skip term typ = do
       return (term', typ', metaId' : metas)
     _ -> return (term, typ, [])
 
+normaliseSolution :: Term -> SM Term
+normaliseSolution t = do
+  norm <- asks searchRewrite
+  lift . normalForm norm =<< instantiateFull t
 
 checkSolved :: SearchBranch -> SM SearchStepResult
 checkSolved branch = do
@@ -1382,7 +1391,7 @@ checkSolved branch = do
   ii <- asks searchInteractionId
   withInteractionId ii $ withBranchState branch $ do
     metaArgs <- getMetaContextArgs topMeta
-    inst <- instantiateFull $ apply (MetaV topMetaId []) metaArgs
+    inst <- normaliseSolution $ apply (MetaV topMetaId []) metaArgs
     case allMetas (:[]) inst of
       [] -> ResultExpr <$> reify inst
       metaIds -> do

test/interaction/Allto.in

@@ -1,2 +1,2 @@
 top_command (cmd_load currentFile [])
-top_command (cmd_autoAll)
+top_command (cmd_autoAll AsIs)

test/interaction/Auto-IndexedDatatypes.in

@@ -1,10 +1,10 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
-goal_command 1 cmd_autoOne ""
-goal_command 2 cmd_autoOne ""
-goal_command 3 cmd_autoOne ""
-goal_command 4 cmd_autoOne ""
-goal_command 5 cmd_autoOne ""
-goal_command 6 cmd_autoOne ""
-goal_command 7 cmd_autoOne "lookup"
-goal_command 8 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""
+goal_command 1 (cmd_autoOne AsIs) ""
+goal_command 2 (cmd_autoOne AsIs) ""
+goal_command 3 (cmd_autoOne AsIs) ""
+goal_command 4 (cmd_autoOne AsIs) ""
+goal_command 5 (cmd_autoOne AsIs) ""
+goal_command 6 (cmd_autoOne AsIs) ""
+goal_command 7 (cmd_autoOne AsIs) "lookup"
+goal_command 8 (cmd_autoOne AsIs) ""

test/interaction/Auto-Modules.in

@@ -1,5 +1,5 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
-goal_command 1 cmd_autoOne ""
-goal_command 2 cmd_autoOne ""
-goal_command 3 cmd_autoOne "p"
+goal_command 0 (cmd_autoOne AsIs) ""
+goal_command 1 (cmd_autoOne AsIs) ""
+goal_command 2 (cmd_autoOne AsIs) ""
+goal_command 3 (cmd_autoOne AsIs) "p"

test/interaction/Issue1148.in

@@ -1,4 +1,4 @@
 top_command (cmd_load currentFile [])
 goal_command 0 (cmd_refine_or_intro False) ""
-goal_command 1 cmd_autoOne ""
+goal_command 1 (cmd_autoOne AsIs) ""
 

test/interaction/Issue1169.in

@@ -1,3 +1,3 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
-goal_command 1 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""
+goal_command 1 (cmd_autoOne AsIs) ""

test/interaction/Issue1226.in

@@ -1,3 +1,3 @@
 ioTCM currentFile None Direct (cmd_load currentFile [])
 ioTCM currentFile Interactive Direct (cmd_refine 1 noRange "unit")
-ioTCM currentFile Interactive Direct (cmd_autoOne 0 noRange "")
+ioTCM currentFile Interactive Direct (cmd_autoOne AsIs 0 noRange "")

test/interaction/Issue1349.in

@@ -1,2 +1,2 @@
 top_command (cmd_load currentFile ["-i.","-i.."])
-goal_command 0 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""

test/interaction/Issue1504.in

@@ -1,2 +1,2 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""

test/interaction/Issue2162.in

@@ -1,2 +1,2 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""

test/interaction/Issue2472.in

@@ -1,2 +1,2 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""

test/interaction/Issue2492.in

@@ -1,2 +1,2 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""

test/interaction/Issue2620.in

@@ -1,2 +1,2 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""

test/interaction/Issue378.in

@@ -1,2 +1,2 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne "-m"
+goal_command 0 (cmd_autoOne AsIs) "-m"

test/interaction/Issue5794.in

@@ -1,2 +1,2 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""

test/interaction/Issue7084.in

@@ -1,2 +1,2 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""

test/interaction/Issue7085.in

@@ -1,3 +1,3 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne "M.a"
-goal_command 1 cmd_autoOne "M.a"
+goal_command 0 (cmd_autoOne AsIs) "M.a"
+goal_command 1 (cmd_autoOne AsIs) "M.a"

test/interaction/Issue7086.in

@@ -1,2 +1,2 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""

test/interaction/Issue7101.in

@@ -1,2 +1,2 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""

test/interaction/Issue7116.in

@@ -1,2 +1,2 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""

test/interaction/Issue7120.in

@@ -1,5 +1,5 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
-goal_command 1 cmd_autoOne ""
-goal_command 2 cmd_autoOne "-u"
-goal_command 3 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""
+goal_command 1 (cmd_autoOne AsIs) ""
+goal_command 2 (cmd_autoOne AsIs) "-u"
+goal_command 3 (cmd_autoOne AsIs) ""

test/interaction/Issue7133.in

@@ -1,2 +1,2 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""

test/interaction/Issue7212.agda

@@ -0,0 +1,12 @@
+
+open import Agda.Builtin.Nat
+
+infix 4 _≡_
+data _≡_ {A : Set} : A → A → Set where
+  refl : ∀ x → x ≡ x
+
+thm₁ : 1 + 1 ≡ 2
+thm₁ = {!!}
+
+thm₂ : 1 + 1 ≡ 2
+thm₂ = {!!}

test/interaction/Issue7212.in

@@ -0,0 +1,2 @@
+goal_command 0 (cmd_autoOne AsIs) ""
+goal_command 1 (cmd_autoOne Normalised) ""

test/interaction/Issue7212.out

@@ -0,0 +1,7 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-give-action 0 "refl (1 + 1)")
+((last . 1) . (agda2-goals-action '(1)))
+(agda2-give-action 1 "refl 2")
+((last . 1) . (agda2-goals-action '()))

test/interaction/Issue957.in

@@ -1,17 +1,17 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
-goal_command 1 cmd_autoOne ""
-goal_command 2 cmd_autoOne ""
-goal_command 3 cmd_autoOne ""
-goal_command 4 cmd_autoOne ""
-goal_command 5 cmd_autoOne ""
-goal_command 6 cmd_autoOne ""
-goal_command 7 cmd_autoOne ""
-goal_command 8 cmd_autoOne ""
-goal_command 9 cmd_autoOne ""
-goal_command 10 cmd_autoOne ""
-goal_command 11 cmd_autoOne ""
-goal_command 12 cmd_autoOne ""
-goal_command 13 cmd_autoOne ""
-goal_command 14 cmd_autoOne ""
-goal_command 15 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""
+goal_command 1 (cmd_autoOne AsIs) ""
+goal_command 2 (cmd_autoOne AsIs) ""
+goal_command 3 (cmd_autoOne AsIs) ""
+goal_command 4 (cmd_autoOne AsIs) ""
+goal_command 5 (cmd_autoOne AsIs) ""
+goal_command 6 (cmd_autoOne AsIs) ""
+goal_command 7 (cmd_autoOne AsIs) ""
+goal_command 8 (cmd_autoOne AsIs) ""
+goal_command 9 (cmd_autoOne AsIs) ""
+goal_command 10 (cmd_autoOne AsIs) ""
+goal_command 11 (cmd_autoOne AsIs) ""
+goal_command 12 (cmd_autoOne AsIs) ""
+goal_command 13 (cmd_autoOne AsIs) ""
+goal_command 14 (cmd_autoOne AsIs) ""
+goal_command 15 (cmd_autoOne AsIs) ""

test/interaction/Long.in

@@ -13,7 +13,7 @@ top_command (cmd_metas Normalised)
 goal_command 0 cmd_make_case "n"
 goal_command 0 (cmd_refine_or_intro False) "Just"
 goal_command 7 (cmd_refine_or_intro False) ""
-goal_command 4 cmd_autoOne ""
+goal_command 4 (cmd_autoOne AsIs) ""
 goal_command 3 (cmd_infer Instantiated) "D"
 goal_command 7 (cmd_context Normalised) ""
 goal_command 7 (cmd_goal_type Normalised) ""

test/interaction/Mimer-BasicLogic.in

@@ -1,19 +1,19 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
-goal_command 1 cmd_autoOne ""
-goal_command 2 cmd_autoOne ""
-goal_command 3 cmd_autoOne ""
--- goal_command 4 cmd_autoOne "-c"
--- goal_command 5 cmd_autoOne "-c"
--- goal_command 6 cmd_autoOne "-c"
-goal_command 7 cmd_autoOne ""
-goal_command 8 cmd_autoOne ""
-goal_command 9 cmd_autoOne ""
--- goal_command 10 cmd_autoOne ""
--- goal_command 11 cmd_autoOne "∨-e ⊥-e"
-goal_command 12 cmd_autoOne ""
-goal_command 13 cmd_autoOne ""
-goal_command 14 cmd_autoOne ""
-goal_command 15 cmd_autoOne ""
-goal_command 16 cmd_autoOne ""
--- goal_command 17 cmd_autoOne "RAA"
+goal_command 0 (cmd_autoOne AsIs) ""
+goal_command 1 (cmd_autoOne AsIs) ""
+goal_command 2 (cmd_autoOne AsIs) ""
+goal_command 3 (cmd_autoOne AsIs) ""
+-- goal_command 4 (cmd_autoOne AsIs) "-c"
+-- goal_command 5 (cmd_autoOne AsIs) "-c"
+-- goal_command 6 (cmd_autoOne AsIs) "-c"
+goal_command 7 (cmd_autoOne AsIs) ""
+goal_command 8 (cmd_autoOne AsIs) ""
+goal_command 9 (cmd_autoOne AsIs) ""
+-- goal_command 10 (cmd_autoOne AsIs) ""
+-- goal_command 11 (cmd_autoOne AsIs) "∨-e ⊥-e"
+goal_command 12 (cmd_autoOne AsIs) ""
+goal_command 13 (cmd_autoOne AsIs) ""
+goal_command 14 (cmd_autoOne AsIs) ""
+goal_command 15 (cmd_autoOne AsIs) ""
+goal_command 16 (cmd_autoOne AsIs) ""
+-- goal_command 17 (cmd_autoOne AsIs) "RAA"

test/interaction/Mimer-Misc.in

@@ -1,3 +1,3 @@
 top_command (cmd_load currentFile [])
-goal_command 0 cmd_autoOne ""
-goal_command 1 cmd_autoOne ""
+goal_command 0 (cmd_autoOne AsIs) ""
+goal_command 1 (cmd_autoOne AsIs) ""