slightly less hacky proof of concept

2 files changed, 145 insertions, 70 deletions

diff --git a/isabelle-proto/src/main.rs b/isabelle-proto/src/main.rs
index 1ee20a9..b16b8ac 100644
--- a/isabelle-proto/src/main.rs
+++ b/isabelle-proto/src/main.rs
@@ -1,9 +1,13 @@
 
+mod session;
+
 use regex::Regex;
 use serde::{Deserialize, Serialize, de::DeserializeOwned};
 use serde_json::{Result, Value};
+use session::IsabelleSession;
 
 use std::{io::{BufRead, BufReader, BufWriter, Write}, path::PathBuf, process::{ChildStdout, Command, Stdio}};
+use std::fmt::Debug;
 
 use isabelle_unicode::PrettyUnicode;
 
@@ -170,6 +174,7 @@ impl Encode for ClientCommand {
         let blob = serde_json::to_string(self).unwrap();
 
         let res = ty.to_owned() + &blob + "\n";
+        println!("encoded: {}", res);
         res
     }
 }
@@ -192,7 +197,7 @@ fn wait_for_client(pipe: &mut BufReader<ChildStdout>) -> Option<ClientHello> {
 
 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,
+where T: DeserializeOwned, E: DeserializeOwned + Debug, N: DeserializeOwned,
 F: FnMut(N)
 {
     for res in reader.lines() {
@@ -206,8 +211,8 @@ F: FnMut(N)
                     match decode_async::<T,E,N>(&line)? {
                         AsyncAnswer::Finished(data)
                             => return Some(data),
-                        AsyncAnswer::Failed(_failed)
-                            => panic!("building session failed"),
+                        AsyncAnswer::Failed(failed)
+                            => panic!("building session failed: {:?}", failed),
                         AsyncAnswer::Note(val) => prog(val)
                     }
                 }
@@ -234,79 +239,23 @@ struct Options {
     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();
+fn main() {
+    let options = Options::from_args();
+    let mut session = IsabelleSession::start_with_client();
 
-            let task = get_async_task_id(&mut reader);
+    let started = session.start_session("HOL".to_owned(),vec![]).unwrap();
 
-            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();
+    println!("{:?}", started);
 
-            started.session_id
-        }
-    };
+    let theoryresults = session.load_theory(
+        options.theory,
+        Some(options.directory)
+    );
 
+    println!("loaded theory: {:?}", theoryresults);
+}
 
-    // 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())
-        });
-}
diff --git a/isabelle-proto/src/session.rs b/isabelle-proto/src/session.rs
new file mode 100644
index 0000000..85081d4
--- /dev/null
+++ b/isabelle-proto/src/session.rs
@@ -0,0 +1,126 @@
+use std::{io::{BufRead, BufReader, Write}, process::{ChildStdin, ChildStdout, Command, Stdio}};
+
+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};
+
+
+
+
+pub struct IsabelleSession {
+    reader : BufReader<ChildStdout>,
+    writer : ChildStdin,
+    session_id : Option<String>
+}
+
+impl IsabelleSession {
+    pub fn start_with_client() -> Self {
+        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 mut reader = BufReader::new(child.stdout.take().unwrap());
+        let a = wait_for_client(&mut reader);
+        println!("client hello: {:?}", a);
+        IsabelleSession {
+            writer: child.stdin.unwrap(),
+            reader,
+            session_id: None
+        }
+    }
+
+    pub  fn start_session(&mut self, session : String, include_sessions : Vec<String>)
+        -> Result<SessionStartedFinished, Value>
+    {
+
+        self.writer.write(ClientCommand::SessionStart {
+            session, include_sessions
+        }.encode().as_bytes()).unwrap();
+        let task_id = get_async_task_id(&mut self.reader);
+        let started = self.await_task::<SessionStartedFinished, Value, Value,_>(&task_id, |_n| {})
+        //    .await
+            .unwrap();
+
+        match started {
+            Ok(ref finished) => self.session_id = Some(finished.session_id.to_owned()),
+            Err(_) => ()
+        };
+
+        started
+    }
+
+
+    pub fn load_theory(&mut self, theory : String, master_dir : Option<String>)
+    -> Result<UseTheoriesFinished, Value> {
+        let session_id = self.session_id.as_ref().unwrap();
+
+        self.writer.write(ClientCommand::UseTheories {
+            session_id: session_id.clone(),
+            theories: vec![ theory ],
+            master_dir,
+        }.encode().as_bytes()).unwrap();
+
+        let task_id = get_async_task_id(&mut self.reader);
+
+        self.await_task::<UseTheoriesFinished, Value, Value, _>(&task_id, |_| {})
+            .unwrap()
+    }
+
+
+
+    fn await_task<'a,T,E,N,F>(
+        &mut self,
+        task_id: &str,
+        mut prog: F)
+    -> Option<Result<T, E>>
+    where T: DeserializeOwned,
+          E: DeserializeOwned,
+          N: DeserializeOwned,
+          F: FnMut(N)
+    {
+        let reader = &mut self.reader;
+        for res in reader.lines() {
+            match res {
+                Err(err) => {
+                    eprintln!("error while reading from pipe: {}", err);
+                    std::process::exit(1);
+                },
+                Ok(line) => {
+                    let regex = Regex::new(r"^[0-9]+$").unwrap();
+                    if regex.is_match(&line) {
+                        // TODO: we don't support the long style of messages yet …
+                        // the following just assumes that the next blob is json
+                        // and does not contain line breaks.
+                    } else {
+                        // TODO: this shouldn't have to parse the json twice
+                        let value : Value = match decode_async(&line).unwrap() {
+                            AsyncAnswer::Finished(v) => v,
+                            AsyncAnswer::Failed(v) => v,
+                            AsyncAnswer::Note(v) => v
+                        };
+                        match value.get("task") {
+                            Some(id) if id == task_id =>
+                                Some(match decode_async::<T,E,N>(&line).unwrap() {
+                                    AsyncAnswer::Finished(data)
+                                        => return Some(Ok(data)),
+                                    AsyncAnswer::Failed(failed)
+                                        => return Some(Err(failed)),
+                                    AsyncAnswer::Note(val) => prog(val)
+
+                                }),
+                            _ => return None
+                        };
+                    }
+                }
+            }
+        }
+         unreachable!{}
+        None
+    }
+}