% (C) September 12th 2005 Markus Triska  triska@gmx.at

natnum1(0).
natnum1(s(X)) :-
	natnum1(X).


mi1(true).
mi1((A,B)) :-
	mi1(A),
	mi1(B).
mi1(G) :-
	G \= true,
	G \= (_,_),
	clause(G, Body),
	mi1(Body).

%complicated_clause(A) :-
%	goal1(A),
%	goal2(A),
%	goal3(A).

mi_clause(Goal, Body) :-
	clause(Goal, Body0),
	defaulty_better(Body0, Body).

defaulty_better(true, true).
defaulty_better((A,B), (BA,BB)) :-
	defaulty_better(A, BA),
	defaulty_better(B, BB).
defaulty_better(G, g(G)) :-
	G \= true,
	G \= (_,_).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%natnum2(0).
%natnum2(s(X)) :-
%	g(natnum2(X)).

mi2(true).
mi2((A,B)) :-
	mi2(A),
	mi2(B).
mi2(g(G)) :-
	clause(G, Body),
	mi2(Body).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

safe_goal(natnum1(_)).

mi2_safe(true).
mi2_safe((A,B)) :-
	mi2_safe(A),
	mi2_safe(B).
mi2_safe(g(G)) :-
	( safe_goal(G) ->
		mi_clause(G, Body),
		mi2_safe(Body)
	;
		format("Sorry, you can't execute ~w\n", [G]),
		fail
	).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

declarative_fail :-
	declarative_fail,
	fail.

mi3(true).
mi3((A,B)) :-
	mi3(B),
	mi3(A).
mi3(g(G)) :-
	clause(G, Body),
	mi3(Body).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

mi_ldclause(natnum(0), Rest, Rest).
mi_ldclause(natnum(s(X)), [natnum(X)|Rest], Rest).

mi_list3([]).
mi_list3([G0|Gs0]) :-
	mi_ldclause(G0, Remaining, Gs0),
	mi_list3(Remaining).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


:- op(750, xfy, =>).

mi_tree(true, true).
mi_tree((A,B), (TA,TB)) :-
	mi_tree(A, TA),
	mi_tree(B, TB).
mi_tree(g(G), TBody => G) :-
	mi_clause(G, Body),
	mi_tree(Body, TBody).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


mi_limit(Goal, Max) :-
	mi_limit(Goal, Max, _).

mi_limit(true, N, N).
mi_limit((A,B), N0, N) :-
	mi_limit(A, N0, N1),
	mi_limit(B, N1, N).
mi_limit(g(G), N0, N) :-
	N0 > 0,
	mi_clause(G, Body),
	N1 is N0 - 1,
	mi_limit(Body, N1, N).

seq(N, N).
seq(N0, N) :-
	N1 is N0 + 1,
	seq(N1, N).

seq(N) :-
	seq(0, N).


mi_id(Goal) :-
	seq(N),
	mi_limit(Goal, N).

edge(a, b).
edge(b, a).
edge(b, c).
edge(c, d).

path(A, B, [e(A,B)|Rest], Rest) :-
	edge(A, B).
path(A, C, [e(A,B)|Es], Rest) :-
	edge(A, B),
	path(B, C, Es, Rest).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


occ(X, f(X)).

mi_occ(true).
mi_occ((A,B)) :-
	mi_occ(A),
	mi_occ(B).
mi_occ(g(G)) :-
	functor(G, F, Arity),
	functor(H, F, Arity),
	mi_clause(H, Body),
	unify_with_occurs_check(G, H),
	mi_occ(Body).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

mi_circ(true).
mi_circ((A,B)) :-
	mi_circ(A),
	mi_circ(B).
mi_circ(clause(A,B)) :-
	clause(A,B).
mi_circ(A \= B) :-
	A \= B.
mi_circ(G) :-
	G \= true,
	G \= (_,_),
	G \= (_\=_),
	G \= clause(_,_),
	clause(G, Body),
	mi_circ(Body).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

as([]).
as([a]).			% redundant
as([a,a]).			% redundant
as([A|As]) :-
        A = a,			% test built-in =/2
	5 is 2 + 3,		% test built-in is/2
	1 > 0,			% test built-in >/2
        as(As).

member_rest(M, [M|Rest], Rest).
member_rest(M, [E|Es], [E|Rest]) :-
	member_rest(M, Es, Rest).

redundant(Functor/Arity, Reds) :-
	functor(Term, Functor, Arity),
	findall(Term-Body, clause(Term, Body), Defs),
	setof(Red, Defs^redundant_(Defs, Red), Reds).

redundant_(Defs, Fact) :-
	member_rest(Fact-true, Defs, Rest),
	once(provable(Fact, Rest)).


provable(true, _) :- !.
provable((G1,G2), Defs) :- !,
	provable(G1, Defs),
	provable(G2, Defs).
provable(BI, _) :-
	predicate_property(BI, built_in),
	!,
	call(BI).
provable(Goal, Defs) :-
	member(Goal-Body, Defs),
	provable(Body, Defs).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

resstep_([Alt|Alts0], Alts) :-
	findall(Gs-G, (Alt = [G0|Rest]-G,mi_ldclause(G0,Gs,Rest)), Gss),
	append(Gss, Alts0, Alts).

mi_backtrack(G0) :-
	mi_backtrack_([[G0]-G0], G0).

mi_backtrack_([[]-G|_], G).
mi_backtrack_(Alts0, G) :-
	resstep_(Alts0, Alts1),
	mi_backtrack_(Alts1, G).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


dcgnumber(0).
dcgnumber(1).

expr(N) -->
	[N],
	{ dcgnumber(N) }.
expr(A+B) -->
	expr(A),
	[(+)],
	expr(B).


dcg_clause(expr(N), [t(N),{dcgnumber(N)}]).
dcg_clause(expr(A+B), [l,nt(expr(A)),t(+),nt(expr(B))]).

mi_dcg(t(T), Rest, Rest, [T|Ts], Ts).
mi_dcg({Goal}, Rest, Rest, Ts, Ts) :-
	call(Goal).
mi_dcg(nt(NT), Rest0, Rest, Ts0, Ts) :-
	dcg_clause(NT, Body),
	mi_dcg_(Body, Rest0, Rest, Ts0, Ts).
mi_dcg(l, [_|Rest], Rest, Ts, Ts).

mi_dcg_([], Rest, Rest, Ts, Ts).
mi_dcg_([G|Gs], Rest0, Rest, Ts0, Ts) :-
	mi_dcg(G, Rest0, Rest1, Ts0, Ts1),
	mi_dcg_(Gs, Rest1, Rest, Ts1, Ts).

mi_dcg(NT, String) :-
	length(String, L),
	length(Rest0, L),
	mi_dcg_([nt(NT)], Rest0, _, String, []).