From c6090f4b7fe238c34d4e15ceda0f1d9812a54276 Mon Sep 17 00:00:00 2001
From: stuebinm
Date: Tue, 26 Oct 2021 17:47:29 +0200
Subject: slightly less hacky proof of concept

---
 isabelle-proto/src/main.rs | 89 ++++++++++------------------------------------
 1 file changed, 19 insertions(+), 70 deletions(-)

(limited to 'isabelle-proto/src/main.rs')

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())
-        });
-}
-- 
cgit v1.2.3