diff options
author | stuebinm | 2021-10-26 17:47:29 +0200 |
---|---|---|
committer | stuebinm | 2021-10-26 17:47:29 +0200 |
commit | c6090f4b7fe238c34d4e15ceda0f1d9812a54276 (patch) | |
tree | 7bfaab865be5803d2b6ad9435c7b1a0d6262170f /isabelle-proto/src/session.rs | |
parent | 5a021caf3ff516c110571bfb4485e833ba8b1d06 (diff) |
slightly less hacky proof of concept
Diffstat (limited to 'isabelle-proto/src/session.rs')
-rw-r--r-- | isabelle-proto/src/session.rs | 126 |
1 files changed, 126 insertions, 0 deletions
diff --git a/isabelle-proto/src/session.rs b/isabelle-proto/src/session.rs new file mode 100644 index 0000000..85081d4 --- /dev/null +++ b/isabelle-proto/src/session.rs @@ -0,0 +1,126 @@ +use std::{io::{BufRead, BufReader, Write}, process::{ChildStdin, ChildStdout, Command, Stdio}}; + +use regex::Regex; +use serde::de::DeserializeOwned; +use serde_json::Value; + +use crate::{AsyncAnswer, ClientCommand, Encode, SessionStartedFinished, UseTheoriesFinished, decode_async, get_async_task_id, wait_for_client}; + + + + +pub struct IsabelleSession { + reader : BufReader<ChildStdout>, + writer : ChildStdin, + session_id : Option<String> +} + +impl IsabelleSession { + pub fn start_with_client() -> Self { + let mut child = Command::new("isabelle") + .arg("client") + .stdin(Stdio::piped()) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .spawn() + .expect("failed to run isabelle client!"); + + let mut reader = BufReader::new(child.stdout.take().unwrap()); + let a = wait_for_client(&mut reader); + println!("client hello: {:?}", a); + IsabelleSession { + writer: child.stdin.unwrap(), + reader, + session_id: None + } + } + + pub fn start_session(&mut self, session : String, include_sessions : Vec<String>) + -> Result<SessionStartedFinished, Value> + { + + self.writer.write(ClientCommand::SessionStart { + session, include_sessions + }.encode().as_bytes()).unwrap(); + let task_id = get_async_task_id(&mut self.reader); + let started = self.await_task::<SessionStartedFinished, Value, Value,_>(&task_id, |_n| {}) + // .await + .unwrap(); + + match started { + Ok(ref finished) => self.session_id = Some(finished.session_id.to_owned()), + Err(_) => () + }; + + started + } + + + pub fn load_theory(&mut self, theory : String, master_dir : Option<String>) + -> Result<UseTheoriesFinished, Value> { + let session_id = self.session_id.as_ref().unwrap(); + + self.writer.write(ClientCommand::UseTheories { + session_id: session_id.clone(), + theories: vec![ theory ], + master_dir, + }.encode().as_bytes()).unwrap(); + + let task_id = get_async_task_id(&mut self.reader); + + self.await_task::<UseTheoriesFinished, Value, Value, _>(&task_id, |_| {}) + .unwrap() + } + + + + fn await_task<'a,T,E,N,F>( + &mut self, + task_id: &str, + mut prog: F) + -> Option<Result<T, E>> + where T: DeserializeOwned, + E: DeserializeOwned, + N: DeserializeOwned, + F: FnMut(N) + { + let reader = &mut self.reader; + for res in reader.lines() { + match res { + Err(err) => { + eprintln!("error while reading from pipe: {}", err); + std::process::exit(1); + }, + Ok(line) => { + let regex = Regex::new(r"^[0-9]+$").unwrap(); + if regex.is_match(&line) { + // TODO: we don't support the long style of messages yet … + // the following just assumes that the next blob is json + // and does not contain line breaks. + } else { + // TODO: this shouldn't have to parse the json twice + let value : Value = match decode_async(&line).unwrap() { + AsyncAnswer::Finished(v) => v, + AsyncAnswer::Failed(v) => v, + AsyncAnswer::Note(v) => v + }; + match value.get("task") { + Some(id) if id == task_id => + Some(match decode_async::<T,E,N>(&line).unwrap() { + AsyncAnswer::Finished(data) + => return Some(Ok(data)), + AsyncAnswer::Failed(failed) + => return Some(Err(failed)), + AsyncAnswer::Note(val) => prog(val) + + }), + _ => return None + }; + } + } + } + } + unreachable!{} + None + } +} |