(* Title:  $ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML

   Author: Walther Neuper 1505

   (c) copyright due to lincense terms.

*)

"------------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"------------------------------------------------------------------------------------------------";

"----------- test example for migration \"isabelle tty \" --> libisabelle -----------------------";

"------------------------------------------------------------------------------------------------";

"------------------------------------------------------------------------------------------------";

"----------- test example for migration \"isabelle tty \" --> libisabelle -----------------------";

"----------- test example for migration \"isabelle tty \" --> libisabelle -----------------------";

"----------- test example for migration \"isabelle tty \" --> libisabelle -----------------------";

"see https://github.com/wneuper/libisabelle/blob/master/doc/test--isac-Java--isac-kernel.txt";

(* see ~/proto4/libisabelle/doc/test--isac-jav--isac-kernel.txt *)

(*------- step 1 -----------------------------------------------------

#I: Formalization

    isac-java/src/java/isac/util/Formalization.java

#O: int

ML {* CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))]; * }

*)

val calcid = 111

val result =

  XML.Elem (("CALCTREE", []), [

    XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)])]);

xmlstr 0 result = "<CALCTREE>\n  <CALCID>\n    111\n  </CALCID>\n</CALCTREE>";

writeln (xmlstr 0 result);

(*------- step 2 -----------------------------------------------------

#I: int

#O: (int, int)

ML {* Iterator 1; * }

*)

val userid = 222

val result =

  XML.Elem (("ADDUSER", []), [

    XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),

      XML.Elem (("USERID", []), [XML.Text (string_of_int userid)])]);

xmlstr 0 result = "<ADDUSER>\n  <CALCID>\n    111\n  </CALCID>\n  <USERID>\n    222\n  </USERID>\n</ADDUSER>\n";

writeln (xmlstr 0 result);

(*------- step 3 -----------------------------------------------------

#I: int

#O: (int, ICalcIterator)

    isac-java/src/java/isac/interfaces/ICalcIterator.java

ML {* moveActiveRoot 1; * }

*)

val pos as (is, kind) = ([], "Pbl")

val result =

  XML.Elem (("CALCITERATOR", []), [

    XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),

    XML.Elem (("POSITION", []), [

      XML.Elem (("INTLIST", []), is),

        XML.Elem (("POS", []), [XML.Text kind])])]);

xmlstr 0 result = "<CALCITERATOR>\n  <CALCID>\n    111\n  </CALCID>\n  <POSITION>\n    <INTLIST>\n    </INTLIST>\n    <POS>\n      Pbl\n    </POS>\n  </POSITION>\n</CALCITERATOR>\n";

writeln (xmlstr 0 result);

(*------- step 4 -----------------------------------------------------

#I: (int, ICalcIterator, ICalcIterator, int, string)

#O: (int, FormHeadsContainer)

    isac-java/src/java/isac/util/formulae/FormHeadsContainer.java, is a list of ...

    isac-java/src/java/isac/util/formulae/CalcFormula.java         and ...

    isac-java/src/java/isac/util/formulae/CalcHead.java

ML {* getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false; * }

*)

val pos as (is, kind) = ([], "Pbl")

val calcformula as (pos, formula) = (pos, "solve (x + 1 = 2, x)")

val formheads = [calcformula (*, calchead .. see below*)]

val result =

  XML.Elem (("GETELEMENTSFROMTO", []), [

    XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),

    XML.Elem (("FORMHEADS", []), [

      XML.Elem (("CALCFORMULA", []),  [

        XML.Elem (("POSITION", []), [

          XML.Elem (("INTLIST", []), is),

          XML.Elem (("POS", []), [XML.Text kind])]),

        XML.Elem (("FORMULA", []), [

          XML.Elem (("MATHML", []), [

            XML.Elem (("ISA", []), [XML.Text formula])])])])])]);

xmlstr 0 result = "<GETELEMENTSFROMTO>\n  <CALCID>\n    111\n  </CALCID>\n  <FORMHEADS>\n    <CALCFORMULA>\n      <POSITION>\n        <INTLIST>\n        </INTLIST>\n        <POS>\n          Pbl\n        </POS>\n      </POSITION>\n      <FORMULA>\n        <MATHML>\n          <ISA>\n            solve (x + 1 = 2, x)\n          </ISA>\n        </MATHML>\n      </FORMULA>\n    </CALCFORMULA>\n  </FORMHEADS>\n</GETELEMENTSFROMTO>\n";

writeln (xmlstr 0 result);

(*------- step 5 -----------------------------------------------------

ML {* refFormula 1 ([],Pbl); * }

  ------- step 6 -----------------------------------------------------

#I: (int, ICalcIterator)

#O: (int, CalcHead)

    isac-java/src/java/isac/util/formulae/CalcHead.java

ML {* refFormula 1 ([],Pbl); * }

*)

val head = "solve (x + 1 = 2, x)"

val given = [] : ((string * string) * string) list

val item as (attr, form) = (("status", "false"), "precond_rootpbl v_v")

val where_ as items = [item]

val find = [] : ((string * string) * string) list

val relate = [] : ((string * string) * string) list

val model = (given, where_, find, relate)

val belongsto = "Pbl"

val specification as (theoryid, problemid, methodid) = (["e_domID"], ["e_pblID"], ["e_metID"])

val calchead = (("status", "incorrect"), (pos, head, model, belongsto, specification))

val result =

  XML.Elem (("REFFORMULA", []), [

    XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),

    XML.Elem (("CALCHEAD", [("status", "\"incorrect\"")]), [

      XML.Elem (("POSITION", []), [

        XML.Elem (("INTLIST", []), is),

        XML.Elem (("POS", []), [XML.Text kind])]),

      XML.Elem (("HEAD", []), [

        XML.Elem (("MATHML", []), [

          XML.Elem (("ISA", []), [XML.Text formula])])]),

      XML.Elem (("MODEL", []), [

        XML.Elem (("GIVEN", []), []),

        XML.Elem (("WHERE", []), [

          XML.Elem (("ITEM", [("status", "\"false\"")]), [

            XML.Elem (("MATHML", []), [

              XML.Elem (("ISA", []), [XML.Text "precond_rootpbl v_v"])])])]),

        XML.Elem (("FIND", []), []),

        XML.Elem (("RELATE", []), [])]),

      XML.Elem (("BELONGSTO", []), [XML.Text "Pbl"]),

      XML.Elem (("SPECIFICATION", []), [

        XML.Elem (("THEORYID", []), [XML.Text "e_domID"]),

        XML.Elem (("PROBLEMID", []), [

          XML.Elem (("STRINGLIST", []), [

            XML.Elem (("STRING", []), [XML.Text "e_pblID"])])]),

        XML.Elem (("METHODID", []), [

          XML.Elem (("STRINGLIST", []), [

            XML.Elem (("STRING", []), [XML.Text "e_metID"])])])])])]);

xmlstr 0 result = "<REFFORMULA>\n  <CALCID>\n    111\n  </CALCID>\n  <CALCHEAD status \"incorrect\">\n    <POSITION>\n      <INTLIST>\n      </INTLIST>\n      <POS>\n        Pbl\n      </POS>\n    </POSITION>\n    <HEAD>\n      <MATHML>\n        <ISA>\n          solve (x + 1 = 2, x)\n        </ISA>\n      </MATHML>\n    </HEAD>\n    <MODEL>\n      <GIVEN>\n      </GIVEN>\n      <WHERE>\n        <ITEM status \"false\">\n          <MATHML>\n            <ISA>\n              precond_rootpbl v_v\n            </ISA>\n          </MATHML>\n        </ITEM>\n      </WHERE>\n      <FIND>\n      </FIND>\n      <RELATE>\n      </RELATE>\n    </MODEL>\n    <BELONGSTO>\n      Pbl\n    </BELONGSTO>\n    <SPECIFICATION>\n      <THEORYID>\n        e_domID\n      </THEORYID>\n      <PROBLEMID>\n        <STRINGLIST>\n          <STRING>\n            e_pblID\n          </STRING>\n        </STRINGLIST>\n      </PROBLEMID>\n      <METHODID>\n        <STRINGLIST>\n          <STRING>\n            e_metID\n          </STRING>\n        </STRINGLIST>\n      </METHODID>\n    </SPECIFICATION>\n ...";

writeln (xmlstr 0 result);

(*------- step 7 -----------------------------------------------------

#I: (int, string)

#O: (int, CalcChanged)

	isac-java/src/java/isac/util/CalcChanged.java

 ML {* autoCalculate 1 CompleteCalc; * }

*)

val pos as (is, kind) = ([], "Pbl")

val result =

  XML.Elem (("AUTOCALC", []), [

    XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),

    XML.Elem (("CALCCHANGED", []),  [

      XML.Elem (("UNCHANGED", []), [

        XML.Elem (("INTLIST", []), is),

        XML.Elem (("POS", []), [XML.Text kind])]),

      XML.Elem (("DELETED", []), [

        XML.Elem (("INTLIST", []), is),

        XML.Elem (("POS", []), [XML.Text kind])]),

     XML.Elem (("GENERATED", []), [

        XML.Elem (("INTLIST", []), is),

        XML.Elem (("POS", []), [XML.Text "Res"])])])]);

xmlstr 0 result = "<AUTOCALC>\n  <CALCID>\n    111\n  </CALCID>\n  <CALCCHANGED>\n    <UNCHANGED>\n      <INTLIST>\n      </INTLIST>\n      <POS>\n        Pbl\n      </POS>\n    </UNCHANGED>\n    <DELETED>\n      <INTLIST>\n      </INTLIST>\n      <POS>\n        Pbl\n      </POS>\n    </DELETED>\n    <GENERATED>\n      <INTLIST>\n      </INTLIST>\n      <POS>\n        Res\n      </POS>\n    </GENERATED>\n  </CALCCHANGED>\n</AUTOCALC>\n";

writeln (xmlstr 0 result);

(*------- step 8 -----------------------------------------------------

ML {* getFormulaeFromTo 1 ([],Pbl) ([],Res) 0 false; * }

  ------- step 9 -----------------------------------------------------

ML {* getFormulaeFromTo 1 ([],Pbl) ([],Res) 0 false; * }

  ------- step 10 -----------------------------------------------------

#I: (int, ICalcIterator)

#O: (int, CalcFormula)

ML {* refFormula 1 ([],Res); * }

*)

val pos as (is, kind) = ([], "Res")

val calcformula as (pos, formula) = (pos, "[x = 1]")

val formheads = [calcformula (*, calchead .. see below*)]

val result =

  XML.Elem (("REFFORMULA", []), [

    XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),

    XML.Elem (("CALCFORMULA", []),  [

      XML.Elem (("POSITION", []), [

        XML.Elem (("INTLIST", []), is),

        XML.Elem (("POS", []), [XML.Text kind])]),

      XML.Elem (("FORMULA", []), [

        XML.Elem (("MATHML", []), [

          XML.Elem (("ISA", []), [XML.Text formula])])])])]);

xmlstr 0 result = "<REFFORMULA>\n  <CALCID>\n    111\n  </CALCID>\n  <CALCFORMULA>\n    <POSITION>\n      <INTLIST>\n      </INTLIST>\n      <POS>\n        Res\n      </POS>\n    </POSITION>\n    <FORMULA>\n      <MATHML>\n        <ISA>\n          [x = 1]\n        </ISA>\n      </MATHML>\n    </FORMULA>\n  </CALCFORMULA>\n</REFFORMULA>\n";

writeln (xmlstr 0 result);

(*------- step 11 -----------------------------------------------------

ML {* refFormula 1 ([],Res); * }

  ------- step 12 -----------------------------------------------------

ML {* refFormula 1 ([],Res); * }

  ------- step 13 -----------------------------------------------------

#I: int

#O: int

ML {* DEconstrCalcTree 1; * }

*)

val result =

  XML.Elem (("DELCALC", []), [

    XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)])]);

xmlstr 0 result = "<CALCTREE>\n  <CALCID>\n    111\n  </CALCID>\n</CALCTREE>";

writeln (xmlstr 0 result);