1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
|
use std::{io::{BufRead, BufReader, Write}, process::{ChildStdin, ChildStdout, Command, Stdio}};
use regex::Regex;
use serde::de::DeserializeOwned;
use serde_json::Value;
use crate::messages::*;
use crate::{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
}
}
|
