wneuper/isac: isac-java/src/java/isac/bridge/xml/JavaToIsa.scala@086b1413d0ae

     1 /*

     2  * @author Walther Neuper

     3  * Copyright (c) due to license terms

     4  * Created on Jul 14, 2015

     5  * Institute for Softwaretechnology, Graz University of Technology, Austria.

     6  */

     8 package isac.bridge.xml

    10 import isac.bridge.CChanged

    11 import isac.util.formulae.CalcFormula

    12 import isac.util.formulae.CalcHead

    13 import isac.util.formulae.Formula

    14 import isac.util.formulae.Position

    15 import isac.util.formulae.Specification

    16 import isac.util.tactics.Tactic

    17 import isac.util.Variant

    18 import isac.util.Formalization

    19 import isac.wsdialog.IContextProvider.ContextType;

    21 import isabelle.XML

    22 import isabelle.Markup

    24 import java.util.ArrayList

    25 import java.util.Vector

    26 import java.math.BigInteger

    27 import scala.math.BigInt

    28 import scala.collection.JavaConverters._

    29 import scala.collection.JavaConversions._

    31 /**

    32  * Convert arguments of JSystem.invoke(Operations.* to XML;

    33  * Conversions use Scala's pattern matching, which is not available in Java.

    34  * The sequence in the kernel's signature below is maintained.

    35  */

    36 object JavaToIsa {

    38 /* from isabisac/src/Tools/Frontend/interface.sml

    39 signature MATH_ENGINE =

    40   sig

    41     val appendFormula : calcID -> cterm' -> XML.tree

    42     val autoCalculate : calcID -> auto -> XML.tree

    43     val applyTactic : calcID -> pos' -> tac -> XML.tree

    44     val CalcTree : fmz list -> XML.tree

    45     val checkContext : calcID -> pos' -> guh -> XML.tree

    46     val DEconstrCalcTree : calcID -> XML.tree

    47     val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree

    48     val fetchProposedTactic : calcID -> XML.tree

    49     val findFillpatterns : calcID -> errpatID -> XML.tree

    50     val getAccumulatedAsms : calcID -> pos' -> XML.tree

    51     val getActiveFormula : calcID -> XML.tree

    52     val getAssumptions : calcID -> pos' -> XML.tree

    53     val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree

    54     val getTactic : calcID -> pos' -> XML.tree

    55     val initContext : calcID -> ketype -> pos' -> XML.tree

    56     val inputFillFormula: calcID -> string -> XML.tree

    57     val interSteps : calcID -> pos' -> XML.tree

    58     val Iterator : calcID -> XML.tree

    59     val IteratorTEST : calcID -> iterID

    60     val modelProblem : calcID -> XML.tree

    61     val modifyCalcHead : calcID -> icalhd -> XML.tree

    62     val moveActiveCalcHead : calcID -> XML.tree

    63     val moveActiveDown : calcID -> XML.tree

    64     val moveActiveFormula : calcID -> pos' -> XML.tree

    65     val moveActiveLevelDown : calcID -> XML.tree

    66     val moveActiveLevelUp : calcID -> XML.tree

    67     val moveActiveRoot : calcID -> XML.tree

    68     val moveActiveRootTEST : calcID -> XML.tree

    69     val moveActiveUp : calcID -> XML.tree

    70     val moveCalcHead : calcID -> pos' -> XML.tree

    71     val moveDown : calcID -> pos' -> XML.tree

    72     val moveLevelDown : calcID -> pos' -> XML.tree

    73     val moveLevelUp : calcID -> pos' -> XML.tree

    74     val moveRoot : calcID -> XML.tree

    75     val moveUp : calcID -> pos' -> XML.tree

    76     val refFormula : calcID -> pos' -> XML.tree

    77     val refineProblem : calcID -> pos' -> guh -> XML.tree

    78     val replaceFormula : calcID -> cterm' -> XML.tree

    79     val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree

    80     val resetCalcHead : calcID -> XML.tree

    81     val setContext : calcID -> pos' -> guh -> XML.tree

    82     val setMethod : calcID -> metID -> XML.tree

    83     val setNextTactic : calcID -> tac -> XML.tree

    84     val setProblem : calcID -> pblID -> XML.tree

    85     val setTheory : calcID -> thyID -> XML.tree

    86   end

    87 */

    89   //fun appendFormula : calcID -> cterm' -> XML.tree

    90   def append_form(calcid: scala.math.BigInt, form: String): XML.Tree =

    91   { XML.Elem(Markup("APPENDFORMULA", Nil), List(

    92       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

    93       DataTypes.xml_of_Formula(form)))

    94   }

    96   //fun autoCalculate : calcID -> auto -> XML.tree

    97   def auto_calculate(calcid: scala.math.BigInt, scope: String, steps: scala.math.BigInt): XML.Tree =

    98   { //ATTENTION the "if" below is according to "fun xml_to_auto" in datatypes.sml,

    99     //but NOT according to "if/else if" in BridgeRMI#autoCalculate for "isabelle tty".

   100     if (steps == 0)

   101       XML.Elem(Markup("AUTOCALC", Nil), List(

   102         XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   103         XML.Elem(Markup("AUTO", Nil), List(XML.Text(scope)))))

   104     else

   105       //dataypes.sml:

   106       //xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text i])) = Step (int_of_str i |>the)

   107       XML.Elem(Markup("AUTOCALC", Nil), List(

   108         XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   109         XML.Elem(Markup("AUTO", Nil), List(XML.Text("Step"), XML.Text(steps.toString())))))

   110   }

   112   //fun applyTactic : calcID -> pos' -> tac -> XML.tree  ...NOT IMPL. IN isac-java WN150813

   113   //fun CalcTree : fmz list -> XML.tree                  ...uses only DataTypes..fmz..

   115   //fun checkContext : calcID -> pos' -> guh -> XML.tree

   116   def   check_ctxt(calcid: scala.math.BigInt, from: Position, kestore_key: String): XML.Tree =

   117   { XML.Elem(Markup("CONTEXTTHY", Nil), List(

   118       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   119       DataTypes.xml_of_Position(from),

   120       XML.Elem(Markup("GUH", Nil), List(XML.Text(kestore_key)))))

   121   }

   123   //fun DEconstrCalcTree : calcID -> XML.tree    ...no further ado: scala.math.BigInt

   125   //fun fetchApplicableTactics : calcID -> int -> pos' -> XML.tree

   126   def   fetch_applicable_tacs(calcid: scala.math.BigInt, scope: scala.math.BigInt, pos: Position): XML.Tree =

   127   { XML.Elem(Markup("APPLICABLETACTICS", Nil), List(

   128       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   129       XML.Elem(Markup("INT", Nil), List(XML.Text(scope.toString()))),

   130       DataTypes.xml_of_Position(pos)))

   131   }

   133   //fun fetchProposedTactic : calcID -> XML.tree

   134   def   fetch_proposed_tac(calcid: scala.math.BigInt): XML.Tree =

   135   { XML.Elem(Markup("NEXTTAC", Nil), List(

   136       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString())))))

   137   }

   139   //fun findFillpatterns : calcID -> errpatID -> XML.tree

   140   //... only implemented in Math_Engine

   142   //fun getAccumulatedAsms : calcID -> pos' -> XML.tree

   143   def   get_accumulated_asms(calcid: scala.math.BigInt, pos: Position): XML.Tree =

   144   { XML.Elem(Markup("GETASSUMPTIONS", Nil), List(

   145       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   146       DataTypes.xml_of_Position(pos)))

   147   }

   149   //fun getActiveFormula : calcID -> XML.tree

   150   def   get_active_form(calcid: scala.math.BigInt): XML.Tree =

   151   { XML.Elem(Markup("CALCITERATOR", Nil), List(

   152       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString())))))

   153   }

   154   //fun getAssumptions : calcID -> pos' -> XML.tree

   155   def   get_asms(calcid: scala.math.BigInt, pos: Position): XML.Tree =

   156   { XML.Elem(Markup("APPLICABLETACTICS", Nil), List(

   157       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   158       DataTypes.xml_of_Position(pos)))

   159   }

   161   //fun getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree

   162   //def get_formulae(calcid: scala.math.BigInt, from: ICalcIterator,to: ICalcIterator,

   163   def   get_formulae(calcid: scala.math.BigInt, from: Position,     to: Position,

   164     level: scala.math.BigInt, rules: Boolean): XML.Tree =

   165   { XML.Elem(Markup("GETFORMULAEFROMTO", Nil), List(

   166       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   167       DataTypes.xml_of_Position(from), //Isabelle/Isac needs no further data from ICalcIterator

   168       DataTypes.xml_of_Position(to),

   169       XML.Elem(Markup("INT", Nil), List(XML.Text(level.toString()))),

   170       XML.Elem(Markup("BOOL", Nil), List(XML.Text(rules.toString)))))

   171   }

   173   //fun getTactic : calcID -> pos' -> XML.tree

   174   def   get_tac(calcid: scala.math.BigInt, pos: Position): XML.Tree =

   175   { XML.Elem(Markup("GETTACTIC", Nil), List(

   176       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   177       DataTypes.xml_of_Position(pos)))

   178   }

   180   //fun initContext : calcID -> ketype -> pos' -> XML.tree

   181   def   init_ctxt(calcid: scala.math.BigInt, ketype: ContextType, pos: Position): XML.Tree =

   182   { XML.Elem(Markup("GETASSUMPTIONS", Nil), List(

   183       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   184       DataTypes.xml_of_ContextType(ketype),

   185       DataTypes.xml_of_Position(pos) ))

   186   }

   188   //fun inputFillFormula: calcID -> string -> XML.tree

   189   //... ONLY IMPL. IN Math_Engine

   191   //fun interSteps : calcID -> pos' -> XML.tree

   192   def   inter_steps(calcid: scala.math.BigInt, pos: Position): XML.Tree =

   193   { XML.Elem(Markup("INTERSTEPS", Nil), List(

   194       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   195       DataTypes.xml_of_Position(pos)))

   196   }

   198   //fun Iterator : calcID -> XML.tree                ...IS ONLY A scala.math.BigInt

   199   //fun IteratorTEST : calcID -> iterID              ... only relevant for Isabelle/Isac

   200   //fun modelProblem : calcID -> XML.tree            ...IS ONLY A scala.math.BigInt

   201   //fun modifyCalcHead : calcID -> icalhd -> XML.tree

   202   def   modify_calchead(calcid: scala.math.BigInt, calchead: CalcHead): XML.Tree =

   203   { XML.Elem(Markup("MODIFYCALCHEAD", Nil), List(

   204       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   205   //====== TODO xml_of_CalcHead not finished =========================================

   206       DataTypes.xml_of_CalcHead(calchead)))

   207   }

   209   //fun moveActiveCalcHead : calcID -> XML.tree

   210   def   move_active_calchead(calcid: scala.math.BigInt): XML.Tree =

   211   { XML.Elem(Markup("CALCITERATOR", Nil), List(

   212       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString())))))

   213   }

   215   // BridgeRMI#moveActiveDown needs Protocol#move_active_down + Protocol#move_down

   216   //fun moveActiveDown : calcID -> XML.tree

   217   def   move_active_down(calcid: scala.math.BigInt): XML.Tree =

   218   { XML.Elem(Markup("CALCITERATOR", Nil), List(

   219       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString())))))

   220   }

   222   //fun moveActiveFormula : calcID -> pos' -> XML.tree

   223   def   move_active_form(calcid: scala.math.BigInt, pos: Position): XML.Tree =

   224   { XML.Elem(Markup("CALCITERATOR", Nil), List(

   225       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   226       DataTypes.xml_of_Position(pos)))

   227   }

   229   //fun moveActiveLevelDown : calcID -> XML.tree

   230   def   move_active_levdown(calcid: scala.math.BigInt): XML.Tree =

   231   { XML.Elem(Markup("CALCITERATOR", Nil), List(

   232       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString())))))

   233   }

   235   //fun moveActiveLevelUp : calcID -> XML.tree

   236   def   move_active_levup(calcid: scala.math.BigInt): XML.Tree =

   237   { XML.Elem(Markup("CALCITERATOR", Nil), List(

   238       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString())))))

   239   }

   241   //fun moveActiveRoot : calcID -> XML.tree

   242   def   moveactiveroot(calcid: scala.math.BigInt): XML.Tree =

   243   { XML.Elem(Markup("CALCITERATOR", Nil), List(

   244       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString())))))

   245   }

   247   //fun moveActiveRootTEST : calcID -> XML.tree

   248   //... only relevant for Isabelle/Isac

   250   //fun moveActiveUp : calcID -> XML.tree

   251   def   move_active_up(calcid: scala.math.BigInt): XML.Tree =

   252   { XML.Elem(Markup("CALCITERATOR", Nil), List(

   253       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString())))))

   254   }

   256   //fun moveCalcHead : calcID -> pos' -> XML.tree

   257   def   move_calchead(calcid: scala.math.BigInt, pos: Position): XML.Tree =

   258   { XML.Elem(Markup("GETTACTIC"/*shortcut in coding*/, Nil), List(

   259       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   260       DataTypes.xml_of_Position(pos)))

   261   }

   263   //fun moveDown : calcID -> pos' -> XML.tree

   264   def   move_down(calcid: scala.math.BigInt, pos: Position): XML.Tree =

   265   { XML.Elem(Markup("CALCITERATOR", Nil), List(

   266       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   267       DataTypes.xml_of_Position(pos)))

   268   }

   269   //fun moveLevelDown : calcID -> pos' -> XML.tree

   270   def   move_levdn(calcid: scala.math.BigInt, pos: Position): XML.Tree =

   271   { XML.Elem(Markup("CALCITERATOR", Nil), List(

   272       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   273       DataTypes.xml_of_Position(pos)))

   274   }

   275   //fun moveLevelUp : calcID -> pos' -> XML.tree

   276   def   move_levup(calcid: scala.math.BigInt, pos: Position): XML.Tree =

   277   { XML.Elem(Markup("CALCITERATOR", Nil), List(

   278       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   279       DataTypes.xml_of_Position(pos)))

   280   }

   281   //fun moveRoot : calcID -> XML.tree

   282   def   move_root(calcid: scala.math.BigInt): XML.Tree =

   283   { XML.Elem(Markup("CALCITERATOR", Nil), List(

   284       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString())))))

   285   }

   286   //fun moveUp : calcID -> pos' -> XML.tree

   287   def   move_up(calcid: scala.math.BigInt, pos: Position): XML.Tree =

   288   { XML.Elem(Markup("CALCITERATOR", Nil), List(

   289       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   290       DataTypes.xml_of_Position(pos)))

   291   }

   293   //fun refFormula : calcID -> pos' -> XML.tree

   294   //def ref_formula(calcid: scala.math.BigInt, pos: ICalcIterator

   295   def   ref_formula(calcid: scala.math.BigInt, pos: Position): XML.Tree =

   296   { XML.Elem(Markup("REFFORMULA", Nil), List(

   297       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   298       DataTypes.xml_of_Position(pos)))

   299   }

   301   //fun refineProblem : calcID -> pos' -> guh -> XML.tree

   302   def   refine_pbl(calcid: scala.math.BigInt, from: Position, kestore_key: String): XML.Tree =

   303   { XML.Elem(Markup("CONTEXTPBL", Nil), List(

   304       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   305       DataTypes.xml_of_Position(from),

   306       XML.Elem(Markup("GUH", Nil), List(XML.Text(kestore_key)))))

   307   }

   309   //fun replaceFormula : calcID -> cterm' -> XML.tree

   310   def replace_form(calcid: scala.math.BigInt, form: String): XML.Tree =

   311   { XML.Elem(Markup("REPLACEFORMULA", Nil), List(

   312       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   313       DataTypes.xml_of_Formula(form)))

   314   }

   316   //fun requestFillformula : calcID -> errpatID * fillpatID -> XML.tree

   317   //...ONLY IMPLEMENTED IN Math_Engine

   319   //fun resetCalcHead : calcID -> XML.tree

   320   def reset_calchead(calcid: scala.math.BigInt): XML.Tree =

   321   { XML.Elem(Markup("MODIFYCALCHEAD", Nil), List(

   322       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString())))))

   323   }

   325   //fun setContext : calcID -> pos' -> guh -> XML.tree

   326   def   set_ctxt(calcid: scala.math.BigInt, pos: Position, kestore_key: String): XML.Tree =

   327   { XML.Elem(Markup("CONTEXT", Nil), List(

   328       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   329       DataTypes.xml_of_Position(pos),

   330       XML.Elem(Markup("GUH", Nil), List(XML.Text(kestore_key)))))

   331   }

   333   //fun setMethod : calcID -> metID -> XML.tree

   334   //======= TODO ============ metID =============================================

   335 //  def   set_met(calcid: scala.math.BigInt, kestore_key: String): XML.Tree =

   336 //  { XML.Elem(Markup("CONTEXT", Nil), List(

   337 //      XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   338 //      DataTypes.xml_of_Position(pos),

   339 //      XML.Elem(Markup("GUH", Nil), List(XML.Text(kestore_key)))))

   340 //  }

   342   //fun setNextTactic : calcID -> tac -> XML.tree

   343   def   set_next_tac(calcid: scala.math.BigInt, tac: Tactic): XML.Tree =

   344   { XML.Elem(Markup("CONTEXT", Nil), List(

   345       XML.Elem(Markup("CALCID", Nil), List(XML.Text(calcid.toString()))),

   346       DataTypesCompanion.xml_of_Tactic(tac)))

   347   }

   348   //======= TODO ================ tac ===========================================

   350   //fun setProblem : calcID -> pblID -> XML.tree

   351   //======= TODO ============= pblID =============================================

   352   //fun setTheory : calcID -> thyID -> XML.tree

   353   //======= GOON TODO ================================================================

   356 }

author	Walther Neuper <wneuper@ist.tugraz.at>
	Sun, 16 Aug 2015 15:14:31 +0200
changeset 4773	086b1413d0ae
parent 4771	3ed5dc655f8e
child 4779	67cd32a43ec2
permissions	-rw-r--r--