diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index f1c2503..484ff51 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -177,6 +177,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): }, newMVars, parentMVar? := .some goal, + calcPrevRhs? := .none } catch exception => return .failure #[← exception.toMessageData.toString] @@ -249,6 +250,49 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St }, newMVars := nextGoals.toSSet, parentMVar? := .some goal, + calcPrevRhs? := .none + } + catch exception => + return .failure #[← exception.toMessageData.toString] +protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): + Elab.TermElabM TacticResult := do + state.restoreElabM + let goal ← match state.savedState.tactic.goals.get? goalId with + | .some goal => pure goal + | .none => return .indexError goalId + let type ← match Parser.runParserCategory + (env := state.env) + (catName := `term) + (input := type) + (fileName := filename) with + | .ok syn => pure syn + | .error error => return .parseError error + let binderName := binderName.toName + try + -- Implemented similarly to the intro tactic + let nextGoals: List MVarId ← goal.withContext do + let type ← Elab.Term.elabType (stx := type) + let lctx ← MonadLCtx.getLCtx + + -- The branch goal inherits the same context, but with a different type + let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type + + let upstreamType := .letE binderName type mvarBranch (← goal.getType) false + let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) + upstreamType (kind := MetavarKind.synthetic) (userName := (← goal.getTag)) + + goal.assign mvarUpstream + + pure [mvarBranch.mvarId!, mvarUpstream.mvarId!] + return .success { + root := state.root, + savedState := { + term := ← MonadBacktrack.saveState, + tactic := { goals := nextGoals } + }, + newMVars := nextGoals.toSSet, + parentMVar? := .some goal, + calcPrevRhs? := .none } catch exception => return .failure #[← exception.toMessageData.toString] @@ -280,6 +324,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat): newMVars := newMVarSet prevMCtx nextMCtx, parentMVar? := .some goal, convMVar? := .some (convRhs, goal), + calcPrevRhs? := .none } catch exception => return .failure #[← exception.toMessageData.toString] @@ -318,6 +363,7 @@ protected def GoalState.convExit (state: GoalState): newMVars := newMVarSet prevMCtx nextMCtx, parentMVar? := .some convGoal, convMVar? := .none + calcPrevRhs? := .none } catch exception => return .failure #[← exception.toMessageData.toString] diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 9be86e7..6b8e2e2 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -169,6 +169,9 @@ def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM Tacti @[export pantograph_goal_have_m] def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := runTermElabM <| state.tryHave goalId binderName type +@[export pantograph_goal_let_m] +def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := + runTermElabM <| state.tryLet goalId binderName type @[export pantograph_goal_conv_m] def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult := diff --git a/Test/Proofs.lean b/Test/Proofs.lean index a3201a2..e14ba4a 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -542,14 +542,89 @@ def test_calc: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome - - where interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) := let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"), ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free buildGoal free target userName? +def test_let (specialized: Bool): TestM Unit := do + let state? ← startProof (.expr "∀ (a: Nat) (p: Prop), p → p ∨ ¬p") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + let tactic := "intro a p h" + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = + #[interiorGoal [] "p ∨ ¬p"]) + + + let letType := "Nat" + let expr := s!"let b: {letType} := _; _" + let result2 ← match specialized with + | true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType) + | false => state1.tryAssign (goalId := 0) (expr := expr) + let state2 ← match result2 with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + let serializedState2 ← state2.serializeGoals (options := ← read) + addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) = + #[ + interiorGoal [] letType, + interiorGoal [] "let b := ?m.20;\np ∨ ¬p" + ]) + -- Check that the goal mvar ids match up + addTest $ LSpec.check expr ((serializedState2.map (·.name) |>.get! 0) = "_uniq.20") + + let tactic := "exact a" + let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) = #[]) + + let state3r ← match state3.continue state2 with + | .error msg => do + addTest $ assertUnreachable $ msg + return () + | .ok state => pure state + addTest $ LSpec.check "(continue)" ((← state3r.serializeGoals (options := ← read)).map (·.devolatilize) = + #[interiorGoal [] "let b := a;\np ∨ ¬p"]) + + let tactic := "exact h" + match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with + | .failure #[message] => + addTest $ LSpec.check tactic (message = "type mismatch\n h\nhas type\n p : Prop\nbut is expected to have type\n let b := a;\n p ∨ ¬p : Prop") + | other => do + addTest $ assertUnreachable $ other.toString + + let tactic := "intro b" + let state4 ← match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + let tactic := "exact Or.inl h" + let state5 ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.test "(5 root)" state5.rootExpr?.isSome + where + interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) := + let free := [("a", "Nat"), ("p", "Prop"), ("h", "p")] ++ free + buildGoal free target userName? + def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ ("Nat.add_comm", test_nat_add_comm false), @@ -560,6 +635,8 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("have", test_have), ("conv", test_conv), ("calc", test_calc), + ("let via assign", test_let false), + ("let via tryLet", test_let true), ] tests.map (fun (name, test) => (name, proofRunner env test))