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
use std::fmt::{Display, Error as FmtError, Formatter};
use crate::base::{ComputeMode, Remove, Rewrite, UseForce};
use crate::hs::HaskellBool;
pub use self::goal::*;
pub use self::iotcm::*;
mod goal;
mod iotcm;
#[derive(Debug, Clone)]
pub enum Cmd {
/// Loads the module in file `path`, using
/// `flags` as the command-line options.
Load {
path: String,
flags: Vec<String>,
},
/// Compiles the module in file `path` using
/// the backend `backend`, using `flags` as the command-line options.
Compile {
backend: String,
path: String,
flags: Vec<String>,
},
Constraints,
/// Show unsolved metas. If there are no unsolved metas but
/// unsolved constraints, show those instead.
Metas,
/// Shows all the top-level names in the given module, along with
/// their types. Uses the top-level scope.
ShowModuleContentsToplevel {
rewrite: Rewrite,
search: String,
},
/// Shows all the top-level names in scope which mention all the given
/// identifiers in their type.
SearchAboutToplevel {
rewrite: Rewrite,
search: String,
},
/// Solve all goals whose values are determined by
/// the constraints.
SolveAll(Rewrite),
/// Solve the goal at point whose value is determined by
/// the constraints.
SolveOne(InputWithRewrite),
/// Solve the goal at point by using Auto.
AutoOne(GoalInput),
/// Solve all goals by using Auto.
AutoAll,
/// Parse the given expression (as if it were defined at the
// top-level of the current module) and infer its type.
InferToplevel {
/// Normalise the type?
rewrite: Rewrite,
code: String,
},
/// Parse and type check the given expression (as if it were defined
/// at the top-level of the current module) and normalise it.
ComputeToplevel {
compute_mode: ComputeMode,
code: String,
},
// Syntax highlighting
//
/// loads syntax highlighting
/// information for the module in `path`, and asks Emacs to apply
/// highlighting info from this file.
///
/// If the module does not exist, or its module name is malformed or
/// cannot be determined, or the module has not already been visited,
/// or the cached info is out of date, then no highlighting information
/// is printed.
///
/// This command is used to load syntax highlighting information when a
/// new file is opened, and it would probably be annoying if jumping to
/// the definition of an identifier reset the proof state, so this
/// command tries not to do that. One result of this is that the
/// command uses the current include directories, whatever they happen
/// to be.
LoadHighlightingInfo {
path: String,
},
/// Tells Agda to compute token-based highlighting information
/// for the file.
///
/// This command works even if the file's module name does not
/// match its location in the file system, or if the file is not
/// scope-correct. Furthermore no file names are put in the
/// generated output. Thus it is fine to put source code into a
/// temporary file before calling this command. However, the file
/// extension should be correct.
///
/// If the second argument is 'Remove', then the (presumably
/// temporary) file is removed after it has been read.
TokenHighlighting {
path: String,
remove: Remove,
},
/// Tells Agda to compute highlighting information for the expression just
/// spliced into an interaction point.
Highlight(GoalInput),
// Implicit arguments
//
/// Tells Agda whether or not to show implicit arguments.
ShowImplicitArgs(bool),
/// Toggle display of implicit arguments.
ToggleImplicitArgs,
// Goal commands
//
/// If the range is 'noRange', then the string comes from the
/// minibuffer rather than the goal.
Give {
force: UseForce,
input: GoalInput,
},
Refine(GoalInput),
Intro {
dunno: bool,
input: GoalInput,
},
RefineOrIntro {
dunno: bool,
input: GoalInput,
},
Context(InputWithRewrite),
HelperFunction(InputWithRewrite),
Infer(InputWithRewrite),
GoalType(InputWithRewrite),
/// Grabs the current goal's type and checks the expression in the hole
/// against it. Returns the elaborated term.
ElaborateGive(InputWithRewrite),
/// Displays the current goal and context.
GoalTypeContext(InputWithRewrite),
/// Displays the current goal and context **and** infers the type of an
/// expression.
GoalTypeContextInfer(InputWithRewrite),
/// Grabs the current goal's type and checks the expression in the hole
/// against it
GoalTypeContextCheck(InputWithRewrite),
/// Shows all the top-level names in the given module, along with
/// their types. Uses the scope of the given goal.
ShowModuleContents(InputWithRewrite),
MakeCase(GoalInput),
Compute {
compute_mode: ComputeMode,
input: GoalInput,
},
WhyInScope(GoalInput),
WhyInScopeToplevel(String),
/// Displays version of the running Agda
ShowVersion,
/// Abort the current computation.
/// Does nothing if no computation is in progress.
Abort,
}
impl Cmd {
pub fn load_simple(path: String) -> Self {
Cmd::Load {
path,
flags: vec![],
}
}
/// Produces [CurrentGoal](crate::resp::GoalInfo::CurrentGoal).
pub fn goal_type(input: GoalInput) -> Self {
Cmd::GoalType(From::from(input))
}
pub fn context(input: GoalInput) -> Self {
Cmd::Context(From::from(input))
}
pub fn split(input: GoalInput) -> Self {
Cmd::MakeCase(input)
}
pub fn search_module(search: String) -> Self {
Cmd::ShowModuleContentsToplevel {
rewrite: Default::default(),
search,
}
}
/// Produces [InferredType](crate::resp::GoalInfo::InferredType).
pub fn infer(input: GoalInput) -> Self {
Cmd::Infer(From::from(input))
}
pub fn give(input: GoalInput) -> Self {
Cmd::Give {
force: UseForce::WithoutForce,
input,
}
}
}
impl Display for Cmd {
fn fmt(&self, f: &mut Formatter) -> Result<(), FmtError> {
use Cmd::*;
match self {
Load { path, flags } => write!(f, "( Cmd_load {:?} {:?} )", path, flags),
Compile {
backend,
path,
flags,
} => write!(f, "( Cmd_compile {:?} {:?} {:?} )", backend, path, flags),
Constraints => f.write_str("Cmd_constraints"),
Metas => f.write_str("Cmd_metas"),
ShowModuleContentsToplevel { rewrite, search } => write!(
f,
"( Cmd_show_module_contents_toplevel {:?} {:?} )",
rewrite, search
),
SearchAboutToplevel { rewrite, search } => write!(
f,
"( Cmd_search_about_toplevel {:?} {:?} )",
rewrite, search
),
SolveAll(rewrite) => write!(f, "( Cmd_solveAll {:?} )", rewrite),
SolveOne(info) => write!(f, "( Cmd_solveOne {} )", info),
AutoOne(input) => write!(f, "( Cmd_autoOne {} )", input),
AutoAll => f.write_str("Cmd_autoAll"),
InferToplevel { rewrite, code } => {
write!(f, "( Cmd_infer_toplevel {:?} {:?} )", rewrite, code)
}
ComputeToplevel { compute_mode, code } => {
write!(f, "( Cmd_compute_toplevel {:?} {:?} )", compute_mode, code)
}
LoadHighlightingInfo { path } => write!(f, "( Cmd_load_highlighting_info {:?} )", path),
TokenHighlighting { path, remove } => {
write!(f, "( Cmd_tokenHighlighting {:?} {:?} ", path, remove)
}
Highlight(input) => write!(f, "( Cmd_highlight {} )", input),
ShowImplicitArgs(show) => {
write!(f, "( ShowImplicitArgs {:?} )", HaskellBool::from(*show))
}
ToggleImplicitArgs => f.write_str("ToggleImplicitArgs"),
Give { force, input } => write!(f, "( Cmd_give {:?} {} )", force, input),
Refine(input) => write!(f, "( Cmd_refine {} )", input),
Intro { dunno, input } => {
write!(f, "( Cmd_intro {:?} {} )", HaskellBool::from(*dunno), input)
}
RefineOrIntro { dunno, input } => write!(
f,
"( Cmd_refine_or_intro {:?} {} )",
HaskellBool::from(*dunno),
input
),
Context(info) => write!(f, "( Cmd_context {} )", info),
HelperFunction(info) => write!(f, "( Cmd_helper_function {} )", info),
Infer(info) => write!(f, "( Cmd_infer {} )", info),
GoalType(info) => write!(f, "( Cmd_goal_type {} )", info),
ElaborateGive(info) => write!(f, "( Cmd_elaborate_give {} )", info),
GoalTypeContext(info) => write!(f, "( Cmd_goal_type_context {} )", info),
GoalTypeContextInfer(info) => write!(f, "( Cmd_goal_type_context_infer {} )", info),
GoalTypeContextCheck(info) => write!(f, "( Cmd_goal_type_context_check {} )", info),
ShowModuleContents(info) => write!(f, "( Cmd_show_module_contents {} )", info),
MakeCase(input) => write!(f, "( Cmd_make_case {} )", input),
Compute {
compute_mode,
input,
} => write!(f, "( Cmd_compute {:?} {} )", compute_mode, input),
WhyInScope(input) => write!(f, "( Cmd_why_in_scope {} )", input),
WhyInScopeToplevel(name) => write!(f, "( Cmd_why_in_scope_toplevel {:?} )", name),
ShowVersion => f.write_str("Cmd_show_version"),
Abort => f.write_str("Cmd_abort"),
}
}
}