From 6c196ec8a41d6ed506c133c8b33dba9684f9a7a6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Mar 2010 12:34:43 +0000 Subject: Updated raytracer test. Added SPASS test. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- test/spass/unify.c | 857 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 857 insertions(+) create mode 100644 test/spass/unify.c (limited to 'test/spass/unify.c') diff --git a/test/spass/unify.c b/test/spass/unify.c new file mode 100644 index 00000000..14cc7a6a --- /dev/null +++ b/test/spass/unify.c @@ -0,0 +1,857 @@ +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * STANDARD UNIFICATION * */ +/* * * */ +/* * $Module: UNIFY * */ +/* * * */ +/* * Copyright (C) 1996, 1997, 1998, 2000, 2001 * */ +/* * MPI fuer Informatik * */ +/* * * */ +/* * This program is free software; you can redistribute * */ +/* * it and/or modify it under the terms of the GNU * */ +/* * General Public License as published by the Free * */ +/* * Software Foundation; either version 2 of the License, * */ +/* * or (at your option) any later version. * */ +/* * * */ +/* * 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., 59 Temple * */ +/* * Place, Suite 330, Boston, MA 02111-1307 USA * */ +/* * * */ +/* * * */ +/* $Revision: 21527 $ * */ +/* $State$ * */ +/* $Date: 2005-04-24 21:10:28 -0700 (Sun, 24 Apr 2005) $ * */ +/* $Author: duraid $ * */ +/* * * */ +/* * Contact: * */ +/* * Christoph Weidenbach * */ +/* * MPI fuer Informatik * */ +/* * Stuhlsatzenhausweg 85 * */ +/* * 66123 Saarbruecken * */ +/* * Email: weidenb@mpi-sb.mpg.de * */ +/* * Germany * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +/* $RCSfile$ */ + +#include "unify.h" + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * INITIALIZATION * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +void unify_Init(void) +/********************************************************** + INPUT: None. + RETURNS: None. + EFFECT: Initializes the unify module. +********************************************************/ +{ + +} + +void unify_Free(void) +/********************************************************** + INPUT: None. + RETURNS: None. + EFFECT: Frees internal structures of the unify module. +********************************************************/ +{ + +} + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * MISC FUNCTIONS * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * OCCUR CHECK * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +BOOL unify_OccurCheckCom(SYMBOL Top, CONTEXT Context, TERM Term) +/********************************************************** + INPUT: A variable symbol, a context, and a term. + RETURNS: TRUE if there is a occur check failure with respect + to the variable symbol and . + The search is started in +***********************************************************/ +{ + int Bottom; + LIST Args; + + Bottom = stack_Bottom(); + + for (;;) { + + if (term_IsVariable(Term)) { + if (symbol_Equal(Top, term_TopSymbol(Term))) { + stack_SetBottom(Bottom); + return TRUE; + } else if (cont_VarIsBound(Context, term_TopSymbol(Term))) { + Term = cont_ContextBindingTerm(Context, term_TopSymbol(Term)); + continue; + } + + } else if (term_IsComplex(Term)) { + + Args = term_ArgumentList(Term); + if (!list_Empty(list_Cdr(Args))) + stack_Push(list_Cdr(Args)); + + Term = list_Car(Args); + continue; + } + + if (stack_Empty(Bottom)) + return FALSE; + else { + Args = (LIST)stack_PopResult(); + Term = list_Car(Args); + if (!list_Empty(list_Cdr(Args))) + stack_Push(list_Cdr(Args)); + } + } +} + + +BOOL unify_OccurCheck(CONTEXT CTop, SYMBOL Top, CONTEXT CTerm, TERM Term) +/********************************************************** + INPUT: A context, a variable symbol, a context, and a term. + RETURNS: TRUE if there is a occur check failure with respect + to the variable symbol and . + The search is started in +***********************************************************/ +{ + int Bottom; + LIST Args; + SYMBOL TermTop; + + Bottom = stack_Bottom(); + + for (;;) { + + if (term_IsVariable(Term)) { + + TermTop = term_TopSymbol(Term); + + if ((CTop == CTerm) && (symbol_Equal(Top, TermTop))) { + stack_SetBottom(Bottom); + return TRUE; + } else if (cont_VarIsBound(CTerm, TermTop)) { + Term = cont_ContextBindingTerm(CTerm, TermTop); + CTerm = cont_ContextBindingContext(CTerm, TermTop); + continue; + } + } else if (term_IsComplex(Term)) { + + Args = term_ArgumentList(Term); + if (!list_Empty(list_Cdr(Args))) { + stack_Push(CTerm); + stack_Push(list_Cdr(Args)); + } + Term = list_Car(Args); + continue; + + } + + if (stack_Empty(Bottom)) + return FALSE; + else { + Args = (LIST)stack_PopResult(); + Term = list_Car(Args); + CTerm = (CONTEXT)stack_Top(); + if (list_Empty(list_Cdr(Args))) + stack_Pop(); + else + stack_Push(list_Cdr(Args)); + } + } +} + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * UNIFICATION * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +BOOL unify_Unify(CONTEXT CtL, TERM TermL, CONTEXT CtR, TERM TermR) +/********************************************************** + INPUT: Two terms which may contain the same variable symbols. + Equal variable symbols are interpreted different in + and , respectively. + RETURNS: TRUE, if and are unifiable, FALSE otherwise. + CAUTION: None. +***********************************************************/ +{ + CONTEXT CHelp; + LIST ArgsL, ArgsR; + int Bottom; + BOOL Bound; + + Bound = FALSE; + Bottom = stack_Bottom(); + + for (;;) { + + while (term_IsVariable(TermL) && + cont_VarIsBound(CtL, term_TopSymbol(TermL))) { + CHelp = cont_ContextBindingContext(CtL, term_TopSymbol(TermL)); + TermL = cont_ContextBindingTerm(CtL, term_TopSymbol(TermL)); + CtL = CHelp; + } + + while (term_IsVariable(TermR) && + cont_VarIsBound(CtR, term_TopSymbol(TermR))) { + CHelp = cont_ContextBindingContext(CtR, term_TopSymbol(TermR)); + TermR = cont_ContextBindingTerm(CtR, term_TopSymbol(TermR)); + CtR = CHelp; + } + + /* Caution: Bindings from variable to variable are made with priority + from the right context into the left context. */ + + if (term_IsVariable(TermL)) { + if (term_IsVariable(TermR)) { + if (!(CtL == CtR && term_EqualTopSymbols(TermL, TermR))) + Bound = cont_CreateBinding(CtR, term_TopSymbol(TermR), CtL, TermL); + } else if (Bound && unify_OccurCheck(CtL, term_TopSymbol(TermL), CtR, TermR)) { + stack_SetBottom(Bottom); + return FALSE; + } else + Bound = cont_CreateBinding(CtL, term_TopSymbol(TermL), CtR, TermR); + + } else if (term_IsVariable(TermR)) { + if (Bound && unify_OccurCheck(CtR, term_TopSymbol(TermR), CtL, TermL)) { + stack_SetBottom(Bottom); + return FALSE; + } else + Bound = cont_CreateBinding(CtR, term_TopSymbol(TermR), CtL, TermL); + + } else if (term_EqualTopSymbols(TermL, TermR)) { + if (term_IsComplex(TermL) && TermL != TermR) { + ArgsL = term_ArgumentList(TermL); + ArgsR = term_ArgumentList(TermR); + if (!list_Empty(list_Cdr(ArgsL))) { + stack_Push(CtL); + stack_Push(CtR); + stack_Push(list_Cdr(ArgsL)); + stack_Push(list_Cdr(ArgsR)); + } + TermL = list_Car(ArgsL); + TermR = list_Car(ArgsR); + continue; + } + } else { + stack_SetBottom(Bottom); + return FALSE; + } + + if (stack_Empty(Bottom)) + return TRUE; + else { + ArgsR = stack_PopResult(); + ArgsL = stack_PopResult(); + TermR = list_Car(ArgsR); + TermL = list_Car(ArgsL); + CtR = (CONTEXT)stack_Top(); + CtL = (CONTEXT)stack_NthTop(1); + if (list_Empty(list_Cdr(ArgsL))) + stack_NPop(2); + else { + stack_Push(list_Cdr(ArgsL)); + stack_Push(list_Cdr(ArgsR)); + } + } + } +} + +BOOL unify_UnifyCom(CONTEXT Context, TERM TermL, TERM TermR) +/********************************************************** + INPUT: Two terms which may contain the same variable symbols. + Equal variable symbols are interpreted equally in + and , respectively. + RETURNS: TRUE, if and are unifiable, FALSE otherwise. + CAUTION: None. +***********************************************************/ +{ + LIST ArgsL, ArgsR; + int Bottom; + + Bottom = stack_Bottom(); + + for (;;) { + + while (term_IsVariable(TermL) && + cont_VarIsBound(Context, term_TopSymbol(TermL))) + TermL = cont_ContextBindingTerm(Context, term_TopSymbol(TermL)); + + while (term_IsVariable(TermR) && + cont_VarIsBound(Context, term_TopSymbol(TermR))) + TermR = cont_ContextBindingTerm(Context, term_TopSymbol(TermR)); + + if (term_EqualTopSymbols(TermL, TermR)) { + if (term_IsComplex(TermL) && TermL != TermR) { + ArgsL = term_ArgumentList(TermL); + ArgsR = term_ArgumentList(TermR); + if (!list_Empty(list_Cdr(ArgsL))) { + stack_Push(list_Cdr(ArgsL)); + stack_Push(list_Cdr(ArgsR)); + } + TermL = list_Car(ArgsL); + TermR = list_Car(ArgsR); + continue; + } + } else if (term_IsVariable(TermL)) { + if (term_IsVariable(TermR)) + cont_CreateBinding(Context, term_TopSymbol(TermL), Context, TermR); + else if (unify_OccurCheckCom(term_TopSymbol(TermL), Context, TermR)) { + stack_SetBottom(Bottom); + return FALSE; + } else + cont_CreateBinding(Context, term_TopSymbol(TermL), Context, TermR); + + } else if (term_IsVariable(TermR)) { + if (unify_OccurCheckCom(term_TopSymbol(TermR), Context, TermL)) { + stack_SetBottom(Bottom); + return FALSE; + } else + cont_CreateBinding(Context, term_TopSymbol(TermR), Context, TermL); + + } else { + stack_SetBottom(Bottom); + return FALSE; + } + + if (stack_Empty(Bottom)) + return TRUE; + else { + ArgsR = stack_PopResult(); + ArgsL = stack_PopResult(); + TermR = list_Car(ArgsR); + TermL = list_Car(ArgsL); + if (!list_Empty(list_Cdr(ArgsL))) { + stack_Push(list_Cdr(ArgsL)); + stack_Push(list_Cdr(ArgsR)); + } + } + } +} + + + +BOOL unify_UnifyNoOC(CONTEXT CtL, TERM TermL, CONTEXT CtR, TERM TermR) +/********************************************************** + INPUT: Two terms which may contain the same variable symbols. + Equal variable symbols are interpreted different in + and , respectively. + RETURNS: TRUE, if and are unifiable, FALSE otherwise. + CAUTION: None. +***********************************************************/ +{ + CONTEXT CHelp; + LIST ArgsL, ArgsR; + int Bottom; + + Bottom = stack_Bottom(); + + for (;;) { + + while (term_IsVariable(TermL) && + cont_VarIsBound(CtL, term_TopSymbol(TermL))) { + CHelp = cont_ContextBindingContext(CtL, term_TopSymbol(TermL)); + TermL = cont_ContextBindingTerm(CtL, term_TopSymbol(TermL)); + CtL = CHelp; + } + + while (term_IsVariable(TermR) && + cont_VarIsBound(CtR, term_TopSymbol(TermR))) { + CHelp = cont_ContextBindingContext(CtR, term_TopSymbol(TermR)); + TermR = cont_ContextBindingTerm(CtR, term_TopSymbol(TermR)); + CtR = CHelp; + } + + /* Caution: Bindings from variable to variable are made with priority + from the right context into the left context. */ + + if (term_IsVariable(TermL)) { + if (term_IsVariable(TermR)) { + if (!(CtL == CtR && term_EqualTopSymbols(TermL, TermR))) + cont_CreateBinding(CtR, term_TopSymbol(TermR), CtL, TermL); + } else + cont_CreateBinding(CtL, term_TopSymbol(TermL), CtR, TermR); + + } else if (term_IsVariable(TermR)) + cont_CreateBinding(CtR, term_TopSymbol(TermR), CtL, TermL); + + else if (term_EqualTopSymbols(TermL, TermR)) { + if (term_IsComplex(TermL) && TermL != TermR) { + ArgsL = term_ArgumentList(TermL); + ArgsR = term_ArgumentList(TermR); + if (!list_Empty(list_Cdr(ArgsL))) { + stack_Push(CtL); + stack_Push(CtR); + stack_Push(list_Cdr(ArgsL)); + stack_Push(list_Cdr(ArgsR)); + } + TermL = list_Car(ArgsL); + TermR = list_Car(ArgsR); + continue; + } + } else { + stack_SetBottom(Bottom); + return FALSE; + } + + if (stack_Empty(Bottom)) + return TRUE; + else { + ArgsR = stack_PopResult(); + ArgsL = stack_PopResult(); + TermR = list_Car(ArgsR); + TermL = list_Car(ArgsL); + CtR = (CONTEXT) stack_Top(); + CtL = (CONTEXT) stack_NthTop(1); + if (list_Empty(list_Cdr(ArgsL))) + stack_NPop(2); + else { + stack_Push(list_Cdr(ArgsL)); + stack_Push(list_Cdr(ArgsR)); + } + } + } +} + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * UNIFICATION WITH FULL OCCUR CHECK (recursive) * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +BOOL unify_UnifyAllOC(CONTEXT IndexContext, CONTEXT CtL, TERM TermL, CONTEXT CtR, TERM TermR) +{ + while (term_IsVariable(TermL)) { + SYMBOL TermTop; + + TermTop = term_TopSymbol(TermL); + + if (cont_VarIsBound(CtL, TermTop)) { + CONTEXT CHelp; + + CHelp = cont_ContextBindingContext(CtL, TermTop); + TermL = cont_ContextBindingTerm(CtL, TermTop); + CtL = CHelp; + } else + break; + } + + while (term_IsVariable(TermR)) { + SYMBOL TermTop; + + TermTop = term_TopSymbol(TermR); + + if (cont_VarIsBound(CtR, TermTop)) { + CONTEXT CHelp; + + CHelp = cont_ContextBindingContext(CtR, TermTop); + TermR = cont_ContextBindingTerm(CtR, TermTop); + CtR = CHelp; + } else + break; + } + + if (term_IsVariable(TermL)) { + + if (term_IsVariable(TermR)) { + if ((CtL != CtR || !term_EqualTopSymbols(TermL, TermR))) { + if (term_IsIndexVariable(TermL)) + cont_CreateBinding(CtL, term_TopSymbol(TermL), CtR, TermR); + else + if (term_IsIndexVariable(TermR) || (CtR == IndexContext)) + cont_CreateBinding(CtR, term_TopSymbol(TermR), CtL, TermL); + else + cont_CreateBinding(CtL, term_TopSymbol(TermL), CtR, TermR); + } + return TRUE; + } + else + if (unify_OccurCheck(CtL, term_TopSymbol(TermL), CtR, TermR)) + return FALSE; + else { + cont_CreateBinding(CtL, term_TopSymbol(TermL), CtR, TermR); + return TRUE; + } + } + else + if (term_IsVariable(TermR)) { + if (unify_OccurCheck(CtR, term_TopSymbol(TermR), CtL, TermL)) + return FALSE; + else { + cont_CreateBinding(CtR, term_TopSymbol(TermR), CtL, TermL); + return TRUE; + } + } + else + if (term_EqualTopSymbols(TermL, TermR)) { + if (term_IsComplex(TermL)) { + LIST ArgL, ArgR; + for (ArgL = term_ArgumentList(TermL), ArgR = term_ArgumentList(TermR); + !list_Empty(ArgL); + ArgL = list_Cdr(ArgL), ArgR = list_Cdr(ArgR)) + if (!unify_UnifyAllOC(IndexContext, CtL, list_Car(ArgL), CtR, list_Car(ArgR))) + return FALSE; + } + return TRUE; + } + else + return FALSE; +} + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * GENERALIZATION TEST * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +BOOL unify_Match(CONTEXT Context, TERM TermL, TERM TermR) +{ + if (term_IsVariable(TermL)) { + if (cont_VarIsBound(Context, term_TopSymbol(TermL))) + return term_Equal(cont_ContextBindingTerm(Context, term_TopSymbol(TermL)), TermR); + else { + cont_CreateBinding(Context, term_TopSymbol(TermL), cont_InstanceContext(), TermR); + return TRUE; + } + } else if (term_EqualTopSymbols(TermL, TermR)) { + if (term_IsComplex(TermL)) { + LIST ArgL; + LIST ArgR; + for (ArgL = term_ArgumentList(TermL), ArgR = term_ArgumentList(TermR); + !list_Empty(ArgL); + ArgL = list_Cdr(ArgL), ArgR = list_Cdr(ArgR)) + if (!unify_Match(Context, list_Car(ArgL), list_Car(ArgR))) + return FALSE; + } + return TRUE; + } else + return FALSE; +} + +BOOL unify_MatchFlexible(CONTEXT Context, TERM TermL, TERM TermR) +/************************************************************** + INPUT: Two terms where symbols with flexible arity are allowed. + RETURNS: TRUE if matches . +***************************************************************/ +{ + if (term_IsVariable(TermL)) { + if (cont_VarIsBound(Context, term_TopSymbol(TermL))) + return term_Equal(cont_ContextBindingTerm(Context, term_TopSymbol(TermL)), TermR); + else { + cont_CreateBinding(Context, term_TopSymbol(TermL), cont_InstanceContext(), TermR); + return TRUE; + } + } else + if (term_EqualTopSymbols(TermL, TermR) + && list_Length(term_ArgumentList(TermL)) == list_Length(term_ArgumentList(TermR))) { + if (term_IsComplex(TermL)) { + LIST ArgL; + LIST ArgR; + for (ArgL = term_ArgumentList(TermL), ArgR = term_ArgumentList(TermR); + !list_Empty(ArgL); + ArgL = list_Cdr(ArgL), ArgR = list_Cdr(ArgR)) + if (!unify_MatchFlexible(Context, list_Car(ArgL), list_Car(ArgR))) + return FALSE; + } + return TRUE; + } + else + return FALSE; +} + + +void unify_EstablishMatcher(CONTEXT Context, SUBST Subst) +{ + while (subst_Exist(Subst)) { + /* Index to query */ + cont_CreateBinding(Context, subst_Dom(Subst), cont_InstanceContext(), subst_Cod(Subst)); + Subst = subst_Next(Subst); + } +} + + +BOOL unify_MatchBindingsHelp(const CONTEXT IndexContext, TERM TermL, CONTEXT CtR, TERM TermR) +{ + while (term_IsVariable(TermR)) { + SYMBOL TermTop; + + TermTop = term_TopSymbol(TermR); + + if (symbol_IsIndexVariable(TermTop)) + CtR = IndexContext; + else if (CtR == cont_InstanceContext()) + break; + + if (cont_VarIsBound(CtR, TermTop)) { + CONTEXT CHelp; + + CHelp = cont_ContextBindingContext(CtR, TermTop); + TermR = cont_ContextBindingTerm(CtR, TermTop); + CtR = CHelp; + } else + break; + } + + if (term_IsVariable(TermL)) { + /* Assertion: Variables of 'TermL' are bound in the index context only. */ + + if (cont_VarIsBound(IndexContext, term_TopSymbol(TermL))) + return + cont_TermEqualModuloBindings(IndexContext, + cont_ContextBindingContext(IndexContext, + term_TopSymbol(TermL)), + cont_ContextBindingTerm(IndexContext, + term_TopSymbol(TermL)), + CtR, + TermR); + else { + cont_CreateBinding(IndexContext, term_TopSymbol(TermL), CtR, TermR); + return TRUE; + } + } else if (term_EqualTopSymbols(TermL, TermR)) { + if (term_IsComplex(TermL)) { + LIST ArgL; + LIST ArgR; + + for (ArgL = term_ArgumentList(TermL), ArgR = term_ArgumentList(TermR); + !list_Empty(ArgL); + ArgL = list_Cdr(ArgL), ArgR = list_Cdr(ArgR)) + if (!unify_MatchBindingsHelp(IndexContext, list_Car(ArgL), CtR, list_Car(ArgR))) + return FALSE; + } + + return TRUE; + } else + return FALSE; +} + + +BOOL unify_MatchBindings(const CONTEXT IndexContext, TERM TermL, TERM TermR) +{ + return unify_MatchBindingsHelp(IndexContext, TermL, cont_InstanceContext(), TermR); +} + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * INSTANCE TEST * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +BOOL unify_MatchReverse(const CONTEXT IndexContext, TERM TermL, CONTEXT CtR, + TERM TermR) +/********************************************************* + INPUT: 'TermL' is in IndexContext and the codomain of a subst., + 'CtR' is the context of 'TermR' which is the codomain of a subst. + obtained by a variable binding, 'Bindings' is + the number of established bindings. + RETURNS: TRUE, if 'TermL' is an instance of 'TermR'; + FALSE, otherwise. +**********************************************************/ +{ + while (term_IsVariable(TermR)) { + SYMBOL TermTop; + + TermTop = term_TopSymbol(TermR); + + if (symbol_IsIndexVariable(TermTop)) + CtR = IndexContext; + else if (CtR == cont_InstanceContext()) + break; + + if (cont_VarIsBound(CtR, TermTop)) { + CONTEXT CHelp; + + CHelp = cont_ContextBindingContext(CtR, TermTop); + TermR = cont_ContextBindingTerm(CtR, TermTop); + CtR = CHelp; + } else + break; + } + + if (term_IsVariable(TermL)) { + if ((CtR == cont_InstanceContext()) && term_EqualTopSymbols(TermL, TermR)) + /* 'TermL' and 'TermR' are exactly the same variables (via bindings), + therefore do not bind them, just return positive. */ + return TRUE; + + else if (term_IsIndexVariable(TermL)) { + cont_CreateBinding(IndexContext, term_TopSymbol(TermL), CtR, TermR); + return TRUE; + + } else if (term_IsVariable(TermR) && + (term_IsIndexVariable(TermR) || (CtR == IndexContext))) { + cont_CreateBinding(IndexContext, term_TopSymbol(TermR), cont_InstanceContext(), TermL); + return TRUE; + + } else + return FALSE; + + } else if (term_IsVariable(TermR)) { + if (term_IsIndexVariable(TermR) || (CtR == IndexContext)) { + cont_CreateBinding(IndexContext, term_TopSymbol(TermR), cont_InstanceContext(), TermL); + return TRUE; + } else + return FALSE; + + } else if (term_EqualTopSymbols(TermL, TermR)) { + + if (term_IsComplex(TermL)) { + LIST ArgL, ArgR; + for (ArgL = term_ArgumentList(TermL), ArgR = term_ArgumentList(TermR); + !list_Empty(ArgL); + ArgL = list_Cdr(ArgL), ArgR = list_Cdr(ArgR)) + if (!unify_MatchReverse(IndexContext, + list_Car(ArgL), + CtR, + list_Car(ArgR))) + return FALSE; + } + return TRUE; + } else + return FALSE; +} + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * VARIATION TEST * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +BOOL unify_Variation(const CONTEXT Context, TERM TermL, TERM TermR) +{ + if (term_IsVariable(TermL)) { + if (term_EqualTopSymbols(TermL, TermR)) + /* TermL and TermR are in different contexts + but both are term variables which do not need to be variated. + Index variables cannot occur in TermR + which is the term to be inserted. */ + return TRUE; + else if (term_IsIndexVariable(TermL)) { + if (cont_VarIsBound(Context, term_TopSymbol(TermL))) + return term_Equal(cont_ContextBindingTerm(Context, term_TopSymbol(TermL)), TermR); + else { + /* Index to query */ + cont_CreateBinding(Context, term_TopSymbol(TermL), Context, TermR); + return TRUE; + } + } + else + return FALSE; + + } else if (term_EqualTopSymbols(TermL, TermR)) { + if (term_IsComplex(TermL)) { + LIST ArgL; + LIST ArgR; + for (ArgL = term_ArgumentList(TermL), ArgR = term_ArgumentList(TermR); + !list_Empty(ArgL); + ArgL = list_Cdr(ArgL), ArgR = list_Cdr(ArgR)) + if (!unify_Variation(Context, list_Car(ArgL), list_Car(ArgR))) + return FALSE; + } + return TRUE; + } else + return FALSE; +} + + +/**************************************************************/ +/* ********************************************************** */ +/* * * */ +/* * COMMON GENERALIZATIONS * */ +/* * * */ +/* ********************************************************** */ +/**************************************************************/ + + +TERM unify_ComGenLinear(const CONTEXT IndexContext, + SUBST* SubstL, TERM TermL, SUBST* SubstR, TERM TermR) +{ + if (term_IsIndexVariable(TermR)) { + *SubstL = subst_Add(term_TopSymbol(TermR), term_Copy(TermL), *SubstL); + + return term_Copy(TermR); + + } else if (term_EqualTopSymbols(TermL, TermR)) { + + LIST ArgList, ArgL, ArgR; + + ArgList = list_Nil(); + for (ArgL = term_ArgumentList(TermL), ArgR = term_ArgumentList(TermR); + !list_Empty(ArgL); + ArgL = list_Cdr(ArgL), ArgR = list_Cdr(ArgR)) + ArgList = list_Nconc(ArgList, + list_List(unify_ComGenLinear(IndexContext, + SubstL, + list_Car(ArgL), + SubstR, + list_Car(ArgR)))); + return term_Create(term_TopSymbol(TermL), ArgList); + + } else { + + SYMBOL Symbol; + + Symbol = cont_NextIndexVariable(IndexContext); + + *SubstL = subst_Add(Symbol, term_Copy(TermL), *SubstL); + *SubstR = subst_Add(Symbol, term_Copy(TermR), *SubstR); + + return term_Create(Symbol, list_Nil()); + } +} + -- cgit