diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/checker_set.rs | 5 | ||||
| -rw-r--r-- | src/checker_signature.rs | 23 | ||||
| -rw-r--r-- | src/checker_state.rs | 6 |
3 files changed, 27 insertions, 7 deletions
diff --git a/src/checker_set.rs b/src/checker_set.rs index 2ea0c3d..2faca9e 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -14,10 +14,7 @@ impl CheckerState { .into_iter() .map(|RecordField { name, set }| { let set = self.check_set(set)?; - Ok(RecordField { - name: name.clone(), - set, - }) + Ok(RecordField { name, set }) }) .collect::<Result<Vec<_>, _>>()?; Ok(Set::Record(fields)) diff --git a/src/checker_signature.rs b/src/checker_signature.rs index 8fc982a..4fa723f 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -6,8 +6,25 @@ use tracing::instrument; impl CheckerState { #[instrument(skip(self), level = "debug", fields(%signature))] pub fn check_signature(&self, signature: Signature) -> Result<Signature, CheckerError> { - Err(CheckerError::Unimplemented( - "signature checking".to_string(), - )) + match signature { + Signature::Set => Ok(Signature::Set), + Signature::Var(v) => { + let deref = self.lookup_signature(&v)?; + Ok(deref.clone()) + } + Signature::Ext { params, codomain } => Err(CheckerError::Unimplemented( + "extension signatures".to_string(), + )), + Signature::Theory(fields) => { + let fields = fields + .into_iter() + .map(|SigField { signature, name }| { + let signature = self.check_signature(signature)?; + Ok(SigField { name, signature }) + }) + .collect::<Result<Vec<_>, _>>()?; + Ok(Signature::Theory(fields)) + } + } } } diff --git a/src/checker_state.rs b/src/checker_state.rs index 8ec153d..31c3bde 100644 --- a/src/checker_state.rs +++ b/src/checker_state.rs @@ -343,4 +343,10 @@ impl CheckerState { Ok(()) } + + pub fn lookup_signature(&self, name: &String) -> Result<&Signature, CheckerError> { + self.wf_signatures + .get(name) + .map_or(Err(CheckerError::Unbound(name.clone())), Ok) + } } |