/*
 *  ADP (Another Data Processor) www.adp.la
 *  Copyright (C) 2010 Katsuhisa Ohfuji <katsuhisa@ohfuji.name>
 *
 *  This program is free software; you can redistribute it and/or modify
 *  it under the terms of the GNU General Public License version 2 as
 *  published by the Free Software Foundation.
 *
 *  This program is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *  GNU General Public License for more details.
 *
 *  You should have received a copy of the GNU General Public License
 *  along with this program; if not, write to the Free Software
 *  Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston,
 *  MA 02110-1301, USA.
 */
#include "adp.h"

#define MYDEBUG_UNIFY	0

/*************************************** getPridicate() ******************************************/
const PPredicate *PVeriable::getPredicate(VLocal *local) const
{
	const PObject	*item = (*local)[idx];
	if ( item == 0 ) {
		return 0;
	} else {	
		return item->getPredicate(local);
	}
}

const PPredicate *PEVeriable::getPredicate(VLocal *local) const
{
	const PObject	*item = (*vl)[idx];
	if ( item == 0 ) {
		return 0;
	} else {	
		return item->getPredicate(local);
	}
}

/*************************************** getPridicateName() ******************************************/
const string *PVeriable::getPredicateName(bool &docache, VLocal *local) const
{
	docache = false;
	const PObject	*item = (*local)[idx];
	if ( item == 0 ) {
		return 0;
	} else {
		return item->getPredicateName(docache,local);
	}
}

const string *PEVeriable::getPredicateName(bool &docache, VLocal *local) const
{
	docache = false;
	const PObject	*item = (*vl)[idx];
	if ( item == 0 ) {
		return 0;
	} else {	
		return item->getPredicateName(docache, local);
	}
}



/*************************************** unify ******************************************/

// 変項のunify本体で使うテンプレート関数
template <class T> bool PEVeriable::vunify(const T &horn, ExecContextRoot *c, VLocal *, VLocal *hlocal) const
{
	VLocal *local = vl;
	const PObject *gitem = (*local)[idx];
	if ( gitem == 0 ) {
		(*local)[idx] = &horn;
	} else {
		return gitem->unify( horn, c, local, hlocal);
	}
	return true;
}

// 変項のunify本体で使うテンプレート関数
template <class T> bool PEVeriable::vunify_getval(const T &horn, ExecContextRoot *c, VLocal *, VLocal *hlocal) const
{
	VLocal *local = vl;
	const PObject *gitem = (*local)[idx];
	if ( gitem == 0 ) {
		//c->assign( local, idx, horn.getval(c, hlocal));
		(*local)[idx] = horn.getval(c, hlocal);
	} else {
		return gitem->unify( horn, c, local, hlocal);
	}
	return true;
}

bool PNil::unify(const PObject &goal, ExecContextRoot *c, VLocal *hlocal, VLocal *glocal) const { return goal.unify(*this, c, glocal, hlocal); }
bool PNil::unify(const PNil &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return true; }
bool PNil::unify(const PList &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return horn.unify( *this, c, hlocal, glocal); }
bool PNil::unify(const PVeriable &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return horn.vunify<PNil>(*this, c, hlocal, glocal); }
bool PNil::unify(const PEVeriable &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return horn.vunify<PNil>(*this, c, hlocal, glocal); }

bool PNil::unify(const PObject &goal, ExecContextRoot *c) const { return goal.unify(*this, c); }
bool PNil::unify(const PNil &horn, ExecContextRoot *c) const { return true; }
bool PNil::unify(const PList &horn, ExecContextRoot *c) const { return horn.unify( *this, c); }
bool PNil::unify(const PVeriable &horn, ExecContextRoot *c) const { return horn.vunify<PNil>(*this, c, c->hl, c->gl); }
bool PNil::unify(const PEVeriable &horn, ExecContextRoot *c) const { return horn.vunify<PNil>(*this, c, c->hl, c->gl); }

bool PString::unify(const PObject &goal, ExecContextRoot *c, VLocal *hlocal, VLocal *glocal) const { return goal.unify(*this, c, glocal, hlocal); }
bool PString::unify(const PString &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return strcmp( value.c_str(), horn.value.c_str()) == 0; }
bool PString::unify(const PVeriable &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return horn.vunify<PString>(*this, c, hlocal, glocal); }
bool PString::unify(const PEVeriable &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return horn.vunify<PString>(*this, c, hlocal, glocal); }

bool PString::unify(const PObject &goal, ExecContextRoot *c) const { return goal.unify(*this, c); }
bool PString::unify(const PString &horn, ExecContextRoot *c) const { return strcmp( value.c_str(), horn.value.c_str()) == 0; }
bool PString::unify(const PVeriable &horn, ExecContextRoot *c) const { return horn.vunify<PString>(*this, c, c->hl, c->gl); }
bool PString::unify(const PEVeriable &horn, ExecContextRoot *c) const { return horn.vunify<PString>(*this, c, c->hl, c->gl); }

bool PDouble::unify(const PObject &goal, ExecContextRoot *c, VLocal *hlocal, VLocal *glocal) const { return goal.unify(*this, c, glocal, hlocal); }
bool PDouble::unify(const PDouble &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return fabs(value - (double)horn.value) < DBL_EPSILON; }
bool PDouble::unify(const PInteger &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return fabs(value - (double)horn.value) < DBL_EPSILON; }
bool PDouble::unify(const PVeriable &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return horn.vunify<PDouble>(*this, c, hlocal, glocal); }
bool PDouble::unify(const PEVeriable &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return horn.vunify<PDouble>(*this, c, hlocal, glocal); }

bool PDouble::unify(const PObject &goal, ExecContextRoot *c) const { return goal.unify(*this, c); }
bool PDouble::unify(const PDouble &horn, ExecContextRoot *c) const { return fabs(value - (double)horn.value) < DBL_EPSILON; }
bool PDouble::unify(const PInteger &horn, ExecContextRoot *c) const { return fabs(value - (double)horn.value) < DBL_EPSILON; }
bool PDouble::unify(const PVeriable &horn, ExecContextRoot *c) const { return horn.vunify<PDouble>(*this, c, c->hl, c->gl); }
bool PDouble::unify(const PEVeriable &horn, ExecContextRoot *c) const { return horn.vunify<PDouble>(*this, c, c->hl, c->gl); }

bool PInteger::unify(const PObject &goal, ExecContextRoot *c, VLocal *hlocal, VLocal *glocal) const { return goal.unify(*this, c, glocal, hlocal); }
bool PInteger::unify(const PDouble &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return fabs(value - (double)horn.value) < DBL_EPSILON; }
bool PInteger::unify(const PInteger &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return value == horn.value; }
bool PInteger::unify(const PVeriable &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return horn.vunify<PInteger>(*this, c, hlocal, glocal); }
bool PInteger::unify(const PEVeriable &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return horn.vunify<PInteger>(*this, c, hlocal, glocal); }

bool PInteger::unify(const PObject &goal, ExecContextRoot *c) const { return goal.unify(*this, c); }
bool PInteger::unify(const PDouble &horn, ExecContextRoot *c) const { return fabs(value - (double)horn.value) < DBL_EPSILON; }
bool PInteger::unify(const PInteger &horn, ExecContextRoot *c) const { return value == horn.value; }
bool PInteger::unify(const PVeriable &horn, ExecContextRoot *c) const { return horn.vunify<PInteger>(*this, c, c->hl, c->gl); }
bool PInteger::unify(const PEVeriable &horn, ExecContextRoot *c) const { return horn.vunify<PInteger>(*this, c, c->hl, c->gl); }

bool PList::unify(const PObject &goal, ExecContextRoot *c, VLocal *hlocal, VLocal *glocal) const { return goal.unify(*this, c, glocal, hlocal); }
bool PList::unify(const PNil &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { 
    if ( typeid(*lvalue) == typeid(PNil) && typeid(*rvalue) == typeid(PNil) ) return true;
    return false;
}
bool PList::unify(const PList &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const
{ 
	if ( horn.lvalue->unify( *lvalue, c, hlocal, glocal) && horn.rvalue->unify( *rvalue, c, hlocal, glocal) ) return true;
	return false; 
}
bool PList::unify(const PVeriable &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return horn.vunify_getval<PList>(*this, c, hlocal, glocal); }
bool PList::unify(const PEVeriable &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return horn.vunify_getval<PList>(*this, c, hlocal, glocal); }

bool PList::unify(const PObject &goal, ExecContextRoot *c) const { return goal.unify(*this, c); }
bool PList::unify(const PNil &horn, ExecContextRoot *c) const { 
    if ( typeid(*lvalue) == typeid(PNil) && typeid(*rvalue) == typeid(PNil) ) return true;
    return false;
}
bool PList::unify(const PList &horn, ExecContextRoot *c) const
{ 
	if ( horn.lvalue->unify( *lvalue, c) && horn.rvalue->unify( *rvalue, c) ) return true;
	return false; 
}
bool PList::unify(const PVeriable &horn, ExecContextRoot *c) const { return horn.vunify_getval<PList>(*this, c, c->hl, c->gl); }
bool PList::unify(const PEVeriable &horn, ExecContextRoot *c) const { return horn.vunify_getval<PList>(*this, c, c->hl, c->gl); }

bool PArray::unify(const PObject &goal, ExecContextRoot *c, VLocal *hlocal, VLocal *glocal) const { return goal.unify(*this, c, glocal, hlocal); }
bool PArray::unify(const PNil &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { if ( value.empty() ) return true; return false; }
bool PArray::unify(const PArray &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const
{ 
	size_t	gsiz = value.size();
	size_t	hsiz = horn.value.size();
	// 片方に@がある場合、引数展開を行なう。両方にある場合、普通に処理する（引数展開しない）
	if ( (args == true || horn.args == true) && (args == false || horn.args == false) ) {
		// 引数展開あり
		size_t	lidx = 0;
		size_t	hridx = hsiz - 1;
		size_t	gridx = gsiz - 1;
		const PObjectArray	*pvalue;
		const PArray	*vary;
		if ( args == true ) {
			// ゴール側引数展開
			if ( hsiz < gsiz ) return false;	// 引数展開側の引数数が多い
			pvalue = &value;
			vary = &horn;
		} else {
			// ホーン側引数展開
			if ( gsiz < hsiz ) return false;	// 引数展開側の引数数が多い
			pvalue = &horn.value;
			vary = this;
		}
		// 左からのチェック（@が出るまで）
		while ( lidx <= gridx && lidx <= hridx ) {
			if ( (*pvalue)[lidx]->isargs() ) break;	// 引数展開の確認
			if ( !horn.value[lidx]->unify( *value[lidx], c, hlocal, glocal) ) return false;
			lidx++;
		}
		// 右からのチェック（引数展開以降のチェック）
		while ( lidx < gridx && lidx < hridx ) {
			if ( horn.value[hridx]->isargs() || value[gridx]->isargs() ) break;	// 引数展開の確認
			if ( !horn.value[hridx]->unify( *value[gridx], c, hlocal, glocal) ) return false;
			hridx--;
			gridx--;
		}

		if ( args == true ) {
			PArray *ao = pmm.newPArray(c->pobjs, *vary, lidx, hridx + 1);
			return (*pvalue)[lidx]->unify( *ao, c, glocal, hlocal);
		} else {
			PArray *ao = pmm.newPArray(c->pobjs, *vary, lidx, gridx + 1);
			return (*pvalue)[lidx]->unify( *ao, c, hlocal, glocal);
		}

	} else {
		// 引数展開なし
		if ( gsiz != hsiz ) return false;
#if 1
		const PObject ** __restrict hargs = &horn.value.front();
		const PObject ** __restrict gargs = &value.front();
		while ( gsiz-- > 0 ) {
			if ( !(*hargs)->unify( **gargs, c, hlocal, glocal) ) return false;
			hargs++;
			gargs++;
		}
#else
		for ( size_t i = 0; i < gsiz; i++ ) {
			if ( !horn.value[i]->unify( *value[i], c, hlocal, glocal) ) {
				return false;
			}
		}
#endif
	}

	return true;
}
bool PArray::unify(const PVeriable &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return horn.vunify_getval<PArray>(*this, c, hlocal, glocal); }
bool PArray::unify(const PEVeriable &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return horn.vunify_getval<PArray>(*this, c, hlocal, glocal); }

bool PArray::unify(const PObject &goal, ExecContextRoot *c) const { return goal.unify(*this, c); }
bool PArray::unify(const PNil &horn, ExecContextRoot *c) const { if ( value.empty() ) return true; return false; }
bool PArray::unify(const PArray &horn, ExecContextRoot *c) const { return unify( horn, c, c->gl, c->hl);}
bool PArray::unify(const PVeriable &horn, ExecContextRoot *c) const { return horn.vunify_getval<PArray>(*this, c, c->hl, c->gl); }
bool PArray::unify(const PEVeriable &horn, ExecContextRoot *c) const { return horn.vunify_getval<PArray>(*this, c,c->hl, c->gl); }

bool PPredicate::unify(const PObject &goal, ExecContextRoot *c, VLocal *hlocal, VLocal *glocal) const { return goal.unify(*this, c, glocal, hlocal); }
bool PPredicate::unify(const PPredicate &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const 
{ 
	// 呼び出し側(goal)がnamespaceを指定した場合、namespaceが一致している必要がある。
	if ( !nspace.empty() && strcmp( horn.nspace.c_str(), nspace.c_str()) != 0 ) { return false; }
	
	if ( !horn.name->unify( *name, c, hlocal, glocal) ) { return false; }
	return arglist.unify( horn.arglist, c, glocal, hlocal); // horn.arglistがPObjextでない場合はこのように呼び出す
}
bool PPredicate::unify(const PVeriable &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return horn.vunify_getval<PPredicate>(*this, c, hlocal, glocal); }
bool PPredicate::unify(const PEVeriable &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return horn.vunify_getval<PPredicate>(*this, c, hlocal, glocal); }

bool PPredicate::unify(const PObject &goal, ExecContextRoot *c) const { return goal.unify(*this, c); }
bool PPredicate::unify(const PPredicate &horn, ExecContextRoot *c) const 
{ 
	// 呼び出し側(goal)がnamespaceを指定した場合、namespaceが一致している必要がある。
	if ( !nspace.empty() && strcmp( horn.nspace.c_str(), nspace.c_str()) != 0 ) { return false; }

	if ( !horn.name->unify( *name, c) ) { return false; }
	return arglist.unify( horn.arglist, c); // horn.arglistがPObjextでない場合はこのように呼び出す
}
bool PPredicate::unify(const PVeriable &horn, ExecContextRoot *c) const { return horn.vunify_getval<PPredicate>(*this, c, c->hl, c->gl); }
bool PPredicate::unify(const PEVeriable &horn, ExecContextRoot *c) const { return horn.vunify_getval<PPredicate>(*this, c, c->hl, c->gl); }


bool PVeriable::unify(const PObject &goal, ExecContextRoot *c, VLocal *hlocal, VLocal *glocal) const { return goal.unify(*this, c, glocal, hlocal); }
bool PVeriable::unify(const PNil &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return vunify<PNil>(horn, c, glocal, hlocal); }
bool PVeriable::unify(const PString &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return vunify<PString>(horn, c, glocal, hlocal); }
bool PVeriable::unify(const PDouble &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return vunify<PDouble>(horn, c, glocal, hlocal); }
bool PVeriable::unify(const PInteger &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return vunify<PInteger>(horn, c, glocal, hlocal); }
bool PVeriable::unify(const PList &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return vunify_getval<PList>(horn, c, glocal, hlocal); }
bool PVeriable::unify(const PArray &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return vunify_getval<PArray>(horn, c, glocal, hlocal); }
bool PVeriable::unify(const PPredicate &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return vunify_getval<PPredicate>(horn, c, glocal, hlocal); }
bool PVeriable::unify(const PVeriable &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { 
	const PObject *gval = (*glocal)[idx];
	const PObject *hval = (*hlocal)[horn.idx];
	if ( gval != 0 ) {
		if ( hval != 0 ) {
			return hval->unify( *gval, c, hlocal, glocal);
		} else {
			(*hlocal)[horn.idx] = gval;
		}
	} else {
		if ( hval != 0 ) {
			(*glocal)[idx] = hval;
		} else {
			ExecContext *ec = dynamic_cast<ExecContext*>(c);
			if ( ec != 0 ) {
				ec->substitutepair.push_back( SubstitutePair(horn.idx, idx) );
			} else {
				(*hlocal)[horn.idx] = getval( c, glocal);
			}
		}
	}
	return true;
}
bool PVeriable::unify(const PEVeriable &horn, ExecContextRoot *c, VLocal *glocal, VLocal *) const { 
	VLocal *hlocal = horn.vl;
	const PObject *gval = (*glocal)[idx];
	const PObject *hval = (*hlocal)[horn.idx];
	if ( gval != 0 ) {
		if ( hval != 0 ) {
			return hval->unify( *gval, c, hlocal, glocal);
		} else {
			(*hlocal)[horn.idx] = gval;
		}
	} else {
		if ( hval != 0 ) {
			(*glocal)[idx] = hval;
		} else {
			// ここには来ないはず
			(*glocal)[idx] = &horn;
		}
	}
	return true;
}

bool PVeriable::unify(const PObject &goal, ExecContextRoot *c) const { return goal.unify(*this, c); }
bool PVeriable::unify(const PNil &horn, ExecContextRoot *c) const { return vunify<PNil>(horn, c, c->gl, c->hl); }
bool PVeriable::unify(const PString &horn, ExecContextRoot *c) const { return vunify<PString>(horn, c, c->gl, c->hl); }
bool PVeriable::unify(const PDouble &horn, ExecContextRoot *c) const { return vunify<PDouble>(horn, c, c->gl, c->hl); }
bool PVeriable::unify(const PInteger &horn, ExecContextRoot *c) const { return vunify<PInteger>(horn, c, c->gl, c->hl); }
bool PVeriable::unify(const PList &horn, ExecContextRoot *c) const { return vunify_getval<PList>(horn, c, c->gl, c->hl); }
bool PVeriable::unify(const PArray &horn, ExecContextRoot *c) const { return vunify_getval<PArray>(horn, c, c->gl, c->hl); }
bool PVeriable::unify(const PPredicate &horn, ExecContextRoot *c) const { return vunify_getval<PPredicate>(horn, c, c->gl, c->hl); }
bool PVeriable::unify(const PVeriable &horn, ExecContextRoot *c) const { 
	VLocal *glocal = c->gl;
	VLocal *hlocal = c->hl;
	const PObject *gval = (*glocal)[idx];
	const PObject *hval = (*hlocal)[horn.idx];
	if ( gval != 0 ) {
		if ( hval != 0 ) {
			return hval->unify( *gval, c, hlocal, glocal);
		} else {
			(*hlocal)[horn.idx] = gval;
		}
	} else {
		if ( hval != 0 ) {
			(*glocal)[idx] = hval;
		} else {
			ExecContext *ec = dynamic_cast<ExecContext*>(c);
			if ( ec != 0 ) {
				ec->substitutepair.push_back( SubstitutePair(horn.idx, idx) );
			} else {
				(*hlocal)[horn.idx] = getval( c, glocal);
			}
		}
	}
	return true;
}
bool PVeriable::unify(const PEVeriable &horn, ExecContextRoot *c) const { 
	VLocal *glocal = c->gl;
	VLocal *hlocal = horn.vl;
	const PObject *gval = (*glocal)[idx];
	const PObject *hval = (*hlocal)[horn.idx];
	if ( gval != 0 ) {
		if ( hval != 0 ) {
			return hval->unify( *gval, c, hlocal, glocal);
		} else {
			(*hlocal)[horn.idx] = gval;
		}
	} else {
		if ( hval != 0 ) {
			(*glocal)[idx] = hval;
		} else {
			// ここには来ないはず
			(*glocal)[idx] = &horn;
		}
	}
	return true;
}


bool PEVeriable::unify(const PObject &goal, ExecContextRoot *c, VLocal *hlocal, VLocal *glocal) const { return goal.unify(*this, c, glocal, hlocal); }
bool PEVeriable::unify(const PNil &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return vunify<PNil>(horn, c, glocal, hlocal); }
bool PEVeriable::unify(const PString &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return vunify<PString>(horn, c, glocal, hlocal); }
bool PEVeriable::unify(const PDouble &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return vunify<PDouble>(horn, c, glocal, hlocal); }
bool PEVeriable::unify(const PInteger &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return vunify<PInteger>(horn, c, glocal, hlocal); }
bool PEVeriable::unify(const PList &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return vunify_getval<PList>(horn, c, glocal, hlocal); }
bool PEVeriable::unify(const PArray &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return vunify_getval<PArray>(horn, c, glocal, hlocal); }
bool PEVeriable::unify(const PPredicate &horn, ExecContextRoot *c, VLocal *glocal, VLocal *hlocal) const { return vunify_getval<PPredicate>(horn, c, glocal, hlocal); }
bool PEVeriable::unify(const PVeriable &horn, ExecContextRoot *c, VLocal *, VLocal *hlocal) const { 
	VLocal *glocal = vl;
	const PObject *gval = (*glocal)[idx];
	const PObject *hval = (*hlocal)[horn.idx];
	if ( gval != 0 ) {
		if ( hval != 0 ) {
			return hval->unify( *gval, c, hlocal, glocal);
		} else {
			(*hlocal)[horn.idx] = gval;
		}
	} else {
		if ( hval != 0 ) {
			(*glocal)[idx] = hval;
		} else {
			(*hlocal)[horn.idx] = this;
		}
	}
	return true;
}
bool PEVeriable::unify(const PEVeriable &horn, ExecContextRoot *c, VLocal *, VLocal *) const { 
	VLocal *glocal = vl;
	VLocal *hlocal = horn.vl;
	const PObject *gval = (*glocal)[idx];
	const PObject *hval = (*hlocal)[horn.idx];
	if ( gval != 0 ) {
		if ( hval != 0 ) {
			return hval->unify( *gval, c, hlocal, glocal);
		} else {
			(*hlocal)[horn.idx] = gval;
		}
	} else {
		if ( hval != 0 ) {
			(*glocal)[idx] = hval;
		} else {
			ExecContext *ec = dynamic_cast<ExecContext*>(c);
			if ( ec != 0 ) {
				ec->substitutepair.push_back( SubstitutePair(horn.idx, idx) );
			} else {
				(*hlocal)[horn.idx] = this;
			}
		}
	}
	return true;
}

bool PEVeriable::unify(const PObject &goal, ExecContextRoot *c) const { return goal.unify(*this, c); }
bool PEVeriable::unify(const PNil &horn, ExecContextRoot *c) const { return vunify<PNil>(horn, c, c->gl, c->hl); }
bool PEVeriable::unify(const PString &horn, ExecContextRoot *c) const { return vunify<PString>(horn, c, c->gl, c->hl); }
bool PEVeriable::unify(const PDouble &horn, ExecContextRoot *c) const { return vunify<PDouble>(horn, c, c->gl, c->hl); }
bool PEVeriable::unify(const PInteger &horn, ExecContextRoot *c) const { return vunify<PInteger>(horn, c, c->gl, c->hl); }
bool PEVeriable::unify(const PList &horn, ExecContextRoot *c) const { return vunify_getval<PList>(horn, c, c->gl, c->hl); }
bool PEVeriable::unify(const PArray &horn, ExecContextRoot *c) const { return vunify_getval<PArray>(horn, c, c->gl, c->hl); }
bool PEVeriable::unify(const PPredicate &horn, ExecContextRoot *c) const { return vunify_getval<PPredicate>(horn, c, c->gl, c->hl); }
bool PEVeriable::unify(const PVeriable &horn, ExecContextRoot *c) const { 
	VLocal *glocal = vl;
	VLocal *hlocal = c->hl;
	const PObject *gval = (*glocal)[idx];
	const PObject *hval = (*hlocal)[horn.idx];
	if ( gval != 0 ) {
		if ( hval != 0 ) {
			return hval->unify( *gval, c, hlocal, glocal);
		} else {
			(*hlocal)[horn.idx] = gval;
		}
	} else {
		if ( hval != 0 ) {
			(*glocal)[idx] = hval;
		} else {
			(*hlocal)[horn.idx] = this;
		}
	}
	return true;
}
bool PEVeriable::unify(const PEVeriable &horn, ExecContextRoot *c) const { 
	VLocal *glocal = vl;
	VLocal *hlocal = horn.vl;
	const PObject *gval = (*glocal)[idx];
	const PObject *hval = (*hlocal)[horn.idx];
	if ( gval != 0 ) {
		if ( hval != 0 ) {
			return hval->unify( *gval, c, hlocal, glocal);
		} else {
			(*hlocal)[horn.idx] = gval;
		}
	} else {
		if ( hval != 0 ) {
			(*glocal)[idx] = hval;
		} else {
			ExecContext *ec = dynamic_cast<ExecContext*>(c);
			if ( ec != 0 ) {
				ec->substitutepair.push_back( SubstitutePair(horn.idx, idx) );
			} else {
				(*hlocal)[horn.idx] = this;
			}
		}
	}
	return true;
}

/*************************************** uphorn ******************************************/
bool PHorn::upHorn(const PPredicate &goal, ExecContext &c, bool skipnamechk)
{
	if ( skipnamechk ) {
		// ホーン節頭部の述語名の確認は既に終わっている
		return goal.arglist.unify( head.arglist, &c, c.gl, c.hl ); // horn.arglistがPObjextでない場合はこのように呼び出す
	} else {
		return goal.unify(head, &c, c.gl, c.hl);
	}
}

/*************************************** getval ******************************************/
const PObject *PList::getval( ExecContextRoot *c)  const
{
	if ( constant ) return this;
	PList	*lo = 0;
	const PObject *l = lvalue->getval(c);
	const PObject *r = rvalue->getval(c);
	if ( l != lvalue || r != rvalue ) {
		lo = pmm.newPList(c->pobjs, const_cast<PObject*>(l), const_cast<PObject*>(r));
	}
	return lo ? lo : this;
}

const PObject *PList::getval( ExecContextRoot *c, VLocal *vlocal)  const
{
	if ( constant ) return this;
	PList	*lo = 0;
	const PObject *l = lvalue->getval(c, vlocal);
	const PObject *r = rvalue->getval(c, vlocal);
	if ( l != lvalue || r != rvalue ) {
		lo = pmm.newPList(c->pobjs, const_cast<PObject*>(l), const_cast<PObject*>(r));
	}
	return lo ? lo : this;
}

const PObject *PArray::getval( ExecContextRoot *c)  const
{
	if ( constant ) return this;
	PArray	*po = 0;

	for ( PObjectArray::const_iterator i = value.begin(); i < value.end(); i++ ) {
		const PObject *p = (*i)->getval( c);
		if ( p != *i && po == 0 ) {
			po = pmm.newPArray(c->pobjs, *this);
		}
		if ( po ) {
			po->value[i - value.begin()] = p;
			po->constant = po->constant && p->isc();
		}
	}
	return po ? po : this;
}


const PObject *PArray::getval( ExecContextRoot *c, VLocal *vlocal)  const
{
	if ( constant ) return this;
	PArray	*po = 0;

	for ( PObjectArray::const_iterator i = value.begin(); i < value.end(); i++ ) {
		const PObject *p = (*i)->getval( c, vlocal);
		if ( p != *i && po == 0 ) {
			po = pmm.newPArray(c->pobjs, *this);
		}
		if ( po ) {
			po->value[i - value.begin()] = p;
			po->constant = po->constant && p->isc();
		}
	}
	return po ? po : this;
}

const PObject *PPredicate::getval( ExecContextRoot *c) const
{
	if ( constant ) return this;

	const PObject *no = name->getval(c);
	const PArray *ao = dynamic_cast<const PArray *>(arglist.getval( c));

	if ( no != name || ao != &arglist ) {
		PPredicate	*po = pmm.newPPredicate(c->pobjs,nspace,no,ao,opt);
		return po;
	}
	
	return this;
}

const PObject *PPredicate::getval( ExecContextRoot *c, VLocal *vlocal) const
{
	if ( constant ) return this;

	const PObject *no = name->getval(c, vlocal);
	const PArray *ao = dynamic_cast<const PArray *>(arglist.getval( c, vlocal));

	if ( no != name || ao != &arglist ) {
		PPredicate	*po = pmm.newPPredicate(c->pobjs,nspace,no,ao,opt);
		return po;
	}
	
	return this;
}

const PObject *PVeriable::getval( ExecContextRoot *c) const 
{
	assert( idx < c->gl->size());
	const PObject	*item = (*c->gl)[idx];
	if ( item == 0 ) {
		PObject *po = pmm.newPEVeriable(c->pobjs, *this, c->gl);
		return po;
	} else {	
		return item->getval(c);
	}
}

const PObject *PVeriable::getval( ExecContextRoot *c, VLocal *vlocal) const 
{
	assert( idx < vlocal->size());
	const PObject	*item = (*vlocal)[idx];
	if ( item == 0 ) {
		PObject *po = pmm.newPEVeriable(c->pobjs, *this, vlocal);
		return po;
	} else {	
		return item->getval(c, vlocal);
	}
}

const PINTEGER32 *PVeriable::c_integer32(ExecContextRoot *c) const
{
	assert( idx < c->gl->size());
	const PObject	*item = (*c->gl)[idx];
	if ( item == 0 ) {
		return 0;
	} else {	
		return item->c_integer32(c);
	}
}

const PINTEGER *PVeriable::c_integer(ExecContextRoot *c) const
{
	assert( idx < c->gl->size());
	const PObject	*item = (*c->gl)[idx];
	if ( item == 0 ) {
		return 0;
	} else {	
		return item->c_integer(c);
	}
}


const PObject *PEVeriable::getval( ExecContextRoot *c) const
{
	VLocal *local = vl;
	const PObject *item = (*local)[idx];
	if ( item == 0 ) {
		return this;
	} else {
		return item->getval(c);
	}
}

const PObject *PEVeriable::getval( ExecContextRoot *c, VLocal *) const
{
	VLocal *local = vl;
	const PObject *item = (*local)[idx];
	if ( item == 0 ) {
		return this;
	} else {
		return item->getval(c, local);
	}
}

const PINTEGER32 *PEVeriable::c_integer32(ExecContextRoot *c) const
{
	VLocal *local = vl;
	const PObject	*item = (*local)[idx];
	if ( item == 0 ) {
		return 0;
	} else {	
		return item->c_integer32(c);
	}
}


const PINTEGER *PEVeriable::c_integer(ExecContextRoot *c) const
{
	VLocal *local = vl;
	const PObject	*item = (*local)[idx];
	if ( item == 0 ) {
		return 0;
	} else {	
		return item->c_integer(c);
	}
}
