wneuper@4772: /* 
wneuper@4772:  * @author Walther Neuper
wneuper@4772:  * Copyright (c) due to license terms
wneuper@4772:  * Created on Aug 16, 2015
wneuper@4772:  * Institute for Softwaretechnology, Graz University of Technology, Austria.
wneuper@4772:  */
wneuper@4772: 
wneuper@4772: package isac.bridge.xml;
wneuper@4772: 
wneuper@4772: import isac.bridge.xml.DataTypes;
wneuper@4810: import isac.util.tactics.TermTactic;
wneuper@4772: import isac.util.tactics.Rewrite;
wneuper@4772: import isac.util.tactics.RewriteInst;
wneuper@4772: import isac.util.tactics.RewriteSet;
wneuper@4772: import isac.util.tactics.RewriteSetInst;
wneuper@4772: import isac.util.tactics.SimpleTactic;
wneuper@4772: import isac.util.tactics.StringListTactic;
wneuper@4772: import isac.util.tactics.SubProblemTactic;
wneuper@4772: import isac.util.tactics.Tactic;
walther@5239: import edu.tum.cs.isabelle.api.XML;
wneuper@4772: 
wneuper@4772: /**
wneuper@4772:  * Trials to cope with type conversions between Java and Scala.
wneuper@4772:  */
wneuper@4772: public class DataTypesCompanion {
wneuper@4772: 	
wneuper@4772: 	// in Scala no way was found for accepting the type conversions:
wneuper@4772: 	//
wneuper@4772: 	//  def xml_of_Tactic(tac: Tactic): isabelle.XML.Tree = tac.getClass.getSimpleName match {
wneuper@4772: 	//    case "SubProblemTactic" => xml_of_SubProblemTactic((SubProblemTactic)tac)
wneuper@4772: 	//    //Substitute  TODO clarify
wneuper@4772: 	//    case "Rewrite" => xml_of_Rewrite((Rewrite)tac)
wneuper@4772: 	//    case "RewriteInst" => xml_of_RewriteInst((RewriteInst)tac)
wneuper@4772: 	//    case "RewriteSet" => xml_of_RewriteSet((RewriteSet)tac)
wneuper@4772: 	//    case "RewriteSetInst" => xml_of_RewriteSetInst((RewriteSetInst)tac)
wneuper@4810: 	//    case "TermTactic" => xml_of_TermTactic((TermTactic)tac)
wneuper@4772: 	//    case "SimpleTactic" => xml_of_SimpleTactic((SimpleTactic)tac)
wneuper@4772: 	//    case "StringListTactic" => xml_of_StringListTactic((StringListTactic)tac)
wneuper@4772: 	//    case str => 
wneuper@4772: 	//      throw new IllegalArgumentException("xml_of_Tactic: case \"" + str + "\" not covered")
wneuper@4772: 	//  }
wneuper@4772: 	// ERROR "This method must return a result of type XML.tree".
wneuper@4772: 	//
wneuper@4772: 	public static XML.Tree xml_of_Tactic (Tactic tac) {
wneuper@4772: 		XML.Tree return_val = null;
wneuper@4772: 	  if (tac instanceof SubProblemTactic) 
wneuper@4772: 		return (XML.Tree)DataTypes.xml_of_SubProblemTactic((SubProblemTactic)tac);
wneuper@4772: 	  //else if (tac instanceof Substitute) 
wneuper@4772: 	  //  return_val =  isabelle.XML.Tree)DataTypes.xml_of_Substitute((Substitute)tac);
wneuper@4772: 	  else if ((tac instanceof Rewrite))
wneuper@4772: 		  return_val =  (XML.Tree)DataTypes.xml_of_Rewrite((Rewrite)tac);
wneuper@4772: 	  else if (tac instanceof RewriteInst)
wneuper@4772: 		  return_val =  (XML.Tree)DataTypes.xml_of_RewriteInst((RewriteInst)tac);
wneuper@4772: 	  else if (tac instanceof RewriteSet)
wneuper@4772: 		  return_val =  (XML.Tree)DataTypes.xml_of_RewriteSet((RewriteSet)tac);
wneuper@4772: 	  else if (tac instanceof RewriteSetInst) 
wneuper@4772: 		  return_val =  (XML.Tree)DataTypes.xml_of_RewriteSetInst((RewriteSetInst)tac);
wneuper@4810: 	  else if (tac instanceof TermTactic) 
wneuper@4810: 		  return_val =  (XML.Tree)DataTypes.xml_of_TermTactic((TermTactic)tac);
wneuper@4772: 	  else if (tac instanceof SimpleTactic) 
wneuper@4772: 		  return_val =  (XML.Tree)DataTypes.xml_of_SimpleTactic((SimpleTactic)tac);
wneuper@4772: 	  else if (tac instanceof StringListTactic) 
wneuper@4772: 		  return_val =  (XML.Tree)DataTypes.xml_of_StringListTactic((StringListTactic)tac);
wneuper@4772: 	return return_val;
wneuper@4772: 	}
wneuper@4772: 	
wneuper@4772: 
wneuper@4772: }