1.1 --- a/src/Tools/isac/Frontend/interface.sml Sun May 31 09:36:22 2015 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Sun May 31 10:24:16 2015 +0200
1.3 @@ -19,24 +19,23 @@
1.4 val autoCalculate : calcID -> auto -> XML.tree (*unit future*)
1.5 val checkContext : calcID -> pos' -> guh -> XML.tree
1.6 val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree
1.7 - val fetchProposedTactic : calcID -> unit
1.8 + val fetchProposedTactic : calcID -> XML.tree
1.9 val applyTactic : calcID -> pos' -> tac -> XML.tree
1.10 - val getAccumulatedAsms : calcID -> pos' -> unit
1.11 + val getAccumulatedAsms : calcID -> pos' -> XML.tree
1.12 val getActiveFormula : calcID -> XML.tree
1.13 - val getAssumptions : calcID -> pos' -> unit
1.14 + val getAssumptions : calcID -> pos' -> XML.tree
1.15 val initContext : calcID -> ketype -> pos' -> XML.tree
1.16 val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree
1.17 - val getTactic : calcID -> pos' -> unit
1.18 + val getTactic : calcID -> pos' -> XML.tree
1.19 val interSteps : calcID -> pos' -> XML.tree
1.20 val modifyCalcHead : calcID -> icalhd -> XML.tree
1.21 val moveActiveCalcHead : calcID -> XML.tree
1.22 val moveActiveDown : calcID -> XML.tree
1.23 - val moveActiveDownTEST : calcID -> unit
1.24 val moveActiveFormula : calcID -> pos' -> XML.tree
1.25 val moveActiveLevelDown : calcID -> XML.tree
1.26 val moveActiveLevelUp : calcID -> XML.tree
1.27 val moveActiveRoot : calcID -> XML.tree
1.28 - val moveActiveRootTEST : calcID -> unit
1.29 + val moveActiveRootTEST : calcID -> XML.tree
1.30 val moveActiveUp : calcID -> XML.tree
1.31 val moveCalcHead : calcID -> pos' -> XML.tree
1.32 val moveDown : calcID -> pos' -> XML.tree
1.33 @@ -48,13 +47,13 @@
1.34 val replaceFormula : calcID -> cterm' -> XML.tree
1.35 val resetCalcHead : calcID -> XML.tree
1.36 val modelProblem : calcID -> XML.tree
1.37 - val refineProblem : calcID -> pos' -> guh -> unit
1.38 + val refineProblem : calcID -> pos' -> guh -> XML.tree
1.39 val setContext : calcID -> pos' -> guh -> XML.tree
1.40 val setMethod : calcID -> metID -> XML.tree
1.41 - val setNextTactic : calcID -> tac -> unit
1.42 + val setNextTactic : calcID -> tac -> XML.tree
1.43 val setProblem : calcID -> pblID -> XML.tree
1.44 val setTheory : calcID -> thyID -> XML.tree
1.45 - val findFillpatterns : calcID -> errpatID -> unit
1.46 + val findFillpatterns : calcID -> errpatID -> XML.tree
1.47 val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree
1.48 val inputFillFormula: calcID -> string -> XML.tree
1.49 (*------------ for tests*)
1.50 @@ -143,8 +142,6 @@
1.51 val ((pt, _), _) = get_calc cI
1.52 val ip = get_pos cI 1
1.53 in case locatetac tac (pt, ip) of
1.54 -(* val ("ok", (tacis, c, (_,p'))) = locatetac tac (pt, ip);
1.55 - *)
1.56 ("ok", (tacis, _, _)) =>
1.57 (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")
1.58 | ("unsafe-ok", (tacis, _, _)) =>
1.59 @@ -152,7 +149,7 @@
1.60 | ("not-applicable",_) => setnexttactic2xml cI "not-applicable"
1.61 | ("end-of-calculation",_) =>
1.62 setnexttactic2xml cI "end-of-calculation"
1.63 - | ("failure",_) => sysERROR2xml cI "failure"
1.64 + | ("failure",_) => sysERROR2xmlTODO cI "failure"
1.65 end;
1.66
1.67 (*. apply a tactic at a position and update the calc-tree if applicable .*)
1.68 @@ -188,7 +185,7 @@
1.69 | ("no-fmz-spec",_) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
1.70 | ("end-of-calculation",_) =>
1.71 fetchproposedtacticERROR2xml cI "end-of-calculation")
1.72 - handle _ => sysERROR2xml cI "error in kernel";
1.73 + handle _ => sysERROR2xmlTODO cI "error in kernel";
1.74
1.75 (*original see ~~/src/Tools/isac/Interpret/solve.sml:
1.76 datatype auto = FIXXXME040624: does NOT match interfaces/ITOCalc.java
1.77 @@ -243,9 +240,9 @@
1.78 val (form, tac, asms) = pt_extract (pt, p)
1.79 in case tac of
1.80 SOME ta => gettacticOK2xml cI ta
1.81 - | NONE => gettacticERROR2xml cI ("no tactic at position "^pos'2str p)
1.82 + | NONE => gettacticERROR2xml cI ("no tactic at position " ^ pos'2str p)
1.83 end)
1.84 - handle _ => sysERROR2xml cI "syserror in getTactic";
1.85 + handle _ => sysERROR2xmlTODO cI "syserror in getTactic";
1.86
1.87 (*. see ICalcIterator#fetchApplicableTactics
1.88 @see #TACTICS_ALL
1.89 @@ -275,7 +272,7 @@
1.90 (let val ((pt,_),_) = get_calc cI
1.91 val (_, _, asms) = pt_extract (pt, p)
1.92 in getasmsOK2xml cI asms end)
1.93 - handle _ => sysERROR2xml cI "syserror in getAssumptions";
1.94 + handle _ => sysERROR2xmlTODO cI "syserror in getAssumptions";
1.95
1.96 (*WN0502 @see ME/ctree: type asms: illdesigned, thus no positions returned*)
1.97 fun getAccumulatedAsms cI (p:pos') =
1.98 @@ -283,7 +280,7 @@
1.99 val ass = get_assumptions_ pt p
1.100 in (*getaccuasmsOK2xml cI (get_assumptions_ pt p)*)
1.101 getasmsOK2xml cI ass end)
1.102 - handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms";
1.103 + handle _ => sysERROR2xmlTODO cI "syserror in getAccumulatedAsms";
1.104
1.105
1.106 (*since moveActive* does NOT transfer pos java --> sml (only sml --> java)
1.107 @@ -508,8 +505,8 @@
1.108 val ((pt,_),_) = get_calc cI
1.109 val pp = par_pblobj pt p
1.110 val chd = tryrefine pblID pt (pp, p_)
1.111 - in matchpbl2xml cI chd end)
1.112 - handle _ => sysERROR2xml cI "error in kernel";
1.113 + in xml_of_matchpbl cI chd end)
1.114 + handle _ => sysERROR2xmlTODO cI "error in kernel";
1.115
1.116 (* append a formula to the calculation *)
1.117 fun appendFormula' cI (ifo:cterm') =
1.118 @@ -570,8 +567,8 @@
1.119 handle e => sysERROR2xmlTODO cI "";
1.120 fun moveActiveRootTEST cI =
1.121 (let val _ = upd_ipos cI 1 ([],Pbl)
1.122 - in (*iteratorOK2xml cI ([],Pbl)*)() end)
1.123 - handle e => sysERROR2xml cI "error in kernel";
1.124 + in iteratorOK2xml cI ([],Pbl) end)
1.125 + handle e => sysERROR2xmlTODO cI "error in kernel";
1.126
1.127 (* val (cI, uI) = (1,1);
1.128 val (cI, uI) = (1,2);
1.129 @@ -599,13 +596,6 @@
1.130 in iteratorOK2xml cI ip' end)
1.131 handle (PTREE e) => iteratorERROR2xml cI)
1.132 handle _ => sysERROR2xmlTODO cI "error in kernel";
1.133 -fun moveActiveDownTEST cI =
1.134 - let val ((pt,_),_) = get_calc cI
1.135 - val ip = get_pos cI 1
1.136 - val ip' = (move_dn [] pt ip)
1.137 - handle _ => ip
1.138 - val _ = upd_ipos cI 1 ip'
1.139 - in (*iteratorOK2xml cI uI*)() end;
1.140
1.141 fun moveActiveLevelDown cI =
1.142 ((let val ((pt,_),_) = get_calc cI
2.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Sun May 31 09:36:22 2015 +0200
2.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Sun May 31 10:24:16 2015 +0200
2.3 @@ -190,8 +190,10 @@
2.4 indt j ^ "<FORMULA>\n"^
2.5 term2xml j term ^"\n"^
2.6 indt j ^ "</FORMULA>\n" : xml;
2.7 -(* writeln(formula2xml 6 (str2term "1+1=2"));
2.8 - *)
2.9 +fun xml_of_formula term =
2.10 + XML.Elem (("FORMULA", []), [
2.11 + XML.Elem (("CALCID", []), [xml_of_term term])])
2.12 +
2.13 fun formulae2xml j [] = ("":xml)
2.14 | formulae2xml j (r::rs) = formula2xml j r ^ formulae2xml j rs;
2.15 (* writeln(formulae2xml 6 [str2term "1+1=2", str2term "1+1+1=3"]);
3.1 --- a/src/Tools/isac/xmlsrc/interface-xml.sml Sun May 31 09:36:22 2015 +0200
3.2 +++ b/src/Tools/isac/xmlsrc/interface-xml.sml Sun May 31 10:24:16 2015 +0200
3.3 @@ -148,6 +148,11 @@
3.4 tac2xml i tac^
3.5 "</GETTACTIC>\n" ^
3.6 "@@@@@end@@@@@");
3.7 +fun gettacticOK2xml (calcid : calcID) tac =
3.8 + XML.Elem (("GETTACTIC", []),[
3.9 + XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
3.10 + XML.Elem (("CALCCHANGED", []), [xml_of_tac tac])])
3.11 +
3.12 fun gettacticERROR2xml (cI:calcID) str =
3.13 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
3.14 "<GETTACTIC>\n" ^
3.15 @@ -155,6 +160,10 @@
3.16 " <ERROR> "^str^" </ERROR>\n" ^
3.17 "</GETTACTIC>\n" ^
3.18 "@@@@@end@@@@@");
3.19 +fun gettacticERROR2xml (calcid : calcID) str =
3.20 + XML.Elem (("GETTACTIC", []),[
3.21 + XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
3.22 + XML.Elem (("ERROR", []), [XML.Text str])])
3.23
3.24 fun applicabletacticsOK cI tacs =
3.25 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
3.26 @@ -179,8 +188,10 @@
3.27 " </ASMLIST>\n" ^
3.28 "</GETASSUMPTIONS>\n" ^
3.29 "@@@@@end@@@@@");
3.30 -(* getasmsOK2xml 333 [str2term "1+1=2", str2term "1+1+1=3"];
3.31 - *)
3.32 +fun getasmsOK2xml (calcid : calcID) terms =
3.33 + XML.Elem (("APPLICABLETACTICS", []), [
3.34 + XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
3.35 + XML.Elem (("ASMLIST", []), (map xml_of_formula terms))])
3.36
3.37 (*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)
3.38 fun getaccuasmsOK2xml cI asms =
3.39 @@ -326,6 +337,10 @@
3.40 " <MESSAGE> "^e^" </MESSAGE>\n" ^
3.41 "</SETNEXTTACTIC>\n" ^
3.42 "@@@@@end@@@@@");
3.43 +fun setnexttactic2xml (calcid : calcID) e =
3.44 + XML.Elem (("SETNEXTTACTIC", []), [
3.45 + XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
3.46 + XML.Elem (("MESSAGE", []), [XML.Text e])])
3.47
3.48 fun fetchproposedtacticOK2xml (cI:calcID) tac _ =
3.49 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
3.50 @@ -345,6 +360,12 @@
3.51 " </TACTICERRORPATTERNS>\n" ^
3.52 "</NEXTTAC>\n" ^
3.53 "@@@@@end@@@@@");
3.54 +fun fetchproposedtacticOK2xml (calcid : calcID) tac (errpatIDs : errpatID list) =
3.55 + XML.Elem (("NEXTTAC", []), [
3.56 + XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
3.57 + XML.Elem (("TACTICERRORPATTERNS", []), [
3.58 + xml_of_strs errpatIDs,
3.59 + xml_of_tac tac])])
3.60
3.61 fun fetchproposedtacticERROR2xml (*uI:userID*) (cI:calcID) e =
3.62 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
3.63 @@ -353,6 +374,10 @@
3.64 " <ERROR> "^ e ^" </ERROR>\n" ^
3.65 "</NEXTTAC>\n" ^
3.66 "@@@@@end@@@@@");
3.67 +fun fetchproposedtacticERROR2xml (calcid : calcID) e =
3.68 + XML.Elem (("NEXTTAC", []), [
3.69 + XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
3.70 + XML.Elem (("ERROR", []), [XML.Text e])])
3.71
3.72 (*. UNCHANGED: the pos' of the active formula autocalculate has been applied at
3.73 DELETED: last pos' of the succesional sequence of formulae prob. deleted
3.74 @@ -445,4 +470,8 @@
3.75 id2xml 3 pattIDs ^
3.76 "</FINDFILLPATTERNS>\n" ^
3.77 "@@@@@end@@@@@");
3.78 +fun findFillpatterns2xml (calcid : calcID) pattIDs =
3.79 + XML.Elem (("FINDFILLPATTERNS", []), [
3.80 + XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
3.81 + xml_of_strs pattIDs])
3.82