test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml
author Walther Neuper <wneuper@ist.tugraz.at>
Thu, 29 Aug 2019 13:52:47 +0200
changeset 59602 89b3eaa34de6
parent 59600 0914ffedb4c5
child 59635 9fc1bb69813c
permissions -rw-r--r--
prep. re-organisation of thys in ProgLang
wneuper@59549
     1
(* Title: "xmlsrc/thy-hierarchy.sml"
wneuper@59549
     2
     tests for xmlsrc/thy-hierarchy.sml
akargl@42176
     3
   Authors: Walther Neuper 060113
neuper@37906
     4
   (c) due to copyright terms
neuper@37906
     5
wneuper@59465
     6
theory Test_Some imports Isac.Build_Thydata begin 
neuper@55397
     7
ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
neuper@55397
     8
ML_file "xmlsrc/thy-hierarchy.sml"
neuper@55397
     9
neuper@37906
    10
CAUTION with testing *2file functions -- they are actually writing to ~/tmp
neuper@37906
    11
*)
neuper@37906
    12
wneuper@59592
    13
val thy = @{theory "Isac_Knowledge"};
neuper@37906
    14
neuper@37906
    15
"-----------------------------------------------------------------";
neuper@37906
    16
"table of contents -----------------------------------------------";
neuper@37906
    17
"-----------------------------------------------------------------";
wneuper@59203
    18
"----------- fun thms_of -----------------------------------------";
neuper@37906
    19
"----------- ### thes2file ... Exception- Match raised -----------";
neuper@55493
    20
"----------- search for data error in thes2file ------------------";
neuper@42407
    21
"----------- thes2file: thy_containing_rls : rls '...' not in ! --";
wneuper@59188
    22
"----------- fun Thm.make_thm ------------------------------------";
neuper@55415
    23
"----------- correct theIDs for e_rls ----------------------------";
neuper@55484
    24
"----------- fun revert_sym --------------------------------------";
neuper@55484
    25
"----------- fun thms_of_rlss ------------------------------------";
neuper@55492
    26
"----------- repair thydata2xml for rls --------------------------";
neuper@37906
    27
"-----------------------------------------------------------------";
neuper@55490
    28
"----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
neuper@55490
    29
"----------- ..CONTINUED: we adapt some required MINIfunctions ---";
neuper@55490
    30
"----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
neuper@55490
    31
"----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
neuper@55490
    32
"-----------------------------------------------------------------";
neuper@37906
    33
"-----------------------------------------------------------------";
neuper@37906
    34
"-----------------------------------------------------------------";
neuper@37906
    35
neuper@37906
    36
wneuper@59203
    37
"----------- fun thms_of -----------------------------------------";
wneuper@59203
    38
"----------- fun thms_of -----------------------------------------";
wneuper@59203
    39
"----------- fun thms_of -----------------------------------------";
wneuper@59203
    40
(*WN160112 WE REPLACED vvv BY "fun thms_of" in src/../thy-hierarchy.sml
wneuper@59203
    41
val ths = MutabelleExtra.thms_of false @{theory Biegelinie};
wneuper@59203
    42
(*val it = 
wneuper@59203
    43
  ["Q' ?x = - qq ?x", "- qq ?x = Q' ?x", "\<not> ?a =!= 0 \<Longrightarrow> (?a * ?f ?x = ?b) = (?f ?x = 1 / ?a * ?b)",
wneuper@59203
    44
   "Q ?x = M_b' ?x", "M_b' ?x = Q ?x", "y'' ?x = - M_b ?x / EI", "M_b ?x = - EI * y'' ?x"]*)
wneuper@59203
    45
map thmID_of_derivation_name' (thms_of thy) = 
wneuper@59203
    46
  ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", 
wneuper@59203
    47
   "Querkraft_Moment", "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"]
wneuper@59203
    48
*)
wneuper@59203
    49
val thy = @{theory Biegelinie};
wneuper@59203
    50
val thms = thms_of thy;
wneuper@59203
    51
if map thmID_of_derivation_name' thms = 
wneuper@59203
    52
  ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", "Querkraft_Moment", 
wneuper@59203
    53
   "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] then ()
wneuper@59549
    54
else error "fun thms_of ...changed";
wneuper@59549
    55
wneuper@59549
    56
val without_partial_functions = thms_of @{theory Biegelinie};
wneuper@59549
    57
if length without_partial_functions = 7 then () else error "thms_of Biegelinie changed";
wneuper@59203
    58
neuper@37906
    59
"----------- ### thes2file ... Exception- Match raised -----------";
neuper@37906
    60
"----------- ### thes2file ... Exception- Match raised -----------";
neuper@37906
    61
"----------- ### thes2file ... Exception- Match raised -----------";
neuper@55490
    62
writeln "what to do when you get, e.g. \n\
neuper@37906
    63
\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\"]\n\
neuper@37906
    64
\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"integration_rules\"]\n\
neuper@37906
    65
\### thes2file: id = [\"IsacKnowledge\",\"Integrate\",\"Rulesets\",\"add_new_c\"]\n\
neuper@55490
    66
\Exception- Match raised\n";
neuper@55490
    67
;
neuper@37906
    68
val theID = ["IsacKnowledge","Integrate","Rulesets","add_new_c"];
neuper@37906
    69
val thydata = get_the theID;
neuper@55490
    70
;
neuper@55490
    71
(* HERE WE DO NOT create a file ...
neuper@55490
    72
thydata2file "/tmp/" [] theID thydata (*reports Exception- Match in question*);
neuper@37906
    73
*)
neuper@55490
    74
;
neuper@55490
    75
thydata2xml (theID, thydata) (*reported Exception- Match in question*);
wneuper@59262
    76
val i = 2;
neuper@55490
    77
;
neuper@55490
    78
val (theID:theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) = (theID, thydata);
neuper@55490
    79
rls2xml i thy_rls            (*reported Exception- Match in question*);
neuper@55490
    80
;
neuper@37906
    81
val (j, (thyID, Seq data)) = (i, thy_rls);
neuper@55490
    82
rls2xml j (thyID, Seq data)  (*reported Exception- Match in question*);
neuper@55490
    83
;
neuper@55490
    84
val (j, (thyID, Seq {id, preconds, rew_ord=(ord,_), erls, errpatts, srls, calc, rules, scr})) = 
neuper@55490
    85
  (j, (thyID, Seq data));
neuper@55490
    86
;
neuper@55490
    87
rules2xml (j+2*i) thyID rules  (*reports Exception- Match in question*);
neuper@55490
    88
(*TODO: Calc + Cal1 in datatypes.sml *)
neuper@42407
    89
neuper@55493
    90
"----------- search for data error in thes2file ------------------";
neuper@55493
    91
"----------- search for data error in thes2file ------------------";
neuper@55493
    92
"----------- search for data error in thes2file ------------------";
neuper@42407
    93
val TESTdump = Unsynchronized.ref 
neuper@42407
    94
  ("path": path, ["ids"]: theID, []: pos, thydata2file, Ptyp ("xxx", [], []): thydata ptyp);
neuper@42407
    95
neuper@42407
    96
fun TESTthenode (pa:path) ids po wfn (Ptyp (id, [n], ns)) TESTids = 
neuper@42407
    97
    let val po' = lev_on po
neuper@42407
    98
    in 
neuper@42407
    99
      if (ids@[id]) = TESTids
neuper@42407
   100
      then
neuper@42407
   101
        (TESTdump := (pa, ids, po', wfn, (Ptyp (id, [n], ns))); 
neuper@42407
   102
          error "stopped before error, created TESTdump") (* this exn creates right signature*)
neuper@42407
   103
      else
neuper@42407
   104
        wfn pa po' (ids @ [id]) n; TESTthenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns TESTids
neuper@42407
   105
    end
neuper@42407
   106
and TESTthenodes _ _ _ _ [] _ = ()
neuper@42407
   107
  | TESTthenodes pa ids po wfn (n::ns) TESTids =
neuper@42407
   108
      (TESTthenode pa ids po wfn n TESTids; TESTthenodes pa ids (lev_on po) wfn ns TESTids);
neuper@42407
   109
neuper@42407
   110
(* /--- side effects from previous test files ---\*)
neuper@42407
   111
    val i = indentation;
neuper@42407
   112
    val j = indentation;
neuper@42407
   113
(* \--- side effects from previous test files ---/*)
neuper@55490
   114
neuper@55490
   115
"~~~~~ fun thes2file, args:"; val (p : path) = ("/tmp/");
neuper@55494
   116
(* recursively descend into thehier just before the error
neuper@55494
   117
   by setting TESTids according to the last line in ouput 
neuper@55494
   118
   ### thes2file: id = : *)
neuper@55494
   119
(TESTthenodes p [] [0] thydata2file (get_thes ()) 
neuper@55494
   120
  ["IsacKnowledge","Rational","Rulesets","norm_Rational_parenthesized"] 
neuper@42407
   121
handle _(* "stopped before error, created TESTdump" *) => ());
neuper@55492
   122
;
neuper@55494
   123
(* /----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----\*)
neuper@55408
   124
val (pa, ids, po', wfn, (Ptyp (id, [n], ns))) = ! TESTdump; 
neuper@55490
   125
;
neuper@42407
   126
"~~~~~ fun thydata2file, args:"; val ((xmldata:path), (pos:pos), (theID:theID), thydata) =
neuper@42407
   127
  (pa, po', (ids@[id]), n);
neuper@42407
   128
"~~~~~ fun thydata2xml, args:"; val (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
neuper@42407
   129
  (theID:theID, thydata);
neuper@42407
   130
"~~~~~ fun rls2xml, args:"; val (j, (thyID, Seq data)) = (i, thy_rls);
neuper@42407
   131
"~~~~~ fun rls2xm, args:"; val (j, (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
neuper@42451
   132
		      srls, calc, errpatts, rules, scr})) = (j, (thyID, "Seq", data));
neuper@42407
   133
"~~~~~ fun rules2xml, args:"; val (j, thyID, (r::rs)) = ((j+2*i), thyID, rules);
neuper@42407
   134
"~~~~~ fun rule2xml, args:"; val (j, thyID, (Rls_ rls)) = (j, thyID, r);
neuper@42407
   135
val rls' = (#id o rep_rls) rls;
neuper@55494
   136
(* \----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----/
neuper@55494
   137
  another way to tackle this kind of error is shown in
neuper@55494
   138
"----------- thes2file: thy_containing_rls : rls '...' not in ! --";   ------------------------*)
neuper@55494
   139
neuper@55494
   140
"----------- thes2file: thy_containing_rls : rls '...' not in ! --";
neuper@55494
   141
"----------- thes2file: thy_containing_rls : rls '...' not in ! --";
neuper@55494
   142
"----------- thes2file: thy_containing_rls : rls '...' not in ! --";
neuper@55494
   143
val theID = ["IsacKnowledge","Rational","Rulesets","norm_Rational_parenthesized"]
neuper@55494
   144
val thydata = get_the theID
neuper@55494
   145
;
neuper@55494
   146
thydata2xml (theID, thydata);
neuper@42407
   147
wneuper@59188
   148
"----------- fun Thm.make_thm ------------------------------------";
wneuper@59188
   149
"----------- fun Thm.make_thm ------------------------------------";
wneuper@59188
   150
"----------- fun Thm.make_thm ------------------------------------";
wneuper@59188
   151
"~~~~~ fun Thm.make_thm, args:"; val (thy, part, (thmID : thmID, thm), (mathauthors : authors)) =
neuper@42411
   152
  (@{theory "Biegelinie"}, "IsacKnowledge",
wneuper@59188
   153
    ("Belastung_Querkraft", Thm.prop_of @{thm Belastung_Querkraft}),
neuper@42411
   154
	      ["Walther Neuper 2005 supported by a grant from NMI Austria"]);
neuper@42411
   155
    val guh = thm2guh (part, theory2thyID thy) thmID
neuper@42411
   156
    val theID = guh2theID guh;
neuper@42411
   157
if guh = "thy_isac_Biegelinie-thm-Belastung_Querkraft" andalso
neuper@42411
   158
  theID = ["IsacKnowledge", "Biegelinie", "Theorems", "Belastung_Querkraft"]
neuper@42411
   159
then () else error "store_thm: guh | theID changed";
neuper@42411
   160
neuper@55415
   161
"----------- correct theIDs for e_rls ----------------------------";
neuper@55415
   162
"----------- correct theIDs for e_rls ----------------------------";
neuper@55415
   163
"----------- correct theIDs for e_rls ----------------------------";
neuper@55458
   164
if thy_containing_rls "Build_Thydata" "e_rls" = ("IsacScripts", "KEStore") then ()
neuper@55415
   165
else error "thy_containing_rls e_rls changed";
neuper@55415
   166
show_thes ();
neuper@55415
   167
(*shows different assignment for "e_rls"...
neuper@55415
   168
  : 
neuper@55415
   169
                                                ["IsacScripts", "KEStore", "Rulesets", "e_rls"], 
neuper@55415
   170
  :*)
neuper@55415
   171
neuper@55484
   172
"----------- fun revert_sym --------------------------------------";
neuper@55484
   173
"----------- fun revert_sym --------------------------------------";
neuper@55484
   174
"----------- fun revert_sym --------------------------------------";
wneuper@59592
   175
val thy = @{theory Isac_Knowledge}
neuper@55484
   176
val (Thm (thmID, thm)) =
neuper@55484
   177
  revert_sym thy (Thm ("sym_real_mult_minus1", num_str (@{thm real_mult_minus1} RS @{thm sym})))
neuper@55484
   178
;
wneuper@59589
   179
if thmID = "Poly.real_mult_minus1" andalso string_of_thmI thm = "-1 * ?z = - ?z"
neuper@55484
   180
then () else error "fun revert_sym changed 1";
neuper@55484
   181
neuper@55484
   182
val (Thm (thmID, thm)) =
neuper@55484
   183
  revert_sym thy (Thm ("real_diff_minus", num_str @{thm real_diff_minus}))
neuper@55484
   184
;
neuper@55484
   185
if thmID = "Root.real_diff_minus" andalso string_of_thmI thm = "?a - ?b = ?a + -1 * ?b"
neuper@55484
   186
then () else error "fun revert_sym changed 2"
neuper@55484
   187
neuper@55484
   188
"----------- fun thms_of_rlss ------------------------------------";
neuper@55484
   189
"----------- fun thms_of_rlss ------------------------------------";
neuper@55484
   190
"----------- fun thms_of_rlss ------------------------------------";
neuper@55484
   191
val rlss = 
neuper@55484
   192
  [("e_rls" : rls', ("KEStore": theory', e_rls)),
neuper@55484
   193
  ("discard_minus" : rls', ("Poly": theory', discard_minus))]
neuper@55484
   194
;
neuper@55484
   195
val [_, (thmID, term)] = thms_of_rlss thy rlss;
neuper@55484
   196
(*
neuper@55484
   197
if thmID = "real_mult_minus1" (* WAS "??.unknown" *)
neuper@55484
   198
then () else error "thms_of_rlss changed"
neuper@55484
   199
*)
neuper@55484
   200
;
wneuper@59592
   201
"~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac_Knowledge}, rlss);
neuper@55484
   202
val rlss' = (rlss : (rls' * (theory' * rls)) list)
neuper@55484
   203
  |> map (thms_of_rls o #2 o #2)
neuper@55484
   204
    (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"), 
neuper@55484
   205
      Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*)
neuper@55484
   206
  |> flat
neuper@55484
   207
    (* = [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"), 
neuper@55484
   208
      Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]*)
neuper@55484
   209
  |> map (revert_sym thy)
neuper@55484
   210
    (* = [Thm ("Poly.real_diff_minus", "?a - ?b = ?a + -1 * ?b"), 
neuper@55484
   211
      Thm ("Delete.real_mult_minus1", "-1 * ?z = - ?z")] : rule list*)
wneuper@59188
   212
  |> map (fn Thm (thmID, thm) => (thmID, Thm.prop_of thm))
neuper@55484
   213
    (* = [("Poly.real_diff_minus", Const ("HOL.Trueprop", "bool \<Rightarrow> prop") $ ...,
neuper@55484
   214
      ("Delete.real_mult_minus1", Const ("HOL.Trueprop", ...)] : (string * term) list*)
neuper@55490
   215
  |> gen_distinct (fn ((thmID1, thm1), (thmID2, thm2)) => thmID1 = thmID2);
neuper@55484
   216
neuper@55492
   217
"----------- repair thydata2xml for rls --------------------------";
neuper@55492
   218
"----------- repair thydata2xml for rls --------------------------";
neuper@55492
   219
"----------- repair thydata2xml for rls --------------------------";
neuper@55492
   220
val theID = ["IsacKnowledge", "Poly", "Rulesets", "expand"]
neuper@55492
   221
val hrls = get_the theID
neuper@55492
   222
;
neuper@55492
   223
if thydata2xml (theID, hrls) = ("<RULESETDATA>\n" ^
neuper@55492
   224
"  <GUH> thy_isac_Poly-rls-expand </GUH>\n" ^
neuper@55492
   225
"  <STRINGLIST>\n" ^
neuper@55492
   226
"    <STRING> IsacKnowledge </STRING>\n" ^
neuper@55492
   227
"    <STRING> Poly </STRING>\n" ^
neuper@55492
   228
"    <STRING> Rulesets </STRING>\n" ^
neuper@55492
   229
"    <STRING> expand </STRING>\n" ^
neuper@55492
   230
"  </STRINGLIST>\n  <RULESET>\n" ^
neuper@55492
   231
"    <ID> expand </ID>\n" ^
neuper@55492
   232
"    <TYPE> Rls </TYPE>\n" ^
neuper@55492
   233
"    <RULES>\n" ^
neuper@55494
   234
"      <RULE>\n" ^                                            
neuper@55492
   235
"        <TAG> Theorem </TAG>\n" ^
neuper@55492
   236
"        <STRING> distrib_right </STRING>\n" ^
neuper@55492
   237
"        <GUH> thy_isac_distrib_right-thm-distrib_right </GUH>\n" ^
neuper@55492
   238
"      </RULE>\n" ^
neuper@55492
   239
"      <RULE>\n" ^
neuper@55492
   240
"        <TAG> Theorem </TAG>\n" ^
neuper@55492
   241
"        <STRING> distrib_left </STRING>\n" ^
neuper@55492
   242
"        <GUH> thy_isac_distrib_left-thm-distrib_left </GUH>\n" ^
neuper@55492
   243
"      </RULE>\n" ^
neuper@55492
   244
"    </RULES>\n" ^
neuper@55492
   245
"    <PRECONDS>     </PRECONDS>\n" ^
neuper@55492
   246
"    <ORDER>\n" ^
neuper@55492
   247
"      <STRING> dummy_ord </STRING>\n" ^
neuper@55492
   248
"    </ORDER>\n" ^
neuper@55492
   249
"    <ERLS>\n" ^
neuper@55492
   250
"      <TAG> Ruleset </TAG>\n" ^
neuper@55492
   251
"      <STRING> e_rls </STRING>\n" ^
neuper@55492
   252
"      <GUH> thy_isac_Poly-rls-e_rls </GUH>\n" ^
neuper@55492
   253
"    </ERLS>\n" ^
neuper@55492
   254
"    <SRLS>\n" ^
neuper@55492
   255
"      <TAG> Ruleset </TAG>\n" ^
neuper@55492
   256
"      <STRING> e_rls </STRING>\n" ^
neuper@55492
   257
"      <GUH> thy_isac_Poly-rls-e_rls </GUH>\n" ^
neuper@55492
   258
"    </SRLS>\n" ^
neuper@55492
   259
"    <SCRIPT>\n" ^
neuper@55492
   260
"      <MATHML>\n" ^
wneuper@59549
   261
"        <ISA> auto_generated t_t =\nRepeat\n" ^
wneuper@59549
   262
" ((Try (Repeat (Rewrite ''distrib_right'' False)) @@\n" ^
wneuper@59549
   263
"   Try (Repeat (Rewrite ''distrib_left'' False)))\n" ^
wneuper@59549
   264
"   ??.empty) </ISA>\n" ^
neuper@55492
   265
"      </MATHML>\n" ^
neuper@55492
   266
"    </SCRIPT>\n" ^
neuper@55492
   267
"  </RULESET>\n" ^
neuper@55492
   268
"  <EXPLANATIONS> </EXPLANATIONS>\n" ^
neuper@55492
   269
"  <MATHAUTHORS>\n" ^
neuper@55492
   270
"    <STRING> isac-team </STRING>\n" ^
neuper@55492
   271
"  </MATHAUTHORS>\n" ^
wneuper@59549
   272
"  <COURSEDESIGNS>\n" ^
wneuper@59549
   273
"  </COURSEDESIGNS>\n" ^
neuper@55492
   274
"</RULESETDATA>\n") then ()
wneuper@59549
   275
else error "thydata2xml for rls changed";
neuper@55492
   276
neuper@55490
   277
"----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
neuper@55490
   278
"----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
neuper@55490
   279
"----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
neuper@55490
   280
  val isacrlsthms = KEStore_Elems.get_rlss @{theory Test_Build_Thydata}
neuper@55490
   281
(*                         CHANGE FOR CODE ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
neuper@55490
   282
    |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "list_rls" (*unpleasant in test*)
neuper@55490
   283
    |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "e_rrls"   (*unpleasant in test*)
neuper@55490
   284
    |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "e_rls"    (*unpleasant in test*)
neuper@55490
   285
    |> thms_of_rlss @{theory}            (*length =  4*)
neuper@55490
   286
neuper@55490
   287
  val rlsthmsNOTisac = isacrlsthms       (*length =  2*)
neuper@55490
   288
    |> filter (fn (deriv, _) => 
neuper@55490
   289
      member op= (map Context.theory_name isabthys') (thyID_of_derivation_name deriv))
neuper@55490
   290
;
neuper@55490
   291
val (knowthys', progthys') = ([@{theory Test_Build_Thydata}], [@{theory Test_Build_Thydata}])
neuper@55490
   292
;
neuper@55490
   293
val thydata_list = 
neuper@55490
   294
  collect_part       "IsacKnowledge" knowledge_parent knowthys' @
neuper@55490
   295
  (map (collect_isab "Isabelle") rlsthmsNOTisac) @
neuper@55490
   296
  collect_part       "IsacScripts" proglang_parent progthys' (* only the thms, no rls *)
neuper@55490
   297
;
neuper@55490
   298
case thydata_list of                     (*length =  8*)
neuper@55490
   299
  [(["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],
neuper@55490
   300
    Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm111", 
neuper@55490
   301
    mathauthors = ["isac-team"], thm = _}),
neuper@55490
   302
  (["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm222"],
neuper@55490
   303
    Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm222", 
neuper@55490
   304
    mathauthors = ["isac-team"], thm = _}),
neuper@55490
   305
  (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls111"],
neuper@55490
   306
    Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls111", 
neuper@55490
   307
    mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rls _)}),
neuper@55490
   308
  (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls222"],
neuper@55490
   309
    Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls222", 
neuper@55490
   310
    mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rls _)}),
neuper@55490
   311
  (["Isabelle", "HOL", "Theorems", "refl"],
neuper@55490
   312
    Hthm {coursedesign = [], fillpats = [], guh = "thy_isab_HOL-thm-refl", 
neuper@55490
   313
    mathauthors = ["Isabelle team, TU Munich"], thm = _}),
neuper@55490
   314
  (["Isabelle", "Fun", "Theorems", "o_def"], Hthm {coursedesign = [], fillpats = [], 
neuper@55490
   315
    guh = "thy_isab_Fun-thm-o_def", mathauthors = ["Isabelle team, TU Munich"], thm = _}),
neuper@55490
   316
  (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm111"],
neuper@55490
   317
    Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm111", 
neuper@55490
   318
    mathauthors = ["isac-team"], thm = _}),
neuper@55490
   319
  (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm222"],
neuper@55490
   320
    Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm222", 
neuper@55490
   321
    mathauthors = ["isac-team"], thm = _})] => ()
neuper@55490
   322
| _ => error "collect thydata from Test_Build_Thydata changed";
neuper@55490
   323
;
neuper@55490
   324
(* we store locally on MINIthehier instead on KEStore, see KEStore: *)
neuper@55490
   325
    fun add_the (thydata, theID) = add_thydata ([], theID) thydata;
neuper@55490
   326
val thes = map (fn (a, b) => (b, a)) thydata_list
neuper@55490
   327
val MINIthehier = (fold add_the thes) (KEStore_Elems.get_thes @{theory Test_Build_Thydata});
neuper@55490
   328
neuper@55490
   329
"----------- ..CONTINUED: we adapt some required MINIfunctions ---";
neuper@55490
   330
"----------- ..CONTINUED: we adapt some required MINIfunctions ---";
neuper@55490
   331
"----------- ..CONTINUED: we adapt some required MINIfunctions ---";
neuper@55490
   332
fun MINIget_the (theID : theID) = get_py MINIthehier theID theID (*see ptyps.sml*)
neuper@55490
   333
fun MINIthy_hierarchy2file (path:path) = 
neuper@55490
   334
  str2file (path ^ "thy_hierarchy.xml") 
neuper@55490
   335
    ("<NODE>\n" ^
neuper@55490
   336
    "  <ID> theory hierarchy </ID>\n" ^
neuper@55490
   337
    "  <NO> 1 </NO>\n" ^
neuper@55490
   338
    "  <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^
neuper@55490
   339
    (hierarchy_guh MINIthehier) ^
neuper@55490
   340
    "</NODE>");
neuper@55490
   341
fun MINIthes2file (p : path) = thenodes p [] [0] thydata2file MINIthehier;
neuper@55490
   342
neuper@55490
   343
"----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
neuper@55490
   344
"----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
neuper@55490
   345
"----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
neuper@55490
   346
case MINIget_the ["IsacScripts", "Test_Build_Thydata", "Theorems", "thm111"] of
neuper@55490
   347
  Hthm {guh = "thy_scri_Test_Build_Thydata-thm-thm111", ...} => ()
neuper@55490
   348
| _ => error "MINIget_the thm111 changed"
neuper@55490
   349
;
neuper@55490
   350
val path = "/tmp/"
neuper@55490
   351
;
neuper@55490
   352
MINIthy_hierarchy2file path            (* ---> /tmp/thy_hierarchy.xml *);
neuper@55490
   353
writeln (file2str path "thy_hierarchy.xml") (* better check in editor *)
neuper@55490
   354
;
neuper@55490
   355
MINIthes2file path                               (* ---> /tmp/thy_... *);
neuper@55490
   356
neuper@55490
   357
"----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
neuper@55490
   358
"----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
neuper@55490
   359
"----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
neuper@55490
   360
"~~~~~ fun MINIthes2file, args:"; val (path) = ("/tmp/");
neuper@55490
   361
"~~~~~ and thenodes, args:"; val (pa, ids, po, wfn, (n::ns)) = 
neuper@55490
   362
  (path, [], [0], thydata2file, MINIthehier);
neuper@55490
   363
"~~~~~ fun thenode, args:"; val ((pa : path), ids, po, wfn, (Ptyp (id, [n], ns))) = 
neuper@55490
   364
  (pa, ids, po, wfn, n);
neuper@55490
   365
val po' = lev_on po;
neuper@55490
   366
(*wfn pa po' (ids @ [id]) n  -------------> writes xml to file; we want xml before written: *)
neuper@55490
   367
neuper@55490
   368
(* we take (theID, thydata) from thydata_list ABOVE: *)
neuper@55490
   369
case hd thydata_list of
neuper@55490
   370
  (["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],
neuper@55490
   371
    Hthm {guh = "thy_isac_Test_Build_Thydata-thm-thm111", mathauthors = ["isac-team"], ...}) => ()
neuper@55490
   372
| _ => error "a change inhibits successful continuation of this test";
neuper@55490
   373
val (theID, thydata) = hd thydata_list;
neuper@55490
   374
"~~~~~ fun thydata2file, args:"; val ((path : path), (pos : pos), (theID : theID), thydata) =
neuper@55490
   375
  (pa, po', (*ids @ [id]*)theID, (*n*)thydata);
neuper@55490
   376
"~~~~~ fun thydata2xml, args:"; val ((theID, Hthm {guh, coursedesign, mathauthors, fillpats, thm}))=
neuper@55490
   377
  ((theID, thydata));
neuper@55490
   378
"~~~~~ to str2file return val:"; val (xml) = 
neuper@55490
   379
      "<THEOREMDATA>\n" ^
neuper@55490
   380
      indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
neuper@55490
   381
      id2xml i theID ^
neuper@55490
   382
      thm''2xml i thm ^
neuper@55490
   383
      indt i ^ "<PROOF>\n" ^
neuper@55490
   384
      extref2xml (i+i) "Proof of the theorem" 
neuper@55490
   385
	      ("http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/" ^
neuper@55490
   386
	        nth 2 theID ^ ".html") ^
neuper@55490
   387
	    indt i ^  "</PROOF>\n" ^
neuper@55490
   388
	    indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
neuper@55490
   389
	    authors2xml i "MATHAUTHORS" mathauthors ^
neuper@55490
   390
	    authors2xml i "COURSEDESIGNS" coursedesign ^
neuper@55490
   391
	    "</THEOREMDATA>\n"
neuper@55490
   392
;
neuper@55490
   393
if xml = ("<THEOREMDATA>\n" ^
neuper@55490
   394
"  <GUH> thy_isac_Test_Build_Thydata-thm-thm111 </GUH>\n" ^
neuper@55490
   395
"  <STRINGLIST>\n" ^
neuper@55490
   396
"    <STRING> IsacKnowledge </STRING>\n" ^
neuper@55490
   397
"    <STRING> Test_Build_Thydata </STRING>\n" ^
neuper@55490
   398
"    <STRING> Theorems </STRING>\n" ^
neuper@55490
   399
"    <STRING> thm111 </STRING>\n" ^
neuper@55490
   400
"  </STRINGLIST>\n" ^
neuper@55490
   401
"  <THEOREM>\n" ^
neuper@55490
   402
"    <ID> thm111 </ID>\n" ^
neuper@55490
   403
"    <MATHML>\n" ^
neuper@55490
   404
"      <ISA> ?thm111.0 = ?thm111.0 + 111 </ISA>\n" ^
neuper@55490
   405
"    </MATHML>\n" ^
neuper@55490
   406
"  </THEOREM>\n" ^
neuper@55490
   407
"  <PROOF>\n" ^
neuper@55490
   408
"    <EXTREF>\n" ^
neuper@55490
   409
"      <TEXT> Proof of the theorem </TEXT>\n" ^
neuper@55490
   410
"      <URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Test_Build_Thydata.html </URL>\n" ^
neuper@55490
   411
"    </EXTREF>\n" ^
neuper@55490
   412
"  </PROOF>\n" ^
neuper@55490
   413
"  <EXPLANATIONS> </EXPLANATIONS>\n" ^
neuper@55490
   414
"  <MATHAUTHORS>\n" ^
neuper@55490
   415
"    <STRING> isac-team </STRING>\n" ^
neuper@55490
   416
"  </MATHAUTHORS>\n" ^
neuper@55490
   417
"  <COURSEDESIGNS>\n" ^
neuper@55490
   418
"  </COURSEDESIGNS>\n" ^
neuper@55490
   419
"</THEOREMDATA>\n") then () else error "thy_isac_Test_Build_Thydata-thm-thm111.xml changed"
neuper@55490
   420