diff options
| -rw-r--r-- | examples/signature_merge.makkai | 12 | ||||
| -rw-r--r-- | src/checker_signature.rs | 53 | ||||
| -rw-r--r-- | src/checker_state.rs | 47 |
3 files changed, 84 insertions, 28 deletions
diff --git a/examples/signature_merge.makkai b/examples/signature_merge.makkai new file mode 100644 index 0000000..5f575d5 --- /dev/null +++ b/examples/signature_merge.makkai @@ -0,0 +1,12 @@ +let signature S = (n : Nat) -> Set +let signature U = (k : Bool) -> S +let signature W = (k : Bool)(n : Nat) -> Set + +let instance u :: U = for (k : Bool), for (n : Nat), (Nat :: Set) +let instance w :: W = u + +let signature F = (n : Nat) (m : Nat) -> Set +let signature G = (n : Nat) -> (m : Nat) -> Set + +let instance f :: F = for (n : Nat) (m : Nat), (Nat :: Set) +let instance g :: G = f diff --git a/src/checker_signature.rs b/src/checker_signature.rs index 2888568..0145e82 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -15,36 +15,67 @@ impl CheckerState { Ok(deref.clone()) } Signature::Ext { params, codomain } => { + if params.is_empty() { + return Err(CheckerError::Unimplemented( + "extension signature with empty params".to_string(), + )); + } let mut ctx = self.clone(); + + // a little juggling here to ensure that we merge names without + // collision, the pattern is: bind to something unique, recurse, + // fix the names which involves in particular messing about with + // counters let params = params .iter() .map(|p| { let set = ctx.check_set(&p.set)?; - let canon = ctx.make_element_binding(p.name.clone(), set.clone())?; + let canon = ctx.make_unique_name(); + ctx.add_element( + p.name.clone(), + Element::Var(canon.clone()).into(), + set.clone(), + )?; + ctx.add_element(canon.clone(), ElementValue::Hypothetical, set.clone())?; Ok(Param { set, name: canon }) }) .collect::<Result<Vec<_>, _>>()?; + + // use tactic "trust_me" + let snapshot = ctx.get_binder_counter(); let codomain = ctx.check_signature(codomain)?; + ctx.set_binder_counter(snapshot); - let result = if let Signature::Ext { + let (params, codomain) = if let Signature::Ext { params: inner, codomain: deep, } = codomain { let mut merged = params.clone(); merged.extend(inner.iter().cloned()); - Signature::Ext { - params: merged, - codomain: deep, - } + (merged, *deep) } else { - Signature::Ext { - params, - codomain: Box::new(codomain), - } + (params, codomain) }; - Ok(result) + // normalise + let mut ctx = self.clone(); + let params = params + .into_iter() + .map(|Param { name, set }| { + let canonical = ctx.make_element_binding(name, set.clone())?; + Ok(Param { + name: canonical, + set, + }) + }) + .collect::<Result<Vec<_>, _>>()?; + let codomain = ctx.check_signature(&codomain)?; + + Ok(Signature::Ext { + params, + codomain: Box::new(codomain), + }) } Signature::Theory(fields) => { let mut ctx = self.clone(); diff --git a/src/checker_state.rs b/src/checker_state.rs index 45d2dab..ad01d50 100644 --- a/src/checker_state.rs +++ b/src/checker_state.rs @@ -380,34 +380,39 @@ impl CheckerState { Ok(()) } - #[instrument(skip(self), level = "debug", fields(%name, %signature))] - pub fn add_signature( + fn _register_signature_fields( &mut self, - name: &String, - signature: Signature, + signature: &Signature, rebind: bool, ) -> Result<(), CheckerError> { - match &signature { + match signature { Signature::Theory(fields) => { for Field { name: field_name, carries: field_sig, } in fields { - let inner_name = self.make_unique_name(); - self.add_signature(&inner_name, field_sig.clone(), rebind)?; - self.add_signature_field(field_name, field_sig, &signature, rebind)?; + self._register_signature_fields(field_sig, rebind)?; + self.add_signature_field(field_name, field_sig, signature, rebind)?; } } Signature::Ext { codomain, .. } => { - let inner_name = self.make_unique_name(); - self.add_signature(&inner_name, (**codomain).clone(), rebind)?; + self._register_signature_fields(codomain, rebind)?; } - Signature::Set | Signature::Var(_) => (), - }; + _ => (), + } + Ok(()) + } + #[instrument(skip(self), level = "debug", fields(%name, %signature))] + pub fn add_signature( + &mut self, + name: &String, + signature: Signature, + rebind: bool, + ) -> Result<(), CheckerError> { + self._register_signature_fields(&signature, rebind)?; self.wf_signatures.insert(name.clone(), signature); - Ok(()) } @@ -453,14 +458,14 @@ impl CheckerState { // ----------------------------------------------------------------------------- // Bindings -fn _reserved_name(n: usize) -> String { - format!("#{}", n) +fn _reserved_name(n: usize, alter: bool) -> String { + format!("{}#{}", if alter { "@" } else { "" }, n) } impl CheckerState { fn _make_canonical_element(&mut self, name: String, set: Set) -> Result<String, CheckerError> { let n = self.binder_element.fetch_add(1, Ordering::Relaxed); - let canonical = _reserved_name(n); + let canonical = _reserved_name(n, false); self.add_element(name, Element::Var(canonical.clone()).into(), set)?; Ok(canonical) } @@ -487,10 +492,18 @@ impl CheckerState { #[instrument(skip(self))] pub fn make_unique_name(&mut self) -> String { let n = self.unique_name.fetch_add(1, Ordering::Relaxed); - _reserved_name(n) + _reserved_name(n, true) } pub fn reset_binders(&mut self) { self.binder_element.store(0, Ordering::Relaxed); } + + pub fn get_binder_counter(&self) -> usize { + self.binder_element.load(Ordering::Relaxed) + } + + pub fn set_binder_counter(&mut self, counter: usize) { + self.binder_element.store(counter, Ordering::Relaxed); + } } |