* 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).
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.
```
InstallSCCCleaner,
InstallInferenceCounter,
ModuleOf,
+ RedoAttrVarBindings,
RemoveCallPolicyCheck,
RemoveInferenceCounter,
RestoreCutPolicy,
&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"),
("$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),
--- /dev/null
+/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+ SICStus implementation of the Minato task.
+ 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 )
+ ).
--- /dev/null
+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([]).
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<CodePtr>,
pub(super) registers: Registers,
- pub(super) special_form_cp: CodePtr,
pub(super) verify_attrs_loc: usize
}
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)
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;
}
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;
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)));
}
self.tr,
self.pstr_tr,
self.heap.h,
- self.b0,
+ self.b0,
self.num_of_args);
self.b = self.or_stack.len();
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")
}
}
_ => 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::<CWILCallPolicy>().ok() {
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 => {
}
};
- self.set_p();
-
- Ok(())
+ Ok(self.set_p())
}
}
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).",
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)"]]);
}
projects / scryer-prolog.git / commitdiff