From: Mark Thom Date: Sat, 9 Feb 2019 20:57:03 +0000 (-0700) Subject: call goals in one batch after rebinding variables, add minatotask.pl, update README X-Git-Tag: v0.8.110~266 X-Git-Url: https://git.sagredo.dev/?a=commitdiff_plain;h=197d079281e4f0c6ec5759c1c24eb05e54dca68a;p=scryer-prolog.git call goals in one batch after rebinding variables, add minatotask.pl, update README --- diff --git a/README.md b/README.md index 09f3019d..b30412b1 100644 --- a/README.md +++ b/README.md @@ -39,6 +39,10 @@ Extend rusty-wam to include the following, among other features: * Attributed variables using the SICStus Prolog interface and semantics. Adding coroutines like `dif/2`, `freeze/2`, etc. is straightforward with attributed variables (_in progress_). + - [x] Support for `verify_attributes/3` in modules + - [ ] Support for `attribute_goals/2` at toplevel and + `project_attributes/2` in modules + - [ ] `call_residue_vars/2` * An occurs check. * Mode declarations. * Extensions for clp(FD). @@ -245,7 +249,7 @@ rusty-wam supports dynamic operators. Using the built-in arithmetic operators with the usual precedences, ``` -prolog> ?- display(-5 + 3 - (2 * 4) // 8). +prolog> ?- writeq(-5 + 3 - (2 * 4) // 8). '-'('+'('-'(5), 3), '//'('*'(2, 4), 8)) true. ``` diff --git a/src/prolog/instructions.rs b/src/prolog/instructions.rs index bb5bc1bb..deb04f98 100644 --- a/src/prolog/instructions.rs +++ b/src/prolog/instructions.rs @@ -249,6 +249,7 @@ pub enum SystemClauseType { InstallSCCCleaner, InstallInferenceCounter, ModuleOf, + RedoAttrVarBindings, RemoveCallPolicyCheck, RemoveInferenceCounter, RestoreCutPolicy, @@ -290,6 +291,7 @@ impl SystemClauseType { &SystemClauseType::InstallSCCCleaner => clause_name!("$install_scc_cleaner"), &SystemClauseType::InstallInferenceCounter => clause_name!("$install_inference_counter"), &SystemClauseType::ModuleOf => clause_name!("$module_of"), + &SystemClauseType::RedoAttrVarBindings => clause_name!("$redo_attr_var_bindings"), &SystemClauseType::RemoveCallPolicyCheck => clause_name!("$remove_call_policy_check"), &SystemClauseType::RemoveInferenceCounter => clause_name!("$remove_inference_counter"), &SystemClauseType::RestoreCutPolicy => clause_name!("$restore_cut_policy"), @@ -330,6 +332,7 @@ impl SystemClauseType { ("$install_scc_cleaner", 2) => Some(SystemClauseType::InstallSCCCleaner), ("$install_inference_counter", 3) => Some(SystemClauseType::InstallInferenceCounter), ("$module_of", 2) => Some(SystemClauseType::ModuleOf), + ("$redo_attr_var_bindings", 0) => Some(SystemClauseType::RedoAttrVarBindings), ("$remove_call_policy_check", 1) => Some(SystemClauseType::RemoveCallPolicyCheck), ("$remove_inference_counter", 2) => Some(SystemClauseType::RemoveInferenceCounter), ("$restore_cut_policy", 0) => Some(SystemClauseType::RestoreCutPolicy), diff --git a/src/prolog/lib/minatotask.pl b/src/prolog/lib/minatotask.pl new file mode 100644 index 00000000..fd1a4233 --- /dev/null +++ b/src/prolog/lib/minatotask.pl @@ -0,0 +1,112 @@ +/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + SICStus implementation of the Minato task. + Written Sept. 2017 by Markus Triska (triska@metalevel.at) + Public domain code. + + For more information, please see: + + https://www.metalevel.at/prolog/attributedvariables + =================================================== + + A ZDD node is either: + + -) a *leaf* of the form b(true) or b(false) + -) an *inner node* of the form ( Var -> Then ; Else ). + + In ZDDs, variables that are *not* encountered on a path to TRUE + must be 0. + + This module exports a single predicate: + + * variables_set_zdd(Vs, ZDD) + + It associates each variable in Vs with the given ZDD. For each + variable, the ZDD is stored as an attribute zdd_vs(ZDD, Vs). This + lets us reason about all variables that originally occurred. + + The internal unification hooks must be implemented so that only + admissible assignments of truth variables to variables succeed. + + In particular, the Minato task: + + ?- ZDD = ( X -> b(true) ; ( Y -> b(true) ; b(false) ) ), + Vs = [X,Y], + variables_set_zdd(Vs, ZDD), + Vs = [1,1]. + + no + + Other examples: + + ?- ZDD = ( X -> b(true) ; ( Y -> b(true) ; b(false) ) ), + Vs = [X,Y], + variables_set_zdd(Vs, ZDD), + X = 1. + + X = 1, + Y = 0, + Vs = [1,0] ? ; + + + ?- ZDD = ( X -> b(true) ; ( Y -> b(true) ; b(false) ) ), + Vs = [X,Y], + variables_set_zdd(Vs, ZDD), + X = 0. + + X = 0, + Vs = [0,Y] ? ; + +- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ + +:- module(zdd, [variables_set_zdd/2]). + +:- use_module(library(atts)). +:- use_module(library(dcgs)). +:- use_module(library(lists)). + +:- attribute zdd_vs/2. + +variables_set_zdd(Vs, ZDD) :- + maplist(set_zdd(ZDD, Vs), Vs). + +set_zdd(ZDD, Vs, V) :- + put_atts(V, +zdd_vs(ZDD, Vs)). + + +verify_attributes(Var, Value, Goals) :- + ( get_atts(Var, +zdd_vs(ZDD0,Vs)) -> + ( integer(Value) -> + zdd_restriction(ZDD0, Var, Value, ZDD) + ; throw(aliasing_not_implemented) + ), + phrase(remaining_vars_0(ZDD, Var, Vs), Goals) + ; Goals = [] + ). + +remaining_vars_0(b(true), Var, Vs) --> all_others_0(Vs, Var). +remaining_vars_0((_;_), _, _) --> []. + +all_others_0([], _) --> []. +all_others_0([V|Vs], Var) --> + ( { var(V), V \== Var } -> [V=0] + ; [] + ), + all_others_0(Vs, Var). + + +/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + Compute the *restriction* of the ZDD. + This means that Var has been instantiated to Value. +- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ + +zdd_restriction(b(T), _, _, b(T)). +zdd_restriction(( Var0 -> Then0 ; Else0), Var, Value, ZDD) :- + ( Var0 == Var -> + ( Value =:= 0 -> ZDD = Else0 + ; Value =:= 1 -> ZDD = Then0 + ; throw(no_boolean) + ) + ; zdd_restriction(Then0, Var, Value, Then), + zdd_restriction(Else0, Var, Value, Else), + ZDD = ( Var0 -> Then ; Else ) + ). diff --git a/src/prolog/machine/attributed_variables.pl b/src/prolog/machine/attributed_variables.pl new file mode 100644 index 00000000..c11ada22 --- /dev/null +++ b/src/prolog/machine/attributed_variables.pl @@ -0,0 +1,38 @@ +driver(Vars, Values) :- + iterate(Vars, Values, ListOfListsOfGoalLists), + '$redo_attr_var_bindings', %% the bindings list is emptied here. + call_goals(ListOfListsOfGoalLists), + '$restore_p_from_sfcp'. + +iterate([Var|VarBindings], [Value|ValueBindings], [ListOfGoalLists | ListsCubed]) :- + '$get_attr_list'(Var, Ls), + call_verify_attributes(Ls, Var, Value, ListOfGoalLists), + iterate(VarBindings, ValueBindings, ListsCubed). +iterate([], [], []). + +call_verify_attributes(Attrs, _, _, []) :- + var(Attrs), !. +call_verify_attributes([Attr|Attrs], Var, Value, [Goals|ListOfGoalLists]) :- + '$module_of'(M, Attr), % write the owning module Attr to M. + catch(M:verify_attributes(Var, Value, Goals), + error(evaluation_error((M:verify_attributes)/3), call_verify_attributes/3), + true), + call_verify_attributes(Attrs, Var, Value, ListOfGoalLists). + +call_goals([ListOfGoalLists | ListsCubed]) :- + call_goals_0(ListOfGoalLists), + call_goals(ListsCubed). +call_goals([]). + +call_goals_0([GoalList | GoalLists]) :- + ( var(GoalList), throw(error(instantiation_error, call_goals_0/1)) + ; true + ), + call_goals_1(GoalList), + call_goals_0(GoalLists). +call_goals_0([]). + +call_goals_1([Goal | Goals]) :- + call(Goal), + call_goals_1(Goals). +call_goals_1([]). diff --git a/src/prolog/machine/attributed_variables.rs b/src/prolog/machine/attributed_variables.rs index 4bf69bc8..685af0e6 100644 --- a/src/prolog/machine/attributed_variables.rs +++ b/src/prolog/machine/attributed_variables.rs @@ -1,35 +1,13 @@ use prolog::machine::*; -pub static VERIFY_ATTRS: &str = " -iterate([Var|VarBindings], [Value|ValueBindings]) :- - '$get_attr_list'(Var, Ls), - call_verify_attributes(Ls, Var, Value), - iterate(VarBindings, ValueBindings). -iterate([], []) :- '$restore_p_from_sfcp'. - -call_verify_attributes(Attrs, _, _) :- - var(Attrs), !. -call_verify_attributes([Attr|Attrs], Var, Value) :- - '$module_of'(M, Attr), % write the owning module Attr to M. - catch(M:verify_attributes(Var, Value, Goals), - error(evaluation_error((M:verify_attributes)/3), verify_attributes/3), - true), - call_verify_attributes_goals(Goals), - call_verify_attributes(Attrs, Var, Value). - -call_verify_attributes_goals(Goals) :- - var(Goals), throw(error(instantiation_error, call_verify_attributes_goals/1)). -call_verify_attributes_goals([Goal|Goals]) :- - call(Goal), !, call_verify_attributes_goals(Goals). -call_verify_attributes_goals([]). -"; +pub static VERIFY_ATTRS: &str = include_str!("attributed_variables.pl"); pub(super) type Bindings = Vec<(usize, Addr)>; pub(super) struct AttrVarInitializer { pub(super) bindings: Bindings, + cp_stack: Vec, pub(super) registers: Registers, - pub(super) special_form_cp: CodePtr, pub(super) verify_attrs_loc: usize } @@ -38,27 +16,42 @@ impl AttrVarInitializer { AttrVarInitializer { bindings: vec![], verify_attrs_loc: p, - special_form_cp: CodePtr::VerifyAttrInterrupt(p), + cp_stack: vec![], registers: vec![Addr::HeapCell(0); MAX_ARITY + 1] } } + #[inline] + pub(super) fn pop_code_ptr(&mut self) -> CodePtr { + self.cp_stack.pop().unwrap() + } + + #[inline] pub(super) fn reset(&mut self) { - self.special_form_cp = CodePtr::VerifyAttrInterrupt(self.verify_attrs_loc); + self.cp_stack.clear(); + self.bindings.clear(); } } impl MachineState { - pub(super) fn add_attr_var_binding(&mut self, h: usize, addr: Addr) + pub(super) fn push_attr_var_binding(&mut self, h: usize, addr: Addr) { + if self.attr_var_init.bindings.is_empty() { + self.attr_var_init.cp_stack.push(self.p.clone() + 1); + self.p = CodePtr::VerifyAttrInterrupt(self.attr_var_init.verify_attrs_loc); + } + self.attr_var_init.bindings.push((h, addr)); + } - if let &CodePtr::VerifyAttrInterrupt(_) = &self.p { - return; - } + fn populate_var_and_value_lists(&mut self) -> (Addr, Addr) { + let iter = self.attr_var_init.bindings.iter().map(|(ref h, _)| Addr::AttrVar(*h)); + let var_list_addr = Addr::HeapCell(self.heap.to_list(iter)); + + let iter = self.attr_var_init.bindings.iter().map(|(_, ref addr)| addr.clone()); + let value_list_addr = Addr::HeapCell(self.heap.to_list(iter)); - mem::swap(&mut self.attr_var_init.special_form_cp, &mut self.p); - self.attr_var_init.special_form_cp += 1; + (var_list_addr, value_list_addr) } pub(super) @@ -68,28 +61,24 @@ impl MachineState { STEP 2: Write the list of bindings to two lists in the heap, one for vars, one for values. STEP 3: Swap the machine's Registers for attr_var_init's Registers. STEP 4: Pass the addresses of the lists to iterate in the attr_vars special form. - STEP 5: Restore AttrVarInitializer::special_form_cp to self.p. - STEP 6: Swap the bindings' Registers back for the machine's Registers. - STEP 7: Redo the bindings. - STEP 8: Continue. + Call verify_attributes/3 wherever applicable. + STEP 5: Redo the bindings. + STEP 6: Call the goals. + STEP 7: Pop the top of AttrVarInitializer::cp_stack to self.p. + STEP 8: Swap the AttrVarInitializer's Registers back for the machine's Registers. */ + // STEP 1. for (h, _) in &self.attr_var_init.bindings { self.heap[*h] = HeapCellValue::Addr(Addr::AttrVar(*h)); } - let (var_list_addr, value_list_addr) = { - let iter = self.attr_var_init.bindings.iter().map(|(ref h, _)| Addr::AttrVar(*h)); - let var_list_addr = Addr::HeapCell(self.heap.to_list(iter)); - - let iter = self.attr_var_init.bindings.iter().map(|(_, ref addr)| addr.clone()); - let value_list_addr = Addr::HeapCell(self.heap.to_list(iter)); - - (var_list_addr, value_list_addr) - }; - + // STEP 2. + let (var_list_addr, value_list_addr) = self.populate_var_and_value_lists(); + // STEP 3. mem::swap(&mut self.registers, &mut self.attr_var_init.registers); + // STEP 4. self[temp_v!(1)] = var_list_addr; self[temp_v!(2)] = value_list_addr; } diff --git a/src/prolog/machine/machine_state.rs b/src/prolog/machine/machine_state.rs index ae81e94a..ffa6da86 100644 --- a/src/prolog/machine/machine_state.rs +++ b/src/prolog/machine/machine_state.rs @@ -378,7 +378,7 @@ pub(crate) trait CallPolicy: Any { machine_st.pstr_trail.truncate(machine_st.pstr_tr); machine_st.heap.truncate(machine_st.or_stack[b].h); - + machine_st.hb = machine_st.heap.h; machine_st.p += offset; diff --git a/src/prolog/machine/machine_state_impl.rs b/src/prolog/machine/machine_state_impl.rs index 1df24b01..95834df9 100644 --- a/src/prolog/machine/machine_state_impl.rs +++ b/src/prolog/machine/machine_state_impl.rs @@ -109,7 +109,7 @@ impl MachineState { self.trail(TrailRef::Ref(Ref::StackCell(fr, sc))); }, _ => { - self.add_attr_var_binding(h, addr.clone()); + self.push_attr_var_binding(h, addr.clone()); self.heap[h] = HeapCellValue::Addr(addr); self.trail(TrailRef::Ref(Ref::AttrVar(h))); } @@ -2260,7 +2260,7 @@ impl MachineState { self.tr, self.pstr_tr, self.heap.h, - self.b0, + self.b0, self.num_of_args); self.b = self.or_stack.len(); diff --git a/src/prolog/machine/mod.rs b/src/prolog/machine/mod.rs index 4990078d..6143ccee 100644 --- a/src/prolog/machine/mod.rs +++ b/src/prolog/machine/mod.rs @@ -325,10 +325,9 @@ impl Machine { match compile_special_form(self, VERIFY_ATTRS.as_bytes()) { Ok(code) => { self.machine_st.attr_var_init.verify_attrs_loc = self.code_repo.code.len(); - self.machine_st.attr_var_init.reset(); self.code_repo.code.extend(code.into_iter()); }, - Err(_e) => panic!("Machine::compile_special_forms() failed") + Err(_) => panic!("Machine::compile_special_forms() failed") } } diff --git a/src/prolog/machine/system_calls.rs b/src/prolog/machine/system_calls.rs index 64837de7..c531b931 100644 --- a/src/prolog/machine/system_calls.rs +++ b/src/prolog/machine/system_calls.rs @@ -399,6 +399,13 @@ impl MachineState { _ => self.fail = true }; }, + &SystemClauseType::RedoAttrVarBindings => { + let mut bindings = mem::replace(&mut self.attr_var_init.bindings, vec![]); + + for (h, addr) in bindings { + self.heap[h] = HeapCellValue::Addr(addr); + } + }, &SystemClauseType::RemoveCallPolicyCheck => { let restore_default = match call_policy.downcast_mut::().ok() { @@ -443,26 +450,9 @@ impl MachineState { CWILCallPolicy.") }, &SystemClauseType::RestoreCodePtrFromSpecialFormCP => { - self.p = mem::replace(&mut self.attr_var_init.special_form_cp, - CodePtr::VerifyAttrInterrupt(self.attr_var_init.verify_attrs_loc)); + self.p = self.attr_var_init.pop_code_ptr(); mem::swap(&mut self.registers, &mut self.attr_var_init.registers); - let mut bindings = vec![]; - mem::swap(&mut bindings, &mut self.attr_var_init.bindings); - - for (h, addr) in bindings { - let deref_h = self.store(self.deref(Addr::AttrVar(h))); - - if &Addr::AttrVar(h) != &deref_h { - if &deref_h != &addr { - self.fail = true; - return Ok(()); - } - } else { - self.heap[h] = HeapCellValue::Addr(addr); - } - } - return Ok(()); }, &SystemClauseType::RestoreCutPolicy => { @@ -639,8 +629,6 @@ impl MachineState { } }; - self.set_p(); - - Ok(()) + Ok(self.set_p()) } } diff --git a/src/tests.rs b/src/tests.rs index 495b875e..2887677b 100644 --- a/src/tests.rs +++ b/src/tests.rs @@ -2164,11 +2164,6 @@ fn test_queries_on_attributed_variables() get_atts(V, my_mod, L).", [["A = _69", "L = [dif(1), frozen(a)]", "V = _27"], ["A = _69", "L = [dif(1), dif(2)]", "V = _27"]]); -// assert_prolog_success!(&mut wam, "?- put_atts(V, my_mod, [dif(1), dif(2), frozen(a)]), -// ( put_atts(V, my_mod, -dif(2)), V = f(a) -// ; put_atts(V, my_mod, -frozen(_)), get_atts(V, my_mod, L) ).", -// [["L = _69", "V = f(a)"], -// ["L = [dif(1), dif(2)]", "V = _27"]]); assert_prolog_success!(&mut wam, "?- put_atts(V, my_mod, [dif(1), dif(2), frozen(a), frozen(b)]), ( put_atts(V, my_mod, -dif(2)) ; put_atts(V, my_mod, -frozen(A)) ), get_atts(V, my_mod, L).", @@ -2188,4 +2183,22 @@ fn test_queries_on_attributed_variables() assert_prolog_success!(&mut wam, "?- put_atts(V, my_mod, [dif(1), frozen(a), dif(2), frozen(b)]), put_atts(V, my_mod, -dif(A)), get_atts(V, my_mod, Ls).", [["A = _98", "Ls = [frozen(a), frozen(b)]", "V = _31"]]); + + submit(&mut wam, include_str!("./prolog/lib/minatotask.pl")); + submit(&mut wam, ":- use_module(library(zdd))."); + + assert_prolog_failure!(&mut wam, "?- ZDD = ( X -> b(true) ; ( Y -> b(true) ; b(false) ) ), + Vs = [X,Y], + variables_set_zdd(Vs, ZDD), + Vs = [1,1]."); + assert_prolog_success!(&mut wam, "?- ZDD = ( X -> b(true) ; ( Y -> b(true) ; b(false) ) ), + Vs = [X,Y], + variables_set_zdd(Vs, ZDD), + X = 1.", + [["X = 1", "Y = 0", "Vs = [1, 0]", "ZDD = 1->b(true);0->b(true);b(false)"]]); + assert_prolog_success!(&mut wam, "?- ZDD = ( X -> b(true) ; ( Y -> b(true) ; b(false) ) ), + Vs = [X,Y], + variables_set_zdd(Vs, ZDD), + X = 0.", + [["Vs = [0, _59]", "X = 0", "Y = _59", "ZDD = 0->b(true);_59->b(true);b(false)"]]); }