(* Title:  tests for libisabelle/libisabelle/src/main/isabelle/Protocol/Protocol.thy

   Author: Walther Neuper 2015

   (c) due to copyright terms

theory Test_Some imports Build_Thydata begin 

ML {* KEStore_Elems.set_ref_thy @{theory};

  fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*) *}

ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"

*)

(* NOTE: Protocol.thy still belongs to a different development at

     https://github.com/wneuper/libisabelle

but Protocol.thy is enclosed in isabisac for testing synchronisation, 

see Build_Isac.thy *)

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

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

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

"----------- fun initContext, fun initcontext_pbl, fun initcontext_met -------";

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

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

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

"----------- fun initContext, fun initcontext_pbl, fun initcontext_met -------";

"----------- fun initContext, fun initcontext_pbl, fun initcontext_met -------";

"----------- fun initContext initcontext_pbl initcontext_met -----------------";

(* compare isac-java/src/java-tests/isac/bridge/TestContext#testContext *)

reset_states ();

CalcTree [(["equality (x + 1 = (2::real))", "solveFor x", "solutions L"],

  ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

(*-->ISA: initContext 1 Thy_ ([1],Frm);  *)

val out = initContext 1 Thy_ ([1],Frm);

if cut_xml out 105 = 

"(CONTEXTTHY)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . thy_isac_Test-rls-norm_equation"

then () else error "initContext 1 Thy_ ([1],Frm); CHANGED";

(*-->ISA: initContext 1 Thy_ ([1],Res);  *)

val out = initContext 1 Thy_ ([1],Res);

if cut_xml out 105 = 

"(CONTEXTTHY)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . thy_isac_Test-rls-Test_simplify"

then () else error "initContext 1 Thy_ ([1],Res); CHANGED";

val ((pt, _), _) = get_calc 1;

(*-->ISA: initContext 1 Pbl_ ([1],Res);  *)

val (p, p_) = ([1], Res)

val pp = par_pblobj pt p

val chd = initcontext_pbl pt (pp,p_)

val out = contextpblOK2xml 1 chd;

if cut_xml out 100 = "(CONTEXTPBL)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . pbl_test_uni_roottest\n. . "

then () else error "initContext 1 Pbl_ ([1],Res); CHANGED";

(*-->ISA: initContext 1 Pbl_ ([3,1],Res); *)

val (p, p_) = ([3, 1], Res)

val pp = par_pblobj pt p

val chd = initcontext_pbl pt (pp,p_)

val out = contextpblOK2xml 1 chd;

if cut_xml out 90 = 

"(CONTEXTPBL)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . pbl_test_uni_lin"

then () else error "initContext 1 Pbl_ ([3,1],Res); CHANGED";

(*-->ISA: initContext 1 Met_ ([1],Res); *)

val (p, p_) = ([1], Res)

(*interface.sml*)val pp = par_pblobj pt p

(*interface.sml*)val chd = initcontext_met pt (pp, p_);

val out = contextmetOK2xml 1 chd; (*ERROR was pblID2guh: not for '[Test,squ-equ-test-subpbl1]'*)

"~~~~~ fun contextmetOK2xml, args:"; val (calcid, contmet) = (1, chd);

"~~~~~ fun xml_of_matchmet, args:"; val (model_ok, pI, scr, pbl, pre) = (contmet);

if metID2guh pI = 

"met_test_squ_sub" then () else error "xml_of_matchmet CHANGED";

if cut_xml out 90 = "(CONTEXTMET)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . met_test_squ_sub"

then () else error "initContext 1 Met_ ([1],Res); CHANGED";

(*-->ISA: initContext 1 Met_ ([3,1],Res); *)

val (p, p_) = ([3,1],Res)

(*interface.sml*)val pp = par_pblobj pt p

(*interface.sml*)val chd = initcontext_met pt (pp, p_);

val out = contextmetOK2xml 1 chd;

if cut_xml out 91 = "(CONTEXTMET)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . met_test_solvelin"

then () else error "initContext 1 Met_ ([3,1],Res); CHANGED";

"~~~~~ fun operation_setup init_ctxt, args:"; val (intree) = 

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

    XML.Elem (("CALCID", []), [XML.Text "1"]),

    XML.Elem (("KETYPE", []), [XML.Text "met"]),

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

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

        XML.Elem (("INT", []), [XML.Text "3"]),

        XML.Elem (("INT", []), [XML.Text "1"])]),

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

fun xxxxx () = (fn intree => 

	 ((let 

	   val (ci, ketype, pos) = case intree of

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

         XML.Elem (("CALCID", []), [XML.Text ci]),

         ketype as XML.Elem (("KETYPE", []), _),

         pos as XML.Elem (("POSITION", []), _)]) 

     => (str2int ci, xml_to_ketype ketype, xml_to_pos pos)

     | tree => raise ERROR ("init_ctxt: WRONG intree = " ^ xmlstr 0 tree)

     val result = Math_Engine.initContext ci ketype pos

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)

	   handle _  => sysERROR2xml 4711 "Protocol.operation_setup init_ctxt UNKNOWN exn")

val out = xxxxx () intree;

if cut_xml out 91 = "(CONTEXTMET)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . met_test_solvelin"

then () else error "operation_setup initContext 1 Met_ ([3,1],Res); CHANGED";