tweak head check
This commit is contained in:
@@ -24,10 +24,10 @@ impl<'a> TermMarker<'a> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn occurs_shallowly_in_head(&self, var: &'a Var, term_loc: GenContext, r: usize) -> bool
|
fn occurs_shallowly_in_head(&self, var: &'a Var, r: usize) -> bool
|
||||||
{
|
{
|
||||||
match (term_loc, self.bindings.get(var).unwrap()) {
|
match self.bindings.get(var).unwrap() {
|
||||||
(GenContext::Head, &VarData::Temp(_, _, ref tvd)) =>
|
&VarData::Temp(_, _, ref tvd) =>
|
||||||
tvd.use_set.contains(&(GenContext::Head, r)),
|
tvd.use_set.contains(&(GenContext::Head, r)),
|
||||||
_ => false
|
_ => false
|
||||||
}
|
}
|
||||||
@@ -304,10 +304,14 @@ impl<'a> TermMarker<'a> {
|
|||||||
}
|
}
|
||||||
},
|
},
|
||||||
Level::Deep if is_new_var =>
|
Level::Deep if is_new_var =>
|
||||||
if self.occurs_shallowly_in_head(var, term_loc, r.reg_num()) {
|
if let GenContext::Head = term_loc {
|
||||||
|
if self.occurs_shallowly_in_head(var, r.reg_num()) {
|
||||||
target.push(Target::subterm_to_value(r));
|
target.push(Target::subterm_to_value(r));
|
||||||
} else {
|
} else {
|
||||||
target.push(Target::subterm_to_variable(r));
|
target.push(Target::subterm_to_variable(r));
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
target.push(Target::subterm_to_variable(r));
|
||||||
},
|
},
|
||||||
Level::Deep =>
|
Level::Deep =>
|
||||||
target.push(Target::subterm_to_value(r))
|
target.push(Target::subterm_to_value(r))
|
||||||
|
|||||||
Reference in New Issue
Block a user