[ refactor ] Avoid special-casing envCurrentlyElaborating in enterClo…

…sure
agda · Dec 21, 2021 · 427911a · 427911a
1 parent c1c7d0b
commit 427911a
Show file tree

Hide file tree

Showing 3 changed files with 55 additions and 57 deletions.
diff --git a/src/full/Agda/Interaction/BasicOps.hs b/src/full/Agda/Interaction/BasicOps.hs
@@ -117,57 +117,56 @@ giveExpr force mii mi e = do
     mv <- lookupMeta mi
     -- In the context (incl. signature) of the meta variable,
     -- type check expression and assign meta
-    withMetaInfo (getMetaInfo mv) $ do
-      let t = case mvJudgement mv of
-                IsSort{}    -> __IMPOSSIBLE__
-                HasType _ _ t -> t
-      reportSDoc "interaction.give" 20 $
-        "give: meta type =" TP.<+> prettyTCM t
-      -- Here, we must be in the same context where the meta was created.
-      -- Thus, we can safely apply its type to the context variables.
-      ctx <- getContextArgs
-      t' <- t `piApplyM` permute (takeP (length ctx) $ mvPermutation mv) ctx
-      traceCall (CheckExprCall CmpLeq e t') $ do
-        reportSDoc "interaction.give" 20 $ do
-          a <- asksTC envAbstractMode
-          TP.hsep
-            [ TP.text ("give(" ++ show a ++ "): instantiated meta type =")
-            , prettyTCM t'
+    let t = case mvJudgement mv of
+              IsSort{}    -> __IMPOSSIBLE__
+              HasType _ _ t -> t
+    reportSDoc "interaction.give" 20 $
+      "give: meta type =" TP.<+> prettyTCM t
+    -- Here, we must be in the same context where the meta was created.
+    -- Thus, we can safely apply its type to the context variables.
+    ctx <- getContextArgs
+    t' <- t `piApplyM` permute (takeP (length ctx) $ mvPermutation mv) ctx
+    traceCall (CheckExprCall CmpLeq e t') $ do
+      reportSDoc "interaction.give" 20 $ do
+        a <- asksTC envAbstractMode
+        TP.hsep
+          [ TP.text ("give(" ++ show a ++ "): instantiated meta type =")
+          , prettyTCM t'
+          ]
+      -- Andreas, 2020-05-27 AIM XXXII, issue #4679
+      -- Clear envMutualBlock since cubical only executes
+      -- certain checks (checkIApplyConfluence) for an extended lambda
+      -- when not in a mutual block.
+      v <- locallyTC eMutualBlock (const Nothing) $
+        checkExpr e t'
+      case mvInstantiation mv of
+
+        InstV{} -> unlessM ((Irrelevant ==) <$> asksTC getRelevance) $ do
+          v' <- instantiate $ MetaV mi $ map Apply ctx
+          reportSDoc "interaction.give" 20 $ TP.sep
+            [ "meta was already set to value v' = " TP.<+> prettyTCM v'
+            , "now comparing it to given value v = " TP.<+> prettyTCM v
+            , "in context " TP.<+> inTopContext (prettyTCM ctx)
             ]
-        -- Andreas, 2020-05-27 AIM XXXII, issue #4679
-        -- Clear envMutualBlock since cubical only executes
-        -- certain checks (checkIApplyConfluence) for an extended lambda
-        -- when not in a mutual block.
-        v <- locallyTC eMutualBlock (const Nothing) $
-          checkExpr e t'
-        case mvInstantiation mv of
-
-          InstV{} -> unlessM ((Irrelevant ==) <$> asksTC getRelevance) $ do
-            v' <- instantiate $ MetaV mi $ map Apply ctx
-            reportSDoc "interaction.give" 20 $ TP.sep
-              [ "meta was already set to value v' = " TP.<+> prettyTCM v'
-              , "now comparing it to given value v = " TP.<+> prettyTCM v
-              , "in context " TP.<+> inTopContext (prettyTCM ctx)
-              ]
-            equalTerm t' v v'
-
-          _ -> do -- updateMeta mi v
-            reportSLn "interaction.give" 20 "give: meta unassigned, assigning..."
-            args <- getContextArgs
-            nowSolvingConstraints $ assign DirEq mi args v (AsTermsOf t')
-
-        reportSDoc "interaction.give" 20 $ "give: meta variable updated!"
-        unless (force == WithForce) $ redoChecks mii
-        wakeupConstraints mi
-        solveSizeConstraints DontDefaultToInfty
-        cubical <- isJust . optCubical <$> pragmaOptions
-        -- don't double check with cubical, because it gets in the way too often.
-        unless (cubical || force == WithForce) $ do
-          -- Double check.
-          reportSDoc "interaction.give" 20 $ "give: double checking"
-          vfull <- instantiateFull v
-          checkInternal vfull CmpLeq t'
-        return v
+          equalTerm t' v v'
+
+        _ -> do -- updateMeta mi v
+          reportSLn "interaction.give" 20 "give: meta unassigned, assigning..."
+          args <- getContextArgs
+          nowSolvingConstraints $ assign DirEq mi args v (AsTermsOf t')
+
+      reportSDoc "interaction.give" 20 $ "give: meta variable updated!"
+      unless (force == WithForce) $ redoChecks mii
+      wakeupConstraints mi
+      solveSizeConstraints DontDefaultToInfty
+      cubical <- isJust . optCubical <$> pragmaOptions
+      -- don't double check with cubical, because it gets in the way too often.
+      unless (cubical || force == WithForce) $ do
+        -- Double check.
+        reportSDoc "interaction.give" 20 $ "give: double checking"
+        vfull <- instantiateFull v
+        checkInternal vfull CmpLeq t'
+      return v
 
 -- | After a give, redo termination etc. checks for function which was complemented.
 redoChecks :: Maybe InteractionId -> TCM ()
@@ -201,7 +200,7 @@ give force ii mr e = liftTCM $ do
   reportSDoc "interaction.give" 10 $ "giving expression" TP.<+> prettyTCM e
   reportSDoc "interaction.give" 50 $ TP.text $ show $ deepUnscope e
   -- Try to give mi := e
-  _ <- do
+  _ <- withInteractionId ii $ do
      setMetaOccursCheck mi DontRunMetaOccursCheck -- #589, #2710: Allow giving recursive solutions.
      giveExpr force (Just ii) mi e
     `catchError` \ case
@@ -227,9 +226,10 @@ elaborate_give norm force ii mr e = withInteractionId ii $ do
   reportSDoc "interaction.give" 10 $ "giving expression" TP.<+> prettyTCM e
   reportSDoc "interaction.give" 50 $ TP.text $ show $ deepUnscope e
   -- Try to give mi := e
-  v <- do
+  v <- withInteractionId ii $ do
      setMetaOccursCheck mi DontRunMetaOccursCheck -- #589, #2710: Allow giving recursive solutions.
-     giveExpr force (Just ii) mi e
+     locallyTC eCurrentlyElaborating (const True) $
+       giveExpr force (Just ii) mi e
     `catchError` \ case
       -- Turn PatternErr into proper error:
       PatternErr{} -> typeError . GenericDocError =<< do

diff --git a/src/full/Agda/Interaction/InteractionTop.hs b/src/full/Agda/Interaction/InteractionTop.hs
@@ -740,8 +740,7 @@ interpret (Cmd_goal_type norm ii _ _) =
   display_info $ Info_GoalSpecific ii (Goal_CurrentGoal norm)
 
 interpret (Cmd_elaborate_give norm ii rng s) =
-  locallyTC eCurrentlyElaborating (const True) $
-    give_gen WithoutForce ii rng s $ ElaborateGive norm
+  give_gen WithoutForce ii rng s $ ElaborateGive norm
 
 interpret (Cmd_goal_type_context norm ii rng s) =
   cmd_goal_type_context_and GoalOnly norm ii rng s

diff --git a/src/full/Agda/TypeChecking/Monad/Closure.hs b/src/full/Agda/TypeChecking/Monad/Closure.hs
@@ -12,10 +12,9 @@ enterClosure :: (MonadTCEnv m, ReadTCState m, LensClosure a c)
              => c -> (a -> m b) -> m b
 enterClosure c k | Closure _sig env scope cps x <- c ^. lensClosure = do
   isDbg <- viewTC eIsDebugPrinting
-  isElab <- viewTC eCurrentlyElaborating
   withScope_ scope
     $ locallyTCState stModuleCheckpoints (const cps)
-    $ withEnv env{ envIsDebugPrinting = isDbg, envCurrentlyElaborating = isElab }
+    $ withEnv env{ envIsDebugPrinting = isDbg }
     $ k x
 
 withClosure :: (MonadTCEnv m, ReadTCState m) => Closure a -> (a -> m b) -> m (Closure b)