tactic_component.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
namespace widget
/-- A component that implicitly depends on tactic_state. For efficiency we always assume that the tactic_state is unchanged between component renderings. -/
meta def tc (π : Type) (α : Type) := component (tactic_state × π) (α)
namespace tc
variables {π ρ α β : Type}
meta def of_component : component π α → tc π α :=
component.map_props prod.snd
meta def map_action (f : α → β) : tc π α → tc π β :=
component.map_action f
meta def map_props (f : π → ρ) : tc ρ α → tc π α :=
component.map_props (prod.map id f)
open interaction_monad
open interaction_monad.result
/-- Make a tactic component from some init, update, views which are expecting a tactic.
The tactic_state never mutates.
-/
meta def mk_simple
[decidable_eq π]
(β σ : Type)
(init : π → tactic σ)
(update : π → σ → β → tactic (σ × option α))
(view : π → σ → tactic (list (html β)))
: tc π α :=
component.with_should_update (λ ⟨_,old_p⟩ ⟨_,new_p⟩, old_p ≠ new_p)
$ @component.stateful
(tactic_state × π)
α
β
(interaction_monad.result tactic_state σ)
(λ ⟨ts,p⟩ last,
match last with
| (some x) := x
| none := init p ts
end)
(λ ⟨ts,p⟩ s b,
match s with
| (success s _) :=
match update p s b ts with
| (success ⟨s,a⟩ _) := prod.mk (success s ts) (a)
| (exception m p ts') := prod.mk (exception m p ts') none
end
| x := ⟨x,none⟩
end
)
(λ ⟨ts,p⟩ s,
match s with
| (success s _) :=
match view p s ts with
| (success h _) := h
| (exception msg pos s) := ["rendering tactic failed "]
end
| (exception msg pos s) := ["state of tactic component has failed!"]
end
)
meta def stateless [decidable_eq π] (view : π → tactic (list (html α))) : tc π α :=
tc.mk_simple α unit (λ p, pure ()) (λ _ _ b, pure ((),some b)) (λ p _, view p)
meta def to_html : tc π α → π → tactic (html α)
| c p ts := success (html.of_component (ts,p) c) ts
meta def to_component : tc unit α → component tactic_state α
| c := component.map_props (λ tc, (tc,())) c
meta instance cfn : has_coe_to_fun (tc π α) := ⟨λ x, π → tactic (html α), to_html⟩
end tc
end widget