nedoPC.org

// пролог

#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);
};