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
128
129
130
|
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 structopt::StructOpt;
fn decode_sync<'a, T> (msg: &'a str) -> Option<SyncAnswer<T, String>>
where T: Deserialize<'a> {
let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap();
let mat = regex.find(msg)?;
let ty = &msg[..mat.end()];
let rest = &msg[mat.end()..];
match ty {
"OK" => Some(SyncAnswer::Ok(serde_json::from_str(&rest).ok()?)),
"ERROR" => Some(SyncAnswer::Error(rest.to_owned())),
_ => None
}
}
fn decode_async<'a,T,E,N> (msg: &'a str) -> Option<AsyncAnswer<T,E,N>>
where T: Deserialize<'a>, N: Deserialize<'a>, E: Deserialize<'a> {
let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap();
let mat = regex.find(msg)?;
let ty = &msg[..mat.end()];
let rest = &msg[mat.end()..];
match ty {
"NOTE" => Some(AsyncAnswer::Note(serde_json::from_str(&rest).ok()?)),
"FINISHED" => Some(AsyncAnswer::Finished(serde_json::from_str(&rest).ok()?)),
"FAILED" => Some(AsyncAnswer::Failed(serde_json::from_str(&rest).ok()?)),
_ => None
}
}
fn wait_for_client(pipe: &mut BufReader<ChildStdout>) -> Option<ClientHello> {
for res in pipe.lines() {
match res {
Err(_) => (),
Ok(line) => {
let hello : Option<SyncAnswer<ClientHello, _>> = decode_sync(&line);
if let Some(SyncAnswer::Ok(data)) = hello {
return Some(data);
}
}
}
}
None
}
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 + Debug, N: DeserializeOwned,
F: FnMut(N)
{
for res in reader.lines() {
match res {
Err(_) => (),
Ok(line) => {
let regex = Regex::new(r"^[0-9]+$").unwrap();
if regex.is_match(&line) {
} else {
match decode_async::<T,E,N>(&line)? {
AsyncAnswer::Finished(data)
=> return Some(data),
AsyncAnswer::Failed(failed)
=> panic!("building session failed: {:?}", failed),
AsyncAnswer::Note(val) => prog(val)
}
}
}
}
};
None
}
fn get_async_task_id (reader: &mut BufReader<ChildStdout>) -> TaskID {
let mut res = String::new();
reader.read_line(&mut res).unwrap();
match decode_sync(&res).unwrap() {
SyncAnswer::Ok(AsyncStartOk { task }) => task,
SyncAnswer::Error(_) => panic!("failed to start async task!")
}
}
#[derive(StructOpt)]
#[structopt(name = "isabelle-proto-POC", about="proof of concept for communicating with an Isabelle server")]
struct Options {
theory : String,
#[structopt(name="directory", default_value=Box::leak(Box::new(std::env::current_dir().unwrap().into_os_string().into_string().unwrap())))]
directory : String
}
fn main() {
let options = Options::from_args();
let mut session = IsabelleSession::start_with_client();
let started = session.start_session("HOL".to_owned(),vec![]).unwrap();
println!("{:?}", started);
let theoryresults = session.load_theory(
options.theory,
Some(options.directory)
);
println!("loaded theory: {:?}", theoryresults);
}
|
