Try to implement bagof/3, but I am not 100% sure it is correct

1 files changed, 149 insertions, 0 deletions

diff --git a/stdlib.pl b/stdlib.pl
index 5c35fbc..c4005cd 100644
--- a/stdlib.pl
+++ b/stdlib.pl
@@ -172,6 +172,50 @@ member(X, [X|_]).
 member(X, [_|Tail]) :-
 	member(X, Tail).
 
+append([], Ys, Ys).
+append([X|Xs], Ys, [X|Zs]) :-
+	append(Xs, Ys, Zs).
+
+length([], 0).
+length([_|T], Len) :-
+	length(T, Len0),
+	Len is Len0 + 1.
+
+unique([], []).
+unique([H|T], [H|Rest]) :-
+	findall(_, (member(X, T), X == H), []),
+	!,
+	unique(T, Rest).
+unique([H|T], Rest) :-
+	unique(T, Rest).
+
+union(A, B, C) :-
+	append(A, B, C0),
+	unique(C0, C).
+
+difference(A, B, Diff) :-
+	append(A, B, AB),
+	unique_in(AB, AB, Diff).
+
+unique_in([], _, []).
+unique_in([H|T], L, [H|Rest]) :-
+	findall(_, (member(X, L), X == H), [_]),
+	!,
+	unique_in(T, L, Rest).
+unique_in([H|T], L, Rest) :-
+	unique_in(T, L, Rest).
+
+include(_, [], []).
+include(Goal, [X|Xs], Included) :-
+	Goal =.. L,
+	append(L, [X], L1),
+	G =.. L1,
+	( call(G)
+	-> Included = [X|Included0]
+	;  Included = Included0
+	),
+	include(Goal, Xs, Included0).
+
 % Additional type tests
 
 callable(T) :- atom(T) ; compound(T).
@@ -182,6 +226,8 @@ list([_|T]) :- list(T).
 partial_list(T) :- var(T).
 partial_list([_|T]) :- partial_list(T).
 
+atomic(T) :- atom(T) ; integer(T) ; float(T).
+
 % type assertions (throws an error if false)
 
 is_callable(T) :- callable(T), ! ; type_error(callable, T).
@@ -210,3 +256,106 @@ findall_collect(Acc, Instances) :-
 findall_collect([], Instances, Instances).
 findall_collect(solution(T), Acc, Instances) :-
 	findall_collect([T|Acc], Instances).
+
+bagof(Template, Goal, Instances) :-
+	free_variable_set(Goal, Template, Witness),
+	iterated_goal(Goal, G),
+	findall(Witness+Template, G, S),
+	bagof_loop(Witness, S, Instances).
+
+bagof_loop(Witness, S, Instances) :-
+	S \== [],
+	member(W+T, S),
+	!,
+	bagof_wt_list(S, W+T, WT_list),
+	bagof_split(WT_list, W_list, T_list),
+	( bagof_unify_list(Witness, W_list), Instances = T_list
+	; bagof_next_s(S, WT_list, S_next), bagof_loop(Witness, S_next, Instances)
+	).
+
+bagof_wt_list([], _, []).
+bagof_wt_list([W+T|Tail], W0+T0, Rest) :-
+	copy_term(W+T, W1+T1),
+	bagof_wt_list(Tail, W0+T0, Rest0),
+	( variant(W1, W0)
+	-> Rest = [W1+T1|Rest0]
+	; Rest = Rest0
+	).
+
+copy_terms_list([], []).
+copy_terms_list([H|T], [HH|TT]) :-
+	copy_term(H, HH),
+	copy_terms_list(T, TT).
+bagof_split([], [], []).
+bagof_split([WW+TT|RestWT], [WW|RestW], [TT|RestT]) :-
+	bagof_split(RestWT, RestW, RestT).
+
+bagof_unify_list(W, []).
+bagof_unify_list(W, [W|T]) :- bagof_unify_list(W, T).
+
+bagof_next_s([], _, []).
+bagof_next_s([H|T], WT_list, Rest) :-
+	bagof_next_s(T, WT_list, Rest0),
+	( findall(_, (member(X, WT_list), variant(X, H)), [])
+	-> Rest = [H|Rest0]
+	; Rest = Rest0
+	).
+
+% misc helpers
+
+variable_set(Term, []) :-
+	atomic(Term).
+variable_set(Term, [Term]) :-
+	var(Term).
+variable_set(Term, Vars) :-
+	compound(Term),
+	Term =.. [_|Args],
+	variable_set(Args, [], Vars0),
+	unique(Vars0, Vars).
+
+variable_set([], Acc, Acc).
+variable_set([Arg|Rest], Acc0, Result) :-
+	variable_set(Arg, VarSet),
+	append(Acc0, VarSet, Acc),
+	variable_set(Rest, Acc, Result).
+
+existential_variable_set(Term, []) :-
+	(atomic(Term) ; var(Term)),
+	!.
+existential_variable_set(V^G, Vars) :-
+	!,
+	existential_variable_set(G, Vars0),
+	variable_set(V, Vars1),
+	union(Vars0, Vars1, Vars).
+existential_variable_set(_, []).
+
+free_variable_set(T, V, Vars) :-
+	variable_set(T, TVars),
+	variable_set(V, VVars),
+	existential_variable_set(T, TExVars),
+	union(VVars, TExVars, BV),
+	difference(TVars, BV, Vars).
+
+iterated_goal(Goal, T) :-
+	compound(Goal),
+	_^G = Goal,
+	!,
+	iterated_goal(G, T).
+iterated_goal(G, G).
+
+variant(T1, T2) :-
+	var(T1), var(T2), !.
+variant(T1, T2) :-
+	compound(T1),
+	compound(T2),
+	!,
+	T1 =.. [Name|Args1],
+	T2 =.. [Name|Args2],
+	variant_list(Args1, Args2).
+variant(T1, T2) :-
+	T1 == T2.
+
+variant_list([], []).
+variant_list([H1|T1], [H2|T2]) :-
+	variant(H1, H2),
+	variant_list(T1, T2).