delay attributed variables goal, naively correct dif/2

Cargo.toml

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

src/prolog/instructions.rs

@@ -53,6 +53,17 @@ pub enum Line {
     Query(QueryInstruction)
 }
 
+impl Line {
+    pub fn is_head_instr(&self) -> bool {
+        match self {
+            &Line::Cut(_) => true,            
+            &Line::Fact(_) => true,
+            &Line::Query(_) => true,
+            _ => false
+        }
+    }
+}
+
 #[derive(Clone)]
 pub enum ArithmeticInstruction {
     Add(ArithmeticTerm, ArithmeticTerm, usize),

src/prolog/lib/dif.pl

@@ -1,6 +1,7 @@
 :- module(dif, [dif/2]).
 
 :- use_module(library(atts)).
+:- use_module(library(lists), [append/3]).
 
 :- attribute dif/1.
 
@@ -16,8 +17,20 @@ dif_set_variables([Var|Vars], X, Y) :-
     put_dif_att(Var, X, Y),
     dif_set_variables(Vars, X, Y).
 
+append_goals([], _).
+append_goals([Var|Vars], Goals) :-
+    (   get_atts(Var, +dif(VarGoals)) ->
+	append(Goals, VarGoals, NewGoals0),
+	sort(NewGoals0, NewGoals)
+    ;   NewGoals = Goals
+    ),
+    put_atts(Var, +dif(NewGoals)),
+    append_goals(Vars, Goals).
+
 verify_attributes(Var, Value, Goals) :-
-    (   get_atts(Var, +dif(Goals)) -> true
+    (   get_atts(Var, +dif(Goals)) ->
+	term_variables(Value, ValueVars),
+	append_goals(ValueVars, Goals)
     ;   Goals = []
     ).
 

src/prolog/lib/lists.pl

@@ -13,7 +13,7 @@ length(Xs, N) :-
     N >= 0, !,
     '$skip_max_list'(M, N, Xs, Xs0),
     (  Xs0 == [] -> N = M
-    ;  var(Xs0)  -> R is N-M, length_rundown(Xs0, R)).
+    ;  var(Xs0)  -> R is N-M, nl, length_rundown(Xs0, R)).
 length(_, N) :-
     integer(N), !,
     throw(error(domain_error(not_less_than_zero, N), length/2)).
@@ -25,7 +25,7 @@ length_addendum([_|Xs], N, M) :-
     M1 is M + 1,
     length_addendum(Xs, N, M1).
 
-length_rundown([], 0) :- !.
+length_rundown(Xs, 0) :- !, Xs = [].
 length_rundown([_|Xs], N) :-
     N1 is N-1,
     length_rundown(Xs, N1).

src/prolog/machine/machine_indices.rs

@@ -280,7 +280,7 @@ pub enum DynamicTransactionType {
 
 #[derive(Clone, Copy, PartialOrd, Ord, PartialEq, Eq)]
 pub enum REPLCodePtr {
-    CompileBatch,    
+    CompileBatch,
     SubmitQueryAndPrintResults
 }
 
@@ -291,7 +291,7 @@ pub enum CodePtr {
     Local(LocalCodePtr),
     DynamicTransaction(DynamicTransactionType, LocalCodePtr), // the type of transaction, the return pointer.
     REPL(REPLCodePtr, LocalCodePtr), // the REPL code, the return pointer.
-    VerifyAttrInterrupt(usize), // location of the verify attribute interrupt code in the CodeDir.    
+    VerifyAttrInterrupt(usize) // location of the verify attribute interrupt code in the CodeDir.
 }
 
 impl CodePtr {
@@ -442,7 +442,7 @@ pub struct IndexStore {
     pub(super) op_dir: OpDir,
 }
 
-impl IndexStore {    
+impl IndexStore {
     pub fn predicate_exists(&self, name: ClauseName, module: ClauseName, arity: usize,
                             op_spec: Option<SharedOpDesc>)
                             -> bool

src/prolog/machine/mod.rs

@@ -675,15 +675,10 @@ impl MachineState {
         output
     }
 
-    fn execute_instr(&mut self, indices: &mut IndexStore, policies: &mut MachinePolicies,
+    fn dispatch_instr(&mut self, instr: &Line, indices: &mut IndexStore, policies: &mut MachinePolicies,
-                     code_repo: &CodeRepo, prolog_stream: &mut PrologStream)
+                      prolog_stream: &mut PrologStream)
     {
-        let instr = match code_repo.lookup_instr(self.last_call, &self.p) {
+        match instr {
-            Some(instr) => instr,
-            None => return
-        };
-
-        match instr.as_ref() {
             &Line::Arithmetic(ref arith_instr) =>
                 self.execute_arith_instr(arith_instr),
             &Line::Choice(ref choice_instr) =>
@@ -709,6 +704,17 @@ impl MachineState {
         }
     }
 
+    fn execute_instr(&mut self, indices: &mut IndexStore, policies: &mut MachinePolicies,
+                     code_repo: &CodeRepo, prolog_stream: &mut PrologStream)
+    {
+        let instr = match code_repo.lookup_instr(self.last_call, &self.p) {
+            Some(instr) => instr,
+            None => return
+        };
+
+        self.dispatch_instr(instr.as_ref(), indices, policies, prolog_stream);
+    }
+
     fn backtrack(&mut self)
     {
         if self.b > 0 {
@@ -727,6 +733,73 @@ impl MachineState {
         }
     }
 
+    fn check_machine_index(&mut self, code_repo: &CodeRepo) -> bool {
+        match self.p {
+            CodePtr::Local(LocalCodePtr::DirEntry(p))
+                if p < code_repo.code.len() => {},
+            CodePtr::Local(LocalCodePtr::UserTermExpansion(p))
+                if p < code_repo.term_expanders.len() => {},
+            CodePtr::Local(LocalCodePtr::UserTermExpansion(_)) =>
+                self.fail = true,
+            CodePtr::Local(LocalCodePtr::UserGoalExpansion(p))
+                if p < code_repo.goal_expanders.len() => {},
+            CodePtr::Local(LocalCodePtr::UserGoalExpansion(_)) =>
+                self.fail = true,
+            CodePtr::Local(LocalCodePtr::InSituDirEntry(p))
+                if p < code_repo.in_situ_code.len() => {},
+            CodePtr::Local(_) | CodePtr::REPL(..) =>
+                return false,
+            CodePtr::DynamicTransaction(..) => {
+                // prevent use of dynamic transactions from
+                // succeeding in expansions. this will be toggled
+                // back to true later.
+                self.fail = true;
+                return false;
+            },
+            _ => {}
+        }
+
+        true
+    }
+
+    // return true iff verify_attr_interrupt is called.
+    fn verify_attr_stepper(&mut self, indices: &mut IndexStore, policies: &mut MachinePolicies,
+                           code_repo: &mut CodeRepo, prolog_stream: &mut PrologStream)
+                           -> bool
+    {
+        loop {
+            let instr = match code_repo.lookup_instr(self.last_call, &self.p) {
+                Some(instr) => {
+                    if instr.as_ref().is_head_instr() {
+                        instr
+                    } else {
+                        let cp = self.p.local();
+                        self.run_verify_attr_interrupt(cp);
+                        return true;
+                    }
+                },
+                None => return false
+            };
+
+            self.dispatch_instr(instr.as_ref(), indices, policies, prolog_stream);
+
+            if self.fail {
+                self.backtrack();
+            }
+
+            if !self.check_machine_index(code_repo) {
+                return false;
+            }
+        }
+    }
+
+    fn run_verify_attr_interrupt(&mut self, cp: LocalCodePtr) {
+        let p = self.attr_var_init.verify_attrs_loc;
+
+        self.attr_var_init.cp = cp;
+        self.verify_attr_interrupt(p);
+    }
+
     fn query_stepper(&mut self, indices: &mut IndexStore, policies: &mut MachinePolicies,
                      code_repo: &mut CodeRepo, prolog_stream: &mut PrologStream)
     {
@@ -738,30 +811,22 @@ impl MachineState {
             }
 
             match self.p {
-                CodePtr::Local(LocalCodePtr::DirEntry(p))
+                CodePtr::VerifyAttrInterrupt(_)  => {
-                    if p < code_repo.code.len() => {},
+                    self.p = CodePtr::Local(self.attr_var_init.cp + 1);
-                CodePtr::Local(LocalCodePtr::UserTermExpansion(p))
+
-                    if p < code_repo.term_expanders.len() => {},
+                    if !self.verify_attr_stepper(indices, policies, code_repo, prolog_stream) {
-                CodePtr::Local(LocalCodePtr::UserTermExpansion(_)) =>
+                        if self.fail {
-                    self.fail = true,
+                            break;
-                CodePtr::Local(LocalCodePtr::UserGoalExpansion(p))
+                        }
-                    if p < code_repo.goal_expanders.len() => {},
+                        
-                CodePtr::Local(LocalCodePtr::UserGoalExpansion(_)) =>
+                        let cp = self.p.local();
-                    self.fail = true,
+                        self.run_verify_attr_interrupt(cp);                    
-                CodePtr::Local(LocalCodePtr::InSituDirEntry(p))
+                    }
-                    if p < code_repo.in_situ_code.len() => {},
-                CodePtr::Local(_) | CodePtr::REPL(..) =>
-                    break,
-                CodePtr::VerifyAttrInterrupt(p) =>
-                    self.verify_attr_interrupt(p),
-                CodePtr::DynamicTransaction(..) => {
-                    // prevent use of dynamic transactions from
-                    // succeeding in expansions. this will be toggled
-                    // back to true later.
-                    self.fail = true;
-                    break;
                 },
-                _ => {}
+                _ =>
+                    if !self.check_machine_index(code_repo) {
+                        break;
+                    }
             }
         }
     }