diff options
Diffstat (limited to '')
-rw-r--r-- | isabelle-proto/src/main.rs | 137 | ||||
-rw-r--r-- | isabelle-proto/src/messages.rs | 143 | ||||
-rw-r--r-- | isabelle-proto/src/session.rs | 3 |
3 files changed, 148 insertions, 135 deletions
diff --git a/isabelle-proto/src/main.rs b/isabelle-proto/src/main.rs index b16b8ac..535dd52 100644 --- a/isabelle-proto/src/main.rs +++ b/isabelle-proto/src/main.rs @@ -1,131 +1,20 @@ mod session; +mod messages; 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 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> { @@ -158,26 +47,6 @@ where T: Deserialize<'a>, N: Deserialize<'a>, E: Deserialize<'a> { -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"; - println!("encoded: {}", res); - res - } -} fn wait_for_client(pipe: &mut BufReader<ChildStdout>) -> Option<ClientHello> { for res in pipe.lines() { diff --git a/isabelle-proto/src/messages.rs b/isabelle-proto/src/messages.rs new file mode 100644 index 0000000..908ddf1 --- /dev/null +++ b/isabelle-proto/src/messages.rs @@ -0,0 +1,143 @@ + +use serde::{Deserialize, Serialize}; + +pub type SessionID = String; +pub type TaskID = String; + +#[derive(Serialize, Deserialize)] +#[serde(untagged)] +pub 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)] +pub enum SyncAnswer<T,E> { + Ok (T), + Error (E), +} + +pub enum AsyncAnswer<T, E, N> { + Finished (T), + Failed (E), + Note (N) +} + +#[derive(Deserialize, Debug)] +pub struct ClientHello { + pub isabelle_id : String, + pub isabelle_version : String +} + +#[allow(dead_code)] +#[derive(Deserialize)] +pub struct SessionStartedOk { + pub session_id : String, + pub tmp_dir : String, + pub task : String +} + +#[allow(dead_code)] +#[derive(Deserialize)] +pub struct SessionStartedNote { + pub percentage : u8, + pub task : TaskID, + pub message : String, + pub kind : String, + pub session : String, + pub theory : String +} + +#[derive(Deserialize, Clone, Debug)] +pub struct SessionStartedFinished { + pub session_id : SessionID, + pub tmp_dir : String, + pub task : TaskID +} + + + +#[derive(Deserialize, Clone, Debug)] +pub struct UseTheoriesFinished { + pub ok : bool, + pub errors : Vec<IsabelleError>, + pub nodes : Vec<IsabelleNode>, + pub task : TaskID, +} + +#[derive(Deserialize, Clone, Debug)] +pub struct IsabelleError { + pub kind : String, + pub message : String, + pub pos : Span +} + +#[derive(Deserialize, Clone, Debug)] +pub struct IsabelleNode { + pub messages : Vec<IsabelleError>, + pub exports : Vec<()>, + pub status : Status, + pub theory_name : String, + pub node_name : String +} + +#[derive(Deserialize, Clone, Debug)] +pub struct Status { + pub percentage : u8, + pub unprocessed : u64, + pub running : u64, + pub finished : u64, + pub failed : u64, + pub total : u64, + pub consolidated : bool, + pub canceled : bool, + pub ok : bool, + pub warned : u64 +} + +#[derive(Deserialize,Clone, Debug)] +pub struct Span { + pub line : u64, + pub offset : u64, + pub end_offset : u64, + pub file : String +} + +#[derive(Deserialize)] +pub struct AsyncStartOk { + pub task : TaskID +} + + + + + +pub 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"; + println!("encoded: {}", res); + res + } +} diff --git a/isabelle-proto/src/session.rs b/isabelle-proto/src/session.rs index 85081d4..11fb5bc 100644 --- a/isabelle-proto/src/session.rs +++ b/isabelle-proto/src/session.rs @@ -4,8 +4,9 @@ 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}; +use crate::messages::*; +use crate::{decode_async, get_async_task_id, wait_for_client}; |