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

   Authors: Walther Neuper 060113

   (c) due to copyright terms

CAUTION with testing *2file functions -- they are actually writing to ~/tmp

*)

val thy = @{theory "Isac"};

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

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

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

"----------- assoc_rls -------------------------------------------";

"----------- thm_hier --------------------------------------------";

"----------- fun thydata2xml -------------------------------------";

"----------- write xml to tmp ------------------------------------";

"----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";

"----------- ### thes2file ... Exception- Match raised -----------";

"----------- thes2file: thy_containing_rls : rls '...' not in ! --";

"----------- fun store_thm ---------------------------------------";

"----------- fun insert_fillpats ---------------------------------";

"----------- fun insert_errpatIDs --------------------------------";

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

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

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

"----------- assoc_rls -------------------------------------------";

"----------- assoc_rls -------------------------------------------";

"----------- assoc_rls -------------------------------------------";

val al = [(1,11),(2,22),(3,33)];

overwrite (al, (2,2222));

(*val it = [(1, 11), (2, 2222), (3, 33)] : (int * int) list*)

val al = [("e_rls",("Atools",e_rls)),("e_rrls",("Atools",e_rrls))];

val bl = [("e_rls",e_rls),("e_rrls",e_rrls)];

val b = ("e_rls",("Atools",e_rrls));

overwrite (al, b);

overwritelthy thy (al, bl);

case assoc' ((Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")),"e_rls") of

  SOME ("Tools", Rls _) => ()

| _ => error "e_rls not in Theory_Data" 

assoc_rls "e_rls";

"----------- thm_hier --------------------------------------------";

"----------- thm_hier --------------------------------------------";

"----------- thm_hier --------------------------------------------";

(curry op:: "xxx") ["yyy","yyy","yyy"];

map (curry op:: "xxx") [["yyy1"],["yyy2"],["yyy3"]];

val thy' = "Integrate";

val thy = assoc_thy (thyID2theory' thy');

"WN120406.GOON --- restarted with 'isolate response' below, because it was very slow ?!?" ^

"slow probably only because of print_depth 999 and large output";

val thm = prop_of @{thm integral_var};

(*-.-.-.-.-.-WN120406 isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

"collect_thms thy'------------------------------------------------";

(apfst single) ("Integrate.integral_var", thm);

(strip_thy o #1) ("Integrate.integral_var", thm);

(*cannot get this as arg from arg        ^^^^^^^^^^^^^^^^*)

    ("Integrate.integral_var", @{thm integral_var});

(*thus new fun....*)

makeHthm ("IsacKnowledge", thy') ("Integrate.integral_var", thm);

(makeHthm ("IsacKnowledge", thy')) ("Integrate.integral_var", thm);

map (makeHthm ("IsacKnowledge", thy')) (Theory.axioms_of thy);

collect_thms' ("IsacKnowledge", thy');

"collect_rlss thy'------------------------------------------------";

makeHrls "IsacKnowledge" ("integration_rules", (thy', integration_rules));

val thy' = "Test";

val rlss = filter ((curry op= thy') o 

			   ((#1 o #2):(rls' * (theory' * rls)) -> theory')) 

			  (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac"));

collect_rlss ("IsacKnowledge",thy');

"collect_thy thy-------------------------------------------------";

val thy' = "ListC";

val thy = assoc_thy (thyID2theory' thy');

((collect_thms' ("IsacKnowledge",thy')) @ 

 (collect_rlss ("IsacKnowledge",thy')) @ 

 (collect_cals ("IsacKnowledge",thy')) @ 

 (collect_ords ("IsacKnowledge",thy')));

collect_thy "IsacKnowledge" thy';

"collect_thydata -------------------------------------------------";

(*map rearrange_inv (! isab_thm_thy); dropped WN120321*)

val xxx = hd (! isab_thm_thy);

(single) xxx;

(apfst ((curry op:: "Isabelle") o single)) xxx;

map (apfst ( (curry op:: "Isabelle") o single) );

map (apfst ((curry op:: "Isabelle") o single)) (! isab_thm_thy);

"thy_hierarchy ---------------------------------------------------";

val theID = ["IsacScripts", "ListC", "Theorems", "append_Cons"]:theID;

val thydat as (theID, thydata) = 

    (theID, Hthm {guh = theID2guh theID, mathauthors = [],

     coursedesign = [], thm = prop_of @{thm append_Cons}});

val th = [] : thehier;

val theID' = cut_theID th theID;

val th = fill_parents th theID' theID;

(* val th =

   [Ptyp ("IsacScripts",

            [Html {guh = "thy_ListG-thm-append_Cons", html = "", ...}],

            [Ptyp ("ListG", ...)])] : thehier *)

(*show_thes*)(writeln o format_pblIDl o (scan [])) th;

writeln (hierarchy_guh th);

"~~~~~ fun collect_thydata, args:"; val () = ();

    val isab_thms = (! isab_thm_thy):  (thmDeriv * term) list

val xxx = hd (! isab_thm_thy);

(collect_isab "Isabelle") xxx;

(map (collect_isab "Isabelle") (! isab_thm_thy));

(* = [(["Isabelle", "HOL", "Theorems", "refl"],

           Hthm {guh = "thy_isab_HOL-thm-refl", thm = Const ("HOL.Trueprop...", ..., 

             mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}),

          (["Isabelle", "Fun", "Theorems", ...],

           Hthm {guh = "thy_isab_Fun-thm-o_apply", thm = Const (......, 

             mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}),

          (["Isabelle", "ListC", ...], ...), (["Isabelle", ...], ...), ([...], ...), ...]:

   (theID * thydata) list*)

(! progthys);

val xxx = hd (map Context.theory_name (! progthys)): theory';

(collect_thy "IsacScripts") xxx;

((flat o (map (collect_thy "IsacScripts"))) (map Context.theory_name (! progthys)));

(* = [(["IsacScripts", "Script", "Theorems", "arity_type_ID"],

           Hthm {guh = "thy_scri_Script-thm-arity_type_ID", thm = Const ("HOL.type_class..., 

             mathauthors = ["isac-team"], coursedesign = []}),

          (["IsacScripts", "Script", "Theorems", ...], 

               Hthm {guh = "thy_scri_Script-thm-arity_type_arg", thm = Const (...) $ Const (...), 

                 mathauthors = ["isac-team"], coursedesign = []}),

          (["IsacScripts", "Tools", ...], ...), (["IsacScripts", ...], ...), ([...], ...), ...]:

   (theID * thydata) list*)

print_depth 5;

((flat o (map (collect_thy "IsacKnowledge"))) (map Context.theory_name (! knowthys)));

(* = [(["IsacKnowledge", "Inverse_Z_Transform", "Theorems", ...],

           Hthm {guh = "thy_isac_Inverse_Z_Transform-thm-rule1", thm =

                 Const (...) $ (Const (...) $ Const (... $ Bound 0 $ Const (...))))))),

                 mathauthors = ["isac-team"], coursedesign = []}),

          (["IsacKnowledge", "Inverse_Z_Transform", ...], ...), 

          (["IsacKnowledge", ...], ...), ([...], ...), ...]:

   (theID * thydata) list*)

"~~~~~ from collect_thydata return val:"; val () = ();

val th = [] : thehier;

val thydats = collect_thydata ();

val th1 = the_hier th thydats (**** insert: not found [".. from fill_parents*);

(*show_thes*)(writeln o format_pblIDl o (scan [])) th1;

writeln (hierarchy_guh th);

(*writeln (hierarchy_guh th);

*)

writeln (hierarchy_guh th1);

(* <NODE>

    <ID> Isabelle </ID>

    <NO> 1 </NO>

    <CONTENTREF> thy_isab_Isabelle-part </CONTENTREF>

  </NODE>*)

"thy_hierarchy2file ----------------------------------------------";

show_thes();

(*

val path = "../../tmp/";

thy_hierarchy2file path;

*)

get_the ["IsacKnowledge"];

(*------------------------ WN120320

get_the ["IsacKnowledge", "Test"];

get_the ["IsacKnowledge", "Test", "Theorems"];

get_the ["IsacKnowledge", "Test", "Theorems", "exp_pow"];

get_the ["IsacKnowledge", "Test", "Rulesets"];

WN120320 ----------------------- *)

(* FIXXXXXXXXXME.WN060713 guh -- theID

case get_the ["IsacKnowledge", "Test", "Rulesets", "Test_simplify"] of

    Hrls {guh = "thy_Test-rls-Test_simplify",thy_rls = ("Test", _),

          mathauthors = _,coursedesign = _} => ()

  | _ => error "thy-hierarchy.sml: [IsacKnowledge,Test,Rulesets]";

*)

-.-.-.-.-.-.-WN120406 isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

"----------- fun thydata2xml -------------------------------------";

"----------- fun thydata2xml -------------------------------------";

"----------- fun thydata2xml -------------------------------------";

(*========== inhibit exn AK110725 ================================================

val theID = ["IsacScripts", "ListG", "Theorems", "append_Cons"];

val thmdata = get_the theID;

writeln(thydata2xml (theID, thmdata));

val theID = ["IsacKnowledge", "Poly", "Rulesets", "norm_Poly"];

val rlsdata = get_the theID;

writeln(thydata2xml (theID, rlsdata));

========== inhibit exn AK110725 ================================================*)

(*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]

  see sml/../datatypes.sml !

val (thy', rls') = ("DiffApp", "Tools.rhs");

thy_containing_rls thy' rls';

print_depth 99; map #1 startsearch; print_depth 3;

*)

(*

val path = "../../tmp/";

thes2file path;

*)

"----------- write xml to tmp ------------------------------------";

"----------- write xml to tmp ------------------------------------";

"----------- write xml to tmp ------------------------------------";

(*

val path = "../../tmp/"; 

pbl_hierarchy2file (path ^ "pbl/");

pbls2file          (path ^ "pbl/");

met_hierarchy2file (path ^ "met/");

mets2file          (path ^ "met/");

thy_hierarchy2file (path ^ "thy/");

thes2file          (path ^ "thy/");

*)

"----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";

"----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";

"----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";

(*

store_isa ["Isabelle"] ["THIS SHOULD not BE OVERWRITTEN below"];

print_depth 99; get_the ["Isabelle"]; print_depth 3;

print_depth 5; thehier;  print_depth 3;

thehier := the_hier (! thehier) (collect_thydata ());

print_depth 99; get_the ["Isabelle"]; print_depth 3;

print_depth 5; thehier;  print_depth 3;

*)

case get_the ["IsacKnowledge", "Biegelinie", "Theorems"] of

   Html {mathauthors =

	 ["Walther Neuper 2005 supported by a grant from NMI Austria"],...}=>()

 | _ => error "thy-hierarchy.sml: store_isa overwritten";

case get_the ["IsacKnowledge","Biegelinie","Theorems","Belastung_Querkraft"] of

   Hthm {mathauthors =

	 ["Walther Neuper 2005 supported by a grant from NMI Austria"],...}=>()

 | _ => error "thy-hierarchy.sml: store_isa overwritten";

(*

print_depth 7; 

get_the ["IsacKnowledge","Biegelinie","Theorems","Belastung_Querkraft"];

print_depth 3;

*)

(*WN060728 strange behaviour:

### fun the_hier reports these not overwritten ?!?...(stored twice ?!?) ...

val it = () : unit

*** insert: preserved ["Isabelle","RealDef","Theorems","mult_assoc"]

*** insert: preserved ["Isabelle","RealDef","Theorems","add_assoc"]

*** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_minus1"]

*** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_2"]

*** insert: preserved ["Isabelle","RealDef","Theorems","mult_assoc"]

*** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_minus_eq1"]

*** insert: preserved ["Isabelle","RealDef","Theorems","add_assoc"]

*** insert: preserved ["Isabelle","RealDef","Theorems","real_minus_divide_eq"]

*** insert: preserved ["IsacScripts","ListG","Theorems","induct"]

*** insert: preserved ["IsacScripts","ListG","Theorems","simps_1"]

*** insert: preserved ["IsacScripts","ListG","Theorems","simps_2"]

val it = () : unit

### but those store_*d in Biegelinie.ML are NOT reported !?!?!?!?!?!?!

### however, '*** insert: not found' is NOT reported below, too....

----------------------------------

*** insert: not found ... IS OK :

comes from fill_parents

----------------------------------

val it = () : unit

*** insert: not found ["Isabelle","NatDef","Theorems","order_refl"]

*** insert: not found ["Isabelle","NatDef","Theorems","order_refl"]*)

"----------- ### thes2file ... Exception- Match raised -----------";

"----------- ### thes2file ... Exception- Match raised -----------";

"----------- ### thes2file ... Exception- Match raised -----------";

writeln "what to do when you get,e.g. \n\

\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\"]\n\

\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"integration_rules\"]\n\

\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"add_new_c\"]\n\

\Exception- Match raised";

val ptyp = hd (! thehier);

val theID = ["IsacKnowledge","Integrate","Rulesets","add_new_c"];

(*========== inhibit exn AK110725 ================================================

val thydata = get_the theID;

(* creates a file ...

thydata2file "~/tmp/"[] theID thydata (*reports Exception- Match in question*);

*)

thydata2xml (theID, thydata) (*reports Exception- Match in question*);

val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) = 

    (theID, thydata);

rls2xml i thy_rls (*reports Exception- Match in question*);

val (j, (thyID, Seq data)) = (i, thy_rls);

(* evaluate this local fun ...

rls2xm j (thyID, "Seq", data) (*reports Exception- Match in question*);

*)

val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,

			 srls, calc, rules, scr})) = 

    (j, (thyID, "Seq", data));

rules2xml (j+2*i) thyID rules (*reports Exception- Match in question*);

============ inhibit exn AK110725 ==============================================*)

"----------- thes2file: thy_containing_rls : rls '...' not in ! --";

"----------- thes2file: thy_containing_rls : rls '...' not in ! --";

"----------- thes2file: thy_containing_rls : rls '...' not in ! --";

val TESTdump = Unsynchronized.ref 

  ("path": path, ["ids"]: theID, []: pos, thydata2file, Ptyp ("xxx", [], []): thydata ptyp);

fun TESTthenode (pa:path) ids po wfn (Ptyp (id, [n], ns)) TESTids = 

    let val po' = lev_on po

    in 

      if (ids@[id]) = TESTids

      then

        (TESTdump := (pa, ids, po', wfn, (Ptyp (id, [n], ns))); 

          error "stopped before error, created TESTdump") (* this exn creates right signature*)

      else

        wfn pa po' (ids @ [id]) n; TESTthenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns TESTids

    end

and TESTthenodes _ _ _ _ [] _ = ()

  | TESTthenodes pa ids po wfn (n::ns) TESTids =

      (TESTthenode pa ids po wfn n TESTids; TESTthenodes pa ids (lev_on po) wfn ns TESTids);

(* /--- side effects from previous test files ---\*)

    val i = indentation;

    val j = indentation;

(* \--- side effects from previous test files ---/*)

"~~~~~ fun thes2file, args:"; val (p : path) = ("../../tmp/");

(* recursively descend into thehier just before the error: *)

(TESTthenodes p [] [0] thydata2file (! thehier)

  ["IsacKnowledge","Poly","Rulesets","norm_Poly"] 

handle _(* "stopped before error, created TESTdump" *) => ());

val (pa, ids, po', wfn, (Ptyp (id, [n], ns))) = ! TESTdump;

"~~~~~ fun thydata2file, args:"; val ((xmldata:path), (pos:pos), (theID:theID), thydata) =

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

"~~~~~ fun thydata2xml, args:"; val (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =

  (theID:theID, thydata);

"~~~~~ fun rls2xml, args:"; val (j, (thyID, Seq data)) = (i, thy_rls);

"~~~~~ fun rls2xm, args:"; val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,

		      srls, calc, errpatts, rules, scr})) = (j, (thyID, "Seq", data));

"~~~~~ fun rules2xml, args:"; val (j, thyID, (r::rs)) = ((j+2*i), thyID, rules);

"~~~~~ fun rule2xml, args:"; val (j, thyID, (Rls_ rls)) = (j, thyID, r);

val rls' = (#id o rep_rls) rls;

"~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = (thyID, rls');

infix mem; (*from Isabelle2002*)

fun x mem [] = false

  | x mem (y :: ys) = x = y orelse x mem ys;

    val rls' = strip_thy rls'

    val thy' = thyID2theory' thy'

    val dropthys =

      takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory'))

        (rev (!theory'));

if map #1 dropthys = ["Isac", "Inverse_Z_Transform", "DiophantEq", "AlgEin", "Biegelinie",

  "Vect", "PolyMinus", "Frontend", "Partial_Fractions", "DiffApp", "Test", "EqSystem", "Integrate",

  "Diff", "LogExp", "Trig", "Calculus", "PolyEq", "RootRatEq", "RootRat", "RatEq", "RootEq",

  "LinEq", "Root", "Equation", "Rational"]

then () else error "thy_containing_rls changed ancestors_rls for (Poly, discard_minus)";

    val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys: string list;

		    val ancestors_rls = 

		      filter_out ((curry ((op mem) o swap) dropthys') o ((#1 o #2): rls'*(theory' * rls)->theory'))

		        (rev (Test_KEStore_Elems.get_rlss (Thy_Info.get_theory "Isac")));

case assoc (ancestors_rls, rls') of

  SOME ("Poly", Rls {id = "discard_minus", ...}) => ()

| _ => error "thy_containing_rls changed 2";

"----------- fun store_thm ---------------------------------------";

"----------- fun store_thm ---------------------------------------";

"----------- fun store_thm ---------------------------------------";

store_thm @{theory "Biegelinie"} "IsacKnowledge"

  ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft})

	    ["Walther Neuper 2005 supported by a grant from NMI Austria"];

"~~~~~ fun store_thm, args:"; val (thy, part, (thmID : thmID, thm), (mathauthors : authors)) =

  (@{theory "Biegelinie"}, "IsacKnowledge",

    ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft}),

	      ["Walther Neuper 2005 supported by a grant from NMI Austria"]);

    val guh = thm2guh (part, theory2thyID thy) thmID

    val theID = guh2theID guh;

if guh = "thy_isac_Biegelinie-thm-Belastung_Querkraft" andalso

  theID = ["IsacKnowledge", "Biegelinie", "Theorems", "Belastung_Querkraft"]

then () else error "store_thm: guh | theID changed";

"----------- fun insert_fillpats ---------------------------------";

"----------- fun insert_fillpats ---------------------------------";

"----------- fun insert_fillpats ---------------------------------";

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

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

val path = ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]: theID;

(*save   *) val Hthm {guh, coursedesign, mathauthors, thm, fillpats = save_fillpats} = get_the path;

val test_fillpats = [

  ("fill-d_d-arg",

    parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),

  ("test-fillpatt", e_term, "test-errpat")]: fillpat list;

insert_fillpats path test_fillpats;

val Hthm {fillpats, ...} = get_the path;

case fillpats of

  [("fill-d_d-arg", _, "chain-rule-diff-both"), ("test-fillpatt", _, "test-errpat")] => ()

| _ => error "insert_fillpats changed"

(*restore*) insert_fillpats path save_fillpats;

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

"----------- fun insert_errpatIDs --------------------------------";

"----------- fun insert_errpatIDs --------------------------------";

"----------- fun insert_errpatIDs --------------------------------";

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

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

(* isolate test: 10 secs *) val original = (! thehier);

(* still ununsed; planned for stepToErrorpattern *)

val path = ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]: theID;

val errpattIDs = ["chain-rule-diff-both", "test-errpatID"];

insert_errpatIDs path errpattIDs;

val Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)} = get_the path

val Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, errpatts} = rls;

if errpattIDs = ["chain-rule-diff-both", "test-errpatID"] then ()

else error "insert_errpatIDs to norm_diff changed";

(* isolate test: 10 secs *) thehier := original;

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

insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]

 ([("fill-d_d-arg",

     parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),

   ("fill-both-args",

     parse_patt thy "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),

   ("fill-d_d",

     parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),

   ("fill-inner-deriv",

     parse_patt thy "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),

   ("fill-all",

     parse_patt thy "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list);