-
Notifications
You must be signed in to change notification settings - Fork 1
/
Rewrite.lean
127 lines (104 loc) · 4.72 KB
/
Rewrite.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
import Std.Lean.Position
import MotivatedMoves.ForMathlib.Utils
import MotivatedMoves.GUI.DynamicEditButton
/-!
# Point-and-click rewriting
This file defines a widget for making targeted rewrites by
pointing and clicking sub-expressions in the infoview.
Once a sub-expression is selected, a `rw` tactic call with
a configuration targeting the selected location is generated.
-/
open Lean Server Elab Meta ProofWidgets Jsx Json Parser Tactic
/-- `Props` for point-and-click rewriting. -/
structure RewriteProps extends InteractiveTacticProps where
/-- A flag to indicate whether to rewrite in reverse. -/
symm : Bool
/-- An expression representing the argument of the rewrite tactic. -/
rwRule : WithRpcRef AbstractMVarsResult
deriving instance TypeName for AbstractMVarsResult
#mkrpcenc RewriteProps
section
/-- Convert `Occurrences` to a `String`. -/
instance : ToString Occurrences where
toString := fun
| .all => ".all"
| .pos occs => s!".pos {occs}"
| .neg occs => s!".neg {occs}"
/-- Convert a `Rewrite.Config` to a `String`.
This instance is restricted to printing just the information about the occurrences. -/
instance : ToString Rewrite.Config where
toString cfg :=
"{ " ++ s!"occs := {cfg.occs}" ++ " }"
/-- Extract the left and right hand sides of an equality or iff statement. -/
def matchEqn? (e : Expr) : MetaM (Option (Expr × Expr)) := do
match ← matchEq? e with
| some (_, lhs, rhs) => return (lhs, rhs)
| none => return e.iff?
end
/-- Specialises the theorem to match the sub-expression at the given position
and calculates its occurrence number in the whole expression. -/
def findRewriteOccurrence (thm : Expr) (symm : Bool)
(position : SubExpr.Pos) (target : Expr) : MetaM (Nat × Expr) := do
let stmt ← inferType thm
let (vars, _, eqn) ← forallMetaTelescopeReducing stmt
let .some (lhs, rhs) ← matchEqn? eqn |
panic! s!"Received {stmt}; equality or iff proof expected."
let hs := if symm then rhs else lhs
let occurrence ← findMatchingOccurrence position target hs
let pattern := mkAppN thm <| ← vars.mapM instantiateMVars
return (occurrence, ← reduce (skipTypes := false) (skipProofs := false) pattern)
/-- Generates a rewrite tactic call with configuration from the arguments. -/
def rewriteTacticCall (loc : SubExpr.GoalsLocation) (goal : Widget.InteractiveGoal)
(thmAbst : AbstractMVarsResult) (symm : Bool) : MetaM String := do
let subExpr ← loc.toSubExpr
let us ← thmAbst.paramNames.mapM <| fun _ ↦ mkFreshLevelMVar
let thm := thmAbst.expr.instantiateLevelParamsArray thmAbst.paramNames us
let (occurrence, pattern) ← findRewriteOccurrence thm symm subExpr.pos subExpr.expr
let cfg : Rewrite.Config := { occs := .pos [occurrence] }
let arg : String := Format.pretty <| ← ppExpr pattern
return s!"rw (config := {cfg}) [{if symm then "← " else "" ++ arg}]{loc.loc.render goal}"
@[server_rpc_method]
def Rewrite.rpc (props : RewriteProps) : RequestM (RequestTask Html) := do
let some loc := props.selectedLocations.back? | return .pure <p>Select a sub-expression to rewrite.</p>
let .some goal := props.goals.find? (·.mvarId == loc.mvarId) | return .pure <p>No goals found.</p>
let tacticStr : String ← goal.ctx.val.runMetaM {} do -- following `SelectInsertConv`
let md ← goal.mvarId.getDecl
let lctx := md.lctx |>.sanitizeNames.run' {options := (← getOptions)}
Meta.withLCtx lctx md.localInstances do
rewriteTacticCall loc goal props.rwRule.val props.symm
return .pure (
<DynamicEditButton
label={"Rewrite sub-term"}
range?={props.replaceRange}
insertion?={some tacticStr}
variant={"contained"}
size={"small"} />
)
@[widget_module]
def Rewrite : Component RewriteProps :=
mk_rpc_widget% Rewrite.rpc
syntax (name := rw_at) "rw" "[" rwRule "]" "at?" : tactic
@[tactic rw_at]
def rewriteAt : Tactic
| stx@`(tactic| rw [$rule] at?) => do
let .some range := (← getFileMap).rangeOfStx? stx | throwError s!"Could not find range of syntax {stx}."
let (symm, arg) :=
match rule with
| `(rwRule| $arg:term) => (false, arg)
| `(rwRule| ← $arg:term) => (true, arg)
-- | `(rwRule| <- $arg:term) => (true, arg)
| _ => panic! s!"Failed to process {rule}."
let argAbst ← abstractMVars <| ← elabTerm arg none
savePanelWidgetInfo stx ``Rewrite do
return json% {
replaceRange : $(range),
symm : $(symm),
rwRule : $(← rpcEncode (WithRpcRef.mk argAbst))
}
| _ => throwUnsupportedSyntax
section Demo
example (h : 5 + 6 = 8 + 7) : 1 + 2 = (3 + 4) + (1 + 2) := by
rw (config := { occs := .all }) [Nat.add_comm 1 2]
rw [Nat.add_comm] at? -- select the sub-expression `5 + 6`
sorry
end Demo