interactive_expr.lean
/-
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
