diff options
| author | tslil <tslil@posteo.de> | 2026-04-28 15:00:45 +0100 |
|---|---|---|
| committer | tslil <tslil@posteo.de> | 2026-04-28 17:07:32 +0100 |
| commit | 67e3285ae6c7b94adc1983dcff18a009455bc582 (patch) | |
| tree | d33fc75fdb041dd92d089f2039ab08902f09d95c /src/checker_set.rs | |
| parent | ecc2c04edbcfdd097377683c28b92cd10e437d35 (diff) | |
snapshot of working through instances/singatures <> sets/elements
Diffstat (limited to 'src/checker_set.rs')
| -rw-r--r-- | src/checker_set.rs | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/checker_set.rs b/src/checker_set.rs index 729ce08..86661c7 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -15,11 +15,7 @@ impl CheckerState { .into_iter() .map(|RecordField { name, set }| { let set = ctx.check_set(set)?; - ctx.add_element( - name.clone(), - Value::Hypothetical(set.clone()), - set.clone(), - )?; + ctx.make_element_binding(name.clone(), set.clone())?; Ok(RecordField { name, set }) }) .collect::<Result<Vec<_>, _>>()?; @@ -38,10 +34,16 @@ impl CheckerState { .collect::<Result<Vec<_>, _>>()?; Ok(Set::Variant(fields)) } - Set::ClaimedSet(_) => Err(CheckerError::Unimplemented("instances as sets".to_string())), + Set::ClaimedSet(instance) => { + let instance = self.check_instance(instance, &Signature::Set)?; + Ok(Set::ClaimedSet(instance)) + } Set::Var(v) => { let deref = self.lookup_set(&v)?; - Ok(deref.clone()) + match deref { + SetValue::Hypothetical => Ok(Set::Var(v)), + SetValue::Concrete(deref) => Ok(deref.clone()), + } } } } @@ -334,7 +336,7 @@ impl CheckerState { } else { new_context.add_element( binding_name.clone(), - Value::Hypothetical(field_set.clone()), + Value::Hypothetical, binding_set, )?; new_context.check_element(arm.body.clone().into(), set)? |