use crate::ast::*;
use crate::checker_state::*;

use tracing::instrument;

impl CheckerState {
    #[instrument(skip(self), level = "debug", fields(%signature))]
    pub fn check_signature(&self, signature: Signature) -> Result<Signature, CheckerError> {
        match signature {
            Signature::Set => Ok(Signature::Set),
            Signature::Var(v) => {
                let deref = self.lookup_signature(&v)?;
                Ok(deref.clone())
            }
            Signature::Ext { .. } => Err(CheckerError::Unimplemented(
                "extension signatures".to_string(),
            )),
            Signature::Theory(fields) => {
                let mut ctx = self.clone();
                let fields = fields
                    .into_iter()
                    .map(|SigField { signature, name }| {
                        let signature = ctx.check_signature(signature)?;
                        ctx.add_instance(
                            name.clone(),
                            InstanceValue::Hypothetical(signature.clone()),
                            signature.clone(),
                        )?;
                        Ok(SigField { name, signature })
                    })
                    .collect::<Result<Vec<_>, _>>()?;
                Ok(Signature::Theory(fields))
            }
        }
    }
}