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) 1994-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: notinstance.pl,v 1.2 2009/07/16 09:11:24 jschimpf Exp $ 27% ---------------------------------------------------------------------- 28 29% 30% ECLiPSe PROLOG LIBRARY MODULE 31% 32% IDENTIFICATION: notinstance.pl 33% 34% AUTHOR: Joachim Schimpf 35% 36% CONTENTS: X ~= Y (X not unifiable with Y) 37% X ~=< Y (X not instance of Y) 38% 39% DESCRIPTION: 40% 41 42:- module(notinstance). 43 44:- comment(categories, ["Algorithms"]). 45:- comment(summary, "Constraints for structural equality and subsumption"). 46:- comment(author, "Joachim Schimpf, ECRC Munich"). 47:- comment(copyright, "Cisco Systems, Inc"). 48:- comment(date, "$Date: 2009/07/16 09:11:24 $"). 49 50:- export op(700, xfx, (~=<)). 51 52:- export (~=<)/2, (~=)/2. 53 54 55:- pragma(nodebug). 56 57%----------------------------------------------------------------- 58% Non-unifiability 59% Fails if X and Y are non-unifiable, otherwise succeeds or delays. 60% Only one delayed goal, explicit wavefront list. 61% Failure is detected eagerly. 62% Success may be detected late. 63%----------------------------------------------------------------- 64 65:- comment((~=)/2, [template:"X ~= Y", 66 summary:"Constrains X and Y to be different", 67 desc:html("Fails if X and Y are non-unifiable, otherwise succeeds 68 or delays. Unlike the implementation of the same predicate in the 69 kernel, this one maintains and explicit wavefront and has only one 70 delayed goal. Failure is detected eagerly. Success may be 71 detected late.")]). 72 73X ~= Y :- 74 nu_wf([X~=Y]). 75 76 77nu_wf([X~=Y|WF0]) :- 78 nu3(X, Y, WF1, WF2), 79 ( WF2 == true -> 80 true 81 ; WF1 == WF2 -> 82 nu_wf(WF0) 83 ; 84 % delay on one undecidable pair (could be more precise) 85 WF1 = WF0, 86 WF2 = [First|_], 87 make_suspension(nu_wf(WF2), 2, Susp), 88 insert_suspension(First, Susp, bound of suspend, suspend) 89 ). 90 91 92nu3(X, Y, Xr0, Xr) :- 93 var(X), var(Y), 94 X == Y, 95 !, 96 Xr = Xr0. % continue 97nu3(X, Y, Xr0, Xr) :- 98 (var(X) ; var(Y)), 99 !, 100 Xr = [X~=Y|Xr0]. % delay 101nu3(X, Y, Xr0, Xr) :- 102 atomic(X), atomic(Y), 103 X = Y, 104 !, 105 Xr = Xr0. 106nu3(X, Y, Xr0, Xr) :- 107 compound(X), compound(Y), 108 functor(X, F, A), 109 functor(Y, F, A), 110 !, 111 nu3_arg(X, Y, Xr0, Xr, A). 112nu3(_X, _Y, _Xr0, true). % succeed 113 114nu3_arg(_X, _Y, Xr0, Xr, 0) :- !, Xr0 = Xr. 115nu3_arg(X, Y, Xr0, Xr, N) :- 116 arg(N, X, Xarg), 117 arg(N, Y, Yarg), 118 nu3(Xarg, Yarg, Xr0, Xr1), 119 ( Xr1 == true -> 120 Xr = true 121 ; 122 N1 is N-1, 123 nu3_arg(X, Y, Xr1, Xr, N1) 124 ). 125 126 127%----------------------------------------------------------------- 128% X ~=< Y Constrain X not to be an instance of Y. 129% 130% We assume: 131% - no shared variables between X and Y 132% - X may get more instantiated, but not Y 133% Failure is detected eagerly. 134% Success may be detected late. 135% The binding table is done very naively currently. 136%----------------------------------------------------------------- 137 138:- comment((~=<)/2, [template:"X ~=< Y", 139 summary:"Constrain X not to be an instance of Y", 140 desc:html("We assume: 141 <UL> 142 <LI> no shared variables between X and Y 143 <LI> X may get more instantiated, but not Y 144 </UL> 145 Failure is detected eagerly. Success may be detected late.")]). 146 147X ~=< Y :- 148 ni_wf(X ~=< Y, [], _V). 149 150ni_wf(X ~=< Y, WF0, V) :- 151 !, 152 ni(X, Y, V, WF1, WF2), 153 ( WF2 == true -> 154 true % definitely not an instance 155 ; WF1 == WF2 -> 156 WF0 = [First|WF3], 157 ni_wf(First, WF3, V) % continue along the wavefront 158 ; 159 % delay on one undecidable pair 160 WF1 = WF0, % prepend 161 WF2 = [First|WF3], 162 make_suspension(ni_wf(First, WF3, V), 2, Susp), 163 ( First = (Lhs ~=< _) -> 164 insert_suspension(Lhs, Susp, constrained of suspend, suspend) 165 ; % First = (_ ~= _) 166 insert_suspension(First, Susp, bound of suspend, suspend) 167 ) 168 ). 169ni_wf(X ~= Y, WF0, V) :- 170 nu3(X, Y, WF1, WF2), 171 ( WF2 == true -> 172 true 173 ; WF1 == WF2 -> 174 WF0 = [First|WF3], 175 ni_wf(First, WF3, V) 176 ; 177 % delay on one undecidable pair 178 WF1 = WF0, 179 WF2 = [First|WF3], 180 make_suspension(ni_wf(First, WF3, V), 2, Susp), 181 insert_suspension(First, Susp, bound of suspend, suspend) 182 ). 183 184 185ni(X, Y, _V, T0, T) :- 186 var(X), nonvar(Y), 187 !, 188 T = [X~=<Y|T0]. 189ni(X, Y, _V, T0, T) :- % nonvar(X);var(Y) 190 meta(Y), 191 \+ instance(X,Y), 192 !, 193 ( atomic(X) -> T = true ; T = [X~=<Y|T0] ). 194ni(X, Y, V, T0, T) :- % nonvar(X);var(Y) 195 var(Y), !, % free(Y);meta(Y) 196 lookup(Y, V, Map), 197 ( var(Map) -> 198 Map = map(X), % remember the mapping Y=X 199 T0 = T % one step closer to failure ... 200 ; 201 Map = map(Xold), 202 nu3(Xold, X, T0, T) % add inequality constraint 203 ). 204ni(X, Y, _V, T0, T) :- 205 atomic(X), % atomic(Y), 206 X = Y, 207 !, 208 T0 = T. % one step closer to failure ... 209ni(X, Y, V, T0, T) :- 210 compound(X), compound(Y), 211 functor(X, F, A), 212 functor(Y, F, A), 213 !, 214 ni_args(X, Y, V, T0, T, A). 215ni(_X, _Y, _V, _T0, true). % not instances: success 216 217ni_args(_X, _Y, _V, T0, T, 0) :- !, T0 = T. 218ni_args(X, Y, V, T0, T, N) :- 219 arg(N, X, Xarg), 220 arg(N, Y, Yarg), 221 ni(Xarg, Yarg, V, T0, T1), 222 ( T1 == true -> 223 T = true 224 ; 225 N1 is N-1, 226 ni_args(X, Y, V, T1, T, N1) 227 ). 228 229 230lookup(Key, List, Entry) :- 231 var(List), !, 232 List = [Key-Entry|_]. 233lookup(Key, [Key0-Entry0|Tail], Entry) :- 234 Key == Key0 -> 235 Entry = Entry0 236 ; 237 lookup(Key, Tail, Entry). 238 239