From: Mark Thom Date: Mon, 29 Apr 2019 04:23:34 +0000 (-0600) Subject: add unify_with_occurs_check/2 X-Git-Tag: v0.8.110~74 X-Git-Url: https://git.sagredo.dev/?a=commitdiff_plain;h=14d629492dd9ac892a80f5f236b8c3689b9abab6;p=scryer-prolog.git add unify_with_occurs_check/2 --- diff --git a/Cargo.toml b/Cargo.toml index 0bcfb2d6..9ff86ad0 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "scryer-prolog" -version = "0.8.74" +version = "0.8.75" authors = ["Mark Thom "] repository = "https://github.com/mthom/scryer-prolog" description = "A modern Prolog implementation written mostly in Rust." diff --git a/README.md b/README.md index da580e50..7c607860 100644 --- a/README.md +++ b/README.md @@ -228,6 +228,7 @@ The following predicates are built-in to Scryer. * `term_variables/2` * `throw/1` * `true/0` +* `unify_with_occurs_check/2` * `user:goal_expansion/2` * `user:term_expansion/2` * `var/1` diff --git a/src/prolog/clause_types.rs b/src/prolog/clause_types.rs index 63e46545..5a88745e 100644 --- a/src/prolog/clause_types.rs +++ b/src/prolog/clause_types.rs @@ -232,7 +232,8 @@ pub enum SystemClauseType { Succeed, TermVariables, TruncateLiftedHeapTo, - UnwindStack, + UnifyWithOccursCheck, + UnwindStack, WriteTerm } @@ -318,6 +319,7 @@ impl SystemClauseType { &SystemClauseType::Succeed => clause_name!("$succeed"), &SystemClauseType::TermVariables => clause_name!("$term_variables"), &SystemClauseType::TruncateLiftedHeapTo => clause_name!("$truncate_lh_to"), + &SystemClauseType::UnifyWithOccursCheck => clause_name!("$unify_with_occurs_check"), &SystemClauseType::UnwindStack => clause_name!("$unwind_stack"), &SystemClauseType::WriteTerm => clause_name!("$write_term"), } @@ -404,6 +406,7 @@ impl SystemClauseType { ("$term_variables", 2) => Some(SystemClauseType::TermVariables), ("$truncate_lh_to", 1) => Some(SystemClauseType::TruncateLiftedHeapTo), ("$unwind_stack", 0) => Some(SystemClauseType::UnwindStack), + ("$unify_with_occurs_check", 2) => Some(SystemClauseType::UnifyWithOccursCheck), ("$write_term", 4) => Some(SystemClauseType::WriteTerm), _ => None } diff --git a/src/prolog/lib/builtins.pl b/src/prolog/lib/builtins.pl index 1c8ea40d..c9b89016 100644 --- a/src/prolog/lib/builtins.pl +++ b/src/prolog/lib/builtins.pl @@ -17,8 +17,9 @@ expand_goal/2, expand_term/2, false/0, findall/3, findall/4, get_char/1, halt/0, number_chars/2, once/1, op/3, read_term/2, repeat/0, retract/1, set_prolog_flag/2, setof/3, - subsumes_term/2, term_variables/2, throw/1, true/0, write/1, - write_canonical/1, write_term/2, writeq/1]). + subsumes_term/2, term_variables/2, throw/1, true/0, + unify_with_occurs_check/2, write/1, write_canonical/1, + write_term/2, writeq/1]). % module resolution operator. :- op(600, xfy, :). @@ -846,3 +847,5 @@ subsumes_term(General, Specific) :- term_variables(SVs1, SVs2), SVs1 == SVs2 ). + +unify_with_occurs_check(X, Y) :- '$unify_with_occurs_check'(X, Y). diff --git a/src/prolog/machine/machine_state_impl.rs b/src/prolog/machine/machine_state_impl.rs index a5d11bb8..78e24f8f 100644 --- a/src/prolog/machine/machine_state_impl.rs +++ b/src/prolog/machine/machine_state_impl.rs @@ -340,6 +340,129 @@ impl MachineState { false } + fn bind_with_occurs_check(&mut self, r: Ref, addr: Addr) { + let mut fail = false; + + for value in self.acyclic_pre_order_iter(addr.clone()) { + if let HeapCellValue::Addr(addr) = value { + if let Some(inner_r) = addr.as_var() { + if r == inner_r { + fail = true; + break; + } + } + } + } + + self.fail = fail; + self.bind(r, addr); + } + + pub(super) fn unify_with_occurs_check(&mut self, a1: Addr, a2: Addr) { + let mut pdl = vec![a1, a2]; + let mut tabu_list: HashSet<(Addr, Addr)> = HashSet::new(); + + self.fail = false; + + while !(pdl.is_empty() || self.fail) { + let d1 = self.deref(pdl.pop().unwrap()); + let d2 = self.deref(pdl.pop().unwrap()); + + if d1 != d2 { + let d1 = self.store(d1); + let d2 = self.store(d2); + + if tabu_list.contains(&(d1.clone(), d2.clone())) { + continue; + } else { + tabu_list.insert((d1.clone(), d2.clone())); + } + + match (d1.clone(), d2.clone()) { + (Addr::AttrVar(h), addr) | (addr, Addr::AttrVar(h)) => + self.bind_with_occurs_check(Ref::AttrVar(h), addr), + (Addr::HeapCell(h), addr) | (addr, Addr::HeapCell(h)) => + self.bind_with_occurs_check(Ref::HeapCell(h), addr), + (Addr::StackCell(fr, sc), addr) | (addr, Addr::StackCell(fr, sc)) => + self.bind_with_occurs_check(Ref::StackCell(fr, sc), addr), + (Addr::Lis(a1), Addr::Str(a2)) | (Addr::Str(a2), Addr::Lis(a1)) => { + if let &HeapCellValue::NamedStr(n2, ref f2, _) = &self.heap[a2] { + if f2.as_str() == "." && n2 == 2 { + pdl.push(Addr::HeapCell(a1)); + pdl.push(Addr::HeapCell(a2 + 1)); + + pdl.push(Addr::HeapCell(a1 + 1)); + pdl.push(Addr::HeapCell(a2 + 2)); + + continue; + } + } + + self.fail = true; + }, + (Addr::Lis(a1), Addr::Con(Constant::String(ref mut s))) + | (Addr::Con(Constant::String(ref mut s)), Addr::Lis(a1)) => { + if match self.flags.double_quotes { + DoubleQuotes::Chars => self.deconstruct_chars(s, a1, &mut pdl), + DoubleQuotes::Codes => self.deconstruct_codes(s, a1, &mut pdl), + DoubleQuotes::Atom => false + } { + continue; + } + + self.fail = true; + }, + (Addr::Con(Constant::EmptyList), Addr::Con(Constant::String(ref s))) + | (Addr::Con(Constant::String(ref s)), Addr::Con(Constant::EmptyList)) + if !self.flags.double_quotes.is_atom() => { + if s.is_expandable() && s.is_empty() { + self.pstr_trail(s.clone()); + s.set_expandable(false); + continue; + } + + self.fail = !s.is_empty(); + }, + (Addr::Lis(a1), Addr::Lis(a2)) => { + pdl.push(Addr::HeapCell(a1)); + pdl.push(Addr::HeapCell(a2)); + + pdl.push(Addr::HeapCell(a1 + 1)); + pdl.push(Addr::HeapCell(a2 + 1)); + }, + (Addr::Con(Constant::String(ref mut s1)), + Addr::Con(Constant::String(ref mut s2))) => + self.fail = !(self.unify_strings(&mut pdl, s1, s2) + || self.unify_strings(&mut pdl, s2, s1)), + (Addr::Con(ref c1), Addr::Con(ref c2)) => + if c1 != c2 { + self.fail = true; + }, + (Addr::Str(a1), Addr::Str(a2)) => { + let r1 = &self.heap[a1]; + let r2 = &self.heap[a2]; + + if let &HeapCellValue::NamedStr(n1, ref f1, _) = r1 { + if let &HeapCellValue::NamedStr(n2, ref f2, _) = r2 { + if n1 == n2 && *f1 == *f2 { + for i in 1 .. n1 + 1 { + pdl.push(Addr::HeapCell(a1 + i)); + pdl.push(Addr::HeapCell(a2 + i)); + } + + continue; + } + } + } + + self.fail = true; + }, + _ => self.fail = true + }; + } + } + } + pub(super) fn unify(&mut self, a1: Addr, a2: Addr) { let mut pdl = vec![a1, a2]; let mut tabu_list: HashSet<(Addr, Addr)> = HashSet::new(); diff --git a/src/prolog/machine/system_calls.rs b/src/prolog/machine/system_calls.rs index bf0735fc..f52a15e5 100644 --- a/src/prolog/machine/system_calls.rs +++ b/src/prolog/machine/system_calls.rs @@ -1594,6 +1594,12 @@ impl MachineState { self.lifted_heap.truncate(lh_offset), _ => self.fail = true }, + &SystemClauseType::UnifyWithOccursCheck => { + let a1 = self[temp_v!(1)].clone(); + let a2 = self[temp_v!(2)].clone(); + + self.unify_with_occurs_check(a1, a2); + }, &SystemClauseType::UnwindStack => self.unwind_stack(), &SystemClauseType::WriteTerm => { let addr = self[temp_v!(1)].clone();