Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Pure/isac/xmlsrc/interface-xml.sml
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 21 Jul 2010 13:53:39 +0200
branchisac-from-Isabelle2009-2
changeset 37871 875b6efa7ced
permissions -rw-r--r--
added isac-hook in Pure/thm and isac-code 
     1 (* interface between isac math engine and java:

     2    java -> sml: strings on stdin

     3    sml -> java: xml on stdout

     4 

     5    WN071004 The xml still reflects the insecurity during the first 

     6    implementation phase, how the communication via stdin/out could

     7    correctly relate multiple sml-calculations and java-calculations.

     8 

     9    Since this insecurity turned out unjustified, the xml can be

    10    simplified in several ways:

    11    # omit the CALCID; the relation is done by 

    12      "@@@@@begin@@@@@\n "^string_of_int uI

    13    # omit the distinctions APPENDFORMULA, REPLACEFORMULA, ...

    14    WN071004 these 2 simplifications are begun with CALCMESSAGE

    15 

    16    use"xmlsrc/interface-xml.sml";

    17    use"interface-xml.sml";

    18    *)

    19 

    20 type iterID = int;

    21 type calcID = int;

    22 

    23 

    24 

    25 (** add and delete users -----------------------------------------------

    26  FIXXME.8.03 addUser: clear code, because only CalcTrees distinguished**)

    27 fun adduserOK2xml (cI:calcID) (uI:iterID) = 

    28     writeln ("@@@@@begin@@@@@\n "^string_of_int uI^" \n\

    29 	     \<ADDUSER>\n\

    30 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

    31 	     \  <USERID> "^string_of_int uI^" </USERID>\n\

    32 	     \</ADDUSER>\n\

    33 	     \@@@@@end@@@@@");

    34 fun deluserOK2xml (cI:calcID) (uI:iterID) = 

    35     writeln ("@@@@@begin@@@@@\n "^string_of_int uI^" \n\

    36 	     \<DELUSER>\n\

    37 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

    38 	     \  <USERID> "^string_of_int uI^" </USERID>\n\

    39 	     \</DELUSER>\n\

    40 	     \@@@@@end@@@@@");

    41 (*---------------------------------------------------------------------*)

    42 

    43 fun calctreeOK2xml (*uI:iterID*) (cI:calcID) = 

    44     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

    45 	     \<CALCTREE>\n\

    46 	     \   <CALCID> "^string_of_int cI^" </CALCID>\n\

    47 	     \</CALCTREE>\n\

    48 	     \@@@@@end@@@@@");

    49 fun deconstructcalctreeOK2xml (*uI:userID*) (cI:calcID) = 

    50     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

    51 	     \<DELCALC>\n\

    52 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

    53 	     \</DELCALC>\n\

    54 	     \@@@@@end@@@@@");

    55 

    56 fun iteratorOK2xml (cI:calcID) (p:pos')= 

    57     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

    58 	     \<CALCITERATOR>\n\

    59 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n" ^

    60 	     pos'2xml i ("POSITION", p) ^

    61 	     "</CALCITERATOR>\n\

    62 	     \@@@@@end@@@@@");

    63 fun iteratorERROR2xml (cI:calcID) = 

    64     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

    65 	     \<CALCITERATOR>\n\

    66 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

    67 	     \  <ERROR> pos does not exist </ERROR>\n\

    68 	     \</CALCITERATOR>\n\

    69 	     \@@@@@end@@@@@");

    70 

    71 fun sysERROR2xml (cI:calcID) "" = 

    72     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

    73 	     \<SYSERROR>\n\

    74 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

    75 	     \  <ERROR> in kernel </ERROR>\n\

    76 	     \</SYSERROR>\n\

    77 	     \@@@@@end@@@@@")

    78   | sysERROR2xml (cI:calcID) str = 

    79     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

    80 	     \<SYSERROR>\n\

    81 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

    82 	     \  <ERROR> "^str^" </ERROR>\n\

    83 	     \</SYSERROR>\n\

    84 	     \@@@@@end@@@@@");

    85 

    86 fun refformulaOK2xml (cI:calcID) p (Form t) = 

    87     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

    88 	     \<REFFORMULA>\n\

    89              \  <CALCID> "^string_of_int cI^" </CALCID>\n\

    90 	     \  <CALCFORMULA>\n"^

    91 	     pos'2xml (2*i) ("POSITION", p) ^

    92 	     "    <FORMULA>"^

    93 	     term2xml (2*i) t ^"\n"^

    94 	     "    </FORMULA>\n\ 

    95 	     \  </CALCFORMULA>\n\ 

    96 	     \</REFFORMULA>\n\ 

    97 	     \@@@@@end@@@@@") 

    98   | refformulaOK2xml (cI:calcID) p (ModSpec modspec) =

    99     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   100 	     \<REFFORMULA>\n\

   101              \  <CALCID> "^string_of_int cI^" </CALCID>\n"^

   102 	     pos'calchead2xml i (p, modspec)^ 

   103 	     "</REFFORMULA>\n\ 

   104 	     \@@@@@end@@@@@"); 

   105 

   106 fun refformulaERROR2xml (cI:calcID) = (*FIXME.WN.29.8.03 unused*)

   107     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   108 	     \<REFFORMULA>\n\

   109 	     \   <ERROR> object is not a formula </ERROR>\n\

   110 	     \</REFFORMULA>\n\

   111 	     \@@@@@end@@@@@");

   112 

   113 (* val (cI, tac) = (cI, ta);

   114    *)

   115 fun gettacticOK2xml (cI:calcID) tac = 

   116     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   117 	     \<GETTACTIC>\n\

   118 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n"^

   119 	     tac2xml i tac^

   120 	     "</GETTACTIC>\n\

   121 	     \@@@@@end@@@@@");

   122 fun gettacticERROR2xml (cI:calcID) str = 

   123     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   124 	     \<GETTACTIC>\n\

   125 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

   126 	     \  <ERROR> "^str^" </ERROR>\n\

   127 	     \</GETTACTIC>\n\

   128 	     \@@@@@end@@@@@");

   129 

   130 fun applicabletacticsOK cI tacs =

   131     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   132 	     \<APPLICABLETACTICS>\n\

   133 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

   134 	     \  <TACLIST>\n"^

   135 	     tacs2xml (2*i) tacs^

   136 	     "  </TACLIST>\n\

   137 	     \</APPLICABLETACTICS>\n\

   138 	     \@@@@@end@@@@@");

   139 

   140 fun getasmsOK2xml (cI:calcID) terms = 

   141     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   142 	     \<GETASSUMPTIONS>\n\

   143 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

   144 	     \  <ASMLIST>\n"^

   145 	     formulae2xml (i+i) terms ^

   146 	     "  </ASMLIST>\n\

   147 	     \</GETASSUMPTIONS>\n\

   148 	     \@@@@@end@@@@@");

   149 (* getasmsOK2xml 333 [str2term "1+1=2", str2term "1+1+1=3"];

   150    *)

   151 

   152 (*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)

   153 fun getaccuasmsOK2xml cI asms =

   154     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   155 	     \<GETACCUMULATEDASMS>\n\

   156 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

   157 	     \  <ASMLIST>\n"^

   158 	     formulae2xml (i+i) asms^

   159 	     "  </ASMLIST>\n\

   160 	     \</GETACCUMULATEDASMS>\n\

   161 	     \@@@@@end@@@@@");

   162 (* getaccuasmsOK2xml 333 [(([1],Res), str2term "1+1=2"),

   163 			  (([2],Res), str2term "1+1+1=3")];

   164    getaccuasmsOK2xml 333 [str2term "1+1=2", str2term "1+1+1=3"];

   165    *)

   166 

   167 fun getintervalOK (cI:calcID) fs = 

   168     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   169 	     \<GETELEMENTSFROMTO>\n\

   170 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

   171 	     \  <FORMHEADS>\n"^	     

   172 	     posterms2xml (2*i) fs^

   173 	     "  </FORMHEADS>\n\	     

   174 	     \</GETELEMENTSFROMTO>\n\

   175 	     \@@@@@end@@@@@");

   176 

   177 

   178 fun matchpbl2xml (cI:calcID) (model_ok, pI, hdl, pbl, pre) =

   179     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^

   180 	     "<CONTEXTPBL>\n" ^

   181 	     "  <GUH> " ^ pblID2guh pI ^ " </GUH>\n" ^

   182 	     "  <STATUS> " ^ (if model_ok 

   183 			     then "correct" 

   184 			     else "incorrect") ^ " </STATUS>\n" ^

   185 	     "  <HEAD>\n" ^

   186 	     term2xml i hdl ^ "\n" ^

   187 	     "  </HEAD>\n" ^

   188 	     model2xml i pbl pre ^

   189 	     "</CONTEXTPBL>\n\

   190 	     \@@@@@end@@@@@");

   191 

   192 fun matchmet2xml (cI:calcID) (model_ok, pI, scr, pbl, pre) =

   193     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^

   194 	     "<CONTEXTMET>\n" ^

   195 	     "  <GUH> " ^ metID2guh pI ^ " </GUH>\n" ^

   196 	     "  <STATUS> " ^ (if model_ok 

   197 			     then "correct" 

   198 			     else "incorrect") ^ " </STATUS>\n" ^

   199 	     scr2xml i scr ^

   200 	     model2xml i pbl pre ^

   201 	     "</CONTEXTMET>\n\

   202 	     \@@@@@end@@@@@");

   203 

   204 

   205 fun tryrefineOK2xml (cI:calcID) (ModSpec modspec) =

   206     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   207 	     \<TRYREFINE>\n\

   208              \  <CALCID> "^string_of_int cI^" </CALCID>\n"^

   209 	     modspec2xml i modspec^ 

   210 	     "</TRYREFINE>\n\ 

   211 	     \@@@@@end@@@@@"); 

   212 

   213 fun appendformulaOK2xml (cI:calcID) (old:pos') (del:pos') (new:pos') =

   214     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   215 	     \<APPENDFORMULA>\n\

   216 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

   217 	     \  <CALCCHANGED>\n" ^

   218 	     pos'2xml (2*i) ("UNCHANGED", old) ^ 

   219 	     pos'2xml (2*i) ("DELETED", del) ^ 

   220 	     pos'2xml (2*i) ("GENERATED", new) ^ 

   221 	     "  </CALCCHANGED>\n\

   222 	     \</APPENDFORMULA>\n\

   223 	     \@@@@@end@@@@@");

   224 (* appendformulaOK2xml 1 ([2],Frm) ([3],Pbl) ([4],Res);

   225    *)

   226 fun appendformulaERROR2xml (cI:calcID) msg =

   227     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   228 	     \<CALCMESSAGE> "^ msg ^" </CALCMESSAGE>\n\

   229 	     \@@@@@end@@@@@");

   230 

   231 fun replaceformulaOK2xml (cI:calcID) (old:pos') (del:pos') (new:pos') =

   232     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   233 	     \<REPLACEFORMULA>\n\

   234 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

   235 	     \  <CALCCHANGED>\n" ^

   236 	     pos'2xml (2*i) ("UNCHANGED", old) ^ 

   237 	     pos'2xml (2*i) ("DELETED", del) ^ 

   238 	     pos'2xml (2*i) ("GENERATED", new) ^ 

   239 	     "  </CALCCHANGED>\n\

   240 	     \</REPLACEFORMULA>\n\

   241 	     \@@@@@end@@@@@");

   242 fun replaceformulaERROR2xml (cI:calcID) msg =

   243     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   244 	     \<CALCMESSAGE> "^ msg ^" </CALCMESSAGE>\n\

   245 	     \@@@@@end@@@@@");

   246 

   247 fun message2xml (cI:calcID) e = 

   248     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   249 	     \<MESSAGE>\n\

   250 	     \   <CALCID> "^string_of_int cI^" </CALCID>\n\

   251 	     \   <STRING> "^e^" </STRING>\n\

   252 	     \</MESSAGE>\n\

   253 	     \@@@@@end@@@@@");

   254 

   255 fun setnexttactic2xml (*uI:iterID*) (cI:calcID) e = 

   256     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   257 	     \<SETNEXTTACTIC>\n\

   258 	     \   <CALCID> "^string_of_int cI^" </CALCID>\n\

   259 	     \   <MESSAGE> "^e^" </MESSAGE>\n\

   260 	     \</SETNEXTTACTIC>\n\

   261 	     \@@@@@end@@@@@");

   262 

   263 fun fetchproposedtacticOK2xml (*uI:userID*) (cI:calcID) tac = 

   264     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   265 	     \<NEXTTAC>\n\

   266 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n"^

   267 	     tac2xml i tac^

   268 (*	     ^(strs2xml o (map (tac2xml i))) tacs^*)

   269 	     "</NEXTTAC>\n\

   270 	     \@@@@@end@@@@@");

   271 (* fetchproposedtactic2xml 11 22 (Rewrite ("rmult_commute","?m *?n =?n *?m"));

   272    *)

   273 fun fetchproposedtacticERROR2xml (*uI:userID*) (cI:calcID) e = 

   274     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   275 	     \<NEXTTAC>\n\

   276 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

   277 	     \  <ERROR> "^ e ^" </ERROR>\n\

   278 	     \</NEXTTAC>\n\

   279 	     \@@@@@end@@@@@");

   280 

   281 (*. UNCHANGED: the pos' of the active formula autocalculate has been applied at

   282     DELETED:   last pos' of the succesional sequence of formulae prob. deleted

   283     GENERATED: the pos' of the new active formula

   284 .*)

   285 fun autocalculateOK2xml (cI:calcID) (old:pos') (del:pos') (new:pos') = 

   286     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   287 	     \<AUTOCALC>\n\

   288 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

   289 	     \  <CALCCHANGED>\n" ^

   290 	     pos'2xml (2*i) ("UNCHANGED", old) ^ 

   291 	     pos'2xml (2*i) ("DELETED", del) ^ 

   292 	     pos'2xml (2*i) ("GENERATED", new) ^ 

   293 	     "  </CALCCHANGED>\n\

   294 	     \</AUTOCALC>\n\

   295 	     \@@@@@end@@@@@");

   296 (* autocalculate2xml 11 22 (Rewrite ("rmult_commute","?m *?n =?n *?m"));

   297    *)

   298 fun autocalculateERROR2xml (cI:calcID) e = 

   299     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   300 	     \<CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n\

   301 	     \@@@@@end@@@@@");

   302 

   303 fun interStepsOK (cI:calcID) (*pos'forms*) (old:pos') (del:pos') (new:pos') =

   304     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   305 	     \<INTERSTEPS>\n\

   306 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

   307 	     \  <CALCCHANGED>\n" ^

   308 	     pos'2xml (2*i) ("UNCHANGED", old) ^ 

   309 	     pos'2xml (2*i) ("DELETED", del) ^ 

   310 	     pos'2xml (2*i) ("GENERATED", new) ^ 

   311 	     "  </CALCCHANGED>\n\

   312 	     \</INTERSTEPS>\n\

   313 	     \@@@@@end@@@@@");

   314 fun interStepsERROR (cI:calcID) e =

   315     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   316 	     \  <CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n\

   317 	     \@@@@@end@@@@@");

   318 

   319 fun modifycalcheadOK2xml (cI:calcID) (chd as (complete,p_,_,_,_,_):ocalhd) =

   320     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   321 	     \<MODIFYCALCHEAD>\n\

   322 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\

   323 	     \  <STATUS> "^(if complete then "complete" 

   324 			    else "incomplete")^ "</STATUS>\n"^

   325 	     modspec2xml i chd^

   326 	     "</MODIFYCALCHEAD>\n\

   327 	     \@@@@@end@@@@@");

   328 

   329 (* val (cI, contthy) = (cI, (context_thy (pt,pos) tac));

   330    *)

   331 fun contextthyOK2xml cI contthy = 

   332     writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\

   333 	     \<CONTEXTTHY>\n\

   334 	     \  <CALCID> "^string_of_int cI^" </CALCID>\n" ^

   335 	     contthy2xml i contthy ^

   336 	     "</CONTEXTTHY>\n\

   337 	     \@@@@@end@@@@@");

   338 

   339 (*

   340 fun contextthyNO2xml guh = 

   341     writeln (datatypes.contextthyNO2xml 0 guh);

   342 *)
wneuper/isa