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
|
use derive_more::Display;
#[derive(Display)]
#[display("{name}{{\n{}\n}}", DHList((stages, "\n")))]
pub struct ASTTheory {
name: String,
stages: Vec<ASTStage>,
}
#[derive(Display)]
#[display("{name} {} => {}", DHList((domain, ",")), DHList((domain, ",")))]
pub struct ASTStage {
name: String,
domain: Vec<ASTRecordEntry>,
codomain: Vec<ASTRecordEntry>,
}
#[derive(Display)]
pub enum ASTRecordEntry {
#[display("{name} type")]
ASTType { name: String },
#[display("{path} : {of}")]
ASTTerm { path: ASTPath, of: String },
#[display("{path} ~: {of}")]
ASTDependency { path: ASTPath, of: String },
#[display("{lhs_path} == {rhs_path}")]
ASTEquality {
lhs_path: ASTPath,
rhs_path: ASTPath,
},
#[display("let {var} = {stage}({})", DHList((args, ", ")))]
ASTLet {
var: String,
stage: String,
args: Vec<ASTPath>,
},
}
#[derive(Display)]
#[display("{}", DHList((_0, ".")))]
pub struct ASTPath(Vec<String>);
#[derive(Display)]
#[display("{}", _0.0.iter().map(|x| x.to_string()).collect::<Vec<_>>().join(_0.1))]
struct DHList<'a, T: std::fmt::Display>((&'a Vec<T>, &'static str));
|
