(* Title: tests for sml/xmlsrc/pbl-met-hierarchy.sml

    Author: Walther Neuper 060209

    (c) isac-team 2006

 use"../smltest/xmlsrc/pbl-met-hierarchy.sml";

 use"pbl-met-hierarchy.sml";

 CAUTION with testing *2file functions -- they are actually writing !!!

 *)

 val thy = @{theory "Isac_Knowledge"};

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

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

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

 "----- pbl2xml ---------------------------------------------------";

 "----- ERROR Illegal reference to internal variable: 'Pure_' -----";

 "----- fun pbl2term ----------------------------------------------";

 "----- fun insert_errpats ----------------------------------------";

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

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

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

 "----- pbl2xml ---------------------------------------------------";

 "----- pbl2xml ---------------------------------------------------";

 "----- pbl2xml ---------------------------------------------------";

 (*what to do if from 'pbls2file "../../xmldata/pbl/";' you get the error

 ### pbl2file: id = ["Biegelinie"]

 *** Type unification failed: Clash of types "fun" and "Program.ID".

 *** Type error in application: Incompatible operand type.

 ***

 *** Operator:  Problem :: ID * ID list => ??'a

 *** Operand:   (Biegelinie, [Biegelinie]) ::

 ***   ((real => real) => una) * ((real => real) => una) list

 ***

 Exception- OPTION raised

 *)

 if  Pbl_Met_Hierarchy.pbl2xml ["Biegelinien"] (Problem.from_store ["Biegelinien"]) =

   "<NODECONTENT>\n"^

   "  <GUH> pbl_bieg </GUH>\n"^

   "  <STRINGLIST>\n"^

   "    <STRING> Biegelinien </STRING>\n"^

   "  </STRINGLIST>\n  <META> </META>\n"^

   "  <HEADLINE>\n"^

   "    <MATHML>\n"^

   "      <ISA> Problem (Biegelinie', [Biegelinien]) </ISA>\n"^

   "    </MATHML>\n"^

   "  </HEADLINE>\n"^

   "  <GIVEN>\n"^

   "    <MATHML>\n"^

   "      <ISA> Traegerlaenge l_l </ISA>\n"^

   "    </MATHML>\n"^

   "    <MATHML>\n"^

   "      <ISA> Streckenlast q_q </ISA>\n"^

   "    </MATHML>  </GIVEN>\n  <WHERE>  </WHERE>\n"^

   "  <FIND>\n"^

   "    <MATHML>\n"^

   "      <ISA> Biegelinie b_b </ISA>\n"^

   "    </MATHML>  </FIND>\n"^

   "  <RELATE>\n"^

   "    <MATHML>\n"^

   "      <ISA> Randbedingungen r_b </ISA>\n"^

   "    </MATHML>  </RELATE>\n"^

   "  <EXPLANATIONS> </EXPLANATIONS>\n"^

   "  <THEORY>\n"^

   "    <KESTOREREF>\n"^

   "      <TAG> Theorem </TAG>\n"^

   "      <ID>  </ID>\n"^

   "      <GUH> thy_isac_Biegelinie-thm- </GUH>\n"^

   "    </KESTOREREF>\n"^

   "  </THEORY>\n"^

   "  <METHODS>\n"^

   "    <KESTOREREF>\n"^

   "      <TAG> MethodC</TAG>\n"^

   "      <ID> [IntegrierenUndKonstanteBestimmen2] </ID>\n"^

   "      <GUH> met_biege_2 </GUH>\n"^

   "    </KESTOREREF>\n"^

   "  </METHODS>\n"^

   "  <EVALPRECOND> empty </EVALPRECOND>\n"^

   "  <MATHAUTHORS>\n"^

   "  </MATHAUTHORS>\n"^

   "  <COURSEDESIGNS>\n"^

   "    <STRING> isac team 2006 </STRING>\n"^

   "  </COURSEDESIGNS>\n"^

   "</NODECONTENT>"

 then () else error "fun pbl2xml 'Biegelinien' changed";

 (* val id = ["Biegelinie"];

    val {(*guh,*)cas,met,ppc,prls,thy,where_} = Problem.from_store ["Biegelinie"];

    AND STEP THROUGH pbl2xml ...

    term2xml i (pbl2term thy id);

    pbl2term thy id;

   *)

 (* val (thy, pblRD) = (thy, id);

    AND STEP THROUGH pbl2term...

    val str = ("Problem (" ^ 

 	   (get_thy o theory2domID) thy ^ ", " ^

 	   (strs2str' o rev) pblRD ^ ")");

   str2term str;

   str2term "Biegelinie";

   str2term "Biegelinien";

   *)

 (*Const

       ("Biegelinie.Biegelinie",

        "("Real.real => "Real.real) => Tools.una") : Term.term

 ..I.E. THE "Program.ID" _WAS_ ALREADY OCCUPIED BY A 'description'*)

 "----- ERROR Illegal reference to internal variable: 'Pure_' -----";

 "----- ERROR Illegal reference to internal variable: 'Pure_' -----";

 "----- ERROR Illegal reference to internal variable: 'Pure_' -----";

 val path = "/tmp/"; 

 "~~~~~ fun pbls2file, args:"; val (p: Pbl_Met_Hierarchy.filepath) = (path ^ "pbl/");

 get_ptyps (); (*not = []*)

 "~~~~~ fun nodes, args:"; val (pa, ids, po, wfn, (n::ns)) =

   (p, []: string list, [0], Pbl_Met_Hierarchy.pbl2file, (get_ptyps ()));

 "~~~~~ fun node, args:"; val (pa: Pbl_Met_Hierarchy.filepath, ids, po, wfn, Store.Node (id,[n],ns)) = (pa, ids, po, wfn, n);

 val po' = lev_on po;

 wfn (*= pbl2file*)

 "~~~~~ fun pbl2file, args:"; val ((path:Pbl_Met_Hierarchy.filepath), (pos:pos), (id: MethodC.id), (pbl as {guh,...})) =

   (pa, po', (ids@[id]), n);

 strs2str id = "[\"e_pblID\"]"; (*true*)

 pos2str pos = "[1]"; (*true*)

 path ^ Thy_Present.guh2filename guh = "/tmp/pbl/pbl_empty.xml"; (*true*)

 "~~~~~ fun pbl2xml, args:"; val (id: Problem.id, {guh,mathauthors,init,cas,met,ppc,prls,thy,where_}) =

   (id, pbl);

 "~~~~~ fun pbl2term, args:"; val (thy, (pblRD:Problem.id_reverse)) = (thy, id);

 if ("Problem (" ^  Context.theory_name thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")") =

   "Problem (Pure', [empty_probl_id])"

 then () else error "fun pbl2term changed";

 "----- fun pbl2term ----------------------------------------------";

 "----- fun pbl2term ----------------------------------------------";

 "----- fun pbl2term ----------------------------------------------";

 (*see WN120405a.TODO.txt*)

 if UnparseC.term (Pbl_Met_Hierarchy.pbl2term (ThyC.get_theory "Isac_Knowledge") ["equations", "univariate", "normalise"]) =

   "Problem (Isac_Knowledge', [normalise, univariate, equations])"

 then () else error "fun pbl2term changed";

 "----- fun insert_errpats ----------------------------------------";

 "----- fun insert_errpats ----------------------------------------";

 "----- fun insert_errpats ----------------------------------------";

 (* vv--- here intermediate save/restore does not work and affects other tests ---vv

          see test/../calcelems.sml --- Unsynchronized.ref doesn't work any more ---

 val errpatstest =

   [("chain-rule-diff-both",

     [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",

      parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",

      parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",

      parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",

      parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],

     [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, 

      @{thm diff_ln_chain}, @{thm  diff_exp_chain}])];

 insert_errpats ["diff", "differentiate_on_R"] errpatstest;

 val {errpats, ...} = MethodC.from_store ["diff", "differentiate_on_R"];

 case errpats of

   ("chain-rule-diff-both", _, _) :: _ => ()

 | _ => error "insert_errpats chain-rule-diff-both changed";

 ^^^^^--- here intermediate save/restore does not work and affects other tests ---^^*)