diff options
Diffstat (limited to 'isabelle-proto')
| -rw-r--r-- | isabelle-proto/Cargo.toml | 14 | ||||
| -rw-r--r-- | isabelle-proto/src/main.rs | 312 |
2 files changed, 326 insertions, 0 deletions
diff --git a/isabelle-proto/Cargo.toml b/isabelle-proto/Cargo.toml new file mode 100644 index 0000000..351532f --- /dev/null +++ b/isabelle-proto/Cargo.toml @@ -0,0 +1,14 @@ +[package] +name = "isabelle-proto" +version = "0.1.0" +authors = ["stuebinm <stuebinm@disroot.org>"] +edition = "2018" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +regex = "1" +serde = { version = "1.0.130", features = [ "derive" ] } +serde_json = "1.0.68" +isabelle-unicode = { path = "../isabelle-unicode" } +structopt = "0.3.23" diff --git a/isabelle-proto/src/main.rs b/isabelle-proto/src/main.rs new file mode 100644 index 0000000..1ee20a9 --- /dev/null +++ b/isabelle-proto/src/main.rs @@ -0,0 +1,312 @@ + +use regex::Regex; +use serde::{Deserialize, Serialize, de::DeserializeOwned}; +use serde_json::{Result, Value}; + +use std::{io::{BufRead, BufReader, BufWriter, Write}, path::PathBuf, process::{ChildStdout, Command, Stdio}}; + +use isabelle_unicode::PrettyUnicode; + +use structopt::StructOpt; + +type SessionID = String; +type TaskID = String; + +#[derive(Serialize, Deserialize)] +#[serde(untagged)] +enum ClientCommand { + UseTheories { + session_id : SessionID, + theories : Vec<String>, + master_dir : Option<String> + }, + SessionStart { + session : String, + include_sessions : Vec<String> + }, + Echo (String), + ShutDown +} + +#[derive(Debug)] +enum SyncAnswer<T,E> { + Ok (T), + Error (E), +} + +enum AsyncAnswer<T, E, N> { + Finished (T), + Failed (E), + Note (N) +} + +#[derive(Deserialize, Debug)] +struct ClientHello { + isabelle_id : String, + isabelle_version : String +} + +#[derive(Deserialize)] +struct SessionStartedOk { + session_id : String, + tmp_dir : String, + task : String +} + +#[derive(Deserialize)] +struct SessionStartedNote { + percentage : u8, + task : TaskID, + message : String, + kind : String, + session : String, + theory : String +} + +#[derive(Deserialize, Clone, Debug)] +struct SessionStartedFinished { + session_id : SessionID, + tmp_dir : String, + task : TaskID +} + + + +#[derive(Deserialize, Clone, Debug)] +struct UseTheoriesFinished { + ok : bool, + errors : Vec<IsabelleError>, + nodes : Vec<IsabelleNode>, + task : TaskID, +} + +#[derive(Deserialize, Clone, Debug)] +struct IsabelleError { + kind : String, + message : String, + pos : Span +} + +#[derive(Deserialize, Clone, Debug)] +struct IsabelleNode { + messages : Vec<IsabelleError>, + exports : Vec<()>, + status : Status, + theory_name : String, + node_name : String +} + +#[derive(Deserialize, Clone, Debug)] +struct Status { + percentage : u8, + unprocessed : u64, + running : u64, + finished : u64, + failed : u64, + total : u64, + consolidated : bool, + canceled : bool, + ok : bool, + warned : u64 +} + +#[derive(Deserialize,Clone, Debug)] +struct Span { + line : u64, + offset : u64, + end_offset : u64, + file : String +} + +#[derive(Deserialize)] +struct AsyncStartOk { + task : TaskID +} + +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 + } +} + + + +trait Encode { + fn encode (&self) -> String; +} + +impl Encode for ClientCommand { + fn encode (&self) -> String { + let ty = match self { + ClientCommand::UseTheories {..} => "use_theories", + ClientCommand::SessionStart {..} => "session_start", + ClientCommand::Echo (..) => "echo", + ClientCommand::ShutDown => "shutdown" + }; + + let blob = serde_json::to_string(self).unwrap(); + + let res = ty.to_owned() + &blob + "\n"; + res + } +} + +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, 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"), + 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")] +struct Options { + theory : String, + #[structopt(name="directory", default_value=Box::leak(Box::new(std::env::current_dir().unwrap().into_os_string().into_string().unwrap())))] + directory : String +} + +fn main() { + let options = Options::from_args(); + println!("will check: {} in {}", options.theory, options.directory); + + 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 stdin = child.stdin.as_mut().unwrap(); + let stdout = child.stdout.take().unwrap(); + + let mut reader = BufReader::new(stdout); + + let _ = wait_for_client(&mut reader); + // TODO: display version information? + + let mut len : usize = 0; + + let session_id = match std::env::var("ISABAT_SESSION_ID") { + Ok(id) => id, + Err(_) => { + + // client should be ready, start a session + stdin.write(ClientCommand::SessionStart{ + session: "HOL".to_string(), + include_sessions: vec![], + }.encode().as_bytes()).unwrap(); + + let task = get_async_task_id(&mut reader); + + let started = wait_for_async_task::<SessionStartedFinished, Value, Value,_>(&mut reader, &task, |note| { + if let Some(Value::String(msg)) = note.get("message") { + len = msg.len(); + print!("{}\r", msg); + std::io::stdout().flush().unwrap(); + } + }).unwrap(); + + started.session_id + } + }; + + + // HOL should be loaded now, include a theory file + + stdin.write(ClientCommand::UseTheories { + session_id, + theories: vec![ options.theory ], + master_dir: Some(options.directory), + }.encode().as_bytes()).unwrap(); + + let task = get_async_task_id(&mut reader); + let result = wait_for_async_task::<UseTheoriesFinished, Value, Value, _>(&mut reader, &task, |note| { + if let Some(Value::String(msg)) = note.get("message") { + let white = len.checked_sub(msg.len()).unwrap_or(0); + len = msg.len(); + print!("{}{}\r", msg, str::repeat(" ", white)); + std::io::stdout().flush().unwrap(); + } + }).unwrap(); + println!("{}", str::repeat(" ", len)); + + // built a theory! Let's display errors + + result + .errors + .iter() + .for_each(|err| { + println!("Isabelle Error:"); + println!("{}", err.message.to_pretty_unicode().unwrap()) + }); +} |