neuper@37871: (* tests for sml/xmlsrc/thy-hierarchy.sml
neuper@37871:    authors: Walther Neuper 060113
neuper@37871:    (c) due to copyright terms
neuper@37871: 
neuper@37871: use"../smltest/xmlsrc/thy-hierarchy.sml";
neuper@37871: use"thy-hierarchy.sml";
neuper@37871: 
neuper@37871: CAUTION with testing *2file functions -- they are actually writing to ~/tmp
neuper@37871: *)
neuper@37871: 
neuper@37871: val thy = Isac.thy;
neuper@37871: 
neuper@37871: "-----------------------------------------------------------------";
neuper@37871: "table of contents -----------------------------------------------";
neuper@37871: "-----------------------------------------------------------------";
neuper@37871: "----------- assoc_rls -------------------------------------------";
neuper@37871: "----------- thm_hier --------------------------------------------";
neuper@37871: "----------- fun thydata2xml -------------------------------------";
neuper@37871: "----------- write xml to tmp ------------------------------------";
neuper@37871: "----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
neuper@37871: "----------- ### thes2file ... Exception- Match raised -----------";
neuper@37871: "-----------------------------------------------------------------";
neuper@37871: "-----------------------------------------------------------------";
neuper@37871: "-----------------------------------------------------------------";
neuper@37871: 
neuper@37871: 
neuper@37871: "----------- assoc_rls -------------------------------------------";
neuper@37871: "----------- assoc_rls -------------------------------------------";
neuper@37871: "----------- assoc_rls -------------------------------------------";
neuper@37871: val al = [(1,11),(2,22),(3,33)];
neuper@37871: overwrite (al, (2,2222));
neuper@37871: (*val it = [(1, 11), (2, 2222), (3, 33)] : (int * int) list*)
neuper@37871: 
neuper@37871: val al = [("e_rls",("Atools",e_rls)),("e_rrls",("Atools",e_rrls))];
neuper@37871: val bl = [("e_rls",e_rls),("e_rrls",e_rrls)];
neuper@37871: val b = ("e_rls",("Atools",e_rrls));
neuper@37871: overwrite (al, b);
neuper@37871: overwritelthy thy (al, bl);
neuper@37871: 
neuper@37871: assoc' (!ruleset',"e_rls");
neuper@37871: assoc_rls "e_rls";
neuper@37871: 
neuper@37871: 
neuper@37871: "----------- thm_hier --------------------------------------------";
neuper@37871: "----------- thm_hier --------------------------------------------";
neuper@37871: "----------- thm_hier --------------------------------------------";
neuper@37871: (curry op:: "xxx") ["yyy","yyy","yyy"];
neuper@37871: map (curry op:: "xxx") [["yyy1"],["yyy2"],["yyy3"]];
neuper@37871: 
neuper@37871: val thy' = "Integrate";
neuper@37871: val thy = assoc_thy (thyID2theory' thy');
neuper@37871: 
neuper@37871: "collect_thms thy'------------------------------------------------";
neuper@37871: (thms_of thy);
neuper@37871: 
neuper@37871: (apfst single) ("Integrate.integral_var", integral_var);
neuper@37871: 
neuper@37871: (strip_thy o #1) ("Integrate.integral_var", integral_var);
neuper@37871: 
neuper@37871: (*cannot get this as arg from arg        ^^^^^^^^^^^^^^^^*)
neuper@37871:     ("Integrate.integral_var", integral_var);
neuper@37871: (*thus new fun....*)
neuper@37871: 
neuper@37871: makeHthm ("IsacKnowledge",thy') ("Integrate.integral_var", integral_var);
neuper@37871: (makeHthm ("IsacKnowledge",thy')) ("Integrate.integral_var", integral_var);
neuper@37871: map (makeHthm ("IsacKnowledge",thy')) (thms_of thy);
neuper@37871: collect_thms' ("IsacKnowledge",thy');
neuper@37871: 
neuper@37871: "collect_rlss thy'------------------------------------------------";
neuper@37871: makeHrls "IsacKnowledge" ("integration_rules", (thy', integration_rules));
neuper@37871: 
neuper@37871: val thy' = "Test";
neuper@37871: val rlss = filter ((curry op= thy') o 
neuper@37871: 			   ((#1 o #2):(rls' * (theory' * rls)) -> theory')) 
neuper@37871: 			  (!ruleset');
neuper@37871: collect_rlss ("IsacKnowledge",thy');
neuper@37871: 
neuper@37871: "collect_thy thy-------------------------------------------------";
neuper@37871: val thy' = "ListG.thy";
neuper@37871: val thy = assoc_thy (thyID2theory' thy');
neuper@37871: ((collect_thms' ("IsacKnowledge",thy')) @ 
neuper@37871:  (collect_rlss ("IsacKnowledge",thy')) @ 
neuper@37871:  (collect_cals ("IsacKnowledge",thy')) @ 
neuper@37871:  (collect_ords ("IsacKnowledge",thy')));
neuper@37871: collect_thy "IsacKnowledge" thy';
neuper@37871: 
neuper@37871: "collect_thydata -------------------------------------------------";
neuper@37871: (!isab_thm_thy);
neuper@37871: map rearrange_inv (!isab_thm_thy);
neuper@37871: (map ((apfst ((curry op:: "Isabelle") o single)) o rearrange_inv));
neuper@37871: (map ((apfst ((curry op:: "Isabelle") o single)) o rearrange_inv)) 
neuper@37871:     (!isab_thm_thy);
neuper@37871: 
neuper@37871: 
neuper@37871: "thy_hierarchy ---------------------------------------------------";
neuper@37871: val theID = ["IsacScripts", "ListG", "Theorems", "append_Cons"]:theID;
neuper@37871: val thydat as (theID, thydata) = 
neuper@37871:     (theID, Hthm {guh=theID2guh theID, mathauthors=[],
neuper@37871:      coursedesign=[], thm=append_Cons});
neuper@37871: 
neuper@37871: val th = [] : thehier;
neuper@37871: val theID' = cut_theID th theID;
neuper@37871: val th = fill_parents th theID' theID;
neuper@37871: (* val th =
neuper@37871:    [Ptyp ("IsacScripts",
neuper@37871:             [Html {guh = "thy_ListG-thm-append_Cons", html = "", ...}],
neuper@37871:             [Ptyp ("ListG", ...)])] : thehier *)
neuper@37871: (*show_thes*)(writeln o format_pblIDl o (scan [])) th;
neuper@37871: writeln (hierarchy_guh th);
neuper@37871: 
neuper@37871: val th = [] : thehier;
neuper@37871: val thydats = collect_thydata ();
neuper@37871: val th1 = the_hier th thydats (**** insert: not found [".. from fill_parents*);
neuper@37871: (*show_thes*)(writeln o format_pblIDl o (scan [])) th1;
neuper@37871: 
neuper@37871: writeln (hierarchy_guh th);
neuper@37871: writeln (hierarchy_guh th1);
neuper@37871: 
neuper@37871: "thy_hierarchy2file ----------------------------------------------";
neuper@37871: show_thes();
neuper@37871: (*
neuper@37871: val path = "/home/neuper/tmp/";
neuper@37871: thy_hierarchy2file path;
neuper@37871: *)
neuper@37871: 
neuper@37871: get_the ["IsacKnowledge"];
neuper@37871: get_the ["IsacKnowledge", "Test"];
neuper@37871: get_the ["IsacKnowledge", "Test", "Theorems"];
neuper@37871: get_the ["IsacKnowledge", "Test", "Theorems", "exp_pow"];
neuper@37871: 
neuper@37871: get_the ["IsacKnowledge", "Test", "Rulesets"];
neuper@37871: 
neuper@37871: (* FIXXXXXXXXXME.WN060713 guh -- theID
neuper@37871: case get_the ["IsacKnowledge", "Test", "Rulesets", "Test_simplify"] of
neuper@37871:     Hrls {guh = "thy_Test-rls-Test_simplify",thy_rls = ("Test", _),
neuper@37871:           mathauthors = _,coursedesign = _} => ()
neuper@37871:   | _ => raise error "thy-hierarchy.sml: [IsacKnowledge,Test,Rulesets]";
neuper@37871: *)
neuper@37871: 
neuper@37871: 
neuper@37871: "----------- fun thydata2xml -------------------------------------";
neuper@37871: "----------- fun thydata2xml -------------------------------------";
neuper@37871: "----------- fun thydata2xml -------------------------------------";
neuper@37871: val theID = ["IsacScripts", "ListG", "Theorems", "append_Cons"];
neuper@37871: val thmdata = get_the theID;
neuper@37871: writeln(thydata2xml (theID, thmdata));
neuper@37871: 
neuper@37871: val theID = ["IsacKnowledge", "Poly", "Rulesets", "norm_Poly"];
neuper@37871: val rlsdata = get_the theID;
neuper@37871: writeln(thydata2xml (theID, rlsdata));
neuper@37871: 
neuper@37871: (*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]
neuper@37871:   see sml/../datatypes.sml !
neuper@37871: val (thy', rls') = ("DiffApp.thy", "Tools.rhs");
neuper@37871: thy_containing_rls thy' rls';
neuper@37871: print_depth 99; map #1 startsearch; print_depth 3;
neuper@37871: *)
neuper@37871: 
neuper@37871: (*
neuper@37871: val path = "/home/neuper/tmp/";
neuper@37871: thes2file path;
neuper@37871: *)
neuper@37871: 
neuper@37871: "----------- write xml to tmp ------------------------------------";
neuper@37871: "----------- write xml to tmp ------------------------------------";
neuper@37871: "----------- write xml to tmp ------------------------------------";
neuper@37871: (*
neuper@37871: val path = "/home/neuper/tmp/"; 
neuper@37871: 
neuper@37871: pbl_hierarchy2file (path ^ "pbl/");
neuper@37871: pbls2file          (path ^ "pbl/");
neuper@37871: 
neuper@37871: met_hierarchy2file (path ^ "met/");
neuper@37871: mets2file          (path ^ "met/");
neuper@37871: 
neuper@37871: thy_hierarchy2file (path ^ "thy/");
neuper@37871: thes2file          (path ^ "thy/");
neuper@37871: *)
neuper@37871: 
neuper@37871: 
neuper@37871: "----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
neuper@37871: "----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
neuper@37871: "----------- the_hier [] (collect_thyda.. NOT overwriting store_ -";
neuper@37871: (*
neuper@37871: store_isa ["Isabelle"] ["THIS SHOULD not BE OBERWRITTEN below"];
neuper@37871: print_depth 99; get_the ["Isabelle"]; print_depth 3;
neuper@37871: print_depth 5; thehier;  print_depth 3;
neuper@37871: 
neuper@37871: thehier := the_hier (!thehier) (collect_thydata ());
neuper@37871: print_depth 99; get_the ["Isabelle"]; print_depth 3;
neuper@37871: print_depth 5; thehier;  print_depth 3;
neuper@37871: *)
neuper@37871: 
neuper@37871: case get_the ["IsacKnowledge", "Biegelinie", "Theorems"] of
neuper@37871:    Html {mathauthors =
neuper@37871: 	 ["Walther Neuper 2005 supported by a grant from NMI Austria"],...}=>()
neuper@37871:  | _ => raise error "thy-hierarchy.sml: store_isa overwritten";
neuper@37871: 
neuper@37871: case get_the ["IsacKnowledge","Biegelinie","Theorems","Belastung_Querkraft"] of
neuper@37871:    Hthm {mathauthors =
neuper@37871: 	 ["Walther Neuper 2005 supported by a grant from NMI Austria"],...}=>()
neuper@37871:  | _ => raise error "thy-hierarchy.sml: store_isa overwritten";
neuper@37871: 
neuper@37871: (*
neuper@37871: print_depth 7; 
neuper@37871: get_the ["IsacKnowledge","Biegelinie","Theorems","Belastung_Querkraft"];
neuper@37871: print_depth 3;
neuper@37871: *)
neuper@37871: 
neuper@37871: (*WN060728 strange behaviour:
neuper@37871: ### fun the_hier reports these not overwritten ?!?...(stored twice ?!?) ...
neuper@37871: 
neuper@37871: val it = () : unit
neuper@37871: *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_assoc"]
neuper@37871: *** insert: preserved ["Isabelle","RealDef","Theorems","real_add_assoc"]
neuper@37871: *** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_minus1"]
neuper@37871: *** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_2"]
neuper@37871: *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_assoc"]
neuper@37871: *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_minus_eq1"]
neuper@37871: *** insert: preserved ["Isabelle","RealDef","Theorems","real_add_assoc"]
neuper@37871: *** insert: preserved ["Isabelle","RealDef","Theorems","real_minus_divide_eq"]
neuper@37871: *** insert: preserved ["IsacScripts","ListG","Theorems","induct"]
neuper@37871: *** insert: preserved ["IsacScripts","ListG","Theorems","simps_1"]
neuper@37871: *** insert: preserved ["IsacScripts","ListG","Theorems","simps_2"]
neuper@37871: val it = () : unit
neuper@37871: 
neuper@37871: ### but those store_*d in Biegelinie.ML are NOT reported !?!?!?!?!?!?!
neuper@37871: ### however, '*** insert: not found' is NOT reported below, too....
neuper@37871: 
neuper@37871: ----------------------------------
neuper@37871: *** insert: not found ... IS OK :
neuper@37871: comes from fill_parents
neuper@37871: ----------------------------------
neuper@37871: 
neuper@37871: val it = () : unit
neuper@37871: *** insert: not found ["Isabelle","NatDef","Theorems","le_refl"]
neuper@37871: *** insert: not found ["Isabelle","NatDef","Theorems","le_refl"]*)
neuper@37871: 
neuper@37871: "----------- ### thes2file ... Exception- Match raised -----------";
neuper@37871: "----------- ### thes2file ... Exception- Match raised -----------";
neuper@37871: "----------- ### thes2file ... Exception- Match raised -----------";
neuper@37871: writeln "what to do when you get,e.g. \n\
neuper@37871: \### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\"]\n\
neuper@37871: \### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"integration_rules\"]\n\
neuper@37871: \### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"add_new_c\"]\n\
neuper@37871: \Exception- Match raised";
neuper@37871: 
neuper@37871: val ptyp = hd (!thehier);
neuper@37871: val theID = ["IsacKnowledge","Integrate","Rulesets","add_new_c"];
neuper@37871: val thydata = get_the theID;
neuper@37871: (* creates a file ...
neuper@37871: thydata2file "~/tmp/"[] theID thydata (*reports Exception- Match in question*);
neuper@37871: *)
neuper@37871: thydata2xml (theID, thydata) (*reports Exception- Match in question*);
neuper@37871: val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) = 
neuper@37871:     (theID, thydata);
neuper@37871: rls2xml i thy_rls (*reports Exception- Match in question*);
neuper@37871: val (j, (thyID, Seq data)) = (i, thy_rls);
neuper@37871: (* evaluate this local fun ...
neuper@37871: rls2xm j (thyID, "Seq", data) (*reports Exception- Match in question*);
neuper@37871: *)
neuper@37871: val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
neuper@37871: 			 srls, calc, rules, scr})) = 
neuper@37871:     (j, (thyID, "Seq", data));
neuper@37871: rules2xml (j+2*i) thyID rules (*reports Exception- Match in question*);
neuper@37871: