From 7acf1ffdf1de629141129a077c5f10405407a81f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 25 Jun 2024 16:58:35 -0400 Subject: [PATCH] refactor: Move `have` to prograde tactic --- Pantograph.lean | 2 +- Pantograph/Compile.lean | 2 +- Pantograph/Compile/Parse.lean | 14 +++++++ Pantograph/Goal.lean | 72 +++------------------------------ Pantograph/Library.lean | 9 ++++- Pantograph/Tactic/Prograde.lean | 25 ++++++++++++ 6 files changed, 53 insertions(+), 71 deletions(-) create mode 100644 Pantograph/Compile/Parse.lean diff --git a/Pantograph.lean b/Pantograph.lean index 097651f..35ab117 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -125,7 +125,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do pure ( Except.ok (← goalAssign goalState args.goalId expr)) | .none, .none, .some type, .none, .none => do let binderName := args.binderName?.getD "" - pure ( Except.ok (← goalHave goalState args.goalId binderName type)) + 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 diff --git a/Pantograph/Compile.lean b/Pantograph/Compile.lean index 15081d9..83b463f 100644 --- a/Pantograph/Compile.lean +++ b/Pantograph/Compile.lean @@ -2,7 +2,7 @@ import Pantograph.Protocol import Pantograph.Compile.Frontend import Pantograph.Compile.Elab - +import Pantograph.Compile.Parse open Lean diff --git a/Pantograph/Compile/Parse.lean b/Pantograph/Compile/Parse.lean new file mode 100644 index 0000000..72eb620 --- /dev/null +++ b/Pantograph/Compile/Parse.lean @@ -0,0 +1,14 @@ +import Lean + +open Lean + +namespace Pantograph.Compile + +def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do + return Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := s) + (fileName := "") + +end Pantograph.Compile diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index b2f6f53..60a28d6 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -5,6 +5,7 @@ All the functions starting with `try` resume their inner monadic state. -/ import Pantograph.Protocol import Pantograph.Tactic +import Pantograph.Compile.Parse import Lean def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog := @@ -277,57 +278,6 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String -- Specialized Tactics -protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): - Elab.TermElabM TacticResult := do - state.restoreElabM - let goal ← match state.savedState.tactic.goals.get? goalId with - | .some goal => pure goal - | .none => return .indexError goalId - goal.checkNotAssigned `GoalState.tryHave - let type ← match Parser.runParserCategory - (env := state.env) - (catName := `term) - (input := type) - (fileName := filename) with - | .ok syn => pure syn - | .error error => return .parseError error - let binderName := binderName.toName - try - -- Implemented similarly to the intro tactic - let nextGoals: List MVarId ← goal.withContext do - let type ← Elab.Term.elabType (stx := type) - let lctx ← MonadLCtx.getLCtx - - -- The branch goal inherits the same context, but with a different type - let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type - - -- Create the context for the `upstream` goal - let fvarId ← mkFreshFVarId - let lctxUpstream := lctx.mkLocalDecl fvarId binderName type - let fvar := mkFVar fvarId - let mvarUpstream ← - withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do - Meta.withNewLocalInstances #[fvar] 0 do - let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) - (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous) - -- FIXME: May be redundant? - let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream - goal.assign expr - pure mvarUpstream - - pure [mvarBranch.mvarId!, mvarUpstream.mvarId!] - return .success { - root := state.root, - savedState := { - term := ← MonadBacktrack.saveState, - tactic := { goals := nextGoals } - }, - newMVars := nextGoals.toSSet, - parentMVar? := .some goal, - calcPrevRhs? := .none - } - catch exception => - return .failure #[← exception.toMessageData.toString] protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Elab.TermElabM TacticResult := do state.restoreElabM @@ -527,33 +477,21 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Elab.TermElabM TacticResult := do state.restoreElabM - let recursor ← match Parser.runParserCategory - (env := state.env) - (catName := `term) - (input := recursor) - (fileName := filename) with + let recursor ← match (← Compile.parseTermM recursor) with | .ok syn => pure syn | .error error => return .parseError error state.execute goalId (tacticM := Tactic.motivatedApply recursor) protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Elab.TermElabM TacticResult := do state.restoreElabM - let recursor ← match Parser.runParserCategory - (env := state.env) - (catName := `term) - (input := eq) - (fileName := filename) with + let eq ← match (← Compile.parseTermM eq) with | .ok syn => pure syn | .error error => return .parseError error - state.execute goalId (tacticM := Tactic.noConfuse recursor) + state.execute goalId (tacticM := Tactic.noConfuse eq) protected def GoalState.tryEval (state: GoalState) (goalId: Nat) (binderName: Name) (expr: String) : Elab.TermElabM TacticResult := do state.restoreElabM - let expr ← match Parser.runParserCategory - (env := state.env) - (catName := `term) - (input := expr) - (fileName := filename) with + let expr ← match (← Compile.parseTermM expr) with | .ok syn => pure syn | .error error => return .parseError error state.execute goalId (tacticM := Tactic.evaluate binderName expr) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 8036103..aa8bcbc 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -180,8 +180,13 @@ def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticRe def goalAssign (state: GoalState) (goalId: Nat) (expr: String): CoreM TacticResult := runTermElabM <| state.tryAssign goalId expr @[export pantograph_goal_have_m] -def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := - runTermElabM <| state.tryHave goalId binderName type +protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (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.execute goalId (Tactic.have_t binderName.toName type) @[export pantograph_goal_let_m] def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := runTermElabM <| state.tryLet goalId binderName type diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean index 81dd28c..4c525c2 100644 --- a/Pantograph/Tactic/Prograde.lean +++ b/Pantograph/Tactic/Prograde.lean @@ -19,4 +19,29 @@ def evaluate (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do pure [mvarUpstream.mvarId!] Elab.Tactic.setGoals nextGoals +def have_t (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do + let goal ← Elab.Tactic.getMainGoal + let nextGoals: List MVarId ← goal.withContext do + let type ← Elab.Term.elabType (stx := type) + let lctx ← MonadLCtx.getLCtx + + -- The branch goal inherits the same context, but with a different type + let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type + + -- Create the context for the `upstream` goal + let fvarId ← mkFreshFVarId + let lctxUpstream := lctx.mkLocalDecl fvarId binderName type + let fvar := mkFVar fvarId + let mvarUpstream ← + withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do + Meta.withNewLocalInstances #[fvar] 0 do + let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) + (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous) + --let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream + goal.assign mvarUpstream + pure mvarUpstream + + pure [mvarBranch.mvarId!, mvarUpstream.mvarId!] + Elab.Tactic.setGoals nextGoals + end Pantograph.Tactic