blob: 1925b41c6ca984dfbefab0b45c2ac18d28dc7814 (
plain)
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
|
mod ast;
mod checker;
mod checker_set;
mod checker_signature;
mod checker_state;
mod parser;
use tracing_subscriber::{layer::SubscriberExt, util::SubscriberInitExt};
use tracing_tree::HierarchicalLayer;
fn main() {
tracing_subscriber::registry()
.with(
HierarchicalLayer::new(2)
.with_targets(false)
.with_bracketed_fields(true),
)
.init();
let src = r#"
// let signature Graph = theory {
// Vertex :: Set,
// Edge :: (s : set-of(Vertex)) (t : set-of(Vertex)) -> Set
// }
// let set Empty = variant[]
// let set Unit = record{}
// let element pt : Unit = {}
// let set F1 = variant [ one0 : Unit ]
// let set F2 = variant [ two0 : Unit | two1 : Unit ]
// let set F3 = variant [ three0 : Unit | three1 : Unit | three2: Unit ]
// let instance oneSimplex :: Graph = {
// .Vertex = F3 :: Set,
// .Edge = for (s : set-of(Vertex)) (t : set-of(Vertex)),
// case s of [
// three0. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Unit :: Set | three2. pt => Unit :: Set ]
// | three1. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Unit :: Set ]
// | three2. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Empty :: Set ]
// ]
// }
// let set OneSimplexEdges = record {
// source: set-of(oneSimplex .Vertex),
// target: set-of(oneSimplex .Vertex),
// connected: set-of(oneSimplex .Edge source target)
// }
// let element vertex0 : F3 = three0. {}
// let element vertex1 : F3 = three1. {}
// let element edge01 : set-of(oneSimplex .Edge vertex0 vertex1) = pt
let signature S = theory {
F :: (x : Nat) (y : Bool) -> Set,
G :: (z : set-of(F 3 5)) -> Set
}
"#;
let programme = parser::parse(src);
if let Err(e) = programme.check() {
println!("{}", e);
}
}
|
