001 package toolbus;
002
003 import java.util.ArrayList;
004 import java.util.Iterator;
005 import java.util.List;
006 import toolbus.environment.Binding;
007 import toolbus.environment.Environment;
008 import toolbus.exceptions.ToolBusException;
009 import toolbus.exceptions.ToolBusInternalError;
010 import aterm.AFun;
011 import aterm.ATerm;
012 import aterm.ATermAppl;
013 import aterm.ATermList;
014 import aterm.ATermPlaceholder;
015 import aterm.pure.PureFactory;
016
017 public class TBTermFactory extends PureFactory{
018 /**
019 * A term of type VAR
020 */
021 public static final int VAR = 80;
022
023 private final AFun fun_TBTermVar;
024
025 public final ATerm True;
026 public final ATerm False;
027
028 public final ATerm BoolType;
029 public final ATerm IntType;
030 public final ATerm RealType;
031 public final ATerm StrType;
032 public final ATerm TermType;
033 public final ATerm ListType;
034 public final ATerm BlobType;
035
036 public final ATerm Undefined;
037
038 public final ATerm BoolPlaceholder;
039 public final ATerm IntPlaceholder;
040 public final ATerm RealPlaceholder;
041 public final ATerm StrPlaceholder;
042 public final ATerm TermPlaceholder;
043 public final ATerm ListPlaceholder;
044 public final ATerm BlobPlaceholder;
045
046 public final ATermList EmptyList;
047
048 protected TBTermFactory(){
049 super();
050
051 fun_TBTermVar = makeAFun("var", 3, false);
052
053 True = make("true");
054 False = make("false");
055
056 BoolType = make("bool");
057 IntType = make("int");
058 RealType = make("real");
059 StrType = make("str");
060 TermType = make("term");
061 ListType = make("list");
062 BlobType = make("blob");
063
064 Undefined = make("undefined");
065
066 BoolPlaceholder = makePlaceholder(BoolType);
067 IntPlaceholder = makePlaceholder(IntType);
068 RealPlaceholder = makePlaceholder(RealType);
069 StrPlaceholder = makePlaceholder(StrType);
070 TermPlaceholder = makePlaceholder(TermType);
071 ListPlaceholder = makePlaceholder(ListType);
072 BlobPlaceholder = makePlaceholder(BlobType);
073
074 EmptyList = makeList();
075
076 Functions.init(this);
077 }
078
079 private static class InstanceKeeper{
080 public final static TBTermFactory instance = new TBTermFactory();
081 }
082
083 public static TBTermFactory getInstance(){
084 return InstanceKeeper.instance;
085 }
086
087 public String statistics(){
088 return toString();
089 }
090
091 public TBTermVar makeTBTermVar(String name, ATerm type, ATerm isResult, ATermList annos){
092 ATerm[] args = new ATerm[3];
093 args[0] = type;
094 args[1] = make(name);
095 args[2] = isResult;
096 return (TBTermVar) build(new TBTermVar(this, annos, fun_TBTermVar, args));
097 }
098
099 public TBTermVar makeTBTermVar(String name, ATerm type){
100 return makeTBTermVar(name, type, False, EmptyList);
101 }
102
103 public TBTermVar makeTBTermVar(String name, ATerm type, ATerm isResVar){
104 return makeTBTermVar(name, type, isResVar, EmptyList);
105 }
106
107 public TBTermVar makeTBTermResVar(String name, ATerm type){
108 return makeTBTermVar(name, type, True, EmptyList);
109 }
110
111 public TBTermVar mkVar(ATerm name, String processName, ATerm type){
112 return makeTBTermVar(name.toString() + "$" + processName, type);
113 }
114
115 public TBTermVar mkResVar(ATerm name, String processName, ATerm type){
116 return makeTBTermResVar(name.toString() + "$" + processName, type);
117 }
118
119 /*****/
120
121 public boolean isTrue(ATerm t){
122 return t == True;
123 }
124
125 public boolean isFalse(ATerm t){
126 return t == False;
127 }
128
129 public boolean isBoolean(ATerm t){
130 return t == True || t == False;
131 }
132
133 public boolean isInt(ATerm t){
134 return t.getType() == ATerm.INT;
135 }
136
137 public boolean isStr(ATerm t){
138 if(isAppl(t)){
139 return (((ATermAppl) t).isQuoted()) && ((ATermAppl) t).getArity() == 0;
140 }
141 return false;
142 }
143
144 public boolean isReal(ATerm t){
145 return (t.getType() == ATerm.REAL);
146 }
147
148 public boolean isAppl(ATerm t){
149 return t.getType() == ATerm.APPL;
150 }
151
152 public boolean isList(ATerm t){
153 return t.getType() == ATerm.LIST;
154 }
155
156 public boolean isBlob(ATerm t){
157 return t.getType() == ATerm.BLOB;
158 }
159
160 public ATerm getArgs(ATerm t){
161 return ((ATermAppl) t).getArguments();
162 }
163
164 public int size(ATerm l){
165 return ((ATermList) l).getLength();
166 }
167
168 public ATerm first(ATerm l){
169 ATermList lst = (ATermList) l;
170 if(!lst.isEmpty()){
171 return lst.elementAt(0);
172 }
173 return Undefined;
174 // throw new ToolBusError("function first cannot be applied to empty list");
175 }
176
177 public ATerm next(ATerm l){
178 ATermList lst = (ATermList) l;
179 if(lst.isEmpty()){
180 return lst;
181 }
182 return lst.getNext();
183 }
184
185 public boolean member(ATerm e, ATerm l){
186 ATermList lst = (ATermList) l;
187 int length = lst.getLength();
188 for(int i = 0; i < length; i++){
189 if(e.isEqual(lst.elementAt(i))) return true;
190 }
191 return false;
192 }
193
194 public boolean subset(ATerm l1, ATerm l2){
195 ATerm terml2 = l2;
196
197 ATermList lst1 = (ATermList) l1;
198 int length1 = lst1.getLength();
199 for(int i = 0; i < length1; i++){
200 ATerm e = lst1.elementAt(i);
201 if(!member(e, terml2)){
202 return false;
203 }
204 terml2 = delete(terml2, e);
205 }
206 return true;
207 }
208
209 public ATermList delete(ATerm l, ATerm e){
210 ATermList lst = (ATermList) l;
211 ATermList res = EmptyList;
212 boolean found = false;
213 for(int i = lst.getLength() - 1; i >= 0; i--){
214 ATerm e2 = lst.elementAt(i);
215 if(e2.isEqual(e) && !found)
216 found = true;
217 else res = makeList(e2, res);
218 }
219 return res;
220 }
221
222 public ATerm diff(ATerm l1, ATerm l2){
223 ATermList lst1 = (ATermList) l1;
224 ATermList res = EmptyList;
225 for(int i = lst1.getLength() - 1; i >= 0; i--){
226 ATerm e = lst1.elementAt(i);
227 if(!member(e, l2)) res = makeList(e, res);
228 }
229 return res;
230 }
231
232 public ATerm inter(ATerm l1, ATerm l2){
233 ATermList lst1 = (ATermList) l1;
234 ATermList res = EmptyList;
235 for(int i = lst1.getLength() - 1; i >= 0; i--){
236 ATerm e = lst1.elementAt(i);
237 if(member(e, l2)) res = makeList(e, res);
238 }
239 // System.err.println("inter(" + l1 + ", " + l2 + ") ==> " + res);
240 return res;
241 }
242
243 public ATerm join(ATerm l1, ATerm l2){
244 // if(l1 == null)
245 // return l2;
246 // if(l2 == null)
247 // return l1;
248 ATermList lst1 = isList(l1) ? (ATermList) l1 : makeList(l1);
249 ATermList res = isList(l2) ? (ATermList) l2 : makeList(l2);
250 for(int i = lst1.getLength() - 1; i >= 0; i--){
251 ATerm e = lst1.elementAt(i);
252 res = makeList(e, res);
253 }
254 // System.err.println("join(" + l1 + ", " + l2 + ") ==> " + res);
255 return res;
256 }
257
258 public ATerm concat(ATerm s1, ATerm s2){
259 String str1 = isStr(s1) ? ((ATermAppl) s1).getName() : s1.toString();
260 String str2 = isStr(s1) ? ((ATermAppl) s2).getName() : s2.toString();
261 String res = str1 + str2;
262 AFun af = makeAFun(res, 0, true);
263 return makeAppl(af);
264 }
265
266 public ATerm index(ATerm l, int i){
267 ATerm res;
268 try{
269 res = ((ATermList) l).elementAt(i - 1);
270 }catch(IllegalArgumentException iaex){
271 throw new IllegalArgumentException("An index out of bounds exception occured while retrieving the term at index: "+i+", from the following list: "+l);
272 }
273 return res;
274 }
275
276 public ATerm replace(ATerm l, int n, ATerm e){
277 ATermList lst = (ATermList) l;
278 ATermList res = EmptyList;
279 for(int i = lst.getLength() - 1; i >= 0; i--){
280 ATerm elem = (i == n - 1) ? e : lst.elementAt(i);
281 res = makeList(elem, res);
282 }
283 return res;
284 }
285
286 public ATerm put(ATerm l, ATerm k, ATerm v){
287 ATermList pair = makeList(k, makeList(v));
288 return makeList(pair, (ATermList) l);
289 }
290
291 public ATerm get(ATerm l, ATerm k){
292 ATermList lst = (ATermList) l;
293 for(ATermList pair = (ATermList) lst.getFirst(); !lst.isEmpty(); lst = lst.getNext()){
294 if(k.isEqual(pair.getFirst())) return pair.getLast();
295 }
296 return Undefined;
297 }
298
299 public boolean isVar(ATerm t){
300 return t.getType() == VAR && !((TBTermVar) t).isResultVar();
301 }
302
303 public boolean isResultVar(ATerm t){
304 return t.getType() == VAR && ((TBTermVar) t).isResultVar();
305 }
306
307 public boolean isAnyVar(ATerm t){
308 return t.getType() == VAR;
309 }
310
311 public TBTermVar replaceAssignableVar(TBTermVar v, Environment env) throws ToolBusException{
312 // System.err.println("replaceAssignableVar: " + v + "; " + env);
313
314 Binding b = env.getBinding(v);
315 // System.err.println("Binding = " + b.var + ";" + b.val);
316 if(b == null || (b.getVal() == Undefined)){
317 return v;
318 }
319 if(b.isFormal() && isResultVar(b.getVal())){
320 return replaceAssignableVar((TBTermVar) b.getVal(), env);
321 }
322 return b.getVar();
323 }
324
325 /**
326 * Replace the formals in ATerm t by their values using Environment env.
327 *
328 * @param t
329 * Aterm containing formals
330 * @param env
331 * environment to be used.
332 */
333 public ATerm replaceFormals(ATerm t, Environment env) throws ToolBusException{
334 if(env.size() == 0) return t;
335
336 switch(t.getType()){
337 case ATerm.BLOB:
338 case ATerm.INT:
339 case ATerm.PLACEHOLDER:
340 case ATerm.REAL:
341 return t;
342
343 case VAR:
344 return env.replaceFormal((TBTermVar) t);
345
346 case ATerm.APPL:
347 ATermAppl apt = (ATermAppl) t;
348
349 AFun afun = apt.getAFun();
350 ATerm args[] = apt.getArgumentArray();
351 ATerm cargs[] = new ATerm[args.length];
352 int nargs = args.length;
353 if(nargs == 0) return t;
354 for(int i = 0; i < nargs; i++){
355 cargs[i] = replaceFormals(args[i], env);
356 }
357 return makeAppl(afun, cargs);
358
359 case ATerm.LIST:
360 ATermList lst = EmptyList;
361 ATermList tlst = (ATermList) t;
362 for(int i = tlst.getLength() - 1; i >= 0; i--){
363 lst = lst.insert(replaceFormals(tlst.elementAt(i), env));
364 }
365 return lst;
366 }
367 throw new ToolBusInternalError("illegal ATerm in replaceFormals: " + t);
368 }
369
370 /**
371 * Transform a term into a pattern that can be used by tool interfaces.
372 */
373 public ATerm makePattern(ATerm t){
374 if(t == Undefined) return t;
375
376 switch(t.getType()){
377 case ATerm.BLOB:
378 return BlobPlaceholder;
379
380 case ATerm.INT:
381 return IntPlaceholder;
382
383 case ATerm.PLACEHOLDER:
384 return t;
385
386 case ATerm.REAL:
387 return RealPlaceholder;
388
389 case VAR:
390 TBTermVar var = (TBTermVar) t;
391 ATerm type = var.getVarType();
392 return makePlaceholder(type);
393
394 case ATerm.APPL:
395 ATermAppl apt = (ATermAppl) t;
396 if(isBoolean(apt)){
397 return BoolPlaceholder;
398 }
399 AFun fun = apt.getAFun();
400 ATerm args[] = apt.getArgumentArray();
401 int nargs = args.length;
402 if(nargs == 0){
403 if(fun.isQuoted()){
404 return StrPlaceholder;
405 }
406 return apt;
407 }
408
409 ATerm vargs[] = new ATerm[nargs];
410 for(int i = 0; i < nargs; i++){
411 vargs[i] = makePattern(args[i]);
412 }
413 return makeAppl(fun, vargs);
414
415 case ATerm.LIST:
416 ATermList lst = EmptyList;
417 ATermList tlst = (ATermList) t;
418 for(int i = tlst.getLength() - 1; i >= 0; i--){
419 lst = lst.insert(makePattern(tlst.elementAt(i)));
420 }
421 return lst;
422
423 }
424 throw new ToolBusInternalError("illegal ATerm in getType: " + t);
425 }
426
427 // TODO Optimize
428 /**
429 * Replace all variables in an ATerm by their value.
430 */
431 public ATerm substitute(ATerm t, Environment env){
432 if(t == Undefined) return t;
433
434 switch(t.getType()){
435 case ATerm.BLOB:
436 case ATerm.INT:
437 case ATerm.PLACEHOLDER:
438 case ATerm.REAL:
439 return t;
440
441 case VAR:
442 TBTermVar var = (TBTermVar) t;
443 if(var.isResultVar()) return var;
444
445 return env.getValue(var);
446
447 case ATerm.APPL:
448 ATermAppl apt = (ATermAppl) t;
449 if(apt.getArity() == 0) return t;
450
451 AFun afun = apt.getAFun();
452 ATerm args[] = apt.getArgumentArray();
453 ATermList applAnnos = apt.getAnnotations();
454
455 int nargs = args.length;
456 ATerm vargs[] = new ATerm[nargs];
457 for(int i = 0; i < nargs; i++){
458 vargs[i] = substitute(args[i], env);
459 }
460 return makeAppl(afun, vargs, applAnnos);
461
462 case ATerm.LIST:
463 ATermList tlst = (ATermList) t;
464 ATermList listAnnos = t.getAnnotations();
465
466 if(tlst == EmptyList) return t;
467
468 int len = tlst.getLength();
469 ATerm[] listContent = new ATerm[len];
470 for(int i = len - 1; i >= 0; i--){
471 listContent[i] = tlst.getFirst();
472 tlst = tlst.getNext();
473 }
474
475 ATermList lst = EmptyList;
476 for(int i = 0; i < len; i++){
477 lst = lst.insert((substitute(listContent[i], env)));
478 }
479
480 lst = (ATermList) lst.setAnnotations(listAnnos);
481
482 return lst;
483 }
484 throw new ToolBusInternalError("Illegal ATerm in substitute: " + t);
485 }
486
487 // TODO Optimize
488 /**
489 * Replaces all variables in an ATerm by their value. If a variable result variable is present
490 * the full substitute can not be completed and null will be returned instead.
491 * @param t
492 * The term in which variables need to be substituted.
493 * @param env
494 * The environment from which the variable values can be retrieved.
495 * @return A complete ATerm tree that doesn't contain any variables; null if the substitute could
496 * not be completed.
497 */
498 public ATerm fullSubstitute(ATerm t, Environment env){
499 if(t == Undefined) return t;
500
501 switch(t.getType()){
502 case ATerm.BLOB:
503 case ATerm.INT:
504 case ATerm.PLACEHOLDER:
505 case ATerm.REAL:
506 return t;
507
508 case VAR:
509 TBTermVar var = (TBTermVar) t;
510 if(var.isResultVar()) return null;
511
512 return env.getValue(var);
513
514 case ATerm.APPL:
515 ATermAppl apt = (ATermAppl) t;
516 if(apt.getArity() == 0) return t;
517
518 AFun afun = apt.getAFun();
519 ATerm args[] = apt.getArgumentArray();
520 ATermList applAnnos = apt.getAnnotations();
521
522 int nargs = args.length;
523 ATerm vargs[] = new ATerm[nargs];
524 for(int i = 0; i < nargs; i++){
525 ATerm result = fullSubstitute(args[i], env);
526 if(result == null) return null;
527 vargs[i] = result;
528 }
529 return makeAppl(afun, vargs, applAnnos);
530
531 case ATerm.LIST:
532 ATermList tlst = (ATermList) t;
533 ATermList listAnnos = t.getAnnotations();
534
535 if(tlst == EmptyList) return t;
536
537 int len = tlst.getLength();
538 ATerm[] listContent = new ATerm[len];
539 for(int i = len - 1; i >= 0; i--){
540 listContent[i] = tlst.getFirst();
541 tlst = tlst.getNext();
542 }
543
544 ATermList lst = EmptyList;
545 for(int i = 0; i < len; i++){
546 ATerm result = fullSubstitute(listContent[i], env);
547 if(result == null) return null;
548 lst = lst.insert(result);
549 }
550
551 lst = (ATermList) lst.setAnnotations(listAnnos);
552
553 return lst;
554 }
555 throw new ToolBusInternalError("Illegal ATerm in substitute: " + t);
556 }
557
558 public boolean match(ATerm left, Environment leftEnv, ATerm right, Environment rightEnv){
559 List<Binding> leftDeltaEnv = new ArrayList<Binding>();
560 List<Binding> rightDeltaEnv = new ArrayList<Binding>();
561
562 boolean matches = performMatch(left, leftEnv, leftDeltaEnv, right, rightEnv, rightDeltaEnv);
563 if(matches){
564 Iterator<Binding> leftDeltaEnvIterator = leftDeltaEnv.iterator();
565 while(leftDeltaEnvIterator.hasNext()){
566 Binding deltaBinding = leftDeltaEnvIterator.next();
567 leftEnv.assignVar(deltaBinding.getVar(), deltaBinding.getVal());
568 }
569
570 Iterator<Binding> rightDeltaEnvIterator = rightDeltaEnv.iterator();
571 while(rightDeltaEnvIterator.hasNext()){
572 Binding deltaBinding = rightDeltaEnvIterator.next();
573 rightEnv.assignVar(deltaBinding.getVar(), deltaBinding.getVal());
574 }
575 }
576
577 return matches;
578 }
579
580 public boolean matchPatternToValue(ATerm left, Environment leftEnv, ATerm right){
581 List<Binding> leftDeltaEnv = new ArrayList<Binding>();
582
583 boolean matches = performPatternMatch(left, leftEnv, right, leftDeltaEnv);
584 if(matches){
585 Iterator<Binding> deltaEnvIterator = leftDeltaEnv.iterator();
586 while(deltaEnvIterator.hasNext()){
587 Binding deltaBinding = deltaEnvIterator.next();
588 leftEnv.assignVar(deltaBinding.getVar(), deltaBinding.getVal());
589 }
590 }
591
592 return matches;
593 }
594
595 public boolean patternMatchesToValue(ATerm pattern, Environment patternEnv, ATerm value){
596 List<Binding> deltaEnv = new ArrayList<Binding>();
597
598 return performPatternMatch(pattern, patternEnv, value, deltaEnv);
599 }
600
601 private boolean performPatternMatch(ATerm pattern, Environment patternEnv, ATerm value, List<Binding> deltaEnv){
602 switch(pattern.getType()){
603 case VAR:
604 TBTermVar pVar = (TBTermVar) pattern;
605 if(pVar.isResultVar()){
606 if(Functions.compatibleTypes(pVar.getVarType(), value)){
607 Binding deltaBinding = new Binding(pVar, value);
608 deltaEnv.add(deltaBinding);
609 return true;
610 }
611 return false;
612 }
613 return performPatternMatch(patternEnv.getValue(pVar), patternEnv, value, deltaEnv);
614
615 case ATerm.APPL:
616 if(value.getType() != ATerm.APPL) return false;
617
618 ATermAppl pa = (ATermAppl) pattern;
619 ATermAppl va = (ATermAppl) value;
620 if(pa.getAFun() != va.getAFun()) return false;
621
622 ATerm[] patternChildren = pa.getArgumentArray();
623 ATerm[] valueChildren = va.getArgumentArray();
624 for(int i = patternChildren.length - 1; i >= 0; i--){
625 if(!performPatternMatch(patternChildren[i], patternEnv, valueChildren[i], deltaEnv)) return false;
626 }
627
628 return true;
629 case ATerm.LIST:
630 if(value.getType() != ATerm.LIST) return false;
631
632 ATermList pl = (ATermList) pattern;
633 ATermList vl = (ATermList) value;
634 int plLength = pl.getLength();
635 if(plLength != vl.getLength()) return false;
636 while(pl != EmptyList){
637 if(!performPatternMatch(pl.getFirst(), patternEnv, vl.getFirst(), deltaEnv)) return false;
638 pl = pl.getNext();
639 vl = vl.getNext();
640 }
641
642 return true;
643 case ATerm.PLACEHOLDER:
644 case ATerm.INT:
645 case ATerm.REAL:
646 case ATerm.BLOB:
647 return ((pattern.hasAnnotations() ? pattern.removeAnnotations() : pattern) == (value.hasAnnotations() ? value.removeAnnotations() : value));
648 default:
649 throw new ToolBusInternalError("Illegal ATerm pattern in matchPatternToValue: " + pattern);
650 }
651 }
652
653 private boolean performMatch(ATerm left, Environment leftEnv, List<Binding> leftDeltaEnv, ATerm right, Environment rightEnv, List<Binding> rightDeltaEnv){
654 ATerm rightTerm = right;
655 if(rightTerm.getType() == VAR){
656 TBTermVar rightVar = (TBTermVar) rightTerm;
657 if(rightVar.isResultVar()){
658 if(left.getType() == VAR){
659 TBTermVar leftVar = (TBTermVar) left;
660 if(!leftVar.isResultVar()){
661 ATerm leftValue = leftEnv.getValue(leftVar);
662
663 if(Functions.compatibleTypes(rightVar.getVarType(), leftValue)){
664 ATerm fullySubstitutedLeftValue = fullSubstitute(leftValue, leftEnv);
665 if(fullySubstitutedLeftValue != null){
666 Binding deltaBinding = new Binding(rightVar, fullySubstitutedLeftValue);
667 rightDeltaEnv.add(deltaBinding);
668 return true;
669 }
670 return false;
671 }
672 }else{
673 return false;
674 }
675 }else{
676 if(Functions.compatibleTypes(rightVar.getVarType(), left)){
677 ATerm fullySubstitutedLeft = fullSubstitute(left, leftEnv);
678 if(fullySubstitutedLeft != null){
679 Binding deltaBinding = new Binding(rightVar, fullySubstitutedLeft);
680 rightDeltaEnv.add(deltaBinding);
681 return true;
682 }
683 return false;
684 }
685 }
686 return false;
687 }
688
689 rightTerm = rightEnv.getValue(rightVar);
690 }
691
692 switch(left.getType()){
693 case VAR:
694 TBTermVar pVar = (TBTermVar) left;
695 if(pVar.isResultVar()){
696 if(Functions.compatibleTypes(pVar.getVarType(), rightTerm)){
697 ATerm fullySubstitutedRightValue = fullSubstitute(rightTerm, rightEnv);
698 if(fullySubstitutedRightValue != null){
699 Binding deltaBinding = new Binding(pVar, fullySubstitutedRightValue);
700 leftDeltaEnv.add(deltaBinding);
701 return true;
702 }
703 return false;
704 }
705 return false;
706 }
707 return performMatch(leftEnv.getValue(pVar), leftEnv, leftDeltaEnv, rightTerm, rightEnv, rightDeltaEnv);
708
709 case ATerm.APPL:
710 if(rightTerm.getType() != ATerm.APPL) return false;
711
712 ATermAppl pa = (ATermAppl) left;
713 ATermAppl va = (ATermAppl) rightTerm;
714 if(pa.getAFun() != va.getAFun()) return false;
715
716 ATerm[] patternChildren = pa.getArgumentArray();
717 ATerm[] valueChildren = va.getArgumentArray();
718 for(int i = patternChildren.length - 1; i >= 0; i--){
719 if(!performMatch(patternChildren[i], leftEnv, leftDeltaEnv, valueChildren[i], rightEnv, rightDeltaEnv)) return false;
720 }
721
722 return true;
723 case ATerm.LIST:
724 if(rightTerm.getType() != ATerm.LIST) return false;
725
726 ATermList pl = (ATermList) left;
727 ATermList vl = (ATermList) rightTerm;
728 int plLength = pl.getLength();
729 if(plLength != vl.getLength()) return false;
730 while(pl != EmptyList){
731 if(!performMatch(pl.getFirst(), leftEnv, leftDeltaEnv, vl.getFirst(), rightEnv, rightDeltaEnv)) return false;
732 pl = pl.getNext();
733 vl = vl.getNext();
734 }
735
736 return true;
737 case ATerm.PLACEHOLDER:
738 case ATerm.INT:
739 case ATerm.REAL:
740 case ATerm.BLOB:
741 return ((left.hasAnnotations() ? left.removeAnnotations() : left) == (rightTerm.hasAnnotations() ? rightTerm.removeAnnotations() : rightTerm));
742 default:
743 throw new ToolBusInternalError("Illegal ATerm pattern in matchPatternToValue: " + left);
744 }
745 }
746
747 public boolean mightMatch(ATerm terma, ATerm termb){
748 switch(terma.getType()){
749 case VAR:
750 return Functions.compatibleTypes(((TBTermVar) terma).getVarType(), termb);
751 case ATerm.BLOB:
752 if(isAnyVar(termb)) return true;
753 return terma.isEqual(termb) || (termb == BlobPlaceholder) || (termb == TermPlaceholder);
754
755 case ATerm.INT:
756 if(isAnyVar(termb)) return true;
757 return terma.isEqual(termb) || (termb == IntPlaceholder) || (termb == TermPlaceholder);
758
759 case ATerm.REAL:
760 if(isAnyVar(termb)) return true;
761 return terma.isEqual(termb) || (termb == RealPlaceholder) || (termb == TermPlaceholder);
762
763 case ATerm.PLACEHOLDER:
764 if(isAnyVar(termb)) return true;
765
766 if(terma == TermPlaceholder) return true;
767
768 switch(termb.getType()){
769 case ATerm.INT:
770 return (terma == IntPlaceholder);
771 case ATerm.REAL:
772 return (terma == RealPlaceholder);
773 case ATerm.APPL:
774 return matchPlaceholder((ATermAppl) termb, (ATermPlaceholder) terma, true);
775 case ATerm.BLOB:
776 return (terma == BlobPlaceholder);
777 case ATerm.LIST:
778 return matchListPlaceholder((ATermList) termb, (ATermPlaceholder) terma, true);
779 }
780 return false;
781
782 case ATerm.APPL:
783 if(isAnyVar(termb)) return true;
784 ATermAppl apta = (ATermAppl) terma;
785
786 switch(termb.getType()){
787 case ATerm.PLACEHOLDER:
788 return matchPlaceholder(apta, (ATermPlaceholder) termb, false);
789
790 case ATerm.APPL:
791 ATermAppl aptb = (ATermAppl) termb;
792 if(apta.getAFun() != aptb.getAFun()) return false;
793
794 ATerm a_args[] = apta.getArgumentArray();
795 ATerm b_args[] = aptb.getArgumentArray();
796 for(int i = a_args.length - 1; i >= 0; i--){
797 if(!mightMatch(a_args[i], b_args[i])) return false;
798 }
799 return true;
800 default:
801 return false;
802 }
803
804 case ATerm.LIST:
805 if(isAnyVar(termb)) return true;
806
807 ATermList lsta = (ATermList) terma;
808 switch(termb.getType()){
809 case ATerm.PLACEHOLDER:
810 return matchListPlaceholder(lsta, (ATermPlaceholder) termb, false);
811
812 case ATerm.LIST:
813 ATermList lstb = (ATermList) termb;
814 if(lsta.getLength() != lstb.getLength()) return false;
815
816 while(!lsta.isEmpty()){
817 if(!mightMatch(lsta.getFirst(), lstb.getFirst())) return false;
818 lsta = lsta.getNext();
819 lstb = lstb.getNext();
820 }
821 return true;
822 default:
823 return false;
824 }
825
826 default:
827 throw new ToolBusInternalError("illegal ATerm in performMatch: " + terma);
828 }
829 }
830
831 private boolean matchListPlaceholder(ATermList terma, ATermPlaceholder tb, boolean swapargs){
832 ATermList ta = terma;
833
834 if(tb == ListPlaceholder) return true;
835
836 ATerm placeholder = tb.getPlaceholder();
837 if(placeholder.getType() == ATerm.APPL){
838 ATermAppl aplPlaceholder = (ATermAppl) placeholder;
839 if(aplPlaceholder.getName() != "list") return false;
840
841 int arity = aplPlaceholder.getArity();
842
843 if(arity == 1){
844 ATerm elemtype = aplPlaceholder.getArgument(0);
845 ATermPlaceholder elm = makePlaceholder(elemtype);
846
847 while(!ta.isEmpty()){
848 if(!swapMatch(elm, ta.getFirst(), swapargs)) return false;
849
850 ta = ta.getNext();
851 }
852 return true;
853 }
854
855 if(arity != ta.getLength()) return false;
856
857 for(int i = 0; i < arity; i++){
858 ATerm elemtype = aplPlaceholder.getArgument(i);
859 ATermPlaceholder elemPlaceholder = makePlaceholder(elemtype);
860
861 if(!swapMatch(elemPlaceholder, ta.getFirst(), swapargs)) return false;
862
863 ta = ta.getNext();
864 }
865 return true;
866 }
867 return swapMatch(ta, placeholder, swapargs);
868 }
869
870 private boolean matchPlaceholder(ATermAppl ta, ATermPlaceholder tb, boolean swapargs){
871 if(tb == StrPlaceholder && ta.getArity() == 0) return true;
872 else if(tb == TermPlaceholder) return true;
873
874 ATerm placeholder = tb.getPlaceholder();
875 if(placeholder.getType() == ATerm.APPL){
876 ATermAppl aplPlaceholder = (ATermAppl) placeholder;
877 int arity = aplPlaceholder.getArity();
878
879 if(arity == 0) return (ta.getName() == aplPlaceholder.getName());
880
881 if(arity != ta.getArity()) return false;
882
883 for(int i = arity - 1; i >= 0; i--){
884 ATerm elemtype = aplPlaceholder.getArgument(i);
885 ATermPlaceholder elemPlaceholder = makePlaceholder(elemtype);
886
887 if(!swapMatch(elemPlaceholder, ta.getArgument(i), swapargs)) return false;
888 }
889 return true;
890
891 }
892 return swapMatch(ta, placeholder, swapargs);
893 }
894
895 private boolean swapMatch(ATerm ta, ATerm tb, boolean swapargs){
896 return swapargs ? mightMatch(tb, ta) : mightMatch(ta, tb);
897 }
898 }