Merge pull request 'fix(frontend): Capture local instances in `MetaTranslate`' (#242) from bug/meta-translate-local-instances into dev

Reviewed-on: #242

Pantograph/Frontend/MetaTranslate.lean

@@ -111,7 +111,7 @@ partial def translateLCtx : MetaTranslateM LocalContext := do
   let lctx ← MonadLCtx.getLCtx
   assert! lctx.isEmpty
   (← getSourceLCtx).foldlM (λ lctx srcLocalDecl => do
-    let localDecl ← Meta.withLCtx lctx #[] do
+    let localDecl ← Meta.withLCtx' lctx do
       translateLocalDecl srcLocalDecl
     pure $ lctx.addDecl localDecl
   ) lctx
@@ -149,6 +149,7 @@ def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab
     let type := termInfo.expectedType?.get!
     let lctx' ← translateLCtx
     let mvar ← Meta.withLCtx lctx' #[] do
+      Meta.withLocalInstances (lctx'.decls.toList.filterMap id) do
       let type' ← translateExpr type
       trace[Pantograph.Frontend.MetaTranslate] "Translating from term info {← Meta.ppExpr type'}"
       Meta.mkFreshExprSyntheticOpaqueMVar type'

Test/Frontend.lean

@@ -182,6 +182,25 @@ example : ∀ (y: Nat), ∃ (x: Nat), y + 1 = x := by
     }
   ])
 
+def test_sorry_with_local_instance : TestT MetaM Unit := do
+  let sketch := "
+def test (α : Type) [s : Inhabited α] : α := @Inhabited.default α s
+example (α : Type) [Inhabited α] : α := sorry
+  "
+  let goalStates ← (collectSorrysFromSource sketch).run' {}
+  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
+  let result ← runTermElabMInMeta $ goalState.tryTactic .unfocus "exact test α"
+  checkTrue "success" $ result matches .success ..
+  match result with
+  | .success .. => return ()
+  | .failure messages =>
+    let messages ← messages.mapM (·.toString)
+    fail s!"Could not execute tactic {messages}"
+  | .parseError e =>
+    fail s!"Parse error: {e}"
+  | .invalidAction e =>
+    fail s!"Invalid action: {e}"
+
 def test_environment_capture: TestT MetaM Unit := do
   let sketch := "
 def mystery (n: Nat) := n + 1
@@ -257,9 +276,10 @@ def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
     ("open", test_open),
     ("multiple_sorrys_in_proof", test_multiple_sorrys_in_proof),
-    ("sorry_in_middle", test_sorry_in_middle),
+    ("sorry in middle", test_sorry_in_middle),
-    ("sorry_in_induction", test_sorry_in_induction),
+    ("sorry in induction", test_sorry_in_induction),
-    ("sorry_in_coupled", test_sorry_in_coupled),
+    ("sorry in coupled", test_sorry_in_coupled),
+    ("sorry with local instances", test_sorry_with_local_instance),
     ("environment_capture", test_environment_capture),
     ("capture_type_mismatch", test_capture_type_mismatch),
     --("capture_type_mismatch_in_binder", test_capture_type_mismatch_in_binder),

Test/Main.lean

@@ -1,4 +1,3 @@
-import LSpec
 import Test.Delate
 import Test.Environment
 import Test.Frontend
@@ -9,6 +8,8 @@ import Test.Proofs
 import Test.Serial
 import Test.Tactic
 
+import LSpec
+
 -- Test running infrastructure
 
 namespace Pantograph.Test