diff options
Diffstat (limited to 'src/checker_signature.rs')
| -rw-r--r-- | src/checker_signature.rs | 14 |
1 files changed, 2 insertions, 12 deletions
diff --git a/src/checker_signature.rs b/src/checker_signature.rs index 55682a9..39a35b4 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -99,12 +99,6 @@ impl CheckerState { name: name.clone(), carries: signature, }); - // We must iteratively add the entire signature so that - // field lookup does something, as we rely on that for type - // checking. We could hack together a signature i suppose, - // but the cleanest thing is to add the truncations of this - // signature. In any event the context is discarded - // afterward. ctx.add_signature(&temp_name, Signature::Theory(new_fields.clone()), true)?; } Ok(Signature::Theory(new_fields)) @@ -112,11 +106,6 @@ impl CheckerState { } } - // the goal here is to spread the love: if we are adding a hypothetical of - // some signature _ : theory { ... } then we must recurse into all of those - // fields and add hypotheticals for them---but, we need to build the tree as - // we go, giving them the concrete value of their path from the root (our - // canonical form). fn _recursively_add_hypothetical_instance( &mut self, name: String, @@ -139,7 +128,7 @@ impl CheckerState { }; // handle the special case canonical form for _ :: Set if signature == Signature::Set { - self.add_set(name.clone(), Set::ClaimedSet(self_instance.clone()))?; + self.add_set(name.clone(), Set::ClaimedSet(self_instance.clone()), false)?; } self.add_instance(name.clone(), value, signature.clone())?; if let Signature::Theory(fields) = signature { @@ -267,6 +256,7 @@ impl CheckerState { ctx.add_set( f_n.clone(), Set::ClaimedSet(Instance::Var(f_n.clone())), + false, )?; } |