wneuper/isa: test/Tools/isac/xmlsrc/datatypes.sml@ddfabb53082c

     1 (* Title: test for sml/xmlsrc/datatypes.sml

     2    Authors: Walther Neuper 2003

     3    (c) due to copyright terms

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

     6 use"datatypes.sml";

     7 *)

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

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

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

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

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

    14 "----------- fun xml_of_model ------------------------------------------------------------------";

    15 "----------- fun xml_of_tac --------------------------------------------------------------------";

    16 "----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";

    17 "----------- fun xml_of_tac: StringListTactic --------------------------------------------------";

    18 "----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";

    19 "-----------------------------------------------------------------";

    20 "-----------------------------------------------------------------";

    21 "-----------------------------------------------------------------";

    25 "----------- fun rules2xml ---------------------------------------";

    26 "----------- fun rules2xml ---------------------------------------";

    27 "----------- fun rules2xml ---------------------------------------";

    29 show_thes();

    30 val thyID = "Test";

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

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

    34 (*AK110725

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

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

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

    38 (*get_py  (Thy_Info.get_theory "Pure") theID theID (get_thes ());

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

    40 (*default_print_depth 3; 999*)

    41 (get_thes ());

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

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

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

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

    47 *)

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

    51 (*for rule2xml...*)

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

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

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

    55 writeln (rules2xml 2 "Test" rules);

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

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

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

    62 show_thes();

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

    64 val thydata = get_the theID;

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

    66 writeln(thydata2xml (theID, thydata));

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

    68 "----------------------------^^^---------^^^------------";

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

    73    *)

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

    76 "----------- fun xml_of_model ------------------------------------------------------------------";

    77 "----------- fun xml_of_model ------------------------------------------------------------------";

    78 "----------- fun xml_of_model ------------------------------------------------------------------";

    79 (*create testdata: see --- tryrefine ---

    80   xml_of_model used via refineProblem \<longrightarrow> matchpbl2xml \<longrightarrow> model2xml*)

    81 reset_states ();

    82 CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",

    83 	    "solveFor x", "solutions L"],

    84 	   ("RatEq",["univariate","equation"],["no_met"]))];

    85 Iterator 1;

    86 moveActiveRoot 1; autoCalculate 1 CompleteCalc;

    87 refineProblem 1 ([1],Res) "pbl_equ_univ";

    88 "~~~~~ fun refineProblem, args:"; val (cI, ((p,p_) : pos'), (guh : guh)) =

    89   (1, ([1],Res), "pbl_equ_univ");

    90 val pblID = guh2kestoreID guh

    91 	 val ((pt,_),_) = get_calc cI

    92 	 val pp = par_pblobj pt p

    93 	 val chd = tryrefine pblID pt (pp, p_);

    94 "~~~~~ fun matchpbl2xml, args:"; val ((cI:calcID), (model_ok, pI, hdl, pbl, pre)) = (cI, chd);

    95 "~~~~~ fun model2xml, args:"; val (j, (itms:itm list), where_) = (i, pbl, pre);

    96 "~~~~~ fun xml_of_model, args:"; val (itms, where_) = (pbl, pre);

    97 val xxx = xml_of_model itms where_;

    98 (xmlstr 0 xxx);

    99 writeln(xmlstr 0 xxx);

   100 if xmlstr 0 xxx = "(MODEL)\n. (GIVEN)\n. . (ITEM status=correct)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . equality (x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 / x)\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/ITEM)\n. . (ITEM status=correct)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . solveFor x\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/ITEM)\n. (/GIVEN)\n. (WHERE)\n. . (ITEM status=correct)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) =\n1 / x is_ratequation_in x\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/ITEM)\n. (/WHERE)\n. (FIND)\n. . (ITEM status=correct)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . solutions L\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/ITEM)\n. (/FIND)\n. (RELATE)\n. (/RELATE)\n(/MODEL)\n"

   101 then () else error ("xml_of_model changed = " ^ xmlstr 0 xxx);

   103 "----------- fun xml_of_tac --------------------------------------------------------------------";

   104 "----------- fun xml_of_tac --------------------------------------------------------------------";

   105 "----------- fun xml_of_tac --------------------------------------------------------------------";

   106 (* WN150814 these are the Java objects.

   107 import isac.util.tactics.RewriteInst

   108 import isac.util.tactics.RewriteSet

   109 import isac.util.tactics.RewriteSetInst

   110 import isac.util.tactics.SimpleTactic        ...not appropriately abstracted

   111 import isac.util.tactics.StringListTactic    ...not appropriately abstracted

   112 import isac.util.tactics.SubProblemTactic

   113 import isac.util.tactics.Tactic

   114 *)

   115 Rewrite: thm'' -> tac;

   116 val tac = Rewrite("refl", @{thm refl});

   117 if xmlstr 0 (xml_of_tac tac) =

   118 (*---xml_of_tac------------------------------------------thm'_to_thm''--------------

   119 "(REWRITETACTIC name=Rewrite)\n" ^

   120 ". (THEOREM)\n" ^

   121 ". . (ID)\n" ^

   122 ". . . refl\n" ^

   123 ". . (/ID)\n" ^

   124 ". . (FORMULA)\n" ^

   125 ". . . (ISA)\n" ^

   126 ". . . . a = a\n" ^

   127 ". . . (/ISA)\n" ^

   128 ". . . (TERM)\n" ^

   129 ". . . . ?t = ?t\n" ^

   130 ". . . (/TERM)\n" ^

   131 ". . (/FORMULA)\n" ^

   132 ". (/THEOREM)\n" ^

   133 -----xml_of_tac------------------------------------------thm'_to_thm''------------*)

   134 "(REWRITETACTIC name=Rewrite)\n" ^

   135 ". (THEOREM)\n" ^

   136 ". . (ID)\n" ^

   137 ". . . refl\n" ^

   138 ". . (/ID)\n" ^

   139 ". . (FORMULA)\n" ^

   140 ". . . ?t = ?t\n" ^

   141 ". . (/FORMULA)\n" ^

   142 ". (/THEOREM)\n" ^

   143 "(/REWRITETACTIC)\n" then () else error "xml_of_tac Rewrite CHANGED";

   145 Rewrite_Inst: subs * thm'' -> tac;

   146 val tac = Rewrite_Inst(["(bdv, x)"], ("refl", @{thm refl}));

   147 if xmlstr 0 (xml_of_tac tac) =

   148 "(REWRITEINSTTACTIC name=Rewrite_Inst)\n" ^

   149 ". (SUBSTITUTION)\n" ^

   150 ". . (PAIR)\n" ^

   151 ". . . (VARIABLE)\n" ^

   152 ". . . . (MATHML)\n" ^ (* TODO *)

   153 ". . . . . (ISA)\n" ^

   154 ". . . . . . bdv\n" ^

   155 ". . . . . (/ISA)\n" ^

   156 ". . . . (/MATHML)\n" ^

   157 ". . . (/VARIABLE)\n" ^

   158 ". . . (VALUE)\n" ^

   159 ". . . . (MATHML)\n" ^

   160 ". . . . . (ISA)\n" ^

   161 ". . . . . . x\n" ^

   162 ". . . . . (/ISA)\n" ^

   163 ". . . . (/MATHML)\n" ^

   164 ". . . (/VALUE)\n" ^

   165 ". . (/PAIR)\n" ^

   166 ". (/SUBSTITUTION)\n" ^

   167 (*---xml_of_tac------------------------------------------thm'_to_thm''--------------

   168 ". (THEOREM)\n" ^

   169 ". . (ID)\n" ^

   170 ". . . refl\n" ^

   171 ". . (/ID)\n" ^

   172 ". . (FORMULA)\n" ^  (* OK *)

   173 ". . . (ISA)\n" ^

   174 ". . . . a = a\n" ^

   175 ". . . (/ISA)\n" ^

   176 ". . . (TERM)\n" ^

   177 ". . . ?t = ?t\n" ^

   178 ". . . (/TERM)\n" ^

   179 ". . (/FORMULA)\n" ^

   180 ". (/THEOREM)\n" ^

   181 -----xml_of_tac------------------------------------------thm'_to_thm''------------*)

   182 ". (THEOREM)\n" ^

   183 ". . (ID)\n" ^

   184 ". . . refl\n" ^

   185 ". . (/ID)\n" ^

   186 ". . (FORMULA)\n" ^

   187 ". . . ?t = ?t\n" ^

   188 ". . (/FORMULA)\n" ^

   189 ". (/THEOREM)\n" ^

   190 "(/REWRITEINSTTACTIC)\n" then () else error "xml_of_tac Rewrite_Inst CHANGED";

   192 Rewrite_Set: rls' -> tac;

   193 val tac = Rewrite_Set("simplify");

   194 if xmlstr 0 (xml_of_tac tac) = "(REWRITESETTACTIC name=Rewrite_Set)\n" ^

   195 ". simplify\n" ^

   196 "(/REWRITESETTACTIC)\n" then () else error "xml_of_tac Rewrite_Set CHANGED";

   198 Rewrite_Set_Inst: subs * rls' -> tac;

   199 val tac = Rewrite_Set_Inst(["(bdv, x)"], "simplify");

   200 if xmlstr 0 (xml_of_tac tac) =

   201 "(REWRITESETINSTTACTIC name=Rewrite_Set_Inst)\n" ^

   202 ". (SUBSTITUTION)\n" ^

   203 ". . (PAIR)\n" ^

   204 ". . . (VARIABLE)\n" ^

   205 ". . . . (MATHML)\n" ^ (* TODO *)

   206 ". . . . . (ISA)\n" ^

   207 ". . . . . . bdv\n" ^

   208 ". . . . . (/ISA)\n" ^

   209 ". . . . (/MATHML)\n" ^

   210 ". . . (/VARIABLE)\n" ^

   211 ". . . (VALUE)\n" ^

   212 ". . . . (MATHML)\n" ^

   213 ". . . . . (ISA)\n" ^

   214 ". . . . . . x\n" ^

   215 ". . . . . (/ISA)\n" ^

   216 ". . . . (/MATHML)\n" ^

   217 ". . . (/VALUE)\n" ^

   218 ". . (/PAIR)\n" ^

   219 ". (/SUBSTITUTION)\n" ^

   220 ". (RULESET)\n" ^

   221 ". . simplify\n" ^

   222 ". (/RULESET)\n" ^

   223 "(/REWRITESETINSTTACTIC)\n"then () else error "xml_of_tac Rewrite_Set_Inst CHANGED";

   226 "----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";

   227 "----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";

   228 "----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";

   230 "----------- these are : cterm' -> tac: WN150814 THESE WELL BECOME TermTactic TERMTACTIC";

   231 Add_Given: cterm' -> tac;

   232 Add_Find: cterm' -> tac;

   233 Add_Relation: cterm' -> tac;

   234 Check_elementwise: cterm' -> tac;

   235 Take: cterm' -> tac;

   237 Add_Given: cterm' -> tac;

   238 val tac = Add_Given("equality (x + 1 = 2)");

   239 xml_of_tac tac;(*

   240 <FORMTACTIC name="Add_Given">

   241   <MATHML>

   242     <ISA>equality (x + 1 = 2)</ISA>

   243   </MATHML>

   244 </FORMTACTIC>*)

   245 if xmlstr 0 (xml_of_tac tac) = "(FORMTACTIC name=Add_Given)\n. (MATHML)\n. . (ISA)\n. . . equality (x + 1 = 2)\n. . (/ISA)\n. (/MATHML)\n(/FORMTACTIC)\n"

   246 then () else error "xml_of_tac Add_Given CHANGED";

   248 "----------- these are : string -> tac: ";

   249 Calculate: string -> tac; (* should be the operator*)

   250 Specify_Theory: domID -> tac;

   251 val tac = Specify_Theory("Differentiate");

   252 xml_of_tac tac;(*

   253 <SIMPLETACTIC name="Specify_Theory">

   254   <MATHML>                               NONSENSE

   255     <ISA>Differentiate</ISA>

   256   </MATHML>

   257 </SIMPLETACTIC>*)

   258 if xmlstr 0 (xml_of_tac tac) = "(SIMPLETACTIC name=Specify_Theory)\n. Differentiate\n(/SIMPLETACTIC)\n"

   259 then () else error "xml_of_tac Specify_Theory CHANGED";

   261 "----------- fun xml_of_tac: StringListTactic --------------------------------------------------";

   262 "----------- fun xml_of_tac: StringListTactic --------------------------------------------------";

   263 "----------- fun xml_of_tac: StringListTactic --------------------------------------------------";

   264 Model_Problem: tac;

   265 Or_to_List: tac;

   267 Apply_Method: metID -> tac;

   268 Refine_Tacitly: pblID -> tac;

   269 Specify_Problem: pblID -> tac;

   270 Specify_Method: metID -> tac;

   271 Substitute: sube -> tac; (* Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT *)

   272 Check_Postcond: pblID -> tac;

   274 Apply_Method: metID -> tac;

   275 val tac = Apply_Method(["test", "equation", "simplify"]);

   276 xml_of_tac tac;(*

   277 <STRINGLISTTACTIC name="Apply_Method">

   278   <STRINGLIST>

   279     <STRING>test</STRING>

   280     <STRING>equation</STRING>

   281     <STRING>simplify</STRING>

   282   </STRINGLIST>

   283 </STRINGLISTTACTIC>*)

   284 if xmlstr 0 (xml_of_tac tac) = "(STRINGLISTTACTIC name=Apply_Method)\n. (STRINGLIST)\n. . (STRING)\n. . . test\n. . (/STRING)\n. . (STRING)\n. . . equation\n. . (/STRING)\n. . (STRING)\n. . . simplify\n. . (/STRING)\n. (/STRINGLIST)\n(/STRINGLISTTACTIC)\n"

   285 then () else error "xml_of_tac Apply_Method CHANGED";

   287 "----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";

   288 "----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";

   289 "----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";

   290 (* Note: tacs Substitute, Rewrite_Inst* have different substitutions,

   291 while input in frontend is not yet clear: *)

   292 Rewrite_Inst: subs * thm'' -> tac;

   293 Substitute  : sube -> tac;

   295 e_subs: cterm' list;

   296 e_subs: subs;

   297 val subs = ["(bdv_1, xxx)","(bdv_2, yyy)"]: cterm' list;

   298 xml_of_subs subs;(*

   299 <SUBSTITUTION>

   300   <PAIR>

   301     <VARIABLE>

   302       <MATHML>

   303         <ISA>bdv_1</ISA>

   304       </MATHML>

   305     </VARIABLE>

   306     <VALUE><

   307       MATHML>

   308         <ISA>xxx</ISA>

   309       </MATHML>

   310     </VALUE>

   311   </PAIR>

   312   <PAIR>

   313     <VARIABLE>

   314       <MATHML>

   315         <ISA>bdv_2</ISA>

   316       </MATHML>

   317     </VARIABLE>

   318     <VALUE>

   319       <MATHML>

   320         <ISA>yyy</ISA>

   321       </MATHML>

   322     </VALUE>

   323   </PAIR>

   324 </SUBSTITUTION>:*)

   325 val tac = Rewrite_Inst (subs, ("diff_sin_chain", @{thm diff_sin_chain}));

   326 val xml = xml_of_tac tac;

   328 if xmlstr 0 (xml_of_tac tac) = "(REWRITEINSTTACTIC name=Rewrite_Inst)\n. (SUBSTITUTION)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_1\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . xxx\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_2\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . yyy\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. (/SUBSTITUTION)\n. (THEOREM)\n. . (ID)\n. . . diff_sin_chain\n. . (/ID)\n. . (FORMULA)\n. . . d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\n. . (/FORMULA)\n. (/THEOREM)\n(/REWRITEINSTTACTIC)\n"

   329 then () else error "xml_of_tac Rewrite_Inst CHANGED";

   331 val Rewrite_Inst (["(bdv_1, xxx)", "(bdv_2, yyy)"], ("diff_sin_chain", term)) = xml_to_tac xml;

   332 if (term2str o Thm.prop_of) term = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"

   333 then () else error "xml_to_tac Rewrite_Inst CHANGED";

   335 val sube = ["(bdv_1 = xxx)", "(bdv_2 = yyy)"]: sube;

   336 e_sube: cterm' list;

   337 e_sube: sube;

   338 xml_of_sube sube;(*

   339 <SUBSTITUTION>

   340   <PAIR>

   341     <VARIABLE>

   342       <MATHML>

   343         <ISA>bdv_1</ISA>

   344       </MATHML>

   345     </VARIABLE>

   346     <VALUE>

   347       <MATHML>

   348         <ISA>xxx</ISA>

   349       </MATHML>

   350     </VALUE>

   351   </PAIR>

   352   <PAIR>

   353     <VARIABLE>

   354       <MATHML>

   355         <ISA>bdv_2</ISA>

   356       </MATHML>

   357     </VARIABLE>

   358     <VALUE>

   359       <MATHML>

   360         <ISA>yyy</ISA>

   361       </MATHML>

   362     </VALUE>

   363   </PAIR>

   364 </SUBSTITUTION>:*)

   365 val tac = Substitute sube;

   366 val xml = xml_of_tac tac;

   368 if xmlstr 0 (xml_of_tac tac) = "(STRINGLISTTACTIC name=Substitute)\n. (SUBSTITUTION)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_1\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . xxx\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_2\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . yyy\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. (/SUBSTITUTION)\n(/STRINGLISTTACTIC)\n"

   369 then () else error "xml_of_tac Substitute CHANGED";

   370 case xml_to_tac xml of Substitute ["bdv_1 = xxx", "bdv_2 = yyy"] => ()

   371 | _ => error "xml_to_tac Substitute CHANGED";

author	Walther Neuper <wneuper@ist.tugraz.at>
	Tue, 06 Feb 2018 16:18:43 +0100
changeset 59348	ddfabb53082c
parent 59253	f0bb15a046ae
child 59361	76b3141b73ab
permissions	-rw-r--r--