From 6ad24b72d474f015543e425f148fb7a3dc7b81da Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 16 May 2024 10:31:38 -0700 Subject: [PATCH] fix: Nested delayed assignment instantiation --- Pantograph/Expr.lean | 93 ++++++++++++++++++++++++++++++++++-------- Pantograph/Serial.lean | 4 +- Test/Proofs.lean | 37 ++++++++++++----- 3 files changed, 106 insertions(+), 28 deletions(-) diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean index 85c7f35..9f4b8d9 100644 --- a/Pantograph/Expr.lean +++ b/Pantograph/Expr.lean @@ -10,35 +10,94 @@ def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ def unfoldAuxLemmas (e : Expr) : CoreM Expr := do Lean.Meta.deltaExpand e Lean.Name.isAuxLemma -def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do - Meta.transform e +/-- +Force the instantiation of delayed metavariables even if they cannot be fully +instantiated. This is used during resumption. + +Since Lean 4 does not have an `Expr` constructor corresponding to delayed +metavariables, any delayed metavariables must be recursively handled by this +function to ensure that nested delayed metavariables can be properly processed. +The caveat is this recursive call will lead to infinite recursion if a loop +between metavariable assignment exists. + +This function ensures any metavariable in the result is either +1. Delayed assigned with its pending mvar not assigned in any form +2. Not assigned (delay or not) + -/ +partial def instantiateDelayedMVars (eOrig: Expr): MetaM Expr := do + --let padding := String.join $ List.replicate level " " + --IO.println s!"{padding}Starting {toString eOrig}" + let result ← Meta.transform (← instantiateMVars eOrig) (pre := fun e => e.withApp fun f args => do + --IO.println s!"{padding} V {toString e}" if let .mvar mvarId := f then if ← mvarId.isAssigned then - return .visit <| (← instantiateMVars e) - if let some decl ← getDelayedMVarAssignment? mvarId then - if args.size ≥ decl.fvars.size then - -- Do not use instantiateMVars here. Only one step of instantiation should happen. - let pending ← instantiateMVars (.mvar decl.mvarIdPending) - if !pending.isMVar then - let pending := pending.abstract decl.fvars - let pending := pending.instantiateRevRange 0 decl.fvars.size args - let pending := mkAppRange pending decl.fvars.size args.size args - return .visit <| pending - return .continue) + --IO.println s!"{padding} A ?{mvarId.name}" + return .continue <| .some (← self e) + if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then + -- No progress can be made on this + if !(← mvarIdPending.isAssigned) then + --IO.println s!"{padding} D/T1: {toString e}" + let args ← args.mapM self + let result := mkAppN f args + return .done result + --IO.println s!"{padding} D ?{mvarId.name} := [{fvars.size}] ?{mvarIdPending.name}" + -- This asstion fails when a tactic or elaboration function is + -- implemented incorrectly. See `instantiateExprMVars` + if args.size < fvars.size then + --IO.println s!"{padding} Illegal callsite: {args.size} < {fvars.size}" + throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}" + assert! !(← mvarIdPending.isDelayedAssigned) + let pending ← self (.mvar mvarIdPending) + if pending == .mvar mvarIdPending then + -- No progress could be made on this case + --IO.println s!"{padding}D/N {toString e}" + assert! !(← mvarIdPending.isAssigned) + assert! !(← mvarIdPending.isDelayedAssigned) + --else if pending.isMVar then + -- assert! !(← pending.mvarId!.isAssigned) + -- assert! !(← pending.mvarId!.isDelayedAssigned) + -- -- Progress made, but this is now another delayed assigned mvar + -- let nextMVarId ← mkFreshMVarId + -- assignDelayedMVar nextMVarId fvars pending.mvarId! + -- let args ← args.mapM self + -- let result := mkAppN (.mvar nextMVarId) args + -- return .done result + else + -- Progress has been made on this mvar + let pending := pending.abstract fvars + let args ← args.mapM self + -- Craete the function call structure + let subst := pending.instantiateRevRange 0 fvars.size args + let result := mkAppRange subst fvars.size args.size args + --IO.println s!"{padding}D/T2 {toString result}" + return .done result + return .continue) + --IO.println s!"{padding}Result {toString result}" + return result + where + self e := instantiateDelayedMVars e + +/-- +Convert an expression to an equiavlent form with +1. No nested delayed assigned mvars +2. No aux lemmas +3. No assigned mvars + -/ @[export pantograph_instantiate_all_meta_m] def instantiateAll (e: Expr): MetaM Expr := do - let e ← instantiateMVars e - let e ← instantiatePartialDelayedMVars e + let e ← instantiateDelayedMVars e let e ← unfoldAuxLemmas e return e structure DelayedMVarInvocation where mvarIdPending: MVarId args: Array (FVarId × (Option Expr)) + -- Extra arguments applied to the result of this substitution tail: Array Expr +-- The pending mvar of any delayed assigned mvar must not be assigned in any way. @[export pantograph_to_delayed_mvar_invocation_meta_m] def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do let .mvar mvarId := e.getAppFn | return .none @@ -48,7 +107,9 @@ def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := d -- Print the function application e. See Lean's `withOverApp` let args := e.getAppArgs - assert! args.size >= decl.fvars.size + assert! args.size ≥ decl.fvars.size + assert! !(← mvarIdPending.isAssigned) + assert! !(← mvarIdPending.isDelayedAssigned) let fvarArgMap: HashMap FVarId Expr := HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do let fvarId := localDecl.fvarId diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 3d46ee2..17dee2d 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -91,7 +91,7 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM where delayedMVarToSexp (e: Expr): MetaM (Option String) := do let .some invocation ← toDelayedMVarInvocation e | return .none - let callee ← self $ ← instantiateMVars $ .mvar invocation.mvarIdPending + let callee ← self $ .mvar invocation.mvarIdPending let sites ← invocation.args.mapM (λ (fvarId, arg) => do let arg := match arg with | .some arg => arg @@ -264,7 +264,7 @@ 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 (← instantiateAll mvarDecl.type)), + target := (← serializeExpression options (← instantiate mvarDecl.type)), vars := vars.reverse.toArray } where diff --git a/Test/Proofs.lean b/Test/Proofs.lean index ea6ff11..aa730ba 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -226,11 +226,25 @@ def test_or_comm: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = - #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"]) + let fvP := "_uniq.10" + let fvQ := "_uniq.13" + let fvH := "_uniq.16" + let state1g0 := "_uniq.17" + addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) = + #[{ + name := state1g0, + target := { pp? := .some "q ∨ p" }, + vars := #[ + { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false }, + { name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false }, + { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" }, isInaccessible? := .some false } + ] + }]) addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone + let state1parent ← serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false) + addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) (:fv {fvP}) (:fv {fvQ}) 0))))") let tactic := "cases h" let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with | .success state => pure state @@ -239,22 +253,25 @@ def test_or_comm: TestM Unit := do return () addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = #[branchGoal "inl" "p", branchGoal "inr" "q"]) + let (caseL, caseR) := ("_uniq.62", "_uniq.75") + addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) = + #[caseL, caseR]) addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone - let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false) - let substHead := "((:c Or.casesOn) (:fv _uniq.10) (:fv _uniq.13) (:lambda t._@._hyg.26 ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:forall h ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) 0) ((:c Or) (:fv _uniq.13) (:fv _uniq.10)))) (:fv _uniq.16) (:lambda h._@._hyg.27 (:fv _uniq.10) (:subst (:lambda h._@._hyg.28 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inl) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47))) (:subst (:subst (:mv _uniq.59) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47) (:fv _uniq.16) (:fv _uniq.50)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.47) 0)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) 0)) (:lambda h._@._hyg.29 (:fv _uniq.13) (:subst (:lambda h._@._hyg.30 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inr) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60))) (:subst (:subst (:mv _uniq.72) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60) (:fv _uniq.16) (:fv _uniq.63)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.60) 0)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) 0)))" - let extra := "((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16))" + let state2parent ← serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false) + let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))" + let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))" addTest $ LSpec.test "(2 parent)" (state2parent == - s!"((:subst {substHead} (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.16)) {extra})") + s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) (:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) {orPQ} (:fv {fvH}) 0) {orQP})) (:fv {fvH}) (:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:mv {caseL}))) (:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:mv {caseR}))) ((:c Eq.refl) {orPQ} (:fv {fvH})))") let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - let state3_1parent ← serializeExpressionSexp state3_1.parentExpr?.get! (sanitize := false) - addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.78))") + let state3_1parent ← serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) (sanitize := false) + addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.87))") addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with | .success state => pure state @@ -262,8 +279,8 @@ def test_or_comm: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check " assumption" state4_1.goals.isEmpty - let state4_1parent ← serializeExpressionSexp state4_1.parentExpr?.get! (sanitize := false) - addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.47)") + let state4_1parent ← instantiateAll state4_1.parentExpr?.get! + addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone let state3_2 ← match ← state2.tryTactic (goalId := 1) (tactic := "apply Or.inl") with | .success state => pure state