001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: // This file is part of KeY - Integrated Deductive Software Design
009: // Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
010: // and Chalmers University of Technology, Sweden
011: //
012: // The KeY system is protected by the GNU General Public License.
013: // See LICENSE.TXT for details.
014: //
015:
016: package de.uka.ilkd.key.logic.op;
017:
018: import de.uka.ilkd.key.logic.Name;
019: import de.uka.ilkd.key.logic.Term;
020: import de.uka.ilkd.key.logic.sort.IteratorOfSort;
021: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
022: import de.uka.ilkd.key.logic.sort.SetOfSort;
023: import de.uka.ilkd.key.logic.sort.Sort;
024:
025: /**
026: * This implements a general conditional operator <tt>if (phi) (t1) (t2)</tt>
027: */
028: public class IfThenElse extends Op {
029:
030: /**
031: * creates the default if-else operator
032: */
033: IfThenElse() {
034: super (new Name("if-then-else"));
035: }
036:
037: /**
038: * creates an if-else operator of the given name
039: */
040: IfThenElse(Name name) {
041: super (name);
042: }
043:
044: public boolean validTopLevel(Term term) {
045: final Sort s0 = term.sub(0).sort();
046: final Sort s1 = term.sub(1).sort();
047: final Sort s2 = term.sub(2).sort();
048:
049: // TODO: like in <code>ConjCond</code>, but this is really bad!!! /PR
050: return term.arity() == arity() && s0 == Sort.FORMULA
051: && (s1 == Sort.FORMULA) == (s2 == Sort.FORMULA);
052: }
053:
054: public Sort sort(Term[] term) {
055: final Sort s2 = term[1].sort();
056: final Sort s3 = term[2].sort();
057: if (s2 instanceof ProgramSVSort
058: || s2 == AbstractMetaOperator.METASORT) {
059: return s3;
060: }
061: if (s3 instanceof ProgramSVSort
062: || s3 == AbstractMetaOperator.METASORT) {
063: return s2;
064: } else {
065: // still a mess but a better one
066: return getCommonSuperSort(s2, s3);
067: }
068: }
069:
070: private Sort getCommonSuperSort(Sort s1, Sort s2) {
071: if (s1 == Sort.FORMULA) {
072: assert s2 == Sort.FORMULA;
073: return Sort.FORMULA;
074: }
075:
076: if (s1.extendsTrans(s2))
077: return s2;
078: else if (s2.extendsTrans(s1))
079: return s1;
080:
081: Sort result = Sort.ANY;
082: final SetOfSort set1 = s1.extendsSorts();
083: final SetOfSort set2 = s2.extendsSorts();
084:
085: final IteratorOfSort sort1It = set1.iterator();
086: while (sort1It.hasNext()) {
087: final Sort sort1 = sort1It.next();
088: if (set2.contains(sort1)) {
089: if (result == Sort.ANY) {
090: result = sort1;
091: } else {
092: // not uniquely determinable
093: return Sort.ANY;
094: }
095: }
096: }
097: return result;
098: }
099:
100: public int arity() {
101: return 3;
102: }
103: }
|