summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--isabelle-proto/src/main.rs91
-rw-r--r--isabelle-proto/src/pipe.rs63
-rw-r--r--isabelle-proto/src/session.rs8
3 files changed, 67 insertions, 95 deletions
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<SyncAnswer<T, String>>
-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<AsyncAnswer<T,E,N>>
-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<ChildStdout>) -> Option<ClientHello> {
- for res in pipe.lines() {
- match res {
- Err(_) => (),
- Ok(line) => {
- let hello : Option<SyncAnswer<ClientHello, _>> = 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<ChildStdout>, task: &str, mut prog: F) -> Option<T>
-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::<T,E,N>(&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<ChildStdout>) -> 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<SyncAnswer<T, String>>
+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<AsyncAnswer<T,E,N>>
+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<ChildStdout>) -> Option<ClientHello> {
+ for res in pipe.lines() {
+ match res {
+ Err(_) => (),
+ Ok(line) => {
+ let hello : Option<SyncAnswer<ClientHello, _>> = decode_sync(&line);
+ if let Some(SyncAnswer::Ok(data)) = hello {
+ return Some(data);
+ }
+ }
+ }
+ }
+ None
+}
+
+
+pub(crate) fn get_async_task_id (reader: &mut BufReader<ChildStdout>) -> 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<ChildStdout>,
@@ -121,7 +118,6 @@ impl IsabelleSession {
}
}
}
- unreachable!{}
- None
+ unreachable!{}
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-04-23 06:16:36 +0000