1.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Fri Aug 14 17:25:55 2015 +0200
1.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Sat Aug 15 08:06:28 2015 +0200
1.3 @@ -778,28 +778,7 @@
1.4 XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
1.5 XML.Elem (("THEORY", []), [XML.Text dI]),
1.6 XML.Elem (("PROBLEM", []), [xml_of_strs pI])])
1.7 - | xml_of_tac Model_Problem =
1.8 - XML.Elem (("STRINGLISTTACTIC", [("name", "Model_Problem")]), [])
1.9 - | xml_of_tac (Refine_Tacitly pI) =
1.10 - XML.Elem (("STRINGLISTTACTIC", [("name", "Refine_Tacitly")]), [xml_of_strs pI])
1.11 - | xml_of_tac (Add_Given ct) =
1.12 - XML.Elem (("TERMTACTIC", [("name", "Add_Given")]), [xml_of_cterm ct])
1.13 - | xml_of_tac (Add_Find ct) =
1.14 - XML.Elem (("TERMTACTIC", [("name", "Add_Find")]), [xml_of_cterm ct])
1.15 - | xml_of_tac (Add_Relation ct) =
1.16 - XML.Elem (("TERMTACTIC", [("name", "Add_Relation")]), [xml_of_cterm ct])
1.17 - | xml_of_tac (Specify_Theory ct) =
1.18 - XML.Elem (("SIMPLETACTIC", [("name", "Specify_Theory")]), [XML.Text ct])
1.19 - | xml_of_tac (Specify_Problem ct) =
1.20 - XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])
1.21 - | xml_of_tac (Specify_Method ct) =
1.22 - XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Method")]), [xml_of_strs ct])
1.23 - | xml_of_tac (Apply_Method mI) =
1.24 - XML.Elem (("STRINGLISTTACTIC", [("name", "Apply_Method")]), [xml_of_strs mI])
1.25 - | xml_of_tac (Take ct) =
1.26 - XML.Elem (("TERMTACTIC", [("name", "Take")]), [xml_of_cterm ct])
1.27 - | xml_of_tac (Calculate opstr) =
1.28 - XML.Elem (("SIMPLETACTIC", [("name", "Calculate")]), [XML.Text opstr])
1.29 + (*----- Rewrite* -----------------------------------------------------*)
1.30 | xml_of_tac (Rewrite thm') =
1.31 XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm' thm'])
1.32 | xml_of_tac (Rewrite_Inst (subs, thm')) =
1.33 @@ -812,53 +791,47 @@
1.34 XML.Elem (("REWRITESETINSTTACTIC", [("name", "Rewrite_Set_Inst")]), (
1.35 XML.Elem (("RULESET", []), [XML.Text rls']) ::
1.36 xml_of_subs subs ::[]))
1.37 - | xml_of_tac (Or_to_List) =
1.38 - XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [])
1.39 + (*----- TERMTACTIC ---------------------------------------------------*)
1.40 + | xml_of_tac (Add_Find ct) =
1.41 + XML.Elem (("TERMTACTIC", [("name", "Add_Find")]), [xml_of_cterm ct])
1.42 + | xml_of_tac (Add_Given ct) =
1.43 + XML.Elem (("TERMTACTIC", [("name", "Add_Given")]), [xml_of_cterm ct])
1.44 + | xml_of_tac (Add_Relation ct) =
1.45 + XML.Elem (("TERMTACTIC", [("name", "Add_Relation")]), [xml_of_cterm ct])
1.46 | xml_of_tac (Check_elementwise ct) =
1.47 XML.Elem (("TERMTACTIC", [("name", "Check_elementwise")]), [xml_of_cterm ct])
1.48 + | xml_of_tac (Take ct) =
1.49 + XML.Elem (("TERMTACTIC", [("name", "Take")]), [xml_of_cterm ct])
1.50 + (*----- SIMPLETACTIC -------------------------------------------------*)
1.51 + | xml_of_tac (Calculate opstr) =
1.52 + XML.Elem (("SIMPLETACTIC", [("name", "Calculate")]), [XML.Text opstr])
1.53 + | xml_of_tac (Or_to_List) =
1.54 + XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [(*//////////*)])
1.55 + | xml_of_tac (Specify_Theory ct) =
1.56 + XML.Elem (("SIMPLETACTIC", [("name", "Specify_Theory")]), [XML.Text ct])
1.57 + (*----- STRINGLISTTACTIC ---------------------------------------------*)
1.58 + | xml_of_tac (Apply_Method mI) =
1.59 + XML.Elem (("STRINGLISTTACTIC", [("name", "Apply_Method")]), [xml_of_strs mI])
1.60 + | xml_of_tac (Check_Postcond pI) =
1.61 + XML.Elem (("STRINGLISTTACTIC", [("name", "Check_Postcond")]), [xml_of_strs pI])
1.62 + | xml_of_tac Model_Problem =
1.63 + XML.Elem (("STRINGLISTTACTIC", [("name", "Model_Problem")]), [])
1.64 + | xml_of_tac (Refine_Tacitly pI) =
1.65 + XML.Elem (("STRINGLISTTACTIC", [("name", "Refine_Tacitly")]), [xml_of_strs pI])
1.66 + | xml_of_tac (Specify_Method ct) =
1.67 + XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Method")]), [xml_of_strs ct])
1.68 + | xml_of_tac (Specify_Problem ct) =
1.69 + XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])
1.70 | xml_of_tac (Substitute cterms) =
1.71 (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
1.72 XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])
1.73 - | xml_of_tac (Check_Postcond pI) =
1.74 - XML.Elem (("STRINGLISTTACTIC", [("name", "Check_Postcond")]), [xml_of_strs pI])
1.75 | xml_of_tac tac = error ("xml_of_tac: not impl. for " ^ tac2str tac);
1.76 +
1.77 fun xml_to_tac
1.78 (XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
1.79 XML.Elem (("THEORY", []), [XML.Text dI]),
1.80 XML.Elem (("PROBLEM", []), [pI])])) = Subproblem (dI, xml_to_strs pI)
1.81 - | xml_to_tac
1.82 - (XML.Elem (("STRINGLISTTACTIC", [
1.83 - ("name", "Model_Problem")]), [])) = Model_Problem
1.84 - | xml_to_tac
1.85 - (XML.Elem (("STRINGLISTTACTIC", [
1.86 - ("name", "Refine_Tacitly")]), [pI])) = Refine_Tacitly (xml_to_strs pI)
1.87 - | xml_to_tac
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 (("TERMTACTIC", [
1.92 - ("name", "Add_Find")]), [ct])) = Add_Find (xml_to_cterm ct)
1.93 - | xml_to_tac
1.94 - (XML.Elem (("TERMTACTIC", [
1.95 - ("name", "Add_Relation")]), [ct])) = Add_Relation (xml_to_cterm ct)
1.96 - | xml_to_tac
1.97 - (XML.Elem (("SIMPLETACTIC", [
1.98 - ("name", "Specify_Theory")]), [XML.Text ct])) = Specify_Theory ct
1.99 - | xml_to_tac
1.100 - (XML.Elem (("STRINGLISTTACTIC", [
1.101 - ("name", "Specify_Problem")]), [ct])) = Specify_Problem (xml_to_strs ct)
1.102 - | xml_to_tac
1.103 - (XML.Elem (("STRINGLISTTACTIC", [
1.104 - ("name", "Specify_Method")]), [ct])) = Specify_Method (xml_to_strs ct)
1.105 - | xml_to_tac
1.106 - (XML.Elem (("STRINGLISTTACTIC", [
1.107 - ("name", "Apply_Method")]), [mI])) = Apply_Method (xml_to_strs mI)
1.108 - | xml_to_tac
1.109 - (XML.Elem (("TERMTACTIC", [
1.110 - ("name", "Take")]), [ct])) = Take (xml_to_cterm ct)
1.111 - | xml_to_tac
1.112 - (XML.Elem (("SIMPLETACTIC", [
1.113 - ("name", "Calculate")]), [XML.Text opstr])) = Calculate opstr
1.114 + (*----- Rewrite* -----------------------------------------------------*)
1.115 | xml_to_tac
1.116 (XML.Elem (("REWRITETACTIC", [
1.117 ("name", "Rewrite")]), [thm'])) = Rewrite (xml_to_thm' thm')
1.118 @@ -874,18 +847,54 @@
1.119 ("name", "Rewrite_Set_Inst")]), [
1.120 XML.Elem (("RULESET", []), [XML.Text rls']),
1.121 subs])) = Rewrite_Set_Inst (xml_to_subs subs, rls')
1.122 + (*----- TERMTACTIC ---------------------------------------------------*)
1.123 + | xml_to_tac
1.124 + (XML.Elem (("TERMTACTIC", [
1.125 + ("name", "Add_Find")]), [ct])) = Add_Find (xml_to_cterm ct)
1.126 + | xml_to_tac
1.127 + (XML.Elem (("TERMTACTIC", [
1.128 + ("name", "Add_Given")]), [ct])) = Add_Given (xml_to_cterm ct)
1.129 + | xml_to_tac
1.130 + (XML.Elem (("TERMTACTIC", [
1.131 + ("name", "Add_Relation")]), [ct])) = Add_Relation (xml_to_cterm ct)
1.132 + | xml_to_tac
1.133 + (XML.Elem (("TERMTACTIC", [
1.134 + ("name", "Take")]), [ct])) = Take (xml_to_cterm ct)
1.135 + | xml_to_tac
1.136 + (XML.Elem (("TERMTACTIC", [
1.137 + ("name", "Check_elementwise")]), [ct])) = Check_elementwise (xml_to_cterm ct)
1.138 + (*----- SIMPLETACTIC -------------------------------------------------*)
1.139 + | xml_to_tac
1.140 + (XML.Elem (("SIMPLETACTIC", [
1.141 + ("name", "Calculate")]), [XML.Text opstr])) = Calculate opstr
1.142 | xml_to_tac
1.143 (XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [])) = Or_to_List
1.144 | xml_to_tac
1.145 - (XML.Elem (("TERMTACTIC", [
1.146 - ("name", "Check_elementwise")]), [ct])) = Check_elementwise (xml_to_cterm ct)
1.147 + (XML.Elem (("SIMPLETACTIC", [
1.148 + ("name", "Specify_Theory")]), [XML.Text ct])) = Specify_Theory ct
1.149 + (*----- STRINGLISTTACTIC ---------------------------------------------*)
1.150 + | xml_to_tac
1.151 + (XML.Elem (("STRINGLISTTACTIC", [
1.152 + ("name", "Apply_Method")]), [mI])) = Apply_Method (xml_to_strs mI)
1.153 + | xml_to_tac
1.154 + (XML.Elem (("STRINGLISTTACTIC", [
1.155 + ("name", "Check_Postcond")]), [pI])) = Check_Postcond (xml_to_strs pI)
1.156 + | xml_to_tac
1.157 + (XML.Elem (("STRINGLISTTACTIC", [
1.158 + ("name", "Model_Problem")]), [])) = Model_Problem
1.159 + | xml_to_tac
1.160 + (XML.Elem (("STRINGLISTTACTIC", [
1.161 + ("name", "Refine_Tacitly")]), [pI])) = Refine_Tacitly (xml_to_strs pI)
1.162 + | xml_to_tac
1.163 + (XML.Elem (("STRINGLISTTACTIC", [
1.164 + ("name", "Specify_Method")]), [ct])) = Specify_Method (xml_to_strs ct)
1.165 + | xml_to_tac
1.166 + (XML.Elem (("STRINGLISTTACTIC", [
1.167 + ("name", "Specify_Problem")]), [ct])) = Specify_Problem (xml_to_strs ct)
1.168 | xml_to_tac
1.169 (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
1.170 (XML.Elem (("STRINGLISTTACTIC", [
1.171 ("name", "Substitute")]), [cterms])) = Substitute (xml_to_sube cterms)
1.172 - | xml_to_tac
1.173 - (XML.Elem (("STRINGLISTTACTIC", [
1.174 - ("name", "Check_Postcond")]), [pI])) = Check_Postcond (xml_to_strs pI)
1.175 | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x);
1.176
1.177 fun tacs2xml j [] = "":xml
2.1 --- a/src/Tools/isac/xmlsrc/xmlsrc.thy Fri Aug 14 17:25:55 2015 +0200
2.2 +++ b/src/Tools/isac/xmlsrc/xmlsrc.thy Sat Aug 15 08:06:28 2015 +0200
2.3 @@ -15,6 +15,9 @@
2.4
2.5 ML {*
2.6 *} ML {*
2.7 +*} ML {*
2.8 +*} ML {*
2.9 +*} ML {*
2.10 *}
2.11
2.12 end
2.13 \ No newline at end of file