From 82d99ccf9bf37106fc76d0b131738cd56fce1f9f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 6 Sep 2024 21:07:12 -0700 Subject: [PATCH 1/8] refactor: Use `MVarId` across the board --- Pantograph.lean | 91 +++++++++++++++++++++------------------ Pantograph/Goal.lean | 75 ++++++++++++++------------------ Pantograph/Library.lean | 31 ++++++------- Pantograph/Protocol.lean | 3 ++ Test/Common.lean | 4 +- Test/Metavar.lean | 22 +++++----- Test/Proofs.lean | 90 +++++++++++++++++++------------------- Test/Tactic/Prograde.lean | 40 ++++++++--------- 8 files changed, 178 insertions(+), 178 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 35ab117..7cedab8 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -1,5 +1,6 @@ import Lean.Data.HashMap import Pantograph.Compile +import Pantograph.Condensed import Pantograph.Environment import Pantograph.Goal import Pantograph.Library @@ -23,6 +24,11 @@ abbrev MainM := ReaderT Context (StateT State Lean.CoreM) -- certain monadic features in `MainM` abbrev CR α := Except Protocol.InteractionError α +def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α := + metaM.run' +def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α := + termElabM.run' (ctx := Condensed.elabContext) |>.run' + def execute (command: Protocol.Command): MainM Lean.Json := do let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := match Lean.fromJson? command.payload with @@ -87,6 +93,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do noRepeat := args.noRepeat?.getD options.noRepeat, printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls, printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps + automaticMode := args.automaticMode?.getD options.automaticMode, } } return .ok { } @@ -95,7 +102,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do let state ← get let env ← Lean.MonadEnv.getEnv - let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with + let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with | .some expr, .none => goalStartExpr expr (args.levels.getD #[]) | .none, .some copyFrom => (match env.find? <| copyFrom.toName with @@ -114,47 +121,47 @@ def execute (command: Protocol.Command): MainM Lean.Json := do return .ok { stateId, root := goalState.root.name.toString } goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do let state ← get - 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?, args.have?, args.calc?, args.conv? with - | .some tactic, .none, .none, .none, .none => do - pure ( Except.ok (← goalTactic goalState args.goalId tactic)) - | .none, .some expr, .none, .none, .none => do - pure ( Except.ok (← goalAssign goalState args.goalId expr)) - | .none, .none, .some type, .none, .none => do - let binderName := args.binderName?.getD "" - pure ( Except.ok (← goalState.tryHave args.goalId binderName type)) - | .none, .none, .none, .some pred, .none => do - pure ( Except.ok (← goalCalc goalState args.goalId pred)) - | .none, .none, .none, .none, .some true => do - pure ( Except.ok (← goalConv goalState args.goalId)) - | .none, .none, .none, .none, .some false => do - pure ( Except.ok (← goalConvExit goalState)) - | _, _, _, _, _ => pure (Except.error <| - errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied") - match nextGoalState? with - | .error error => return .error error - | .ok (.success nextGoalState) => - let nextStateId := state.nextId - set { state with - goalStates := state.goalStates.insert state.nextId nextGoalState, - nextId := state.nextId + 1, - } - let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run' - return .ok { - nextStateId? := .some nextStateId, - goals? := .some goals, - } - | .ok (.parseError message) => - return .ok { parseError? := .some message } - | .ok (.indexError goalId) => - return .error $ errorIndex s!"Invalid goal id index {goalId}" - | .ok (.invalidAction message) => - return .error $ errorI "invalid" message - | .ok (.failure messages) => - return .ok { tacticErrors? := .some messages } + let .some goalState := state.goalStates.find? args.stateId | + return .error $ errorIndex s!"Invalid state index {args.stateId}" + let .some goal := goalState.goals.get? args.goalId | + return .error $ errorIndex s!"Invalid goal index {args.goalId}" + let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do + match args.tactic?, args.expr?, args.have?, args.calc?, args.conv? with + | .some tactic, .none, .none, .none, .none => do + pure <| Except.ok <| ← goalState.tryTactic goal tactic + | .none, .some expr, .none, .none, .none => do + pure <| Except.ok <| ← goalState.tryAssign goal expr + | .none, .none, .some type, .none, .none => do + let binderName := args.binderName?.getD "" + pure <| Except.ok <| ← goalState.tryHave goal binderName type + | .none, .none, .none, .some pred, .none => do + pure <| Except.ok <| ← goalState.tryCalc goal pred + | .none, .none, .none, .none, .some true => do + pure <| Except.ok <| ← goalState.conv goal + | .none, .none, .none, .none, .some false => do + pure <| Except.ok <| ← goalState.convExit + | _, _, _, _, _ => + let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied" + pure $ Except.error $ error + match nextGoalState? with + | .error error => return .error error + | .ok (.success nextGoalState) => + let nextStateId := state.nextId + set { state with + goalStates := state.goalStates.insert state.nextId nextGoalState, + nextId := state.nextId + 1, + } + let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run' + return .ok { + nextStateId? := .some nextStateId, + goals? := .some goals, + } + | .ok (.parseError message) => + return .ok { parseError? := .some message } + | .ok (.invalidAction message) => + return .error $ errorI "invalid" message + | .ok (.failure messages) => + return .ok { tacticErrors? := .some messages } goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do let state ← get match state.goalStates.find? args.target with diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index d92a807..0df3a4b 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -30,7 +30,7 @@ structure GoalState where convMVar?: Option (MVarId × MVarId) := .none -- Previous RHS for calc, so we don't have to repeat it every time -- WARNING: If using `state with` outside of `calc`, this must be set to `.none` - calcPrevRhs?: Option Expr := .none + calcPrevRhs?: Option (MVarId × Expr) := .none @[export pantograph_goal_state_create_m] protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do @@ -147,24 +147,24 @@ protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) return expr @[export pantograph_goal_state_get_mvar_e_assignment] -protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvar: MVarId): Option Expr := do - let expr ← goalState.mctx.eAssignment.find? mvar +protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarId): Option Expr := do + let expr ← goalState.mctx.eAssignment.find? mvarId let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) return expr --- Tactic execution functions --- -protected def GoalState.step (state: GoalState) (mvarId: MVarId) (tacticM: Elab.Tactic.TacticM Unit) +protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit) : Elab.TermElabM GoalState := do - unless (← getMCtx).decls.contains mvarId do - throwError s!"MVarId is not in context: {mvarId.name}" - mvarId.checkNotAssigned `GoalState.step - let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [mvarId] } + unless (← getMCtx).decls.contains goal do + throwError s!"Goal is not in context: {goal.name}" + goal.checkNotAssigned `GoalState.step + let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } let nextElabState ← MonadBacktrack.saveState return { state with savedState := { term := nextElabState, tactic := newGoals }, - parentMVar? := .some mvarId, + parentMVar? := .some goal, calcPrevRhs? := .none, } @@ -176,25 +176,20 @@ inductive TacticResult where | failure (messages: Array String) -- Could not parse tactic | parseError (message: String) - -- The goal index is out of bounds - | indexError (goalId: Nat) -- The given action cannot be executed in the state | invalidAction (message: String) /-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/ -protected def GoalState.tryTacticM (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit): +protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit): Elab.TermElabM TacticResult := do - let mvarId ← match state.savedState.tactic.goals.get? goalId with - | .some goal => pure $ goal - | .none => return .indexError goalId try - let nextState ← state.step mvarId tacticM + let nextState ← state.step goal tacticM return .success nextState catch exception => return .failure #[← exception.toMessageData.toString] -/-- Execute a string tactic on given state -/ -protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String): +/-- Execute a string tactic on given state. Restores TermElabM -/ +protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: String): Elab.TermElabM TacticResult := do state.restoreElabM let tactic ← match Parser.runParserCategory @@ -204,9 +199,9 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri (fileName := filename) with | .ok stx => pure $ stx | .error error => return .parseError error - state.tryTacticM goalId $ Elab.Tactic.evalTactic tactic + state.tryTacticM goal $ Elab.Tactic.evalTactic tactic -protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): +protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String): Elab.TermElabM TacticResult := do state.restoreElabM let expr ← match Parser.runParserCategory @@ -216,11 +211,11 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String (fileName := filename) with | .ok syn => pure syn | .error error => return .parseError error - state.tryTacticM goalId $ Tactic.evalAssign expr + state.tryTacticM goal $ Tactic.evalAssign expr -- Specialized Tactics -protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): +protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): Elab.TermElabM TacticResult := do state.restoreElabM let type ← match Parser.runParserCategory @@ -230,16 +225,13 @@ protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: Str (fileName := filename) with | .ok syn => pure syn | .error error => return .parseError error - state.tryTacticM goalId $ Tactic.evalLet binderName.toName type + state.tryTacticM goal $ Tactic.evalLet binderName.toName type /-- Enter conv tactic mode -/ -protected def GoalState.conv (state: GoalState) (goalId: Nat): +protected def GoalState.conv (state: GoalState) (goal: MVarId): Elab.TermElabM TacticResult := do if state.convMVar?.isSome then return .invalidAction "Already in conv state" - let goal ← match state.savedState.tactic.goals.get? goalId with - | .some goal => pure goal - | .none => return .indexError goalId goal.checkNotAssigned `GoalState.conv let tacticM : Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do state.restoreTacticM goal @@ -298,19 +290,17 @@ protected def GoalState.convExit (state: GoalState): catch exception => return .failure #[← exception.toMessageData.toString] -protected def GoalState.calcPrevRhsOf? (state: GoalState) (goalId: Nat) := - if goalId == 1 then - state.calcPrevRhs? +protected def GoalState.calcPrevRhsOf? (state: GoalState) (goal: MVarId): Option Expr := do + let (mvarId, rhs ) ← state.calcPrevRhs? + if mvarId == goal then + .some rhs else .none -protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): +protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String): Elab.TermElabM TacticResult := do state.restoreElabM if state.convMVar?.isSome then return .invalidAction "Cannot initiate `calc` while in `conv` state" - let goal ← match state.savedState.tactic.goals.get? goalId with - | .some goal => pure goal - | .none => return .indexError goalId let `(term|$pred) ← match Parser.runParserCategory (env := state.env) (catName := `term) @@ -319,9 +309,10 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): | .ok syn => pure syn | .error error => return .parseError error goal.checkNotAssigned `GoalState.tryCalc - let calcPrevRhs? := state.calcPrevRhsOf? goalId - let target ← instantiateMVars (← goal.getDecl).type - let tag := (← goal.getDecl).userName + let calcPrevRhs? := state.calcPrevRhsOf? goal + let decl ← goal.getDecl + let target ← instantiateMVars decl.type + let tag := decl.userName try goal.withContext do @@ -345,7 +336,7 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): (userName := tag ++ `calc) let mvarBranch := proof.mvarId! - let calcPrevRhs? := Option.some rhs + let calcPrevRhs? := Option.some (goal, rhs) let mut proofType ← Meta.inferType proof let mut remainder := Option.none @@ -377,19 +368,19 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): return .failure #[← exception.toMessageData.toString] -protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): +protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String): Elab.TermElabM TacticResult := do state.restoreElabM let recursor ← match (← Compile.parseTermM recursor) with | .ok syn => pure syn | .error error => return .parseError error - state.tryTacticM goalId (tacticM := Tactic.evalMotivatedApply recursor) -protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String): + state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor) +protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String): Elab.TermElabM TacticResult := do state.restoreElabM let eq ← match (← Compile.parseTermM eq) with | .ok syn => pure syn | .error error => return .parseError error - state.tryTacticM goalId (tacticM := Tactic.evalNoConfuse eq) + state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq) end Pantograph diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index c4ce4ff..2b2f223 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -156,41 +156,38 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.G } @[export pantograph_goal_tactic_m] -def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticResult := - runTermElabM <| state.tryTactic goalId tactic +def goalTactic (state: GoalState) (goal: MVarId) (tactic: String): CoreM TacticResult := + runTermElabM <| state.tryTactic goal tactic @[export pantograph_goal_assign_m] -def goalAssign (state: GoalState) (goalId: Nat) (expr: String): CoreM TacticResult := - runTermElabM <| state.tryAssign goalId expr +def goalAssign (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult := + runTermElabM <| state.tryAssign goal expr @[export pantograph_goal_have_m] -protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := do +protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := do let type ← match (← Compile.parseTermM type) with | .ok syn => pure syn | .error error => return .parseError error runTermElabM do state.restoreElabM - state.tryTacticM goalId $ Tactic.evalHave binderName.toName type + state.tryTacticM goal $ Tactic.evalHave binderName.toName type @[export pantograph_goal_try_define_m] -protected def GoalState.tryDefine (state: GoalState) (goalId: Nat) (binderName: String) (expr: String): CoreM TacticResult := do +protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): CoreM TacticResult := do let expr ← match (← Compile.parseTermM expr) with | .ok syn => pure syn | .error error => return .parseError error runTermElabM do state.restoreElabM - state.tryTacticM goalId (Tactic.evalDefine binderName.toName expr) + state.tryTacticM goal (Tactic.evalDefine binderName.toName expr) @[export pantograph_goal_let_m] -def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := - runTermElabM <| state.tryLet goalId binderName type +def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := + runTermElabM <| state.tryLet goal binderName type @[export pantograph_goal_conv_m] -def goalConv (state: GoalState) (goalId: Nat): CoreM TacticResult := - runTermElabM <| state.conv goalId +def goalConv (state: GoalState) (goal: MVarId): CoreM TacticResult := + runTermElabM <| state.conv goal @[export pantograph_goal_conv_exit_m] def goalConvExit (state: GoalState): CoreM TacticResult := runTermElabM <| state.convExit @[export pantograph_goal_calc_m] -def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult := - runTermElabM <| state.tryCalc goalId pred -@[export pantograph_goal_focus] -def goalFocus (state: GoalState) (goalId: Nat): Option GoalState := - state.focus goalId +def goalCalc (state: GoalState) (goal: MVarId) (pred: String): CoreM TacticResult := + runTermElabM <| state.tryCalc goal pred end Pantograph diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 1a52c8a..223fcfe 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -27,6 +27,8 @@ structure Options where printAuxDecls: Bool := false -- See `pp.implementationDetailHyps` printImplementationDetailHyps: Bool := false + -- If this is set to `true`, goals will never go dormant, so you don't have to manage resumption + automaticMode: Bool := false deriving Lean.ToJson abbrev OptionsT := ReaderT Options @@ -190,6 +192,7 @@ structure OptionsSet where noRepeat?: Option Bool printAuxDecls?: Option Bool printImplementationDetailHyps?: Option Bool + automaticMode?: Option Bool deriving Lean.FromJson structure OptionsSetResult where deriving Lean.ToJson diff --git a/Test/Common.lean b/Test/Common.lean index 83f2e7b..2d98aca 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -62,13 +62,15 @@ protected def Goal.devolatilize (goal: Goal): Goal := end Condensed +def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals.get! i +def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.goals.get! goalId) tactic + 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}" | .invalidAction error => s!".invalidAction {error}" namespace Test diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 2fcab28..dbaf2cc 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -83,7 +83,7 @@ def test_m_couple: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with + let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -92,7 +92,7 @@ def test_m_couple: TestM Unit := do #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone -- Set m to 3 - let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 3") with + let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 3") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -115,7 +115,7 @@ def test_m_couple_simp: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with + let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -126,7 +126,7 @@ def test_m_couple_simp: TestM Unit := do addTest $ LSpec.check "(metavariables)" (serializedState1.map (·.target.dependentMVars?.get!) = #[#["_uniq.38"], #["_uniq.38"], #[]]) - let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 2") with + let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 2") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -140,7 +140,7 @@ def test_m_couple_simp: TestM Unit := do addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = #[.some "2 ≤ 2", .some "2 ≤ 5"]) addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone - let state3 ← match ← state1b.tryTactic (goalId := 0) (tactic := "simp") with + let state3 ← match ← state1b.tacticOn (goalId := 0) (tactic := "simp") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -150,7 +150,7 @@ def test_m_couple_simp: TestM Unit := do addTest $ assertUnreachable $ msg return () | .ok state => pure state - let state5 ← match ← state4.tryTactic (goalId := 0) (tactic := "simp") with + let state5 ← match ← state4.tacticOn (goalId := 0) (tactic := "simp") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -177,7 +177,7 @@ def test_proposition_generation: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply PSigma.mk") with + let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply PSigma.mk") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -191,7 +191,7 @@ def test_proposition_generation: TestM Unit := do 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 + let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := "λ (x: Nat) => _") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -201,7 +201,7 @@ def test_proposition_generation: TestM Unit := do addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone let assign := "Eq.refl x" - let state3 ← match ← state2.tryAssign (goalId := 0) (expr := assign) with + let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := assign) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -220,7 +220,7 @@ def test_partial_continuation: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with + let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -228,7 +228,7 @@ def test_partial_continuation: TestM Unit := do 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.tryTactic (goalId := 2) (tactic := "apply Nat.succ") with + let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "apply Nat.succ") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString diff --git a/Test/Proofs.lean b/Test/Proofs.lean index ba97ad7..1da21ae 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -91,7 +91,7 @@ def test_identity: TestM Unit := do return () let tactic := "intro p h" - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + let state1 ← match ← state0.tacticOn 0 tactic with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -118,7 +118,7 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro n m") with + let state1 ← match ← state0.tacticOn 0 "intro n m" with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -126,13 +126,13 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = #[buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"]) - match ← state1.tryTactic (goalId := 0) (tactic := "assumption") with + match ← state1.tacticOn 0 "assumption" with | .failure #[message] => addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n") | other => do addTest $ assertUnreachable $ other.toString - let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "rw [Nat.add_comm]") with + let state2 ← match ← state1.tacticOn 0 "rw [Nat.add_comm]" with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -150,14 +150,14 @@ def test_delta_variable: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro n") with + let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "intro n") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) = #[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"]) - let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "intro m") with + let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "intro m") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -189,14 +189,14 @@ def test_arith: TestM Unit := do return () let tactic := "intros" - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check tactic (state1.goals.length = 1) addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone - let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with + let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -204,7 +204,7 @@ def test_arith: TestM Unit := do addTest $ LSpec.check "simp ..." (state2.goals.length = 1) addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone let tactic := "assumption" - let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with + let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -239,7 +239,7 @@ def test_or_comm: TestM Unit := do addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone let tactic := "intro p q h" - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -265,7 +265,7 @@ def test_or_comm: TestM Unit := do 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}) 2 1 0))))") let tactic := "cases h" - let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with + let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -289,7 +289,7 @@ def test_or_comm: TestM Unit := do addTest $ LSpec.test "(2 parent)" (state2parent == s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})") - let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with + let state3_1 ← match ← state2.tacticOn (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -298,7 +298,7 @@ def test_or_comm: TestM Unit := do 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.91))") addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) - let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with + let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -307,13 +307,13 @@ def test_or_comm: TestM Unit := do 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 + let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1) - let state4_2 ← match ← state3_2.tryTactic (goalId := 0) (tactic := "assumption") with + let state4_2 ← match ← state3_2.tacticOn (goalId := 0) (tactic := "assumption") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -327,13 +327,13 @@ def test_or_comm: TestM Unit := do return () | .ok state => pure state addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0]) - let state3_1 ← match ← state2b.tryTactic (goalId := 0) (tactic := "apply Or.inr") with + let state3_1 ← match ← state2b.tacticOn (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) - let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with + let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -372,7 +372,7 @@ def test_conv: TestM Unit := do return () let tactic := "intro a b c1 c2 h" - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -380,7 +380,7 @@ def test_conv: TestM Unit := do addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = #[interiorGoal [] "a + b + c1 = b + a + c2"]) - let state2 ← match ← state1.conv (goalId := 0) with + let state2 ← match ← state1.conv (state1.get! 0) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -389,7 +389,7 @@ def test_conv: TestM Unit := do #[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }]) let convTactic := "rhs" - let state3R ← match ← state2.tryTactic (goalId := 0) convTactic with + let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -398,7 +398,7 @@ def test_conv: TestM Unit := do #[{ interiorGoal [] "b + a + c2" with isConversion := true }]) let convTactic := "lhs" - let state3L ← match ← state2.tryTactic (goalId := 0) convTactic with + let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -407,7 +407,7 @@ def test_conv: TestM Unit := do #[{ interiorGoal [] "a + b + c1" with isConversion := true }]) let convTactic := "congr" - let state4 ← match ← state3L.tryTactic (goalId := 0) convTactic with + let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -419,7 +419,7 @@ def test_conv: TestM Unit := do ]) let convTactic := "rw [Nat.add_comm]" - let state5_1 ← match ← state4.tryTactic (goalId := 0) convTactic with + let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -428,7 +428,7 @@ def test_conv: TestM Unit := do #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }]) let convTactic := "rfl" - let state6_1 ← match ← state5_1.tryTactic (goalId := 0) convTactic with + let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -443,7 +443,7 @@ def test_conv: TestM Unit := do return () let convTactic := "rfl" - let state6 ← match ← state4_1.tryTactic (goalId := 0) convTactic with + let state6 ← match ← state4_1.tacticOn (goalId := 0) convTactic with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -458,7 +458,7 @@ def test_conv: TestM Unit := do return () let tactic := "exact h" - let stateF ← match ← state1_1.tryTactic (goalId := 0) (tactic := tactic) with + let stateF ← match ← state1_1.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -485,7 +485,7 @@ def test_calc: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () let tactic := "intro a b c d h1 h2" - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -493,7 +493,7 @@ def test_calc: TestM Unit := do addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = #[interiorGoal [] "a + b = c + d"]) let pred := "a + b = b + c" - let state2 ← match ← state1.tryCalc (goalId := 0) (pred := pred) with + let state2 ← match ← state1.tryCalc (state1.get! 0) (pred := pred) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -503,11 +503,11 @@ def test_calc: TestM Unit := do interiorGoal [] "a + b = b + c" (.some "calc"), interiorGoal [] "b + c = c + d" ]) - addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? 0 |>.isNone) - addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? 1 |>.isSome) + addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 0) |>.isNone) + addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 1) |>.isSome) let tactic := "apply h1" - let state2m ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with + let state2m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -518,7 +518,7 @@ def test_calc: TestM Unit := do addTest $ expectationFailure "continue" e return () let pred := "_ = c + d" - let state4 ← match ← state3.tryCalc (goalId := 0) (pred := pred) with + let state4 ← match ← state3.tryCalc (state3.get! 0) (pred := pred) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -527,9 +527,9 @@ def test_calc: TestM Unit := do #[ interiorGoal [] "b + c = c + d" (.some "calc") ]) - addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? 0 |>.isNone) + addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? (state4.get! 0) |>.isNone) let tactic := "apply h2" - let state4m ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with + let state4m ← match ← state4.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -549,7 +549,7 @@ def test_nat_zero_add: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () let tactic := "intro n" - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -557,7 +557,7 @@ def test_nat_zero_add: TestM Unit := do addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = #[buildGoal [("n", "Nat")] "n + 0 = n"]) let recursor := "@Nat.brecOn" - let state2 ← match ← state1.tryMotivatedApply (goalId := 0) (recursor := recursor) with + let state2 ← match ← state1.tryMotivatedApply (state1.get! 0) (recursor := recursor) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -571,7 +571,7 @@ def test_nat_zero_add: TestM Unit := do ]) let tactic := "exact n" - let state3b ← match ← state2.tryTactic (goalId := 1) (tactic := tactic) with + let state3b ← match ← state2.tacticOn (goalId := 1) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -584,7 +584,7 @@ def test_nat_zero_add: TestM Unit := do addTest $ assertUnreachable e return () let tactic := "exact (λ x => x + 0 = x)" - let state3c ← match ← state2b.tryTactic (goalId := 0) (tactic := tactic) with + let state3c ← match ← state2b.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -597,7 +597,7 @@ def test_nat_zero_add: TestM Unit := do addTest $ assertUnreachable e return () let tactic := "intro t h" - let state3 ← match ← state2c.tryTactic (goalId := 0) (tactic := tactic) with + let state3 ← match ← state2c.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -606,7 +606,7 @@ def test_nat_zero_add: TestM Unit := do #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"]) let tactic := "simp" - let state3d ← match ← state3.tryTactic (goalId := 0) (tactic := tactic) with + let state3d ← match ← state3.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -617,7 +617,7 @@ def test_nat_zero_add: TestM Unit := do addTest $ assertUnreachable e return () let tactic := "rfl" - let stateF ← match ← state2d.tryTactic (goalId := 0) (tactic := tactic) with + let stateF ← match ← state2d.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -637,7 +637,7 @@ def test_nat_zero_add_alt: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () let tactic := "intro n" - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -645,7 +645,7 @@ def test_nat_zero_add_alt: TestM Unit := do addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = #[buildGoal [("n", "Nat")] "n + 0 = n"]) let recursor := "@Nat.brecOn" - let state2 ← match ← state1.tryMotivatedApply (goalId := 0) (recursor := recursor) with + let state2 ← match ← state1.tryMotivatedApply (state1.get! 0) (recursor := recursor) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -660,7 +660,7 @@ def test_nat_zero_add_alt: TestM Unit := do ]) let tactic := "intro x" - let state3m ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with + let state3m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -668,7 +668,7 @@ def test_nat_zero_add_alt: TestM Unit := do addTest $ LSpec.check tactic ((← state3m.serializeGoals (options := ← read)).map (·.devolatilize) = #[buildGoal [("n", "Nat"), ("x", "Nat")] "Prop" (.some "motive")]) let tactic := "apply Eq" - let state3m2 ← match ← state3m.tryTactic (goalId := 0) (tactic := tactic) with + let state3m2 ← match ← state3m.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean index 22b342e..132718a 100644 --- a/Test/Tactic/Prograde.lean +++ b/Test/Tactic/Prograde.lean @@ -55,7 +55,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))" let state0 ← GoalState.create rootExpr let tactic := "intro p q h" - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -64,7 +64,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"]) let expr := "Or.inl (Or.inl h)" - let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with + let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -74,7 +74,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do let evalBind := "y" let evalExpr := "Or.inl h" - let state2 ← match ← state1.tryDefine (goalId := 0) (binderName := evalBind) (expr := evalExpr) with + let state2 ← match ← state1.tryDefine (state1.get! 0) (binderName := evalBind) (expr := evalExpr) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -94,7 +94,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do }]) let expr := "Or.inl y" - let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with + let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -112,22 +112,22 @@ def fun_define_root_expr: ∀ (p: Prop), PProd (Nat → p) Unit → p := by def test_define_root_expr : TestT Elab.TermElabM Unit := do --let rootExpr ← parseSentence "Nat" --let state0 ← GoalState.create rootExpr - --let .success state1 ← state0.tryTactic (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5" + --let .success state1 ← state0.tacticOn (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5" --let .some rootExpr := state1.rootExpr? | addTest $ assertUnreachable "Root expr" --addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "5") let rootExpr ← parseSentence "∀ (p: Prop), PProd (Nat → p) Unit → p" let state0 ← GoalState.create rootExpr let tactic := "intro p x" - let .success state1 ← state0.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic + let .success state1 ← state0.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic let binderName := `binder let value := "x.fst" let expr ← state1.goals[0]!.withContext $ strToTermSyntax value let tacticM := Tactic.evalDefine binderName expr - let .success state2 ← state1.tryTacticM (goalId := 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}" + let .success state2 ← state1.tryTacticM (state1.get! 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}" let tactic := s!"apply {binderName}" - let .success state3 ← state2.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic + let .success state3 ← state2.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic let tactic := s!"exact 5" - let .success state4 ← state3.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic + let .success state4 ← state3.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr" addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n let binder := x.fst;\n binder 5") @@ -139,7 +139,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))" let state0 ← GoalState.create rootExpr let tactic := "intro p q h" - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -148,7 +148,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"]) let expr := "Or.inl (Or.inl h)" - let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with + let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -158,7 +158,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do let haveBind := "y" let haveType := "p ∨ q" - let state2 ← match ← state1.tryHave (goalId := 0) (binderName := haveBind) (type := haveType) with + let state2 ← match ← state1.tryHave (state1.get! 0) (binderName := haveBind) (type := haveType) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -170,7 +170,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do ]) let expr := "Or.inl h" - let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with + let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -184,7 +184,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do addTest $ assertUnreachable e return () let expr := "Or.inl y" - let state4 ← match ← state2b.tryAssign (goalId := 0) (expr := expr) with + let state4 ← match ← state2b.tryAssign (state2b.get! 0) (expr := expr) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -199,7 +199,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))" let state0 ← GoalState.create rootExpr let tactic := "intro a p h" - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -213,8 +213,8 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do 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) + | true => state1.tryLet (state1.get! 0) (binderName := "b") (type := letType) + | false => state1.tryAssign (state1.get! 0) (expr := expr) let state2 ← match result2 with | .success state => pure state | other => do @@ -240,7 +240,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do ]) let tactic := "exact 1" - let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with + let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString @@ -266,14 +266,14 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do ]) let tactic := "exact h" - match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with + match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with | .failure #[message] => addTest $ LSpec.check tactic (message = s!"type mismatch\n h\nhas type\n a : Prop\nbut is expected to have type\n {mainTarget} : Prop") | other => do addTest $ assertUnreachable $ other.toString let tactic := "exact Or.inl (Or.inl h)" - let state4 ← match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with + let state4 ← match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString -- 2.44.1 From 37473b3efbec7be8e103b93ff343ad46dd0f4a35 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 6 Sep 2024 21:30:11 -0700 Subject: [PATCH 2/8] feat: Automatic mode (auto resume) --- Pantograph.lean | 13 ++++++++++++- Pantograph/Goal.lean | 24 ++++++++++++++++++++---- 2 files changed, 32 insertions(+), 5 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index 7cedab8..004c63f 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -20,6 +20,7 @@ structure State where /-- Main state monad for executing commands -/ abbrev MainM := ReaderT Context (StateT State Lean.CoreM) + -- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables -- certain monadic features in `MainM` abbrev CR α := Except Protocol.InteractionError α @@ -145,7 +146,17 @@ def execute (command: Protocol.Command): MainM Lean.Json := do pure $ Except.error $ error match nextGoalState? with | .error error => return .error error - | .ok (.success nextGoalState) => + | .ok (.success nextGoalState) => do + let nextGoalState ← match state.options.automaticMode, args.conv? with + | true, .none => do + let .ok result := nextGoalState.resume goalState.goals | throwError "Resuming known goals" + pure result + | true, .some true => pure nextGoalState + | true, .some false => do + let .some (_, _, dormantGoals) := goalState.convMVar? | throwError "If conv exit succeeded this should not fail" + let .ok result := nextGoalState.resume dormantGoals | throwError "Resuming known goals" + pure result + | false, _ => pure nextGoalState let nextStateId := state.nextId set { state with goalStates := state.goalStates.insert state.nextId nextGoalState, diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 0df3a4b..7486103 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -27,7 +27,8 @@ structure GoalState where parentMVar?: Option MVarId -- Existence of this field shows that we are currently in `conv` mode. - convMVar?: Option (MVarId × MVarId) := .none + -- (convRhs, goal, dormant) + convMVar?: Option (MVarId × MVarId × List MVarId) := .none -- Previous RHS for calc, so we don't have to repeat it every time -- WARNING: If using `state with` outside of `calc`, this must be set to `.none` calcPrevRhs?: Option (MVarId × Expr) := .none @@ -97,6 +98,20 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState calcPrevRhs? := .none, } +/-- Immediately bring all parent goals back into scope. Used in automatic mode -/ +@[export pantograph_goal_state_immediate_resume_parent] +protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState := + -- Prune parents solved goals + let mctx := state.mctx + let parentGoals := parent.goals.filter $ λ goal => mctx.eAssignment.contains goal + { + state with + savedState := { + state.savedState with + tactic := { goals := state.goals ++ parentGoals }, + }, + } + /-- Brings into scope a list of goals -/ @@ -116,7 +131,6 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S term := state.savedState.term, tactic := { goals := unassigned }, }, - calcPrevRhs? := .none, } /-- Brings into scope all goals from `branch` @@ -244,11 +258,13 @@ protected def GoalState.conv (state: GoalState) (goal: MVarId): return (← MonadBacktrack.saveState, convMVar) try let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic + -- Other goals are now dormant + let otherGoals := state.goals.filter $ λ g => g != goal return .success { root := state.root, savedState := nextSavedState parentMVar? := .some goal, - convMVar? := .some (convRhs, goal), + convMVar? := .some (convRhs, goal, otherGoals), calcPrevRhs? := .none } catch exception => @@ -257,7 +273,7 @@ protected def GoalState.conv (state: GoalState) (goal: MVarId): /-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/ protected def GoalState.convExit (state: GoalState): Elab.TermElabM TacticResult := do - let (convRhs, convGoal) ← match state.convMVar? with + let (convRhs, convGoal, _) ← match state.convMVar? with | .some mvar => pure mvar | .none => return .invalidAction "Not in conv state" let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do -- 2.44.1 From e2ad6ce6b3d2f57670313a0a975a3389d46a439f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 6 Sep 2024 21:32:02 -0700 Subject: [PATCH 3/8] doc: Documentation for automatic mode --- README.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/README.md b/README.md index 562f7ac..8bda1ef 100644 --- a/README.md +++ b/README.md @@ -90,6 +90,10 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va 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/Protocol.lean` + + One particular option for interest for machine learning researchers is the automatic mode. + `options.set { "automaticMode": true }`. This makes Pantograph act like + LeanDojo, with no resumption necessary to manage your goals. * `options.print`: Display the current set of options * `goal.start {["name": ], ["expr": ], ["levels": []], ["copyFrom": ]}`: Start a new proof from a given expression or symbol -- 2.44.1 From a7b30af36b7cf45182e6d4413018f7febcfd0396 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 6 Sep 2024 22:01:36 -0700 Subject: [PATCH 4/8] refactor: Refactor REPL out of main library fix: Calc previous rhs not found bug --- Main.lean | 1 + Pantograph.lean | 223 +----------------------------------------- Pantograph/Goal.lean | 10 +- Repl.lean | 223 ++++++++++++++++++++++++++++++++++++++++++ Test/Integration.lean | 2 + flake.nix | 30 ++++-- lakefile.lean | 5 +- 7 files changed, 257 insertions(+), 237 deletions(-) create mode 100644 Repl.lean diff --git a/Main.lean b/Main.lean index de73033..eb5240d 100644 --- a/Main.lean +++ b/Main.lean @@ -4,6 +4,7 @@ import Lean.Environment import Pantograph.Version import Pantograph.Library import Pantograph +import Repl -- Main IO functions open Pantograph diff --git a/Pantograph.lean b/Pantograph.lean index 004c63f..09327e8 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -1,4 +1,3 @@ -import Lean.Data.HashMap import Pantograph.Compile import Pantograph.Condensed import Pantograph.Environment @@ -6,224 +5,4 @@ import Pantograph.Goal import Pantograph.Library import Pantograph.Protocol import Pantograph.Serial - -namespace Pantograph - -structure Context where - imports: List String - -/-- Stores state of the REPL -/ -structure State where - options: Protocol.Options := {} - nextId: Nat := 0 - goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty - -/-- Main state monad for executing commands -/ -abbrev MainM := ReaderT Context (StateT State Lean.CoreM) - --- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables --- certain monadic features in `MainM` -abbrev CR α := Except Protocol.InteractionError α - -def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α := - metaM.run' -def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α := - termElabM.run' (ctx := Condensed.elabContext) |>.run' - -def execute (command: Protocol.Command): MainM Lean.Json := do - let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := - match Lean.fromJson? command.payload with - | .ok args => do - match (← comm args) with - | .ok result => return Lean.toJson result - | .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 - | "env.catalog" => run env_catalog - | "env.inspect" => run env_inspect - | "env.add" => run env_add - | "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 - | "compile.unit" => run compile_unit - | cmd => - let error: Protocol.InteractionError := - errorCommand s!"Unknown command {cmd}" - return Lean.toJson error - where - errorCommand := errorI "command" - errorIndex := errorI "index" - -- Command Functions - reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do - let state ← get - let nGoals := state.goalStates.size - set { state with nextId := 0, goalStates := Lean.HashMap.empty } - return .ok { nGoals } - stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do - let state ← get - let nGoals := state.goalStates.size - return .ok { nGoals } - env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do - let result ← Environment.catalog args - return .ok result - env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do - let state ← get - Environment.inspect args state.options - env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do - Environment.addDecl args - expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do - let state ← get - exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options) - options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do - let state ← get - let options := state.options - set { state with - options := { - -- FIXME: This should be replaced with something more elegant - printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty, - printExprPretty := args.printExprPretty?.getD options.printExprPretty, - printExprAST := args.printExprAST?.getD options.printExprAST, - printDependentMVars := args.printDependentMVars?.getD options.printDependentMVars, - noRepeat := args.noRepeat?.getD options.noRepeat, - printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls, - printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps - automaticMode := args.automaticMode?.getD options.automaticMode, - } - } - return .ok { } - options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do - return .ok (← get).options - goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do - let state ← get - let env ← Lean.MonadEnv.getEnv - let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with - | .some expr, .none => goalStartExpr expr (args.levels.getD #[]) - | .none, .some copyFrom => - (match env.find? <| copyFrom.toName with - | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" - | .some cInfo => return .ok (← GoalState.create cInfo.type)) - | _, _ => - return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied") - match expr? with - | .error error => return .error error - | .ok goalState => - 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 - let .some goalState := state.goalStates.find? args.stateId | - return .error $ errorIndex s!"Invalid state index {args.stateId}" - let .some goal := goalState.goals.get? args.goalId | - return .error $ errorIndex s!"Invalid goal index {args.goalId}" - let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do - match args.tactic?, args.expr?, args.have?, args.calc?, args.conv? with - | .some tactic, .none, .none, .none, .none => do - pure <| Except.ok <| ← goalState.tryTactic goal tactic - | .none, .some expr, .none, .none, .none => do - pure <| Except.ok <| ← goalState.tryAssign goal expr - | .none, .none, .some type, .none, .none => do - let binderName := args.binderName?.getD "" - pure <| Except.ok <| ← goalState.tryHave goal binderName type - | .none, .none, .none, .some pred, .none => do - pure <| Except.ok <| ← goalState.tryCalc goal pred - | .none, .none, .none, .none, .some true => do - pure <| Except.ok <| ← goalState.conv goal - | .none, .none, .none, .none, .some false => do - pure <| Except.ok <| ← goalState.convExit - | _, _, _, _, _ => - let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied" - pure $ Except.error $ error - match nextGoalState? with - | .error error => return .error error - | .ok (.success nextGoalState) => do - let nextGoalState ← match state.options.automaticMode, args.conv? with - | true, .none => do - let .ok result := nextGoalState.resume goalState.goals | throwError "Resuming known goals" - pure result - | true, .some true => pure nextGoalState - | true, .some false => do - let .some (_, _, dormantGoals) := goalState.convMVar? | throwError "If conv exit succeeded this should not fail" - let .ok result := nextGoalState.resume dormantGoals | throwError "Resuming known goals" - pure result - | false, _ => pure nextGoalState - let nextStateId := state.nextId - set { state with - goalStates := state.goalStates.insert state.nextId nextGoalState, - nextId := state.nextId + 1, - } - let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run' - return .ok { - nextStateId? := .some nextStateId, - goals? := .some goals, - } - | .ok (.parseError message) => - return .ok { parseError? := .some message } - | .ok (.invalidAction message) => - return .error $ errorI "invalid" message - | .ok (.failure messages) => - return .ok { tacticErrors? := .some messages } - goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do - let state ← get - 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.find? branchId with - | .none => return .error $ errorIndex s!"Invalid state index {branchId}" - | .some branch => pure $ goalContinue target branch - | .none, .some goals => - pure $ goalResume target goals - | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied" - match nextState? with - | .error error => return .error <| errorI "structure" error - | .ok nextGoalState => - let nextStateId := state.nextId - set { state with - goalStates := state.goalStates.insert nextStateId nextGoalState, - nextId := state.nextId + 1 - } - let goals ← goalSerialize nextGoalState (options := state.options) - return .ok { - nextStateId, - goals, - } - goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do - let state ← get - 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.find? args.stateId with - | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" - | .some goalState => runMetaM <| do - return .ok (← goalPrint goalState state.options) - compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do - let module := args.module.toName - try - let steps ← Compile.processSource module - let units? := if args.compilationUnits then - .some $ steps.map λ step => (step.src.startPos.byteIdx, step.src.stopPos.byteIdx) - else - .none - let invocations? ← if args.invocations then - pure $ .some (← Compile.collectTacticsFromCompilation steps) - else - pure .none - return .ok { units?, invocations? } - catch e => - return .error $ errorI "compile" (← e.toMessageData.toString) - -end Pantograph +import Pantograph.Version diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 7486103..225b8ac 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -307,7 +307,7 @@ protected def GoalState.convExit (state: GoalState): return .failure #[← exception.toMessageData.toString] protected def GoalState.calcPrevRhsOf? (state: GoalState) (goal: MVarId): Option Expr := do - let (mvarId, rhs ) ← state.calcPrevRhs? + let (mvarId, rhs) ← state.calcPrevRhs? if mvarId == goal then .some rhs else @@ -352,9 +352,8 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String) (userName := tag ++ `calc) let mvarBranch := proof.mvarId! - let calcPrevRhs? := Option.some (goal, rhs) let mut proofType ← Meta.inferType proof - let mut remainder := Option.none + let mut remainder? := Option.none -- The calc tactic either solves the main goal or leaves another relation. -- Replace the main goal, and save the new goal if necessary @@ -367,10 +366,11 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String) let lastStepGoal ← Meta.mkFreshExprSyntheticOpaqueMVar lastStep tag (proof, proofType) ← Elab.Term.mkCalcTrans proof proofType lastStepGoal lastStep unless ← Meta.isDefEq proofType target do throwFailed - remainder := .some lastStepGoal.mvarId! + remainder? := .some lastStepGoal.mvarId! goal.assign proof - let goals := [ mvarBranch ] ++ remainder.toList + let goals := [ mvarBranch ] ++ remainder?.toList + let calcPrevRhs? := remainder?.map $ λ g => (g, rhs) return .success { root := state.root, savedState := { diff --git a/Repl.lean b/Repl.lean new file mode 100644 index 0000000..da594e3 --- /dev/null +++ b/Repl.lean @@ -0,0 +1,223 @@ +import Lean.Data.HashMap +import Pantograph + +namespace Pantograph + +structure Context where + imports: List String + +/-- Stores state of the REPL -/ +structure State where + options: Protocol.Options := {} + nextId: Nat := 0 + goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty + +/-- Main state monad for executing commands -/ +abbrev MainM := ReaderT Context (StateT State Lean.CoreM) + +-- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables +-- certain monadic features in `MainM` +abbrev CR α := Except Protocol.InteractionError α + +def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α := + metaM.run' +def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α := + termElabM.run' (ctx := Condensed.elabContext) |>.run' + +def execute (command: Protocol.Command): MainM Lean.Json := do + let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := + match Lean.fromJson? command.payload with + | .ok args => do + match (← comm args) with + | .ok result => return Lean.toJson result + | .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 + | "env.catalog" => run env_catalog + | "env.inspect" => run env_inspect + | "env.add" => run env_add + | "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 + | "compile.unit" => run compile_unit + | cmd => + let error: Protocol.InteractionError := + errorCommand s!"Unknown command {cmd}" + return Lean.toJson error + where + errorCommand := errorI "command" + errorIndex := errorI "index" + -- Command Functions + reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do + let state ← get + let nGoals := state.goalStates.size + set { state with nextId := 0, goalStates := Lean.HashMap.empty } + return .ok { nGoals } + stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do + let state ← get + let nGoals := state.goalStates.size + return .ok { nGoals } + env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do + let result ← Environment.catalog args + return .ok result + env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do + let state ← get + Environment.inspect args state.options + env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do + Environment.addDecl args + expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do + let state ← get + exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options) + options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do + let state ← get + let options := state.options + set { state with + options := { + -- FIXME: This should be replaced with something more elegant + printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty, + printExprPretty := args.printExprPretty?.getD options.printExprPretty, + printExprAST := args.printExprAST?.getD options.printExprAST, + printDependentMVars := args.printDependentMVars?.getD options.printDependentMVars, + noRepeat := args.noRepeat?.getD options.noRepeat, + printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls, + printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps + automaticMode := args.automaticMode?.getD options.automaticMode, + } + } + return .ok { } + options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do + return .ok (← get).options + goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do + let state ← get + let env ← Lean.MonadEnv.getEnv + let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with + | .some expr, .none => goalStartExpr expr (args.levels.getD #[]) + | .none, .some copyFrom => + (match env.find? <| copyFrom.toName with + | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" + | .some cInfo => return .ok (← GoalState.create cInfo.type)) + | _, _ => + return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied") + match expr? with + | .error error => return .error error + | .ok goalState => + 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 + let .some goalState := state.goalStates.find? args.stateId | + return .error $ errorIndex s!"Invalid state index {args.stateId}" + let .some goal := goalState.goals.get? args.goalId | + return .error $ errorIndex s!"Invalid goal index {args.goalId}" + let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do + match args.tactic?, args.expr?, args.have?, args.calc?, args.conv? with + | .some tactic, .none, .none, .none, .none => do + pure <| Except.ok <| ← goalState.tryTactic goal tactic + | .none, .some expr, .none, .none, .none => do + pure <| Except.ok <| ← goalState.tryAssign goal expr + | .none, .none, .some type, .none, .none => do + let binderName := args.binderName?.getD "" + pure <| Except.ok <| ← goalState.tryHave goal binderName type + | .none, .none, .none, .some pred, .none => do + pure <| Except.ok <| ← goalState.tryCalc goal pred + | .none, .none, .none, .none, .some true => do + pure <| Except.ok <| ← goalState.conv goal + | .none, .none, .none, .none, .some false => do + pure <| Except.ok <| ← goalState.convExit + | _, _, _, _, _ => + let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied" + pure $ Except.error $ error + match nextGoalState? with + | .error error => return .error error + | .ok (.success nextGoalState) => do + let nextGoalState ← match state.options.automaticMode, args.conv? with + | true, .none => do + let .ok result := nextGoalState.resume goalState.goals | throwError "Resuming known goals" + pure result + | true, .some true => pure nextGoalState + | true, .some false => do + let .some (_, _, dormantGoals) := goalState.convMVar? | throwError "If conv exit succeeded this should not fail" + let .ok result := nextGoalState.resume dormantGoals | throwError "Resuming known goals" + pure result + | false, _ => pure nextGoalState + let nextStateId := state.nextId + set { state with + goalStates := state.goalStates.insert state.nextId nextGoalState, + nextId := state.nextId + 1, + } + let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run' + return .ok { + nextStateId? := .some nextStateId, + goals? := .some goals, + } + | .ok (.parseError message) => + return .ok { parseError? := .some message } + | .ok (.invalidAction message) => + return .error $ errorI "invalid" message + | .ok (.failure messages) => + return .ok { tacticErrors? := .some messages } + goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do + let state ← get + 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.find? branchId with + | .none => return .error $ errorIndex s!"Invalid state index {branchId}" + | .some branch => pure $ goalContinue target branch + | .none, .some goals => + pure $ goalResume target goals + | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied" + match nextState? with + | .error error => return .error <| errorI "structure" error + | .ok nextGoalState => + let nextStateId := state.nextId + set { state with + goalStates := state.goalStates.insert nextStateId nextGoalState, + nextId := state.nextId + 1 + } + let goals ← goalSerialize nextGoalState (options := state.options) + return .ok { + nextStateId, + goals, + } + goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do + let state ← get + 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.find? args.stateId with + | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" + | .some goalState => runMetaM <| do + return .ok (← goalPrint goalState state.options) + compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do + let module := args.module.toName + try + let steps ← Compile.processSource module + let units? := if args.compilationUnits then + .some $ steps.map λ step => (step.src.startPos.byteIdx, step.src.stopPos.byteIdx) + else + .none + let invocations? ← if args.invocations then + pure $ .some (← Compile.collectTacticsFromCompilation steps) + else + pure .none + return .ok { units?, invocations? } + catch e => + return .error $ errorI "compile" (← e.toMessageData.toString) + +end Pantograph diff --git a/Test/Integration.lean b/Test/Integration.lean index 931c9f2..3ccff81 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -2,6 +2,8 @@ -/ import LSpec import Pantograph +import Repl + namespace Pantograph.Test.Integration open Pantograph diff --git a/flake.nix b/flake.nix index 088f306..70c84b5 100644 --- a/flake.nix +++ b/flake.nix @@ -37,14 +37,25 @@ }; project = leanPkgs.buildLeanPackage { name = "Pantograph"; - roots = [ "Main" "Pantograph" ]; - src = pkgs.lib.cleanSourceWith { + roots = [ "Pantograph" ]; + src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { src = ./.; filter = path: type: !(pkgs.lib.hasInfix "/Test/" path) && !(pkgs.lib.hasSuffix ".md" path) && - !(pkgs.lib.hasSuffix "Makefile" path); - }; + !(pkgs.lib.hasSuffix "Repl.lean" path); + }); + }; + repl = leanPkgs.buildLeanPackage { + name = "Repl"; + roots = [ "Main" "Repl" ]; + deps = [ project ]; + src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { + src = ./.; + filter = path: type: + !(pkgs.lib.hasInfix "/Test/" path) && + !(pkgs.lib.hasSuffix ".md" path); + }); }; test = leanPkgs.buildLeanPackage { name = "Test"; @@ -52,18 +63,19 @@ # root begins (e.g. `import Test.Environment` and not `import # Environment`) and thats where `lakefile.lean` resides. roots = [ "Test.Main" ]; - deps = [ lspecLib project ]; - src = pkgs.lib.cleanSourceWith { + deps = [ lspecLib repl ]; + src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { src = ./.; filter = path: type: !(pkgs.lib.hasInfix "Pantograph" path); - }; + }); }; in rec { packages = { inherit (leanPkgs) lean lean-all; - inherit (project) sharedLib executable; - default = project.executable; + inherit (project) sharedLib; + inherit (repl) executable; + default = repl.executable; }; legacyPackages = { inherit project leanPkgs; diff --git a/lakefile.lean b/lakefile.lean index c68d0db..e29fa0e 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,11 +4,14 @@ open Lake DSL package pantograph lean_lib Pantograph { + roots := #[`Pantograph] defaultFacets := #[LeanLib.sharedFacet] } +lean_lib Repl { +} @[default_target] -lean_exe pantograph { +lean_exe repl { root := `Main -- Solves the native symbol not found problem supportInterpreter := true -- 2.44.1 From 9b3eef35ec40a09bba7140ecfc04dafddbd92c27 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 6 Sep 2024 22:22:19 -0700 Subject: [PATCH 5/8] fix: Forgot to include the current goals in resume --- Repl.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Repl.lean b/Repl.lean index da594e3..08533b0 100644 --- a/Repl.lean +++ b/Repl.lean @@ -143,12 +143,12 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .ok (.success nextGoalState) => do let nextGoalState ← match state.options.automaticMode, args.conv? with | true, .none => do - let .ok result := nextGoalState.resume goalState.goals | throwError "Resuming known goals" + let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) | throwError "Resuming known goals" pure result | true, .some true => pure nextGoalState | true, .some false => do let .some (_, _, dormantGoals) := goalState.convMVar? | throwError "If conv exit succeeded this should not fail" - let .ok result := nextGoalState.resume dormantGoals | throwError "Resuming known goals" + let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) | throwError "Resuming known goals" pure result | false, _ => pure nextGoalState let nextStateId := state.nextId -- 2.44.1 From 68dac4c951c1b6eddfa2044daffed26f9cea7fae Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 7 Sep 2024 13:55:41 -0700 Subject: [PATCH 6/8] chore: Version bump to 0.2.18 --- Pantograph/Version.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index f3bcf93..ed33cbb 100644 --- a/Pantograph/Version.lean +++ b/Pantograph/Version.lean @@ -1,6 +1,6 @@ namespace Pantograph @[export pantograph_version] -def version := "0.2.17" +def version := "0.2.18" end Pantograph -- 2.44.1 From e4d53733d008bbda48c7d3513ac901fb4c3f3f12 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 7 Sep 2024 14:03:29 -0700 Subject: [PATCH 7/8] feat: Simplify repl --- Repl.lean | 53 +++++++++++++++++++++++++---------------------------- 1 file changed, 25 insertions(+), 28 deletions(-) diff --git a/Repl.lean b/Repl.lean index 08533b0..a916f3f 100644 --- a/Repl.lean +++ b/Repl.lean @@ -169,30 +169,28 @@ 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.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.find? branchId with - | .none => return .error $ errorIndex s!"Invalid state index {branchId}" - | .some branch => pure $ goalContinue target branch - | .none, .some goals => - pure $ goalResume target goals - | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied" - match nextState? with - | .error error => return .error <| errorI "structure" error - | .ok nextGoalState => - let nextStateId := state.nextId - set { state with - goalStates := state.goalStates.insert nextStateId nextGoalState, - nextId := state.nextId + 1 - } - let goals ← goalSerialize nextGoalState (options := state.options) - return .ok { - nextStateId, - goals, - } + let .some target := state.goalStates.find? args.target | return .error $ errorIndex s!"Invalid state index {args.target}" + let nextState? ← match args.branch?, args.goals? with + | .some branchId, .none => do + match state.goalStates.find? branchId with + | .none => return .error $ errorIndex s!"Invalid state index {branchId}" + | .some branch => pure $ goalContinue target branch + | .none, .some goals => + pure $ goalResume target goals + | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied" + match nextState? with + | .error error => return .error <| errorI "structure" error + | .ok nextGoalState => + let nextStateId := state.nextId + set { state with + goalStates := state.goalStates.insert nextStateId nextGoalState, + nextId := state.nextId + 1 + } + let goals ← goalSerialize nextGoalState (options := state.options) + return .ok { + nextStateId, + goals, + } goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do let state ← get let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates @@ -200,10 +198,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do return .ok {} goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do let state ← get - match state.goalStates.find? args.stateId with - | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" - | .some goalState => runMetaM <| do - return .ok (← goalPrint goalState state.options) + let .some goalState := state.goalStates.find? args.stateId | return .error $ errorIndex s!"Invalid state index {args.stateId}" + let result ← runMetaInMainM <| goalPrint goalState state.options + return .ok result compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do let module := args.module.toName try -- 2.44.1 From 25bb96460455a29630a6ac86af389a0eefd07101 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 8 Sep 2024 11:57:39 -0700 Subject: [PATCH 8/8] test: Automatic mode testing refactor: Simplified integration test structure --- Test/Integration.lean | 224 ++++++++++++++++++++++-------------------- Test/Main.lean | 2 +- 2 files changed, 121 insertions(+), 105 deletions(-) diff --git a/Test/Integration.lean b/Test/Integration.lean index 3ccff81..b82962b 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -3,40 +3,23 @@ import LSpec import Pantograph import Repl +import Test.Common namespace Pantograph.Test.Integration open Pantograph -def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json)) - (expected: Lean.Json): MainM LSpec.TestSeq := do - let result ← execute { cmd := cmd, payload := Lean.Json.mkObj payload } - return LSpec.test name (toString result = toString expected) -def subroutine_step (cmd: String) (payload: List (String × Lean.Json)) - (expected: Lean.Json): MainM LSpec.TestSeq := subroutine_named_step cmd cmd payload expected +def step { α } [Lean.ToJson α] (cmd: String) (payload: List (String × Lean.Json)) + (expected: α) (name? : Option String := .none): MainM LSpec.TestSeq := do + let payload := Lean.Json.mkObj payload + let name := name?.getD s!"{cmd} {payload.compress}" + let result ← execute { cmd, payload } + return LSpec.test name (toString result = toString (Lean.toJson expected)) -def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := do - -- Setup the environment for execution - let env ← Lean.importModules - (imports := #[{module := Lean.Name.str .anonymous "Init", runtimeOnly := false }]) - (opts := {}) - (trustLevel := 1) - let context: Context := { - imports := ["Init"] - } - let coreContext: Lean.Core.Context ← createCoreContext #[] - let commands: MainM LSpec.TestSeq := - steps.foldlM (λ suite step => do - let result ← step - return suite ++ result) LSpec.TestSeq.done - try - let coreM := commands.run context |>.run' {} - return Prod.fst $ (← coreM.toIO coreContext { env := env }) - catch ex => - return LSpec.check s!"Uncaught IO exception: {ex.toString}" false +abbrev Test := List (MainM LSpec.TestSeq) -def test_elab : IO LSpec.TestSeq := - subroutine_runner [ - subroutine_step "expr.echo" +def test_elab : Test := + [ + step "expr.echo" [("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])] (Lean.toJson ({ type := { pp? := .some "{α : Type u} → Type u" }, @@ -44,46 +27,33 @@ def test_elab : IO LSpec.TestSeq := }: Protocol.ExprEchoResult)), ] -def test_option_modify : IO LSpec.TestSeq := +def test_option_modify : Test := let pp? := Option.some "∀ (n : Nat), n + 1 = n.succ" let sexp? := Option.some "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))" let module? := Option.some "Init.Data.Nat.Basic" let options: Protocol.Options := {} - subroutine_runner [ - subroutine_step "env.inspect" - [("name", .str "Nat.add_one")] - (Lean.toJson ({ - type := { pp? }, module? }: - Protocol.EnvInspectResult)), - subroutine_step "options.set" - [("printExprAST", .bool true)] - (Lean.toJson ({ }: - Protocol.OptionsSetResult)), - subroutine_step "env.inspect" - [("name", .str "Nat.add_one")] - (Lean.toJson ({ - type := { pp?, sexp? }, module? }: - Protocol.EnvInspectResult)), - subroutine_step "options.print" - [] - (Lean.toJson ({ options with printExprAST := true }: - Protocol.Options)) + [ + step "env.inspect" [("name", .str "Nat.add_one")] + ({ type := { pp? }, module? }: Protocol.EnvInspectResult), + step "options.set" [("printExprAST", .bool true)] + ({ }: Protocol.OptionsSetResult), + step "env.inspect" [("name", .str "Nat.add_one")] + ({ type := { pp?, sexp? }, module? }: Protocol.EnvInspectResult), + step "options.print" [] + ({ options with printExprAST := true }: Protocol.Options), ] -def test_malformed_command : IO LSpec.TestSeq := +def test_malformed_command : Test := let invalid := "invalid" - subroutine_runner [ - subroutine_named_step "Invalid command" invalid - [("name", .str "Nat.add_one")] - (Lean.toJson ({ - error := "command", desc := s!"Unknown command {invalid}"}: - Protocol.InteractionError)), - subroutine_named_step "JSON Deserialization" "expr.echo" - [(invalid, .str "Random garbage data")] - (Lean.toJson ({ - error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}: - Protocol.InteractionError)) + [ + step invalid [("name", .str "Nat.add_one")] + ({ error := "command", desc := s!"Unknown command {invalid}" }: Protocol.InteractionError) + (name? := .some "Invalid Command"), + step "expr.echo" [(invalid, .str "Random garbage data")] + ({ error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected" }: + Protocol.InteractionError) + (name? := .some "JSON Deserialization") ] -def test_tactic : IO LSpec.TestSeq := +def test_tactic : Test := let goal1: Protocol.Goal := { name := "_uniq.11", target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" }, @@ -97,77 +67,123 @@ def test_tactic : IO LSpec.TestSeq := { name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }} ], } - subroutine_runner [ - subroutine_step "goal.start" - [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")] - (Lean.toJson ({stateId := 0, root := "_uniq.9"}: - Protocol.GoalStartResult)), - subroutine_step "goal.tactic" - [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")] - (Lean.toJson ({ - nextStateId? := .some 1, - goals? := #[goal1], - }: - Protocol.GoalTacticResult)), - subroutine_step "goal.print" - [("stateId", .num 1)] - (Lean.toJson ({ - parent? := .some { pp? := .some "fun x => ?m.12 x" }, - }: - Protocol.GoalPrintResult)), - subroutine_step "goal.tactic" - [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")] - (Lean.toJson ({ - nextStateId? := .some 2, - goals? := #[goal2], - }: - Protocol.GoalTacticResult)) + [ + step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")] + ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult), + step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")] + ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult), + step "goal.print" [("stateId", .num 1)] + ({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult), + step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")] + ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult), + ] +def test_automatic_mode (automatic: Bool): Test := + let varsPQ := #[ + { name := "_uniq.10", userName := "p", type? := .some { pp? := .some "Prop" }}, + { name := "_uniq.13", userName := "q", type? := .some { pp? := .some "Prop" }} + ] + let goal1: Protocol.Goal := { + name := "_uniq.17", + target := { pp? := .some "q ∨ p" }, + vars := varsPQ ++ #[ + { name := "_uniq.16", userName := "h", type? := .some { pp? := .some "p ∨ q" }} + ], + } + let goal2l: Protocol.Goal := { + name := "_uniq.59", + userName? := .some "inl", + target := { pp? := .some "q ∨ p" }, + vars := varsPQ ++ #[ + { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true} + ], + } + let goal2r: Protocol.Goal := { + name := "_uniq.72", + userName? := .some "inr", + target := { pp? := .some "q ∨ p" }, + vars := varsPQ ++ #[ + { name := "_uniq.60", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true} + ], + } + let goal3l: Protocol.Goal := { + name := "_uniq.78", + userName? := .some "inl.h", + target := { pp? := .some "p" }, + vars := varsPQ ++ #[ + { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true} + ], + } + [ + step "options.set" [("automaticMode", .bool automatic)] + ({}: Protocol.OptionsSetResult), + step "goal.start" [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")] + ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult), + step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro p q h")] + ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult), + step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "cases h")] + ({ nextStateId? := .some 2, goals? := #[goal2l, goal2r], }: Protocol.GoalTacticResult), + let goals? := if automatic then #[goal3l, goal2r] else #[goal3l] + step "goal.tactic" [("stateId", .num 2), ("goalId", .num 0), ("tactic", .str "apply Or.inr")] + ({ nextStateId? := .some 3, goals?, }: Protocol.GoalTacticResult), ] -def test_env_add_inspect : IO LSpec.TestSeq := +def test_env_add_inspect : Test := let name1 := "Pantograph.mystery" let name2 := "Pantograph.mystery2" - subroutine_runner [ - subroutine_step "env.add" + [ + step "env.add" [ ("name", .str name1), ("type", .str "Prop → Prop → Prop"), ("value", .str "λ (a b: Prop) => Or a b"), ("isTheorem", .bool false) ] - (Lean.toJson ({}: Protocol.EnvAddResult)), - subroutine_step "env.inspect" - [("name", .str name1)] - (Lean.toJson ({ + ({}: Protocol.EnvAddResult), + step "env.inspect" [("name", .str name1)] + ({ value? := .some { pp? := .some "fun a b => a ∨ b" }, type := { pp? := .some "Prop → Prop → Prop" }, }: - Protocol.EnvInspectResult)), - subroutine_step "env.add" + Protocol.EnvInspectResult), + step "env.add" [ ("name", .str name2), ("type", .str "Nat → Int"), ("value", .str "λ (a: Nat) => a + 1"), ("isTheorem", .bool false) ] - (Lean.toJson ({}: Protocol.EnvAddResult)), - subroutine_step "env.inspect" - [("name", .str name2)] - (Lean.toJson ({ + ({}: Protocol.EnvAddResult), + step "env.inspect" [("name", .str name2)] + ({ value? := .some { pp? := .some "fun a => ↑a + 1" }, type := { pp? := .some "Nat → Int" }, }: - Protocol.EnvInspectResult)) + Protocol.EnvInspectResult) ] -def suite: List (String × IO LSpec.TestSeq) := - [ - ("Elab", test_elab), - ("Option modify", test_option_modify), +def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do + -- Setup the environment for execution + let context: Context := { + imports := ["Init"] + } + let commands: MainM LSpec.TestSeq := + steps.foldlM (λ suite step => do + let result ← step + return suite ++ result) LSpec.TestSeq.done + runCoreMSeq env <| commands.run context |>.run' {} + + +def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := + let tests := [ + ("expr.echo", test_elab), + ("options.set options.print", test_option_modify), ("Malformed command", test_malformed_command), ("Tactic", test_tactic), + ("Manual Mode", test_automatic_mode false), + ("Automatic Mode", test_automatic_mode true), ("env.add env.inspect", test_env_add_inspect), ] + tests.map (fun (name, test) => (name, runTest env test)) end Pantograph.Test.Integration diff --git a/Test/Main.lean b/Test/Main.lean index 89c757a..6da6640 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -44,7 +44,7 @@ def main (args: List String) := do let suites: List (String × List (String × IO LSpec.TestSeq)) := [ ("Environment", Environment.suite), - ("Integration", Integration.suite), + ("Integration", Integration.suite env_default), ("Library", Library.suite env_default), ("Metavar", Metavar.suite env_default), ("Proofs", Proofs.suite env_default), -- 2.44.1