/
interactive_expr.lean
294 lines (257 loc) · 10.5 KB
/
interactive_expr.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
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
/-
Copyright (c) E.W.Ayers. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: E.W.Ayers
-/
prelude
import init.meta.widget.basic
import init.meta.widget.tactic_component
import init.meta.tagged_format
import init.data.punit
import init.meta.mk_dec_eq_instance
meta def subexpr := (expr × expr.address)
namespace widget
open tagged_format
open html attr
namespace interactive_expression
/-- eformat but without any of the formatting stuff like highlighting, groups etc. -/
meta inductive sf : Type
| tag_expr : expr.address → expr → sf → sf
| compose : sf → sf → sf
| of_string : string → sf
meta def sf.repr : sf → format
| (sf.tag_expr addr e a) := format.group $ format.nest 2 $
"(tag_expr " ++ to_fmt addr ++ format.line ++
"`(" ++ to_fmt e ++ ")" ++ format.line ++ a.repr ++ ")"
| (sf.compose a b) := a.repr ++ format.line ++ b.repr
| (sf.of_string s) := repr s
meta instance : has_to_format sf := ⟨sf.repr⟩
meta instance : has_to_string sf := ⟨λ s, s.repr.to_string⟩
meta instance : has_repr sf := ⟨λ s, s.repr.to_string⟩
meta def sf.of_eformat : eformat → sf
| (tag ⟨ea,e⟩ m) := sf.tag_expr ea e $ sf.of_eformat m
| (group m) := sf.of_eformat m
| (nest i m) := sf.of_eformat m
| (highlight i m) := sf.of_eformat m
| (of_format f) := sf.of_string $ format.to_string f
| (compose x y) := sf.compose (sf.of_eformat x) (sf.of_eformat y)
meta def sf.flatten : sf → sf
| (sf.tag_expr e ea m) := (sf.tag_expr e ea $ sf.flatten m)
| (sf.compose x y) :=
match (sf.flatten x), (sf.flatten y) with
| (sf.of_string sx), (sf.of_string sy) := sf.of_string (sx ++ sy)
| (sf.of_string sx), (sf.compose (sf.of_string sy) z) := sf.compose (sf.of_string (sx ++ sy)) z
| (sf.compose x (sf.of_string sy)), (sf.of_string sz) := sf.compose x (sf.of_string (sy ++ sz))
| (sf.compose x (sf.of_string sy1)), (sf.compose (sf.of_string sy2) z) := sf.compose x (sf.compose (sf.of_string (sy1 ++ sy2)) z)
| x, y := sf.compose x y
end
| (sf.of_string s) := sf.of_string s
meta inductive action (γ : Type)
| on_mouse_enter : subexpr → action
| on_mouse_leave_all : action
| on_click : subexpr → action
| on_tooltip_action : γ → action
| on_close_tooltip : action
meta def view {γ} (tooltip_component : tc subexpr (action γ)) (click_address : option expr.address) (select_address : option expr.address) :
subexpr → sf → tactic (list (html (action γ)))
| ⟨ce, current_address⟩ (sf.tag_expr ea e m) := do
let new_address := current_address ++ ea,
let select_attrs : list (attr (action γ)) := if some new_address = select_address then [className "highlight"] else [],
click_attrs : list (attr (action γ)) ←
if some new_address = click_address then do
content ← tc.to_html tooltip_component (e, new_address),
pure [tooltip $ h "div" [] [
h "button" [cn "fr pointer ba br3", on_click (λ _, action.on_close_tooltip)] ["x"],
content
]]
else pure [],
let as := [className "expr-boundary", key (ea)] ++ select_attrs ++ click_attrs,
inner ← view (e,new_address) m,
pure [h "span" as inner]
| ca (sf.compose x y) := pure (++) <*> view ca x <*> view ca y
| ca (sf.of_string s) := pure
[h "span" [
on_mouse_enter (λ _, action.on_mouse_enter ca),
on_click (λ _, action.on_click ca),
key s
] [html.of_string s]]
/-- Make an interactive expression. -/
meta def mk {γ} (tooltip : tc subexpr γ) : tc expr γ :=
let tooltip_comp :=
component.with_should_update (λ (x y : tactic_state × expr × expr.address), x.2.2 ≠ y.2.2)
$ component.map_action (action.on_tooltip_action) tooltip in
tc.mk_simple
(action γ)
(option subexpr × option subexpr)
(λ e, pure $ (none, none))
(λ e ⟨ca, sa⟩ act, pure $
match act with
| (action.on_mouse_enter ⟨e, ea⟩) := ((ca, some (e, ea)), none)
| (action.on_mouse_leave_all) := ((ca, none), none)
| (action.on_click ⟨e, ea⟩) := if some (e,ea) = ca then ((none, sa), none) else ((some (e, ea), sa), none)
| (action.on_tooltip_action g) := ((none, sa), some g)
| (action.on_close_tooltip) := ((none, sa), none)
end
)
(λ e ⟨ca, sa⟩, do
ts ← tactic.read,
let m : sf := sf.flatten $ sf.of_eformat $ tactic_state.pp_tagged ts e,
let m : sf := sf.tag_expr [] e m, -- [hack] in pp.cpp I forgot to add an expr-boundary for the root expression.
v ← view tooltip_comp (prod.snd <$> ca) (prod.snd <$> sa) ⟨e, []⟩ m,
pure $
[ h "span" [
className "expr",
key e.hash,
on_mouse_leave (λ _, action.on_mouse_leave_all) ] $ v
]
)
/-- Render the implicit arguments for an expression in fancy, little pills. -/
meta def implicit_arg_list (tooltip : tc subexpr empty) (e : expr) : tactic $ html empty := do
fn ← (mk tooltip) $ expr.get_app_fn e,
args ← list.mmap (mk tooltip) $ expr.get_app_args e,
pure $ h "div" []
( (h "span" [className "bg-blue br3 ma1 ph2 white"] [fn]) ::
list.map (λ a, h "span" [className "bg-gray br3 ma1 ph2 white"] [a]) args
)
meta def type_tooltip : tc subexpr empty :=
tc.stateless (λ ⟨e,ea⟩, do
y ← tactic.infer_type e,
y_comp ← mk type_tooltip y,
implicit_args ← implicit_arg_list type_tooltip e,
pure [
h "div" [] [
h "div" [] [y_comp],
h "hr" [] [],
implicit_args
]
]
)
end interactive_expression
@[derive decidable_eq]
meta inductive filter_type
| none
| no_instances
| only_props
meta def filter_local : filter_type → expr → tactic bool
| (filter_type.none) e := pure tt
| (filter_type.no_instances) e := do
t ← tactic.infer_type e,
bnot <$> tactic.is_class t
| (filter_type.only_props) e := do
t ← tactic.infer_type e,
tactic.is_prop t
meta def filter_component : component filter_type filter_type :=
component.stateless (λ lf,
[ h "label" [] ["filter: "],
select [
⟨filter_type.none, "0", ["no filter"]⟩,
⟨filter_type.no_instances, "1", ["no instances"]⟩,
⟨filter_type.only_props, "2", ["only props"]⟩
] lf
]
)
meta def html.of_name {α : Type} : name → html α
| n := html.of_string $ name.to_string n
open tactic
meta def show_type_component : tc expr empty :=
tc.stateless (λ x, do
y ← infer_type x,
y_comp ← interactive_expression.mk interactive_expression.type_tooltip $ y,
pure y_comp
)
/-- A group of local constants in the context that should be rendered as one line. -/
@[derive decidable_eq]
meta structure local_collection :=
(key : string)
(locals : list expr)
(type : expr)
/-- Group consecutive locals according to whether they have the same type -/
meta def to_local_collection : list local_collection → list expr → tactic (list local_collection)
| acc [] := pure $ list.map (λ lc : local_collection, {locals := lc.locals.reverse, ..lc}) $ list.reverse $ acc
| acc (l::ls) := do
l_type ← infer_type l,
(do (⟨k,ns,t⟩::acc) ← pure acc,
is_def_eq t l_type,
to_local_collection (⟨k,l::ns,t⟩::acc) ls)
<|> (to_local_collection (⟨to_string $ expr.local_uniq_name $ l, [l], l_type⟩::acc) ls)
/-- Component that displays the main (first) goal. -/
meta def tactic_view_goal {γ} (local_c : tc local_collection γ) (target_c : tc expr γ) : tc filter_type γ :=
tc.stateless $ λ ft, do
g@(expr.mvar u_n pp_n y) ← main_goal,
t ← get_tag g,
let case_tag : list (html γ) :=
match interactive.case_tag.parse t with
| some t :=
[h "li" [key "_case"] $ [h "span" [cn "goal-case b"] ["case"]] ++
(t.case_names.bind $ λ n, [" ", n])]
| none := []
end,
lcs ← local_context,
lcs ← list.mfilter (filter_local ft) lcs,
lcs ← to_local_collection [] lcs,
lchs ← lcs.mmap (λ lc, do
lh ← local_c lc,
ns ← pure $ lc.locals.map (λ n, h "span" [cn "goal-hyp b pr2"] [html.of_name $ expr.local_pp_name n]),
pure $ h "li" [key lc.key] (ns ++ [": ", h "span" [cn "goal-hyp-type"] [lh]])),
t_comp ← target_c g,
pure $ h "ul" [key g.hash, className "list pl0 font-code"] $ case_tag ++ lchs ++ [
h "li" [key u_n] [
h "span" [cn "goal-vdash b"] ["⊢ "],
t_comp
]]
meta inductive tactic_view_action (γ : Type)
| out (a:γ): tactic_view_action
| filter (f: filter_type): tactic_view_action
/-- Component that displays all goals, together with the `$n goals` message. -/
meta def tactic_view_component {γ} (local_c : tc local_collection γ) (target_c : tc expr γ) : tc unit γ :=
tc.mk_simple
(tactic_view_action γ)
(filter_type)
(λ _, pure $ filter_type.none)
(λ ⟨⟩ ft a, match a with
| (tactic_view_action.out a) := pure (ft, some a)
| (tactic_view_action.filter ft) := pure (ft, none)
end)
(λ ⟨⟩ ft, do
gs ← get_goals,
hs ← gs.mmap (λ g, do set_goals [g], flip tc.to_html ft $ tactic_view_goal local_c target_c),
set_goals gs,
let goal_message :=
if gs.length = 0 then
"goals accomplished"
else if gs.length = 1 then
"1 goal"
else
to_string gs.length ++ " goals",
let goal_message : html γ := h "strong" [cn "goal-goals"] [goal_message],
let goals : html γ := h "ul" [className "list pl0"]
$ list.map_with_index (λ i x,
h "li" [className $ "lh-copy mt2", key i] [x])
$ (goal_message :: hs),
pure [
h "div" [className "fr"] [html.of_component ft $ component.map_action tactic_view_action.filter filter_component],
html.map_action tactic_view_action.out goals
])
/-- Component that displays the term-mode goal. -/
meta def tactic_view_term_goal {γ} (local_c : tc local_collection γ) (target_c : tc expr γ) : tc unit γ :=
tc.stateless $ λ _, do
goal ← flip tc.to_html (filter_type.none) $ tactic_view_goal local_c target_c,
pure [h "ul" [className "list pl0"] [
h "li" [className "lh-copy"] [h "strong" [cn "goal-goals"] ["expected type:"]],
h "li" [className "lh-copy"] [goal]]]
meta def show_local_collection_component : tc local_collection empty :=
tc.stateless (λ lc, do
(l::_) ← pure lc.locals,
c ← show_type_component l,
pure [c]
)
meta def tactic_render : tc unit empty :=
component.ignore_action $ tactic_view_component show_local_collection_component show_type_component
meta def tactic_state_widget : component tactic_state empty :=
tc.to_component tactic_render
/--
Widget used to display term-proof goals.
-/
meta def term_goal_widget : component tactic_state empty :=
(tactic_view_term_goal show_local_collection_component show_type_component).to_component
end widget