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
131
132
133
134
135
136
137
138
139
140
141
142
143
|
use serde::{Deserialize, Serialize};
pub type SessionID = String;
pub type TaskID = String;
#[derive(Serialize, Deserialize)]
#[serde(untagged)]
pub enum ClientCommand {
UseTheories {
session_id : SessionID,
theories : Vec<String>,
master_dir : Option<String>
},
SessionStart {
session : String,
include_sessions : Vec<String>
},
Echo (String),
ShutDown
}
#[derive(Debug)]
pub enum SyncAnswer<T,E> {
Ok (T),
Error (E),
}
pub enum AsyncAnswer<T, E, N> {
Finished (T),
Failed (E),
Note (N)
}
#[derive(Deserialize, Debug)]
pub struct ClientHello {
pub isabelle_id : String,
pub isabelle_version : String
}
#[allow(dead_code)]
#[derive(Deserialize)]
pub struct SessionStartedOk {
pub session_id : String,
pub tmp_dir : String,
pub task : String
}
#[allow(dead_code)]
#[derive(Deserialize)]
pub struct SessionStartedNote {
pub percentage : u8,
pub task : TaskID,
pub message : String,
pub kind : String,
pub session : String,
pub theory : String
}
#[derive(Deserialize, Clone, Debug)]
pub struct SessionStartedFinished {
pub session_id : SessionID,
pub tmp_dir : String,
pub task : TaskID
}
#[derive(Deserialize, Clone, Debug)]
pub struct UseTheoriesFinished {
pub ok : bool,
pub errors : Vec<IsabelleError>,
pub nodes : Vec<IsabelleNode>,
pub task : TaskID,
}
#[derive(Deserialize, Clone, Debug)]
pub struct IsabelleError {
pub kind : String,
pub message : String,
pub pos : Span
}
#[derive(Deserialize, Clone, Debug)]
pub struct IsabelleNode {
pub messages : Vec<IsabelleError>,
pub exports : Vec<()>,
pub status : Status,
pub theory_name : String,
pub node_name : String
}
#[derive(Deserialize, Clone, Debug)]
pub struct Status {
pub percentage : u8,
pub unprocessed : u64,
pub running : u64,
pub finished : u64,
pub failed : u64,
pub total : u64,
pub consolidated : bool,
pub canceled : bool,
pub ok : bool,
pub warned : u64
}
#[derive(Deserialize,Clone, Debug)]
pub struct Span {
pub line : u64,
pub offset : u64,
pub end_offset : u64,
pub file : String
}
#[derive(Deserialize)]
pub struct AsyncStartOk {
pub task : TaskID
}
pub trait Encode {
fn encode (&self) -> String;
}
impl Encode for ClientCommand {
fn encode (&self) -> String {
let ty = match self {
ClientCommand::UseTheories {..} => "use_theories",
ClientCommand::SessionStart {..} => "session_start",
ClientCommand::Echo (..) => "echo",
ClientCommand::ShutDown => "shutdown"
};
let blob = serde_json::to_string(self).unwrap();
let res = ty.to_owned() + &blob + "\n";
println!("encoded: {}", res);
res
}
}
|
