1.1 --- a/src/Tools/isac/Interpret/ctree.sml Fri Aug 14 10:01:33 2015 +0200
1.2 +++ b/src/Tools/isac/Interpret/ctree.sml Fri Aug 14 17:25:55 2015 +0200
1.3 @@ -231,6 +231,7 @@
1.4
1.5 val subte2sube = map term2str;
1.6 val subst2subs = map (pair2str o (apfst term2str) o (apsnd term2str));
1.7 +fun subst2sube subst = map term2str (map HOLogic.mk_eq subst)
1.8 val subst2subs' = map ((apfst term2str) o (apsnd term2str));
1.9 fun subs2subst thy s = map (isapair2pair o (parse_patt thy)) s;
1.10 fun sube2subst thy s = map (dest_equals' o (parse_patt thy)) s;
2.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Fri Aug 14 10:01:33 2015 +0200
2.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Fri Aug 14 17:25:55 2015 +0200
2.3 @@ -522,6 +522,12 @@
2.4 (XML.Elem (("SUBSTITUTION", []),
2.5 subs)) = (subst2subs (map xml_to_sub subs) : subs)
2.6 | xml_to_subs x = raise ERROR ("xml_to_subs wrong arg: " ^ xmlstr 0 x)
2.7 +fun xml_of_sube (sube : sube) =
2.8 + XML.Elem (("SUBSTITUTION", []), map xml_of_sub (sube2subst (assoc_thy "Isac") sube))
2.9 +fun xml_to_sube
2.10 + (XML.Elem (("SUBSTITUTION", []),
2.11 + xml_var_val_pairs)) = subst2sube (map xml_to_sub xml_var_val_pairs)
2.12 + | xml_to_sube x = raise ERROR ("xml_to_sube wrong arg: " ^ xmlstr 0 x)
2.13
2.14 fun subst2xml j (subst:subst) =
2.15 (indt j ^"<SUBSTITUTION>\n"^
2.16 @@ -784,7 +790,6 @@
2.17 XML.Elem (("TERMTACTIC", [("name", "Add_Relation")]), [xml_of_cterm ct])
2.18 | xml_of_tac (Specify_Theory ct) =
2.19 XML.Elem (("SIMPLETACTIC", [("name", "Specify_Theory")]), [XML.Text ct])
2.20 -
2.21 | xml_of_tac (Specify_Problem ct) =
2.22 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])
2.23 | xml_of_tac (Specify_Method ct) =
2.24 @@ -795,7 +800,6 @@
2.25 XML.Elem (("TERMTACTIC", [("name", "Take")]), [xml_of_cterm ct])
2.26 | xml_of_tac (Calculate opstr) =
2.27 XML.Elem (("SIMPLETACTIC", [("name", "Calculate")]), [XML.Text opstr])
2.28 -
2.29 | xml_of_tac (Rewrite thm') =
2.30 XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm' thm'])
2.31 | xml_of_tac (Rewrite_Inst (subs, thm')) =
2.32 @@ -810,12 +814,11 @@
2.33 xml_of_subs subs ::[]))
2.34 | xml_of_tac (Or_to_List) =
2.35 XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [])
2.36 -
2.37 | xml_of_tac (Check_elementwise ct) =
2.38 XML.Elem (("TERMTACTIC", [("name", "Check_elementwise")]), [xml_of_cterm ct])
2.39 | xml_of_tac (Substitute cterms) =
2.40 (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
2.41 - XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_strs cterms])
2.42 + XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])
2.43 | xml_of_tac (Check_Postcond pI) =
2.44 XML.Elem (("STRINGLISTTACTIC", [("name", "Check_Postcond")]), [xml_of_strs pI])
2.45 | xml_of_tac tac = error ("xml_of_tac: not impl. for " ^ tac2str tac);
2.46 @@ -841,7 +844,6 @@
2.47 | xml_to_tac
2.48 (XML.Elem (("SIMPLETACTIC", [
2.49 ("name", "Specify_Theory")]), [XML.Text ct])) = Specify_Theory ct
2.50 -
2.51 | xml_to_tac
2.52 (XML.Elem (("STRINGLISTTACTIC", [
2.53 ("name", "Specify_Problem")]), [ct])) = Specify_Problem (xml_to_strs ct)
2.54 @@ -857,7 +859,6 @@
2.55 | xml_to_tac
2.56 (XML.Elem (("SIMPLETACTIC", [
2.57 ("name", "Calculate")]), [XML.Text opstr])) = Calculate opstr
2.58 -
2.59 | xml_to_tac
2.60 (XML.Elem (("REWRITETACTIC", [
2.61 ("name", "Rewrite")]), [thm'])) = Rewrite (xml_to_thm' thm')
2.62 @@ -875,16 +876,13 @@
2.63 subs])) = Rewrite_Set_Inst (xml_to_subs subs, rls')
2.64 | xml_to_tac
2.65 (XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [])) = Or_to_List
2.66 -
2.67 | xml_to_tac
2.68 (XML.Elem (("TERMTACTIC", [
2.69 ("name", "Check_elementwise")]), [ct])) = Check_elementwise (xml_to_cterm ct)
2.70 -
2.71 | xml_to_tac
2.72 (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
2.73 (XML.Elem (("STRINGLISTTACTIC", [
2.74 - ("name", "Substitute")]), [cterms])) = Substitute (xml_to_strs cterms)
2.75 -
2.76 + ("name", "Substitute")]), [cterms])) = Substitute (xml_to_sube cterms)
2.77 | xml_to_tac
2.78 (XML.Elem (("STRINGLISTTACTIC", [
2.79 ("name", "Check_Postcond")]), [pI])) = Check_Postcond (xml_to_strs pI)
3.1 --- a/test/Tools/isac/xmlsrc/datatypes.sml Fri Aug 14 10:01:33 2015 +0200
3.2 +++ b/test/Tools/isac/xmlsrc/datatypes.sml Fri Aug 14 17:25:55 2015 +0200
3.3 @@ -15,6 +15,7 @@
3.4 "----------- fun xml_of_tac --------------------------------------------------------------------";
3.5 "----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";
3.6 "----------- fun xml_of_tac: StringListTactic --------------------------------------------------";
3.7 +"----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";
3.8 "-----------------------------------------------------------------";
3.9 "-----------------------------------------------------------------";
3.10 "-----------------------------------------------------------------";
3.11 @@ -240,3 +241,87 @@
3.12 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"
3.13 then () else error "xml_of_tac Apply_Method CHANGED";
3.14
3.15 +"----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";
3.16 +"----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";
3.17 +"----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";
3.18 +(* Note: tacs Substitute, Rewrite_Inst* have different substitutions,
3.19 +while input in frontend is not yet clear: *)
3.20 +Rewrite_Inst: subs * thm' -> tac;
3.21 +Substitute : sube -> tac;
3.22 +
3.23 +e_subs: cterm' list;
3.24 +e_subs: subs;
3.25 +val subs = ["(bdv_1, xxx)","(bdv_2, yyy)"]: cterm' list;
3.26 +xml_of_subs subs;(*
3.27 +<SUBSTITUTION>
3.28 + <PAIR>
3.29 + <VARIABLE>
3.30 + <MATHML>
3.31 + <ISA>bdv_1</ISA>
3.32 + </MATHML>
3.33 + </VARIABLE>
3.34 + <VALUE><
3.35 + MATHML>
3.36 + <ISA>xxx</ISA>
3.37 + </MATHML>
3.38 + </VALUE>
3.39 + </PAIR>
3.40 + <PAIR>
3.41 + <VARIABLE>
3.42 + <MATHML>
3.43 + <ISA>bdv_2</ISA>
3.44 + </MATHML>
3.45 + </VARIABLE>
3.46 + <VALUE>
3.47 + <MATHML>
3.48 + <ISA>yyy</ISA>
3.49 + </MATHML>
3.50 + </VALUE>
3.51 + </PAIR>
3.52 +</SUBSTITUTION>:*)
3.53 +val tac = Rewrite_Inst (subs, ("diff_sin_chain", "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"));
3.54 +val xml = xml_of_tac tac;
3.55 +
3.56 +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"
3.57 +then () else error "xml_of_tac Rewrite_Inst CHANGED";
3.58 +if xml_to_tac xml = Rewrite_Inst (["(bdv_1, xxx)", "(bdv_2, yyy)"], ("diff_sin_chain", "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))
3.59 +then () else error "xml_to_tac Rewrite_Inst CHANGED";
3.60 +
3.61 +
3.62 +val sube = ["(bdv_1 = xxx)", "(bdv_2 = yyy)"]: sube;
3.63 +e_sube: cterm' list;
3.64 +e_sube: sube;
3.65 +xml_of_sube sube;(*
3.66 +<SUBSTITUTION>
3.67 + <PAIR>
3.68 + <VARIABLE>
3.69 + <MATHML>
3.70 + <ISA>bdv_1</ISA>
3.71 + </MATHML>
3.72 + </VARIABLE>
3.73 + <VALUE>
3.74 + <MATHML>
3.75 + <ISA>xxx</ISA>
3.76 + </MATHML>
3.77 + </VALUE>
3.78 + </PAIR>
3.79 + <PAIR>
3.80 + <VARIABLE>
3.81 + <MATHML>
3.82 + <ISA>bdv_2</ISA>
3.83 + </MATHML>
3.84 + </VARIABLE>
3.85 + <VALUE>
3.86 + <MATHML>
3.87 + <ISA>yyy</ISA>
3.88 + </MATHML>
3.89 + </VALUE>
3.90 + </PAIR>
3.91 +</SUBSTITUTION>:*)
3.92 +val tac = Substitute sube;
3.93 +val xml = xml_of_tac tac;
3.94 +
3.95 +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"
3.96 +then () else error "xml_of_tac Substitute CHANGED";
3.97 +if xml_to_tac xml = Substitute ["bdv_1 = xxx", "bdv_2 = yyy"]
3.98 +then () else error "xml_to_tac Substitute CHANGED";