-
Notifications
You must be signed in to change notification settings - Fork 80
/
hole_command.lean
64 lines (57 loc) · 1.93 KB
/
hole_command.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
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.meta.tactic
/--
The front-end (e.g., Emacs, VS Code) can invoke commands for holes `{! ... !}` in
a declaration. A command is a tactic that takes zero or more pre-terms in the
hole, and returns a list of pair (s, descr) where 's' is a substitution and 'descr' is
a short explanation for the substitution.
Each string 's' represents a different way to fill the hole.
The front-end is responsible for replacing the hole with the string/alternative selected by the user.
This infra-structure can be use to implement auto-fill and/or refine commands.
An action may return an empty list. This is useful for actions that just return
information such as: the type of an expression, its normal form, etc.
-/
meta structure hole_command :=
(name : string)
(descr : string)
(action : list pexpr → tactic (list (string × string)))
open tactic
@[hole_command]
meta def infer_type_cmd : hole_command :=
{ name := "Infer",
descr := "Infer type of the expression in the hole",
action := λ ps, do
[p] ← return ps | fail "Infer command failed, the hole must contain a single term",
e ← to_expr p,
t ← infer_type e,
trace t,
return []
}
@[hole_command]
meta def show_goal_cmd : hole_command :=
{ name := "Show",
descr := "Show the current goal",
action := λ _, do
trace_state,
return []
}
@[hole_command]
meta def use_cmd : hole_command :=
{ name := "Use",
descr := "Try to fill the hole using the given argument",
action := λ ps, do
[p] ← return ps | fail "Use command failed, the hole must contain a single term",
t ← target,
e ← to_expr ``(%%p : %%t),
ty ← infer_type e,
is_def_eq t ty,
fmt ← tactic_format_expr e,
o ← get_options,
let s := fmt.to_string o,
return [(s, "")]
}