(* 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  pbl2xml ["Biegelinien"] (get_pbt ["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> Method</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_} = get_pbt ["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:filepath) = (path ^ "pbl/");

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

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

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

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

val po' = lev_on po;

wfn (*= pbl2file*)

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

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

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

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

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

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

  (id, pbl);

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

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

  "Problem (Pure', [e_pblID])"

then () else error "fun pbl2term changed";

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

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

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

(*see WN120405a.TODO.txt*)

if UnparseC.term (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, ...} = get_met ["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 ---^^*)