[ fix agda#5695 ] New implementation of elaborate-and-give command (C…

…-c C-m)

src/full/Agda/Interaction/BasicOps.hs

@@ -212,6 +212,31 @@ give force ii mr e = liftTCM $ do
   removeInteractionPoint ii
   return e
 
+-- | Try to fill hole by elaborated expression.
+elaborate_give
+  :: Rewrite        -- ^ Normalise result?
+  -> UseForce       -- ^ Skip safety checks?
+  -> InteractionId  -- ^ Hole.
+  -> Maybe Range
+  -> Expr           -- ^ The expression to give.
+  -> TCM Expr       -- ^ If successful, return the elaborated expression.
+elaborate_give norm force ii mr e = withInteractionId ii $ do
+  -- if Range is given, update the range of the interaction meta
+  mi  <- lookupInteractionId ii
+  whenJust mr $ updateMetaVarRange mi
+  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
+     setMetaOccursCheck mi DontRunMetaOccursCheck -- #589, #2710: Allow giving recursive solutions.
+     giveExpr force (Just ii) mi e
+    `catchError` \ case
+      -- Turn PatternErr into proper error:
+      PatternErr{} -> typeError . GenericDocError =<< do
+        withInteractionId ii $ "Failed to give" TP.<+> prettyTCM e
+      err -> throwError err
+  nv <- normalForm norm v
+  locallyTC ePrintMetasBare (const True) $ reify nv
 
 -- | Try to refine hole by expression @e@.
 --

src/full/Agda/Interaction/InteractionTop.hs

@@ -739,16 +739,7 @@ interpret (Cmd_goal_type norm ii _ _) =
   display_info $ Info_GoalSpecific ii (Goal_CurrentGoal norm)
 
 interpret (Cmd_elaborate_give norm ii rng s) = do
-  have <- liftLocalState $ B.withInteractionId ii $ do
-    expr <- B.parseExprIn ii rng s
-    goal <- B.typeOfMeta AsIs ii
-    term <- case goal of
-      OfType _ ty -> checkExpr expr =<< isType_ ty
-      _           -> __IMPOSSIBLE__
-    nf <- B.normalForm norm term
-    txt <- localTC (\ e -> e { envPrintMetasBare = True }) (TCP.prettyTCM nf)
-    return $ show txt
-  give_gen WithoutForce ii rng have $ 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
@@ -979,7 +970,7 @@ give_gen force ii rng s0 giveRefine = do
             Give               -> B.give
             Refine             -> B.refine
             Intro              -> B.refine
-            ElaborateGive norm -> B.give
+            ElaborateGive norm -> B.elaborate_give norm
     -- save scope of the interaction point (for printing the given expr. later)
     scope     <- getInteractionScope ii
     -- parse string and "give", obtaining an abstract expression

test/interaction/Issue3316.out

@@ -4,6 +4,7 @@
 (agda2-status-action "")
 (agda2-info-action "*All Goals*" "?0 : Set " nil)
 ((last . 1) . (agda2-goals-action '(0)))
-(agda2-info-action "*Error*" "1,1-12 Not in scope: Issue3316.A at 1,1-12 when scope checking Issue3316.A" nil)
-(agda2-highlight-load-and-delete-action)
+(agda2-give-action 0 "Issue3316.A")
 (agda2-status-action "")
+(agda2-info-action "*All Done*" "" nil)
+((last . 1) . (agda2-goals-action '()))

test/interaction/Issue5695.agda

@@ -0,0 +1,15 @@
+open import Agda.Builtin.Bool
+open import Agda.Builtin.List
+open import Agda.Builtin.Nat
+open import Agda.Builtin.Unit
+open import Agda.Builtin.Reflection
+
+macro
+  printType : Term → TC ⊤
+  printType hole = bindTC (inferType hole) λ t → typeError (termErr t ∷ [])
+
+test1 : (a : Nat) → Nat
+test1 = {! printType  !}
+
+test2 : (a : Bool) → Bool
+test2 = {! printType  !}

test/interaction/Issue5695.in

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

test/interaction/Issue5695.out

@@ -0,0 +1,12 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-status-action "")
+(agda2-info-action "*All Goals*" "?0 : Nat → Nat ?1 : Bool → Bool " nil)
+((last . 1) . (agda2-goals-action '(0 1)))
+(agda2-info-action "*Error*" "1,1-10 (a : Nat) → Nat when checking that the expression unquote printType has type Nat → Nat" nil)
+(agda2-highlight-load-and-delete-action)
+(agda2-status-action "")
+(agda2-info-action "*Error*" "1,1-10 (a : Bool) → Bool when checking that the expression unquote printType has type Bool → Bool" nil)
+(agda2-highlight-load-and-delete-action)
+(agda2-status-action "")