Пытаюсь сделать что-то типа локальных баз данных с возможностью доказательства только в рамках утверждённого в них и импортированного в них.
Породил следующее:
member2(X, _, [Y|_]) :- copy_term(Y, Z), Z = X.
member2(_, X, [Y|_]) :- copy_term(Y, Z), Z = X.
member2(X, Y, [_|T]) :-
member2(X, Y, T).
prove((Goal1, Goal2), Db) :-
prove(Goal1, Db),
prove(Goal2, Db).
prove(Goal, db(Clauses, Imports)) :-
member2(Goal, (Goal :- Procedure), Clauses),
(\+ var(Procedure)
->
prove(Procedure, db(Clauses, Imports))
;
true
).
prove(Goal, db(_, Imports)) :-
functor(Goal, F, A),
member(F/A, Imports),
call(Goal).
mdb(db([
fact(0, 1),
(fact(N, R) :- N1 is N - 1, fact(N1, R1), R is N * R1)
], [is/2])).
Проблема заключается в работе с рекурсивными правилами, ибо при унификации головы правила (второе правило предиката prove/2) переменные из базы инстанцируются внекоторые значения и последующие инстантинации проваливаются. Например, если я вызываю fact(2, N), то голова правила fact(N, R) :- ... принимает вид fact(2, R), и при рекурсивном вызове fact(1, R) унификация не срабатывает.
Пока проблему решил, что называется, "в лоб" — при поиске в базе данных создаю копии через copy_term/2 и пытаюсь унифицироваться с ними (см member2). Работает, но меня этот метод коробит, ибо копии создаются для каждой унификации, даже если она окажется неудачной. Понятно, что все лишние термы выбарсываются и будут удалены сборщиком мусора. Однако это лишняя нагрузка на систему.
Есть идеи, как решить проблему с "порчей" переменных в БД без такого брутального копирования?
Заранее спасибо.