Code: Select all
// пролог
#define LISTK %(((отец маша эрнест)) \
((мать маша вика)) \
((отец давид арнольд)) \
((мать давид лена)) \
((отец настя давид)) \
((мать настя маша)) \
((дедушка (var дедушка) (var внук)) \
(родитель (var дедушка) (var родитель)) \
(родитель (var родитель) (var внук))) \
((родитель (var родитель) (var ребенок)) \
(мать (var родитель) (var ребенок))) \
((родитель (var родитель) (var ребенок)) \
(отец (var родитель) (var ребенок))))
#define LISTL %(((отец маша эрнест)) \
((мать маша вика)) \
((отец давид арнольд)) \
((мать давид лена)) \
((отец настя давид)) \
((мать настя маша)) \
((родитель (var родитель) (var ребенок)) \
(мать (var родитель) (var ребенок))))
global программа1;
define поменяй_имена(терм, уровень) {
declare ret;
cond {
(переменная?(терм)) do ret:=append(терм, уровень);
(atomp(терм)) do ret:=терм;
do ret:=cons(поменяй_имена(car(терм), уровень),поменяй_имена(cdr(терм), уровень));
};
ret;
};
define докажи (предикаты, связи, программа, уровень) {
declare ret;
print("докажи");
princ("предикаты=");print(предикаты);
cond {
(предикаты=nil) do { выведи_связи(связи, связи); ret:=true; };
do ret:=докажи_каждый(программа, программа, cdr(предикаты), car(предикаты), связи, уровень);
};
princ("конец докажи ret=");print(ret);
ret;
};
define выведи_связи(связи, связи1)
{
print(связи);
};
define докажи_каждый(остаток_прогр, программа, остаток_пред, пред, связи, уровень) {
declare ret;
declare теорема;
declare новые_связи;
print("докажи_каждый");
if(остаток_прогр=nil) {
print("остаток_прогр nil");
ret:=true;
} else {
теорема:=поменяй_имена(car(остаток_прогр),cons(уровень, nil));
princ("пред=");print(пред);
princ("head теорема=");print(car(теорема));
новые_связи:=унифицируй(пред, car(теорема), связи);
princ("новые_связи=");print(новые_связи);
if(новые_связи) {
print("новые_связи = nil");
ret:=докажи_каждый(cdr(остаток_прогр), программа, остаток_пред, пред, связи, уровень);
} else {
princ("теорема ");print(теорема);
ret:=докажи(append(cdr(теорема),остаток_пред), новые_связи, программа, уровень+1);
if(ret) {
ret:=true;
} else {
ret:=докажи_каждый(cdr(остаток_прогр), программа, остаток_пред, пред, связи, уровень);
};
};
};
princ("конец докажи_каждый ret=");print(ret);
ret;
};
#define first head
#define rest last
define унифицируй(x,y,связи) {
declare ret;
declare новые_связи;
print("унифицируй");
x:=значение(x, связи);
y:=значение(y, связи);
cond {
переменная?(x) do ret:=cons(list(x,y),связи);
переменная?(y) do ret:=cons(list(y,x),связи);
((atomp(x)=true) or (atomp(y)=true)) do ret:=((x=y) and связи);
do {
новые_связи:=унифицируй(car(x),car(y),связи);
princ("новые_связи=");print(новые_связи);
princ("x=");princ(x);
princ(" y=");print(y);
ret:=((новые_связи) and (унифицируй(cdr(x),cdr(y),новые_связи)));
};
};
ret;
};
define значение(x, связи) {
declare ret;
declare связь;
if(переменная?(x)) {
связь:=assoc(x,связи);
if(связь=nil) {
ret:=x;
} else {
ret:=значение(second(связь),связи);
};
} else {
ret:=x;
};
ret;
};
define переменная?(x) {
declare ret;
if(listp(x)) {
ret:=((atomp(car(x))) and (car(x)='var));
} else {
ret:=false;
};
ret;
};
define listp(x) {
declare ret;
asm {
loadal x;
jlst label_listp;
drop;
};
ret:=false;
asm {
jmp label_listp_ret;
label_listp:
drop;
};
ret:=true;
asm {
label_listp_ret: loadvl ret;
};
ret;
};
define atomp(x) {
declare ret;
asm {
loadal x;
jlst label_atomp;
jtpl label_atomp;
drop;
};
ret:=true;
asm {
jmp label_atomp_ret;
label_atomp:
drop;
};
ret:=false;
asm {
label_atomp_ret: loadvl ret;
};
ret;
};
define null(x) {
declare ret=false;
cond {
(listp(x)) do ret:=false;
(x=nil) do ret:=x;
};
ret;
};
define assoc (x, a) {
declare ret;
cond {
(a=nil) do ret:=nil;
(car(a)=nil) do ret:=nil;
(x=car(car(a))) do ret:=car(a);
do ret:=assoc(x,cdr(a));
};
ret;
};
define append (a, b) {
declare ret;
cond {
(atomp(a)) do ret:=a;
(b=nil) do ret:=a;
(atomp(cdr(a))) do rplaca(a,b);
do ret:=append(cdr(a),b);
};
a;
};
#define LIST3 %(a (var X) c (var Y))
#define LIST2 %(a b (var Z) c)
//#define LIST3 %(дедушка (var X) (var Y))
//#define LIST2 %(отец маша эрнест)
define unify_test {
declare a;
declare b;
declare d=0;
a:=LIST2;
b:=LIST3;
print(a);
print(b);
lcond {
(d=1000) do {
print(d);
};
do {
print_stack_ptr();
print(унифицируй(a,b,nil));
print_stack_ptr();
d:=d+1;
};
};
};
define list(...) {
declare ret=nil;
declare v=nil;
declare na=1;
v:=(argument na);
asm {
loadvl v;
jnil listl31;
drop;
enter;
listl11:
nop;
};
v:=(argument na);
asm {
loadvl v;
jnil listl21;
};
na:=na+1;
asm {
jmp listl11;
listl21:
drop;
call list;
savevl ret;
};
asm {
listl31:
nop;
};
ret:=cons((argument 0),ret);
ret;
};
define main {
unify_test();
declare предикаты;
программа1:=LISTL;
предикаты:=%(дедушка (var X) (var Y));
докажи(list(поменяй_имена(предикаты, %(0))), %((основа)), программа1, 1);
предикаты:=%(мать настя маша);
докажи(list(поменяй_имена(предикаты, %(0))), %((основа)), программа1, 1);
предикаты:=%(мать (var X) маша);
докажи(list(поменяй_имена(предикаты, %(0))), %((основа)), программа1, 1);
};