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;
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._
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.
38 /* from isabisac/src/Tools/Frontend/interface.sml
39 signature MATH_ENGINE =
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
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)))
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".
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)))))
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())))))
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)))))
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)))
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())))))
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)))
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())))))
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)))
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)))))
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)))
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) ))
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)))
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)))
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())))))
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())))))
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)))
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())))))
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())))))
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())))))
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())))))
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)))
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)))
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)))
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)))
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())))))
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)))
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)))
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)))))
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)))
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())))))
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)))))
333 //fun setMethod : calcID -> metID -> XML.tree
334 //======= TODO ============ metID =============================================
335 // def set_met(calcid: scala.math.BigInt, met_key: java.util.Vector[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(met_key))) ))
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)))
348 //======= TODO ================ tac ===========================================
350 //fun setProblem : calcID -> pblID -> XML.tree
351 //======= TODO ============= pblID =============================================
352 //fun setTheory : calcID -> thyID -> XML.tree
353 //======= GOON TODO ================================================================