eliminate use of Thy_Info 12: prep.arg. ctxt in TermC, UnparseC
1 (* convert sml-datatypes to xml for libisabelle and for kbase.
2 authors: Walther Neuper 2003, 2016
3 (c) due to copyright terms
5 This code remains in order to
6 keep tests of interaction Java-frontend <-> Kernel running.
9 (*** convert sml-datatypes to xml for kbase ***)
13 | filt ((s, (t1, t2)) :: ps) =
14 if str = s then (t1 $ t2) :: filt ps else filt ps
16 fun pattern2xml j p where_ =
17 (case filterpbl "#Given" p of
18 [] => (indt j) ^ "<GIVEN> </GIVEN>\n"
19 (* val gis = filterpbl "#Given" p;
21 | gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml' j gis ^
22 (indt j) ^ "</GIVEN>\n")
25 [] => (indt j) ^ "<WHERE> </WHERE>\n"
26 | whs => (indt j) ^ "<WHERE>\n" ^ terms2xml' j whs ^
27 (indt j) ^ "</WHERE>\n")
29 (case filterpbl "#Find" p of
30 [] => (indt j) ^ "<FIND> </FIND>\n"
31 | fis => (indt j) ^ "<FIND>\n" ^ terms2xml' j fis ^
32 (indt j) ^ "</FIND>\n")
34 (case filterpbl "#Relate" p of
35 [] => (indt j) ^ "<RELATE> </RELATE>\n"
36 | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^
37 (indt j) ^ "</RELATE>\n");
39 fun prepa12xml j (terms, term) =
41 indt (j+i) ^"<PRECONDS>\n"^
42 terms2xml (j+2*i) terms ^
43 indt (j+i) ^"</PRECONDS>\n"^
44 indt (j+i) ^"<PATTERN>\n"^
45 term2xml (j+2*i) term ^
46 indt (j+i) ^"</PATTERN>\n"^
47 indt j ^"</PREPAT>\n";
48 fun prepat2xml _ [] = ""
49 | prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps;
52 (*** convert sml-datatypes to xml for libisabelle ***)
54 (** general types: lists, etc **)
56 fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
58 fun xml_of_str str = XML.Elem (("STRING", []), [XML.Text str])
59 fun xml_of_strs strs = XML.Elem (("STRINGLIST", []), map xml_of_str strs)
61 fun xml_of_int i = XML.Elem (("INT", []), [XML.Text (string_of_int i)])
63 XML.Elem (("INTLIST", []), map xml_of_int is)
65 (** isac datatypes **)
67 fun xml_of_pos tag (is, pp) =
68 XML.Elem ((tag, []), [
70 XML.Elem (("POS", []), [XML.Text (Pos.pos_2str pp)])])
72 fun xml_of_auto (Solve.Steps i) =
73 XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text (string_of_int i)])
74 | xml_of_auto Solve.CompleteModel = XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])
75 | xml_of_auto Solve.CompleteCalcHead = XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])
76 | xml_of_auto Solve.CompleteToSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])
77 | xml_of_auto Solve.CompleteSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])
78 | xml_of_auto Solve.CompleteCalc = XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])
82 | filt ((s, (t1, t2)) :: ps) =
83 if str = s then (t1 $ t2) :: filt ps else filt ps
86 fun xml_of_itm_ (I_Model.Cor (dts, _)) =
87 XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (Input_Descript.join' dts)])
88 | xml_of_itm_ (I_Model.Syn c) =
89 XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])
90 | xml_of_itm_ (I_Model.Typ c) =
91 XML.Elem (("ITEM", [("status", "typeerror")]), [XML.Text c])
92 (*type item also has 'False of cterm' set in preconds2xml WN 050618*)
93 | xml_of_itm_ (I_Model.Inc (dts, _)) =
94 XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (Input_Descript.join' dts)])
95 | xml_of_itm_ (I_Model.Sup dts) =
96 XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (Input_Descript.join' dts)])
97 | xml_of_itm_ (I_Model.Mis (d, pid)) =
98 XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])
99 | xml_of_itm_ _ = raise ERROR "xml_of_itm_: wrong argument"
100 fun xml_of_itms itms =
102 fun extract (_, _, _, _, itm_) = itm_
103 in map (xml_of_itm_ o extract) itms end
105 fun xml_of_precond (status, term) =
106 XML.Elem (("ITEM", [("status", if status then "correct" else "false")]), [xml_of_term term])
107 fun xml_of_preconds ps = map xml_of_precond ps
109 fun xml_of_model itms where_ =
111 fun eq str (_, _, _,field, _) = str = field
113 XML.Elem (("MODEL", []), [
114 XML.Elem (("GIVEN", []),
115 filter (eq "#Given") itms |> xml_of_itms),
116 XML.Elem (("WHERE", []),
117 xml_of_preconds where_),
118 XML.Elem (("FIND", []),
119 filter (eq "#Find") itms |> xml_of_itms),
120 XML.Elem (("RELATE", []),
121 filter (eq "#Relate") itms |> xml_of_itms)])
124 fun xml_of_spec (thyID, pblID, metID) =
125 XML.Elem (("SPECIFICATION", []), [
126 XML.Elem (("THEORYID", []), [XML.Text thyID]),
127 XML.Elem (("PROBLEMID", []), [xml_of_strs pblID]),
128 XML.Elem (("METHODID", []), [xml_of_strs metID])])
130 fun xml_of_variant (items, spec) =
131 XML.Elem (("VARIANT", []), [xml_of_strs items, xml_of_spec spec])
133 fun xml_of_fmz [] = xml_of_fmz [Formalise.empty]
134 | xml_of_fmz vs = XML.Elem (("FORMALIZATION", []), map xml_of_variant vs)
136 fun xml_of_modspec ((b, p_, head, gfr, where_, spec): SpecificationC.T) =
137 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
138 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
139 xml_of_model gfr where_,
140 XML.Elem (("BELONGSTO", []), [
141 XML.Text (case p_ of Pos.Pbl => "Pbl" | Pos.Met => "Met" | _ => "Und")]),
144 fun xml_of_posmodspec ((p: Pos.pos', (b, p_, head, gfr, where_, spec): SpecificationC.T)) =
145 XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [
146 xml_of_pos "POSITION" p,
147 XML.Elem (("HEAD", []), [xml_of_term_NEW head]),
148 xml_of_model gfr where_,
149 XML.Elem (("BELONGSTO", []), [
150 XML.Text (case p_ of Pos.Pbl => "Pbl" | Pos.Met => "Met" | _ => "Und")]),
153 fun xml_of_sub (id, value) =
154 XML.Elem (("PAIR", []), [
155 XML.Elem (("VARIABLE", []), [xml_of_term id]),
156 XML.Elem (("VALUE", []), [xml_of_term value])])
157 fun xml_of_subs (subs : Subst.input) =
158 XML.Elem (("SUBSTITUTION", []),
159 map xml_of_sub (Tactic.subst_adapt_to_type (ThyC.id_to_ctxt "Isac_Knowledge") subs))
160 fun xml_of_sube sube =
161 XML.Elem (("SUBSTITUTION", []),
162 map xml_of_sub (Subst.T_from_string_eqs (Know_Store.get_via_last_thy "Isac_Knowledge") sube))
164 fun thm''2xml j (thm : thm) =
165 indt j ^ "<THEOREM>\n" ^
166 indt (j+i) ^ "<ID> " ^ ThmC.id_of_thm thm ^ " </ID>\n"^
167 term2xml j (Thm.prop_of thm) ^ "\n" ^
168 indt j ^ "</THEOREM>\n";
169 fun xml_of_thm' (ID, form) =
170 XML.Elem (("THEOREM", []), [
171 XML.Elem (("ID", []), [XML.Text ID]),
172 XML.Elem (("FORMULA", []), [
173 XML.Text form])]) (* repair for MathML: use term instead String *)
174 (* at the front-end theorems can be shown by their term, so term is transported isac-java <--- ME *)
175 fun xml_of_thm'' (ID, thm) =
176 XML.Elem (("THEOREM", []), [
177 XML.Elem (("ID", []), [XML.Text ID]),
178 XML.Elem (("FORMULA", []), [
179 XML.Text ((UnparseC.term o Thm.prop_of) thm)])]) (* repair for MathML: use term instead String *)
181 fun xml_of_src Rule.Empty_Prog =
182 XML.Elem (("NOCODE", []), [XML.Text "empty"])
183 | xml_of_src (Rule.Prog term) =
184 XML.Elem (("CODE", []), [
185 if term = TermC.empty then xml_of_src Rule.Empty_Prog
186 else xml_of_term (TermC.inst_abs term)])
187 | xml_of_src (Rule.Rfuns _) =
188 XML.Elem (("NOCODE", []), [XML.Text "reverse rewrite functions"])
190 (*.convert a tactic into xml-format .*)
191 fun xml_of_tac (Tactic.Subproblem (dI, pI)) =
192 XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [
193 XML.Elem (("THEORY", []), [XML.Text dI]),
194 XML.Elem (("PROBLEM", []), [xml_of_strs pI])])
195 | xml_of_tac (Tactic.Substitute cterms) =
196 (*Substitute: sube -> tac; Subst.string_eqs_empty: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
197 XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])
198 (*----- Rewrite* -----------------------------------------------------*)
199 | xml_of_tac (Tactic.Rewrite thm'') =
200 XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm'' thm''])
201 | xml_of_tac (Tactic.Rewrite_Inst (subs, thm'')) =
202 XML.Elem (("REWRITEINSTTACTIC", [("name", "Rewrite_Inst")]), (
204 xml_of_thm'' thm'' :: []))
205 | xml_of_tac (Tactic.Rewrite_Set rls') =
206 XML.Elem (("REWRITESETTACTIC", [("name", "Rewrite_Set")]), [XML.Text rls'])
207 | xml_of_tac (Tactic.Rewrite_Set_Inst (subs, rls')) =
208 XML.Elem (("REWRITESETINSTTACTIC", [("name", "Rewrite_Set_Inst")]), ([
210 XML.Elem (("RULESET", []), [XML.Text rls'])]))
211 (*----- FORMTACTIC ---------------------------------------------------*)
212 | xml_of_tac (Tactic.Add_Find ct) =
213 XML.Elem (("FORMTACTIC", [("name", "Add_Find")]), [xml_of_cterm ct])
214 | xml_of_tac (Tactic.Add_Given ct) =
215 XML.Elem (("FORMTACTIC", [("name", "Add_Given")]), [xml_of_cterm ct])
216 | xml_of_tac (Tactic.Add_Relation ct) =
217 XML.Elem (("FORMTACTIC", [("name", "Add_Relation")]), [xml_of_cterm ct])
218 | xml_of_tac (Tactic.Check_elementwise ct) =
219 XML.Elem (("FORMTACTIC", [("name", "Check_elementwise")]), [xml_of_cterm ct])
220 | xml_of_tac (Tactic.Take ct) =
221 XML.Elem (("FORMTACTIC", [("name", "Take")]), [xml_of_cterm ct])
222 (*----- SIMPLETACTIC -------------------------------------------------*)
223 | xml_of_tac (Tactic.Calculate opstr) =
224 XML.Elem (("SIMPLETACTIC", [("name", "Calculate")]), [XML.Text opstr])
225 | xml_of_tac (Tactic.Or_to_List) =
226 XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [(*//////////*)])
227 | xml_of_tac (Tactic.Specify_Theory ct) =
228 XML.Elem (("SIMPLETACTIC", [("name", "Specify_Theory")]), [XML.Text ct])
229 (*----- STRINGLISTTACTIC ---------------------------------------------*)
230 | xml_of_tac (Tactic.Apply_Method mI) =
231 XML.Elem (("STRINGLISTTACTIC", [("name", "Apply_Method")]), [xml_of_strs mI])
232 | xml_of_tac (Tactic.Check_Postcond pI) =
233 XML.Elem (("STRINGLISTTACTIC", [("name", "Check_Postcond")]), [xml_of_strs pI])
234 | xml_of_tac Tactic.Model_Problem =
235 XML.Elem (("STRINGLISTTACTIC", [("name", "Model_Problem")]), [])
236 | xml_of_tac (Tactic.Refine_Tacitly pI) =
237 XML.Elem (("STRINGLISTTACTIC", [("name", "Refine_Tacitly")]), [xml_of_strs pI])
238 | xml_of_tac (Tactic.Specify_Method ct) =
239 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Method")]), [xml_of_strs ct])
240 | xml_of_tac (Tactic.Specify_Problem ct) =
241 XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])
244 val ctxt = Proof_Context.init_global (Know_Store.get_via_last_thy "Isac_Knowledge")
246 raise ERROR ("xml_of_tac: not impl. for " ^ Tactic.input_to_string ctxt tac)
249 val e_pblterm = TermC.parseNEW'' @{theory Prog_Tac}
250 ("Problem (" ^ ThyC.id_empty ^ ", " ^ strs2str' Problem.id_empty ^ ")");
252 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
253 fun xml_of_posterm (p, t, _) =
254 let val input_request = Free ("________________________________________________", dummyT)
256 XML.Elem (("CALCFORMULA", []),
257 [xml_of_pos "POSITION" p,
258 if t = e_pblterm (*headline in pbl is e_ <- _root_pbl for CAS-command*)
259 then xml_of_term_NEW input_request
260 else xml_of_term_NEW t])
263 fun xml_of_asm_val (asm, vl) =
264 XML.Elem (("ASMEVALUATED", []),[
265 XML.Elem (("ASM", []), [xml_of_term asm]),
266 XML.Elem (("VALUE", []), [xml_of_term vl])])
268 fun xml_of_matchpbl (model_ok, _(*pI*), hdl, pbl, where_) =
269 XML.Elem (("CONTEXTDATA", []), [
270 XML.Elem (("GUH", []), [(XML.Text "would-need-ctxt")(*XML.Text (Ptool.pblID2guh pI)*)]),
271 XML.Elem (("STATUS", []), [
272 XML.Text ((if model_ok then "correct" else "incorrect"))]),
273 XML.Elem (("HEAD", []), [xml_of_term_NEW hdl]),
274 xml_of_model pbl where_])
276 fun xml_of_matchmet (model_ok, pI, program, pbl, where_) =
277 XML.Elem (("CONTEXTDATA", []), [
278 XML.Elem (("GUH", []), [XML.Text (Ptool.metID2guh pI)]),
279 XML.Elem (("STATUS", []), [
280 XML.Text ((if model_ok then "correct" else "incorrect"))]),
281 XML.Elem (("PROGRAM", []), [xml_of_src program]),
282 xml_of_model pbl where_])
284 fun xml_of_calcchanged calcid tag old del new =
285 XML.Elem ((tag, []),[
286 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
287 XML.Elem (("CALCCHANGED", []), [
288 xml_of_pos "UNCHANGED" old,
289 xml_of_pos "DELETED" del,
290 xml_of_pos "GENERATED" new])])
292 (* for checking output at Frontend *)
293 fun cut_xml xml i = xml |> xmlstr 0 |> Symbol.explode |> curry take i |> implode