agda_mode/agda/
mod.rs

1use std::io;
2use std::process::Stdio;
3
4use tokio::io::{AsyncWriteExt, BufReader};
5use tokio::process::{Child, ChildStdin, ChildStdout, Command};
6
7use crate::cmd::{Cmd, IOTCM};
8use crate::debug::debug_command;
9
10pub use self::read::*;
11pub use self::repl::*;
12
13/// Agda message reading.
14mod read;
15/// Repl state wrapper.
16mod repl;
17/// Verify whether Agda is working.
18pub mod verify;
19
20pub const INTERACTION_COMMAND: &str = "--interaction-json";
21pub const START_FAIL: &str = "Failed to start Agda";
22
23pub struct ProcessStdio(pub Child, pub JustStdio);
24
25pub struct JustStdio(pub ChildStdin, pub ChildStdout);
26
27pub fn init_agda_process(agda_program: &str) -> io::Result<ProcessStdio> {
28    let mut process = Command::new(agda_program)
29        .arg(INTERACTION_COMMAND)
30        .stdout(Stdio::piped())
31        .stdin(Stdio::piped())
32        .spawn()?; // cannot spawn
33    let stdin = process.stdin.take().expect("Failed to pipe stdin");
34    let stdout = process.stdout.take().expect("Failed to pipe stdout");
35    // The above two should not panic, because both stdio are piped
36    Ok(ProcessStdio(process, JustStdio(stdin, stdout)))
37}
38
39impl ReplState {
40    pub async fn start(agda_program: &str, file: String) -> io::Result<Self> {
41        let JustStdio(stdin, out) = start_agda(agda_program);
42        Self::from_io(stdin, BufReader::new(out), file).await
43    }
44
45    pub async fn from_io(
46        mut stdin: ChildStdin,
47        stdout: BufReader<ChildStdout>,
48        file: String,
49    ) -> io::Result<Self> {
50        let iotcm = load_file(file.clone());
51        send_command(&mut stdin, &iotcm).await?;
52        Ok(Self {
53            file,
54            iotcm,
55            stdin,
56            interaction_points: vec![],
57            agda: AgdaRead::from(stdout),
58        })
59    }
60}
61
62/// Start the Agda process and return the stdio handles.
63///
64/// Note that this function may panic.
65pub fn start_agda(agda_program: &str) -> JustStdio {
66    let ProcessStdio(process, stdio) = init_agda_process(agda_program).expect(START_FAIL);
67    tokio::spawn(async {
68        let status = process.wait_with_output().await.expect(START_FAIL);
69        println!("Agda exits with status {}.", status.status);
70    });
71    stdio
72}
73
74/// Send an [`IOTCM`](crate::cmd::IOTCM) command to Agda.
75pub async fn send_command(stdin: &mut ChildStdin, command: &IOTCM) -> io::Result<()> {
76    let string = command.to_string();
77    unsafe { debug_command(format!("[CMD]: {}", string)) };
78    stdin.write(string.as_bytes()).await?;
79    stdin.flush().await
80}
81
82/// Common command: load file in Agda.
83pub fn load_file(path: String) -> IOTCM {
84    let command = Cmd::load_simple(path.clone());
85    IOTCM::simple(path, command)
86}
agda_mode/agda/mod.rs

agda_mode/agda/
mod.rs
