/**************************************************************/ /* ********************************************************** */ /* * * */ /* * SUBSTITUTION * */ /* * * */ /* * $Module: SUBSTITUTION * */ /* * * */ /* * Copyright (C) 1996, 1997, 1998, 1999, 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$ * */ /* $State$ * */ /* $Date$ * */ /* $Author$ * */ /* * * */ /* * Contact: * */ /* * Christoph Weidenbach * */ /* * MPI fuer Informatik * */ /* * Stuhlsatzenhausweg 85 * */ /* * 66123 Saarbruecken * */ /* * Email: weidenb@mpi-sb.mpg.de * */ /* * Germany * */ /* * * */ /* ********************************************************** */ /**************************************************************/ /* $RCSfile$ */ #include "subst.h" /**************************************************************/ /* ********************************************************** */ /* * * */ /* * SUBSTITUTION CREATION AND DELETION * */ /* * * */ /* ********************************************************** */ /**************************************************************/ SUBST subst_Add(SYMBOL Symbol, TERM Codomain, SUBST Subst) { SUBST Result; Result = subst_Get(); Result->next = Subst; Result->dom = Symbol; Result->codomain = Codomain; return Result; } void subst_Delete(SUBST Subst) { SUBST Next; while (subst_Exist(Subst)) { Next = subst_Next(Subst); if (subst_Cod(Subst)) term_Delete(subst_Cod(Subst)); subst_FreeOneNode(Subst); Subst = Next; } } void subst_Free(SUBST Subst) { SUBST Next; while (subst_Exist(Subst)) { Next = subst_Next(Subst); subst_FreeOneNode(Subst); Subst = Next; } } /**************************************************************/ /* ********************************************************** */ /* * * */ /* * FUNCTIONS ON SUBSTITUTIONS * */ /* * * */ /* ********************************************************** */ /**************************************************************/ TERM subst_Term(SYMBOL Symbol, SUBST Subst) { for (; subst_Exist(Subst); Subst = subst_Next(Subst)) if (symbol_Equal(Symbol,subst_Dom(Subst))) return subst_Cod(Subst); return (TERM)NULL; } static TERM subst_ApplyIntern(SUBST Subst, TERM Term) { TERM RplacTerm; LIST Arglist; SYMBOL Top; Top = term_TopSymbol(Term); if (symbol_IsVariable(Top) && (RplacTerm = subst_Term(Top,Subst))) { Arglist = term_CopyTermList(term_ArgumentList(RplacTerm)); term_RplacTop(Term, term_TopSymbol(RplacTerm)); term_DeleteTermList(term_ArgumentList(Term)); term_RplacArgumentList(Term, Arglist); } else { for (Arglist = term_ArgumentList(Term); !list_Empty(Arglist); Arglist = list_Cdr(Arglist)) subst_ApplyIntern(Subst, list_Car(Arglist)); } return Term; } TERM subst_Apply(SUBST Subst, TERM Term) { if (subst_Empty(Subst)) return Term; return subst_ApplyIntern(Subst, Term); } SUBST subst_Merge(SUBST Source, SUBST Drain) { SUBST Scan; BOOL Changed; for (; subst_Exist(Source); Source = subst_Next(Source)) { /* Apply current assignment of Source to all */ /* assignments of Drain. If the current ass. */ /* cannot be applied to any codomain in Drain */ /* the current assignment is added to Drain. */ Changed = FALSE; for (Scan = Drain; subst_Exist(Scan); Scan = subst_Next(Scan)) if (term_SubstituteVariable(Source->dom, Source->codomain, &(Scan->codomain))) Changed = TRUE; if (!Changed) Drain = subst_Add(Source->dom, term_Copy(Source->codomain), Drain); } return Drain; } SUBST subst_Compose(SUBST Outer, SUBST Inner) /************************************************************** INPUT: Two substitutions. RETURNS: The substitution corresponding to the composition of and . EFFECT: is destructively applied to the codomain of is destructively extended ***************************************************************/ { SUBST Scan1,Scan2,New; New = subst_Nil(); for (Scan1=Outer; subst_Exist(Scan1); Scan1 = subst_Next(Scan1)) { for (Scan2 = Inner;subst_Exist(Scan2);Scan2 = subst_Next(Scan2)) term_SubstituteVariable(subst_Dom(Scan1),subst_Cod(Scan1),&(Scan2->codomain)); if (!subst_BindVar(subst_Dom(Scan1),Inner)) New = subst_Add(subst_Dom(Scan1), term_Copy(subst_Cod(Scan1)),New); } return subst_NUnion(Inner,New); } BOOL subst_BindVar(SYMBOL Var, SUBST Subst) /************************************************************** INPUT: A variable symbol and a substitution. RETURNS: TRUE iff is contained in the domain of ***************************************************************/ { SUBST Scan; for (Scan=Subst; subst_Exist(Scan); Scan = subst_Next(Scan)) if (symbol_Equal(subst_Dom(Scan),Var)) return TRUE; return FALSE; } SUBST subst_Copy(SUBST Subst) { SUBST Copy, Result; for (Result = subst_Nil(), Copy = subst_Nil(); subst_Exist(Subst); Subst = subst_Next(Subst)) if (subst_Exist(Result)) { subst_SetNext(Copy, subst_Add(subst_Dom(Subst), term_Copy(subst_Cod(Subst)), subst_Nil())); Copy = subst_Next(Copy); } else { Result = subst_Add(subst_Dom(Subst), term_Copy(subst_Cod(Subst)), subst_Nil()); Copy = Result; } return Result; } BOOL subst_MatchTops(const CONTEXT Context, SUBST Subst) { for ( ; subst_Exist(Subst); Subst = subst_Next(Subst)) if (cont_ContextBindingTerm(Context, subst_Dom(Subst)) && term_EqualTopSymbols(cont_ContextBindingTerm(Context, subst_Dom(Subst)), subst_Cod(Subst))) return TRUE; return FALSE; } /**************************************************************/ /* ********************************************************** */ /* * * */ /* * UNIFICATION TEST * */ /* * * */ /* ********************************************************** */ /**************************************************************/ BOOL subst_Unify(CONTEXT IndexContext, SUBST Subst) /********************************************************* INPUT: RETURNS: CAUTION: 'Subst' IS ASSUMED TO BE NON-EMPTY. **********************************************************/ { while (subst_Exist(Subst)) { if (!cont_VarIsBound(IndexContext, subst_Dom(Subst))) { if (unify_OccurCheck(IndexContext, subst_Dom(Subst), IndexContext, subst_Cod(Subst))) return FALSE; else cont_CreateBinding(IndexContext, subst_Dom(Subst), IndexContext, subst_Cod(Subst)); } else if (!unify_UnifyAllOC(IndexContext, IndexContext, subst_Cod(Subst), cont_ContextBindingContext(IndexContext, subst_Dom(Subst)), cont_ContextBindingTerm(IndexContext, subst_Dom(Subst)))) return FALSE; Subst = subst_Next(Subst); } return TRUE; } BOOL subst_IsShallow(SUBST Subst) { /********************************************************** INPUT: A unifier RETURNS: TRUE, if the unifier is valid : a variable or a ground term or a function with only variables or ground terms as arguments. ***********************************************************/ SUBST SubstScan; for (SubstScan = Subst; SubstScan != subst_Nil(); SubstScan = subst_Next(SubstScan)) { TERM Codomain = subst_Cod(SubstScan); if ((!term_IsVariable(Codomain)) && (!term_IsGround(Codomain))) { LIST Scan ; for (Scan = term_ArgumentList(Codomain); Scan != list_Nil(); Scan = list_Cdr(Scan)) { if ((!term_IsVariable(list_Car(Scan)) && (!term_IsGround(list_Car(Scan))))) return FALSE; } } } return TRUE; } /**************************************************************/ /* ********************************************************** */ /* * * */ /* * GENERALIZATION TEST * */ /* * * */ /* ********************************************************** */ /**************************************************************/ BOOL subst_Match(const CONTEXT Context, SUBST Subst) /********************************************************* INPUT: RETURNS: CAUTION: 'Subst' IS ASSUMED TO BE NON-EMPTY. **********************************************************/ { while (subst_Exist(Subst)) { if (!cont_VarIsBound(Context, subst_Dom(Subst)) || !unify_Match(Context, subst_Cod(Subst), cont_ContextBindingTerm(Context, subst_Dom(Subst)))) return FALSE; Subst = subst_Next(Subst); } return TRUE; } /**************************************************************/ /* ********************************************************** */ /* * * */ /* * INSTANCE TEST * */ /* * * */ /* ********************************************************** */ /**************************************************************/ BOOL subst_MatchReverse(const CONTEXT IndexContext, SUBST Subst) /********************************************************* INPUT: RETURNS: CAUTION: 'Subst' IS ASSUMED TO BE NON-EMPTY. **********************************************************/ { while (subst_Exist(Subst)) { if (!cont_VarIsBound(IndexContext, subst_Dom(Subst))) { if (symbol_IsIndexVariable(subst_Dom(Subst))) cont_CreateBinding(IndexContext, subst_Dom(Subst), cont_InstanceContext(), subst_Cod(Subst)); else return FALSE; } else if (!unify_MatchReverse(IndexContext, subst_Cod(Subst), cont_ContextBindingContext(IndexContext, subst_Dom(Subst)), cont_ContextBindingTerm(IndexContext, subst_Dom(Subst)))) return FALSE; Subst = subst_Next(Subst); } return TRUE; } /**************************************************************/ /* ********************************************************** */ /* * * */ /* * VARIATION TEST * */ /* * * */ /* ********************************************************** */ /**************************************************************/ BOOL subst_Variation(const CONTEXT Context, SUBST Subst) /********************************************************* INPUT: RETURNS: CAUTION: 'Subst' IS ASSUMED TO BE NON-EMPTY. **********************************************************/ { while (subst_Exist(Subst)) { if (!cont_VarIsBound(Context, subst_Dom(Subst)) || !unify_Variation(Context, subst_Cod(Subst), cont_ContextBindingTerm(Context, subst_Dom(Subst)))) return FALSE; Subst = subst_Next(Subst); } return TRUE; } /**************************************************************/ /* ********************************************************** */ /* * * */ /* * COMMON GENERALIZATIONS * */ /* * * */ /* ********************************************************** */ /**************************************************************/ SUBST subst_ComGen(const CONTEXT Context, SUBST Subst, SUBST* SubstOld, SUBST* SubstNew) /********************************************************* INPUT: RETURNS: CAUTION: 'Subst' IS ASSUMED TO BE NON-EMPTY. **********************************************************/ { SUBST Result; Result = *SubstOld = *SubstNew = NULL; do { if (!cont_VarIsBound(Context, subst_Dom(Subst))) *SubstOld=subst_Add(subst_Dom(Subst), term_Copy(subst_Cod(Subst)), *SubstOld); else if (term_Equal(cont_ContextBindingTerm(Context, subst_Dom(Subst)), subst_Cod(Subst))) Result = subst_Add(subst_Dom(Subst), term_Copy(subst_Cod(Subst)), Result); else if (!symbol_Equal(term_TopSymbol(cont_ContextBindingTerm(Context, subst_Dom(Subst))), term_TopSymbol(subst_Cod(Subst)))) { *SubstOld=subst_Add(subst_Dom(Subst), term_Copy(subst_Cod(Subst)), *SubstOld); *SubstNew=subst_Add(subst_Dom(Subst), term_Copy(cont_ContextBindingTerm(Context, subst_Dom(Subst))), *SubstNew); } else Result = subst_Add(subst_Dom(Subst), unify_ComGenLinear(Context, SubstNew, cont_ContextBindingTerm(Context, subst_Dom(Subst)), SubstOld, subst_Cod(Subst)), Result); cont_CloseBinding(Context, subst_Dom(Subst)); Subst = subst_Next(Subst); } while (subst_Exist(Subst)); return Result; } /**************************************************************/ /* ********************************************************** */ /* * * */ /* * CLOSE BINDINGS * */ /* * * */ /* ********************************************************** */ /**************************************************************/ void subst_CloseVariables(const CONTEXT Context, SUBST Subst) { for (; subst_Exist(Subst); Subst = subst_Next(Subst)) cont_CloseBinding(Context, subst_Dom(Subst)); } SUBST subst_CloseOpenVariables(SUBST Result) { while (cont_LastBinding()) { if (cont_LastIsBound()) Result = subst_Add(cont_LastBindingSymbol(), term_Copy(cont_LastBindingTerm()), Result); cont_BackTrackLastBinding(); } return Result; } /**************************************************************/ /* ********************************************************** */ /* * * */ /* * EXTRACT UNIFIER * */ /* * * */ /* ********************************************************** */ /**************************************************************/ void subst_ExtractUnifier(const CONTEXT CL, SUBST* LeftSubst, const CONTEXT CR, SUBST* RightSubst) /********************************************************* INPUT: 'LeftSubst', 'RightSubst' for the unifier, renaming the codomain variables starts at 'MinimumCoVariable' excl., number of renamings are ADDED to 'Bindings'. RETURNS: Nothing. SUMMARY: Extracts the unifier into two substitutions with renamed variables in the codomain. CAUTION: DOES NOT RESET THE BINDINGS, CREATES EVEN MORE BINDINGS BECAUSE OF RENAMING. **********************************************************/ { CONTEXT Scan; *LeftSubst = subst_Nil(); *RightSubst = subst_Nil(); Scan = cont_LastBinding(); while (Scan) { if (cont_IsInContext(CL, cont_BindingSymbol(Scan), Scan)) *LeftSubst = subst_Add(cont_BindingSymbol(Scan), cont_CopyAndApplyBindings(cont_BindingContext(Scan), cont_BindingTerm(Scan)), *LeftSubst); else if (cont_IsInContext(CR, cont_BindingSymbol(Scan), Scan)) *RightSubst = subst_Add(cont_BindingSymbol(Scan), cont_CopyAndApplyBindings(cont_BindingContext(Scan), cont_BindingTerm(Scan)), *RightSubst); Scan = cont_BindingLink(Scan); } } void subst_ExtractUnifierCom(const CONTEXT Context, SUBST* Subst) /********************************************************* INPUT: 'LeftSubst', 'RightSubst' for the unifier, renaming the codomain variables starts at 'MinimumCoVariable' excl., number of renamings are ADDED to 'Bindings'. RETURNS: Nothing. SUMMARY: Extracts the unifier into two substitutions with renamed variables in the codomain. CAUTION: DOES NOT RESET THE BINDINGS, CREATES EVEN MORE BINDINGS BECAUSE OF RENAMING. **********************************************************/ { CONTEXT Scan; *Subst = subst_Nil(); Scan = cont_LastBinding(); while (Scan) { *Subst = subst_Add(cont_BindingSymbol(Scan), cont_CopyAndApplyBindingsCom(Context, cont_BindingTerm(Scan)), *Subst); Scan = cont_BindingLink(Scan); } } /**************************************************************/ /* ********************************************************** */ /* * * */ /* * EXTRACT MATCHER * */ /* * * */ /* ********************************************************** */ /**************************************************************/ SUBST subst_ExtractMatcher(void) /********************************************************* INPUT: None. RETURNS: The matcher. SUMMARY: Extracts the matcher without renaming. CAUTION: DOES NOT RESET THE BINDINGS, DOES NOT COPY THE CODOMAINS. **********************************************************/ { CONTEXT Scan; SUBST Result; for (Scan = cont_LastBinding(), Result = subst_Nil(); Scan; Scan = cont_BindingLink(Scan)) Result = subst_Add(cont_BindingSymbol(Scan), cont_BindingTerm(Scan), Result); return Result; } /**************************************************************/ /* ********************************************************** */ /* * * */ /* * OUTPUT * */ /* * * */ /* ********************************************************** */ /**************************************************************/ void subst_Print(SUBST Subst) { fputs("{ ", stdout); for (; subst_Exist(Subst); Subst = subst_Next(Subst)) { symbol_Print(subst_Dom(Subst)); if (subst_Cod(Subst)) { fputs(" -> ", stdout); term_PrintPrefix(subst_Cod(Subst)); } if (subst_Next(Subst)) fputs("; ", stdout); } fputs(" }", stdout); }