From 03ecb6cf19b7741a6bb20f2eb969374ac59b8643 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 11 May 2024 20:01:02 -0700 Subject: [PATCH] feat: Partial instantiate metavariables --- Pantograph/Library.lean | 4 ++-- Pantograph/Serial.lean | 32 ++++++++++++++++++------- Test/Integration.lean | 4 ++-- Test/Proofs.lean | 2 +- Test/Serial.lean | 1 + Test/Tactic/MotivatedApply.lean | 42 +++++++++++++++++++++++++++++++-- 6 files changed, 70 insertions(+), 15 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 3ae852f..59d7adc 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -176,9 +176,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto state.restoreMetaM return { root? := ← state.rootExpr?.mapM (λ expr => do - serializeExpression options (← unfoldAuxLemmas expr)), + serializeExpression options (← instantiateAll expr)), parent? := ← state.parentExpr?.mapM (λ expr => do - serializeExpression options (← unfoldAuxLemmas expr)), + serializeExpression options (← instantiateAll expr)), } @[export pantograph_goal_diag_m] def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String := diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index b2a4529..cdb35ce 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -18,6 +18,23 @@ namespace Pantograph def unfoldAuxLemmas (e : Expr) : CoreM Expr := do Lean.Meta.deltaExpand e Lean.Name.isAuxLemma +def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do + Meta.transform e + (pre := fun e => e.withApp fun f args => do + if let .mvar mvarId := f then + if let some decl ← getDelayedMVarAssignment? mvarId then + if args.size ≥ decl.fvars.size then + let pending ← instantiateMVars (.mvar decl.mvarIdPending) + if !pending.isMVar then + return .visit <| (← Meta.mkLambdaFVars decl.fvars pending).beta args + return .continue) + +def instantiateAll (e: Expr): MetaM Expr := do + let e ← instantiateMVars e + let e ← unfoldAuxLemmas e + let e ← instantiatePartialDelayedMVars e + return e + --- Input Functions --- /-- Read syntax object from string -/ @@ -103,11 +120,9 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM let name := ofName fvarId.name pure s!"(:fv {name})" | .mvar mvarId => do - if ← mvarId.isDelayedAssigned then - pure s!"(:mv)" - else + let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv" let name := ofName mvarId.name - pure s!"(:mv {name})" + pure s!"(:{pref} {name})" | .sort level => let level := serializeSortLevel level sanitize pure s!"(:sort {level})" @@ -210,7 +225,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava match localDecl with | .cdecl _ fvarId userName type _ _ => let userName := userName.simpMacroScopes - let type ← instantiateMVars type + let type ← instantiate type return { name := ofName fvarId.name, userName:= ofName userName, @@ -219,9 +234,9 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava } | .ldecl _ fvarId userName type val _ _ => do let userName := userName.simpMacroScopes - let type ← instantiateMVars type + let type ← instantiate type let value? ← if showLetValues then - let val ← instantiateMVars val + let val ← instantiate val pure $ .some (← serializeExpression options val) else pure $ .none @@ -248,10 +263,11 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava name := ofName goal.name, userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName), isConversion := isLHSGoal? mvarDecl.type |>.isSome, - target := (← serializeExpression options (← instantiateMVars mvarDecl.type)), + target := (← serializeExpression options (← instantiateAll mvarDecl.type)), vars := vars.reverse.toArray } where + instantiate := instantiateAll ofName (n: Name) := serializeName n (sanitize := false) protected def GoalState.serializeGoals diff --git a/Test/Integration.lean b/Test/Integration.lean index 9bd5db6..66b3637 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -88,11 +88,11 @@ def test_tactic : IO LSpec.TestSeq := vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}], } let goal2: Protocol.Goal := { - name := "_uniq.14", + name := "_uniq.17", target := { pp? := .some "x ∨ y → y ∨ x" }, vars := #[ { name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}, - { name := "_uniq.13", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }} + { name := "_uniq.16", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }} ], } subroutine_runner [ diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 04fe79c..496bcc8 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -245,7 +245,7 @@ def test_or_comm: TestM Unit := do let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false) -- This is due to delayed assignment addTest $ LSpec.test "(2 parent)" (state2parent == - "((:mv) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))") + "((:mvd _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))") let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state diff --git a/Test/Serial.lean b/Test/Serial.lean index f55c18f..093dd8b 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -52,6 +52,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do ("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"), -- This tests `autoBoundImplicit` ("λ {α : Sort (u + 1)} => List α", "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"), + ("(2: Nat) <= (5: Nat)", "((:c LE.le) (:mv _uniq.37) (:mv _uniq.38) ((:c OfNat.ofNat) (:mv _uniq.23) (:lit 2) (:mv _uniq.24)) ((:c OfNat.ofNat) (:mv _uniq.33) (:lit 5) (:mv _uniq.34)))"), ] let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do let env ← MonadEnv.getEnv diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean index 84ca804..ad8ebdc 100644 --- a/Test/Tactic/MotivatedApply.lean +++ b/Test/Tactic/MotivatedApply.lean @@ -93,12 +93,50 @@ def test_list_brec_on (env: Environment): IO LSpec.TestSeq := tests := tests ++ test return tests +def test_partial_motive_instantiation (env: Environment): IO LSpec.TestSeq := do + let expr := "λ (n t: Nat) => n + 0 = n" + runMetaMSeq env $ runTermElabMInMeta do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := "@Nat.brecOn") + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + let (expr, exprType) ← valueAndType expr + Meta.lambdaTelescope expr $ λ _ body => do + let mut tests := LSpec.TestSeq.done + -- Apply the tactic + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let tactic := Tactic.motivatedApply recursor + let newGoals ← runTacticOnMVar tactic target.mvarId! + tests := tests ++ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = + [ + "Nat → Prop", + "Nat", + "∀ (t : Nat), Nat.below t → ?motive t", + "?motive ?m.69 = (n + 0 = n)", + ])) + let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number" + tests := tests ++ (LSpec.check "goal name" (major.name.toString = "_uniq.69")) + + -- Assign motive to `λ x => x + _` + let (motive_assign, _) ← valueAndType "λ (x: Nat) => @Nat.add x + 0 = _" + motive.assign motive_assign + + let test ← conduit.withContext do + let t := toString (← Meta.ppExpr $ ← conduit.getType) + return LSpec.check "conduit" (t = "(?m.69.add + 0 = ?m.140 ?m.69) = (n + 0 = n)") + tests := tests ++ test + + return tests def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ ("type_extract", test_type_extract env), - ("nat_brec_on", test_nat_brec_on env), - ("list_brec_on", test_list_brec_on env), + ("Nat.brecOn", test_nat_brec_on env), + ("List.brecOn", test_list_brec_on env), + ("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation env), ] end Pantograph.Test.Tactic.MotivatedApply