add unify_with_occurs_check/2

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "scryer-prolog"
-version = "0.8.74"
+version = "0.8.75"
 authors = ["Mark Thom <markjordanthom@gmail.com>"]
 repository = "https://github.com/mthom/scryer-prolog"
 description = "A modern Prolog implementation written mostly in Rust."

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`

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
         }

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,
+	subsumes_term/2, term_variables/2, throw/1, true/0,
-	write_canonical/1, write_term/2, writeq/1]).
+	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).

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();

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();