| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * 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 |
| <Outer> and <Inner>. |
| EFFECT: <Outer> is destructively applied to the codomain of <Inner> |
| <Inner> 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 <Var> is contained in the domain of <Subst> |
| ***************************************************************/ |
| { |
| 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); |
| } |
| |
