src/checker_signature.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

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))
            }
        }
    }
}