diff options
| -rw-r--r-- | examples/equality.makkai | 6 | ||||
| -rw-r--r-- | src/checker_set.rs | 6 | ||||
| -rw-r--r-- | src/checker_signature.rs | 23 | ||||
| -rw-r--r-- | src/checker_state.rs | 8 |
4 files changed, 37 insertions, 6 deletions
diff --git a/examples/equality.makkai b/examples/equality.makkai index 438e930..ac668c7 100644 --- a/examples/equality.makkai +++ b/examples/equality.makkai @@ -19,7 +19,11 @@ let instance eqThree :: SetWithEquivRelation = { | one. z => case y of [ zero. w => Empty :: Set | one. w => Unit :: Set | two. w => Empty :: Set ] | two. z => case y of [ zero. w => Empty :: Set | one. w => Empty :: Set | two. w => Unit :: Set ] ], .Reflexive = for (x: Three), case x of [ zero. z => <pt> | one. z => <pt> | two. z => <pt> ], - .Symmetric = for (x: Three)(y: Three)(r: set-of(Relation x y)), <pt>, + .Symmetric = for (x: Three) (y: Three) (r: set-of(Relation x y)), + case x of [ zero. z => case y of [ zero. z => <r> | one. z => <r> | two. z => <r> ] + | one. z => case y of [ zero. z => <r> | one. z => <r> | two. z => <r> ] + | two. z => case y of [ zero. z => <r> | one. z => <r> | two. z => <r> ] + ], .Transitive = for (x: Three)(y: Three)(z: Three)(r: set-of(Relation x y))(s: set-of(Relation y z)), <pt> } diff --git a/src/checker_set.rs b/src/checker_set.rs index 1a89631..83d97a1 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -103,13 +103,15 @@ impl CheckerState { } Element::Var(v) => { let lookup = self.lookup_element(&v)?; + let container = self.check_set(&lookup.container)?; // TODO: necessary why? + // we have previously done the work to discover the type of // this element, so what we're claiming now must match! - if !self.equal(set, &lookup.container) { + if !self.equal(set, &container) { return Err(CheckerError::WrongSetForElement { value: element.clone().into(), claimed: set.clone(), - real: lookup.container.clone(), + real: container, }); } // If we found a formal binding, we have no value to report. diff --git a/src/checker_signature.rs b/src/checker_signature.rs index ab54fd1..9d0bffe 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -107,7 +107,7 @@ impl CheckerState { } } - #[instrument(skip(self), level = "debug", fields(%instance, ?signature))] + #[instrument(skip(self), level = "debug", fields(%instance, signature=%signature.map(|s| s.to_string()).unwrap_or_default()) )] pub fn check_instance( &self, instance: &Instance, @@ -140,10 +140,24 @@ impl CheckerState { claimed: signature.clone(), }); }; + println!("{self}"); let element = self.check_element(element, set)?; Ok(Instance::ElementCoerce(element)) } else { // todo!("how do we handle check_element without a set?"); + println!("THISISATTODO"); + // quick hack: + let element = if let Element::Var(v) = element { + let lookup = self.lookup_element(&v)?; + if let ElementValue::Concrete(ref x) = lookup.value { + x.clone() + } else { + element.clone() + } + } else { + element.clone() + }; + Ok(Instance::ElementCoerce(element.clone())) } } @@ -491,6 +505,7 @@ impl CheckerState { claimed: signature.clone(), }); } + let mut ctx = self.clone(); let inst_params = zip(inst_params, sig_params) .map( @@ -519,6 +534,12 @@ impl CheckerState { Element::Var(set_n.clone()).into(), set_s.clone(), )?; + // TODO should this be unconditional? + ctx.add_element( + set_n.clone(), + ElementValue::Hypothetical, + set_s.clone() + )?; Ok(Param { name: set_n.clone(), set: set_s, diff --git a/src/checker_state.rs b/src/checker_state.rs index a88c6b0..77abbdd 100644 --- a/src/checker_state.rs +++ b/src/checker_state.rs @@ -464,8 +464,12 @@ fn _reserved_name(n: usize, alter: bool) -> String { 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, false); + let canonical = if name.starts_with("#") { + name.clone() + } else { + let n = self.binder_element.fetch_add(1, Ordering::Relaxed); + _reserved_name(n, false) + }; self.add_element(name, Element::Var(canonical.clone()).into(), set)?; Ok(canonical) } |