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 X be the set Y, call it Z
let set X = record { b : Bool, n : Nat }
let set Y = X
let set Z = record { y : Y }
// make some elements
let element x : X = { .b = true, .n = 41 }
let element z : Z = { .y = x }
// exercise case matching
let set Z_or_Float = variant [ z : Z | f : Float ]
let element injected : Z_or_Float = z. z
let element check_cases : Nat = case injected of [ z. myz => myz .y .n | f. myf => 2 ]

// this should be difficult unless we correctly handle various forms of alpha/beta
let signature OneSet = theory { F :: Set }
let signature T = theory {
    A :: Set,
    B :: (x : set-of({ .F = A } .F)) -> Set,
    C :: (x : set-of(A)) (b : set-of(B x)) -> Set
}

let signature Graph = theory {
    Node :: Set,
    Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set
}

let instance natPoset :: Graph = {
    .Node = Nat,
    .Edge = for (s : Nat) (t : Nat), Bool
}

let element node : set-of(natPoset .Node) = 7

let set NatEdges = record {
  source: set-of(natPoset .Node),
  target: set-of(natPoset .Node),
  connected: set-of(natPoset .Edge source target)
}
"#;
    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);
    }
}