agda_mode/agda/
repl.rs

1use std::io;
2
3use tokio::io::AsyncWriteExt;
4use tokio::process::ChildStdin;
5
6use crate::cmd::{Cmd, IOTCM};
7use crate::pos::InteractionPoint;
8use crate::resp::{AgdaError, DisplayInfo, Resp};
9
10use super::{send_command, AgdaRead};
11
12/// Simple REPL state wrapper.
13pub struct ReplState {
14    pub stdin: ChildStdin,
15    pub agda: AgdaRead,
16    pub file: String,
17    pub(super) interaction_points: Vec<InteractionPoint>,
18    pub(super) iotcm: IOTCM,
19}
20
21/// An Agda response that is either something good or some error.
22pub type AgdaResult<T> = Result<T, String>;
23/// Return type of `next_*` functions.
24pub type NextResult<T> = io::Result<AgdaResult<T>>;
25
26pub fn preprint_agda_result<T>(t: AgdaResult<T>) -> Option<T> {
27    t.map_err(|e| eprintln!("Errors:\n{}", e)).ok()
28}
29
30impl ReplState {
31    /// Print all goals.
32    pub fn print_goal_list(&self) {
33        let ips = self.interaction_points();
34        if ips.is_empty() {
35            println!("No goals, you're all set.");
36        }
37        for interaction_point in ips {
38            // This shouldn't fail
39            let range = &interaction_point.range;
40            debug_assert_eq!(range.len(), 1);
41            let interval = &range[0];
42            println!("?{} at line {}", interaction_point.id, interval.start.line)
43        }
44    }
45
46    pub async fn reload_file(&mut self) -> io::Result<()> {
47        self.command(Cmd::load_simple(self.file.clone())).await
48    }
49
50    pub async fn command(&mut self, cmd: Cmd) -> io::Result<()> {
51        self.iotcm.command = cmd;
52        send_command(&mut self.stdin, &self.iotcm).await
53    }
54
55    pub async fn command_raw(&mut self, raw_command: &str) -> io::Result<()> {
56        self.stdin.write(raw_command.as_bytes()).await?;
57        self.stdin.flush().await
58    }
59
60    pub async fn shutdown(&mut self) -> io::Result<()> {
61        self.stdin.shutdown().await
62    }
63
64    /// Skip information until the next display info.
65    pub async fn next_display_info(&mut self) -> io::Result<DisplayInfo> {
66        loop {
67            match self.response().await? {
68                Resp::DisplayInfo { info: Some(info) } => break Ok(info),
69                _ => {}
70            }
71        }
72    }
73
74    /// Returns the latest [`next_goals`](Self::next_goals) result.
75    pub fn interaction_points(&self) -> &[InteractionPoint] {
76        &self.interaction_points
77    }
78
79    /// Skip information until the next interaction point (goal) list.
80    /// The result can be queried via [`interaction_points`](Self::interaction_points).
81    ///
82    /// # Note
83    ///
84    /// This information normally comes right after `all_goals_warnings`,
85    /// and when you call [`next_all_goals_warnings`](Self::next_all_goals_warnings),
86    /// you've already eliminated errors.
87    /// Therefore this method don't deal with errors.
88    pub async fn next_goals(&mut self) -> io::Result<()> {
89        use Resp::*;
90        self.interaction_points = loop {
91            match self.response().await? {
92                InteractionPoints { interaction_points } => break interaction_points,
93                _ => {}
94            }
95        };
96        Ok(())
97    }
98
99    /// Skip information until an error.
100    pub async fn next_error(&mut self) -> io::Result<AgdaError> {
101        use crate::resp::DisplayInfo::Error as DisError;
102        loop {
103            match self.next_display_info().await? {
104                DisError(e) => break Ok(e),
105                _ => {}
106            }
107        }
108    }
109}
110
111macro_rules! next_resp_of {
112    ($f:ident, $p:ident, $d:literal) => {
113        next_resp_of!($f, $p, crate::resp::$p, $d);
114    };
115
116    ($f:ident, $p:ident, $t:ty, $d:literal) => {
117        impl ReplState {
118            #[doc($d)]
119            pub async fn $f(&mut self) -> NextResult<$t> {
120                loop {
121                    match self.response().await? {
122                        Resp::$p(ga) => break Ok(Ok(ga)),
123                        Resp::DisplayInfo {
124                            info: Some(crate::resp::DisplayInfo::Error(e)),
125                        } => break Ok(e.into()),
126                        _ => {}
127                    }
128                }
129            }
130        }
131    };
132}
133
134next_resp_of!(next_give_action, GiveAction, "Skip until next give-action.");
135next_resp_of!(next_make_case, MakeCase, "Skip until next make-case.");
136next_resp_of!(
137    next_highlight,
138    HighlightingInfo,
139    "Skip until next highlight."
140);
141
142macro_rules! next_disp_of {
143    ($f:ident, $p:ident, $d:literal) => {
144        next_disp_of!($f, $p, crate::resp::$p, $d);
145    };
146
147    ($f:ident, $p:ident, $t:ty, $d:literal) => {
148        impl ReplState {
149            #[doc($d)]
150            pub async fn $f(&mut self) -> NextResult<$t> {
151                loop {
152                    match self.next_display_info().await? {
153                        DisplayInfo::Error(e) => break Ok(e.into()),
154                        DisplayInfo::$p(agw) => break Ok(Ok(agw)),
155                        _ => {}
156                    }
157                }
158            }
159        }
160    };
161}
162
163next_disp_of!(
164    next_all_goals_warnings,
165    AllGoalsWarnings,
166    "Skip until next interaction point (goal) list."
167);
168next_disp_of!(
169    next_goal_specific,
170    GoalSpecific,
171    "Skip until next goal specific information."
172);
173next_disp_of!(
174    next_module_contents,
175    ModuleContents,
176    "Skip until next module contents response."
177);
178next_disp_of!(next_normal_form, NormalForm, "Skip until next normal form.");
179next_disp_of!(next_context, Context, "Skip until next context.");
180next_disp_of!(
181    next_inferred_type,
182    InferredType,
183    "Skip until next inferred type."
184);
agda_mode/agda/repl.rs

agda_mode/agda/
repl.rs
