2 * @author Walther Neuper
3 * Copyright (c) due to license terms
4 * Created on Aug 16, 2015
5 * Institute for Softwaretechnology, Graz University of Technology, Austria.
8 package isac.bridge.xml;
10 import isac.bridge.xml.DataTypes;
11 import isac.util.tactics.TermTactic;
12 import isac.util.tactics.Rewrite;
13 import isac.util.tactics.RewriteInst;
14 import isac.util.tactics.RewriteSet;
15 import isac.util.tactics.RewriteSetInst;
16 import isac.util.tactics.SimpleTactic;
17 import isac.util.tactics.StringListTactic;
18 import isac.util.tactics.SubProblemTactic;
19 import isac.util.tactics.Tactic;
20 import edu.tum.cs.isabelle.api.XML;
23 * Trials to cope with type conversions between Java and Scala.
25 public class DataTypesCompanion {
27 // in Scala no way was found for accepting the type conversions:
29 // def xml_of_Tactic(tac: Tactic): isabelle.XML.Tree = tac.getClass.getSimpleName match {
30 // case "SubProblemTactic" => xml_of_SubProblemTactic((SubProblemTactic)tac)
31 // //Substitute TODO clarify
32 // case "Rewrite" => xml_of_Rewrite((Rewrite)tac)
33 // case "RewriteInst" => xml_of_RewriteInst((RewriteInst)tac)
34 // case "RewriteSet" => xml_of_RewriteSet((RewriteSet)tac)
35 // case "RewriteSetInst" => xml_of_RewriteSetInst((RewriteSetInst)tac)
36 // case "TermTactic" => xml_of_TermTactic((TermTactic)tac)
37 // case "SimpleTactic" => xml_of_SimpleTactic((SimpleTactic)tac)
38 // case "StringListTactic" => xml_of_StringListTactic((StringListTactic)tac)
40 // throw new IllegalArgumentException("xml_of_Tactic: case \"" + str + "\" not covered")
42 // ERROR "This method must return a result of type XML.tree".
44 public static XML.Tree xml_of_Tactic (Tactic tac) {
45 XML.Tree return_val = null;
46 if (tac instanceof SubProblemTactic)
47 return (XML.Tree)DataTypes.xml_of_SubProblemTactic((SubProblemTactic)tac);
48 //else if (tac instanceof Substitute)
49 // return_val = isabelle.XML.Tree)DataTypes.xml_of_Substitute((Substitute)tac);
50 else if ((tac instanceof Rewrite))
51 return_val = (XML.Tree)DataTypes.xml_of_Rewrite((Rewrite)tac);
52 else if (tac instanceof RewriteInst)
53 return_val = (XML.Tree)DataTypes.xml_of_RewriteInst((RewriteInst)tac);
54 else if (tac instanceof RewriteSet)
55 return_val = (XML.Tree)DataTypes.xml_of_RewriteSet((RewriteSet)tac);
56 else if (tac instanceof RewriteSetInst)
57 return_val = (XML.Tree)DataTypes.xml_of_RewriteSetInst((RewriteSetInst)tac);
58 else if (tac instanceof TermTactic)
59 return_val = (XML.Tree)DataTypes.xml_of_TermTactic((TermTactic)tac);
60 else if (tac instanceof SimpleTactic)
61 return_val = (XML.Tree)DataTypes.xml_of_SimpleTactic((SimpleTactic)tac);
62 else if (tac instanceof StringListTactic)
63 return_val = (XML.Tree)DataTypes.xml_of_StringListTactic((StringListTactic)tac);