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: //
009: //
010:
011: package de.uka.ilkd.key.logic.op;
012:
013: import java.util.HashSet;
014:
015: import de.uka.ilkd.key.logic.Name;
016: import de.uka.ilkd.key.logic.ProgramElementName;
017: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
018: import de.uka.ilkd.key.logic.sort.Sort;
019:
020: /** A factory class for different Schema Variables
021: */
022: public class SchemaVariableFactory {
023:
024: private SchemaVariableFactory() {
025: }
026:
027: /**
028: * creates a SchemaVariable representing quantified variables
029: * @param name the Name of the SchemaVariable
030: * @param sort the Sort of the variable the SchemaVariable will be
031: * used to represent
032: * @param listSV a boolean which is true iff the schemavariable is allowed
033: * to match a list of quantified variables
034: * @return the SchemaVariable
035: */
036: public static SchemaVariable createVariableSV(Name name, Sort sort,
037: boolean listSV) {
038: return new VariableSV(name, sort, listSV);
039: }
040:
041: /**
042: * creates a SchemaVariable representing a term but not a formula
043: * @param name the Name of the SchemaVariable
044: * @param sort the Sort of the term the SchemaVariable will be
045: * used to represent
046: * @param listSV a boolean which is true iff the schemavariable is allowed
047: * to match a list of terms
048: * @param rigidness true iff this SV may only match rigid
049: * terms/formulas
050: * @param strictSV boolean indicating if the schemavariable is declared as strict
051: * forcing exact type match
052: * @return the SchemaVariable
053: */
054: public static SchemaVariable createTermSV(Name name, Sort sort,
055: boolean listSV, boolean rigidness, boolean strictSV) {
056: return new TermSV(name, sort, listSV, rigidness, strictSV);
057: }
058:
059: /**
060: * creates a SchemaVariable representing an operator
061: * @param name the Name of the SchemaVariable
062: * @param arity the arity of the modal operators represented by this SV
063: * param modalitylist the list of actual modalities to match this SV (right now box & diamond)
064: * @return the SchemaVariable
065: */
066: public static SchemaVariable createOperatorSV(Name name,
067: Class matchingType, Sort sort, int arity, HashSet operators) {
068: if (matchingType == Modality.class) {
069: return new ModalOperatorSV(name, arity, operators);
070: } else {
071: return new OperatorSV(name, sort, arity, operators);
072: }
073: }
074:
075: public static SchemaVariable createTermSV(Name name, Sort sort,
076: boolean listSV) {
077: return createTermSV(name, sort, listSV, false, false);
078: }
079:
080: /** creates a SchemaVariable representing a formula
081: * @param name the Name of the SchemaVariable
082: * @param rigidness true iff this SV may only match rigid
083: * terms/formulas
084: * @param listSV a boolean which is true iff the schemavariable is allowed
085: * to match a list of formulas
086: * @return the SchemaVariable
087: */
088: public static SchemaVariable createFormulaSV(Name name,
089: boolean listSV, boolean rigidness) {
090: return new FormulaSV(name, listSV, rigidness);
091: }
092:
093: public static SchemaVariable createFormulaSV(Name name,
094: boolean listSV) {
095: return createFormulaSV(name, listSV, false);
096: }
097:
098: public static SchemaVariable createListSV(Name name, Class matchType) {
099: return new ListSV(name, matchType);
100: }
101:
102: public static SchemaVariable createNameSV(Name name) {
103: return new NameSV(name);
104: }
105:
106: /** creates a SchemaVariable representing a program construct
107: * @param name the ProgramElementName of the SchemaVariable
108: * @param listSV a boolean which is true iff the schemavariable is allowed
109: * to match a list of program constructs
110: * @return the SchemaVariable
111: */
112: public static SchemaVariable createProgramSV(
113: ProgramElementName name, ProgramSVSort s, boolean listSV) {
114: return new ProgramSV(name, s, listSV);
115: }
116:
117: /**
118: * creates a SchemaVariable representing a skolem term
119: * @param name the Name of the SchemaVariable
120: * @param listSV a boolean which is true iff the schemavariable is allowed
121: * to match a list of skolem terms
122: * @return the SchemaVariable
123: */
124: public static SchemaVariable createSkolemTermSV(Name name, Sort s,
125: boolean listSV) {
126: return new SkolemTermSV(name, s, listSV);
127: }
128: }
|