1.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Thu Apr 22 16:49:41 2021 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Thu Apr 22 21:34:20 2021 +0200
1.3 @@ -11,8 +11,8 @@
1.4 begin
1.5 ML_file "present-tool.sml"
1.6 ML_file "thy-present.sml"
1.7 -(**)ML_file mathml.sml(**)
1.8 -(**)ML_file datatypes.sml(**)
1.9 + ML_file mathml.sml
1.10 + ML_file datatypes.sml
1.11 ML_file "pbl-met-hierarchy.sml"
1.12 ML_file "thy-hierarchy.sml"
1.13 ML_file "interface-xml.sml"
2.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu Apr 22 16:49:41 2021 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu Apr 22 21:34:20 2021 +0200
2.3 @@ -1,77 +1,21 @@
2.4 (* convert sml-datatypes to xml for libisabelle and for kbase.
2.5 authors: Walther Neuper 2003, 2016
2.6 (c) due to copyright terms
2.7 +
2.8 +This code remains for the purpose of running tests
2.9 +which imitate interaction via libisabelle.
2.10 *)
2.11
2.12 -signature DATATYPES = (*TODO: redo with xml_of/to *)
2.13 - sig
2.14 - val authors2xml : int -> string -> string list -> xml
2.15 - val calc2xml : int -> ThyC.id * Rule_Def.calc -> xml
2.16 - val calcrefs2xml : int -> ThyC.id * Rule_Def.calc list -> xml
2.17 - val extref2xml : int -> string -> string -> xml
2.18 - val filterpbl :
2.19 - ''a -> (''a * (Term.term * Term.term)) list -> Term.term list
2.20 - val formula2xml : int -> Term.term -> xml
2.21 - val formulae2xml : int -> Term.term list -> xml
2.22 - val i : int
2.23 - val id2xml : int -> string list -> string
2.24 - val ints2xml : int -> int list -> string
2.25 - val itm_2xml : int -> I_Model.feedback -> xml
2.26 - val itms2xml : int -> I_Model.T -> string
2.27 - val keref2xml : int -> Ptool.ketype -> Ptool.kestoreID -> xml
2.28 - val model2xml :
2.29 - int -> I_Model.T -> (bool * Term.term) list -> xml
2.30 - val modspec2xml : int -> SpecificationC.T -> xml
2.31 - val pattern2xml : int -> Model_Pattern.T -> Term.term list -> string
2.32 - val pos'2xml : int -> string * Pos.pos' -> string
2.33 - val pos'calchead2xml : int -> Pos.pos' * SpecificationC.T -> xml
2.34 - val pos_2xml : int -> Pos.pos_ -> string
2.35 - val posform2xml : int -> Pos.pos' * Term.term -> xml
2.36 - val posformhead2xml : int -> Pos.pos' * Ctree.ptform -> string
2.37 - val posformheads2xml : int -> (Pos.pos' * Ctree.ptform) list -> xml
2.38 - val posforms2xml : int -> (Pos.pos' * Term.term) list -> xml
2.39 - val posterms2xml : int -> (Pos.pos' * term) list -> xml
2.40 - val precond2xml : int -> bool * Term.term -> xml
2.41 - val preconds2xml : int -> (bool * Term.term) list -> xml
2.42 - val rls2xml : int -> ThyC.id * Rule_Set.T -> xml
2.43 - val rule2xml : int -> Check_Unique.id -> Rule.rule -> xml
2.44 - val rules2xml : int -> Check_Unique.id -> Rule.rule list -> xml
2.45 - val scr2xml : int -> Program.T -> xml
2.46 - val spec2xml : int -> References.T -> xml
2.47 - val sub2xml : int -> Term.term * Term.term -> xml
2.48 - val subs2xml : int -> Subst.input -> xml
2.49 - val subst2xml : int -> subst -> xml
2.50 - val tac2xml : int -> Tactic.input -> xml
2.51 - val tacs2xml : int -> Tactic.input list -> xml
2.52 - val theref2xml : int -> ThyC.id -> string -> xstring -> string
2.53 - val thm''2xml : int -> thm -> xml
2.54 - val thmstr2xml : int -> string -> xml
2.55 - end
2.56 -
2.57 (*------------------------------------------------------------------
2.58 -structure datatypes:DATATYPES =
2.59 +structure datatypes: DATATYPES =
2.60 (*structure datatypes =*)
2.61 struct
2.62 ------------------------------------------------------------------*)
2.63
2.64 (*** convert sml-datatypes to xml for kbase ***)
2.65 -(* NOTE: funs with siblings in xml_of_* are together with them in 'xml for libisabelle' *)
2.66
2.67 val i = indentation;
2.68
2.69 -fun id2xml j ids =
2.70 - let fun id2x _ [] = ""
2.71 - | id2x j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
2.72 - (id2x j ss)
2.73 - in (indt j) ^ "<STRINGLIST>\n" ^
2.74 - (id2x (j + indentation) ids) ^
2.75 - (indt j) ^ "</STRINGLIST>\n" end;
2.76 -(* writeln(id2xml 8 ["linear", "univariate", "equation"]);
2.77 - <STRINGLIST>
2.78 - <STRING>linear</STRING>
2.79 - <STRING>univariate</STRING>
2.80 - <STRING>equation</STRING>
2.81 - </STRINGLIST>*)
2.82 fun calc2xml j (thyID, (scrop, (rewop, _))) =
2.83 indt j ^ "<CALC>\n" ^
2.84 indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^
2.85 @@ -79,44 +23,6 @@
2.86 thyID) scrop ^ "</GUH>\n" ^
2.87 indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^
2.88 indt j ^ "</CALC>\n";
2.89 -(*replace by 'fun calc2xml' as developed for thy in 0607*)
2.90 -fun calc2xmlOLD _ (scr_op, (isa_op, _)) =
2.91 - indt i ^ "<CALCULATE> (" ^ scr_op ^ ", (" ^ isa_op ^ ")) </CALCULATE>\n";
2.92 -fun calcs2xmlOLD _ [] = "" (*TODO replace with 'strs2xml'*)
2.93 - | calcs2xmlOLD j (r::rs) = calc2xmlOLD j r ^ calcs2xmlOLD j rs;
2.94 -
2.95 -(*.for creating a href for a rule within an rls's rule list;
2.96 - the guh points to the thy of definition of the rule, NOT of use in rls.*)
2.97 -fun rule2xml _ _ Rule.Erule =
2.98 - raise ERROR "rule2xml called with 'Erule'"
2.99 - | rule2xml j _ (Rule.Thm (thmDeriv, _)) =
2.100 - indt j ^ "<RULE>\n" ^
2.101 - indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
2.102 - indt (j+i) ^ "<STRING> " ^ ThmC.cut_id thmDeriv ^ " </STRING>\n" ^
2.103 - indt (j+i) ^ "<GUH> " ^
2.104 - Thy_Write.thm2guh (Thy_Read.thy_containing_thm thmDeriv) (ThmC.cut_id thmDeriv) ^ " </GUH>\n" ^
2.105 - indt j ^ "</RULE>\n"
2.106 - | rule2xml _ _ (Rule.Eval (_(*termop*), _)) = ""
2.107 -(*FIXXXXXXXME.WN060714 in rls make Eval : calc -> rule [add scriptop!]
2.108 - see smltest/../datatypes.sml !
2.109 - indt j ^ "<RULE>\n" ^
2.110 - indt (j+i) ^ "<STRING> " ^ termop ^ " </STRING>\n" ^
2.111 - indt (j+i) ^ "<GUH> " ^ cal2guh (thy_containing_cal thyID termop)
2.112 - termop ^ " </GUH>\n" ^
2.113 - indt j ^ "</RULE>\n"
2.114 -*)
2.115 - | rule2xml _ _ (Rule.Cal1 (_(*termop*), _)) = ""
2.116 - | rule2xml j thyID (Rule.Rls_ rls) =
2.117 - let val rls' = (#id o Rule_Set.rep) rls
2.118 - in
2.119 - indt j ^ "<RULE>\n" ^
2.120 - indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^
2.121 - indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^
2.122 - indt (j+i) ^ "<GUH> " ^ Thy_Write.rls2guh (Thy_Read.thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
2.123 - indt j ^ "</RULE>\n"
2.124 - end;
2.125 -fun rules2xml _ _ [] = ""
2.126 - | rules2xml j thyID (r::rs) = rule2xml j thyID r ^ rules2xml j thyID rs;
2.127
2.128 fun filterpbl str =
2.129 let fun filt [] = []
2.130 @@ -145,57 +51,6 @@
2.131 [] => (indt j) ^ "<RELATE> </RELATE>\n"
2.132 | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^
2.133 (indt j) ^ "</RELATE>\n");
2.134 -(*
2.135 -writeln(pattern2xml 3 ((#ppc o get_pbt)
2.136 - ["squareroot", "univariate", "equation", "test"]) []);
2.137 - *)
2.138 -
2.139 -(*url to a source external to isac*)
2.140 -fun extref2xml j linktext url =
2.141 - indt j ^ "<EXTREF>\n" ^
2.142 - indt (j+i) ^ "<TEXT> " ^ linktext ^ " </TEXT>\n" ^
2.143 - indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^
2.144 - indt j ^ "</EXTREF>\n";
2.145 -fun theref2xml j thyID typ xstring =
2.146 - let val guh = Thy_Write.theID2guh ["IsacKnowledge", thyID, typ, xstring]
2.147 - val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
2.148 - in indt j ^ "<KESTOREREF>\n" ^
2.149 - indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
2.150 - indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^
2.151 - indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
2.152 - indt j ^ "</KESTOREREF>\n"
2.153 - end;
2.154 -fun keref2xml j typ kestoreID =
2.155 - let val id = strs2str' kestoreID
2.156 - val guh = Ptool.kestoreID2guh typ kestoreID
2.157 - in indt j ^ "<KESTOREREF>\n" ^
2.158 - indt (j+i) ^ "<TAG> " ^ Ptool.ketype2str' typ ^ "</TAG>\n" ^
2.159 - indt (j+i) ^ "<ID> " ^ id ^ " </ID>\n" ^
2.160 - indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
2.161 - indt j ^ "</KESTOREREF>\n"
2.162 - end;
2.163 -fun authors2xml j str auts =
2.164 - let fun autx _ [] = ""
2.165 - | autx j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
2.166 - (autx j ss)
2.167 - in indt j ^ "<"^str^">\n" ^
2.168 - autx (j + i) auts ^
2.169 - indt j ^ "</"^str^">\n"
2.170 - end;
2.171 -(* writeln(authors2xml 2 "MATHAUTHORS" []);
2.172 - writeln(authors2xml 2 "MATHAUTHORS"
2.173 - ["isac-team 2001", "Richard Lang 2003"]);
2.174 - *)
2.175 -fun scr2xml j Rule.Empty_Prog =
2.176 - indt j ^"<SCRIPT> </SCRIPT>\n"
2.177 - | scr2xml j (Rule.Prog term) =
2.178 - if term = TermC.empty
2.179 - then indt j ^"<SCRIPT> </SCRIPT>\n"
2.180 - else indt j ^"<SCRIPT>\n"^
2.181 - term2xml j (TermC.inst_abs term) ^ "\n" ^
2.182 - indt j ^"</SCRIPT>\n"
2.183 - | scr2xml j (Rule.Rfuns _) =
2.184 - indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n";
2.185
2.186 fun calcref2xml j (thyID, (scrop, (_(*rewop*), _))) =
2.187 indt j ^ "<CALCREF>\n" ^
2.188 @@ -219,112 +74,25 @@
2.189 fun prepat2xml _ [] = ""
2.190 | prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps;
2.191
2.192 -fun rls2xm j (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
2.193 - srls, calc, rules, errpatts, scr}) =
2.194 - indt j ^"<RULESET>\n"^
2.195 - indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
2.196 - indt (j+i) ^"<TYPE> "^ seqrls ^" </TYPE>\n"^
2.197 - indt (j+i) ^"<RULES>\n" ^
2.198 - rules2xml (j+2*i) thyID rules ^
2.199 - indt (j+i) ^"</RULES>\n" ^
2.200 - indt (j+i) ^"<PRECONDS> " ^
2.201 - terms2xml' (j+2*i) preconds ^
2.202 - indt (j+i) ^"</PRECONDS>\n" ^
2.203 - indt (j+i) ^"<ORDER>\n" ^
2.204 - indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
2.205 -(*WN060714 thy_isac_*-ord-*.xml not yet generated ................
2.206 - indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
2.207 - thyID) ord ^ " </GUH>\n" ^
2.208 -..................................................................*)
2.209 - indt (j+i) ^"</ORDER>\n" ^
2.210 - indt (j+i) ^"<ERLS>\n" ^
2.211 - indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
2.212 - indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id erls ^ " </STRING>\n" ^
2.213 - indt (j+2*i) ^ "<GUH> " ^ Thy_Write.rls2guh ("IsacKnowledge", thyID)
2.214 - (Rule_Set.id erls) ^ " </GUH>\n" ^
2.215 - indt (j+i) ^"</ERLS>\n" ^
2.216 - indt (j+i) ^"<SRLS>\n" ^
2.217 - indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
2.218 - indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id erls ^ " </STRING>\n" ^
2.219 - indt (j+2*i) ^ "<GUH> " ^ Thy_Write.rls2guh ("IsacKnowledge", thyID)
2.220 - (Rule_Set.id srls) ^ " </GUH>\n" ^
2.221 - indt (j+i) ^"</SRLS>\n" ^
2.222 - calcrefs2xml (j+i) (thyID, calc) ^
2.223 - scr2xml (j+i) scr ^
2.224 - indt j ^"</RULESET>\n";
2.225 -fun rls2xml j (thyID, Rule_Set.Empty) = rls2xml j (thyID, Rule_Set.empty)
2.226 - | rls2xml j (thyID, Rule_Def.Repeat data) = rls2xm j (thyID, "Rls", data)
2.227 - | rls2xml j (thyID, Rule_Set.Sequence data) = rls2xm j (thyID, "Seq", data)
2.228 - | rls2xml j (thyID, Rule_Set.Rrls {id, prepat, rew_ord=(ord,_), erls, calc, errpatts, scr}) =
2.229 - indt j ^"<RULESET>\n"^
2.230 - indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
2.231 - indt (j+i) ^"<TYPE> Rrls </TYPE>\n"^
2.232 - prepat2xml (j+i) prepat ^
2.233 - indt (j+i) ^"<ORDER> " ^
2.234 - indt (j+2*i) ^ "<TAG> Rewrite order </TAG>\n" ^
2.235 - indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
2.236 -(*WN060714 thy_isac_*-ord-*.xml not yet generated ................
2.237 - indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
2.238 - thyID) ord ^ " </GUH>\n" ^
2.239 -.................................................................*)
2.240 - indt (j+i) ^"</ORDER>\n" ^
2.241 - indt (j+i) ^"<ERLS> " ^
2.242 - indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
2.243 - indt (j+2*i) ^ "<STRING> " ^ Rule_Set.id erls ^ " </STRING>\n" ^
2.244 - indt (j+2*i) ^ "<GUH> " ^ Thy_Write.rls2guh ("IsacKnowledge", thyID) (Rule_Set.id erls) ^ " </GUH>\n" ^
2.245 - indt (j+i) ^"</ERLS>\n" ^
2.246 - calcrefs2xml (j+i) (thyID, calc) ^
2.247 - indt (j+i) ^"<SCRIPT>\n"^
2.248 - scr2xml (j+2*i) scr ^
2.249 - indt (j+i) ^" </SCRIPT>\n"^
2.250 - indt j ^"</RULESET>\n";
2.251
2.252 (*** convert sml-datatypes to xml for libisabelle ***)
2.253
2.254 (** general types: lists, **)
2.255
2.256 fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
2.257 -(*
2.258 -fun xml_to_bool (XML.Elem (("BOOL", []), [XML.Text b])) = string_to_bool b
2.259 - | xml_to_bool tree = raise ERROR ("xml_to_bool: wrong XML.tree \n" ^ xmlstr 0 tree)
2.260 -
2.261 -fun xml_to_ketype (XML.Elem (("KETYPE", []), [XML.Text str])) = Ptool.str2ketype' str
2.262 - | xml_to_ketype tree = raise ERROR ("xml_to_ketype: wrong XML.tree \n" ^ xmlstr 0 tree)
2.263 -*)
2.264
2.265 fun xml_of_str str = XML.Elem (("STRING", []), [XML.Text str])
2.266 fun xml_of_strs strs = XML.Elem (("STRINGLIST", []), map xml_of_str strs)
2.267
2.268 -(*
2.269 -fun xml_to_str (XML.Elem (("STRING", []), [XML.Text str])) = str
2.270 - | xml_to_str tree = raise ERROR ("xml_to_str: wrong XML.tree \n" ^ xmlstr 0 tree)
2.271 -fun xml_to_strs (XML.Elem (("STRINGLIST", []), strs)) = map xml_to_str strs
2.272 - | xml_to_strs tree = raise ERROR ("xml_to_strs: wrong XML.tree \n" ^ xmlstr 0 tree)
2.273 -*)
2.274 -
2.275 fun xml_of_int i = XML.Elem (("INT", []), [XML.Text (string_of_int i)])
2.276 fun xml_of_ints is =
2.277 XML.Elem (("INTLIST", []), map xml_of_int is)
2.278
2.279 -(*
2.280 -fun xml_to_int (XML.Elem (("INT", []), [XML.Text i])) =
2.281 - (case TermC.int_opt_of_string i of SOME i => i | _ => raise ERROR "xml_to_int: int_of_str \<Rightarrow> NONE")
2.282 - | xml_to_int tree = raise ERROR ("xml_to_int: wrong XML.tree \n" ^ xmlstr 0 tree)
2.283 -fun xml_to_ints (XML.Elem (("INTLIST", []), is)) = map xml_to_int is
2.284 - | xml_to_ints tree = raise ERROR ("xml_to_ints: wrong XML.tree \n" ^ xmlstr 0 tree)
2.285 -*)
2.286 -
2.287 (** isac datatypes **)
2.288 fun xml_of_pos tag (is, pp) =
2.289 XML.Elem ((tag, []), [
2.290 xml_of_ints is,
2.291 XML.Elem (("POS", []), [XML.Text (Pos.pos_2str pp)])])
2.292 -(*
2.293 -fun xml_to_pos_ (XML.Elem (("POS", []), [XML.Text pp])) = Pos.str2pos_ pp
2.294 - | xml_to_pos_ tree = raise ERROR ("xml_to_pos_: wrong XML.tree \n" ^ xmlstr 0 tree)
2.295 -fun xml_to_pos (XML.Elem (("POSITION", []), [is, pp])) = (xml_to_ints is, xml_to_pos_ pp) (*: pos'*)
2.296 - | xml_to_pos tree = raise ERROR ("xml_to_pos: wrong XML.tree \n" ^ xmlstr 0 tree)
2.297 -*)
2.298
2.299 fun xml_of_auto (Solve.Steps i) =
2.300 XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text (string_of_int i)])
2.301 @@ -333,16 +101,6 @@
2.302 | xml_of_auto CompleteToSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])
2.303 | xml_of_auto CompleteSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])
2.304 | xml_of_auto CompleteCalc = XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])
2.305 -(*
2.306 -fun xml_to_auto (XML.Elem (("AUTO", []), [
2.307 - XML.Elem (("STEP", []), [XML.Text i])])) = Solve.Steps (TermC.int_opt_of_string i |> the)
2.308 - | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])) = Solve.CompleteModel
2.309 - | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])) = Solve.CompleteCalcHead
2.310 - | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])) = Solve.CompleteToSubpbl
2.311 - | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])) = Solve.CompleteSubpbl
2.312 - | xml_to_auto (XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])) = Solve.CompleteCalc
2.313 - | xml_to_auto tree = raise ERROR ("xml_to_auto: wrong XML.tree \n" ^ xmlstr 0 tree)
2.314 -*)
2.315
2.316 fun filterpbl str =
2.317 let fun filt [] = []
2.318 @@ -394,28 +152,12 @@
2.319 XML.Elem (("THEORYID", []), [XML.Text thyID]),
2.320 XML.Elem (("PROBLEMID", []), [xml_of_strs pblID]),
2.321 XML.Elem (("METHODID", []), [xml_of_strs metID])])
2.322 -(*
2.323 -fun xml_to_spec (XML.Elem (("SPECIFICATION", []), [
2.324 - XML.Elem (("THEORYID", []), [XML.Text thyID]),
2.325 - XML.Elem (("PROBLEMID", []), [ps]),
2.326 - XML.Elem (("METHODID", []), [ms])])) = (thyID, xml_to_strs ps, xml_to_strs ms)
2.327 - | xml_to_spec tree = raise ERROR ("xml_to_spec: wrong XML.tree \n" ^ xmlstr 0 tree)
2.328 -*)
2.329
2.330 fun xml_of_variant (items, spec) =
2.331 XML.Elem (("VARIANT", []), [xml_of_strs items, xml_of_spec spec])
2.332 -(*
2.333 -fun xml_to_variant (XML.Elem (("VARIANT", []), [items, spec])) =
2.334 - (xml_to_strs items, xml_to_spec spec)
2.335 - | xml_to_variant tree = raise ERROR ("xml_to_variant: wrong XML.tree \n" ^ xmlstr 0 tree)
2.336 -*)
2.337
2.338 fun xml_of_fmz [] = xml_of_fmz [Formalise.empty]
2.339 | xml_of_fmz vs = XML.Elem (("FORMALIZATION", []), map xml_of_variant vs)
2.340 -(*
2.341 -fun xml_to_fmz (XML.Elem (("FORMALIZATION", []), vars)) = map xml_to_variant vars
2.342 - | xml_to_fmz tree = raise ERROR ("xml_to_fmz: wrong XML.tree \n" ^ xmlstr 0 tree)
2.343 -*)
2.344
2.345 fun xml_of_modspec ((b, p_, head, gfr, pre, spec): SpecificationC.T) =
2.346 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
2.347 @@ -433,56 +175,15 @@
2.348 XML.Elem (("BELONGSTO", []), [
2.349 XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
2.350 xml_of_spec spec])
2.351 -(*
2.352 -fun xml_to_imodel
2.353 - (XML.Elem (("IMODEL", []), [
2.354 - XML.Elem (("GIVEN", []), givens),
2.355 - (*XML.Elem (("WHERE", []), wheres), ... Where is never input*)
2.356 - XML.Elem (("FIND", []), finds),
2.357 - XML.Elem (("RELATE", []), relates)])) =
2.358 - ([P_Spec.Given (map xml_to_cterm givens),
2.359 - P_Spec.Find (map xml_to_cterm finds),
2.360 - P_Spec.Relate (map xml_to_cterm relates)]) : P_Spec.imodel
2.361 - | xml_to_imodel x = raise ERROR ("xml_to_imodel: WRONG arg = " ^ xmlstr 0 x)
2.362 -fun xml_to_icalhd
2.363 - (XML.Elem (( "ICALCHEAD", []), [
2.364 - pos as XML.Elem (( "POSITION", []), _),
2.365 - XML.Elem (( "HEAD", []), [form]),
2.366 - imodel as XML.Elem (("MATHML", []), _), (* TODO WN150813 ?!?*)
2.367 - XML.Elem (( "POS", []), [XML.Text belongsto]),
2.368 - spec as XML.Elem (( "SPECIFICATION", []), _)])) =
2.369 - (xml_to_pos pos, xml_to_term_NEW form |> UnparseC.term, xml_to_imodel imodel,
2.370 - Pos.str2pos_ belongsto, xml_to_spec spec) : P_Spec.icalhd
2.371 - | xml_to_icalhd x = raise ERROR ("xml_to_icalhd: WRONG arg = " ^ xmlstr 0 x)
2.372 -*)
2.373
2.374 fun xml_of_sub (id, value) =
2.375 XML.Elem (("PAIR", []), [
2.376 XML.Elem (("VARIABLE", []), [xml_of_term id]),
2.377 XML.Elem (("VALUE", []), [xml_of_term value])])
2.378 -(*
2.379 -fun xml_to_sub
2.380 - (XML.Elem (("PAIR", []), [
2.381 - XML.Elem (("VARIABLE", []), [id]),
2.382 - XML.Elem (("VALUE", []), [value])])) = (xml_to_term id, xml_to_term value)
2.383 - | xml_to_sub x = raise ERROR ("xml_to_sub wrong arg: " ^ xmlstr 0 x)
2.384 -*)
2.385 fun xml_of_subs (subs : Subst.input) =
2.386 XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Subst.T_from_input (ThyC.get_theory "Isac_Knowledge") subs))
2.387 -(*
2.388 -fun xml_to_subs
2.389 - (XML.Elem (("SUBSTITUTION", []),
2.390 - subs)) = Subst.T_to_input (map xml_to_sub subs)
2.391 - | xml_to_subs x = raise ERROR ("xml_to_subs wrong arg: " ^ xmlstr 0 x)
2.392 -*)
2.393 fun xml_of_sube sube =
2.394 XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Subst.T_from_string_eqs (ThyC.get_theory "Isac_Knowledge") sube))
2.395 -(*
2.396 -fun xml_to_sube
2.397 - (XML.Elem (("SUBSTITUTION", []),
2.398 - xml_var_val_pairs)) = Subst.T_to_string_eqs (map xml_to_sub xml_var_val_pairs)
2.399 - | xml_to_sube x = raise ERROR ("xml_to_sube wrong arg: " ^ xmlstr 0 x)
2.400 -*)
2.401
2.402 fun thm''2xml j (thm : thm) =
2.403 indt j ^ "<THEOREM>\n" ^
2.404 @@ -496,39 +197,11 @@
2.405 XML.Text form])]) (* repair for MathML: use term instead String *)
2.406 (* at the front-end theorems can be shown by their term, so term is transported isac-java <--- ME *)
2.407 fun xml_of_thm'' (ID, thm) =
2.408 -(*---xml_of_thm''------------------------------------------thm'_to_thm''--------------
2.409 - XML.Elem (("THEOREM", []), [
2.410 - XML.Elem (("ID", []), [XML.Text ID]),
2.411 - xml_of_term_NEW term])
2.412 ------xml_of_thm''------------------------------------------thm'_to_thm''------------*)
2.413 XML.Elem (("THEOREM", []), [
2.414 XML.Elem (("ID", []), [XML.Text ID]),
2.415 XML.Elem (("FORMULA", []), [
2.416 XML.Text ((UnparseC.term o Thm.prop_of) thm)])]) (* repair for MathML: use term instead String *)
2.417
2.418 -(*
2.419 -fun xml_to_thm'
2.420 - (XML.Elem (("THEOREM", []), [
2.421 - XML.Elem (("ID", []), [XML.Text ID]),
2.422 - XML.Elem (("FORMULA", []), [XML.Text "NO_ad_hoc_thm_FROM_FRONTEND = True"])])) =
2.423 - (ID, "NO_ad_hoc_thm_FROM_GUI = True")
2.424 - | xml_to_thm' x = raise ERROR ("xml_of_thm' wrong arg:\n" ^ xmlstr 0 x)
2.425 -(* at the front-end theorems are identified only by their name, so NO isac-java \<longrightarrow> ME *)
2.426 -fun xml_to_thm''
2.427 -(*---xml_of_thm''------------------------------------------thm'_to_thm''--------------
2.428 - (XML.Elem (("THEOREM", []), [
2.429 - XML.Elem (("ID", []), [XML.Text ID]),
2.430 - xterm])) =
2.431 - (ID, xml_to_term_NEW xterm) : thm''
2.432 - | xml_to_thm'' x = raise ERROR ("xml_to_thm'' wrong arg:\n" ^ xmlstr 0 x)
2.433 ------xml_of_thm''------------------------------------------thm'_to_thm''------------*)
2.434 - (XML.Elem (("THEOREM", []), [
2.435 - XML.Elem (("ID", []), [XML.Text ID]),
2.436 - XML.Elem (("FORMULA", []), [
2.437 - XML.Text term])])) = (ID, ThmC.thm_from_thy (ThyC.Isac ()) ID)
2.438 - | xml_to_thm'' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
2.439 -*)
2.440 -
2.441 fun xml_of_src Rule.Empty_Prog =
2.442 XML.Elem (("NOCODE", []), [XML.Text "empty"])
2.443 | xml_of_src (Rule.Prog term) =
2.444 @@ -592,78 +265,6 @@
2.445 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])
2.446 | xml_of_tac tac = raise ERROR ("xml_of_tac: not impl. for " ^ Tactic.input_to_string tac);
2.447
2.448 -(*
2.449 -fun xml_to_tac
2.450 - (XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
2.451 - XML.Elem (("THEORY", []), [XML.Text dI]),
2.452 - XML.Elem (("PROBLEM", []), [pI])])) = Tactic.Subproblem (dI, xml_to_strs pI)
2.453 - | xml_to_tac
2.454 - (*Substitute: sube -> tac; Subst.string_eqs_empty: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
2.455 - (XML.Elem (("STRINGLISTTACTIC", [
2.456 - ("name", "Substitute")]), [cterms])) = Tactic.Substitute (xml_to_sube cterms)
2.457 - (*----- Rewrite* -----------------------------------------------------*)
2.458 - | xml_to_tac
2.459 - (XML.Elem (("REWRITETACTIC", [
2.460 - ("name", "Rewrite")]), [thm])) = Tactic.Rewrite (xml_to_thm'' thm)
2.461 - | xml_to_tac
2.462 - (XML.Elem (("REWRITEINSTTACTIC", [
2.463 - ("name", "Rewrite_Inst")]), [
2.464 - subs, thm])) = Tactic.Rewrite_Inst (xml_to_subs subs, xml_to_thm'' thm)
2.465 - | xml_to_tac
2.466 - (XML.Elem (("REWRITESETTACTIC", [
2.467 - ("name", "Rewrite_Set")]), [XML.Text rls'])) = Tactic.Rewrite_Set (rls')
2.468 - | xml_to_tac
2.469 - (XML.Elem (("REWRITESETINSTTACTIC", [
2.470 - ("name", "Rewrite_Set_Inst")]), [
2.471 - subs,
2.472 - XML.Elem (("RULESET", []), [XML.Text rls'])])) = Tactic.Rewrite_Set_Inst (xml_to_subs subs, rls')
2.473 - (*----- FORMTACTIC ---------------------------------------------------*)
2.474 - | xml_to_tac
2.475 - (XML.Elem (("FORMTACTIC", [
2.476 - ("name", "Add_Find")]), [ct])) = Tactic.Add_Find (xml_to_cterm ct)
2.477 - | xml_to_tac
2.478 - (XML.Elem (("FORMTACTIC", [
2.479 - ("name", "Add_Given")]), [ct])) = Tactic.Add_Given (xml_to_cterm ct)
2.480 - | xml_to_tac
2.481 - (XML.Elem (("FORMTACTIC", [
2.482 - ("name", "Add_Relation")]), [ct])) = Tactic.Add_Relation (xml_to_cterm ct)
2.483 - | xml_to_tac
2.484 - (XML.Elem (("FORMTACTIC", [
2.485 - ("name", "Take")]), [ct])) = Tactic.Take (xml_to_cterm ct)
2.486 - | xml_to_tac
2.487 - (XML.Elem (("FORMTACTIC", [
2.488 - ("name", "Check_elementwise")]), [ct])) = Tactic.Check_elementwise (xml_to_cterm ct)
2.489 - (*----- SIMPLETACTIC -------------------------------------------------*)
2.490 - | xml_to_tac
2.491 - (XML.Elem (("SIMPLETACTIC", [
2.492 - ("name", "Calculate")]), [XML.Text opstr])) = Tactic.Calculate opstr
2.493 - | xml_to_tac
2.494 - (XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [])) = Tactic.Or_to_List
2.495 - | xml_to_tac
2.496 - (XML.Elem (("SIMPLETACTIC", [
2.497 - ("name", "Specify_Theory")]), [XML.Text ct])) = Tactic.Specify_Theory ct
2.498 - (*----- STRINGLISTTACTIC ---------------------------------------------*)
2.499 - | xml_to_tac
2.500 - (XML.Elem (("STRINGLISTTACTIC", [
2.501 - ("name", "Apply_Method")]), [mI])) = Tactic.Apply_Method (xml_to_strs mI)
2.502 - | xml_to_tac
2.503 - (XML.Elem (("STRINGLISTTACTIC", [
2.504 - ("name", "Check_Postcond")]), [pI])) = Tactic.Check_Postcond (xml_to_strs pI)
2.505 - | xml_to_tac
2.506 - (XML.Elem (("STRINGLISTTACTIC", [
2.507 - ("name", "Model_Problem")]), [])) = Tactic.Model_Problem
2.508 - | xml_to_tac
2.509 - (XML.Elem (("STRINGLISTTACTIC", [
2.510 - ("name", "Refine_Tacitly")]), [pI])) = Tactic.Refine_Tacitly (xml_to_strs pI)
2.511 - | xml_to_tac
2.512 - (XML.Elem (("STRINGLISTTACTIC", [
2.513 - ("name", "Specify_Method")]), [ct])) = Tactic.Specify_Method (xml_to_strs ct)
2.514 - | xml_to_tac
2.515 - (XML.Elem (("STRINGLISTTACTIC", [
2.516 - ("name", "Specify_Problem")]), [ct])) = Tactic.Specify_Problem (xml_to_strs ct)
2.517 - | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x);
2.518 -*)
2.519 -
2.520 val e_pblterm = (Thm.term_of o the o (TermC.parse @{theory Prog_Tac}))
2.521 ("Problem (" ^ ThyC.id_empty ^ ", " ^ strs2str' Problem.id_empty ^ ")");
2.522
2.523 @@ -683,11 +284,7 @@
2.524 XML.Elem (("ASM", []), [xml_of_term asm]),
2.525 XML.Elem (("VALUE", []), [xml_of_term vl])])
2.526
2.527 -(*.a reference to an element in the theory hierarchy;
2.528 - compare 'fun keref2xml'.*)
2.529 -(* val (j, thyID, typ, xstring) =
2.530 - (i+i, snd (thy_containing_rls thy' prls'), "Rulesets", prls');
2.531 - *)
2.532 +(* reference to an element in the theory hierarchy *)
2.533 fun theref2xml j thyID typ xstring =
2.534 let val guh = Thy_Write.theID2guh ["IsacKnowledge", thyID, typ, xstring]
2.535 val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
2.536 @@ -708,7 +305,6 @@
2.537 XML.Elem (("GUH", []), [XML.Text guh])])
2.538 end
2.539
2.540 -
2.541 fun xml_of_matchpbl (model_ok, pI, hdl, pbl, pre) =
2.542 XML.Elem (("CONTEXTDATA", []), [
2.543 XML.Elem (("GUH", []), [XML.Text (Ptool.pblID2guh pI)]),
2.544 @@ -726,18 +322,12 @@
2.545 xml_of_model pbl pre])
2.546
2.547 fun xml_of_calcchanged calcid tag old del new =
2.548 - (*TODO: make analogous to xml_to_calcchanged*)
2.549 XML.Elem ((tag, []),[
2.550 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
2.551 XML.Elem (("CALCCHANGED", []), [
2.552 xml_of_pos "UNCHANGED" old,
2.553 xml_of_pos "DELETED" del,
2.554 xml_of_pos "GENERATED" new])])
2.555 -(*
2.556 -fun xml_to_calcchanged (XML.Elem (("CALCCHANGED", []), [old, del, new])) =
2.557 - (xml_to_pos old, xml_to_pos del, xml_to_pos new)
2.558 - | xml_to_calcchanged x = raise ERROR ("xml_to_calcchanged: WRONG arg = " ^ xmlstr 0 x)
2.559 -*)
2.560
2.561 (* for checking output at Frontend *)
2.562 fun cut_xml xml i = xml |> xmlstr 0 |> Symbol.explode |> curry take i |> implode
3.1 --- a/src/Tools/isac/BridgeLibisabelle/interface-xml.sml Thu Apr 22 16:49:41 2021 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface-xml.sml Thu Apr 22 21:34:20 2021 +0200
3.3 @@ -1,17 +1,9 @@
3.4 -(* interface between isac math engine and java:
3.5 - java -> sml: strings on stdin
3.6 - sml -> java: xml on stdout
3.7 +(* XML for the Interface between the isac-kernel and the java-frontend,
3.8 + authors: Walther Neuper 2002
3.9 + (c) due to copyright terms
3.10
3.11 - WN071004 The xml still reflects the insecurity during the first
3.12 - implementation phase, how the communication via stdin/out could
3.13 - correctly relate multiple sml-calculations and java-calculations.
3.14 -
3.15 - Since this insecurity turned out unjustified, the xml can be
3.16 - simplified in several ways:
3.17 - # omit the CALCID; the relation is done by
3.18 - "@@@@@begin@@@@@\n "^string_of_int uI
3.19 - # omit the distinctions APPENDFORMULA, REPLACEFORMULA, ...
3.20 - WN071004 these 2 simplifications are begun with CALCMESSAGE
3.21 +This code remains for the purpose of running tests
3.22 +which imitate interaction via libisabelle.
3.23 *)
3.24
3.25 (**FIXXME.8.03 addUser: clear code, because only CalcTrees distinguished**)
3.26 @@ -79,8 +71,7 @@
3.27 indt j ^ "</FORMULA>\n" : xml;
3.28 fun formulae2xml j [] = ("": xml)
3.29 | formulae2xml j (r::rs) = formula2xml j r ^ formulae2xml j rs;
3.30 -(* writeln(formulae2xml 6 [str2term "1+1=2", str2term "1+1+1=3"]);
3.31 - *)
3.32 +
3.33 fun getaccuasmsOK2xml cI asms =
3.34 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
3.35 "<GETACCUMULATEDASMS>\n" ^
3.36 @@ -90,10 +81,6 @@
3.37 " </ASMLIST>\n" ^
3.38 "</GETACCUMULATEDASMS>\n" ^
3.39 "@@@@@end@@@@@");
3.40 -(* getaccuasmsOK2xml 333 [(([1],Res), str2term "1+1=2"),
3.41 - (([2],Res), str2term "1+1+1=3")];
3.42 - getaccuasmsOK2xml 333 [str2term "1+1=2", str2term "1+1+1=3"];
3.43 - *)
3.44
3.45 fun getintervalOK (calcid : calcID) fs =
3.46 XML.Elem (("GETELEMENTSFROMTO", []),
4.1 --- a/src/Tools/isac/BridgeLibisabelle/mathml.sml Thu Apr 22 16:49:41 2021 +0200
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/mathml.sml Thu Apr 22 21:34:20 2021 +0200
4.3 @@ -45,13 +45,7 @@
4.4 fun xmlstr i (XML.Text str) = indent i ^ str ^ "\n"
4.5 | xmlstr i (XML.Elem (("TERM", []), [xt])) =
4.6 indent i ^ "(" ^ "TERM" ^ ")" ^ "\n" ^
4.7 - indent (i + 1) ^
4.8 -(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
4.9 - (xt |> Codec.decode Codec.term |> Codec.the_success |> UnparseC.term)
4.10 -( *------------------------------------ rm libisabelle -----------------------------------------*)
4.11 - "rm libisabelle: xt NOT DECODED"
4.12 -(*\\---------------------------------- rm libisabelle ---------------------------------------//*)
4.13 - ^ "\n" ^
4.14 + indent (i + 1) ^ "rm libisabelle: xt NOT DECODED" ^ "\n" ^
4.15 indent i ^ "(/" ^ "TERM" ^ ")" ^ "\n"
4.16 | xmlstr i (XML.Elem ((str, []), trees)) =
4.17 indent i ^ "(" ^ str ^ ")" ^ "\n" ^
4.18 @@ -65,9 +59,6 @@
4.19 raise ERROR "xmlstr: TODO review attribute \"status\" etc";
4.20
4.21 fun strs2xml strs = foldl (op ^) ("", strs);
4.22 -(* writeln (strs2xml ["<XXX> xxx </XXX>\n", "<YYY> yyy </YYY>\n"]);
4.23 -<XXX> xxx </XXX>
4.24 -<YYY> yyy </YYY>*)
4.25
4.26 val indentation = 2;
4.27 val i = indentation;
4.28 @@ -86,44 +77,14 @@
4.29 XML.Elem (("MATHML", []),
4.30 [XML.Elem (("ISA", []), [XML.Text ((decode o UnparseC.term) t)])])
4.31 fun xml_of_terms ts = map xml_of_term ts
4.32 -(*
4.33 -fun xml_to_term
4.34 - ((XML.Elem (("MATHML", []), [
4.35 - XML.Elem (("ISA", []), [XML.Text str])]))) = str |> encode |> TermC.str2term
4.36 - | xml_to_term xx = raise ERROR ("xml_to_term wrong arg: " ^ xmlstr 0 xx)
4.37 -fun xml_to_term_NEW
4.38 - ((XML.Elem (("FORMULA", []), [
4.39 - XML.Elem (("ISA", []), [XML.Text str])]))) = str |> encode |> TermC.str2term
4.40 - | xml_to_term_NEW xx = raise ERROR ("xml_to_term_NEW wrong arg: " ^ xmlstr 0 xx)
4.41 -fun xml_to_terms ts = map xml_to_term ts
4.42 -fun xml_to_terms_NEW ts = map xml_to_term_NEW ts
4.43 -*)
4.44
4.45 (* intermediate replacements while introducing transfer of terms by libisabelle *)
4.46 fun xml_of_term_NEW (t : term) =
4.47 XML.Elem (("FORMULA", []), [
4.48 XML.Elem (("ISA", []), [XML.Text ((decode o UnparseC.term) t)]),
4.49 -(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
4.50 - XML.Elem (("TERM", []), [Codec.encode Codec.term t])
4.51 -( *------------------------------------ rm libisabelle -----------------------------------------*)
4.52 XML.Text ("(TERM)\n " ^ UnparseC.term t ^ "\n(/TERM)")
4.53 -(*\\---------------------------------- rm libisabelle ---------------------------------------//*)
4.54 ])
4.55
4.56 -(*
4.57 -(* unused: formulas come as strings from frontend and are parsed by Isabelle *)
4.58 -fun xml_to_term_UNUSED
4.59 - ((XML.Elem (("FORMULA", []), [
4.60 - XML.Elem (("ISA", []), [XML.Text _]),
4.61 - XML.Elem (("TERM", []), [xt])]))) =
4.62 -(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
4.63 - xt |> Codec.decode Codec.term |> Codec.the_success
4.64 -( *------------------------------------ rm libisabelle -----------------------------------------*)
4.65 - Const ("rm libisabelle: xt NOT DECODED", HOLogic.realT)
4.66 -(*\\---------------------------------- rm libisabelle ---------------------------------------//*)
4.67 - | xml_to_term_UNUSED xx = raise ERROR ("xml_to_term_NEW wrong arg: " ^ xmlstr 0 xx)
4.68 -*)
4.69 -
4.70 (*version for TextIO*)
4.71 fun terms2xml j [] = ""
4.72 | terms2xml j (t::ts) = term2xml j t ^ terms2xml j ts;
4.73 @@ -140,12 +101,6 @@
4.74 fun xml_of_cterm ct =
4.75 XML.Elem (("MATHML", []),
4.76 [XML.Elem (("ISA", []), [XML.Text ct])])
4.77 -(*
4.78 -fun xml_to_cterm
4.79 - (XML.Elem (("MATHML", []),
4.80 - [XML.Elem (("ISA", []), [XML.Text ct])])) = ct
4.81 - | xml_to_cterm x = raise ERROR ("xml_to_cterm wrong arg: " ^ xmlstr 0 x)
4.82 -*)
4.83
4.84 (*version for TextIO*)
4.85 fun cterms2xml j [] = ""
4.86 @@ -153,12 +108,3 @@
4.87 (*version for writeln: extra \n*)
4.88 fun cterms2xml' j [] = ""
4.89 | cterms2xml' j (t::ts) = cterm2xml j t ^"\n"^ cterms2xml j ts;
4.90 -
4.91 -(* writeln(cterms2xml 5 ["cterm1", "cterm2"]);
4.92 - <MATHML>
4.93 - <ISA> cterm1 </ISA>
4.94 - </MATHML>
4.95 - <MATHML>
4.96 - <ISA> cterm2 </ISA>
4.97 - </MATHML>
4.98 -*)
4.99 \ No newline at end of file
5.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Thu Apr 22 16:49:41 2021 +0200
5.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Thu Apr 22 21:34:20 2021 +0200
5.3 @@ -1,29 +1,24 @@
5.4 -(* export problem-data and method-data to xml
5.5 +(* ~/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml
5.6 author: Walther Neuper 2004
5.7 (c) isac-team
5.8 +
5.9 +Create XML for the tree structure of problem-patterns and methods.
5.10 +This is kept as a model for some browsing facility, which is required
5.11 +in parallel to PIDE, because these structures are different
5.12 +from the dependency graph of Isabelle's theories.
5.13 *)
5.14 signature PROBLEM_METHOD_HIERARCHY =
5.15 sig
5.16 val format_pblIDl : string list list -> string
5.17 eqtype filepath
5.18 val file2str: filepath -> Thy_Present.filename -> string
5.19 - val hierarchy: string -> 'a Store.node list -> string
5.20 val hierarchy_met: MethodC.T Store.node list -> xml
5.21 val hierarchy_pbl: Problem.T Store.node list -> xml
5.22 val i: int
5.23 - val id2filename: string list -> string
5.24 - val met2file: filepath -> Pos.pos -> MethodC.id -> MethodC.T -> unit
5.25 - val met2xml: MethodC.id -> MethodC.T -> xml
5.26 +
5.27 + val pbl_hierarchy2file: filepath -> unit
5.28 val met_hierarchy2file: filepath -> unit
5.29 - val mets2file: filepath -> unit
5.30 - val node: filepath -> string list -> Pos.pos -> (filepath -> Pos.pos -> string list -> 'a -> 'b) -> 'a Store.node -> unit
5.31 - val nodes: filepath -> string list -> Pos.pos -> (filepath -> Pos.pos -> string list -> 'a -> 'b) -> 'a Store.node list -> unit
5.32 - val pbl2file: filepath -> Pos.pos -> MethodC.id -> Problem.T -> unit
5.33 - val pbl2term: theory -> Problem.id -> term
5.34 - val pbl2xml: Problem.id -> Problem.T -> xml
5.35 - val pbl_hierarchy2file: filepath -> unit
5.36 - val pbls2file: filepath -> unit
5.37 - val pos2filename: int list -> string
5.38 +
5.39 val str2file: Thy_Present.filename -> string -> unit
5.40 val update_metdata: MethodC.T -> Error_Pattern_Def.T list -> MethodC.T
5.41 val update_metpair: theory -> MethodC.id -> Error_Pattern_Def.T list -> MethodC.T * MethodC.id
5.42 @@ -52,38 +47,10 @@
5.43 TextIO.flushOut file;
5.44 TextIO.closeOut file
5.45 end
5.46 -fun pos2filename [] = raise ERROR "pos2filename called with []"
5.47 - | pos2filename [i] = "_" ^ string_of_int i ^ ".xml"
5.48 - | pos2filename (i::is) = "_" ^ string_of_int i ^ pos2filename is;
5.49 -(* pos2filename [1,22,3];
5.50 -val it = "_1_22_3.xml" : string
5.51 +
5.52 +(*
5.53 + create XML for the tree structure of problem-patterns.
5.54 *)
5.55 -fun id2filename [] = raise ERROR "id2filename called with []"
5.56 - | id2filename [s] = s ^ ".xml"
5.57 - | id2filename (s::ss) = s ^ "_" ^ id2filename ss;
5.58 -(* id2filename ["linear", "univariate", "equation"];
5.59 -val it = "linear_univariate_equation.xml" : string
5.60 -*)
5.61 -
5.62 -(*ad DTD: a NODE contains an ID and zero or more NODEs*)
5.63 -(*old version with pos2filename*)
5.64 -fun hierarchy pm(*"pbl" | "met"*) h =
5.65 - let val j = indentation
5.66 - fun nd i p (Store.Node (id,_,ns)) =
5.67 - let val p' = Pos.lev_on p
5.68 - in (indt i) ^ "<NODE>\n" ^
5.69 - (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
5.70 - (indt (i+j)) ^ "<NO> " (*on this level*) ^
5.71 - (string_of_int o last_elem) p' ^ " </NO>\n" ^
5.72 - (indt (i+j)) ^ "<CONTENTREF> " ^ pm ^ pos2filename p' ^
5.73 - " </CONTENTREF>\n" ^
5.74 - (nds (i+j) (Pos.lev_dn p') ns) ^
5.75 - (indt i) ^ "</NODE>\n"
5.76 - end
5.77 - and nds _ _ [] = ""
5.78 - | nds i p (n::ns) = (nd i p n) ^ (nds i (Pos.lev_on p) ns);
5.79 - in nds j [0] h end;
5.80 -(*.create a hierarchy with references to the guh's.*)
5.81 fun hierarchy_pbl h =
5.82 let val j = indentation
5.83 fun nd i p (Store.Node (id,[n as {guh,...} : Problem.T],ns)) =
5.84 @@ -150,186 +117,6 @@
5.85 *)
5.86 val i = indentation;
5.87
5.88 -(* new version with <KESTOREREF>s -- not used *)
5.89 -fun pbl2xml (id:(*pblRD*)Problem.id) ({guh,mathauthors,init,cas,met,ppc,prls,
5.90 - thy,where_}:Problem.T) =
5.91 - let val thy' = Context.theory_name thy
5.92 - val prls' = (#id o Rule_Set.rep) prls
5.93 - in "<NODECONTENT>\n" ^
5.94 - indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
5.95 - (((id2xml i)(* o rev*)) id) ^
5.96 - indt i ^ "<META> </META>\n" ^
5.97 - (*--------------- begin display ------------------------------*)
5.98 - indt i ^ "<HEADLINE>\n" ^
5.99 - (case cas of NONE => term2xml i (pbl2term thy id)
5.100 - | SOME t => term2xml i t) ^ "\n" ^
5.101 - indt i ^ "</HEADLINE>\n" ^
5.102 - (*--------------- hline --------------------------------------*)
5.103 - pattern2xml i ppc where_ ^
5.104 - (*--------------- hline --------------------------------------*)
5.105 - indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n"
5.106 - (*--------------- end display --------------------------------*)
5.107 - ^
5.108 - indt i ^ "<THEORY>\n" ^
5.109 - theref2xml (i+i) thy' "Theorems" "" ^
5.110 - indt i ^ "</THEORY>\n" ^
5.111 - (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
5.112 - | _ => (indt i) ^ "<METHODS>\n" ^
5.113 - foldl op ^ ("", map (keref2xml (i+i) Ptool.Met_) met) ^
5.114 - (indt i) ^ "</METHODS>\n") ^
5.115 - indt i ^ "<EVALPRECOND>\n" ^
5.116 - theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' prls')) "Rulesets" prls'^
5.117 - indt i ^ "</EVALPRECOND>\n" ^
5.118 - authors2xml i "MATHAUTHORS" mathauthors ^
5.119 - authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
5.120 - "</NODECONTENT>" : xml
5.121 - end;
5.122 -(* old version with 'dead' strings for rls, calc, ....* *)
5.123 -fun pbl2xml (id:(*pblRD*)Problem.id) ({guh,mathauthors,init,cas,met,ppc,prls,
5.124 - thy,where_}:Problem.T) =
5.125 - "<NODECONTENT>\n" ^
5.126 - indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
5.127 - (((id2xml i)(* o rev*)) id) ^
5.128 - indt i ^ "<META> </META>\n" ^
5.129 - (*--------------- begin display ------------------------------*)
5.130 - indt i ^ "<HEADLINE>\n" ^
5.131 - (case cas of NONE => term2xml i (pbl2term thy id)
5.132 - | SOME t => term2xml i t) ^ "\n" ^
5.133 - indt i ^ "</HEADLINE>\n" ^
5.134 - (*--------------- hline --------------------------------------*)
5.135 - pattern2xml i ppc where_ ^
5.136 - (*--------------- hline --------------------------------------*)
5.137 - indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n"
5.138 - (*--------------- end display --------------------------------*)
5.139 - ^
5.140 - indt i ^ "<THEORY>\n" ^
5.141 - theref2xml (i+i) (Context.theory_name thy) "Theorems" "" ^
5.142 - indt i ^ "</THEORY>\n" ^
5.143 - (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
5.144 - | _ => (indt i) ^ "<METHODS>\n" ^
5.145 - foldl op^ ("", map (keref2xml (i+i) Ptool.Met_) met) ^
5.146 - (indt i) ^ "</METHODS>\n") ^
5.147 - indt i ^ "<EVALPRECOND> " ^ (#id o Rule_Set.rep)
5.148 - prls ^ " </EVALPRECOND>\n" ^
5.149 - authors2xml i "MATHAUTHORS" mathauthors ^
5.150 - authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
5.151 - "</NODECONTENT>" : xml;
5.152 -
5.153 -
5.154 -(**. write pbls from hierarchy to files.**)
5.155 -fun pbl2file path (pos: Pos.pos) (id: MethodC.id) (pbl as {guh, ...}) =
5.156 - (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ Pos.pos2str pos);
5.157 - ((str2file (path ^ Thy_Present.guh2filename guh)) o (pbl2xml id)) pbl
5.158 - );
5.159 -
5.160 -(**. write mets from hierarchy to files.**)
5.161 -(*.format a method in xml for presentation on the method browser;
5.162 - new version with <KESTOREREF>s -- not used because linking
5.163 - requires elements (rls, calc, ...) to be reorganized.*)
5.164 -(*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
5.165 -fun met2xml (id: MethodC.id) ({guh,mathauthors,init,ppc,pre,scr,calc,
5.166 - crls,erls,errpats,nrls,prls,srls,rew_ord'}: MethodC.T) =
5.167 - let val thy' = "Isac_Knowledge" (*FIXME.WN0607 get thy from met ?!?*)
5.168 - val crls' = (#id o Rule_Set.rep) crls
5.169 - val erls' = (#id o Rule_Set.rep) erls
5.170 - val nrls' = (#id o Rule_Set.rep) nrls
5.171 - val prls' = (#id o Rule_Set.rep) prls
5.172 - val srls' = (#id o Rule_Set.rep) srls
5.173 - in "<NODECONTENT>\n" ^
5.174 - indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
5.175 - id2xml i id ^
5.176 - indt i ^ "<META> </META>\n" ^
5.177 - scr2xml i scr ^
5.178 - pattern2xml i ppc pre ^
5.179 - indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
5.180 - indt i ^ "<EVALPRECOND>\n" ^
5.181 - theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' prls')) "Rulesets" prls'^
5.182 - indt i ^ "</EVALPRECOND>\n" ^
5.183 - indt i ^ "<EVALCOND>\n" ^
5.184 - theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' erls')) "Rulesets" erls'^
5.185 - indt i ^ "</EVALCOND>\n" ^
5.186 - indt i ^ "<EVALLISTEXPR>\n"^
5.187 - theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' srls')) "Rulesets" srls'^
5.188 - indt i ^ "</EVALLISTEXPR>\n" ^
5.189 - indt i ^ "<CHECKELEMENTWISE>\n" ^
5.190 - theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' crls')) "Rulesets" crls'^
5.191 - indt i ^ "</CHECKELEMENTWISE>\n" ^
5.192 - indt i ^ "<NORMALFORM>\n" ^
5.193 - theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' nrls')) "Rulesets" nrls'^
5.194 - indt i ^ "</NORMALFORM>\n" ^
5.195 - indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^
5.196 - calcs2xmlOLD i calc ^
5.197 - authors2xml i "MATHAUTHORS" mathauthors ^
5.198 - authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
5.199 - "</NODECONTENT>" : xml
5.200 - end;
5.201 -(*.format a method in xml for presentation on the method browser;
5.202 - old version with 'dead' strings for rls, calc, ....*)
5.203 -fun met2xml (id: MethodC.id) ({guh,mathauthors,init,ppc,pre,scr,calc,
5.204 - crls,erls,errpats,nrls,prls,srls,rew_ord'}: MethodC.T) =
5.205 - "<NODECONTENT>\n" ^
5.206 - indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
5.207 - id2xml i id ^
5.208 - indt i ^ "<META> </META>\n" ^
5.209 - scr2xml i scr ^
5.210 - pattern2xml i ppc pre ^
5.211 - indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
5.212 - indt i ^ "<EVALPRECOND> " ^ (#id o Rule_Set.rep) prls ^ " </EVALPRECOND>\n" ^
5.213 - indt i ^ "<EVALCOND> " ^ (#id o Rule_Set.rep) erls ^ " </EVALCOND>\n" ^
5.214 - indt i ^ "<EVALLISTEXPR> "^ (#id o Rule_Set.rep) srls ^ " </EVALLISTEXPR>\n" ^
5.215 - indt i ^ "<CHECKELEMENTWISE> " ^ (#id o Rule_Set.rep)
5.216 - crls ^ " </CHECKELEMENTWISE>\n" ^
5.217 - indt i ^ "<NORMALFORM> " ^ (#id o Rule_Set.rep) nrls ^ " </NORMALFORM>\n" ^
5.218 - indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^
5.219 - calcs2xmlOLD i calc ^
5.220 - authors2xml i "MATHAUTHORS" mathauthors ^
5.221 - authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
5.222 - "</NODECONTENT>" : xml;
5.223 -(* writeln (met2xml ["Test", "solve_linear"]
5.224 - (get_met ["Test", "solve_linear"]));
5.225 - *)
5.226 -
5.227 -(*.write the files using an int-key (pos') as filename.*)
5.228 -fun met2file path (pos: Pos.pos) (id: MethodC.id) met =
5.229 - (writeln ("### met2file: id = " ^ strs2str id);
5.230 - ((str2file (path ^ "met" ^ pos2filename pos)) o (met2xml id)) met);
5.231 -
5.232 -(*.write the files using the guh as filename.*)
5.233 -fun met2file path (pos: Pos.pos) (id: MethodC.id) (met as {guh,...}) =
5.234 - (writeln ("### met2file: id = " ^ strs2str id);
5.235 - ((str2file (path ^ Thy_Present.guh2filename guh)) o (met2xml id)) met);
5.236 -
5.237 -(*.scan the mtree Ptyp and print the nodes using wfn.*)
5.238 -fun node pa ids po wfn (Store.Node (id, [n], ns)) =
5.239 - let val po' = Pos.lev_on po
5.240 - in
5.241 - wfn pa po' (ids@[id]) n;
5.242 - nodes pa (ids@[id]) (Pos.lev_dn po') wfn ns
5.243 - end
5.244 -and nodes _ _ _ _ [] = ()
5.245 - | nodes pa ids po wfn (n::ns) =
5.246 - (node pa ids po wfn n; nodes pa ids (Pos.lev_on po) wfn ns);
5.247 -
5.248 -fun pbls2file path = nodes path [] [0] pbl2file (get_ptyps ());
5.249 -fun mets2file path = nodes path [] [0] met2file (get_mets ());
5.250 -(*
5.251 -~@wneuper-w541:~/tmp$ mkdir pbl
5.252 -~@wneuper-w541:~/tmp$ mkdir met
5.253 -~@wneuper-w541:~/tmp$ mkdir thy
5.254 -
5.255 -val path = "/home/wneuper/proto2/isac/xmldata/";
5.256 -val path = "/home/wneuper/tmp/";
5.257 -
5.258 -pbl_hierarchy2file (path ^ "pbl/");
5.259 -pbls2file (path ^ "pbl/");
5.260 -
5.261 -met_hierarchy2file (path ^ "met/");
5.262 -mets2file (path ^ "met/");
5.263 -
5.264 -thy_hierarchy2file (path ^ "thy/");
5.265 -thes2file (path ^ "thy/");
5.266 -*)
5.267 -
5.268 fun update_metdata
5.269 ({guh, mathauthors, init, rew_ord', erls, srls, prls, crls, nrls, calc, ppc, pre, scr, ...}: MethodC.T)
5.270 errpats' =
6.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Thu Apr 22 16:49:41 2021 +0200
6.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Thu Apr 22 21:34:20 2021 +0200
6.3 @@ -190,4 +190,3 @@
6.4 in (hrls', theID) end
6.5
6.6 (**)end(**)
6.7 -(** )open Thy_Hierarchy( **)
7.1 --- a/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Thu Apr 22 16:49:41 2021 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,174 +0,0 @@
7.4 -(* Title: tests for sml/xmlsrc/pbl-met-hierarchy.sml
7.5 - Author: Walther Neuper 060209
7.6 - (c) isac-team 2006
7.7 -
7.8 -use"../smltest/xmlsrc/pbl-met-hierarchy.sml";
7.9 -use"pbl-met-hierarchy.sml";
7.10 -
7.11 -CAUTION with testing *2file functions -- they are actually writing !!!
7.12 -*)
7.13 -
7.14 -val thy = @{theory "Isac_Knowledge"};
7.15 -
7.16 -"-----------------------------------------------------------------";
7.17 -"table of contents -----------------------------------------------";
7.18 -"-----------------------------------------------------------------";
7.19 -"----- pbl2xml ---------------------------------------------------";
7.20 -"----- ERROR Illegal reference to internal variable: 'Pure_' -----";
7.21 -"----- fun pbl2term ----------------------------------------------";
7.22 -"----- fun insert_errpats ----------------------------------------";
7.23 -"-----------------------------------------------------------------";
7.24 -"-----------------------------------------------------------------";
7.25 -"-----------------------------------------------------------------";
7.26 -
7.27 -
7.28 -
7.29 -"----- pbl2xml ---------------------------------------------------";
7.30 -"----- pbl2xml ---------------------------------------------------";
7.31 -"----- pbl2xml ---------------------------------------------------";
7.32 -(*what to do if from 'pbls2file "../../xmldata/pbl/";' you get the error
7.33 -
7.34 -### pbl2file: id = ["Biegelinie"]
7.35 -*** Type unification failed: Clash of types "fun" and "Program.ID".
7.36 -*** Type error in application: Incompatible operand type.
7.37 -***
7.38 -*** Operator: Problem :: ID * ID list => ??'a
7.39 -*** Operand: (Biegelinie, [Biegelinie]) ::
7.40 -*** ((real => real) => una) * ((real => real) => una) list
7.41 -***
7.42 -Exception- OPTION raised
7.43 -*)
7.44 -
7.45 -if Pbl_Met_Hierarchy.pbl2xml ["Biegelinien"] (Problem.from_store ["Biegelinien"]) =
7.46 - "<NODECONTENT>\n"^
7.47 - " <GUH> pbl_bieg </GUH>\n"^
7.48 - " <STRINGLIST>\n"^
7.49 - " <STRING> Biegelinien </STRING>\n"^
7.50 - " </STRINGLIST>\n <META> </META>\n"^
7.51 - " <HEADLINE>\n"^
7.52 - " <MATHML>\n"^
7.53 - " <ISA> Problem (Biegelinie', [Biegelinien]) </ISA>\n"^
7.54 - " </MATHML>\n"^
7.55 - " </HEADLINE>\n"^
7.56 -
7.57 - " <GIVEN>\n"^
7.58 - " <MATHML>\n"^
7.59 - " <ISA> Traegerlaenge l_l </ISA>\n"^
7.60 - " </MATHML>\n"^
7.61 - " <MATHML>\n"^
7.62 - " <ISA> Streckenlast q_q </ISA>\n"^
7.63 - " </MATHML> </GIVEN>\n <WHERE> </WHERE>\n"^
7.64 - " <FIND>\n"^
7.65 - " <MATHML>\n"^
7.66 - " <ISA> Biegelinie b_b </ISA>\n"^
7.67 - " </MATHML> </FIND>\n"^
7.68 - " <RELATE>\n"^
7.69 - " <MATHML>\n"^
7.70 - " <ISA> Randbedingungen r_b </ISA>\n"^
7.71 - " </MATHML> </RELATE>\n"^
7.72 -
7.73 - " <EXPLANATIONS> </EXPLANATIONS>\n"^
7.74 - " <THEORY>\n"^
7.75 - " <KESTOREREF>\n"^
7.76 - " <TAG> Theorem </TAG>\n"^
7.77 - " <ID> </ID>\n"^
7.78 - " <GUH> thy_isac_Biegelinie-thm- </GUH>\n"^
7.79 - " </KESTOREREF>\n"^
7.80 - " </THEORY>\n"^
7.81 -
7.82 - " <METHODS>\n"^
7.83 - " <KESTOREREF>\n"^
7.84 - " <TAG> MethodC</TAG>\n"^
7.85 - " <ID> [IntegrierenUndKonstanteBestimmen2] </ID>\n"^
7.86 - " <GUH> met_biege_2 </GUH>\n"^
7.87 - " </KESTOREREF>\n"^
7.88 - " </METHODS>\n"^
7.89 -
7.90 - " <EVALPRECOND> empty </EVALPRECOND>\n"^
7.91 - " <MATHAUTHORS>\n"^
7.92 - " </MATHAUTHORS>\n"^
7.93 - " <COURSEDESIGNS>\n"^
7.94 - " <STRING> isac team 2006 </STRING>\n"^
7.95 - " </COURSEDESIGNS>\n"^
7.96 - "</NODECONTENT>"
7.97 -then () else error "fun pbl2xml 'Biegelinien' changed";
7.98 -
7.99 -(* val id = ["Biegelinie"];
7.100 - val {(*guh,*)cas,met,ppc,prls,thy,where_} = Problem.from_store ["Biegelinie"];
7.101 - AND STEP THROUGH pbl2xml ...
7.102 -
7.103 - term2xml i (pbl2term thy id);
7.104 - pbl2term thy id;
7.105 - *)
7.106 -(* val (thy, pblRD) = (thy, id);
7.107 - AND STEP THROUGH pbl2term...
7.108 -
7.109 - val str = ("Problem (" ^
7.110 - (get_thy o theory2domID) thy ^ ", " ^
7.111 - (strs2str' o rev) pblRD ^ ")");
7.112 - TermC.str2term str;
7.113 - TermC.str2term "Biegelinie";
7.114 - TermC.str2term "Biegelinien";
7.115 - *)
7.116 -(*Const
7.117 - ("Biegelinie.Biegelinie",
7.118 - "("Real.real => "Real.real) => Tools.una") : Term.term
7.119 -..I.E. THE "Program.ID" _WAS_ ALREADY OCCUPIED BY A 'description'*)
7.120 -
7.121 -
7.122 -"----- ERROR Illegal reference to internal variable: 'Pure_' -----";
7.123 -"----- ERROR Illegal reference to internal variable: 'Pure_' -----";
7.124 -"----- ERROR Illegal reference to internal variable: 'Pure_' -----";
7.125 -val path = "/tmp/";
7.126 -"~~~~~ fun pbls2file, args:"; val (p: Pbl_Met_Hierarchy.filepath) = (path ^ "pbl/");
7.127 -get_ptyps (); (*not = []*)
7.128 -"~~~~~ fun nodes, args:"; val (pa, ids, po, wfn, (n::ns)) =
7.129 - (p, []: string list, [0], Pbl_Met_Hierarchy.pbl2file, (get_ptyps ()));
7.130 -"~~~~~ fun node, args:"; val (pa: Pbl_Met_Hierarchy.filepath, ids, po, wfn, Store.Node (id,[n],ns)) = (pa, ids, po, wfn, n);
7.131 -val po' = lev_on po;
7.132 -wfn (*= pbl2file*)
7.133 -"~~~~~ fun pbl2file, args:"; val ((path:Pbl_Met_Hierarchy.filepath), (pos:pos), (id: MethodC.id), (pbl as {guh,...})) =
7.134 - (pa, po', (ids@[id]), n);
7.135 -strs2str id = "[\"e_pblID\"]"; (*true*)
7.136 -pos2str pos = "[1]"; (*true*)
7.137 -path ^ Thy_Present.guh2filename guh = "/tmp/pbl/pbl_empty.xml"; (*true*)
7.138 -"~~~~~ fun pbl2xml, args:"; val (id: Problem.id, {guh,mathauthors,init,cas,met,ppc,prls,thy,where_}) =
7.139 - (id, pbl);
7.140 -"~~~~~ fun pbl2term, args:"; val (thy, (pblRD:Problem.id_reverse)) = (thy, id);
7.141 -if ("Problem (" ^ Context.theory_name thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")") =
7.142 - "Problem (Pure', [empty_probl_id])"
7.143 -then () else error "fun pbl2term changed";
7.144 -
7.145 -
7.146 -"----- fun pbl2term ----------------------------------------------";
7.147 -"----- fun pbl2term ----------------------------------------------";
7.148 -"----- fun pbl2term ----------------------------------------------";
7.149 -(*see WN120405a.TODO.txt*)
7.150 -if UnparseC.term (Pbl_Met_Hierarchy.pbl2term (ThyC.get_theory "Isac_Knowledge") ["equations", "univariate", "normalise"]) =
7.151 - "Problem (Isac_Knowledge', [normalise, univariate, equations])"
7.152 -then () else error "fun pbl2term changed";
7.153 -
7.154 -"----- fun insert_errpats ----------------------------------------";
7.155 -"----- fun insert_errpats ----------------------------------------";
7.156 -"----- fun insert_errpats ----------------------------------------";
7.157 -(* vv--- here intermediate save/restore does not work and affects other tests ---vv
7.158 - see test/../calcelems.sml --- Unsynchronized.ref doesn't work any more ---
7.159 -
7.160 -val errpatstest =
7.161 - [("chain-rule-diff-both",
7.162 - [TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
7.163 - TermC.parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
7.164 - TermC.parse_patt @{theory} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)",
7.165 - TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
7.166 - TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
7.167 - [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
7.168 - @{thm diff_ln_chain}, @{thm diff_exp_chain}])];
7.169 -
7.170 -insert_errpats ["diff", "differentiate_on_R"] errpatstest;
7.171 -
7.172 -val {errpats, ...} = MethodC.from_store ["diff", "differentiate_on_R"];
7.173 -case errpats of
7.174 - ("chain-rule-diff-both", _, _) :: _ => ()
7.175 -| _ => error "insert_errpats chain-rule-diff-both changed";
7.176 - \<up> ^^--- here intermediate save/restore does not work and affects other tests ---^^*)
7.177 -
8.1 --- a/test/Tools/isac/Test_Isac.thy Thu Apr 22 16:49:41 2021 +0200
8.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Apr 22 21:34:20 2021 +0200
8.3 @@ -295,7 +295,6 @@
8.4 ML_file "BridgeLibisabelle/thy-present.sml"
8.5 ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
8.6 ML_file "BridgeLibisabelle/datatypes.sml" (*TODO/part.*)
8.7 - ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
8.8 ML_file "BridgeLibisabelle/thy-hierarchy.sml"
8.9 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
8.10 ML_file "BridgeLibisabelle/interface.sml"
9.1 --- a/test/Tools/isac/Test_Isac_Short.thy Thu Apr 22 16:49:41 2021 +0200
9.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu Apr 22 21:34:20 2021 +0200
9.3 @@ -263,7 +263,6 @@
9.4
9.5 ML_file "BridgeLibisabelle/thy-present.sml"
9.6 ML_file "BridgeLibisabelle/mathml.sml" (*part.*)
9.7 - ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
9.8 ML_file "BridgeLibisabelle/thy-hierarchy.sml"
9.9 ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*)
9.10 ML_file "BridgeLibisabelle/interface.sml"