1% ----------------------------------------------------------------------
2% BEGIN LICENSE BLOCK
3% Version: CMPL 1.1
4%
5% The contents of this file are subject to the Cisco-style Mozilla Public
6% License Version 1.1 (the "License"); you may not use this file except
7% in compliance with the License.  You may obtain a copy of the License
8% at www.eclipse-clp.org/license.
9%
10% Software distributed under the License is distributed on an "AS IS"
11% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied.  See
12% the License for the specific language governing rights and limitations
13% under the License.
14%
15% The Original Code is  The ECLiPSe Constraint Logic Programming System.
16% The Initial Developer of the Original Code is  Cisco Systems, Inc.
17% Portions created by the Initial Developer are
18% Copyright (C) 1993-2006 Cisco Systems, Inc.  All Rights Reserved.
19%
20% Contributor(s): ECRC GmbH
21% Contributor(s): IC-Parc, Imperal College London
22%
23% END LICENSE BLOCK
24%
25% System:	ECLiPSe Constraint Logic Programming System
26% Version:	$Id: anti_unify.pl,v 1.2 2009/07/16 09:11:24 jschimpf Exp $
27% ----------------------------------------------------------------------
28
29%
30% ECLIPSE PROLOG LIBRARY MODULE
31%
32% IDENTIFICATION:	anti_unify.pl
33%
34% AUTHOR:		Joachim Schimpf
35%
36% CONTENTS:		anti_unify/3
37%
38% DESCRIPTION:		anti_unify(Term1, Term2, General)
39%			Computes the most specific generalization of two
40%			terms in n*log(n) time, where n is the size of
41%			the smaller term.
42%
43
44:- module(anti_unify).
45:- export anti_unify/3.
46
47:- comment(categories, ["Algorithms"]).
48:- comment(summary, "Computes the most specific generalization of two terms").
49:- comment(author, "Joachim Schimpf, ECRC Munich").
50:- comment(copyright, "Cisco Systems, Inc").
51:- comment(date, "$Date: 2009/07/16 09:11:24 $").
52
53:- comment(anti_unify/3, [
54    template:"anti_unify(Term1, Term2, General)",
55    summary:"Computes the most specific generalization of two terms in
56    N*log(N) time, where N is the size of the smaller term.",
57    eg:"
58    [eclipse 10]: anti_unify(a, b, X).
59    X = _65
60    yes.
61
62    [eclipse 11]: anti_unify(a, a, X).
63    X = a
64    yes.
65
66    [eclipse 9]: anti_unify(foo(a,b,c), foo(b,b,b), X).
67    X = foo(_115, b, _98)
68    yes.
69
70    [eclipse 8]: anti_unify(foo(a,a,a), foo(b,b,b), X).
71    X = foo(_98, _98, _98)
72    yes.
73    "]).
74
75
76anti_unify(A, B, G) :-
77	map(A, B, G, [], Map),
78	sort(0, =<, Map, SortedMap),
79	unify_duplicates(SortedMap).
80
81:- mode map(?,?,?,+,-).
82
83map(A, B, G, Map, NewMap) :-
84	atomic(A), atomic(B),
85	A = B,
86	!,
87	G = A,
88	NewMap = Map.
89map(A, B, G, Map0, Map) :-
90	nonvar(A), A=[AH|AT],
91	nonvar(B), B=[BH|BT],
92	!,
93	G = [GH|GT],
94	map(AH, BH, GH, Map0, Map1),
95	map(AT, BT, GT, Map1, Map).
96map(A, B, G, Map, NewMap) :-
97	compound(A),
98	compound(B),
99	functor(A, Name, Arity),
100	functor(B, Name, Arity),
101	!,
102	functor(G, Name, Arity),
103	map_arg(A, B, G, Map, NewMap, Arity).
104map(A, B, G, Map, [subst(A, B, G)| Map]).
105
106:- mode map_arg(?,?,?,+,-,+).
107
108map_arg(_, _, _, Map, Map, 0) :-
109	!.
110map_arg(A, B, G, Map0, NewMap, N) :-
111	arg(N, A, An),
112	arg(N, B, Bn),
113	arg(N, G, Gn),
114	map(An, Bn, Gn, Map0, Map1),
115	N1 is N-1,
116	map_arg(A, B, G, Map1, NewMap, N1).
117
118:- mode unify_duplicates(+), unify_duplicates(+,+).
119
120unify_duplicates([]).
121unify_duplicates([H|T]) :-
122	unify_duplicates(H, T).
123
124unify_duplicates(_, []).
125unify_duplicates(subst(A1, B1, G1), [H|T]) :-
126	H = subst(A2, B2, G2),
127	( A1 == A2, B1 == B2 -> G1 = G2 ; true ),
128	unify_duplicates(H, T).
129
130