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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60

mod ast;
mod checker;
mod checker_set;
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 set X = record { .b : Bool, .n : Nat } // basic

let set Y = X

let set Z = record { .y : Y }

let set W = variant [ z. : Z | f. : Float ]

let element x : X = { .b = true, .n = 41 }

let element z : Z = { .y = x }

let element the_nat : Nat = z .y .n

let element injected : W = z. z

let element compute : Nat = case injected of [ z. myz => myz .y .n | f. myf => myf ]

// let signature Graph = theory {
//     .Node :: Set,
//     .Edge :: (s : Node) (t : Node) -> Set
// }
//
// let instance natPoset :: Graph = {
//     .Node = Nat,
//     .Edge = for (s : Nat) (t : Nat), Bool
// }
//
// let element node : set-of(natPoset .Node) = 7
"#;
    let programme = parser::parser::program(src);

    assert!(programme.is_ok());
    let programme = programme.unwrap();
    println!("Parsed:\n```\n{}\n```\n", programme);

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