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.
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 edu.tum.cs.isabelle.api.XML
23 import java.util.ArrayList
24 import java.util.Vector
25 import java.math.BigInteger
26 import scala.math.BigInt
27 import scala.collection.JavaConverters._
28 import scala.collection.JavaConversions._
31 * Convert arguments of JSystem.invoke(Operations.* to XML;
32 * Conversions use Scala's pattern matching, which is not available in Java.
33 * The sequence in the kernel's signature below is maintained.
37 /* from isabisac/src/Tools/Frontend/interface.sml
38 signature MATH_ENGINE =
40 val appendFormula : calcID -> cterm' -> XML.tree
41 val autoCalculate : calcID -> auto -> XML.tree
42 val applyTactic : calcID -> pos' -> tac -> XML.tree
43 val CalcTree : fmz list -> XML.tree
44 val checkContext : calcID -> pos' -> guh -> XML.tree
45 val DEconstrCalcTree : calcID -> XML.tree
46 val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree
47 val fetchProposedTactic : calcID -> XML.tree
48 val findFillpatterns : calcID -> errpatID -> XML.tree
49 val getAccumulatedAsms : calcID -> pos' -> XML.tree
50 val getActiveFormula : calcID -> XML.tree
51 val getAssumptions : calcID -> pos' -> XML.tree
52 val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree
53 val getTactic : calcID -> pos' -> XML.tree
54 val initContext : calcID -> ketype -> pos' -> XML.tree
55 val inputFillFormula: calcID -> string -> XML.tree
56 val interSteps : calcID -> pos' -> XML.tree
57 val Iterator : calcID -> XML.tree
58 val IteratorTEST : calcID -> iterID
59 val modelProblem : calcID -> XML.tree
60 val modifyCalcHead : calcID -> icalhd -> XML.tree
61 val moveActiveCalcHead : calcID -> XML.tree
62 val moveActiveDown : calcID -> XML.tree
63 val moveActiveFormula : calcID -> pos' -> XML.tree
64 val moveActiveLevelDown : calcID -> XML.tree
65 val moveActiveLevelUp : calcID -> XML.tree
66 val moveActiveRoot : calcID -> XML.tree
67 val moveActiveRootTEST : calcID -> XML.tree
68 val moveActiveUp : calcID -> XML.tree
69 val moveCalcHead : calcID -> pos' -> XML.tree
70 val moveDown : calcID -> pos' -> XML.tree
71 val moveLevelDown : calcID -> pos' -> XML.tree
72 val moveLevelUp : calcID -> pos' -> XML.tree
73 val moveRoot : calcID -> XML.tree
74 val moveUp : calcID -> pos' -> XML.tree
75 val refFormula : calcID -> pos' -> XML.tree
76 val refineProblem : calcID -> pos' -> guh -> XML.tree
77 val replaceFormula : calcID -> cterm' -> XML.tree
78 val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree
79 val resetCalcHead : calcID -> XML.tree
80 val setContext : calcID -> pos' -> guh -> XML.tree
81 val setMethod : calcID -> metID -> XML.tree
82 val setNextTactic : calcID -> tac -> XML.tree
83 val setProblem : calcID -> pblID -> XML.tree
84 val setTheory : calcID -> thyID -> XML.tree
88 //fun appendFormula : calcID -> cterm' -> XML.tree
89 def append_form(calcid: scala.math.BigInt, form: Formula): XML.Tree =
90 { XML.Elem(("APPENDFORMULA", Nil), List(
91 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
92 DataTypes.xml_of_Formula_NEW(form)))
95 //fun autoCalculate : calcID -> auto -> XML.tree
96 def auto_calculate(calcid: scala.math.BigInt, scope: String, steps: scala.math.BigInt): XML.Tree =
97 { //ATTENTION the "if" below is according to "fun xml_to_auto" in datatypes.sml,
98 //but NOT according to "if/else if" in BridgeRMI#autoCalculate for "isabelle tty".
100 XML.Elem(("AUTOCALC", Nil), List(
101 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
102 XML.Elem(("AUTO", Nil), List(XML.Text(scope)))))
105 //xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text i])) = Step (int_of_str i |>the)
106 XML.Elem(("AUTOCALC", Nil), List(
107 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
108 XML.Elem(("AUTO", Nil), List(
109 XML.Elem(("STEP", Nil), List(XML.Text(steps.toString()))) )) ))
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(("CONTEXTTHY", Nil), List(
118 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
119 DataTypes.xml_of_Position(from),
120 XML.Elem(("GUH", Nil), List(XML.Text(kestore_key)))))
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(("APPLICABLETACTICS", Nil), List(
128 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
129 XML.Elem(("INT", Nil), List(XML.Text(scope.toString()))),
130 DataTypes.xml_of_Position(pos)))
133 //fun fetchProposedTactic : calcID -> XML.tree
134 def fetch_proposed_tac(calcid: scala.math.BigInt): XML.Tree =
135 { XML.Elem(("NEXTTAC", Nil), List(
136 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString())))))
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(("GETASSUMPTIONS", Nil), List(
145 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
146 DataTypes.xml_of_Position(pos)))
149 //fun getActiveFormula : calcID -> XML.tree
150 def get_active_form(calcid: scala.math.BigInt): XML.Tree =
151 { XML.Elem(("CALCITERATOR", Nil), List(
152 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString())))))
154 //fun getAssumptions : calcID -> pos' -> XML.tree
155 def get_asms(calcid: scala.math.BigInt, pos: Position): XML.Tree =
156 { XML.Elem(("APPLICABLETACTICS", Nil), List(
157 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
158 DataTypes.xml_of_Position(pos)))
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(("GETFORMULAEFROMTO", Nil), List(
166 XML.Elem(("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(("INT", Nil), List(XML.Text(level.toString()))),
170 XML.Elem(("BOOL", Nil), List(XML.Text(rules.toString)))))
173 //fun getTactic : calcID -> pos' -> XML.tree
174 def get_tac(calcid: scala.math.BigInt, pos: Position): XML.Tree =
175 { XML.Elem(("GETTACTIC", Nil), List(
176 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
177 DataTypes.xml_of_Position(pos)))
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(("INITCONTEXT", Nil), List(
183 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
184 DataTypes.xml_of_ContextType(ketype),
185 DataTypes.xml_of_Position(pos) ))
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(("INTERSTEPS", Nil), List(
194 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
195 DataTypes.xml_of_Position(pos)))
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(("MODIFYCALCHEAD", Nil), List(
204 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
205 DataTypes.xml_of_CalcHead(calchead)))
208 //fun moveActiveCalcHead : calcID -> XML.tree
209 def move_active_calchead(calcid: scala.math.BigInt): XML.Tree =
210 { XML.Elem(("CALCITERATOR", Nil), List(
211 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString())))))
214 // BridgeRMI#moveActiveDown needs Protocol#move_active_down + Protocol#move_down
215 //fun moveActiveDown : calcID -> XML.tree
216 def move_active_down(calcid: scala.math.BigInt): XML.Tree =
217 { XML.Elem(("CALCITERATOR", Nil), List(
218 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString())))))
221 //fun moveActiveFormula : calcID -> pos' -> XML.tree
222 def move_active_form(calcid: scala.math.BigInt, pos: Position): XML.Tree =
223 { XML.Elem(("CALCITERATOR", Nil), List(
224 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
225 DataTypes.xml_of_Position(pos)))
228 //fun moveActiveLevelDown : calcID -> XML.tree
229 def move_active_levdown(calcid: scala.math.BigInt): XML.Tree =
230 { XML.Elem(("CALCITERATOR", Nil), List(
231 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString())))))
234 //fun moveActiveLevelUp : calcID -> XML.tree
235 def move_active_levup(calcid: scala.math.BigInt): XML.Tree =
236 { XML.Elem(("CALCITERATOR", Nil), List(
237 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString())))))
240 //fun moveActiveRoot : calcID -> XML.tree
241 // uses only an BigInt, not an XML.Tree
243 //fun moveActiveRootTEST : calcID -> XML.tree
244 //... only relevant for Isabelle/Isac
246 //fun moveActiveUp : calcID -> XML.tree
247 def move_active_up(calcid: scala.math.BigInt): XML.Tree =
248 { XML.Elem(("CALCITERATOR", Nil), List(
249 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString())))))
252 //fun moveCalcHead : calcID -> pos' -> XML.tree
253 def move_calchead(calcid: scala.math.BigInt, pos: Position): XML.Tree =
254 { XML.Elem(("GETTACTIC"/*shortcut in coding*/, Nil), List(
255 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
256 DataTypes.xml_of_Position(pos)))
259 //fun moveDown : calcID -> pos' -> XML.tree
260 def move_down(calcid: scala.math.BigInt, pos: Position): XML.Tree =
261 { XML.Elem(("CALCITERATOR", Nil), List(
262 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
263 DataTypes.xml_of_Position(pos)))
265 //fun moveLevelDown : calcID -> pos' -> XML.tree
266 def move_levdn(calcid: scala.math.BigInt, pos: Position): XML.Tree =
267 { XML.Elem(("CALCITERATOR", Nil), List(
268 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
269 DataTypes.xml_of_Position(pos)))
271 //fun moveLevelUp : calcID -> pos' -> XML.tree
272 def move_levup(calcid: scala.math.BigInt, pos: Position): XML.Tree =
273 { XML.Elem(("CALCITERATOR", Nil), List(
274 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
275 DataTypes.xml_of_Position(pos)))
277 //fun moveRoot : calcID -> XML.tree
278 def move_root(calcid: scala.math.BigInt): XML.Tree =
279 { XML.Elem(("CALCITERATOR", Nil), List(
280 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString())))))
282 //fun moveUp : calcID -> pos' -> XML.tree
283 def move_up(calcid: scala.math.BigInt, pos: Position): XML.Tree =
284 { XML.Elem(("CALCITERATOR", Nil), List(
285 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
286 DataTypes.xml_of_Position(pos)))
289 //fun refFormula : calcID -> pos' -> XML.tree
290 //def ref_formula(calcid: scala.math.BigInt, pos: ICalcIterator
291 def ref_formula(calcid: scala.math.BigInt, pos: Position): XML.Tree =
292 { XML.Elem(("REFFORMULA", Nil), List(
293 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
294 DataTypes.xml_of_Position(pos)))
297 //fun refineProblem : calcID -> pos' -> guh -> XML.tree
298 def refine_pbl(calcid: scala.math.BigInt, from: Position, kestore_key: String): XML.Tree =
299 { XML.Elem(("CONTEXTPBL", Nil), List(
300 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
301 DataTypes.xml_of_Position(from),
302 XML.Elem(("GUH", Nil), List(XML.Text(kestore_key)))))
305 //fun replaceFormula : calcID -> cterm' -> XML.tree
306 def replace_form(calcid: scala.math.BigInt, form: Formula): XML.Tree =
307 { XML.Elem(("REPLACEFORMULA", Nil), List(
308 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
309 DataTypes.xml_of_Formula_NEW(form)))
312 //fun requestFillformula : calcID -> errpatID * fillpatID -> XML.tree
313 //...ONLY IMPLEMENTED IN Math_Engine
315 //fun resetCalcHead : calcID -> XML.tree
316 def reset_calchead(calcid: scala.math.BigInt): XML.Tree =
317 { XML.Elem(("MODIFYCALCHEAD", Nil), List(
318 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString())))))
321 //fun setContext : calcID -> pos' -> guh -> XML.tree
322 def set_ctxt(calcid: scala.math.BigInt, pos: Position, kestore_key: String): XML.Tree =
323 { XML.Elem(("CONTEXT", Nil), List(
324 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
325 DataTypes.xml_of_Position(pos),
326 XML.Elem(("GUH", Nil), List(XML.Text(kestore_key)))))
329 //fun setMethod : calcID -> metID -> XML.tree
330 def set_met(calcid: scala.math.BigInt, met_key: java.util.Vector[String]): XML.Tree =
331 { XML.Elem(("MODIFYCALCHEAD", Nil), List(
332 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
333 XML.Elem(("METHODID", Nil), List(
334 DataTypes.xml_of_VectorString(met_key)))))
337 //fun setNextTactic : calcID -> tac -> XML.tree
338 def set_next_tac(calcid: scala.math.BigInt, tac: Tactic): XML.Tree =
339 { XML.Elem(("SETNEXTTACTIC", Nil), List(
340 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
341 DataTypesCompanion.xml_of_Tactic(tac)))
344 //fun setProblem : calcID -> pblID -> XML.tree
345 def set_pbl(calcid: scala.math.BigInt, pbl_key: java.util.Vector[String]): XML.Tree =
346 { XML.Elem(("MODIFYCALCHEAD", Nil), List(
347 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
348 XML.Elem(("PROBLEMID", Nil), List(
349 DataTypes.xml_of_VectorString(pbl_key)))))
351 //fun setTheory : calcID -> thyID -> XML.tree
352 def set_thy(calcid: scala.math.BigInt, thy_id: String): XML.Tree =
353 { XML.Elem(("MODIFYCALCHEAD", Nil), List(
354 XML.Elem(("CALCID", Nil), List(XML.Text(calcid.toString()))),
355 XML.Elem(("THEORYID", Nil), List(XML.Text(calcid.toString())))))