Meta-Programming in Prolog - Part 2

database.lgt

:- object(database).

   :- public(rule/2).

   nat(zero) :- true.
   nat(s(X)) :- nat(X).

   add(zero, Y, Y) :- true.
   add(s(X), Y, s(Z)) :- 
       add(X, Y, Z).

   append([_X], Ys, Ys) :- true.
   append([X|Xs], Ys, [X|Zs]) :-
        append(Xs, Ys, Zs).

   prove(G) :-
       prove1([G]).

   prove1([]) :- true.
   prove1([G|Gs]) :-
       rule(G, B),
       prove1(B),
       prove1(Gs).

   length([], 0) :- true.
   length([_|Xs], N) :-
       length(Xs, N1),
       N is N1 + 1.

:- end_object.

debugging.lgt

:- object(debugging).

   %Based on source code from The Art of Prolog.
   :- public(false_solution/2).

   false_solution(G, Clause) :-
       interpreter::prove(G, T),
       false_goal(T, Clause).

   false_goal((A :- B), Clause) :-
       (    false_conjunction(B, Clause) ->
            true
       ;    Clause = (A :- B1),
            extract_body(B, B1)
       ).

   false_conjunction(((A :- B), _Bs), Clause) :-
       query_goal(A, false),
       !,
       false_goal((A :- B), Clause).
   %Almost the same as above, but with only one element.
   false_conjunction((A :- B), Clause) :-
       query_goal(A, false),
       !,
       false_goal((A :- B), Clause).
   false_conjunction((_A, As), Clause) :-
       %A is implicitly true.
       false_conjunction(As, Clause).

   extract_body(true, true).
   extract_body((A :- _B), A).
   extract_body(((A :- _B), Bs), (A, As)) :-
       extract_body(Bs, As).

   query_goal(G, Answer) :-
       write('Is the goal '),
       write(G),
       write(' true?'),
       nl,
       read(Answer).

:- end_object.

interpreter.lgt

:- object(interpreter).

   :- public(prove/1).
   :- public(prove/2).

   %Initialize the goal list with G.
   prove(G) :-
       prove1([G]).

   prove1([]).
   prove1([G|Gs]) :-
       rule(G, B),
       prove1(B),
       prove1(Gs).

   prove(G, T) :-
       prove1([G], T0),
	   filter(T0, T).

   prove1([], true).
   prove1([G|Gs], ((G :- T1), T2)) :-
       rule(G, B),
       prove1(B, T1),
       prove1(Gs, T2).

   filter(true, true).
   filter((T0, true), T) :-
       filter(T0, T).
   filter((T1, T2), (T3, T4)) :-
       T2 \= true,
       filter(T1, T3),
       filter(T2, T4).
   filter((A :- B0), A :- B) :-
       filter(B0, B).

   rule(rule(A, B), []) :- rule(A, B).
   rule((X is Y), []) :- X is Y.

   rule(G, B) :-
       database::rule(G, B).

:- end_object.

loader.lgt

:- initialization((
   logtalk_load(library(metapredicates_loader)),
   logtalk_load(library(types_loader)),
   logtalk_load(rule_expansion),
   logtalk_load(database, [hook(rule_expansion)]),
   logtalk_load(interpreter),
   logtalk_load(debugging))).