1.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Thu Oct 06 17:03:44 2016 +0200
1.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Mon Oct 10 18:24:14 2016 +0200
1.3 @@ -1,12 +1,8 @@
1.4 -(* convert sml-datatypes to xml
1.5 - authors: Walther Neuper 2003
1.6 +(* convert sml-datatypes to xml for libisabelle and for kbase.
1.7 + authors: Walther Neuper 2003, 2016
1.8 (c) due to copyright terms
1.9 -
1.10 -use"xmlsrc/datatypes.sml";
1.11 -use"datatypes.sml";
1.12 *)
1.13
1.14 -
1.15 signature DATATYPES = (*TODO: redo with xml_of/to *)
1.16 sig
1.17 val authors2xml : int -> string -> string list -> xml
1.18 @@ -59,14 +55,239 @@
1.19 val thmstr2xml : int -> string -> xml
1.20 end
1.21
1.22 -
1.23 -
1.24 (*------------------------------------------------------------------
1.25 structure datatypes:DATATYPES =
1.26 (*structure datatypes =*)
1.27 struct
1.28 ------------------------------------------------------------------*)
1.29
1.30 +(*** convert sml-datatypes to xml for kbase ***)
1.31 +(* NOTE: funs with siblings in xml_of_* are together with them in 'xml for libisabelle' *)
1.32 +
1.33 +val i = indentation;
1.34 +
1.35 +fun id2xml j ids =
1.36 + let fun id2x _ [] = ""
1.37 + | id2x j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
1.38 + (id2x j ss)
1.39 + in (indt j) ^ "<STRINGLIST>\n" ^
1.40 + (id2x (j + indentation) ids) ^
1.41 + (indt j) ^ "</STRINGLIST>\n" end;
1.42 +(* writeln(id2xml 8 ["linear","univariate","equation"]);
1.43 + <STRINGLIST>
1.44 + <STRING>linear</STRING>
1.45 + <STRING>univariate</STRING>
1.46 + <STRING>equation</STRING>
1.47 + </STRINGLIST>*)
1.48 +fun calc2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
1.49 + indt j ^ "<CALC>\n" ^
1.50 + indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^
1.51 + indt (j+i) ^ "<GUH>\n" ^ cal2guh ("IsacKnowledge",
1.52 + thyID) scrop ^ "</GUH>\n" ^
1.53 + indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^
1.54 + indt j ^ "</CALC>\n" : xml;
1.55 +(*replace by 'fun calc2xml' as developed for thy in 0607*)
1.56 +fun calc2xmlOLD _ ((scr_op, (isa_op, _)):calc) =
1.57 + indt i ^ "<CALCULATE> (" ^ scr_op ^ ", (" ^ isa_op ^ ")) </CALCULATE>\n";
1.58 +fun calcs2xmlOLD _ [] = ("":xml) (*TODO replace with 'strs2xml'*)
1.59 + | calcs2xmlOLD j (r::rs) = calc2xmlOLD j r ^ calcs2xmlOLD j rs;
1.60 +
1.61 +(*.for creating a href for a rule within an rls's rule list;
1.62 + the guh points to the thy of definition of the rule, NOT of use in rls.*)
1.63 +fun rule2xml _ (_ : thyID) Erule =
1.64 + error "rule2xml called with 'Erule'"
1.65 + | rule2xml j _ (Thm (thmDeriv, _)) =
1.66 + indt j ^ "<RULE>\n" ^
1.67 + indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
1.68 + indt (j+i) ^ "<STRING> " ^ thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
1.69 + indt (j+i) ^ "<GUH> " ^
1.70 + thm2guh (thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
1.71 + indt j ^ "</RULE>\n" : xml
1.72 + | rule2xml _ _ (Calc (_(*termop*), _)) = ""
1.73 +(*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]
1.74 + see smltest/../datatypes.sml !
1.75 + indt j ^ "<RULE>\n" ^
1.76 + indt (j+i) ^ "<STRING> " ^ termop ^ " </STRING>\n" ^
1.77 + indt (j+i) ^ "<GUH> " ^ cal2guh (thy_containing_cal thyID termop)
1.78 + termop ^ " </GUH>\n" ^
1.79 + indt j ^ "</RULE>\n"
1.80 +*)
1.81 + | rule2xml _ _ (Cal1 (_(*termop*), _)) = ""
1.82 + | rule2xml j thyID (Rls_ rls) =
1.83 + let val rls' = (#id o rep_rls) rls
1.84 + in
1.85 + indt j ^ "<RULE>\n" ^
1.86 + indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^
1.87 + indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^
1.88 + indt (j+i) ^ "<GUH> " ^ rls2guh (thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
1.89 + indt j ^ "</RULE>\n"
1.90 + end;
1.91 +fun rules2xml _ _ [] = ("":xml)
1.92 + | rules2xml j thyID (r::rs) = rule2xml j thyID r ^ rules2xml j thyID rs;
1.93 +
1.94 +fun filterpbl str =
1.95 + let fun filt [] = []
1.96 + | filt ((s, (t1, t2)) :: ps) =
1.97 + if str = s then (t1 $ t2) :: filt ps else filt ps
1.98 + in filt end;
1.99 +fun pattern2xml j p where_ =
1.100 + (case filterpbl "#Given" p of
1.101 + [] => (indt j) ^ "<GIVEN> </GIVEN>\n"
1.102 +(* val gis = filterpbl "#Given" p;
1.103 + *)
1.104 + | gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml' j gis ^
1.105 + (indt j) ^ "</GIVEN>\n")
1.106 + ^
1.107 + (case where_ of
1.108 + [] => (indt j) ^ "<WHERE> </WHERE>\n"
1.109 + | whs => (indt j) ^ "<WHERE>\n" ^ terms2xml' j whs ^
1.110 + (indt j) ^ "</WHERE>\n")
1.111 + ^
1.112 + (case filterpbl "#Find" p of
1.113 + [] => (indt j) ^ "<FIND> </FIND>\n"
1.114 + | fis => (indt j) ^ "<FIND>\n" ^ terms2xml' j fis ^
1.115 + (indt j) ^ "</FIND>\n")
1.116 + ^
1.117 + (case filterpbl "#Relate" p of
1.118 + [] => (indt j) ^ "<RELATE> </RELATE>\n"
1.119 + | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^
1.120 + (indt j) ^ "</RELATE>\n");
1.121 +(*
1.122 +writeln(pattern2xml 3 ((#ppc o get_pbt)
1.123 + ["squareroot","univariate","equation","test"]) []);
1.124 + *)
1.125 +
1.126 +(*url to a source external to isac*)
1.127 +fun extref2xml j linktext url =
1.128 + indt j ^ "<EXTREF>\n" ^
1.129 + indt (j+i) ^ "<TEXT> " ^ linktext ^ " </TEXT>\n" ^
1.130 + indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^
1.131 + indt j ^ "</EXTREF>\n" : xml;
1.132 +fun theref2xml j (thyID:thyID) typ (xstring:xstring) =
1.133 + let val guh = theID2guh ["IsacKnowledge", thyID, typ, xstring]
1.134 + val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
1.135 + in indt j ^ "<KESTOREREF>\n" ^
1.136 + indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
1.137 + indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^
1.138 + indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
1.139 + indt j ^ "</KESTOREREF>\n" : xml
1.140 + end;
1.141 +fun keref2xml j typ (kestoreID:kestoreID) =
1.142 + let val id = strs2str' kestoreID
1.143 + val guh = kestoreID2guh typ kestoreID
1.144 + in indt j ^ "<KESTOREREF>\n" ^
1.145 + indt (j+i) ^ "<TAG> " ^ ketype2str' typ ^ "</TAG>\n" ^
1.146 + indt (j+i) ^ "<ID> " ^ id ^ " </ID>\n" ^
1.147 + indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
1.148 + indt j ^ "</KESTOREREF>\n" : xml
1.149 + end;
1.150 +fun authors2xml j str auts =
1.151 + let fun autx _ [] = ""
1.152 + | autx j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
1.153 + (autx j ss)
1.154 + in indt j ^ "<"^str^">\n" ^
1.155 + autx (j + i) auts ^
1.156 + indt j ^ "</"^str^">\n" : xml
1.157 + end;
1.158 +(* writeln(authors2xml 2 "MATHAUTHORS" []);
1.159 + writeln(authors2xml 2 "MATHAUTHORS"
1.160 + ["isac-team 2001", "Richard Lang 2003"]);
1.161 + *)
1.162 +fun scr2xml j EmptyScr =
1.163 + indt j ^"<SCRIPT> </SCRIPT>\n" : xml
1.164 + | scr2xml j (Prog term) =
1.165 + if term = e_term
1.166 + then indt j ^"<SCRIPT> </SCRIPT>\n"
1.167 + else indt j ^"<SCRIPT>\n"^
1.168 + term2xml j (inst_abs (assoc_thy "Isac") term) ^ "\n" ^
1.169 + indt j ^"</SCRIPT>\n"
1.170 + | scr2xml j (Rfuns _) =
1.171 + indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n";
1.172 +
1.173 +fun calcref2xml j (thyID:thyID, (scrop, (_(*rewop*), _)):calc) =
1.174 + indt j ^ "<CALCREF>\n" ^
1.175 + indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^
1.176 + indt (j+i) ^ "<GUH> " ^ cal2guh ("IsacKnowledge",
1.177 + thyID) scrop ^ " </GUH>\n" ^
1.178 + indt j ^ "</CALCREF>\n" : xml;
1.179 +fun calcrefs2xml _ (_,[]) = "":xml
1.180 + | calcrefs2xml j (thyID, cal::cs) =
1.181 + calcref2xml j (thyID, cal) ^ calcrefs2xml j (thyID, cs);
1.182 +
1.183 +fun prepa12xml j (terms, term) =
1.184 + indt j ^"<PREPAT>\n"^
1.185 + indt (j+i) ^"<PRECONDS>\n"^
1.186 + terms2xml (j+2*i) terms ^
1.187 + indt (j+i) ^"</PRECONDS>\n"^
1.188 + indt (j+i) ^"<PATTERN>\n"^
1.189 + term2xml (j+2*i) term ^
1.190 + indt (j+i) ^"</PATTERN>\n"^
1.191 + indt j ^"</PREPAT>\n" : xml;
1.192 +fun prepat2xml _ [] = ""
1.193 + | prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps : xml;
1.194 +
1.195 +fun rls2xm j (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
1.196 + srls, calc, rules, errpatts, scr}) =
1.197 + indt j ^"<RULESET>\n"^
1.198 + indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
1.199 + indt (j+i) ^"<TYPE> "^ seqrls ^" </TYPE>\n"^
1.200 + indt (j+i) ^"<RULES>\n" ^
1.201 + rules2xml (j+2*i) thyID rules ^
1.202 + indt (j+i) ^"</RULES>\n" ^
1.203 + indt (j+i) ^"<PRECONDS> " ^
1.204 + terms2xml' (j+2*i) preconds ^
1.205 + indt (j+i) ^"</PRECONDS>\n" ^
1.206 + indt (j+i) ^"<ORDER>\n" ^
1.207 + indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
1.208 +(*WN060714 thy_isac_*-ord-*.xml not yet generated ................
1.209 + indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
1.210 + thyID) ord ^ " </GUH>\n" ^
1.211 +..................................................................*)
1.212 + indt (j+i) ^"</ORDER>\n" ^
1.213 + indt (j+i) ^"<ERLS>\n" ^
1.214 + indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
1.215 + indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
1.216 + indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID)
1.217 + (id_rls erls) ^ " </GUH>\n" ^
1.218 + indt (j+i) ^"</ERLS>\n" ^
1.219 + indt (j+i) ^"<SRLS>\n" ^
1.220 + indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
1.221 + indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
1.222 + indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID)
1.223 + (id_rls srls) ^ " </GUH>\n" ^
1.224 + indt (j+i) ^"</SRLS>\n" ^
1.225 + calcrefs2xml (j+i) (thyID, calc) ^
1.226 + scr2xml (j+i) scr ^
1.227 + indt j ^"</RULESET>\n" : xml;
1.228 +fun rls2xml j (thyID, Erls) = rls2xml j (thyID, e_rls)
1.229 + | rls2xml j (thyID, Rls data) = rls2xm j (thyID, "Rls", data)
1.230 + | rls2xml j (thyID, Seq data) = rls2xm j (thyID, "Seq", data)
1.231 + | rls2xml j (thyID, Rrls {id, prepat, rew_ord=(ord,_), erls, calc, errpatts, scr}) =
1.232 + indt j ^"<RULESET>\n"^
1.233 + indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
1.234 + indt (j+i) ^"<TYPE> Rrls </TYPE>\n"^
1.235 + prepat2xml (j+i) prepat ^
1.236 + indt (j+i) ^"<ORDER> " ^
1.237 + indt (j+2*i) ^ "<TAG> Rewrite order </TAG>\n" ^
1.238 + indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
1.239 +(*WN060714 thy_isac_*-ord-*.xml not yet generated ................
1.240 + indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
1.241 + thyID) ord ^ " </GUH>\n" ^
1.242 +.................................................................*)
1.243 + indt (j+i) ^"</ORDER>\n" ^
1.244 + indt (j+i) ^"<ERLS> " ^
1.245 + indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
1.246 + indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
1.247 + indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) (id_rls erls) ^ " </GUH>\n" ^
1.248 + indt (j+i) ^"</ERLS>\n" ^
1.249 + calcrefs2xml (j+i) (thyID, calc) ^
1.250 + indt (j+i) ^"<SCRIPT>\n"^
1.251 + scr2xml (j+2*i) scr ^
1.252 + indt (j+i) ^" </SCRIPT>\n"^
1.253 + indt j ^"</RULESET>\n" : xml;
1.254 +
1.255 +(*** convert sml-datatypes to xml for libisabelle ***)
1.256 +
1.257 (** general types: lists, **)
1.258
1.259 fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
1.260 @@ -85,7 +306,7 @@
1.261 | xml_to_strs tree = raise ERROR ("xml_to_strs: wrong XML.tree \n" ^ xmlstr 0 tree)
1.262
1.263 fun xml_of_int i = XML.Elem (("INT", []), [XML.Text (string_of_int i)])
1.264 -fun xml_of_ints is = (*xml/datatypes.sml: fun ints2xml*)
1.265 +fun xml_of_ints is =
1.266 XML.Elem (("INTLIST", []), map xml_of_int is)
1.267
1.268 fun xml_to_int (XML.Elem (("INT", []), [XML.Text i])) =
1.269 @@ -94,7 +315,6 @@
1.270 fun xml_to_ints (XML.Elem (("INTLIST", []), is)) = map xml_to_int is
1.271 | xml_to_ints tree = raise ERROR ("xml_to_ints: wrong XML.tree \n" ^ xmlstr 0 tree)
1.272
1.273 -
1.274 (** isac datatypes **)
1.275 fun xml_of_pos tag (is, pp) =
1.276 XML.Elem ((tag, []), [
1.277 @@ -140,7 +360,7 @@
1.278 XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (comp_dts' dts)])
1.279 | xml_of_itm_ (Mis (d, pid)) =
1.280 XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])
1.281 -
1.282 + | xml_of_itm_ _ = error "xml_of_itm_: wrong argument"
1.283 fun xml_of_itms itms =
1.284 let
1.285 fun extract (_, _, _, _, itm_) = itm_
1.286 @@ -247,22 +467,33 @@
1.287 xml_var_val_pairs)) = subst2sube (map xml_to_sub xml_var_val_pairs)
1.288 | xml_to_sube x = raise ERROR ("xml_to_sube wrong arg: " ^ xmlstr 0 x)
1.289
1.290 +fun thm''2xml j (thm : thm) =
1.291 + indt j ^ "<THEOREM>\n" ^
1.292 + indt (j+i) ^ "<ID> " ^ thmID_of_derivation_name' thm ^ " </ID>\n"^
1.293 + term2xml j (Thm.prop_of thm) ^ "\n" ^
1.294 + indt j ^ "</THEOREM>\n" : xml;
1.295 fun xml_of_thm' ((ID, form) : thm') =
1.296 XML.Elem (("THEOREM", []), [
1.297 XML.Elem (("ID", []), [XML.Text ID]),
1.298 XML.Elem (("FORMULA", []), [
1.299 XML.Text form])]) (* repair for MathML: use term instead String *)
1.300 +(* at the front-end theorems can be shown by their term, so term is transported isac-java <--- ME *)
1.301 +fun xml_of_thm'' ((ID, term) : thm'') =
1.302 + XML.Elem (("THEOREM", []), [
1.303 + XML.Elem (("ID", []), [XML.Text ID]),
1.304 + xml_of_term_NEW term])
1.305 fun xml_to_thm'
1.306 (XML.Elem (("THEOREM", []), [
1.307 XML.Elem (("ID", []), [XML.Text ID]),
1.308 XML.Elem (("FORMULA", []), [(* repair for MathML: use term instead String *)
1.309 XML.Text form])])) = ((ID, form) : thm')
1.310 | xml_to_thm' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
1.311 -
1.312 -fun xml_of_thm (thm : thm) =
1.313 - XML.Elem (("THEOREM", []), [
1.314 - XML.Elem (("ID", []), [XML.Text (thmID_of_derivation_name' thm)]),
1.315 - xml_of_term (Thm.prop_of thm)])
1.316 +(* at the front-end theorems are identified only by their name, so NO isac-java \<longrightarrow> ME *)
1.317 +fun xml_to_thm''
1.318 + (XML.Elem (("THEOREM", []), [
1.319 + XML.Elem (("ID", []), [XML.Text ID])])) =
1.320 + (ID, Thm.prop_of (Global_Theory.get_thm (Isac ()) ID)) : thm''
1.321 + | xml_to_thm'' x = raise ERROR ("xml_to_thm'' wrong arg:" ^ xmlstr 0 x)
1.322
1.323 fun xml_of_src EmptyScr =
1.324 XML.Elem (("NOCODE", []), [XML.Text "empty"])
1.325 @@ -282,12 +513,12 @@
1.326 (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
1.327 XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])
1.328 (*----- Rewrite* -----------------------------------------------------*)
1.329 - | xml_of_tac (Rewrite thm') =
1.330 - XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm' thm'])
1.331 - | xml_of_tac (Rewrite_Inst (subs, thm')) =
1.332 + | xml_of_tac (Rewrite thm'') =
1.333 + XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm'' thm''])
1.334 + | xml_of_tac (Rewrite_Inst (subs, thm'')) =
1.335 XML.Elem (("REWRITEINSTTACTIC", [("name", "Rewrite_Inst")]), (
1.336 xml_of_subs subs ::
1.337 - xml_of_thm' thm' :: []))
1.338 + xml_of_thm'' thm'' :: []))
1.339 | xml_of_tac (Rewrite_Set rls') =
1.340 XML.Elem (("REWRITESETTACTIC", [("name", "Rewrite_Set")]), [XML.Text rls'])
1.341 | xml_of_tac (Rewrite_Set_Inst (subs, rls')) =
1.342 @@ -338,11 +569,11 @@
1.343 (*----- Rewrite* -----------------------------------------------------*)
1.344 | xml_to_tac
1.345 (XML.Elem (("REWRITETACTIC", [
1.346 - ("name", "Rewrite")]), [thm'])) = Rewrite (xml_to_thm' thm')
1.347 + ("name", "Rewrite")]), [thm])) = Rewrite (xml_to_thm'' thm)
1.348 | xml_to_tac
1.349 (XML.Elem (("REWRITEINSTTACTIC", [
1.350 ("name", "Rewrite_Inst")]), [
1.351 - subs, thm'])) = Rewrite_Inst (xml_to_subs subs, xml_to_thm' thm')
1.352 + subs, thm])) = Rewrite_Inst (xml_to_subs subs, xml_to_thm'' thm)
1.353 | xml_to_tac
1.354 (XML.Elem (("REWRITESETTACTIC", [
1.355 ("name", "Rewrite_Set")]), [XML.Text rls'])) = Rewrite_Set (rls')