Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/xmlsrc/datatypes.sml
author Walther Neuper <neuper@ist.tugraz.at>
Mon, 02 Sep 2013 16:16:08 +0200
changeset 52101 c3f399ce32af
parent 42176 3573fd729e99
child 55421 107f40711818
permissions -rw-r--r--
Test_Isac works again, almost ..

4 files raise errors:
# Interpret/solve.sml: "solve.sml: interSteps on norm_Rational 2"
# Interpret/inform.sml: "inform.sml: [rational,simplification] 2"
# Knowledge/partial_fractions.sml: "autoCalculate for met_partial_fraction changed: final result"
# Knowledge/eqsystem.sml: "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed"

The chunk of changes is due to the fact, that Isac's code still is unstable.
The changes are accumulated since e8f46493af82. 
     1 (* Title: test for sml/xmlsrc/datatypes.sml

     2    Authors: Walther Neuper 2003

     3    (c) due to copyright terms

     4 

     5 use"../smltest/xmlsrc/datatypes.sml";

     6 use"datatypes.sml";

     7 *)

     8 

     9 "-----------------------------------------------------------------";

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

    11 "-----------------------------------------------------------------";

    12 "----------- fun rules2xml ---------------------------------------";

    13 "----------- fun thm''2xml ---------------------------------------";

    14 "-----------------------------------------------------------------";

    15 "-----------------------------------------------------------------";

    16 "-----------------------------------------------------------------";

    17 

    18 

    19 

    20 "----------- fun rules2xml ---------------------------------------";

    21 "----------- fun rules2xml ---------------------------------------";

    22 "----------- fun rules2xml ---------------------------------------";

    23 

    24 show_thes();

    25 val thyID = "Test";

    26 

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

    28 val thydata = get_the ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"];

    29 (*AK110725 

    30 (*val thydata = get_the ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]; 

    31   (* ERROR: get_pbt not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)

    32 "~~~~~ fun get_the, args:"; val (theID:theID) = (["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]);

    33 (*get_py  (Thy_Info.get_theory "Pure") theID theID (! thehier); 

    34   (* ERROR: get_pbt not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)

    35 print_depth 3; (*999*)

    36 (!thehier);

    37 

    38 (*"~~~~~ fun get_py, args:"; val (thy, d, _, []) = ((Thy_Info.get_theory "Pure"), theID, theID, (! thehier));*)

    39 "~~~~~ fun get_py, args:"; val (thy, d, _, [_]) = ((Thy_Info.get_theory "Pure"), theID, theID, (!thehier));

    40 error ("get_pbt not found: "^(strs2str d));

    41 (*AK110725 To be continued...s*)

    42 *)

    43 

    44 val Hrls {thy_rls = (_,Rls {rules = rules as rule::_,...}),...} = thydata;

    45 

    46 (*for rule2xml...*)

    47 val (j, thyID, Thm (thmID, thm)) = (2, thyID, rule);

    48 val (isa, thyID') = thy_containing_thm thyID thmID;

    49 val guh = thm2guh (isa, thyID') thmID;

    50 writeln (rules2xml 2 "Test" rules);

    51 

    52 

    53 "----------- fun thm''2xml ---------------------------------------";

    54 "----------- fun thm''2xml ---------------------------------------";

    55 "----------- fun thm''2xml ---------------------------------------";

    56 

    57 show_thes();

    58 val theID = ["IsacKnowledge", "Diff", "Theorems", "frac_conv"];

    59 val thydata = get_the theID;

    60 val Hthm {guh=guh, thm=thm, mathauthors=ma, coursedesign=co} = thydata;

    61 writeln(thydata2xml (theID, thydata));

    62 "----- check 'manually' ...0 &lt ?n |] ==&gt ?a... -----";

    63 "----------------------------^^^---------^^^------------";

    64 

    65 

    66 

    67 (* use"../smltest/xmlsrc/datatypes.sml";

    68    *)

    69 ============ inhibit exn AK110725 ==============================================*)
wneuper/isa