agda_mode/cmd/
mod.rs

1use std::fmt::{Display, Error as FmtError, Formatter};
2
3use crate::base::{ComputeMode, Remove, Rewrite, UseForce};
4use crate::hs::HaskellBool;
5
6pub use self::goal::*;
7pub use self::iotcm::*;
8
9mod goal;
10mod iotcm;
11
12#[derive(Debug, Clone)]
13pub enum Cmd {
14    /// Loads the module in file `path`, using
15    /// `flags` as the command-line options.
16    Load {
17        path: String,
18        flags: Vec<String>,
19    },
20    /// Compiles the module in file `path` using
21    /// the backend `backend`, using `flags` as the command-line options.
22    Compile {
23        backend: String,
24        path: String,
25        flags: Vec<String>,
26    },
27    Constraints,
28    /// Show unsolved metas. If there are no unsolved metas but
29    /// unsolved constraints, show those instead.
30    Metas,
31    /// Shows all the top-level names in the given module, along with
32    /// their types. Uses the top-level scope.
33    ShowModuleContentsToplevel {
34        rewrite: Rewrite,
35        search: String,
36    },
37    /// Shows all the top-level names in scope which mention all the given
38    /// identifiers in their type.
39    SearchAboutToplevel {
40        rewrite: Rewrite,
41        search: String,
42    },
43    /// Solve all goals whose values are determined by
44    /// the constraints.
45    SolveAll(Rewrite),
46    /// Solve the goal at point whose value is determined by
47    /// the constraints.
48    SolveOne(InputWithRewrite),
49    /// Solve the goal at point by using Auto.
50    AutoOne(GoalInput),
51    /// Solve all goals by using Auto.
52    AutoAll,
53    /// Parse the given expression (as if it were defined at the
54    // top-level of the current module) and infer its type.
55    InferToplevel {
56        /// Normalise the type?
57        rewrite: Rewrite,
58        code: String,
59    },
60    /// Parse and type check the given expression (as if it were defined
61    /// at the top-level of the current module) and normalise it.
62    ComputeToplevel {
63        compute_mode: ComputeMode,
64        code: String,
65    },
66
67    // Syntax highlighting
68    //
69    /// loads syntax highlighting
70    /// information for the module in `path`, and asks Emacs to apply
71    /// highlighting info from this file.
72    ///
73    /// If the module does not exist, or its module name is malformed or
74    /// cannot be determined, or the module has not already been visited,
75    /// or the cached info is out of date, then no highlighting information
76    /// is printed.
77    ///
78    /// This command is used to load syntax highlighting information when a
79    /// new file is opened, and it would probably be annoying if jumping to
80    /// the definition of an identifier reset the proof state, so this
81    /// command tries not to do that. One result of this is that the
82    /// command uses the current include directories, whatever they happen
83    /// to be.
84    LoadHighlightingInfo {
85        path: String,
86    },
87    /// Tells Agda to compute token-based highlighting information
88    /// for the file.
89    ///
90    /// This command works even if the file's module name does not
91    /// match its location in the file system, or if the file is not
92    /// scope-correct. Furthermore no file names are put in the
93    /// generated output. Thus it is fine to put source code into a
94    /// temporary file before calling this command. However, the file
95    /// extension should be correct.
96    ///
97    /// If the second argument is 'Remove', then the (presumably
98    /// temporary) file is removed after it has been read.
99    TokenHighlighting {
100        path: String,
101        remove: Remove,
102    },
103    /// Tells Agda to compute highlighting information for the expression just
104    /// spliced into an interaction point.
105    Highlight(GoalInput),
106    // Implicit arguments
107    //
108    /// Tells Agda whether or not to show implicit arguments.
109    ShowImplicitArgs(bool),
110    /// Toggle display of implicit arguments.
111    ToggleImplicitArgs,
112    // Goal commands
113    //
114    /// If the range is 'noRange', then the string comes from the
115    /// minibuffer rather than the goal.
116    Give {
117        force: UseForce,
118        input: GoalInput,
119    },
120    Refine(GoalInput),
121    Intro {
122        dunno: bool,
123        input: GoalInput,
124    },
125    RefineOrIntro {
126        dunno: bool,
127        input: GoalInput,
128    },
129    Context(InputWithRewrite),
130    HelperFunction(InputWithRewrite),
131    Infer(InputWithRewrite),
132    GoalType(InputWithRewrite),
133    /// Grabs the current goal's type and checks the expression in the hole
134    /// against it. Returns the elaborated term.
135    ElaborateGive(InputWithRewrite),
136    /// Displays the current goal and context.
137    GoalTypeContext(InputWithRewrite),
138    /// Displays the current goal and context **and** infers the type of an
139    /// expression.
140    GoalTypeContextInfer(InputWithRewrite),
141    /// Grabs the current goal's type and checks the expression in the hole
142    /// against it
143    GoalTypeContextCheck(InputWithRewrite),
144    /// Shows all the top-level names in the given module, along with
145    /// their types. Uses the scope of the given goal.
146    ShowModuleContents(InputWithRewrite),
147    MakeCase(GoalInput),
148    Compute {
149        compute_mode: ComputeMode,
150        input: GoalInput,
151    },
152    WhyInScope(GoalInput),
153    WhyInScopeToplevel(String),
154    /// Displays version of the running Agda
155    ShowVersion,
156    /// Abort the current computation.
157    /// Does nothing if no computation is in progress.
158    Abort,
159}
160
161impl Cmd {
162    pub fn load_simple(path: String) -> Self {
163        Cmd::Load {
164            path,
165            flags: vec![],
166        }
167    }
168
169    /// Produces [CurrentGoal](crate::resp::GoalInfo::CurrentGoal).
170    pub fn goal_type(input: GoalInput) -> Self {
171        Cmd::GoalType(From::from(input))
172    }
173
174    pub fn context(input: GoalInput) -> Self {
175        Cmd::Context(From::from(input))
176    }
177
178    pub fn split(input: GoalInput) -> Self {
179        Cmd::MakeCase(input)
180    }
181
182    pub fn search_module(search: String) -> Self {
183        Cmd::ShowModuleContentsToplevel {
184            rewrite: Default::default(),
185            search,
186        }
187    }
188
189    /// Produces [InferredType](crate::resp::GoalInfo::InferredType).
190    pub fn infer(input: GoalInput) -> Self {
191        Cmd::Infer(From::from(input))
192    }
193
194    pub fn give(input: GoalInput) -> Self {
195        Cmd::Give {
196            force: UseForce::WithoutForce,
197            input,
198        }
199    }
200}
201
202impl Display for Cmd {
203    fn fmt(&self, f: &mut Formatter) -> Result<(), FmtError> {
204        use Cmd::*;
205        match self {
206            Load { path, flags } => write!(f, "( Cmd_load {:?} {:?} )", path, flags),
207            Compile {
208                backend,
209                path,
210                flags,
211            } => write!(f, "( Cmd_compile {:?} {:?} {:?} )", backend, path, flags),
212            Constraints => f.write_str("Cmd_constraints"),
213            Metas => f.write_str("Cmd_metas"),
214            ShowModuleContentsToplevel { rewrite, search } => write!(
215                f,
216                "( Cmd_show_module_contents_toplevel {:?} {:?} )",
217                rewrite, search
218            ),
219            SearchAboutToplevel { rewrite, search } => write!(
220                f,
221                "( Cmd_search_about_toplevel {:?} {:?} )",
222                rewrite, search
223            ),
224            SolveAll(rewrite) => write!(f, "( Cmd_solveAll {:?} )", rewrite),
225            SolveOne(info) => write!(f, "( Cmd_solveOne {} )", info),
226            AutoOne(input) => write!(f, "( Cmd_autoOne {} )", input),
227            AutoAll => f.write_str("Cmd_autoAll"),
228            InferToplevel { rewrite, code } => {
229                write!(f, "( Cmd_infer_toplevel {:?} {:?} )", rewrite, code)
230            }
231            ComputeToplevel { compute_mode, code } => {
232                write!(f, "( Cmd_compute_toplevel {:?} {:?} )", compute_mode, code)
233            }
234            LoadHighlightingInfo { path } => write!(f, "( Cmd_load_highlighting_info {:?} )", path),
235            TokenHighlighting { path, remove } => {
236                write!(f, "( Cmd_tokenHighlighting {:?} {:?} ", path, remove)
237            }
238            Highlight(input) => write!(f, "( Cmd_highlight {} )", input),
239            ShowImplicitArgs(show) => {
240                write!(f, "( ShowImplicitArgs {:?} )", HaskellBool::from(*show))
241            }
242            ToggleImplicitArgs => f.write_str("ToggleImplicitArgs"),
243            Give { force, input } => write!(f, "( Cmd_give {:?} {} )", force, input),
244            Refine(input) => write!(f, "( Cmd_refine {} )", input),
245            Intro { dunno, input } => {
246                write!(f, "( Cmd_intro {:?} {} )", HaskellBool::from(*dunno), input)
247            }
248            RefineOrIntro { dunno, input } => write!(
249                f,
250                "( Cmd_refine_or_intro {:?} {} )",
251                HaskellBool::from(*dunno),
252                input
253            ),
254            Context(info) => write!(f, "( Cmd_context {} )", info),
255            HelperFunction(info) => write!(f, "( Cmd_helper_function {} )", info),
256            Infer(info) => write!(f, "( Cmd_infer {} )", info),
257            GoalType(info) => write!(f, "( Cmd_goal_type {} )", info),
258            ElaborateGive(info) => write!(f, "( Cmd_elaborate_give {} )", info),
259            GoalTypeContext(info) => write!(f, "( Cmd_goal_type_context {} )", info),
260            GoalTypeContextInfer(info) => write!(f, "( Cmd_goal_type_context_infer {} )", info),
261            GoalTypeContextCheck(info) => write!(f, "( Cmd_goal_type_context_check {} )", info),
262            ShowModuleContents(info) => write!(f, "( Cmd_show_module_contents {} )", info),
263            MakeCase(input) => write!(f, "( Cmd_make_case {} )", input),
264            Compute {
265                compute_mode,
266                input,
267            } => write!(f, "( Cmd_compute {:?} {} )", compute_mode, input),
268            WhyInScope(input) => write!(f, "( Cmd_why_in_scope {} )", input),
269            WhyInScopeToplevel(name) => write!(f, "( Cmd_why_in_scope_toplevel {:?} )", name),
270            ShowVersion => f.write_str("Cmd_show_version"),
271            Abort => f.write_str("Cmd_abort"),
272        }
273    }
274}
agda_mode/cmd/mod.rs

agda_mode/cmd/
mod.rs
