src/main.rs


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

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 {
    Node :: Set,
    Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set
}

let set FinTwo = variant [ zero : record{} | one : record{} ]

let instance natGraph :: Graph = {
    .Node = FinTwo :: Set,
    .Edge = for (s : set-of(Node)) (t : set-of(Node)), case s of [ zero. ignore => Bool :: Set | one. ignore => Nat :: Set ]
}

let set NatEdges = record {
  source: set-of(natGraph .Node),
  target: set-of(natGraph .Node),
  connected: set-of(natGraph .Edge source target)
}
"#;
    let programme = parser::debug_parse(src);

    if let Err(e) = programme.check() {
        println!("{}", e);
    }
}