1.1 --- a/isac-java/src/java/isac/bridge/xml/DataTypes.scala Sun Aug 09 06:51:36 2015 +0200
1.2 +++ b/isac-java/src/java/isac/bridge/xml/DataTypes.scala Sun Aug 09 07:21:24 2015 +0200
1.3 @@ -11,10 +11,18 @@
1.4
1.5 package isac.bridge.xml
1.6
1.7 +import isac.bridge.CChanged
1.8 +import isac.util.Formalization
1.9 +import isac.util.formulae.CalcFormula
1.10 +import isac.util.formulae.CalcHead
1.11 +import isac.util.formulae.CalcHeadSimpleID
1.12 +import isac.util.formulae.Formula
1.13 +import isac.util.formulae.HierarchyKey
1.14 +import isac.util.formulae.ModelItem
1.15 +import isac.util.formulae.ModelItemList
1.16 +import isac.util.formulae.Model
1.17 import isac.util.formulae.Position
1.18 -import isac.util.Formalization
1.19 import isac.util.formulae.Specification
1.20 -import isac.bridge.CChanged
1.21
1.22 import isabelle.XML
1.23 import isabelle.Markup
1.24 @@ -30,7 +38,9 @@
1.25 */
1.26 object DataTypes {
1.27
1.28 - /** auxiliary methods */
1.29 + /**
1.30 + * auxiliary methods, both directions
1.31 + **/
1.32
1.33 def xml_of_int (i: scala.math.BigInt): XML.Tree = {
1.34 XML.Elem(Markup("INT", Nil), List(XML.Text(i.toString())))
1.35 @@ -57,12 +67,16 @@
1.36 case _ => throw new IllegalArgumentException("xml_to_pos exn")
1.37 }
1.38 def xml_to_VectorString (t: XML.Tree): Vector[java.lang.String] = t match {
1.39 - case XML.Elem(Markup("STRINGLIST", Nil), ss) => {
1.40 + case XML.Elem(Markup("STRINGLIST", Nil), is) => {
1.41 val v = new java.util.Vector[java.lang.String];
1.42 - ss.foreach { case (XML.Elem(Markup("STRING", Nil), List(XML.Text(str)))) => v.add(str) }
1.43 + is.foreach {
1.44 + case (XML.Elem(Markup("STRING", Nil), List(XML.Text(str))))
1.45 + => v.add(str)
1.46 + case _ => throw new IllegalArgumentException("xml_to_VectorString 1 wrong arg: " + t)
1.47 + }
1.48 v
1.49 }
1.50 - case _ => throw new IllegalArgumentException("xml_to_VectorInteger exn")
1.51 + case _ => throw new IllegalArgumentException("xml_to_VectorString 2 wrong arg: " + t)
1.52 }
1.53 // Note: java.int-->scala.BigInt not done here, because "int" is unknown in Scala.
1.54 def Integer_to_BigInt (i: java.lang.Integer): scala.math.BigInt = {
1.55 @@ -97,12 +111,131 @@
1.56 XML.Elem(Markup("THEORYID", Nil), List(XML.Text(thy))),
1.57 XML.Elem(Markup("PROBLEMID", Nil), List(pbl)),
1.58 XML.Elem(Markup("METHODID", Nil), List(met)))) =>
1.59 - (thy, DataTypes.xml_to_strs(pbl), DataTypes.xml_to_strs(met))
1.60 + (thy, DataTypes.xml_to_strs(pbl), xml_to_strs(met))
1.61 case _ => throw new IllegalArgumentException("xml_to_spec exn")
1.62 }
1.63 + def xml_to_VectorInteger (t: XML.Tree): Vector[java.lang.Integer] = t match {
1.64 + case XML.Elem(Markup("INTLIST", Nil), is) => {
1.65 + val v = new java.util.Vector[java.lang.Integer];
1.66 + is.foreach {
1.67 + case (XML.Elem(Markup("INT", Nil), List(XML.Text(i))))
1.68 + => v.add(new java.lang.Integer(i))
1.69 + case _ => throw new IllegalArgumentException("xml_to_VectorInteger 1 wrong arg: " + t)
1.70 + }
1.71 + v
1.72 + }
1.73 + case _ => throw new IllegalArgumentException("xml_to_VectorInteger 2 wrong arg: " + t)
1.74 + }
1.75 + def sListToVectorCalcFormula (forms: List[CalcFormula]): Vector[CalcFormula] = {
1.76 + val v = new java.util.Vector[CalcFormula];
1.77 + forms.foreach { form => v.add(form) }
1.78 + v
1.79 + }
1.80 + def xml_to_String (t: XML.Tree): java.lang.String = t match {
1.81 + case XML.Text(str) => str
1.82 + }
1.83
1.84 - /** conversion XML <--> Java-objects in isac-java used by libisabelle */
1.85 + /**
1.86 + * conversion XML <--> Java-objects in isac-java used by libisabelle
1.87 + **/
1.88
1.89 + def xml_to_ModelItem(t: XML.Tree): isac.util.formulae.ModelItem = t match {
1.90 + case
1.91 + XML.Elem(Markup("ITEM", List(("status", status))), List(
1.92 + XML.Elem(Markup("MATHML", Nil), List(
1.93 + XML.Elem(Markup("ISA", Nil), List(XML.Text(form_isa)))))))
1.94 + => new ModelItem(status, form_isa)
1.95 + case _ => throw new IllegalArgumentException("xml_to_ModelItem wrong arg: " + t)
1.96 + }
1.97 + def sList2jVectorModelItem(ilist: List[ModelItem]): Vector[ModelItem] = {
1.98 + val ivect = new Vector[ModelItem]()
1.99 + for (n <- 0 to ilist.size - 1) ivect.add(ilist(n))
1.100 + ivect
1.101 + }
1.102 + //for test on console:
1.103 + def sList2jVector(ilist: List[Integer]): Vector[Integer] = {
1.104 + val ivect = new Vector[Integer]()
1.105 + for (n <- 0 to ilist.size - 1) ivect.add(ilist(n))
1.106 + ivect
1.107 + }
1.108 + def xml_to_VectorModelItem(t: XML.Tree): java.util.Vector[ModelItem] = t match {
1.109 + case
1.110 + XML.Elem(Markup("GIVEN", Nil), list_xml)
1.111 + => sList2jVectorModelItem(list_xml map xml_to_ModelItem)
1.112 + case
1.113 + XML.Elem(Markup("WHERE", Nil), list_xml)
1.114 + => sList2jVectorModelItem(list_xml map xml_to_ModelItem)
1.115 + case
1.116 + XML.Elem(Markup("FIND", Nil), list_xml)
1.117 + => sList2jVectorModelItem(list_xml map xml_to_ModelItem)
1.118 + case
1.119 + XML.Elem(Markup("RELATE", Nil), list_xml)
1.120 + => sList2jVectorModelItem(list_xml map xml_to_ModelItem)
1.121 + case _ => throw new IllegalArgumentException("xml_to_VectorModelItem wrong arg: " + t)
1.122 + }
1.123 + def xml_to_Model(t: XML.Tree): Model = t match {
1.124 + case
1.125 + XML.Elem(Markup("MODEL", Nil), List(xml_given, xml_where, xml_find, xml_relate))
1.126 + => new Model(
1.127 + new ModelItemList(xml_to_VectorModelItem(xml_given)),
1.128 + new ModelItemList(xml_to_VectorModelItem(xml_where)),
1.129 + new ModelItemList(xml_to_VectorModelItem(xml_find)),
1.130 + new ModelItemList(xml_to_VectorModelItem(xml_relate)))
1.131 + case _ => throw new IllegalArgumentException("xml_to_Model wrong arg: " + t)
1.132 + }
1.133 +
1.134 + def xml_to_Specification(t: XML.Tree): isac.util.formulae.Specification = t match {
1.135 + case
1.136 + XML.Elem(Markup("SPECIFICATION", Nil), List(
1.137 + XML.Elem(Markup("THEORYID", Nil), List(xml_thy)),
1.138 + XML.Elem(Markup("PROBLEMID", Nil), List(xml_pbl)),
1.139 + XML.Elem(Markup("METHODID", Nil), List(xml_met))))
1.140 + => { val thy_key = new CalcHeadSimpleID()
1.141 + thy_key.setID(DataTypes.xml_to_String(xml_thy))
1.142 + val pbl_key = new HierarchyKey()
1.143 + pbl_key.setID(DataTypes.xml_to_VectorString(xml_pbl))
1.144 + val met_key = new HierarchyKey()
1.145 + met_key.setID(DataTypes.xml_to_VectorString(xml_met))
1.146 + new Specification(thy_key, pbl_key, met_key)
1.147 + }
1.148 + case _ => throw new IllegalArgumentException("xml_to_Specification wrong arg: " + t)
1.149 + }
1.150 +
1.151 + def xml_to_CalcHead(t: XML.Tree): CalcHead = t match {
1.152 + case
1.153 + XML.Elem(Markup("CALCHEAD", List(("status", status))), List(
1.154 + xml_pos, xml_head, xml_model,
1.155 + XML.Elem(Markup("BELONGSTO", Nil), List(XML.Text(pbl_met))),
1.156 + xml_spec))
1.157 + => {
1.158 + val head_str = DataTypes.xml_to_Formula(xml_head);
1.159 + val head_form = new Formula(); head_form.setText(head_str)
1.160 + new CalcHead(DataTypes.xml_to_Position(xml_pos), head_form, xml_to_Model(xml_model),
1.161 + pbl_met, xml_to_Specification(xml_spec), status)
1.162 + }
1.163 + case _ => throw new IllegalArgumentException("xml_to_CalcHead wrong arg: " + t)
1.164 + }
1.165 + //WN150720 hack: improve ^^^ remove vvv
1.166 + //hack vvv due to inability "CalcFormula(Position pos, Formula form)"
1.167 + def xml_to_Formula(t: XML.Tree): String = t match {
1.168 + case
1.169 + XML.Elem(Markup("FORMULA", Nil), List(
1.170 + XML.Elem(Markup("MATHML", Nil), List(
1.171 + XML.Elem(Markup("ISA", Nil), List(XML.Text(form_isa)))))))
1.172 + => form_isa //WN150720 TAKE new Formula(form_isa)
1.173 + case
1.174 + XML.Elem(Markup("HEAD", Nil), List(
1.175 + XML.Elem(Markup("MATHML", Nil), List(
1.176 + XML.Elem(Markup("ISA", Nil), List(XML.Text(head_isa)))))))
1.177 + => head_isa //WN150720 TAKE new Formula(head_isa)
1.178 + case _ => throw new IllegalArgumentException("xml_to_Formula wrong arg: " + t)
1.179 + }
1.180 + def xml_to_CalcFormula(t: XML.Tree): CalcFormula = t match {
1.181 + case
1.182 + XML.Elem(Markup("CALCFORMULA", Nil), List(pos, form))
1.183 + => new CalcFormula(DataTypes.xml_to_Position(pos), xml_to_Formula(form))
1.184 + case _ => throw new IllegalArgumentException("xml_to_CalcFormula wrong arg: " + t)
1.185 + }
1.186 def xml_of_Formalization(fmz: Formalization): XML.Tree = {
1.187 XML.Elem(Markup("FORMALIZATION", Nil), fmz.getVariants().asScala.toList map xml_of_Variant)
1.188 }
1.189 @@ -110,6 +243,13 @@
1.190 val is: List[Integer] = pos.getIntList().asInstanceOf[Vector[Integer]].asScala.toList
1.191 xml_of_pos(is map Integer_to_BigInt, pos.getKind())
1.192 }
1.193 + def xml_to_Position(t: XML.Tree): Position = t match {
1.194 + case
1.195 + XML.Elem(Markup("POSITION", Nil), List(
1.196 + ints, XML.Elem(Markup("POS", Nil), List(XML.Text(kind)))))
1.197 + => new Position(xml_to_VectorInteger(ints), kind)
1.198 + case _ => throw new IllegalArgumentException("xml_to_Position wrong arg: " + t)
1.199 + }
1.200 def xml_to_Items (t: XML.Tree): Vector[java.lang.String] = t match { //Java <-- XML(Scala)
1.201 case XML.Elem(Markup("GIVEN", Nil), its) => {
1.202 val v = new java.util.Vector[java.lang.String];