summaryrefslogtreecommitdiff
path: root/isabelle-proto
diff options
context:
space:
mode:
Diffstat (limited to 'isabelle-proto')
-rw-r--r--isabelle-proto/src/main.rs137
-rw-r--r--isabelle-proto/src/messages.rs143
-rw-r--r--isabelle-proto/src/session.rs3
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};