diff options
author | stuebinm | 2021-10-26 18:04:16 +0200 |
---|---|---|
committer | stuebinm | 2021-10-26 18:04:16 +0200 |
commit | 4c6d323ad1536e9ef6082eb34d872ccae1f389ef (patch) | |
tree | fda19c10314be1ed6a8ab3abba5fd5d43151fd4a /isabelle-proto/src/main.rs | |
parent | c6090f4b7fe238c34d4e15ceda0f1d9812a54276 (diff) |
better code structure for isabelle-proto
Diffstat (limited to '')
-rw-r--r-- | isabelle-proto/src/main.rs | 137 |
1 files changed, 3 insertions, 134 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() { |