mirror of
https://github.com/Mercury-Language/mercury.git
synced 2026-04-15 01:13:30 +00:00
276 lines
10 KiB
Mathematica
276 lines
10 KiB
Mathematica
%---------------------------------------------------------------------------%
|
|
% vim: ts=4 sw=4 et ft=mercury
|
|
%---------------------------------------------------------------------------%
|
|
% Copyright (C) 1993-2000,2003-2009,2011-2012 The University of Melbourne.
|
|
% Copyright (C) 2014-2022, 2025-2026 The Mercury team.
|
|
% This file is distributed under the terms specified in COPYING.LIB.
|
|
%---------------------------------------------------------------------------%
|
|
%
|
|
% File: term_unify.m.
|
|
% Main author: fjh.
|
|
% Stability: high.
|
|
%
|
|
% This file provides predicates to unify terms.
|
|
%
|
|
%---------------------------------------------------------------------------%
|
|
%---------------------------------------------------------------------------%
|
|
|
|
:- module term_unify.
|
|
:- interface.
|
|
|
|
:- import_module list.
|
|
:- import_module term.
|
|
|
|
%---------------------------------------------------------------------------%
|
|
%
|
|
% Predicates to unify terms.
|
|
%
|
|
|
|
% unify_terms(TermA, TermB, !Subst):
|
|
%
|
|
% Unify (with occur check) two terms with respect to the current
|
|
% substitution, and update that substitution as necessary.
|
|
%
|
|
:- pred unify_terms(term(T)::in, term(T)::in,
|
|
substitution(T)::in, substitution(T)::out) is semidet.
|
|
|
|
% unify_term_lists(TermsA, TermsB, !Subst):
|
|
%
|
|
% Unify (with occur check) two lists of terms with respect to the current
|
|
% substitution, and update that substitution as necessary.
|
|
% Fail if the lists are not of equal length.
|
|
%
|
|
:- pred unify_term_lists(list(term(T))::in, list(term(T))::in,
|
|
substitution(T)::in, substitution(T)::out) is semidet.
|
|
|
|
% unify_terms_dont_bind(TermA, TermB, DontBindVars, !Subst):
|
|
%
|
|
% Do the same job as unify_terms(TermA, TermB, !Subst), but fail
|
|
% if any of the variables in DontBindVars would become bound
|
|
% by the unification.
|
|
%
|
|
:- pred unify_terms_dont_bind(term(T)::in, term(T)::in,
|
|
list(var(T))::in, substitution(T)::in, substitution(T)::out) is semidet.
|
|
|
|
% unify_term_lists_dont_bind(TermsA, TermsB, DontBindVars, !Subst):
|
|
%
|
|
% Do the same job as unify_term_lists(TermsA, TermsB, !Subst), but fail
|
|
% if any of the variables in DontBindVars would become bound
|
|
% by the unification.
|
|
%
|
|
:- pred unify_term_lists_dont_bind(list(term(T))::in, list(term(T))::in,
|
|
list(var(T))::in, substitution(T)::in, substitution(T)::out) is semidet.
|
|
|
|
%---------------------------------------------------------------------------%
|
|
%
|
|
% Predicates to test subsumption.
|
|
%
|
|
|
|
% first_term_list_subsumes_second(TermsA, TermsB, Subst):
|
|
%
|
|
% Succeeds if-and-only-if the list TermsA subsumes (is more general than)
|
|
% TermsB, producing a substitution which, when applied to TermsA,
|
|
% will give TermsB.
|
|
%
|
|
:- pred first_term_list_subsumes_second(list(term(T))::in, list(term(T))::in,
|
|
substitution(T)::out) is semidet.
|
|
|
|
%---------------------------------------------------------------------------%
|
|
%---------------------------------------------------------------------------%
|
|
|
|
:- implementation.
|
|
|
|
:- import_module map.
|
|
:- import_module term_context.
|
|
:- import_module term_subst.
|
|
:- import_module term_vars.
|
|
|
|
%---------------------------------------------------------------------------%
|
|
|
|
unify_terms(TermX, TermY, !Subst) :-
|
|
(
|
|
TermX = variable(X, _),
|
|
TermY = variable(Y, _),
|
|
( if map.search(!.Subst, X, TermBoundToX) then
|
|
( if map.search(!.Subst, Y, TermBoundToY) then
|
|
% Both X and Y already have bindings, so just unify
|
|
% the terms they are bound to.
|
|
unify_terms(TermBoundToX, TermBoundToY, !Subst)
|
|
else
|
|
% X is bound, but Y isn't.
|
|
term_subst.apply_rec_substitution_in_term(!.Subst,
|
|
TermBoundToX, SubstTermBoundToX),
|
|
( if SubstTermBoundToX = variable(Y, _) then
|
|
true
|
|
else
|
|
not var_occurs_in_subst_term(Y, !.Subst,
|
|
SubstTermBoundToX),
|
|
map.det_insert(Y, SubstTermBoundToX, !Subst)
|
|
)
|
|
)
|
|
else
|
|
( if map.search(!.Subst, Y, TermBoundToY) then
|
|
% Y is bound, but X isn't.
|
|
term_subst.apply_rec_substitution_in_term(!.Subst,
|
|
TermBoundToY, SubstTermBoundToY),
|
|
( if SubstTermBoundToY = variable(X, _) then
|
|
true
|
|
else
|
|
not var_occurs_in_subst_term(X, !.Subst,
|
|
SubstTermBoundToY),
|
|
map.det_insert(X, SubstTermBoundToY, !Subst)
|
|
)
|
|
else
|
|
% Neither X nor Y are bound, so bind one to the other.
|
|
( if X = Y then
|
|
true
|
|
else
|
|
map.det_insert(X, TermY, !Subst)
|
|
)
|
|
)
|
|
)
|
|
;
|
|
TermX = variable(X, _),
|
|
TermY = functor(_, ArgTermsY, _),
|
|
( if map.search(!.Subst, X, TermBoundToX) then
|
|
unify_terms(TermBoundToX, TermY, !Subst)
|
|
else
|
|
not var_occurs_in_subst_terms(X, !.Subst, ArgTermsY),
|
|
map.det_insert(X, TermY, !Subst)
|
|
)
|
|
;
|
|
TermX = functor(_, ArgTermsX, _),
|
|
TermY = variable(Y, _),
|
|
( if map.search(!.Subst, Y, TermBoundToY) then
|
|
unify_terms(TermX, TermBoundToY, !Subst)
|
|
else
|
|
not var_occurs_in_subst_terms(Y, !.Subst, ArgTermsX),
|
|
map.det_insert(Y, TermX, !Subst)
|
|
)
|
|
;
|
|
TermX = functor(NameX, ArgTermsX, _),
|
|
TermY = functor(NameY, ArgTermsY, _),
|
|
NameX = NameY,
|
|
% We could pretest whether the lengths of the argument lists match.
|
|
unify_term_lists(ArgTermsX, ArgTermsY, !Subst)
|
|
).
|
|
|
|
unify_term_lists([], [], !Subst).
|
|
unify_term_lists([TermX | TermXs], [TermY | TermYs], !Subst) :-
|
|
unify_terms(TermX, TermY, !Subst),
|
|
unify_term_lists(TermXs, TermYs, !Subst).
|
|
|
|
%---------------------------------------------------------------------------%
|
|
|
|
unify_terms_dont_bind(TermX, TermY, DontBindVars, !Subst) :-
|
|
(
|
|
TermX = variable(X, _),
|
|
TermY = variable(Y, _),
|
|
( if list.member(Y, DontBindVars) then
|
|
unify_terms_bound_var(X, Y, DontBindVars, !Subst)
|
|
else if list.member(X, DontBindVars) then
|
|
unify_terms_bound_var(Y, X, DontBindVars, !Subst)
|
|
else if map.search(!.Subst, X, TermBoundToX) then
|
|
( if map.search(!.Subst, Y, TermBoundToY) then
|
|
% Both X and Y already have bindings, so just unify
|
|
% the terms they are bound to.
|
|
unify_terms_dont_bind(TermBoundToX, TermBoundToY, DontBindVars,
|
|
!Subst)
|
|
else
|
|
% X is bound, but Y isn't.
|
|
term_subst.apply_rec_substitution_in_term(!.Subst,
|
|
TermBoundToX, SubstTermBoundToX),
|
|
( if SubstTermBoundToX = variable(Y, _) then
|
|
true
|
|
else
|
|
not var_occurs_in_subst_term(Y, !.Subst,
|
|
SubstTermBoundToX),
|
|
map.det_insert(Y, SubstTermBoundToX, !Subst)
|
|
)
|
|
)
|
|
else
|
|
( if map.search(!.Subst, Y, TermBoundToY) then
|
|
% Y is bound, but X isn't.
|
|
term_subst.apply_rec_substitution_in_term(!.Subst,
|
|
TermBoundToY, SubstTermBoundToY),
|
|
( if SubstTermBoundToY = variable(X, _) then
|
|
true
|
|
else
|
|
not var_occurs_in_subst_term(X, !.Subst,
|
|
SubstTermBoundToY),
|
|
map.det_insert(X, SubstTermBoundToY, !Subst)
|
|
)
|
|
else
|
|
% Neither X nor Y are bound, so bind one to the other.
|
|
( if X = Y then
|
|
true
|
|
else
|
|
map.det_insert(X, TermY, !Subst)
|
|
)
|
|
)
|
|
)
|
|
;
|
|
TermX = variable(X, _),
|
|
TermY = functor(_, ArgTermsY, _),
|
|
( if map.search(!.Subst, X, TermBoundToX) then
|
|
unify_terms_dont_bind(TermBoundToX, TermY, DontBindVars, !Subst)
|
|
else
|
|
not var_occurs_in_subst_terms(X, !.Subst, ArgTermsY),
|
|
not list.member(X, DontBindVars),
|
|
map.det_insert(X, TermY, !Subst)
|
|
)
|
|
;
|
|
TermX = functor(_, ArgTermsX, _),
|
|
TermY = variable(Y, _),
|
|
( if map.search(!.Subst, Y, TermBoundToY) then
|
|
unify_terms_dont_bind(TermX, TermBoundToY, DontBindVars, !Subst)
|
|
else
|
|
not var_occurs_in_subst_terms(Y, !.Subst, ArgTermsX),
|
|
not list.member(Y, DontBindVars),
|
|
map.det_insert(Y, TermX, !Subst)
|
|
)
|
|
;
|
|
TermX = functor(NameX, ArgTermsX, _CX),
|
|
TermY = functor(NameY, ArgTermsY, _CY),
|
|
NameX = NameY,
|
|
list.length(ArgTermsX, ArityX),
|
|
list.length(ArgTermsY, ArityY),
|
|
ArityX = ArityY,
|
|
unify_term_lists_dont_bind(ArgTermsX, ArgTermsY, DontBindVars, !Subst)
|
|
).
|
|
|
|
unify_term_lists_dont_bind([], [], _, !Subst).
|
|
unify_term_lists_dont_bind([TermX | TermXs], [TermY | TermYs],
|
|
DontBindVars, !Subst) :-
|
|
unify_terms_dont_bind(TermX, TermY, DontBindVars, !Subst),
|
|
unify_term_lists_dont_bind(TermXs, TermYs, DontBindVars, !Subst).
|
|
|
|
:- pred unify_terms_bound_var(var(T)::in, var(T)::in, list(var(T))::in,
|
|
substitution(T)::in, substitution(T)::out) is semidet.
|
|
|
|
unify_terms_bound_var(X, BoundY, DontBindVars, !Subst) :-
|
|
( if map.search(!.Subst, X, TermBoundToX) then
|
|
TermBoundToX = variable(NewX, _),
|
|
unify_terms_bound_var(NewX, BoundY, DontBindVars, !Subst)
|
|
else
|
|
( if X = BoundY then
|
|
true
|
|
else
|
|
not list.member(X, DontBindVars),
|
|
map.det_insert(X, variable(BoundY, dummy_context), !Subst)
|
|
)
|
|
).
|
|
|
|
%---------------------------------------------------------------------------%
|
|
|
|
first_term_list_subsumes_second(Terms1, Terms2, Subst) :-
|
|
% Terms1 subsumes Terms2 if-and-only-if Terms1 can be unified with Terms2
|
|
% without binding any of the variables in Terms2.
|
|
vars_in_terms(Terms2, Terms2Vars),
|
|
map.init(Subst0),
|
|
unify_term_lists_dont_bind(Terms1, Terms2, Terms2Vars, Subst0, Subst).
|
|
|
|
%---------------------------------------------------------------------------%
|
|
:- end_module term_unify.
|
|
%---------------------------------------------------------------------------%
|