add unify_with_occurs_check/2

diff --git a/Cargo.toml b/Cargo.toml
index 0bcfb2d68647a8148943175efe63fb2f1061f357..9ff86ad0322e3247f7042683ce6bf18e4ed67fd0 100644 (file)
--- 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 <[email protected]>"]
 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 da580e50ae8ecc1ad430bee3162eb39f0a63a482..7c607860700cb64cf477fbc7296862aa66012946 100644 (file)
--- 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 63e46545bc8d40889816c06f633f3f3aa9ca41d6..5a88745ef2f1ff108d65f71ee9361ef26d929f31 100644 (file)
--- 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 1c8ea40d5c34fb205f8750586f5cc8e2901eb02e..c9b89016b0d4a1d8a1cc0c42c57417b904df199b 100644 (file)
--- 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 a5d11bb860d761cfc722d3922de1a7802c08abd0..78e24f8f2f45d16209aff85ca3e9258f23fc5154 100644 (file)
--- 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 bf0735fc4b9409dc6fc15aca321ca736b7d4fe9d..f52a15e5e3ce8427b9279caf42a6b8fb6a0db7c6 100644 (file)
--- 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();