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 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 = {
    .Node = F3 :: Set,
    .Edge = for (s : set-of(Node)) (t : set-of(Node)),
              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 .Node),
  target: set-of(oneSimplex .Node),
  connected: set-of(oneSimplex .Edge source target)
}

let element edge : set-of(oneSimplex .Edge (three0. pt) (three1. pt)) = pt
"#;
    let programme = parser::parse(src);

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