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

   authors: Walther Neuper 060113

   (c) due to copyright terms

use"../smltest/xmlsrc/thy-hierarchy.sml";

use"thy-hierarchy.sml";

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

*)

val thy = Isac.thy;

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

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

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

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

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

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

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

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

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

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

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

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

"----------- 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);

assoc' (!ruleset',"e_rls");

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');

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

(PureThy.all_thms_of thy);

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

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

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

    ("Integrate.integral_var", integral_var);

(*thus new fun....*)

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

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

map (makeHthm ("IsacKnowledge",thy')) (PureThy.all_thms_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')) 

			  (!ruleset');

collect_rlss ("IsacKnowledge",thy');

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

val thy' = "ListG.thy";

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 -------------------------------------------------";

(!isab_thm_thy);

map rearrange_inv (!isab_thm_thy);

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

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

    (!isab_thm_thy);

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

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

val thydat as (theID, thydata) = 

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

     coursedesign=[], 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);

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 th1);

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

show_thes();

(*

val path = "/home/neuper/tmp/";

thy_hierarchy2file path;

*)

get_the ["IsacKnowledge"];

get_the ["IsacKnowledge", "Test"];

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

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

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

(* 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]";

*)

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

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

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

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));

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

  see sml/../datatypes.sml !

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

thy_containing_rls thy' rls';

print_depth 99; map #1 startsearch; print_depth 3;

*)

(*

val path = "/home/neuper/tmp/";

thes2file path;

*)

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

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

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

(*

val path = "/home/neuper/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 OBERWRITTEN 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","real_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","real_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","real_le_refl"]

*** insert: not found ["Isabelle","NatDef","Theorems","real_le_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"];

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*);