use crate::ast::*;
use crate::checker_state::{CheckerError, CheckerState};

use tracing::{debug, instrument};

impl Programme {
    pub fn check(&self) -> Result<(), CheckerError> {
        let mut state = CheckerState::default();
        state.check(self)
    }
}

impl CheckerState {
    #[instrument(skip(self, prog), level = "debug")]
    pub fn check(&mut self, prog: &Programme) -> Result<(), CheckerError> {
        let Programme(decls) = prog;

        for decl in decls {
            print!("{decl} ... ");
            self.reset_binders();
            match decl {
                Decl::Set { name, set } => {
                    self.assert_unbound_set(name)?;
                    let set = self.check_set(set)?;
                    self.add_set(name.clone(), set, false)
                }

                Decl::Element { name, element, set } => {
                    self.assert_unbound_element(name)?;
                    let set = self.check_set(set)?;
                    let element = self.check_element(element.into(), Some(&set))?;
                    self.add_element(name.clone(), element.into(), set)
                }
                Decl::Signature { name, signature } => {
                    self.assert_unbound_signature(name)?;
                    let signature = self.check_signature(signature)?;
                    self.add_signature(name, signature, false)
                }
                Decl::Instance {
                    name,
                    instance,
                    signature,
                } => {
                    self.assert_unbound_instance(name)?;
                    let signature = self.check_signature(signature)?;
                    let instance = self.check_instance(instance, (&signature).into())?;
                    self.add_instance(name.clone(), instance.into(), signature)
                }
            }?;
            println!("Ok");
        }
        debug!(%self);
        Ok(())
    }
}