/* ----------------------------------------------------------
% (C)1992 Institute for New Generation Computer Technology
% (Read COPYRIGHT for detailed information.)
----------------------------------------------------------- */
/*=====================================================================
* cu-Prolog III (Constraint Unification Prolog)
* Copyright: Institute for New Generation Computer Technology,Japan
* 1989--91
==================================================================== */
/*--------------------------------------------------------------------
* << UNIFY.C >>
* safe/unsafe/PST unification
* 94.5.20 remove_pst_ob
* 94.6.27 pst_unify, remove_pst_object_if_not_equal()
--------------------------------------------------------------------*/
#include "include.h"
#define Npstobj(Head,Env,Tail,Flag) Neclause(Head,Env,Tail,Flag)
#define UNSAFE 0
#define SAFE 1
#define NOEXTRACT 2
#define EXTRACT 3
#define PSTDEBUG 0
int Ocheck_max;
/*+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
int tunify(t,e,u,f,flag)
term unification between (t,e) and (u,f)
flag = 0: unsafe
1: safe, no extract
2: safe, extract
return_value --> TRUE/FALSE
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
int tunify(t,e,u,f,flag) /* term unification entry */
register struct term *t, *u;
register struct pair *e, *f;
int flag; /* 1:safe no-extract, 2:safe extract, 0:unsafe */
{
struct ustack *usave = usp;
int *hsave = hp, res;
struct pair *esave = ep;
Ocheck_max = 0;
if (flag == 1)
res = safe_unify(t,e,u,f,NOEXTRACT);
else if (flag == 2)
res = safe_unify(t,e,u,f,EXTRACT);
else
res = unify(t,e,u,f);
if (res == FALSE)
{
undo(usave);
hp = hsave;
ep = esave;
return(FALSE);
}
else return(TRUE);
}
struct pair *LastEnv;
/*+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
int tunify_apply(t,e,u,newf,flag)
newf= newly-defined environment
does not push the address in newf
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
int tunify_apply(t,e,u,f,flag) /* term unification entry */
register struct term *t, *u;
register struct pair *e, *f;
int flag; /* 1:safe no-extract, 2:safe extract, 0:unsafe (only) */
{
struct ustack *usave = usp;
int *hsave = hp, res;
struct pair *esave = ep;
LastEnv=f;
res = tunify(t,e,u,f,flag);
LastEnv=NULL_ENV;
return(res);
}
int ocheck(p, t, e) /* occur check of normal unification */
/* check if var p is contained in (t,e)
if contained, return FALSE,
else return TRUE
*/
register struct pair *p; /* var */
register struct term *t;
register struct pair *e;
{
register struct pair *q;
register int i, j;
if (Ocheck_max++ > 50) return(FALSE); /* in case of infinite loop */
/* printf("ocheck ");
Pterm(p->p_body, p->p_env);
printf(" in ");
Pterm(t,e);
NL;
*/
if (t == NULL_TERM) return(TRUE);
down(q, t, e);
if (q != NULL_ENV) { /* if t is var */
if (p == q) /* occured !! ==> fail */
return(FALSE);
else
return(TRUE);
}
switch (t->type.ident) {
case ATOMIC_TYPE:
case CONST_LIST_TYPE:
return(TRUE);
case LIST_TYPE:
case CLAUSE_TYPE:
if (ocheck(p,head_of_list(t),e) == TRUE &&
ocheck(p,tail_of_list(t),e) == TRUE)
return(TRUE);
else return(FALSE);
case PST_TYPE: { /* pst */
struct eclause *ptt;
struct pst_item *item;
if ((item = find_pstitem(t,e)) == NULL_PSTIT) {
ptt = ((struct pst *)t)->p_lists;
while (ptt != NULL_ECL) {
t = Arg2(ptt->c_form);
if (ocheck(p,t,e) == FALSE) return(FALSE);
ptt = ptt->c_link;
}
}
else {
ptt = item->p_lists;
while (ptt != NULL_ECL) {
t = Arg2(ptt->c_form);
e = ptt->c_env;
if (ocheck(p, t, e) == FALSE) return(FALSE);
ptt=ptt->c_link;
}
}
return(TRUE);
}
default: /* functor */
for(i = 0, j = t->t_arity; i < j; i++)
if (ocheck(p, Arg(t,i), e) == FALSE) return(FALSE);
}
return(TRUE);
}
int unify(t, e, u, f)
register struct term *t, *u;
register struct pair *e, *f;
{
register struct pair *p, *q;
#if PSTDEBUG == 1
printf("unify:");
Pterm(t,e);
printf(" and ");
Pterm(u,f);
NL;
#endif
down(p, t, e);
down(q, u, f);
if (p != NULL_ENV) /* if t = var */
if (p==Anonymous_env) return(TRUE); /* if t = Anonymous Var */
else if(q != NULL) /* t:var, u:var */
if(p == q) /* t,u : the same var */
return(TRUE);
else if (q==Anonymous_env) /* u : Anonymous Var */
return(TRUE);
else {
if (e != LastEnv)
{
upush(&(p->p_body)); /* t->u */
upush(&(p->p_env));
}
p->p_body = u;
p->p_env = f;
return(TRUE);
}
else { /* t:var, u:non-var */
if (e != LastEnv)
{
upush(&(p->p_body)); /* t->u */
upush(&(p->p_env));
}
p->p_body = u;
p->p_env = f;
return(TRUE);
}
else if(q != NULL)
if (q==Anonymous_env) return(TRUE);
else { /* t:nonvar , u:var */
if (f != LastEnv)
{
upush(&(q->p_body)); /* u->t */
upush(&(q->p_env));
}
q->p_body = t;
q->p_env = e;
return(TRUE);
}
/* t,u : nonvar */
switch (u->type.ident) {
case ATOMIC_TYPE : /* t,u: atomic (string,num,quote) */
{
if ((t==u) || (atomic_equal(u,t))) return(TRUE);
else return(FALSE);
}
case LIST_TYPE:
case CONST_LIST_TYPE:
if (is_list(t)) {
if(unify(head_of_list(t),e,head_of_list(u),f) &&
unify(tail_of_list(t),e,tail_of_list(u),f))
return(TRUE);
}
return(FALSE);
case CLAUSE_TYPE:
if (is_clause(t)) {
while ((t != NULL) && (u != NULL)) {
if (unify(((struct clause *)t)->c_form,e,
((struct clause *)u)->c_form,f) == FALSE)
return(FALSE);
t=(struct term *)((struct clause *)t)->c_link;
u=(struct term *)((struct clause *)u)->c_link;
}
if (t == u) return(TRUE);
}
return(FALSE);
case PST_TYPE:
if (is_pst(t)) {
return(pst_unify(t,e,u,f,UNSAFE));
}
return(FALSE);
default : /* functor */
if(Pred(t) == Pred(u)) {/* t,u: complex term */
register int i, j;
for(i = 0, j = Pred(t)->f_arity; i < j; i++)
if (unify(Arg(t,i), e, Arg(u,i), f) == FALSE)
return(FALSE);
/* unify each arg */
return(TRUE);
}
return(FALSE);
}
}
int unify_pst_extract();
int safe_unify(t, e, u, f, extflag) /* unify with occur check */
register struct term *t, *u;
register struct pair *e, *f;
int extflag; /* NOEXTRACT or EXTRACT */
{
register struct pair *p, *q;
int i, j;
#if PSTDEBUG == 1
printf("safe_unify ");
Pterm(t,e);
printf(" and ");
Pterm(u,f);
NL;
#endif
down(p, t, e);
down(q, u, f);
if(p != NULL) /* if t = var */
if (p==Anonymous_env) return(TRUE); /* if t = Anonymous Var */
else if(q != NULL) /* t:var, u:var */
if(p == q) /* t,u : the same var */
return(TRUE);
else if (q==Anonymous_env) /* u : Anonymous Var */
return(TRUE);
else {
if (e != LastEnv) {
upush(&(p->p_body)); /* t->u */
upush(&(p->p_env));
}
p->p_body = u;
p->p_env = f;
return(TRUE);
}
else { /* t:var, u:non-var */
if (ocheck(p,u,f) == FALSE) return(FALSE);
if (e != LastEnv)
{
upush(&(p->p_body)); /* t->u */
upush(&(p->p_env));
}
p->p_body = u;
p->p_env = f;
return(TRUE);
}
else if(q != NULL)
if (q==Anonymous_env) return(TRUE);
else { /* t:nonvar , u:var */
if (ocheck(q,t,e) == FALSE) return(FALSE);
if (f != LastEnv)
{
upush(&(q->p_body)); /* u->t */
upush(&(q->p_env));
}
q->p_body = t;
q->p_env = e;
return(TRUE);
}
/* t,u : nonvar */
switch (u->type.ident) {
case ATOMIC_TYPE : /* t,u: atomic (string,num,quote) */
{
if ((t==u) || (atomic_equal(u,t))) return(TRUE);
else return(FALSE);
}
case LIST_TYPE:
case CONST_LIST_TYPE:
if (is_list(t) &&
safe_unify(head_of_list(t),e,head_of_list(u),f,extflag) == TRUE &&
safe_unify(tail_of_list(t),e,tail_of_list(u),f,extflag) == TRUE)
return(TRUE);
else return(FALSE);
case CLAUSE_TYPE:
if (is_clause(t)) {
while ((t != NULL) && (u != NULL)) {
if (safe_unify(((struct clause *)t)->c_form,e,
((struct clause *)u)->c_form,f,extflag) == FALSE)
return(FALSE);
t=(struct term *)((struct clause *)t)->c_link;
u=(struct term *)((struct clause *)u)->c_link;
}
if (t == u) return(TRUE);
}
return(FALSE);
case PST_TYPE:
if (is_pst(t)) {
/* if (extflag == NOEXTRACT)
pst_unify(t,e,u,f,SAFE);
else
unify_pst_extract(t,e,u,f); */
return(pst_unify(t,e,u,f,SAFE));
}
else return(FALSE);
default : /* functor */
if(Pred(t) == Pred(u)) {/* t,u: complex term */
for(i = 0, j = Pred(t)->f_arity; i < j; i++)
if (safe_unify(Arg(t,i), e, Arg(u,i), f,extflag) == FALSE)
return(FALSE);
/* unify each arg */
return(TRUE);
}
return(FALSE);
}
}
int pst_unify(t,e,u,f,safeflag)
register struct term *t,*u;
register struct pair *e,*f;
int safeflag; /* SAFE(1) or UNSAFE(0) */
{
struct pst_item *target, *object;
#if PSTDEBUG != 0
printf("pst_unify %d ",safeflag);
Pterm(t,e);
printf(" & ");
Pterm(u,f);
printf(" ---> ");
#endif
target = find_pstitem(t,e);
if (target != NULL_PSTIT) {
object = remove_pstitem_if_not_equal(u,f,target);
if (object == target) /* p.var==t.var */
{
#if PSTDEBUG != 0
printf("<C#0>");
#endif
return(TRUE);
}
else if (object != NULL_PSTIT) /* t,u exist in psttable */
{
#if PSTDEBUG != 0
printf("<C#1>");
#endif
if (unify_merge_psts(target,object->p_lists,safeflag) == FALSE)
return(FALSE);
}
else { /* t exist, u doesn't exist */
#if PSTDEBUG != 0
printf("<C#2>");
#endif
if (unify_pstlist_objects(target,((struct pst *)u)->p_lists, f,
safeflag) == FALSE) return(FALSE);
}
if (unify(((struct pst *)u)->p_var,f,
((struct pst *)t)->p_var,e) == FALSE) return(FALSE);
/* u.var -> t.var */
}
else {
object = find_pstitem(u,f);
if (object != NULL_PSTIT) /* t doesn't exist, u:exists */
{
#if PSTDEBUG != 0
printf("<C#3>");
#endif
if (unify_pstlist_objects(object,((struct pst *)t)->p_lists, e,
safeflag) == FALSE) return(FALSE);
if (unify(((struct pst *)t)->p_var,e,
((struct pst *)u)->p_var,f) == FALSE) return(FALSE);
/* t.var -> u.var */
}
else { /* t,u don't exist */
#if PSTDEBUG != 0
printf("<C#4>");
#endif
target = record_pstobjects((struct pst *)t,e);
if (unify_pstlist_objects(target,((struct pst *)u)->p_lists, f,
safeflag)==FALSE) return(FALSE);
if (unify(((struct pst *)u)->p_var,f,
((struct pst *)t)->p_var,e) == FALSE) return(FALSE);
/* u.var -> t.var */
}
}
#if PSTDEBUG != 0
Pterm(t,e); NL;
#endif
return(TRUE);
}
/* one-way unification */
int unify_pst_extract(t,e,u,f) /* safe, extract pst unification */
struct pst *t,*u; /* t may be changed */
struct pair *e,*f;
{
struct pst_item *object,*target;
struct eclause *nttbegin,*ntt,*ot,*tt;
int i;
target = find_pstitem(t,e);
object = find_pstitem(u,f);
if (target == NULL_PSTIT)
target = record_pstobjects((struct pst *)t,e);
if (object == NULL_PSTIT)
object = record_pstobjects((struct pst *)u,f);
nttbegin=NULL_ECL;
for(ot=object->p_lists,tt=target->p_lists; ((ot!=NULL) && (tt!=NULL));)
{
i = Pred(Arg1(tt->c_form))->f_number -
Pred(Arg1(ot->c_form))->f_number;
if (i == 0)
{
if (safe_unify(tt->c_form,e,ot->c_form,f,1) == FALSE)
return(FALSE);
tt = tt->c_link;
ot = ot->c_link;
}
else if (i < 0) tt = tt->c_link;
else
{ /* ntt is in (u,f), but not in (t,e) */
if (nttbegin==NULL) nttbegin=ntt=ot;
else {
upush(&(ntt->c_link));
ntt->c_link = ot;
ntt = ot;
}
ot = ot->c_link;
}
}
if (nttbegin != NULL) {
upush(&(ntt->c_link));
ntt->c_link = ot;
}
else nttbegin = ot;
upush(&(target->p_lists));
target->p_lists = nttbegin; /* new target = (u,f)-(t,e) */
return(TRUE);
}
int unify_pstlist_objects(entry, ol, e, safeflag)
struct pst_item *entry;
struct eclause *ol;
struct pair *e;
int safeflag; /* SAFE or UNSAFE */
{
register int i;
struct eclause *pl;
if (ol==NULL_ECL) return(TRUE);
pl=entry->p_lists; /* pl must NOT be NULL */
#if PSTDEBUG != 0
printf("unify_pstlist_obj ");
Peclause(pl);
printf(" -- ");
Peclause(ol);
NL;
#endif
if (pl == NULL_ECL) {
upush(&(entry->p_lists));
entry->p_lists=record_pstlists(ol,e);
return(TRUE);
}
i = Pred(Arg1(pl->c_form))->f_number - Pred(Arg1(ol->c_form))->f_number;
if (i == 0) {
if (safeflag == UNSAFE)
{
if (unify(pl->c_form,pl->c_env,ol->c_form,e) == FALSE)
return(FALSE);
}
else
{
if (safe_unify(pl->c_form,pl->c_env,ol->c_form,e,NOEXTRACT) == FALSE) return(FALSE);
}
ol=ol->c_link;
}
/* pl={f1/v1,f2/v2,..} object={g1/t1,g2/t2,...}, f1 > g1 */
/* --> pl={g1/t1,f1/v1,...} object={g2/t2,...} */
else if (i > 0) {
upush(&(entry->p_lists));
entry->p_lists = Npstobj(ol->c_form,e,pl,MEDIUM);
ol = ol->c_link;
pl=entry->p_lists;
}
/* else goes on */
for (; ol != NULL_ECL &&
pl->c_link != NULL_ECL; )
{
i = Pred(Arg1(pl->c_link->c_form))->f_number -
Pred(Arg1(ol->c_form))->f_number;
if (i == 0) {
if (safeflag== UNSAFE)
{
if (unify(pl->c_link->c_form,pl->c_link->c_env,
ol->c_form,e) == FALSE) return(FALSE);
}
else
{
if (safe_unify(pl->c_link->c_form,pl->c_link->c_env,
ol->c_form,e,NOEXTRACT) == FALSE) return(FALSE);
}
ol = ol->c_link;
pl = pl->c_link;
}
else if (i > 0) {
upush(&(pl->c_link));
pl->c_link = Npstobj(ol->c_form,e,pl->c_link,MEDIUM);
ol = ol->c_link;
pl = pl->c_link;
}
else
{
pl = pl->c_link;
}
}
if (pl->c_link == NULL_ECL) {
upush(&(pl->c_link));
pl->c_link = record_pstlists(ol,e);
}
return(TRUE);
}
int unify_merge_psts(target,object,safeflag)
struct pst_item *target;
struct eclause *object;
int safeflag; /* SAFE or UNSAFE */
{
register int i;
struct eclause *pnext,*onext, *pl;
if (object==NULL_ECL) return(TRUE);
pl=target->p_lists;
if (pl == NULL_ECL) {
upush(&(target->p_lists));
target->p_lists = object;
return(TRUE);
}
i = Pred(Arg1(pl->c_form))->f_number - Pred(Arg1(object->c_form))->f_number;
if (i == 0) {
if (safeflag == UNSAFE)
{
if (unify(pl->c_form,pl->c_env,
object->c_form,object->c_env) == FALSE) return(FALSE);
}
else
{
if (safe_unify(pl->c_form,pl->c_env,
object->c_form,object->c_env,EXTRACT) == FALSE)
return(FALSE);
}
object=object->c_link;
}
/* pl={f1/v1,f2/v2,..} object={g1/t1,g2/t2,...}, f1 > g1 */
/* --> pl={g1/t1,f1/v1,...} object={g2/t2,...} */
else if (i > 0) { /* 93.8.17 by H.Sirai */
upush(&(target->p_lists)); /* pl.. > ol.. -> ol,pl.. & ol... */
target->p_lists =
Npstobj(object->c_form,object->c_env,pl,MEDIUM);
object = object->c_link;
pl = target->p_lists;
}
/* else goes on */
for (; object != NULL_ECL &&
pl->c_link != NULL_ECL; )
{
i = Pred(Arg1(pl->c_link->c_form))->f_number -
Pred(Arg1(object->c_form))->f_number;
if (i == 0) {
if (safeflag == UNSAFE)
{
if (unify(pl->c_link->c_form,pl->c_link->c_env,
object->c_form,object->c_env) == FALSE) return(FALSE);
}
else
{
if(safe_unify(pl->c_link->c_form,pl->c_link->c_env,
object->c_form,object->c_env,NOEXTRACT) == FALSE)
return(FALSE);
}
pl=pl->c_link;
object=object->c_link;
}
else if (i > 0) { /* pl->pnext-> ==> pl->object->pnext */
pnext=pl->c_link;
onext=object->c_link;
upush(&(pl->c_link));
pl->c_link = object;
upush(&(object->c_link));
object->c_link = pnext;
pl=pl->c_link;
object=onext;
}
else {
pl=pl->c_link;
}
}
if (pl->c_link == NULL_ECL) {
upush(&(pl->c_link));
pl->c_link = object;
}
return(TRUE);
}
syntax highlighted by Code2HTML, v. 0.9.1