1.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Thu Aug 13 10:46:31 2015 +0200
1.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Fri Aug 14 10:01:33 2015 +0200
1.3 @@ -486,7 +486,7 @@
1.4 (XML.Elem (("ICALCHEAD", []), [
1.5 pos as XML.Elem (("POSITION", []), _),
1.6 headln as XML.Elem (("MATHML", []), _),
1.7 - imodel as XML.Elem (("MATHML", []), _),
1.8 + imodel as XML.Elem (("MATHML", []), _), (* TODO WN150813 ?!?*)
1.9 XML.Elem (("POS", []), [XML.Text belongsto]),
1.10 spec as XML.Elem (("SPECIFICATION", []), _)])) =
1.11 (xml_to_pos pos, xml_to_cterm headln, xml_to_imodel imodel,
1.12 @@ -547,11 +547,13 @@
1.13 fun xml_of_thm' ((ID, form) : thm') =
1.14 XML.Elem (("THEOREM", []), [
1.15 XML.Elem (("ID", []), [XML.Text ID]),
1.16 - XML.Elem (("FORMULA", []), [XML.Text form])])
1.17 + XML.Elem (("FORMULA", []), [
1.18 + XML.Text form])]) (* repair for MathML: use term instead String *)
1.19 fun xml_to_thm'
1.20 (XML.Elem (("THEOREM", []), [
1.21 XML.Elem (("ID", []), [XML.Text ID]),
1.22 - XML.Elem (("FORMULA", []), [XML.Text form])])) = ((ID, form) : thm')
1.23 + XML.Elem (("FORMULA", []), [(* repair for MathML: use term instead String *)
1.24 + XML.Text form])])) = ((ID, form) : thm')
1.25 | xml_to_thm' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
1.26
1.27 (*WN060627 scope of thy's not considered ?!?*)
1.28 @@ -775,14 +777,14 @@
1.29 | xml_of_tac (Refine_Tacitly pI) =
1.30 XML.Elem (("STRINGLISTTACTIC", [("name", "Refine_Tacitly")]), [xml_of_strs pI])
1.31 | xml_of_tac (Add_Given ct) =
1.32 - XML.Elem (("SIMPLETACTIC", [("name", "Add_Given")]), [xml_of_cterm ct])
1.33 + XML.Elem (("TERMTACTIC", [("name", "Add_Given")]), [xml_of_cterm ct])
1.34 | xml_of_tac (Add_Find ct) =
1.35 - XML.Elem (("SIMPLETACTIC", [("name", "Add_Find")]), [xml_of_cterm ct])
1.36 + XML.Elem (("TERMTACTIC", [("name", "Add_Find")]), [xml_of_cterm ct])
1.37 | xml_of_tac (Add_Relation ct) =
1.38 - XML.Elem (("SIMPLETACTIC", [("name", "Add_Relation")]), [xml_of_cterm ct])
1.39 + XML.Elem (("TERMTACTIC", [("name", "Add_Relation")]), [xml_of_cterm ct])
1.40 | xml_of_tac (Specify_Theory ct) =
1.41 - (*WN060513 Specify_Theory = fn : domID -> tac and domID is a string, not a cterm *)
1.42 - XML.Elem (("SIMPLETACTIC", [("name", "Specify_Theory")]), [xml_of_cterm ct])
1.43 + XML.Elem (("SIMPLETACTIC", [("name", "Specify_Theory")]), [XML.Text ct])
1.44 +
1.45 | xml_of_tac (Specify_Problem ct) =
1.46 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])
1.47 | xml_of_tac (Specify_Method ct) =
1.48 @@ -790,10 +792,10 @@
1.49 | xml_of_tac (Apply_Method mI) =
1.50 XML.Elem (("STRINGLISTTACTIC", [("name", "Apply_Method")]), [xml_of_strs mI])
1.51 | xml_of_tac (Take ct) =
1.52 - XML.Elem (("SIMPLETACTIC", [("name", "Take")]), [xml_of_cterm ct])
1.53 + XML.Elem (("TERMTACTIC", [("name", "Take")]), [xml_of_cterm ct])
1.54 | xml_of_tac (Calculate opstr) =
1.55 - (*WN060513 Calculate = fn : string -> tac 'string', _NOT_ 'cterm' ..flaw from RG*)
1.56 - XML.Elem (("SIMPLETACTIC", [("name", "Calculate")]), [xml_of_cterm opstr])
1.57 + XML.Elem (("SIMPLETACTIC", [("name", "Calculate")]), [XML.Text opstr])
1.58 +
1.59 | xml_of_tac (Rewrite thm') =
1.60 XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm' thm'])
1.61 | xml_of_tac (Rewrite_Inst (subs, thm')) =
1.62 @@ -807,15 +809,15 @@
1.63 XML.Elem (("RULESET", []), [XML.Text rls']) ::
1.64 xml_of_subs subs ::[]))
1.65 | xml_of_tac (Or_to_List) =
1.66 - XML.Elem (("STRINGLISTTACTIC", [("name", "Or_to_List")]), [])
1.67 + XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [])
1.68 +
1.69 | xml_of_tac (Check_elementwise ct) =
1.70 - XML.Elem (("SIMPLETACTIC", [("name", "Check_elementwise")]), [xml_of_cterm ct])
1.71 + XML.Elem (("TERMTACTIC", [("name", "Check_elementwise")]), [xml_of_cterm ct])
1.72 | xml_of_tac (Substitute cterms) =
1.73 - (*WN0605 quick and dirty: cterms is _NOT_ a stringlist like pblID...
1.74 - cterms2xml (j+i) cterms^ ....should be WN060514: TODO TERMLISTTACTIC?*)
1.75 + (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
1.76 XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_strs cterms])
1.77 | xml_of_tac (Check_Postcond pI) =
1.78 - XML.Elem (("STRINGLISTTACTIC", [("name", "Or_to_List")]), [xml_of_strs pI])
1.79 + XML.Elem (("STRINGLISTTACTIC", [("name", "Check_Postcond")]), [xml_of_strs pI])
1.80 | xml_of_tac tac = error ("xml_of_tac: not impl. for " ^ tac2str tac);
1.81 fun xml_to_tac
1.82 (XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
1.83 @@ -828,17 +830,18 @@
1.84 (XML.Elem (("STRINGLISTTACTIC", [
1.85 ("name", "Refine_Tacitly")]), [pI])) = Refine_Tacitly (xml_to_strs pI)
1.86 | xml_to_tac
1.87 - (XML.Elem (("SIMPLETACTIC", [
1.88 + (XML.Elem (("TERMTACTIC", [
1.89 ("name", "Add_Given")]), [ct])) = Add_Given (xml_to_cterm ct)
1.90 | xml_to_tac
1.91 - (XML.Elem (("SIMPLETACTIC", [
1.92 + (XML.Elem (("TERMTACTIC", [
1.93 ("name", "Add_Find")]), [ct])) = Add_Find (xml_to_cterm ct)
1.94 | xml_to_tac
1.95 - (XML.Elem (("SIMPLETACTIC", [
1.96 + (XML.Elem (("TERMTACTIC", [
1.97 ("name", "Add_Relation")]), [ct])) = Add_Relation (xml_to_cterm ct)
1.98 | xml_to_tac
1.99 (XML.Elem (("SIMPLETACTIC", [
1.100 - ("name", "Specify_Theory")]), [ct])) = Specify_Theory (xml_to_cterm ct)
1.101 + ("name", "Specify_Theory")]), [XML.Text ct])) = Specify_Theory ct
1.102 +
1.103 | xml_to_tac
1.104 (XML.Elem (("STRINGLISTTACTIC", [
1.105 ("name", "Specify_Problem")]), [ct])) = Specify_Problem (xml_to_strs ct)
1.106 @@ -849,11 +852,12 @@
1.107 (XML.Elem (("STRINGLISTTACTIC", [
1.108 ("name", "Apply_Method")]), [mI])) = Apply_Method (xml_to_strs mI)
1.109 | xml_to_tac
1.110 - (XML.Elem (("SIMPLETACTIC", [
1.111 + (XML.Elem (("TERMTACTIC", [
1.112 ("name", "Take")]), [ct])) = Take (xml_to_cterm ct)
1.113 | xml_to_tac
1.114 (XML.Elem (("SIMPLETACTIC", [
1.115 - ("name", "Calculate")]), [opstr])) = Calculate (xml_to_cterm opstr)
1.116 + ("name", "Calculate")]), [XML.Text opstr])) = Calculate opstr
1.117 +
1.118 | xml_to_tac
1.119 (XML.Elem (("REWRITETACTIC", [
1.120 ("name", "Rewrite")]), [thm'])) = Rewrite (xml_to_thm' thm')
1.121 @@ -870,18 +874,20 @@
1.122 XML.Elem (("RULESET", []), [XML.Text rls']),
1.123 subs])) = Rewrite_Set_Inst (xml_to_subs subs, rls')
1.124 | xml_to_tac
1.125 - (XML.Elem (("STRINGLISTTACTIC", [("name", "Or_to_List")]), [])) = Or_to_List
1.126 + (XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [])) = Or_to_List
1.127 +
1.128 | xml_to_tac
1.129 - (XML.Elem (("SIMPLETACTIC", [
1.130 + (XML.Elem (("TERMTACTIC", [
1.131 ("name", "Check_elementwise")]), [ct])) = Check_elementwise (xml_to_cterm ct)
1.132 +
1.133 | xml_to_tac
1.134 - (*WN0605 quick and dirty: cterms is _NOT_ a stringlist like pblID...
1.135 - cterms2xml (j+i) cterms^ ....should be WN060514: TODO TERMLISTTACTIC?*)
1.136 + (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
1.137 (XML.Elem (("STRINGLISTTACTIC", [
1.138 - ("name", "Substitute")]), [ cterms])) = Substitute (xml_to_strs cterms)
1.139 + ("name", "Substitute")]), [cterms])) = Substitute (xml_to_strs cterms)
1.140 +
1.141 | xml_to_tac
1.142 (XML.Elem (("STRINGLISTTACTIC", [
1.143 - ("name", "Or_to_List")]), [pI])) = Check_Postcond (xml_to_strs pI)
1.144 + ("name", "Check_Postcond")]), [pI])) = Check_Postcond (xml_to_strs pI)
1.145 | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x);
1.146
1.147 fun tacs2xml j [] = "":xml
2.1 --- a/src/Tools/isac/xmlsrc/mathml.sml Thu Aug 13 10:46:31 2015 +0200
2.2 +++ b/src/Tools/isac/xmlsrc/mathml.sml Fri Aug 14 10:01:33 2015 +0200
2.3 @@ -38,8 +38,8 @@
2.4 indent i ^ "<" ^ str ^ ">" ^ "\n" ^
2.5 List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
2.6 indent i ^ "</" ^ str ^ ">" ^ "\n"
2.7 - | xmlstr i (XML.Elem ((str, [("status", a)]), trees)) =
2.8 - indent i ^ "<" ^ str ^ " status " ^ a ^ ">" ^ "\n" ^
2.9 + | xmlstr i (XML.Elem ((str, [(flag, value)]), trees)) =
2.10 + indent i ^ "<" ^ str ^ " " ^ flag ^ "=" ^ value ^ ">" ^ "\n" ^
2.11 List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
2.12 indent i ^ "</" ^ str ^ ">" ^ "\n"
2.13 | xmlstr _ (XML.Elem ((_, (_ :: _)), _)) =
3.1 --- a/test/Pure/PIDE/xml.ML Thu Aug 13 10:46:31 2015 +0200
3.2 +++ b/test/Pure/PIDE/xml.ML Fri Aug 14 10:01:33 2015 +0200
3.3 @@ -13,17 +13,6 @@
3.4 "----------- test example for migration \"isabelle tty \" --> libisabelle -----------------------";
3.5 "----------- test example for migration \"isabelle tty \" --> libisabelle -----------------------";
3.6 "see https://github.com/wneuper/libisabelle/blob/master/doc/test--isac-Java--isac-kernel.txt";
3.7 -fun xmlstr i (XML.Text str) = indent i ^ str ^ "\n"
3.8 - | xmlstr i (XML.Elem ((str, []), trees)) =
3.9 - indent i ^ "<" ^ str ^ ">" ^ "\n" ^
3.10 - List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
3.11 - indent i ^ "</" ^ str ^ ">" ^ "\n"
3.12 - | xmlstr i (XML.Elem ((str, [("status", a)]), trees)) =
3.13 - indent i ^ "<" ^ str ^ " status " ^ a ^ ">" ^ "\n" ^
3.14 - List.foldr op ^ "" (map (xmlstr (i + 1)) trees) ^
3.15 - indent i ^ "</" ^ str ^ ">" ^ "\n"
3.16 - | xmlstr _ (XML.Elem ((_, (_ :: _)), _)) =
3.17 - error "xmlstr: TODO review attribute \"status\" etc";
3.18
3.19 (* see ~/proto4/libisabelle/doc/test--isac-jav--isac-kernel.txt *)
3.20 (*------- step 1 -----------------------------------------------------
4.1 --- a/test/Tools/isac/xmlsrc/datatypes.sml Thu Aug 13 10:46:31 2015 +0200
4.2 +++ b/test/Tools/isac/xmlsrc/datatypes.sml Fri Aug 14 10:01:33 2015 +0200
4.3 @@ -12,6 +12,9 @@
4.4 "----------- fun rules2xml ---------------------------------------";
4.5 "----------- fun thm''2xml ---------------------------------------";
4.6 "----------- fun xml_of_model ------------------------------------------------------------------";
4.7 +"----------- fun xml_of_tac --------------------------------------------------------------------";
4.8 +"----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";
4.9 +"----------- fun xml_of_tac: StringListTactic --------------------------------------------------";
4.10 "-----------------------------------------------------------------";
4.11 "-----------------------------------------------------------------";
4.12 "-----------------------------------------------------------------";
4.13 @@ -93,6 +96,147 @@
4.14 val xxx = xml_of_model itms where_;
4.15 (xmlstr 0 xxx);
4.16 writeln(xmlstr 0 xxx);
4.17 -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"
4.18 +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"
4.19 then () else error ("xml_of_model changed = " ^ xmlstr 0 xxx);
4.20
4.21 +"----------- fun xml_of_tac --------------------------------------------------------------------";
4.22 +"----------- fun xml_of_tac --------------------------------------------------------------------";
4.23 +"----------- fun xml_of_tac --------------------------------------------------------------------";
4.24 +(* WN150814 these are the Java objects.
4.25 +import isac.util.tactics.RewriteInst
4.26 +import isac.util.tactics.RewriteSet
4.27 +import isac.util.tactics.RewriteSetInst
4.28 +import isac.util.tactics.SimpleTactic ...not appropriately abstracted
4.29 +import isac.util.tactics.StringListTactic ...not appropriately abstracted
4.30 +import isac.util.tactics.SubProblemTactic
4.31 +import isac.util.tactics.Tactic
4.32 +*)
4.33 +Rewrite: thm' -> tac;
4.34 +val tac = Rewrite("refl", "? a = ? a");
4.35 +xml_of_tac tac;(*
4.36 +<REWRITETACTIC name="Rewrite">
4.37 + <THEOREM>
4.38 + <ID>refl</ID>
4.39 + <FORMULA>? a = ? a</FORMULA>
4.40 + </THEOREM>
4.41 +</REWRITETACTIC>*)
4.42 +if xmlstr 0 (xml_of_tac tac) = "<REWRITETACTIC name=Rewrite>\n. <THEOREM>\n. . <ID>\n. . . refl\n. . </ID>\n. . <FORMULA>\n. . . ? a = ? a\n. . </FORMULA>\n. </THEOREM>\n</REWRITETACTIC>\n"
4.43 +then () else error "xml_of_tac Rewrite CHANGED";
4.44 +
4.45 +Rewrite_Inst: subs * thm' -> tac;
4.46 +val tac = Rewrite_Inst(["(bdv, x)"], ("refl", "? a = ? a"));
4.47 +xml_of_tac tac;(*
4.48 +<REWRITEINSTTACTIC name="Rewrite_Inst">
4.49 + <SUBSTITUTION>
4.50 + <PAIR>
4.51 + <VARIABLE>
4.52 + <MATHML>
4.53 + <ISA>bdv</ISA>
4.54 + </MATHML>
4.55 + </VARIABLE>
4.56 + <VALUE>
4.57 + <MATHML>
4.58 + <ISA>x</ISA>
4.59 + </MATHML>
4.60 + </VALUE>
4.61 + </PAIR>
4.62 + </SUBSTITUTION>
4.63 + <THEOREM>
4.64 + <ID>refl</ID>
4.65 + <FORMULA>? a = ? a</FORMULA>
4.66 + </THEOREM>
4.67 +</REWRITEINSTTACTIC>:*)
4.68 +if xmlstr 0 (xml_of_tac tac) = "<REWRITEINSTTACTIC name=Rewrite_Inst>\n. <SUBSTITUTION>\n. . <PAIR>\n. . . <VARIABLE>\n. . . . <MATHML>\n. . . . . <ISA>\n. . . . . . bdv\n. . . . . </ISA>\n. . . . </MATHML>\n. . . </VARIABLE>\n. . . <VALUE>\n. . . . <MATHML>\n. . . . . <ISA>\n. . . . . . x\n. . . . . </ISA>\n. . . . </MATHML>\n. . . </VALUE>\n. . </PAIR>\n. </SUBSTITUTION>\n. <THEOREM>\n. . <ID>\n. . . refl\n. . </ID>\n. . <FORMULA>\n. . . ? a = ? a\n. . </FORMULA>\n. </THEOREM>\n</REWRITEINSTTACTIC>\n"
4.69 +then () else error "xml_of_tac Rewrite_Inst CHANGED";
4.70 +
4.71 +Rewrite_Set: rls' -> tac;
4.72 +val tac = Rewrite_Set("simplify");
4.73 +xml_of_tac tac;(*
4.74 +<REWRITESETTACTIC name="Rewrite_Set">simplify</REWRITESETTACTIC>*)
4.75 +if xmlstr 0 (xml_of_tac tac) = "<REWRITESETTACTIC name=Rewrite_Set>\n. simplify\n</REWRITESETTACTIC>\n"
4.76 +then () else error "xml_of_tac Rewrite_Set CHANGED";
4.77 +
4.78 +Rewrite_Set_Inst: subs * rls' -> tac;
4.79 +val tac = Rewrite_Set_Inst(["(bdv, x)"], "simplify");
4.80 +xml_of_tac tac;(*
4.81 +<REWRITESETINSTTACTIC name="Rewrite_Set_Inst">
4.82 + <RULESET>simplify</RULESET>
4.83 + <SUBSTITUTION>
4.84 + <PAIR>
4.85 + <VARIABLE>
4.86 + <MATHML>
4.87 + <ISA>bdv</ISA>
4.88 + </MATHML>
4.89 + </VARIABLE>
4.90 + <VALUE>
4.91 + <MATHML>
4.92 + <ISA>x</ISA>
4.93 + </MATHML>
4.94 + </VALUE>
4.95 + </PAIR>
4.96 + </SUBSTITUTION>
4.97 +</REWRITESETINSTTACTIC>:*)
4.98 +if xmlstr 0 (xml_of_tac tac) = "<REWRITESETINSTTACTIC name=Rewrite_Set_Inst>\n. <RULESET>\n. . simplify\n. </RULESET>\n. <SUBSTITUTION>\n. . <PAIR>\n. . . <VARIABLE>\n. . . . <MATHML>\n. . . . . <ISA>\n. . . . . . bdv\n. . . . . </ISA>\n. . . . </MATHML>\n. . . </VARIABLE>\n. . . <VALUE>\n. . . . <MATHML>\n. . . . . <ISA>\n. . . . . . x\n. . . . . </ISA>\n. . . . </MATHML>\n. . . </VALUE>\n. . </PAIR>\n. </SUBSTITUTION>\n</REWRITESETINSTTACTIC>\n"
4.99 +then () else error "xml_of_tac Rewrite_Set_Inst CHANGED";
4.100 +
4.101 +"----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";
4.102 +"----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";
4.103 +"----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";
4.104 +
4.105 +"----------- these are : cterm' -> tac: WN150814 THESE WELL BECOME TermTactic TERMTACTIC";
4.106 +Add_Given: cterm' -> tac;
4.107 +Add_Find: cterm' -> tac;
4.108 +Add_Relation: cterm' -> tac;
4.109 +Check_elementwise: cterm' -> tac;
4.110 +Take: cterm' -> tac;
4.111 +
4.112 +Add_Given: cterm' -> tac;
4.113 +val tac = Add_Given("equality (x + 1 = 2)");
4.114 +xml_of_tac tac;(*
4.115 +<SIMPLETACTIC name="Add_Given">
4.116 + <MATHML>
4.117 + <ISA>equality (x + 1 = 2)</ISA>
4.118 + </MATHML>
4.119 +</SIMPLETACTIC>*)
4.120 +if xmlstr 0 (xml_of_tac tac) = "<TERMTACTIC name=Add_Given>\n. <MATHML>\n. . <ISA>\n. . . equality (x + 1 = 2)\n. . </ISA>\n. </MATHML>\n</TERMTACTIC>\n"
4.121 +then () else error "xml_of_tac Add_Given CHANGED";
4.122 +
4.123 +"----------- these are : string -> tac: ";
4.124 +Calculate: string -> tac; (* should be the operator*)
4.125 +Specify_Theory: domID -> tac;
4.126 +val tac = Specify_Theory("Differentiate");
4.127 +xml_of_tac tac;(*
4.128 +<SIMPLETACTIC name="Specify_Theory">
4.129 + <MATHML> NONSENSE
4.130 + <ISA>Differentiate</ISA>
4.131 + </MATHML>
4.132 +</SIMPLETACTIC>*)
4.133 +if xmlstr 0 (xml_of_tac tac) = "<SIMPLETACTIC name=Specify_Theory>\n. Differentiate\n</SIMPLETACTIC>\n"
4.134 +then () else error "xml_of_tac Specify_Theory CHANGED";
4.135 +
4.136 +"----------- fun xml_of_tac: StringListTactic --------------------------------------------------";
4.137 +"----------- fun xml_of_tac: StringListTactic --------------------------------------------------";
4.138 +"----------- fun xml_of_tac: StringListTactic --------------------------------------------------";
4.139 +Model_Problem: tac;
4.140 +Or_to_List: tac;
4.141 +
4.142 +Apply_Method: metID -> tac;
4.143 +Refine_Tacitly: pblID -> tac;
4.144 +Specify_Problem: pblID -> tac;
4.145 +Specify_Method: metID -> tac;
4.146 +Substitute: sube -> tac; (* Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT *)
4.147 +Check_Postcond: pblID -> tac;
4.148 +
4.149 +Apply_Method: metID -> tac;
4.150 +val tac = Apply_Method(["test", "equation", "simplify"]);
4.151 +xml_of_tac tac;(*
4.152 +<STRINGLISTTACTIC name="Apply_Method">
4.153 + <STRINGLIST>
4.154 + <STRING>test</STRING>
4.155 + <STRING>equation</STRING>
4.156 + <STRING>simplify</STRING>
4.157 + </STRINGLIST>
4.158 +</STRINGLISTTACTIC>*)
4.159 +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"
4.160 +then () else error "xml_of_tac Apply_Method CHANGED";
4.161 +