01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: /*
12: * This class is used to create new metavariables, which are also
13: * added to the variable namespace.
14: */
15:
16: package de.uka.ilkd.key.logic;
17:
18: import de.uka.ilkd.key.java.Services;
19: import de.uka.ilkd.key.logic.op.Metavariable;
20: import de.uka.ilkd.key.logic.sort.Sort;
21: import de.uka.ilkd.key.proof.Counter;
22: import de.uka.ilkd.key.proof.Goal;
23: import de.uka.ilkd.key.proof.Proof;
24:
25: public class MetavariableDeliverer {
26:
27: private Proof proof;
28:
29: public MetavariableDeliverer(Proof p_proof) {
30: proof = p_proof;
31: }
32:
33: /**
34: * Check whether p_sort allows metavariables
35: * This is currently hard-coded and only forbidden for the
36: * "numbers"-sort
37: * @return true iff p_sort allows metavariables
38: */
39: private static boolean checkSort(Sort p_sort, Services services) {
40: return services.getTypeConverter().getIntegerLDT()
41: .getNumberSymbol().argSort(0) != p_sort;
42: }
43:
44: /**
45: * Construct a unique identifier by adding a number to the base
46: * name
47: */
48: public static int mv_Counter(String base, Goal g) {
49: Counter c = g.proof().getServices().getCounter(
50: "metavar_" + base);
51: return c.getCountPlusPlusWithParent(g.node());
52: }
53:
54: /**
55: * Create new metavariable and add it to the namespace var_ns of
56: * the mediator.
57: * @param name name of the variable
58: * @param p_sort Sort of the variable
59: * @return New metavariable, or null iff p_sort allows no
60: * metavariables
61: */
62: public Metavariable createNewVariable(String name, Sort p_sort) {
63: if (!checkSort(p_sort, proof.getServices()))
64: return null;
65: Metavariable var = new Metavariable(new Name(name), p_sort);
66: proof.getNamespaces().variables().add(var);
67: return var;
68: }
69:
70: /**
71: * Create new variable for instantiation of unknown schema
72: * variables when applying taclets.
73: * @param p_sort Sort of the variable
74: * @return New metavariable, or null iff p_sort allows no
75: * metavariables
76: */
77: public static Metavariable createNewMatchVariable(
78: String p_basename, Sort p_sort, Services services) {
79: if (!checkSort(p_sort, services))
80: return null;
81:
82: return Metavariable.createTemporaryVariable(
83: new Name(p_basename), p_sort);
84: }
85: }
|