From dc2cc5be773d3cf95fe67cd30f9843c7fc3854a2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 4 Nov 2023 15:00:51 -0700 Subject: [PATCH 01/12] test: Separate mvar coupling tests --- Pantograph/Goal.lean | 9 ++- Test/Common.lean | 15 +++++ Test/Holes.lean | 129 ++++++++++++++++++++++++++++++------------- Test/Main.lean | 4 +- Test/Proofs.lean | 95 +------------------------------ 5 files changed, 116 insertions(+), 136 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 78a4194..eeb5a10 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -170,15 +170,18 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic /-- After finishing one branch of a proof (`graftee`), pick up from the point where the proof was left off (`target`) -/ -protected def GoalState.continue (target: GoalState) (graftee: GoalState): Except String GoalState := +protected def GoalState.continue (target: GoalState) (graftee: GoalState) (goals: Option (List MVarId) := .none): Except String GoalState := + let goals := match goals with + | .some goals => goals + | .none => target.goals if target.root != graftee.root then .error s!"Roots of two continued goal states do not match: {target.root.name} != {graftee.root.name}" -- Ensure goals are not dangling - else if ¬ (target.goals.all (λ goal => graftee.mvars.contains goal)) then + else if ¬ (goals.all (λ goal => graftee.mvars.contains goal)) then .error s!"Some goals in target are not present in the graftee" else -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic. - let unassigned := target.goals.filter (λ goal => + let unassigned := goals.filter (λ goal => let mctx := graftee.mctx ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal)) .ok { diff --git a/Test/Common.lean b/Test/Common.lean index f74e6a2..5b74a0f 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -1,4 +1,6 @@ import Pantograph.Protocol +import Pantograph.Goal +import LSpec namespace Pantograph @@ -15,6 +17,19 @@ def Goal.devolatilize (goal: Goal): Goal := v with name := "" } +deriving instance DecidableEq, Repr for Expression +deriving instance DecidableEq, Repr for Variable +deriving instance DecidableEq, Repr for Goal end Protocol +def TacticResult.toString : TacticResult → String + | .success state => s!".success ({state.goals.length} goals)" + | .failure messages => + let messages := "\n".intercalate messages.toList + s!".failure {messages}" + | .parseError error => s!".parseError {error}" + | .indexError index => s!".indexError {index}" + +def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false + end Pantograph diff --git a/Test/Holes.lean b/Test/Holes.lean index 64f2e2c..9b38087 100644 --- a/Test/Holes.lean +++ b/Test/Holes.lean @@ -1,31 +1,28 @@ import LSpec import Pantograph.Goal import Pantograph.Serial +import Test.Common namespace Pantograph.Test.Holes open Pantograph open Lean -abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Commands.Options M) +abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M) -deriving instance DecidableEq, Repr for Commands.Expression -deriving instance DecidableEq, Repr for Commands.Variable -deriving instance DecidableEq, Repr for Commands.Goal - -def add_test (test: LSpec.TestSeq): TestM Unit := do +def addTest (test: LSpec.TestSeq): TestM Unit := do set $ (← get) ++ test -def start_goal (hole: String): TestM (Option GoalState) := do +def startProof (expr: String): TestM (Option GoalState) := do let env ← Lean.MonadEnv.getEnv - let syn? := syntax_from_str env hole - add_test $ LSpec.check s!"Parsing {hole}" (syn?.isOk) + let syn? := syntax_from_str env expr + addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk) match syn? with | .error error => IO.println error return Option.none | .ok syn => - let expr? ← syntax_to_expr syn - add_test $ LSpec.check s!"Elaborating" expr?.isOk + let expr? ← syntax_to_expr_type syn + addTest $ LSpec.check s!"Elaborating" expr?.isOk match expr? with | .error error => IO.println error @@ -34,40 +31,21 @@ def start_goal (hole: String): TestM (Option GoalState) := do let goal ← GoalState.create (expr := expr) return Option.some goal -def assert_unreachable (message: String): LSpec.TestSeq := LSpec.check message false - -def build_goal (nameType: List (String × String)) (target: String): Commands.Goal := +def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal := { + userName?, target := { pp? := .some target}, vars := (nameType.map fun x => ({ - name := x.fst, + userName := x.fst, type? := .some { pp? := .some x.snd }, isInaccessible? := .some false })).toArray } --- Like `build_goal` but allow certain variables to be elided. -def build_goal_selective (nameType: List (String × Option String)) (target: String): Commands.Goal := - { - target := { pp? := .some target}, - vars := (nameType.map fun x => ({ - name := x.fst, - type? := x.snd.map (λ type => { pp? := type }), - isInaccessible? := x.snd.map (λ _ => false) - })).toArray - } - -def construct_sigma: TestM Unit := do - let goal? ← start_goal "∀ (n m: Nat), n + m = m + n" - add_test $ LSpec.check "Start goal" goal?.isSome - if let .some goal := goal? then - return () - - -def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do +def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options let coreContext: Lean.Core.Context := { - currNamespace := str_to_name "Aniva", + currNamespace := Name.append .anonymous "Aniva", openDecls := [], -- No 'open' directives needed fileName := "", fileMap := { source := "", positions := #[0], lines := #[1] } @@ -83,17 +61,94 @@ def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq : | .ok (_, a) => return a +/-- M-coupled goals -/ +def test_m_couple: TestM Unit := do + let state? ← startProof "(2: Nat) ≤ 5" + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) = + #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) + addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone + -- Set m to 3 + let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone + let state1b ← match state1.continue state2 with + | .error msg => do + addTest $ assertUnreachable $ msg + return () + | .ok state => pure state + addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = + #[.some "2 ≤ 3", .some "3 ≤ 5"]) + addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone + return () + +def test_proposition_generation: TestM Unit := do + let state? ← startProof "Σ' p:Prop, p" + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply PSigma.mk") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = + #[ + buildGoal [] "?fst" (userName? := .some "snd"), + buildGoal [] "Prop" (userName? := .some "fst") + ]) + if let #[goal1, goal2] := ← state1.serializeGoals (options := { (← read) with printExprAST := true }) then + addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})") + addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone + + let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) = + #[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"]) + addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone + + let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) = + #[]) + addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome + return () + + def suite: IO LSpec.TestSeq := do let env: Lean.Environment ← Lean.importModules (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false })) (opts := {}) (trustLevel := 1) let tests := [ - ("Σ'", construct_sigma) + ("2 < 5", test_m_couple), + ("Proposition Generation", test_proposition_generation) ] let tests ← tests.foldlM (fun acc tests => do let (name, tests) := tests - let tests ← proof_runner env tests + let tests ← proofRunner env tests return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done return LSpec.group "Holes" tests diff --git a/Test/Main.lean b/Test/Main.lean index 5b9a24a..cb7c055 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -1,5 +1,5 @@ import LSpec ---import Test.Holes +import Test.Holes import Test.Integration import Test.Proofs import Test.Serial @@ -11,7 +11,7 @@ unsafe def main := do Lean.initSearchPath (← Lean.findSysroot) let suites := [ - --Holes.suite, + Holes.suite, Integration.suite, Proofs.suite, Serial.suite diff --git a/Test/Proofs.lean b/Test/Proofs.lean index c08ecb2..8ec01a7 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -6,17 +6,6 @@ import Pantograph.Goal import Pantograph.Serial import Test.Common -namespace Pantograph - -def TacticResult.toString : TacticResult → String - | .success state => s!".success ({state.goals.length} goals)" - | .failure messages => - let messages := "\n".intercalate messages.toList - s!".failure {messages}" - | .parseError error => s!".parseError {error}" - | .indexError index => s!".indexError {index}" -end Pantograph - namespace Pantograph.Test.Proofs open Pantograph open Lean @@ -27,10 +16,6 @@ inductive Start where abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M) -deriving instance DecidableEq, Repr for Protocol.Expression -deriving instance DecidableEq, Repr for Protocol.Variable -deriving instance DecidableEq, Repr for Protocol.Goal - def addTest (test: LSpec.TestSeq): TestM Unit := do set $ (← get) ++ test @@ -64,8 +49,6 @@ def startProof (start: Start): TestM (Option GoalState) := do let goal ← GoalState.create (expr := expr) return Option.some goal -def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false - def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal := { userName?, @@ -303,80 +286,6 @@ def proof_or_comm: TestM Unit := do ] } -/-- M-coupled goals -/ -def proof_m_couple: TestM Unit := do - let state? ← startProof (.expr "(2: Nat) ≤ 5") - let state0 ← match state? with - | .some state => pure state - | .none => do - addTest $ assertUnreachable "Goal could not parse" - return () - - let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) = - #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) - addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone - -- Set m to 3 - let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone - let state1b ← match state1.continue state2 with - | .error msg => do - addTest $ assertUnreachable $ msg - return () - | .ok state => pure state - addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = - #[.some "2 ≤ 3", .some "3 ≤ 5"]) - addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone - return () - -def proof_proposition_generation: TestM Unit := do - let state? ← startProof (.expr "Σ' p:Prop, p") - let state0 ← match state? with - | .some state => pure state - | .none => do - addTest $ assertUnreachable "Goal could not parse" - return () - - let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply PSigma.mk") with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = - #[ - buildGoal [] "?fst" (userName? := .some "snd"), - buildGoal [] "Prop" (userName? := .some "fst") - ]) - if let #[goal1, goal2] := ← state1.serializeGoals (options := { (← read) with printExprAST := true }) then - addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})") - addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone - - let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) = - #[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"]) - addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone - - let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) = - #[]) - addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome - return () def suite: IO LSpec.TestSeq := do let env: Lean.Environment ← Lean.importModules @@ -388,9 +297,7 @@ def suite: IO LSpec.TestSeq := do ("Nat.add_comm manual", proof_nat_add_comm true), ("Nat.add_comm delta", proof_delta_variable), ("arithmetic", proof_arith), - ("Or.comm", proof_or_comm), - ("2 < 5", proof_m_couple), - ("Proposition Generation", proof_proposition_generation) + ("Or.comm", proof_or_comm) ] let tests ← tests.foldlM (fun acc tests => do let (name, tests) := tests From 754fb69cffa23f97cd917bf9a59d88bb72c71b3a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 4 Nov 2023 15:33:53 -0700 Subject: [PATCH 02/12] feat: Partial state continuation --- Pantograph/Goal.lean | 32 ++++++++++++++++-------------- Test/Holes.lean | 46 ++++++++++++++++++++++++++++++++++++++++++-- Test/Proofs.lean | 2 +- 3 files changed, 63 insertions(+), 17 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index eeb5a10..fd24232 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -169,30 +169,34 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String return .failure #[← exception.toMessageData.toString] tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic -/-- After finishing one branch of a proof (`graftee`), pick up from the point where the proof was left off (`target`) -/ -protected def GoalState.continue (target: GoalState) (graftee: GoalState) (goals: Option (List MVarId) := .none): Except String GoalState := - let goals := match goals with - | .some goals => goals - | .none => target.goals - if target.root != graftee.root then - .error s!"Roots of two continued goal states do not match: {target.root.name} != {graftee.root.name}" - -- Ensure goals are not dangling - else if ¬ (goals.all (λ goal => graftee.mvars.contains goal)) then - .error s!"Some goals in target are not present in the graftee" +/-- +Brings into scope a list of goals +-/ +protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := + if ¬ (goals.all (λ goal => state.mvars.contains goal)) then + .error s!"Goals not in scope" else -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic. let unassigned := goals.filter (λ goal => - let mctx := graftee.mctx + let mctx := state.mctx ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal)) .ok { + state with savedState := { - term := graftee.savedState.term, + term := state.savedState.term, tactic := { goals := unassigned }, }, - root := target.root, - newMVars := graftee.newMVars, } +/-- +Brings into scope all goals from `branch` +-/ +protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState := + if target.root != branch.root then + .error s!"Roots of two continued goal states do not match: {target.root.name} != {branch.root.name}" + else + target.resume (goals := branch.goals) + protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := let expr := goalState.mctx.eAssignment.find! goalState.root let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) diff --git a/Test/Holes.lean b/Test/Holes.lean index 9b38087..8692c2a 100644 --- a/Test/Holes.lean +++ b/Test/Holes.lean @@ -85,7 +85,7 @@ def test_m_couple: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone - let state1b ← match state1.continue state2 with + let state1b ← match state2.continue state1 with | .error msg => do addTest $ assertUnreachable $ msg return () @@ -136,6 +136,47 @@ def test_proposition_generation: TestM Unit := do addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome return () +def test_partial_continuation: TestM Unit := do + let state? ← startProof "(2: Nat) ≤ 5" + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) = + #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) + + let state2 ← match ← state1.execute (goalId := 2) (tactic := "apply Nat.succ") with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "apply Nat.succ" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) = + #[.some "Nat"]) + + -- Execute a partial continuation + let coupled_goals := state1.goals ++ state2.goals + let state1b ← match state2.resume (goals := coupled_goals) with + | .error msg => do + addTest $ assertUnreachable $ msg + return () + | .ok state => pure state + addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = + #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"]) + addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone + + -- Continuation should fail if the state does not exist: + match state0.resume coupled_goals with + | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals not in scope") + | .ok _ => addTest $ assertUnreachable "(continuation failure)" + return () + def suite: IO LSpec.TestSeq := do let env: Lean.Environment ← Lean.importModules @@ -144,7 +185,8 @@ def suite: IO LSpec.TestSeq := do (trustLevel := 1) let tests := [ ("2 < 5", test_m_couple), - ("Proposition Generation", test_proposition_generation) + ("Proposition Generation", test_proposition_generation), + ("Partial Continuation", test_partial_continuation) ] let tests ← tests.foldlM (fun acc tests => do let (name, tests) := tests diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 8ec01a7..0d5fb4e 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -253,7 +253,7 @@ def proof_or_comm: TestM Unit := do addTest $ LSpec.check " assumption" state4_2.goals.isEmpty addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone -- Ensure the proof can continue from `state4_2`. - let state2b ← match state2.continue state4_2 with + let state2b ← match state4_2.continue state2 with | .error msg => do addTest $ assertUnreachable $ msg return () From db706070ad56bdbdcadf8d119259868258b18e20 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 4 Nov 2023 15:51:09 -0700 Subject: [PATCH 03/12] feat: Add goal.continue command --- Pantograph.lean | 25 +++++++++++++++++++++++++ Pantograph/Protocol.lean | 15 +++++++++++++++ 2 files changed, 40 insertions(+) diff --git a/Pantograph.lean b/Pantograph.lean index 00782d5..0984db8 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -38,6 +38,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | "options.print" => run options_print | "goal.start" => run goal_start | "goal.tactic" => run goal_tactic + | "goal.continue" => run goal_continue | "goal.delete" => run goal_delete | "goal.print" => run goal_print | cmd => @@ -170,6 +171,30 @@ def execute (command: Protocol.Command): MainM Lean.Json := do return .error $ errorIndex s!"Invalid goal id index {goalId}" | .ok (.failure messages) => return .ok { tacticErrors? := .some messages } + goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do + let state ← get + match state.goalStates.get? args.target with + | .none => return .error $ errorIndex s!"Invalid state index {args.target}" + | .some target => do + let nextState? ← match args.branch?, args.goals? with + | .some branchId, .none => do + match state.goalStates.get? branchId with + | .none => return .error $ errorIndex s!"Invalid state index {branchId}" + | .some branch => pure $ target.continue branch + | .none, .some goals => + let goals := goals.map (λ name => { name := str_to_name name }) + pure $ target.resume goals + | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied" + match nextState? with + | .error error => return .ok { error? := .some error } + | .ok nextGoalState => + let (goalStates, nextStateId) := state.goalStates.insert nextGoalState + set { state with goalStates } + let goals ← nextGoalState.serializeGoals (parent := .some target) (options := state.options) + return .ok { + nextStateId? := .some nextStateId, + goals? := .some goals, + } goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do let state ← get let goalStates := args.stateIds.foldl (λ map id => map.remove id) state.goalStates diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index fd790bb..2469a6c 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -163,6 +163,21 @@ structure GoalTacticResult where -- Existence of this field shows the tactic parsing has failed parseError?: Option String := .none deriving Lean.ToJson +structure GoalContinue where + -- State from which the continuation acquires the context + target: Nat + + -- One of the following must be supplied + -- The state which is an ancestor of `target` where goals will be extracted from + branch?: Option Nat := .none + -- Or, the particular goals that should be brought back into scope + goals?: Option (List String) := .none + deriving Lean.FromJson +structure GoalContinueResult where + error?: Option String := .none + nextStateId?: Option Nat := .none + goals?: Option (Array Goal) := .none + deriving Lean.ToJson -- Remove goal states structure GoalDelete where From d809a960f99e339f0849c2c8a1fec76ceb3c3976 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 4 Nov 2023 15:53:57 -0700 Subject: [PATCH 04/12] feat: Goal continuation fails if target has goals --- Pantograph/Goal.lean | 4 +++- Test/Holes.lean | 5 +++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index fd24232..3645087 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -192,7 +192,9 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S Brings into scope all goals from `branch` -/ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState := - if target.root != branch.root then + if !target.goals.isEmpty then + .error s!"Target state has unresolved goals" + else if target.root != branch.root then .error s!"Roots of two continued goal states do not match: {target.root.name} != {branch.root.name}" else target.resume (goals := branch.goals) diff --git a/Test/Holes.lean b/Test/Holes.lean index 8692c2a..b6647ef 100644 --- a/Test/Holes.lean +++ b/Test/Holes.lean @@ -133,6 +133,7 @@ def test_proposition_generation: TestM Unit := do return () addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) = #[]) + addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome return () @@ -175,6 +176,10 @@ def test_partial_continuation: TestM Unit := do match state0.resume coupled_goals with | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals not in scope") | .ok _ => addTest $ assertUnreachable "(continuation failure)" + -- Continuation should fail if some goals have not been solved + match state2.continue state1 with + | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Target state has unresolved goals") + | .ok _ => addTest $ assertUnreachable "(continuation failure)" return () From 782ce38c872492f293838ea10912d1da940b66bb Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 4 Nov 2023 15:54:28 -0700 Subject: [PATCH 05/12] chore: Version bump to 0.2.8 --- Pantograph/Version.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index 29b3613..3fb09e9 100644 --- a/Pantograph/Version.lean +++ b/Pantograph/Version.lean @@ -1,5 +1,5 @@ namespace Pantograph -def version := "0.2.7" +def version := "0.2.8" end Pantograph From dbace9f2d57a4415c61eb9d4895a85bb9f7d54ae Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 6 Nov 2023 10:45:11 -0800 Subject: [PATCH 06/12] fix: Use Lean's built in name parser The `str_to_name` parser cannot handle numerical names and escapes. --- Main.lean | 4 ++-- Pantograph.lean | 6 +++--- Pantograph/Symbol.lean | 4 ---- Test/Holes.lean | 16 +++++++++++++++- Test/Proofs.lean | 2 +- Test/Serial.lean | 20 ++++++++------------ 6 files changed, 29 insertions(+), 23 deletions(-) diff --git a/Main.lean b/Main.lean index d7f936e..bed33bb 100644 --- a/Main.lean +++ b/Main.lean @@ -46,7 +46,7 @@ namespace Lean def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO Options := do let ps := (entry.splitOn "=").map String.trim let [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form ' = '" - let key := Pantograph.str_to_name key + let key := key.toName let defValue ← getOptionDefaultValue key match defValue with | DataValue.ofString _ => pure $ opts.setString key val @@ -88,7 +88,7 @@ unsafe def main (args: List String): IO Unit := do let imports:= args.filter (λ s => ¬ (s.startsWith "--")) let env ← Lean.importModules - (imports := imports.toArray.map (λ str => { module := str_to_name str, runtimeOnly := false })) + (imports := imports.toArray.map (λ str => { module := str.toName, runtimeOnly := false })) (opts := {}) (trustLevel := 1) let context: Context := { diff --git a/Pantograph.lean b/Pantograph.lean index 0984db8..fb4cc41 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -69,7 +69,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do lib_inspect (args: Protocol.LibInspect): MainM (CR Protocol.LibInspectResult) := do let state ← get let env ← Lean.MonadEnv.getEnv - let name := str_to_name args.name + let name := args.name.toName let info? := env.find? name match info? with | none => return .error $ errorIndex s!"Symbol not found {args.name}" @@ -132,7 +132,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .error str => return .error <| errorI "elab" str | .ok expr => return .ok expr)) | .none, .some copyFrom => - (match env.find? <| str_to_name copyFrom with + (match env.find? <| copyFrom.toName with | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" | .some cInfo => return .ok cInfo.type) | _, _ => @@ -182,7 +182,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .none => return .error $ errorIndex s!"Invalid state index {branchId}" | .some branch => pure $ target.continue branch | .none, .some goals => - let goals := goals.map (λ name => { name := str_to_name name }) + let goals := goals.map (λ name => { name := name.toName }) pure $ target.resume goals | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied" match nextState? with diff --git a/Pantograph/Symbol.lean b/Pantograph/Symbol.lean index 81d7deb..fb0ea1d 100644 --- a/Pantograph/Symbol.lean +++ b/Pantograph/Symbol.lean @@ -2,10 +2,6 @@ import Lean.Declaration namespace Pantograph -/-- Converts a symbol of the form `aa.bb.cc` to a name -/ -def str_to_name (s: String): Lean.Name := - (s.splitOn ".").foldl Lean.Name.str Lean.Name.anonymous - def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool := let nameDeduce: Bool := match n.getRoot with | .str _ name => name.startsWith "_" ∨ name == "Lean" diff --git a/Test/Holes.lean b/Test/Holes.lean index b6647ef..afad4e8 100644 --- a/Test/Holes.lean +++ b/Test/Holes.lean @@ -172,6 +172,20 @@ def test_partial_continuation: TestM Unit := do #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"]) addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone + -- Roundtrip + --let coupled_goals := coupled_goals.map (λ g => + -- { name := str_to_name $ name_to_ast g.name (sanitize := false)}) + let coupled_goals := coupled_goals.map (λ g => name_to_ast g.name (sanitize := false)) + let coupled_goals := coupled_goals.map (λ g => { name := g.toName }) + let state1b ← match state2.resume (goals := coupled_goals) with + | .error msg => do + addTest $ assertUnreachable $ msg + return () + | .ok state => pure state + addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = + #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"]) + addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone + -- Continuation should fail if the state does not exist: match state0.resume coupled_goals with | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals not in scope") @@ -185,7 +199,7 @@ def test_partial_continuation: TestM Unit := do def suite: IO LSpec.TestSeq := do let env: Lean.Environment ← Lean.importModules - (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false })) + (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false })) (opts := {}) (trustLevel := 1) let tests := [ diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 0d5fb4e..8992697 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -23,7 +23,7 @@ def startProof (start: Start): TestM (Option GoalState) := do let env ← Lean.MonadEnv.getEnv match start with | .copy name => - let cInfo? := str_to_name name |> env.find? + let cInfo? := name.toName |> env.find? addTest $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome match cInfo? with | .some cInfo => diff --git a/Test/Serial.lean b/Test/Serial.lean index dfa3890..c057bfb 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -9,9 +9,6 @@ open Lean deriving instance Repr, DecidableEq for Protocol.BoundExpression -def test_str_to_name: LSpec.TestSeq := - LSpec.test "Symbol parsing" (Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run") - def test_name_to_ast: LSpec.TestSeq := let quote := "\"" let escape := "\\" @@ -21,14 +18,14 @@ def test_name_to_ast: LSpec.TestSeq := LSpec.test s!"«̈{escape}{quote}»" (name_to_ast (Name.str .anonymous s!"{escape}{quote}") = s!"{quote}«{escape}{quote}»{quote}") def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do - let entries: List (String × Protocol.BoundExpression) := [ - ("Nat.add_comm", { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }), - ("Nat.le_of_succ_le", { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "Nat.succ n ≤ m")], target := "n ≤ m" }) + let entries: List (Name × Protocol.BoundExpression) := [ + ("Nat.add_comm".toName, { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }), + ("Nat.le_of_succ_le".toName, { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "Nat.succ n ≤ m")], target := "n ≤ m" }) ] - let coreM := entries.foldlM (λ suites (symbol, target) => do + let coreM: CoreM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do let env ← MonadEnv.getEnv - let expr := str_to_name symbol |> env.find? |>.get! |>.type - let test := LSpec.check symbol ((← type_expr_to_bound expr) = target) + let expr := env.find? symbol |>.get! |>.type + let test := LSpec.check symbol.toString ((← type_expr_to_bound expr) = target) return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run' let coreContext: Core.Context := { currNamespace := Lean.Name.str .anonymous "Aniva" @@ -54,7 +51,7 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do ] let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do let env ← MonadEnv.getEnv - let expr := str_to_name symbol |> env.find? |>.get! |>.type + let expr := env.find? symbol.toName |>.get! |>.type let test := LSpec.check symbol ((serialize_expression_ast expr) = target) return LSpec.TestSeq.append suites test) LSpec.TestSeq.done let coreM := metaM.run' @@ -72,12 +69,11 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do def suite: IO LSpec.TestSeq := do let env: Environment ← importModules - (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false })) + (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false })) (opts := {}) (trustLevel := 1) return LSpec.group "Serialization" $ - (LSpec.group "str_to_name" test_str_to_name) ++ (LSpec.group "name_to_ast" test_name_to_ast) ++ (LSpec.group "Expression binder" (← test_expr_to_binder env)) ++ (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env)) From a7aeb03b43cad5b4c30610c83ad510cca59f383f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 6 Nov 2023 11:04:28 -0800 Subject: [PATCH 07/12] chore: Update documentation --- README.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 0c19a3a..2b8425c 100644 --- a/README.md +++ b/README.md @@ -33,7 +33,7 @@ result of a command execution. The command can be passed in one of two formats command { ... } { "cmd": command, "payload": ... } ``` -The list of available commands can be found in `Pantograph/Commands.lean` and below. An +The list of available commands can be found in `Pantograph/Protocol.lean` and below. An empty command aborts the REPL. The `pantograph` executable must be run with a list of modules to import. It can @@ -54,18 +54,18 @@ Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_ ``` $ pantograph Init goal.start {"expr": "∀ (n m : Nat), n + m = m + n"} -goal.tactic {"goalId": 0, "tactic": "intro n m"} -goal.tactic {"goalId": 1, "tactic": "assumption"} -goal.delete {"goalIds": [0]} +goal.tactic {"stateId": 0, "goalId": 0, "tactic": "intro n m"} +goal.tactic {"stateId": 1, "goalId": 0, "tactic": "assumption"} +goal.delete {"stateIds": [0]} stat {} -goal.tactic {"goalId": 1, "tactic": "rw [Nat.add_comm]"} +goal.tactic {"stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"} stat ``` where the application of `assumption` should lead to a failure. ## Commands -See `Pantograph/Commands.lean` for a description of the parameters and return values in JSON. +See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. - `reset`: Delete all cached expressions and proof trees - `expr.echo {"expr": }`: Determine the type of an expression and round-trip it - `lib.catalog`: Display a list of all safe Lean symbols in the current context @@ -73,10 +73,11 @@ See `Pantograph/Commands.lean` for a description of the parameters and return va given symbol; If value flag is set, the value is printed or hidden. By default only the values of definitions are printed. - `options.set { key: value, ... }`: Set one or more options (not Lean options; those - have to be set via command line arguments.), for options, see `Pantograph/Commands.lean` + have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` - `options.print`: Display the current set of options - `goal.start {["name": ], ["expr": ], ["copyFrom": ]}`: Start a new goal from a given expression or symbol - `goal.tactic {"stateId": , "goalId": , ["tactic": ], ["expr": ]}`: Execute a tactic string on a given goal +- `goal.continue {"stateId": , ["branch": ], ["goals": ]}`: Continue from a proof state - `goal.remove {"stateIds": []}"`: Remove a bunch of stored goals. - `goal.print {"stateId": }"`: Print a goal state - `stat`: Display resource usage From 245e76b2f1b5f0938989850e9a979250133ef651 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 6 Nov 2023 11:51:31 -0800 Subject: [PATCH 08/12] feat: Print the root mvar name --- Pantograph.lean | 2 +- Pantograph/Protocol.lean | 2 ++ Test/Integration.lean | 2 +- 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index fb4cc41..6ec4ac1 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -143,7 +143,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let goalState ← GoalState.create expr let (goalStates, stateId) := state.goalStates.insert goalState set { state with goalStates } - return .ok { stateId } + return .ok { stateId, root := goalState.root.name.toString } goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do let state ← get match state.goalStates.get? args.stateId with diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 2469a6c..ce42d9d 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -142,6 +142,8 @@ structure GoalStart where deriving Lean.FromJson structure GoalStartResult where stateId: Nat := 0 + -- Name of the root metavariable + root: String deriving Lean.ToJson structure GoalTactic where -- Identifiers for tree, state, and goal diff --git a/Test/Integration.lean b/Test/Integration.lean index 0420a29..d8570b0 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -91,7 +91,7 @@ def test_tactic : IO LSpec.TestSeq := subroutine_runner [ subroutine_step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")] - (Lean.toJson ({stateId := 0}: + (Lean.toJson ({stateId := 0, root := "_uniq.8"}: Protocol.GoalStartResult)), subroutine_step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")] From 7076669c3de25ab637d3465c153ff32622d025a6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 6 Nov 2023 12:20:08 -0800 Subject: [PATCH 09/12] chore: Code formatting --- Pantograph.lean | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 6ec4ac1..a1f2602 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -29,17 +29,17 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .error ierror => return Lean.toJson ierror | .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}" match command.cmd with - | "reset" => run reset - | "stat" => run stat - | "expr.echo" => run expr_echo - | "lib.catalog" => run lib_catalog - | "lib.inspect" => run lib_inspect - | "options.set" => run options_set - | "options.print" => run options_print - | "goal.start" => run goal_start - | "goal.tactic" => run goal_tactic - | "goal.continue" => run goal_continue - | "goal.delete" => run goal_delete + | "reset" => run reset + | "stat" => run stat + | "expr.echo" => run expr_echo + | "lib.catalog" => run lib_catalog + | "lib.inspect" => run lib_inspect + | "options.set" => run options_set + | "options.print" => run options_print + | "goal.start" => run goal_start + | "goal.tactic" => run goal_tactic + | "goal.continue" => run goal_continue + | "goal.delete" => run goal_delete | "goal.print" => run goal_print | cmd => let error: Protocol.InteractionError := From 764be6d14b5e77771e8233e12c83b1c40125f861 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 7 Nov 2023 12:09:54 -0800 Subject: [PATCH 10/12] fix: Remove the error prone SemihashMap --- Pantograph.lean | 36 +++++---- Pantograph/SemihashMap.lean | 149 ------------------------------------ 2 files changed, 22 insertions(+), 163 deletions(-) delete mode 100644 Pantograph/SemihashMap.lean diff --git a/Pantograph.lean b/Pantograph.lean index a1f2602..0ae8192 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -1,8 +1,8 @@ import Pantograph.Goal import Pantograph.Protocol -import Pantograph.SemihashMap import Pantograph.Serial import Pantograph.Symbol +import Lean.Data.HashMap namespace Pantograph @@ -12,7 +12,8 @@ structure Context where /-- Stores state of the REPL -/ structure State where options: Protocol.Options := {} - goalStates: SemihashMap GoalState := SemihashMap.empty + nextId: Nat := 0 + goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty /-- Main state monad for executing commands -/ abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM) @@ -53,7 +54,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do let state ← get let nGoals := state.goalStates.size - set { state with goalStates := SemihashMap.empty } + set { state with goalStates := Lean.HashMap.empty } return .ok { nGoals } stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do let state ← get @@ -141,12 +142,15 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .error error => return .error error | .ok expr => let goalState ← GoalState.create expr - let (goalStates, stateId) := state.goalStates.insert goalState - set { state with goalStates } + let stateId := state.nextId + set { state with + goalStates := state.goalStates.insert stateId goalState, + nextId := state.nextId + 1 + } return .ok { stateId, root := goalState.root.name.toString } goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do let state ← get - match state.goalStates.get? args.stateId with + match state.goalStates.find? args.stateId with | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" | .some goalState => do let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with @@ -158,8 +162,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match nextGoalState? with | .error error => return .error error | .ok (.success nextGoalState) => - let (goalStates, nextStateId) := state.goalStates.insert nextGoalState - set { state with goalStates } + let nextStateId := state.nextId + let goalStates := state.goalStates.insert state.nextId goalState + set { state with goalStates, nextId := state.nextId + 1 } let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) return .ok { nextStateId? := .some nextStateId, @@ -173,12 +178,12 @@ def execute (command: Protocol.Command): MainM Lean.Json := do return .ok { tacticErrors? := .some messages } goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do let state ← get - match state.goalStates.get? args.target with + match state.goalStates.find? args.target with | .none => return .error $ errorIndex s!"Invalid state index {args.target}" | .some target => do let nextState? ← match args.branch?, args.goals? with | .some branchId, .none => do - match state.goalStates.get? branchId with + match state.goalStates.find? branchId with | .none => return .error $ errorIndex s!"Invalid state index {branchId}" | .some branch => pure $ target.continue branch | .none, .some goals => @@ -188,8 +193,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do match nextState? with | .error error => return .ok { error? := .some error } | .ok nextGoalState => - let (goalStates, nextStateId) := state.goalStates.insert nextGoalState - set { state with goalStates } + let nextStateId := state.nextId + set { state with + goalStates := state.goalStates.insert nextStateId nextGoalState, + nextId := state.nextId + 1 + } let goals ← nextGoalState.serializeGoals (parent := .some target) (options := state.options) return .ok { nextStateId? := .some nextStateId, @@ -197,12 +205,12 @@ def execute (command: Protocol.Command): MainM Lean.Json := do } goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do let state ← get - let goalStates := args.stateIds.foldl (λ map id => map.remove id) state.goalStates + let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates set { state with goalStates } return .ok {} goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do let state ← get - match state.goalStates.get? args.stateId with + match state.goalStates.find? args.stateId with | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" | .some goalState => do let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr) diff --git a/Pantograph/SemihashMap.lean b/Pantograph/SemihashMap.lean deleted file mode 100644 index 1d9ebae..0000000 --- a/Pantograph/SemihashMap.lean +++ /dev/null @@ -1,149 +0,0 @@ - -namespace Pantograph.SemihashMap - -structure Imp (β: Type u) where - data: Array (Option β) - - -- Number of elements currently in use - size: Nat - - -- Next index that has never been touched - allocFront: Nat - - -- Deallocated indices - deallocs: Array Nat - - -- Number of valid entries in `deallocs` array - lastDealloc: Nat - -namespace Imp - -structure WF (m: Imp β): Prop where - capacity: m.data.size = m.deallocs.size - front_dealloc: ∀ i: Fin m.deallocs.size, (i < m.allocFront) → (m.deallocs.get i) < m.allocFront - front_data: ∀ i: Fin m.data.size, (i ≥ m.allocFront) → (m.data.get i).isNone - -def empty (capacity := 16): Imp β := - { - data := mkArray capacity .none, - size := 0, - allocFront := 0, - deallocs := mkArray capacity 0, - lastDealloc := 0, - } - -private theorem list_get_replicate (x: α) (i: Fin (List.replicate n x).length): - List.get (List.replicate n x) i = x := by - sorry - -theorem empty_wf : WF (empty n: Imp β) := by - unfold empty - apply WF.mk - case capacity => - conv => - lhs - congr - simp - conv => - rhs - congr - simp - simp - case front_dealloc => - simp_all - intro i - intro a - contradiction - case front_data => - simp_all - intro i - unfold Imp.data at i - simp at i - conv => - lhs - unfold Array.get - unfold mkArray - simp [List.replicate] - rewrite [list_get_replicate] - --- FIXME: Merge this with the well-formed versions below so proof and code can --- mesh seamlessly. -@[inline] def insert (map: Imp β) (v: β): (Imp β × Nat) := - match map.lastDealloc with - | 0 => -- Capacity is full, buffer expansion is required - if map.size == map.data.size then - let nextIndex := map.data.size - let extendCapacity := map.size - let result: Imp β := { - data := (map.data.append #[Option.some v]).append (mkArray extendCapacity .none), - size := map.size + 1, - allocFront := map.size + 1, - deallocs := mkArray (map.data.size + 1 + extendCapacity) 0, - lastDealloc := 0, - } - (result, nextIndex) - else - let nextIndex := map.size - let result: Imp β := { - map - with - data := map.data.set ⟨nextIndex, sorry⟩ (Option.some v), - size := map.size + 1, - allocFront := map.allocFront + 1, - } - (result, nextIndex) - | (.succ k) => -- Allocation list has space - let nextIndex := map.deallocs.get! k - let result: Imp β := { - map with - data := map.data.set ⟨nextIndex, sorry⟩ (Option.some v), - size := map.size + 1, - lastDealloc := map.lastDealloc - 1 - } - (result, nextIndex) - -@[inline] def remove (map: Imp β) (index: Fin (map.size)): Imp β := - have h: index.val < map.data.size := by sorry - match map.data.get ⟨index.val, h⟩ with - | .none => map - | .some _ => - { - map with - data := map.data.set ⟨index, sorry⟩ .none, - size := map.size - 1, - deallocs := map.deallocs.set ⟨map.lastDealloc, sorry⟩ index, - lastDealloc := map.lastDealloc + 1, - } - -/-- Retrieval is efficient -/ -@[inline] def get? (map: Imp β) (index: Fin (map.size)): Option β := - have h: index.val < map.data.size := by sorry - map.data.get ⟨index.val, h⟩ -@[inline] def capacity (map: Imp β): Nat := map.data.size - -end Imp - - -/-- -This is like a hashmap but you cannot control the keys. --/ -def _root_.Pantograph.SemihashMap β := {m: Imp β // m.WF} - -@[inline] def empty (capacity := 16): SemihashMap β := - ⟨ Imp.empty capacity, Imp.empty_wf ⟩ -@[inline] def insert (map: SemihashMap β) (v: β): (SemihashMap β × Nat) := - let ⟨imp, pre⟩ := map - let ⟨result, id⟩ := imp.insert v - ( ⟨ result, sorry ⟩, id) -@[inline] def remove (map: SemihashMap β) (index: Nat): SemihashMap β := - let ⟨imp, pre⟩ := map - let result := imp.remove ⟨index, sorry⟩ - ⟨ result, sorry ⟩ -@[inline] def get? (map: SemihashMap β) (index: Nat): Option β := - let ⟨imp, _⟩ := map - imp.get? ⟨index, sorry⟩ -@[inline] def size (map: SemihashMap β): Nat := - let ⟨imp, _⟩ := map - imp.size - -end Pantograph.SemihashMap From 736e68639fed25fea192575f2661acf1e9e126f2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 7 Nov 2023 13:07:50 -0800 Subject: [PATCH 11/12] fix: New goal state not inserted correctly --- Pantograph.lean | 8 +++++--- Test/Integration.lean | 19 +++++++++++++++++-- 2 files changed, 22 insertions(+), 5 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 0ae8192..2532d75 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -54,7 +54,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do let state ← get let nGoals := state.goalStates.size - set { state with goalStates := Lean.HashMap.empty } + set { state with nextId := 0, goalStates := Lean.HashMap.empty } return .ok { nGoals } stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do let state ← get @@ -163,8 +163,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .error error => return .error error | .ok (.success nextGoalState) => let nextStateId := state.nextId - let goalStates := state.goalStates.insert state.nextId goalState - set { state with goalStates, nextId := state.nextId + 1 } + set { state with + goalStates := state.goalStates.insert state.nextId nextGoalState, + nextId := state.nextId + 1, + } let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) return .ok { nextStateId? := .some nextStateId, diff --git a/Test/Integration.lean b/Test/Integration.lean index d8570b0..65c2da6 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -83,11 +83,19 @@ def test_malformed_command : IO LSpec.TestSeq := Protocol.InteractionError)) ] def test_tactic : IO LSpec.TestSeq := - let goal: Protocol.Goal := { + let goal1: Protocol.Goal := { name := "_uniq.10", target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" }, vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}], } + let goal2: Protocol.Goal := { + name := "_uniq.13", + target := { pp? := .some "x ∨ y → y ∨ x" }, + vars := #[ + { name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}, + { name := "_uniq.12", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }} + ], + } subroutine_runner [ subroutine_step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")] @@ -97,7 +105,14 @@ def test_tactic : IO LSpec.TestSeq := [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")] (Lean.toJson ({ nextStateId? := .some 1, - goals? := #[goal], + goals? := #[goal1], + }: + Protocol.GoalTacticResult)), + subroutine_step "goal.tactic" + [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")] + (Lean.toJson ({ + nextStateId? := .some 2, + goals? := #[goal2], }: Protocol.GoalTacticResult)) ] From 8218d3f004726e4758612a4fa0951e89ac4c9a74 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 7 Nov 2023 13:10:14 -0800 Subject: [PATCH 12/12] fix: Do not show parent state in continue --- Pantograph.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph.lean b/Pantograph.lean index 2532d75..f9f8cc6 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -200,7 +200,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do goalStates := state.goalStates.insert nextStateId nextGoalState, nextId := state.nextId + 1 } - let goals ← nextGoalState.serializeGoals (parent := .some target) (options := state.options) + let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options) return .ok { nextStateId? := .some nextStateId, goals? := .some goals,