From e7427d5c67c0a90c369adecb4b0c65c043cb2e34 Mon Sep 17 00:00:00 2001 From: stuebinm Date: Tue, 26 Oct 2021 18:13:50 +0200 Subject: actually usable code structure for isabelle-proto --- isabelle-proto/src/main.rs | 91 +------------------------------------------ isabelle-proto/src/pipe.rs | 63 ++++++++++++++++++++++++++++++ isabelle-proto/src/session.rs | 8 +--- 3 files changed, 67 insertions(+), 95 deletions(-) create mode 100644 isabelle-proto/src/pipe.rs diff --git a/isabelle-proto/src/main.rs b/isabelle-proto/src/main.rs index 535dd52..1b52e27 100644 --- a/isabelle-proto/src/main.rs +++ b/isabelle-proto/src/main.rs @@ -1,104 +1,17 @@ mod session; mod messages; +mod pipe; + -use regex::Regex; -use serde::{Deserialize, Serialize, de::DeserializeOwned}; -use serde_json::{Result, Value}; use session::IsabelleSession; -use messages::*; -use std::{io::{BufRead, BufReader, BufWriter, Write}, path::PathBuf, process::{ChildStdout, Command, Stdio}}; -use std::fmt::Debug; use structopt::StructOpt; -fn decode_sync<'a, T> (msg: &'a str) -> Option> -where T: Deserialize<'a> { - let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap(); - let mat = regex.find(msg)?; - let ty = &msg[..mat.end()]; - let rest = &msg[mat.end()..]; - - match ty { - "OK" => Some(SyncAnswer::Ok(serde_json::from_str(&rest).ok()?)), - "ERROR" => Some(SyncAnswer::Error(rest.to_owned())), - _ => None - } -} - -fn decode_async<'a,T,E,N> (msg: &'a str) -> Option> -where T: Deserialize<'a>, N: Deserialize<'a>, E: Deserialize<'a> { - let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap(); - let mat = regex.find(msg)?; - let ty = &msg[..mat.end()]; - let rest = &msg[mat.end()..]; - - match ty { - "NOTE" => Some(AsyncAnswer::Note(serde_json::from_str(&rest).ok()?)), - "FINISHED" => Some(AsyncAnswer::Finished(serde_json::from_str(&rest).ok()?)), - "FAILED" => Some(AsyncAnswer::Failed(serde_json::from_str(&rest).ok()?)), - _ => None - } -} - - - - -fn wait_for_client(pipe: &mut BufReader) -> Option { - for res in pipe.lines() { - match res { - Err(_) => (), - Ok(line) => { - let hello : Option> = decode_sync(&line); - if let Some(SyncAnswer::Ok(data)) = hello { - return Some(data); - } - } - } - } - None -} - - -fn wait_for_async_task<'a,T,E,N,F> - (reader: &mut BufReader, task: &str, mut prog: F) -> Option -where T: DeserializeOwned, E: DeserializeOwned + Debug, N: DeserializeOwned, -F: FnMut(N) -{ - for res in reader.lines() { - match res { - Err(_) => (), - Ok(line) => { - let regex = Regex::new(r"^[0-9]+$").unwrap(); - if regex.is_match(&line) { - - } else { - match decode_async::(&line)? { - AsyncAnswer::Finished(data) - => return Some(data), - AsyncAnswer::Failed(failed) - => panic!("building session failed: {:?}", failed), - AsyncAnswer::Note(val) => prog(val) - } - } - } - } - }; - None -} - -fn get_async_task_id (reader: &mut BufReader) -> TaskID { - let mut res = String::new(); - reader.read_line(&mut res).unwrap(); - match decode_sync(&res).unwrap() { - SyncAnswer::Ok(AsyncStartOk { task }) => task, - SyncAnswer::Error(_) => panic!("failed to start async task!") - } -} #[derive(StructOpt)] #[structopt(name = "isabelle-proto-POC", about="proof of concept for communicating with an Isabelle server")] diff --git a/isabelle-proto/src/pipe.rs b/isabelle-proto/src/pipe.rs new file mode 100644 index 0000000..ef80ff3 --- /dev/null +++ b/isabelle-proto/src/pipe.rs @@ -0,0 +1,63 @@ + +use regex::Regex; +use serde::Deserialize; +use std::{io::{BufRead, BufReader}, process::ChildStdout}; + +use crate::messages::*; + +pub(crate) fn decode_sync<'a, T> (msg: &'a str) -> Option> +where T: Deserialize<'a> { + let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap(); + let mat = regex.find(msg)?; + let ty = &msg[..mat.end()]; + let rest = &msg[mat.end()..]; + + match ty { + "OK" => Some(SyncAnswer::Ok(serde_json::from_str(&rest).ok()?)), + "ERROR" => Some(SyncAnswer::Error(rest.to_owned())), + _ => None + } +} + +pub(crate) fn decode_async<'a,T,E,N> (msg: &'a str) -> Option> +where T: Deserialize<'a>, N: Deserialize<'a>, E: Deserialize<'a> { + let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap(); + let mat = regex.find(msg)?; + let ty = &msg[..mat.end()]; + let rest = &msg[mat.end()..]; + + match ty { + "NOTE" => Some(AsyncAnswer::Note(serde_json::from_str(&rest).ok()?)), + "FINISHED" => Some(AsyncAnswer::Finished(serde_json::from_str(&rest).ok()?)), + "FAILED" => Some(AsyncAnswer::Failed(serde_json::from_str(&rest).ok()?)), + _ => None + } +} + + + + +pub(crate) fn wait_for_client(pipe: &mut BufReader) -> Option { + for res in pipe.lines() { + match res { + Err(_) => (), + Ok(line) => { + let hello : Option> = decode_sync(&line); + if let Some(SyncAnswer::Ok(data)) = hello { + return Some(data); + } + } + } + } + None +} + + +pub(crate) fn get_async_task_id (reader: &mut BufReader) -> TaskID { + let mut res = String::new(); + reader.read_line(&mut res).unwrap(); + match decode_sync(&res).unwrap() { + SyncAnswer::Ok(AsyncStartOk { task }) => task, + SyncAnswer::Error(_) => panic!("failed to start async task!") + } +} diff --git a/isabelle-proto/src/session.rs b/isabelle-proto/src/session.rs index 11fb5bc..b1716d6 100644 --- a/isabelle-proto/src/session.rs +++ b/isabelle-proto/src/session.rs @@ -5,10 +5,7 @@ use serde::de::DeserializeOwned; use serde_json::Value; use crate::messages::*; - -use crate::{decode_async, get_async_task_id, wait_for_client}; - - +use crate::pipe::*; pub struct IsabelleSession { reader : BufReader, @@ -121,7 +118,6 @@ impl IsabelleSession { } } } - unreachable!{} - None + unreachable!{} } } -- cgit v1.2.3