36a326908c
git-svn-id: https://yap.svn.sf.net/svnroot/yap/trunk@1711 b08c6af1-5177-4d33-ba66-4b1c6b8b522a
96 lines
1.9 KiB
Plaintext
96 lines
1.9 KiB
Plaintext
|
|
:- category(solver).
|
|
|
|
:- info([
|
|
version is 1.0,
|
|
date is 2004/5/2,
|
|
author is 'Paulo Moura',
|
|
comment is 'Simple meta-interpreter for pure Prolog with only conjunctions as clause bodies.']).
|
|
|
|
:- public(solve/1).
|
|
:- mode(solve(+goal), zero_or_more).
|
|
:- info(solve/1, [
|
|
comment is 'Proves goal.',
|
|
argnames is ['Goal']]).
|
|
|
|
solve(true) :-
|
|
!.
|
|
solve((A, B)) :-
|
|
!,
|
|
solve(A),
|
|
solve(B).
|
|
solve(A) :-
|
|
::clause(A, B),
|
|
solve(B).
|
|
|
|
:- end_category.
|
|
|
|
|
|
:- category(proof_tree).
|
|
|
|
:- info([
|
|
version is 1.0,
|
|
date is 2004/5/2,
|
|
author is 'Paulo Moura',
|
|
comment is 'Meta-interpreter for pure Prolog with only conjunctions as clause bodies.']).
|
|
|
|
:- public(proof_tree/2).
|
|
:- mode(proof_tree(+goal, -tree), zero_or_more).
|
|
:- info(proof_tree/2, [
|
|
comment is 'Constructs a proof tree for a goal.',
|
|
argnames is ['Goal', 'Tree']]).
|
|
|
|
proof_tree(true, true) :-
|
|
!.
|
|
proof_tree((A, B), (PA, PB)) :-
|
|
!,
|
|
proof_tree(A, PA),
|
|
proof_tree(B, PB).
|
|
proof_tree(A, (A :- PB)) :-
|
|
::clause(A, B),
|
|
proof_tree(B, PB).
|
|
|
|
:- end_category.
|
|
|
|
|
|
:- category(tracer).
|
|
|
|
:- info([
|
|
version is 1.0,
|
|
date is 2004/5/5,
|
|
author is 'Paulo Moura',
|
|
comment is 'A simple tracer meta-interpreter for pure Prolog with only conjunctions as clause bodies.']).
|
|
|
|
:- public(trace/1).
|
|
:- mode(trace(+goal), zero_or_more).
|
|
:- info(trace/1, [
|
|
comment is 'Traces goal proof.',
|
|
argnames is ['Goal']]).
|
|
|
|
trace(Goal) :-
|
|
trace(Goal, 1).
|
|
|
|
trace(true, _) :-
|
|
!.
|
|
trace((A, B), Depth) :-
|
|
!,
|
|
trace(A, Depth),
|
|
trace(B, Depth).
|
|
trace(A, Depth) :-
|
|
write_trace(call, A, Depth),
|
|
clause(A, B),
|
|
Depth2 is Depth + 1,
|
|
trace(B, Depth2),
|
|
( write_trace(exit, A, Depth)
|
|
;
|
|
write_trace(redo, A, Depth),
|
|
fail).
|
|
trace(A, Depth) :-
|
|
write_trace(fail, A, Depth),
|
|
fail.
|
|
|
|
write_trace(Port, Goal, Depth) :-
|
|
write(Depth), write(' '), write(Port), write(': '), writeq(Goal), nl.
|
|
|
|
:- end_category.
|