1.1 --- a/src/java-tests/isac/util/tactics/TestTactic.java Thu Feb 21 14:19:57 2008 +0100
1.2 +++ b/src/java-tests/isac/util/tactics/TestTactic.java Thu Feb 21 16:48:59 2008 +0100
1.3 @@ -59,8 +59,20 @@
1.4 xxx = form.toString();
1.5 xxx = (thm.getFormula()).toString();
1.6 xxx = tac.showToBeginner();
1.7 - System.out.println("xxx="+ tac.showToBeginner());
1.8 + assertEquals("l * n + m * n = (l + m) * n", tac.showToBeginner());
1.9
1.10 + form.setText("?a = ?a");
1.11 + thm.setFormula(form);
1.12 + ((Rewrite) tac).setTheorem(thm);
1.13 + assertEquals("a = a", tac.showToBeginner());
1.14 +
1.15 + tac = null;
1.16 + tac = new RewriteInst();
1.17 + form.setText("(?k + ?bdv = ?m) = (?bdv = ?m + -1 * ?k)");
1.18 + thm.setFormula(form);
1.19 + ((RewriteInst) tac).setTheorem(thm);
1.20 + assertEquals("(k + bdv = m) = (bdv = m + -1 * k)", tac.showToBeginner());
1.21 +
1.22 System.out
1.23 .println("---END isac.util.tactics.TestTactic#testShowToBeginner");
1.24 }
2.1 --- a/src/java/isac/gui/treetable/CalcModelNode.java Thu Feb 21 14:19:57 2008 +0100
2.2 +++ b/src/java/isac/gui/treetable/CalcModelNode.java Thu Feb 21 16:48:59 2008 +0100
2.3 @@ -123,7 +123,7 @@
2.4 UIActionOnCalcElement uaoce = (UIActionOnCalcElement) tactic;
2.5
2.6 tacticPopupHandler_.addAction(tactic, ((Tactic) uaoce.getCalcElement())
2.7 - .toSMLString());
2.8 + .showToBeginner());
2.9 }
2.10
2.11 /**
3.1 --- a/src/java/isac/util/tactics/Rewrite.java Thu Feb 21 14:19:57 2008 +0100
3.2 +++ b/src/java/isac/util/tactics/Rewrite.java Thu Feb 21 16:48:59 2008 +0100
3.3 @@ -19,10 +19,11 @@
3.4 }
3.5
3.6 /**
3.7 - *
3.8 + * show a tactic as simple as possible: theorems in rewrite-tactics without
3.9 + * '?' etc.
3.10 */
3.11 public String showToBeginner() {
3.12 - return theorem_.getFormula();
3.13 + return theorem_.getFormulaSimplified();
3.14 }
3.15
3.16 /**
4.1 --- a/src/java/isac/util/tactics/RewriteInst.java Thu Feb 21 14:19:57 2008 +0100
4.2 +++ b/src/java/isac/util/tactics/RewriteInst.java Thu Feb 21 16:48:59 2008 +0100
4.3 @@ -8,16 +8,24 @@
4.4 * @author Richard Gradischnegg
4.5 */
4.6 public class RewriteInst extends Tactic {
4.7 - String variable, value;
4.8 + String variable, value;//FIXME.WN082021 this should be a Vektor of pairs !
4.9
4.10 - Theorem theorem;
4.11 + Theorem theorem_;
4.12
4.13 public RewriteInst() {
4.14 }
4.15
4.16 public String toSMLString() {
4.17 return name_ + " ([\"(" + variable + "," + value + ")\"],"
4.18 - + theorem.toSMLString() + ")";
4.19 + + theorem_.toSMLString() + ")";
4.20 + }
4.21 +
4.22 + /**
4.23 + * show a tactic as simple as possible: theorems in rewrite-tactics without
4.24 + * '?' etc.
4.25 + */
4.26 + public String showToBeginner() {
4.27 + return theorem_.getFormulaSimplified();
4.28 }
4.29
4.30 /**
4.31 @@ -52,14 +60,14 @@
4.32 * @return
4.33 */
4.34 public Theorem getTheorem() {
4.35 - return theorem;
4.36 + return theorem_;
4.37 }
4.38
4.39 /**
4.40 * @param theorem
4.41 */
4.42 public void setTheorem(Theorem theorem) {
4.43 - this.theorem = theorem;
4.44 + this.theorem_ = theorem;
4.45 }
4.46
4.47 }
4.48 \ No newline at end of file
5.1 --- a/src/java/isac/util/tactics/Tactic.java Thu Feb 21 14:19:57 2008 +0100
5.2 +++ b/src/java/isac/util/tactics/Tactic.java Thu Feb 21 16:48:59 2008 +0100
5.3 @@ -107,11 +107,9 @@
5.4 }
5.5
5.6 /**
5.7 - * show the tactic to a beginner in a most simple form
5.8 + * show the tactic to a beginner in a most simple form;
5.9 *
5.10 - * WN080221 only shown like ..
5.11 - *
5.12 - * @see isac.util.tactics.Tactic#getTheoremSymbolic()
5.13 + * WN080221 only implemented for rewrite-tacs
5.14 */
5.15 public String showToBeginner() {
5.16 return this.toSMLString();
6.1 --- a/src/java/isac/util/tactics/Theorem.java Thu Feb 21 14:19:57 2008 +0100
6.2 +++ b/src/java/isac/util/tactics/Theorem.java Thu Feb 21 16:48:59 2008 +0100
6.3 @@ -16,10 +16,13 @@
6.4
6.5 public class Theorem implements Serializable {
6.6 static final long serialVersionUID = -233677392264313623L;
6.7 - String id, formula;
6.8
6.9 - //Theorem consist of the ID, and
6.10 - //the formula (still as a string -- waiting for MathML)
6.11 + String id_;
6.12 +
6.13 + String formula_;// FIXME.WN080221 Formula !
6.14 +
6.15 + // Theorem consist of the ID, and
6.16 + // the formula (still as a string -- waiting for MathML)
6.17
6.18 /**
6.19 * Format the class to a string which can be used as SML-Input
6.20 @@ -27,28 +30,50 @@
6.21 * @return
6.22 */
6.23 public String toSMLString() {
6.24 - return "(\"" + id + "\",\"\")"; //formula may be empty at input
6.25 + return "(\"" + id_ + "\",\"\")"; // formula may be empty at input
6.26 }
6.27
6.28 public String getFormula() {
6.29 - return formula;
6.30 + return formula_;
6.31 + }
6.32 +
6.33 + public String getFormulaSimplified() {
6.34 + // remove premises, they are hard to understand
6.35 + String cut = formula_;
6.36 + int prems = formula_.lastIndexOf("==>");
6.37 + if (prems > 0) {
6.38 + cut = formula_.substring(prems + 4);// "==>" always followed by " "
6.39 + }
6.40 + // remove '?' as done within Isabelle theories
6.41 + char[] cs1 = cut.toCharArray();
6.42 + StringBuffer cs2 = new StringBuffer();
6.43 + // System.out.println("cut = " + cut);
6.44 + for (int i = 0; i < cs1.length; i++) {
6.45 + if (cs1[i] != '?') {
6.46 + cs2.append(cs1[i]);
6.47 + }
6.48 + // System.out.println("i = " + i + ", cs1[i] = " + cs1[i] + ", cs2 =
6.49 + // "
6.50 + // + cs2.toString());
6.51 + }
6.52 + return cs2.toString();
6.53 }
6.54
6.55 public String getId() {
6.56 - return id;
6.57 + return id_;
6.58 }
6.59
6.60 - //WN060327 quick and dirty for XMLParserDigest
6.61 + // WN060327 quick and dirty for XMLParserDigest
6.62 public void setFormula(Formula form) {
6.63 - formula = form.toSMLString();
6.64 + formula_ = form.toSMLString();
6.65 }
6.66
6.67 public void setFormula(String string) {
6.68 - formula = string;
6.69 + formula_ = string;
6.70 }
6.71
6.72 public void setId(String string) {
6.73 - id = string;
6.74 + id_ = string;
6.75 }
6.76
6.77 }
6.78 \ No newline at end of file