unfy/unfy.c

/*    This file is part of unfy.
 *
 *    Unfy is free software: you can redistribute it and/or modify
 *    it under the terms of the GNU Lesser General Public License as published by
 *    the Free Software Foundation, either version 3 of the License, or
 *    (at your option) any later version.
 *
 *    Unfy 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 Lesser General Public License for more details.
 *
 *    You should have received a copy of the GNU Lesser General Public License
 *    along with unfy.  If not, see <http://www.gnu.org/licenses/>.
*/

#include <rid.h>
#include <stdlib.h>

#define STYLE_9
#include "unfy.h"

#define SWAP(ptr1, ptr2) \
	do { void *SWAP = ptr1; ptr1 = ptr2; ptr2 = SWAP; } while (0)

static Unfy_term *
get_term(Unfy_recycle *rec)
{
	Unfy_term *term = rec->terms;

	if (!term)
		return malloc(sizeof(*term));

	rec->terms = term->u.dat;
	return term;
}

static Unfy_list *
get_list(Unfy_recycle *rec)
{
	Unfy_list *list = rec->lists;

	if (!list)
		return malloc(sizeof(*list));

	rec->lists = list->next;
	return list;
}

static Unfy_bind *
get_bind(Unfy_recycle *rec)
{
	Unfy_bind *bind = rec->binds;

	if (!bind)
		return malloc(sizeof(*bind));

	rec->binds = bind->next;
	return bind;
}

void
unfy_recycle_init(Unfy_recycle *rec)
{
	rec->terms = NULL;
	rec->lists = NULL;
	rec->binds = NULL;
}

void
unfy_recycle_empty(Unfy_recycle *rec)
{
	while (rec->terms) {
		Unfy_term *term = rec->terms;

		rec->terms = term->u.dat;
		free(term);
	}

	while (rec->lists) {
		Unfy_list *tmp = rec->lists;

		rec->lists = tmp->next;
		free(tmp);
	}

	while (rec->binds) {
		Unfy_bind *tmp = rec->binds;

		rec->binds = tmp->next;
		free(tmp);
	}
}

void
unfy_recycle_term(Unfy_recycle *rec, Unfy_term *term)
{
	if (!term)
		return;

	switch (term->type) {
	case UNFY_LIST:
		unfy_recycle_list(rec, term->u.list);
		/* fall through */
	case UNFY_CONST:
	case UNFY_ORDER:
	case UNFY_IGN:
	case UNFY_VAR:
		term->u.dat = rec->terms;
		rec->terms = term;
	}
}

void
unfy_recycle_list(Unfy_recycle *rec, Unfy_list *list)
{
	Unfy_list *end = list;

	if (!list)
		return;

	while (1) {
		unfy_recycle_term(rec, end->term);

		if (!end->next)
			break;

		end = end->next;
	}

	end->next = rec->lists;
	rec->lists = list;
}

void
unfy_recycle_bind(Unfy_recycle *rec, Unfy_bind *bind)
{
	Unfy_bind *end = bind;

	if (!bind)
		return;

	while (1) {
		unfy_recycle_term(rec, end->term);

		if (!end->next)
			break;

		end = end->next;
	}

	end->next = rec->binds;
	rec->binds = bind;
}

Unfy_term *
unfy_term(Unfy_type type, void *dat, Unfy_recycle *rec)
{
	Unfy_term *term = get_term(rec);

        if (!term)
		return NULL;

	unfy_term_init(term, type, dat);
	return term;
}

Unfy_term *
unfy_term_id(Unfy_type type, const Rid id, Unfy_recycle *rec)
{
	Unfy_term *term = get_term(rec);

        if (!term)
		return NULL;

	term->type = type;
	rid_set(term->u.id, id);
	return term;
}

Unfy_term *
unfy_term_copy(const Unfy_term *term, Unfy_recycle *rec)
{
	Unfy_term *copy = get_term(rec);

        if (!copy)
		return NULL;

	if (unfy_term_init_copy(copy, term, rec) < 0) {
		unfy_recycle_term(rec, copy);
		return NULL;
	}

	return copy;
}

void
unfy_term_init(Unfy_term *term, Unfy_type type, void *dat)
{
	switch ((term->type = type)) {
	case UNFY_ORDER:
		term->u.order = *(size_t *) dat;
		break;
	case UNFY_IGN:
		break;
	case UNFY_CONST:
		/* fallthru */
	case UNFY_VAR:
		rid_set(term->u.id, dat);
		break;
	case UNFY_LIST:
		term->u.list = dat;
		break;
	}
}

int
unfy_term_init_copy(Unfy_term *des, const Unfy_term *src, Unfy_recycle *rec)
{
	Unfy_list *list = NULL;

	switch (src->type) {
	case UNFY_CONST:
	case UNFY_VAR:
		rid_set(des->u.id, src->u.id);
		break;
	case UNFY_ORDER:
		des->u.order = src->u.order;
		break;
	case UNFY_IGN:
		break;
	case UNFY_LIST:
		if (src->u.list && unfy_list_copy(&list, src->u.list, rec) < 0)
				return -1;

		des->u.list = list;
		break;
	}

	des->type = src->type;
	return 0;
}

Unfy_stat
unfy_list_same(Unfy_info *info, Unfy_list *llist, Unfy_list *rlist,
	       Unfy_recycle *rec)
{
	Unfy_term *tmp_left = info->left;
	Unfy_term *tmp_right = info->right;
	Unfy_stat stat;

	for (; llist; llist = llist->next, rlist = rlist->next) {
		if (!rlist) {
			info->rsn = UNFY_RSN_LEN;
			return UNFY_NO;
		}

		info->left = llist->term;
		info->right = rlist->term;
		stat = unfy_term_same(info, rec);

		if (stat != UNFY_YES)
			return stat;

		info->left = tmp_left;
		info->right = tmp_right;
	}

	if (rlist) {
		info->rsn = UNFY_RSN_LEN;
		return UNFY_NO;
	}

	return UNFY_YES;
}

Unfy_stat
unfy_term_same(Unfy_info *info, Unfy_recycle *rec)
{
	Unfy_term *copy;

	if (info->left->type != info->right->type) {
		info->rsn = UNFY_RSN_TYPE;
		return UNFY_NO;
	}

	switch (info->right->type) {
	case UNFY_CONST:
		if (!rid_cmp(info->left->u.id, info->right->u.id))
			return UNFY_YES;

		info->rsn = UNFY_RSN_VAL;
		return UNFY_NO;
	case UNFY_ORDER:
		if (info->left->u.order == info->right->u.order)
			return UNFY_YES;

		info->rsn = UNFY_RSN_VAL;
		return UNFY_NO;
	case UNFY_IGN:
		return UNFY_YES;
	case UNFY_LIST:
		return unfy_list_same(info, info->left->u.list,
				      info->right->u.list, rec);
	case UNFY_VAR:
		if ((copy = unfy_bind_get(info->lbind, info->left->u.id))) {
			if (!rid_cmp(copy->u.id, info->right->u.id))
				return UNFY_YES;

			info->rsn = UNFY_RSN_FORM;
			return UNFY_NO;
		}

		if (!(copy = unfy_term_copy(info->right, rec)))
			break;

		if (unfy_bind(&info->lbind, info->left->u.id, copy, rec) < 0) {
			unfy_recycle_term(rec, copy);
			break;
		}

		return UNFY_YES;
	}

	return UNFY_ERR;
}

static int
has_var(const Unfy_term *term, const Rid var_id)
{
	const Unfy_list *list;

	switch (term->type) {
	case UNFY_CONST:
	case UNFY_ORDER:
	case UNFY_IGN:
		break;
	case UNFY_LIST:
		list = term->u.list;

	        for (; list; list = list->next)
			if (has_var(list->term, var_id))
				return 1;

		break;
	case UNFY_VAR:
		return !rid_cmp(term->u.id, var_id);
	}

	return 0;
}

int
unfy_term_revar(const Unfy_term *term, Unfy_bind **bind, Unfy_recycle *rec)
{
	const Unfy_list *list;
        Unfy_term *var;

	switch (term->type) {
	case UNFY_CONST:
	case UNFY_ORDER:
	case UNFY_IGN:
		return 0;
	case UNFY_LIST:
		if (!(list = term->u.list))
			return 0;

		for (; list; list = list->next)
			if (unfy_term_revar(list->term, bind, rec) < 0)
				return -1;

		return 0;
	case UNFY_VAR:
		if (unfy_bind_get(*bind, term->u.id))
			return 0;

		if (!(var = unfy_term(UNFY_VAR, NULL, rec))) {
			unfy_recycle_bind(rec, *bind);
			*bind = NULL;
			return -1;
		}

		if (unfy_bind(bind, term->u.id, var, rec) < 0) {
			unfy_recycle_term(rec, var);
			unfy_recycle_bind(rec, *bind);
			*bind = NULL;
		        return -1;
		}

		return 0;
	}

	unfy_recycle_bind(rec, *bind);
	*bind = NULL;
	return -1;
}

Unfy_list *
unfy_list(Unfy_term *term, Unfy_list *next, Unfy_recycle *rec)
{
	Unfy_list *list = get_list(rec);

        if (!list)
		return NULL;

	unfy_list_init(list, term, next);
	return list;
}

int
unfy_list_copy(Unfy_list **copy, const Unfy_list *list, Unfy_recycle *rec)
{
	Unfy_list *head = NULL;
	Unfy_list **tail = &head;

        for (; list; list = list->next) {
		Unfy_term *term = unfy_term_copy(list->term, rec);

		if (!term) {
			unfy_recycle_list(rec, head);
			*copy = NULL;
			return -1;
		}

		if (!(tail = unfy_list_append(tail, term, rec))) {
			unfy_recycle_term(rec, term);
			unfy_recycle_list(rec, head);
			*copy = NULL;
			return -1;
		}
	}

        *copy = head;
	return 0;
}

void
unfy_list_init(Unfy_list *list, Unfy_term *term, Unfy_list *next)
{
	list->term = term;
	list->next = next;
}

int
unfy_list_init_copy(Unfy_list *copy, const Unfy_list *list, Unfy_recycle *rec)
{
	Unfy_term *term = unfy_term_copy(list->term, rec);
	Unfy_list *next;

        if (!term)
		return -1;

	if (unfy_list_copy(&next, list->next, rec) < 0) {
		unfy_recycle_term(rec, term);
		return -1;
	}

	unfy_list_init(copy, term, next);
	return 0;
}

Unfy_list **
unfy_list_append(Unfy_list **tail, Unfy_term *term, Unfy_recycle *rec)
{
	Unfy_list *new_tail = get_list(rec);

        if (!new_tail)
		return NULL;

	new_tail->term = term;
	new_tail->next = NULL;
	*tail = new_tail;
	return &new_tail->next;
}

int
unfy_bind(Unfy_bind **bind, const Rid var_id, Unfy_term *term,
	  Unfy_recycle *rec)
{
	Unfy_bind *new_bind = get_bind(rec);

	if (!new_bind)
		return -1;

	new_bind->next = *bind;
	rid_set(new_bind->var_id, var_id);
	new_bind->term = term;
	*bind = new_bind;
	return 0;
}

Unfy_bind *
unfy_bind_copy(const Unfy_bind *bind, Unfy_recycle *rec)
{
	Unfy_bind *copy = NULL;

	for (; bind; bind = bind->next) {
		Unfy_term *term = unfy_term_copy(bind->term, rec);

		if (!term) {
			unfy_recycle_bind(rec, copy);
			return NULL;
		}

		if (unfy_bind(&copy, bind->var_id, term, rec) < 0) {
			unfy_recycle_bind(rec, copy);
			unfy_recycle_term(rec, term);
			return NULL;
		}
	}

		return copy;
}

Unfy_term *
unfy_bind_get(const Unfy_bind *bind, const Rid var_id)
{
        for (; bind; bind = bind->next)
		if (!rid_cmp(bind->var_id, var_id))
			return bind->term;

	return NULL;
}

static Unfy_stat
term_replace(Unfy_term *term, const Rid var_id, const Unfy_term *val,
	     Unfy_recycle *rec)
{
	Unfy_list *list;

	switch (term->type) {
	case UNFY_CONST:
	case UNFY_ORDER:
	case UNFY_IGN:
		/* will never happen */
	        return UNFY_ERR;
	case UNFY_LIST:
		list = term->u.list;

	        for (; list; list = list->next)
			if (term_replace(list->term, var_id, val, rec) != UNFY_YES)
				return UNFY_ERR;

		break;
	case UNFY_VAR:
		if (!rid_cmp(term->u.id, var_id) &&
		    unfy_term_init_copy(term, val, rec) < 0)
			return UNFY_ERR;

		break;
	}

	return UNFY_YES;
}

Unfy_stat
unfy_bind_replace(Unfy_bind *bind, const Rid var_id, const Unfy_term *val,
		  Unfy_recycle *rec)
{
	for (; bind; bind = bind->next) {
		/* if the term does not have the var, ignore */
		if (!has_var(bind->term, var_id))
			continue;

		/* var cannot be replaced by a list containing itself */
		if (val->type == UNFY_LIST && has_var(val, bind->var_id))
			return UNFY_NO;

		/* shared var cannot be replaced by a list containing itself */
		if (bind->term->type == UNFY_VAR && val->type == UNFY_LIST &&
		    has_var(val, bind->term->u.id))
			return UNFY_NO;

		if (term_replace(bind->term, var_id, val, rec) != UNFY_YES)
			return UNFY_ERR;
	}

	return UNFY_YES;
}

Unfy_term *
unfy_term_bind(const Unfy_term *term, const Unfy_bind *bind, Unfy_recycle *rec)
{
	Unfy_term *copy = unfy_term_copy(term, rec);

        if (!copy)
		return NULL;

	if (unfy_term_bind_set(copy, bind, rec) < 0) {
		unfy_recycle_term(rec, copy);
		return NULL;
	}

	return copy;
}

int
unfy_term_bind_set(Unfy_term *term, const Unfy_bind *bind, Unfy_recycle *rec)
{
	Unfy_list *list;
	const Unfy_term *val;

	switch (term->type) {
	case UNFY_CONST:
	case UNFY_ORDER:
	case UNFY_IGN:
	        break;
	case UNFY_VAR:
		if (!(val = unfy_bind_get(bind, term->u.id)))
			break;

		return unfy_term_init_copy(term, val, rec);
	case UNFY_LIST:
		list = term->u.list;

	        for (; list; list = list->next)
			if (unfy_term_bind_set(list->term, bind, rec) < 0)
				return -1;

		break;
	}

	return 0;
}

static Unfy_stat
unify_consts(Unfy_info *info, Unfy_recycle *rec)
{
	(void) rec;

	if (rid_cmp(info->left->u.id, info->right->u.id)) {
		info->rsn = UNFY_RSN_VAL;
		return UNFY_NO;
	}

	return UNFY_YES;
}

static Unfy_stat
unify_orders(Unfy_info *info, Unfy_recycle *rec)
{
	(void) rec;

	if (info->left->u.order != info->right->u.order) {
		info->rsn = UNFY_RSN_VAL;
		return UNFY_NO;
	}

	return UNFY_YES;
}

static Unfy_stat
dont_unify(Unfy_info *info, Unfy_recycle *rec)
{
	(void) rec;

	info->rsn = UNFY_RSN_TYPE;
	return UNFY_NO;
}

static Unfy_stat
unify_lists(Unfy_info *info, Unfy_recycle *rec)
{
	Unfy_list *llist = info->left->u.list;
	Unfy_list *rlist = info->right->u.list;
	Unfy_term *tmp_left = info->left;
	Unfy_term *tmp_right = info->right;
	Unfy_stat stat;

        for (; llist; llist = llist->next, rlist = rlist->next) {
		if (!rlist) {
			info->rsn = UNFY_RSN_LEN;
			return UNFY_NO;
		}

	        info->left = llist->term;
	        info->right = rlist->term;
		stat = unfy_unify(info, rec);

		if (stat != UNFY_YES)
			return stat;

		info->left = tmp_left;
		info->right = tmp_right;
	}

	if (rlist) {
		info->rsn = UNFY_RSN_LEN;
		return UNFY_NO;
	}

	return UNFY_YES;
}

/* only use with a var_id from top level term since var_id is not copied */
static Unfy_stat
bind_add(Unfy_bind **primary, Unfy_bind **secondary,
	 const Rid var_id, const Unfy_term *val,
	 Unfy_recycle *rec)
{
	Unfy_term *bound = unfy_term_bind(val, *secondary, rec);

        if (!bound)
		return UNFY_ERR;

	/* var cannot be replaced by a list containing itself */
	if (bound->type == UNFY_LIST && has_var(bound, var_id)) {
		unfy_recycle_term(rec, bound);
		return UNFY_NO;
	}

	if (unfy_bind(primary, var_id, bound, rec) < 0) {
		unfy_recycle_term(rec, bound);
		return UNFY_ERR;
	}

	return unfy_bind_replace(*secondary, var_id, bound, rec);
}

static Unfy_stat
bind_set(Unfy_bind **primary, Unfy_bind **secondary,
	 Rid var_id, const Unfy_term *val, Unfy_recycle *rec)
{
	Unfy_term *bound = unfy_term_bind(val, *secondary, rec);
	Rid var_id2; /* var_id can be overwritten in replacement */
	Unfy_stat stat;

        if (!bound)
		return UNFY_ERR;

	rid_set(var_id2, var_id);

	if ((stat = unfy_bind_replace(*primary, var_id2, bound, rec)) == UNFY_YES)
		stat = unfy_bind_replace(*secondary, var_id2, bound, rec);

	unfy_recycle_term(rec, bound);
	return stat;
}

static Unfy_stat
unify_nonvar_var(Unfy_info *info, Unfy_recycle *rec)
{
	Unfy_term *val = unfy_bind_get(info->rbind, info->right->u.id);
	Unfy_stat stat;

	if (!val) {
		if ((stat = bind_add(&info->rbind, &info->lbind,
				     info->right->u.id, info->left,
				     rec)) == UNFY_NO)
			goto no;

		return stat;
	}

	if (val->type == UNFY_VAR) {
		if ((stat = bind_set(&info->rbind, &info->lbind,
				     val->u.id, info->left, rec)) == UNFY_NO)
			goto no;

		return stat;
	}

	/* swap temporarily if not no */
	SWAP(val, info->right);

        if ((stat = unfy_unify(info, rec)) == UNFY_NO) {
		info->rvar = info->rvar ? info->rvar : val;
	} else
		SWAP(val, info->right);

	return stat;
no:
	info->rsn = UNFY_RSN_SELF;
	return stat;
}

static Unfy_stat
unify_var_nonvar(Unfy_info *info, Unfy_recycle *rec)
{
	Unfy_stat stat;

	SWAP(info->left, info->right);
	SWAP(info->lbind, info->rbind);
        stat = unify_nonvar_var(info, rec);
	SWAP(info->left, info->right);
	SWAP(info->lbind, info->rbind);
	SWAP(info->lvar, info->rvar);
	return stat;
}

static Unfy_stat
unify_vars(Unfy_info *info, Unfy_recycle *rec)
{
	Unfy_term *lval = unfy_bind_get(info->lbind, info->left->u.id);
	Unfy_term *rval = unfy_bind_get(info->rbind, info->right->u.id);
	Unfy_stat stat;

	if (!lval) {
		Unfy_term shared;

		if (rval) {
			if ((stat = bind_add(&info->lbind, &info->rbind,
					     info->left->u.id,
					     rval, rec)) == UNFY_NO)
			        goto no;

			return stat;
		}

		/* create a new variable to be shared */
		unfy_term_init(&shared, UNFY_VAR, NULL);

		if ((stat = bind_add(&info->lbind, &info->rbind, info->left->u.id,
				     &shared, rec)) == UNFY_NO)
			goto no;

		if (stat != UNFY_YES)
			return stat;

	        if ((stat = bind_add(&info->rbind, &info->lbind,
				     info->right->u.id, &shared,
				     rec)) == UNFY_NO)
			goto no;

		return stat;
	}

	if (!rval) {
	        if ((stat = bind_add(&info->rbind, &info->lbind,
				     info->right->u.id, lval, rec)) == UNFY_NO)
			goto no;

		return stat;
	}

	if (lval->type == UNFY_VAR) {
		/* don't do extra work if same */
		if (rval->type == UNFY_VAR &&
		    !rid_cmp(lval->u.id, rval->u.id))
			return UNFY_YES;

	        if ((stat = bind_set(&info->lbind, &info->rbind,
				     lval->u.id, rval, rec)) == UNFY_NO)
			goto no;

		return stat;
	}

	if (rval->type == UNFY_VAR) {
	        if ((stat = bind_set(&info->rbind, &info->lbind,
				     rval->u.id, lval, rec)) == UNFY_NO)
			goto no;

		return stat;
	}

	/* temporary swap if not no */
	SWAP(info->left, lval);
	SWAP(info->right, rval);

        if ((stat = unfy_unify(info, rec)) == UNFY_NO) {
		info->lvar = info->lvar ? info->lvar : lval;
		info->lvar = info->rvar ? info->rvar : rval;
	} else {
		SWAP(info->left, lval);
		SWAP(info->right, rval);
	}

	return stat;
no:
	info->rsn = UNFY_RSN_SELF;
	return UNFY_NO;
}

static Unfy_stat
unify_ignore(Unfy_info *info, Unfy_recycle *rec)
{
	(void) info;
	(void) rec;

	return UNFY_YES;
}

Unfy_stat
unfy_unify(Unfy_info *info, Unfy_recycle *rec)
{
	typedef Unfy_stat (*Unfy_func)(Unfy_info *info, Unfy_recycle *rec);

	const Unfy_func table[5][5] = {
		[UNFY_CONST][UNFY_CONST] = unify_consts,
		[UNFY_CONST][UNFY_ORDER] = dont_unify,
		[UNFY_CONST][UNFY_IGN]   = unify_ignore,
		[UNFY_CONST][UNFY_LIST]  = dont_unify,
		[UNFY_CONST][UNFY_VAR]   = unify_nonvar_var,

		[UNFY_ORDER][UNFY_CONST] = dont_unify,
		[UNFY_ORDER][UNFY_ORDER] = unify_orders,
		[UNFY_ORDER][UNFY_IGN]   = unify_ignore,
		[UNFY_ORDER][UNFY_LIST]  = dont_unify,
		[UNFY_ORDER][UNFY_VAR]   = unify_nonvar_var,

		[UNFY_IGN]  [UNFY_CONST] = unify_ignore,
		[UNFY_IGN]  [UNFY_ORDER] = unify_ignore,
		[UNFY_IGN]  [UNFY_IGN]   = unify_ignore,
		[UNFY_IGN]  [UNFY_LIST]  = unify_ignore,
		[UNFY_IGN]  [UNFY_VAR]   = unify_ignore,

		[UNFY_LIST] [UNFY_CONST] = dont_unify,
		[UNFY_LIST] [UNFY_ORDER] = dont_unify,
		[UNFY_LIST] [UNFY_IGN]   = unify_ignore,
		[UNFY_LIST] [UNFY_LIST]  = unify_lists,
		[UNFY_LIST] [UNFY_VAR]   = unify_nonvar_var,

		[UNFY_VAR]  [UNFY_CONST] = unify_var_nonvar,
		[UNFY_VAR]  [UNFY_ORDER] = unify_var_nonvar,
		[UNFY_VAR]  [UNFY_IGN]   = unify_ignore,
		[UNFY_VAR]  [UNFY_LIST]  = unify_var_nonvar,
		[UNFY_VAR]  [UNFY_VAR]   = unify_vars,
	};

	return table[info->left->type][info->right->type](info, rec);
}

void
unfy_info_init(Unfy_info *info, Unfy_term *left, Unfy_term *right)
{
	info->lbind = NULL;
	info->rbind = NULL;
	info->rsn = UNFY_RSN_OKAY;
	info->left = left;
	info->right = right;
	info->lvar = NULL;
	info->rvar = NULL;
}

void
unfy_info_dispose(Unfy_info *info, Unfy_recycle *rec)
{
	unfy_recycle_bind(rec, info->lbind);
	unfy_recycle_bind(rec, info->rbind);
}