summaryrefslogtreecommitdiff
path: root/isabelle-proto/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--isabelle-proto/src/main.rs89
-rw-r--r--isabelle-proto/src/session.rs126
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
+ }
+}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 05:52:31 +0000