-
Notifications
You must be signed in to change notification settings - Fork 80
/
my_tac_class.lean
68 lines (54 loc) · 1.81 KB
/
my_tac_class.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
meta def mytac :=
state_t nat tactic
section
local attribute [reducible] mytac
meta instance : monad mytac := by apply_instance
meta instance : monad_state nat mytac := by apply_instance
meta instance : has_monad_lift tactic mytac := by apply_instance
end
meta instance (α : Type) : has_coe (tactic α) (mytac α) :=
⟨monad_lift⟩
namespace mytac
meta def step {α : Type} (t : mytac α) : mytac unit :=
t >> return ()
meta def istep {α : Type} (line0 col0 line col : nat) (t : mytac α) : mytac unit :=
⟨λ v s, result.cases_on (@scope_trace _ line col (λ_, t.run v s))
(λ ⟨a, v⟩ new_s, result.success ((), v) new_s)
(λ opt_msg_thunk e new_s,
match opt_msg_thunk with
| some msg_thunk :=
let msg := λ _ : unit, msg_thunk () ++ format.line ++ to_fmt "value: " ++ to_fmt v ++ format.line ++ to_fmt "state:" ++ format.line ++ new_s^.to_format in
interaction_monad.result.exception (some msg) (some ⟨line, col⟩) new_s
| none := interaction_monad.silent_fail new_s
end)⟩
meta instance : interactive.executor mytac :=
{ config_type := unit, execute_with := λ _ tac, tac.run 0 >> return () }
meta def save_info (p : pos) : mytac unit :=
do v ← get,
s ← tactic.read,
tactic.save_info_thunk p
(λ _, to_fmt "Custom state: " ++ to_fmt v ++ format.line ++
tactic_state.to_format s)
namespace interactive
meta def intros : mytac unit :=
tactic.intros >> return ()
meta def constructor : mytac unit :=
tactic.constructor >> return ()
meta def trace (s : string) : mytac unit :=
tactic.trace s
meta def assumption : mytac unit :=
tactic.assumption
meta def inc : mytac punit :=
modify (+1)
end interactive
end mytac
example (p q : Prop) : p → q → p ∧ q :=
begin [mytac]
intros,
inc,
trace "test",
constructor,
inc,
assumption,
assumption
end