wneuper@31
|
1 |
(* the interface between the isac-kernel and the java-frontend;
|
wneuper@31
|
2 |
the isac-kernel holds calc-trees; stdout in XML-format.
|
wneuper@31
|
3 |
authors: Walther Neuper 2002
|
wneuper@31
|
4 |
(c) due to copyright terms
|
wneuper@31
|
5 |
|
wneuper@31
|
6 |
use"FE-interface/interface.sml";
|
wneuper@31
|
7 |
use"interface.sml";
|
wneuper@31
|
8 |
*)
|
wneuper@31
|
9 |
|
wneuper@31
|
10 |
signature INTERFACE =
|
wneuper@31
|
11 |
sig
|
wneuper@31
|
12 |
val CalcTree : fmz list -> unit
|
wneuper@31
|
13 |
val DEconstrCalcTree : calcID -> unit
|
wneuper@31
|
14 |
val Iterator : calcID -> unit
|
wneuper@31
|
15 |
val IteratorTEST : calcID -> iterID
|
wneuper@31
|
16 |
val appendFormula : calcID -> cterm' -> unit
|
wneuper@31
|
17 |
val autoCalculate : calcID -> auto -> unit
|
wneuper@31
|
18 |
val checkContext : calcID -> pos' -> guh -> unit
|
wneuper@31
|
19 |
val fetchApplicableTactics : calcID -> int -> pos' -> unit
|
wneuper@31
|
20 |
val fetchProposedTactic : calcID -> unit
|
wneuper@31
|
21 |
val getAccumulatedAsms : calcID -> pos' -> unit
|
wneuper@31
|
22 |
val getActiveFormula : calcID -> unit
|
wneuper@31
|
23 |
val getAssumptions : calcID -> pos' -> unit
|
wneuper@31
|
24 |
val initContext : calcID -> ketype -> pos' -> unit
|
wneuper@31
|
25 |
val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> unit
|
wneuper@31
|
26 |
val getTactic : calcID -> pos' -> unit
|
wneuper@31
|
27 |
val interSteps : calcID -> pos' -> unit
|
wneuper@31
|
28 |
val modifyCalcHead : calcID -> icalhd -> unit
|
wneuper@31
|
29 |
val moveActiveCalcHead : calcID -> unit
|
wneuper@31
|
30 |
val moveActiveDown : calcID -> unit
|
wneuper@31
|
31 |
val moveActiveDownTEST : calcID -> unit
|
wneuper@31
|
32 |
val moveActiveFormula : calcID -> pos' -> unit
|
wneuper@31
|
33 |
val moveActiveLevelDown : calcID -> unit
|
wneuper@31
|
34 |
val moveActiveLevelUp : calcID -> unit
|
wneuper@31
|
35 |
val moveActiveRoot : calcID -> unit
|
wneuper@31
|
36 |
val moveActiveRootTEST : calcID -> unit
|
wneuper@31
|
37 |
val moveActiveUp : calcID -> unit
|
wneuper@31
|
38 |
val moveCalcHead : calcID -> pos' -> unit
|
wneuper@31
|
39 |
val moveDown : calcID -> pos' -> unit
|
wneuper@31
|
40 |
val moveLevelDown : calcID -> pos' -> unit
|
wneuper@31
|
41 |
val moveLevelUp : calcID -> pos' -> unit
|
wneuper@31
|
42 |
val moveRoot : calcID -> unit
|
wneuper@31
|
43 |
val moveUp : calcID -> pos' -> unit
|
wneuper@31
|
44 |
val refFormula : calcID -> pos' -> unit
|
wneuper@31
|
45 |
val replaceFormula : calcID -> cterm' -> unit
|
wneuper@31
|
46 |
val resetCalcHead : calcID -> unit
|
wneuper@31
|
47 |
val modelProblem : calcID -> unit
|
wneuper@31
|
48 |
val refineProblem : calcID -> pos' -> guh -> unit
|
wneuper@31
|
49 |
val setContext : calcID -> pos' -> guh -> unit
|
wneuper@31
|
50 |
val setMethod : calcID -> metID -> unit
|
wneuper@31
|
51 |
val setNextTactic : calcID -> tac -> unit
|
wneuper@31
|
52 |
val setProblem : calcID -> pblID -> unit
|
wneuper@31
|
53 |
val setTheory : calcID -> thyID -> unit
|
wneuper@31
|
54 |
end
|
wneuper@31
|
55 |
|
wneuper@31
|
56 |
|
wneuper@31
|
57 |
(*------------------------------------------------------------------*)
|
wneuper@31
|
58 |
structure interface : INTERFACE =
|
wneuper@31
|
59 |
struct
|
wneuper@31
|
60 |
(*------------------------------------------------------------------*)
|
wneuper@31
|
61 |
|
wneuper@207
|
62 |
(*.encode "Isabelle"-strings as seen by the user to the
|
wneuper@207
|
63 |
format accepted by Isabelle.
|
wneuper@207
|
64 |
encode "^" ---> "^^^"; see IsacKnowledge/Atools.thy;
|
wneuper@31
|
65 |
called for each cterm', icalhd, fmz in this interface;
|
wneuper@31
|
66 |
+ see "fun decode" in xmlsrc/mathml.sml.*)
|
wneuper@31
|
67 |
fun encode (str:cterm') =
|
wneuper@31
|
68 |
let fun enc [] = []
|
wneuper@31
|
69 |
| enc ("^"::cs) = "^"::"^"::"^"::(enc cs)
|
wneuper@31
|
70 |
| enc (c::cs) = c::(enc cs)
|
wneuper@31
|
71 |
in (implode o enc o explode) str:cterm' end;
|
wneuper@31
|
72 |
fun encode_imodel (imodel:imodel) =
|
wneuper@31
|
73 |
let fun enc (Given ifos) = Given (map encode ifos)
|
wneuper@31
|
74 |
| enc (Find ifos) = Find (map encode ifos)
|
wneuper@31
|
75 |
| enc (Relate ifos) = Relate (map encode ifos)
|
wneuper@31
|
76 |
in map enc imodel:imodel end;
|
wneuper@31
|
77 |
fun encode_icalhd ((pos', headl, imodel, pos_, spec):icalhd) =
|
wneuper@31
|
78 |
(pos', encode headl, encode_imodel imodel, pos_, spec):icalhd;
|
wneuper@31
|
79 |
fun encode_fmz ((ifos, spec):fmz) = (map encode ifos, spec):fmz;
|
wneuper@31
|
80 |
|
wneuper@31
|
81 |
|
wneuper@31
|
82 |
(***. CalcTree .***)
|
wneuper@31
|
83 |
|
wneuper@31
|
84 |
(** add and delete users **)
|
wneuper@31
|
85 |
|
wneuper@31
|
86 |
(*.'Iterator 1' must exist with each CalcTree;
|
wneuper@31
|
87 |
the only for updating the calc-tree
|
wneuper@31
|
88 |
WN.0411: only 'Iterator 1' is stored,
|
wneuper@31
|
89 |
all others are just calculated on the fly
|
wneuper@31
|
90 |
TODO: adapt Iterator, add_user(= add_iterator!),etc. accordingly .*)
|
wneuper@31
|
91 |
fun Iterator (cI:calcID) = (*returned ID unnecessary after WN.0411*)
|
wneuper@31
|
92 |
(adduserOK2xml cI (add_user (cI:calcID)))
|
wneuper@31
|
93 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
94 |
fun IteratorTEST (cI:calcID) = add_user (cI:calcID);
|
wneuper@31
|
95 |
(*fun DEconstructIterator (cI:calcID) (uI:iterID) =
|
wneuper@31
|
96 |
deluserOK2xml (del_user cI uI);*)
|
wneuper@31
|
97 |
|
wneuper@31
|
98 |
(*.create a calc-tree; for calls from java: thus ^^^ decoded to ^;
|
wneuper@31
|
99 |
compare "fun CalcTreeTEST" which does NOT decode.*)
|
wneuper@31
|
100 |
fun CalcTree
|
wneuper@31
|
101 |
[(fmz, sp):fmz] (*for several variants lateron*) =
|
wneuper@31
|
102 |
(* val[(fmz,sp):fmz]=[(["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
|
wneuper@31
|
103 |
"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
|
wneuper@31
|
104 |
"relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
|
wneuper@31
|
105 |
"relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
|
wneuper@31
|
106 |
"boundVariable a","boundVariable b","boundVariable alpha",
|
wneuper@31
|
107 |
"interval {x::real. 0 <= x & x <= 2*r}",
|
wneuper@31
|
108 |
"interval {x::real. 0 <= x & x <= 2*r}",
|
wneuper@31
|
109 |
"interval {x::real. 0 <= x & x <= pi}",
|
wneuper@31
|
110 |
"errorBound (eps=(0::real))"],
|
wneuper@31
|
111 |
("DiffApp.thy", ["maximum_of","function"],
|
wneuper@31
|
112 |
["DiffApp","max_by_calculus"]))];
|
wneuper@31
|
113 |
|
wneuper@31
|
114 |
*)
|
wneuper@31
|
115 |
(let val cs = nxt_specify_init_calc (encode_fmz (fmz, sp))
|
wneuper@31
|
116 |
(*FIXME.WN.8.03: error-handling missing*)
|
wneuper@31
|
117 |
val cI = add_calc cs
|
wneuper@31
|
118 |
in calctreeOK2xml cI end)
|
wneuper@31
|
119 |
handle _ => sysERROR2xml 0 "error in kernel";
|
wneuper@31
|
120 |
|
wneuper@31
|
121 |
fun DEconstrCalcTree (cI:calcID) =
|
wneuper@31
|
122 |
deconstructcalctreeOK2xml (del_calc cI);
|
wneuper@31
|
123 |
|
wneuper@31
|
124 |
|
wneuper@31
|
125 |
fun getActiveFormula (cI:calcID) = iteratorOK2xml cI (get_pos cI 1);
|
wneuper@31
|
126 |
|
wneuper@31
|
127 |
fun moveActiveFormula (cI:calcID) (p:pos') =
|
wneuper@31
|
128 |
let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
129 |
in if existpt' p pt then (upd_ipos cI 1 p; iteratorOK2xml cI p)
|
wneuper@31
|
130 |
else sysERROR2xml cI "frontend sends a non-existing pos" end;
|
wneuper@31
|
131 |
|
wneuper@31
|
132 |
(* val (cI, tac) = (1, Add_Given "equality (x ^^^ 2 + 4 * x + 3 = 0)");
|
wneuper@31
|
133 |
val (cI, tac) = (1, Specify_Theory "PolyEq.thy");
|
wneuper@31
|
134 |
val (cI, tac) = (1, Specify_Problem ["normalize","polynomial",
|
wneuper@31
|
135 |
"univariate","equation"]);
|
wneuper@31
|
136 |
val (cI, tac) = (1, Subproblem ("Poly.thy",
|
wneuper@31
|
137 |
["polynomial","univariate","equation"]));
|
wneuper@31
|
138 |
val (cI, tac) = (1, Model_Problem["linear","univariate","equation","test"]);
|
wneuper@31
|
139 |
val (cI, tac) = (1, Detail_Set "Test_simplify");
|
wneuper@31
|
140 |
val (cI, tac) = (1, Apply_Method ["Test", "solve_linear"]);
|
wneuper@31
|
141 |
val (cI, tac) = (1, Rewrite_Set "Test_simplify");
|
wneuper@31
|
142 |
*)
|
wneuper@31
|
143 |
fun setNextTactic (cI:calcID) tac =
|
wneuper@31
|
144 |
let val ((pt, _), _) = get_calc cI
|
wneuper@31
|
145 |
val ip = get_pos cI 1
|
wneuper@31
|
146 |
in case locatetac tac (pt, ip) of
|
wneuper@31
|
147 |
(* val ("ok", (tacis, c, (_,p'))) = locatetac tac (pt, ip);
|
wneuper@31
|
148 |
*)
|
wneuper@31
|
149 |
("ok", (tacis, _, _)) =>
|
wneuper@31
|
150 |
(upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")
|
wneuper@31
|
151 |
| ("unsafe-ok", (tacis, _, _)) =>
|
wneuper@31
|
152 |
(upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "unsafe-ok")
|
wneuper@31
|
153 |
| ("not-applicable",_) => setnexttactic2xml cI "not-applicable"
|
wneuper@31
|
154 |
| ("end-of-calculation",_) =>
|
wneuper@31
|
155 |
setnexttactic2xml cI "end-of-calculation"
|
wneuper@31
|
156 |
| ("failure",_) => sysERROR2xml cI "failure"
|
wneuper@31
|
157 |
end;
|
wneuper@31
|
158 |
|
wneuper@31
|
159 |
(* val cI = 1;
|
wneuper@31
|
160 |
*)
|
wneuper@31
|
161 |
fun fetchProposedTactic (cI:calcID) =
|
wneuper@31
|
162 |
(case step (get_pos cI 1) (get_calc cI) of
|
wneuper@31
|
163 |
("ok", (tacis, _, _)) =>
|
wneuper@31
|
164 |
let val _= upd_tacis cI tacis
|
wneuper@31
|
165 |
val (tac,_,_) = last_elem tacis
|
wneuper@31
|
166 |
in fetchproposedtacticOK2xml cI tac end
|
wneuper@31
|
167 |
| ("helpless",_) => fetchproposedtacticERROR2xml cI "helpless"
|
wneuper@31
|
168 |
| ("no-fmz-spec",_) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
|
wneuper@31
|
169 |
| ("end-of-calculation",_) =>
|
wneuper@31
|
170 |
fetchproposedtacticERROR2xml cI "end-of-calculation")
|
wneuper@31
|
171 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
172 |
|
wneuper@31
|
173 |
(*datatype auto = FIXXXME040624: does NOT match interfaces/ITOCalc.java
|
wneuper@31
|
174 |
Step of int (*1 do #int steps (may stop in model/specify)
|
wneuper@31
|
175 |
IS VERY INEFFICIENT IN MODEL/SPECIY*)
|
wneuper@31
|
176 |
| CompleteModel (*2 complete modeling
|
wneuper@31
|
177 |
if model complete, finish specifying*)
|
wneuper@31
|
178 |
| CompleteCalcHead (*3 complete model/specify in one go*)
|
wneuper@31
|
179 |
| CompleteToSubpbl (*4 stop at the next begin of a subproblem,
|
wneuper@31
|
180 |
if none, complete the actual (sub)problem*)
|
wneuper@31
|
181 |
| CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems)*)
|
wneuper@31
|
182 |
| CompleteCalc; (*6 complete the calculation as a whole*)*)
|
wneuper@31
|
183 |
fun autoCalculate (cI:calcID) auto =
|
wneuper@31
|
184 |
(* val (cI, auto) = (1,CompleteCalc);
|
wneuper@31
|
185 |
val (cI, auto) = (1,CompleteModel);
|
wneuper@31
|
186 |
val (cI, auto) = (1,CompleteCalcHead);
|
wneuper@31
|
187 |
val (cI, auto) = (1,Step 1);
|
wneuper@31
|
188 |
*)
|
wneuper@31
|
189 |
(let val pold = get_pos cI 1
|
wneuper@31
|
190 |
val x = autocalc [] pold (get_calc cI) auto
|
wneuper@31
|
191 |
in
|
wneuper@31
|
192 |
case x of
|
wneuper@31
|
193 |
(* val (str, c, ptp as (_,p)) = x;
|
wneuper@31
|
194 |
*)
|
wneuper@31
|
195 |
("ok", c, ptp as (_,p)) =>
|
wneuper@31
|
196 |
(upd_calc cI (ptp, []); upd_ipos cI 1 p;
|
wneuper@31
|
197 |
autocalculateOK2xml cI pold (if null c then pold
|
wneuper@31
|
198 |
else last_elem c) p)
|
wneuper@31
|
199 |
| ("end-of-calculation", c, ptp as (_,p)) =>
|
wneuper@31
|
200 |
(upd_calc cI (ptp, []); upd_ipos cI 1 p;
|
wneuper@31
|
201 |
autocalculateOK2xml cI pold (if null c then pold
|
wneuper@31
|
202 |
else last_elem c) p)
|
wneuper@31
|
203 |
| (str, _, _) => autocalculateERROR2xml cI str
|
wneuper@31
|
204 |
end)
|
wneuper@31
|
205 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
206 |
|
wneuper@31
|
207 |
|
wneuper@31
|
208 |
(* val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
|
wneuper@31
|
209 |
(1, (([],Pbl), "not used here",
|
wneuper@31
|
210 |
[Given ["fixedValues [r=Arbfix]"],
|
wneuper@31
|
211 |
Find ["maximum A", "valuesFor [a,b]"(*new input*)],
|
wneuper@31
|
212 |
Relate ["relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], Pbl,
|
wneuper@31
|
213 |
("DiffApp.thy", ["maximum_of","function"],
|
wneuper@31
|
214 |
["DiffApp","max_by_calculus"])));
|
wneuper@31
|
215 |
val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
|
wneuper@31
|
216 |
(1, (([],Pbl),"solve (x+1=2, x)",
|
wneuper@31
|
217 |
[Given ["equality (x+1=2)", "solveFor x"],
|
wneuper@31
|
218 |
Find ["solutions L"]],
|
wneuper@31
|
219 |
Pbl,
|
wneuper@31
|
220 |
("Test.thy", ["linear","univariate","equation","test"],
|
wneuper@31
|
221 |
["Test","solve_linear"])));
|
wneuper@31
|
222 |
val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
|
wneuper@31
|
223 |
(1, (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], [])));
|
wneuper@31
|
224 |
val (cI, p:pos')=(1, ([1],Frm));
|
wneuper@31
|
225 |
val (cI, p:pos')=(1, ([1,2,1,3],Res));
|
wneuper@31
|
226 |
*)
|
wneuper@31
|
227 |
fun getTactic cI (p:pos') =
|
wneuper@31
|
228 |
(let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
229 |
val (form, tac, asms) = pt_extract (pt, p)
|
wneuper@31
|
230 |
in case tac of
|
wneuper@31
|
231 |
(* val Some ta = tac;
|
wneuper@31
|
232 |
*)
|
wneuper@31
|
233 |
Some ta => gettacticOK2xml cI ta
|
wneuper@31
|
234 |
| None => gettacticERROR2xml cI ("no tactic at position "^pos'2str p)
|
wneuper@31
|
235 |
end)
|
wneuper@31
|
236 |
handle _ => sysERROR2xml cI "syserror in getTactic";
|
wneuper@31
|
237 |
|
wneuper@31
|
238 |
(*. see ICalcIterator#fetchApplicableTactics
|
wneuper@31
|
239 |
@see #TACTICS_ALL
|
wneuper@31
|
240 |
@see #TACTICS_CURRENT_THEORY
|
wneuper@31
|
241 |
@see #TACTICS_CURRENT_METHOD ..the only impl.WN040307.*)
|
wneuper@268
|
242 |
(*. fetch tactics to be applied to a particular step.*)
|
wneuper@268
|
243 |
(* WN071231 kept this version for later parametrisation*)
|
wneuper@268
|
244 |
(*.version 1: fetch _all_ tactics from script .*)
|
wneuper@31
|
245 |
fun fetchApplicableTactics cI (scope:int) (p:pos') =
|
wneuper@31
|
246 |
(let val ((pt, _), _) = get_calc cI
|
wneuper@31
|
247 |
in (applicabletacticsOK cI (sel_rules pt p))
|
wneuper@31
|
248 |
handle PTREE str => sysERROR2xml cI str
|
wneuper@31
|
249 |
end)
|
wneuper@31
|
250 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@268
|
251 |
(*.version 2: fetch _applicable_ _elementary_ (ie. recursively
|
wneuper@268
|
252 |
decompose rule-sets) Rewrite*, Calculate .*)
|
wneuper@268
|
253 |
fun fetchApplicableTactics cI (scope:int) (p:pos') =
|
wneuper@268
|
254 |
(let val ((pt, _), _) = get_calc cI
|
wneuper@269
|
255 |
in (applicabletacticsOK cI (sel_appl_atomic_tacs pt p))
|
wneuper@268
|
256 |
handle PTREE str => sysERROR2xml cI str
|
wneuper@268
|
257 |
end)
|
wneuper@268
|
258 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@269
|
259 |
|
wneuper@31
|
260 |
fun getAssumptions cI (p:pos') =
|
wneuper@31
|
261 |
(let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
262 |
val (_, _, asms) = pt_extract (pt, p)
|
wneuper@31
|
263 |
in getasmsOK2xml cI asms end)
|
wneuper@31
|
264 |
handle _ => sysERROR2xml cI "syserror in getAssumptions";
|
wneuper@31
|
265 |
|
wneuper@31
|
266 |
(*WN0502 @see ME/ctree: type asms: illdesigned, thus no positions returned*)
|
wneuper@31
|
267 |
fun getAccumulatedAsms cI (p:pos') =
|
wneuper@31
|
268 |
(let val ((pt, _), _) = get_calc cI
|
wneuper@31
|
269 |
val ass = map fst (get_assumptions_ pt p)
|
wneuper@31
|
270 |
in (*getaccuasmsOK2xml cI (get_assumptions_ pt p)*)
|
wneuper@31
|
271 |
getasmsOK2xml cI ass end)
|
wneuper@31
|
272 |
handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms";
|
wneuper@31
|
273 |
|
wneuper@31
|
274 |
|
wneuper@31
|
275 |
(*since moveActive* does NOT transfer pos java --> sml (only sml --> java)
|
wneuper@31
|
276 |
refFormula might become involved in far-off errors !!!*)
|
wneuper@31
|
277 |
fun refFormula cI (p:pos') = (*WN0501 rename to 'fun getElement' !*)
|
wneuper@31
|
278 |
(* val (cI, uI) = (1,1);
|
wneuper@31
|
279 |
*)
|
wneuper@31
|
280 |
(let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
281 |
val (form, tac, asms) = pt_extract (pt, p)
|
wneuper@31
|
282 |
in refformulaOK2xml cI p form end)
|
wneuper@31
|
283 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
284 |
|
wneuper@31
|
285 |
(*.get formulae 'from' 'to' w.r.t. ordering in Position#compareTo(Position p);
|
wneuper@31
|
286 |
in case of CalcHeads only the headline is taken
|
wneuper@31
|
287 |
(the pos' allows distinction between PrfObj and PblObj anyway);
|
wneuper@31
|
288 |
'level' is adjusted such that an 'interval' of formulae is returned;
|
wneuper@31
|
289 |
'from' 'to' are designed for use by iterators of calcChangedEvent;
|
wneuper@31
|
290 |
thus 'from' is the last unchanged position.*)
|
wneuper@31
|
291 |
fun getFormulaeFromTo cI (from as ([],Pbl):pos') (to as ([],Pbl):pos')_ false =
|
wneuper@31
|
292 |
(*special case because 'from' is _before_ the first elements to be returned*)
|
wneuper@31
|
293 |
(* val (cI, from, to, level) = (1, ([],Pbl), ([],Pbl), 1);
|
wneuper@31
|
294 |
*)
|
wneuper@31
|
295 |
((let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
296 |
val (ModSpec (_,_,headline,_,_,_),_,_) = pt_extract (pt, to)
|
wneuper@31
|
297 |
in getintervalOK cI [(to, headline)] end)
|
wneuper@31
|
298 |
handle _ => sysERROR2xml cI "error in kernel")
|
wneuper@31
|
299 |
|
wneuper@31
|
300 |
| getFormulaeFromTo cI (from:pos') (to:pos') level false =
|
wneuper@31
|
301 |
(* val (cI, from, to, level) = (1, unc, gen, 0);
|
wneuper@31
|
302 |
val (cI, from, to, level) = (1, unc, gen, 1);
|
wneuper@31
|
303 |
*)
|
wneuper@31
|
304 |
(if from = to then sysERROR2xml cI "getFormulaeFromTo: From = To"
|
wneuper@31
|
305 |
else
|
wneuper@31
|
306 |
(case from of
|
wneuper@31
|
307 |
([],Res) => sysERROR2xml cI "getFormulaeFromTo does: moveDown \
|
wneuper@31
|
308 |
\from=([],Res) .. goes beyond result"
|
wneuper@31
|
309 |
| _ => let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
310 |
val f = move_dn [] pt from
|
wneuper@31
|
311 |
fun max (a,b) = if a < b then b else a
|
wneuper@31
|
312 |
(*must reach margins ...*)
|
wneuper@31
|
313 |
val lev = max (level, max (lev_of from, lev_of to))
|
wneuper@31
|
314 |
in getintervalOK cI (get_interval f to lev pt) end)
|
wneuper@31
|
315 |
handle _ => sysERROR2xml cI "error in getFormulaeFromTo")
|
wneuper@31
|
316 |
|
wneuper@31
|
317 |
| getFormulaeFromTo cI from to level true =
|
wneuper@207
|
318 |
sysERROR2xml cI "getFormulaeFromTo impl.for formulae only,\
|
wneuper@207
|
319 |
\i.e. last arg only impl. for false, _NOT_ true";
|
wneuper@31
|
320 |
|
wneuper@31
|
321 |
|
wneuper@31
|
322 |
(* val (cI, ip) = (1, ([1,9], Res));
|
wneuper@31
|
323 |
val (cI, ip) = (1, ([], Res));
|
wneuper@31
|
324 |
val (cI, ip) = (1, ([2], Res));
|
wneuper@31
|
325 |
val (cI, ip) = (1, ([3,1], Res));
|
wneuper@31
|
326 |
val (cI, ip) = (1, ([1,2,1], Res));
|
wneuper@31
|
327 |
*)
|
wneuper@31
|
328 |
fun interSteps cI ip =
|
wneuper@31
|
329 |
(let val ((pt,p), tacis) = get_calc cI
|
wneuper@31
|
330 |
in if (not o is_interpos) ip
|
wneuper@31
|
331 |
then interStepsERROR cI "only formulae with position (_,Res) \
|
wneuper@31
|
332 |
\may have intermediate steps above them"
|
wneuper@31
|
333 |
else let val ip' = lev_pred' pt ip
|
wneuper@31
|
334 |
(* val (str, pt', lastpos) = detailstep pt ip;
|
wneuper@31
|
335 |
*)
|
wneuper@31
|
336 |
in case detailstep pt ip of
|
wneuper@31
|
337 |
("detailrls", pt(*, pos'forms*), lastpos) =>
|
wneuper@31
|
338 |
(upd_calc cI ((pt, p), tacis);
|
wneuper@31
|
339 |
interStepsOK cI (*pos'forms*) ip' ip' lastpos)
|
wneuper@31
|
340 |
| ("no-Rewrite_Set...", _, _) =>
|
wneuper@31
|
341 |
sysERROR2xml cI "no Rewrite_Set..."
|
wneuper@31
|
342 |
| (_, _(*, pos'formshds*), lastpos) =>
|
wneuper@31
|
343 |
interStepsOK cI (*pos'formshds*) ip' ip' lastpos
|
wneuper@31
|
344 |
end
|
wneuper@31
|
345 |
end)
|
wneuper@31
|
346 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
347 |
|
wneuper@31
|
348 |
fun modifyCalcHead (cI:calcID) (ichd as ((p,_),_,_,_,_):icalhd) =
|
wneuper@31
|
349 |
(let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
350 |
val (pt, chd as (_,p_,_,_,_,_)) = input_icalhd pt ichd
|
wneuper@31
|
351 |
in (upd_calc cI ((pt, (p,p_)), []);
|
wneuper@31
|
352 |
modifycalcheadOK2xml cI chd) end)
|
wneuper@31
|
353 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
354 |
|
wneuper@31
|
355 |
(*.at the activeFormula set the Model, the Guard and the Specification
|
wneuper@31
|
356 |
to empty and return a CalcHead;
|
wneuper@31
|
357 |
the 'origin' remains (for reconstructing all that).*)
|
wneuper@31
|
358 |
fun resetCalcHead (cI:calcID) =
|
wneuper@31
|
359 |
(let val (ptp,_) = get_calc cI
|
wneuper@31
|
360 |
val ptp = reset_calchead ptp
|
wneuper@31
|
361 |
in (upd_calc cI (ptp, []);
|
wneuper@31
|
362 |
modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
|
wneuper@31
|
363 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
364 |
|
wneuper@31
|
365 |
(*.at the activeFormula insert all the Descriptions in the Model
|
wneuper@31
|
366 |
(_not_ in the Guard) and return a CalcHead;
|
wneuper@31
|
367 |
the Descriptions are for user-guidance; the rest of the items
|
wneuper@31
|
368 |
are left empty for user-input;
|
wneuper@31
|
369 |
includes a resetCalcHead for the Model and the Guard.*)
|
wneuper@31
|
370 |
fun modelProblem (cI:calcID) =
|
wneuper@31
|
371 |
(let val (ptp, _) = get_calc cI
|
wneuper@31
|
372 |
val ptp = reset_calchead ptp
|
wneuper@31
|
373 |
val (_, _, ptp) = nxt_specif Model_Problem ptp
|
wneuper@31
|
374 |
in (upd_calc cI (ptp, []);
|
wneuper@31
|
375 |
modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
|
wneuper@31
|
376 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
377 |
|
wneuper@31
|
378 |
|
wneuper@31
|
379 |
(*.set the context determined on a knowledgebrowser to the current calc.*)
|
wneuper@31
|
380 |
fun setContext (cI:calcID) (ip as (_,p_):pos') (guh:guh) =
|
wneuper@31
|
381 |
(case (implode o (take_fromto 1 4) o explode) guh of
|
wneuper@31
|
382 |
"thy_" =>
|
wneuper@31
|
383 |
(* val (cI, ip as (_,p_), guh) = (1, p, "thy_isac_Test-rls-Test_simplify");
|
wneuper@31
|
384 |
*)
|
wneuper@31
|
385 |
if p_ mem [Pbl,Met] then message2xml cI "thy-context not to calchead"
|
wneuper@31
|
386 |
else if ip = ([],Res) then message2xml cI "no thy-context at result"
|
wneuper@31
|
387 |
else if no_thycontext guh then message2xml cI ("no thy-context for '"^
|
wneuper@31
|
388 |
guh ^ "'")
|
wneuper@31
|
389 |
else let val (ptp as (pt,pold),_) = get_calc cI
|
wneuper@31
|
390 |
val is = get_istate pt ip
|
wneuper@31
|
391 |
val subs = subs_from is "dummy" guh
|
wneuper@31
|
392 |
val tac = guh2rewtac guh subs
|
wneuper@31
|
393 |
in case locatetac tac (pt, ip) of (*='fun setNextTactic'+step*)
|
wneuper@31
|
394 |
("ok", (tacis, c, ptp as (_,p))) =>
|
wneuper@31
|
395 |
(* val (str, (tacis, c, ptp as (_,p))) = locatetac tac (pt, ip);
|
wneuper@31
|
396 |
*)
|
wneuper@31
|
397 |
(upd_calc cI ((pt,p), []);
|
wneuper@31
|
398 |
autocalculateOK2xml cI pold (if null c then pold
|
wneuper@31
|
399 |
else last_elem c) p)
|
wneuper@31
|
400 |
| ("unsafe-ok", (tacis, c, ptp as (_,p))) =>
|
wneuper@31
|
401 |
(upd_calc cI ((pt,p), []);
|
wneuper@31
|
402 |
autocalculateOK2xml cI pold (if null c then pold
|
wneuper@31
|
403 |
else last_elem c) p)
|
wneuper@31
|
404 |
| ("end-of-calculation",_) =>
|
wneuper@31
|
405 |
message2xml cI "end-of-calculation"
|
wneuper@31
|
406 |
| ("failure",_) => sysERROR2xml cI "failure"
|
wneuper@31
|
407 |
| ("not-applicable",_) => (*the rule comes from anywhere..*)
|
wneuper@31
|
408 |
(case applicable_in ip pt tac of
|
wneuper@31
|
409 |
|
wneuper@31
|
410 |
Notappl e => message2xml cI ("'" ^ tac2str tac ^
|
wneuper@31
|
411 |
"' not-applicable")
|
wneuper@31
|
412 |
| Appl m =>
|
wneuper@31
|
413 |
let val (p,c,_,pt) = generate1 (assoc_thy"Isac.thy")
|
wneuper@31
|
414 |
m Uistate ip pt
|
wneuper@31
|
415 |
in upd_calc cI ((pt,p),[]);
|
wneuper@31
|
416 |
autocalculateOK2xml cI pold (if null c then pold
|
wneuper@31
|
417 |
else last_elem c) p
|
wneuper@31
|
418 |
end)
|
wneuper@31
|
419 |
end
|
wneuper@31
|
420 |
(* val (cI, ip as (_,p_), guh) = (1, pos, guh);
|
wneuper@31
|
421 |
*)
|
wneuper@31
|
422 |
| "pbl_" =>
|
wneuper@31
|
423 |
let val pI = guh2kestoreID guh
|
wneuper@31
|
424 |
val ((pt, _), _) = get_calc cI
|
wneuper@31
|
425 |
(*val ip as (_, p_) = get_pos cI 1*)
|
wneuper@31
|
426 |
in if p_ mem [Pbl, Met]
|
wneuper@31
|
427 |
then let val (pt, chd) = set_problem pI (pt, ip)
|
wneuper@31
|
428 |
in (upd_calc cI ((pt, ip), []);
|
wneuper@31
|
429 |
modifycalcheadOK2xml cI chd) end
|
wneuper@31
|
430 |
else sysERROR2xml cI "setContext for pbl requires ActiveFormula \
|
wneuper@31
|
431 |
\on CalcHead"
|
wneuper@31
|
432 |
end
|
wneuper@31
|
433 |
(* val (cI, ip as (_,p_), guh) = (1, pos, "met_eq_lin");
|
wneuper@31
|
434 |
*)
|
wneuper@31
|
435 |
| "met_" =>
|
wneuper@31
|
436 |
let val mI = guh2kestoreID guh
|
wneuper@31
|
437 |
val ((pt, _), _) = get_calc cI
|
wneuper@31
|
438 |
in if p_ mem [Pbl, Met]
|
wneuper@31
|
439 |
then let val (pt, chd) = set_method mI (pt, ip)
|
wneuper@31
|
440 |
in (upd_calc cI ((pt, ip), []);
|
wneuper@31
|
441 |
modifycalcheadOK2xml cI chd) end
|
wneuper@31
|
442 |
else sysERROR2xml cI "setContext for met requires ActiveFormula \
|
wneuper@31
|
443 |
\on CalcHead"
|
wneuper@31
|
444 |
end)
|
wneuper@31
|
445 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
446 |
|
wneuper@31
|
447 |
|
wneuper@31
|
448 |
(*.specify the Method at the activeFormula and return a CalcHead
|
wneuper@31
|
449 |
containing the Guard.
|
wneuper@31
|
450 |
WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*)
|
wneuper@31
|
451 |
fun setMethod (cI:calcID) (mI:metID) =
|
wneuper@31
|
452 |
(* val (cI, mI) = (1, ["Test","solve_linear"]);
|
wneuper@31
|
453 |
*)
|
wneuper@31
|
454 |
(let val ((pt, _), _) = get_calc cI
|
wneuper@31
|
455 |
val ip as (_, p_) = get_pos cI 1
|
wneuper@31
|
456 |
in if p_ mem [Pbl, Met]
|
wneuper@31
|
457 |
then let val (pt, chd) = set_method mI (pt, ip)
|
wneuper@31
|
458 |
in (upd_calc cI ((pt, ip), []);
|
wneuper@31
|
459 |
modifycalcheadOK2xml cI chd) end
|
wneuper@31
|
460 |
else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead"
|
wneuper@31
|
461 |
end)
|
wneuper@31
|
462 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
463 |
|
wneuper@31
|
464 |
(*.specify the Problem at the activeFormula and return a CalcHead
|
wneuper@31
|
465 |
containing the Model; special case of checkContext;
|
wneuper@31
|
466 |
WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem '.*)
|
wneuper@31
|
467 |
fun setProblem (cI:calcID) (pI:pblID) =
|
wneuper@31
|
468 |
(let val ((pt, _), _) = get_calc cI
|
wneuper@31
|
469 |
val ip as (_, p_) = get_pos cI 1
|
wneuper@31
|
470 |
in if p_ mem [Pbl, Met]
|
wneuper@31
|
471 |
then let val (pt, chd) = set_problem pI (pt, ip)
|
wneuper@31
|
472 |
in (upd_calc cI ((pt, ip), []);
|
wneuper@31
|
473 |
modifycalcheadOK2xml cI chd) end
|
wneuper@31
|
474 |
else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
|
wneuper@31
|
475 |
end)
|
wneuper@31
|
476 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
477 |
|
wneuper@31
|
478 |
(*.specify the Theory at the activeFormula and return a CalcHead;
|
wneuper@31
|
479 |
special case of checkContext;
|
wneuper@31
|
480 |
WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*)
|
wneuper@31
|
481 |
fun setTheory (cI:calcID) (tI:thyID) =
|
wneuper@31
|
482 |
(let val ((pt, _), _) = get_calc cI
|
wneuper@31
|
483 |
val ip as (_, p_) = get_pos cI 1
|
wneuper@31
|
484 |
in if p_ mem [Pbl, Met]
|
wneuper@31
|
485 |
then let val (pt, chd) = set_theory tI (pt, ip)
|
wneuper@31
|
486 |
in (upd_calc cI ((pt, ip), []);
|
wneuper@31
|
487 |
modifycalcheadOK2xml cI chd) end
|
wneuper@31
|
488 |
else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
|
wneuper@31
|
489 |
end)
|
wneuper@31
|
490 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
491 |
|
wneuper@31
|
492 |
|
wneuper@31
|
493 |
(**. without update of CalcTree .**)
|
wneuper@31
|
494 |
|
wneuper@31
|
495 |
(*.match the model of a problem at pos p
|
wneuper@31
|
496 |
with the model-pattern of the problem with pblID*)
|
wneuper@31
|
497 |
(*fun tryMatchProblem cI pblID =
|
wneuper@31
|
498 |
(let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
499 |
val p = get_pos cI 1
|
wneuper@31
|
500 |
val chd = trymatch pblID pt p
|
wneuper@31
|
501 |
in trymatchOK2xml cI chd end)
|
wneuper@31
|
502 |
handle _ => sysERROR2xml cI "error in kernel";*)
|
wneuper@31
|
503 |
|
wneuper@31
|
504 |
(*.refinement for the parent-problem of the position.*)
|
wneuper@31
|
505 |
(* val (cI, (p,p_), guh) = (1, ([1],Res), "pbl_equ_univ");
|
wneuper@31
|
506 |
*)
|
wneuper@31
|
507 |
fun refineProblem cI ((p,p_) : pos') (guh : guh) =
|
wneuper@31
|
508 |
(let val pblID = guh2kestoreID guh
|
wneuper@31
|
509 |
val ((pt,_),_) = get_calc cI
|
wneuper@31
|
510 |
val pp = par_pblobj pt p
|
wneuper@31
|
511 |
val chd = tryrefine pblID pt (pp, p_)
|
wneuper@31
|
512 |
in matchpbl2xml cI chd end)
|
wneuper@31
|
513 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
514 |
|
wneuper@31
|
515 |
(* val (cI, ifo) = (1, "-2 * 1 + (1 + x) = 0");
|
wneuper@31
|
516 |
val (cI, ifo) = (1, "x = 2");
|
wneuper@31
|
517 |
val (cI, ifo) = (1, "[x = 3 + -2*1]");
|
wneuper@31
|
518 |
val (cI, ifo) = (1, "-1 + x = 0");
|
wneuper@31
|
519 |
val (cI, ifo) = (1, "x - 4711 = 0");
|
wneuper@31
|
520 |
val (cI, ifo) = (1, "2+ -1 + x = 2");
|
wneuper@31
|
521 |
val (cI, ifo) = (1, " x - ");
|
wneuper@31
|
522 |
val (cI, ifo) = (1, "(-3 * x + 4 * y + -1 * x * y) / (x * y)");
|
wneuper@31
|
523 |
val (cI, ifo) = (1, "(4 * y + -3 * x) / (x * y) + -1");
|
wneuper@31
|
524 |
*)
|
wneuper@31
|
525 |
fun appendFormula cI (ifo:cterm') =
|
wneuper@31
|
526 |
(let val cs = get_calc cI
|
wneuper@31
|
527 |
val pos as (_,p_) = get_pos cI 1
|
wneuper@31
|
528 |
in case step pos cs of
|
wneuper@31
|
529 |
(* val (str, cs') = step pos cs;
|
wneuper@31
|
530 |
*)
|
wneuper@31
|
531 |
("ok", cs') =>
|
wneuper@31
|
532 |
(case inform cs' (encode ifo) of
|
wneuper@31
|
533 |
(* val (str, (_, c, ptp as (_,p))) = inform cs' (encode ifo);
|
wneuper@31
|
534 |
*)
|
wneuper@31
|
535 |
("ok", (_(*use in DG !!!*), c, ptp as (_,p))) =>
|
wneuper@31
|
536 |
(upd_calc cI (ptp, []); upd_ipos cI 1 p;
|
wneuper@31
|
537 |
appendformulaOK2xml cI pos (if null c then pos
|
wneuper@31
|
538 |
else last_elem c) p)
|
wneuper@31
|
539 |
| ("same-formula", (_, c, ptp as (_,p))) =>
|
wneuper@31
|
540 |
(upd_calc cI (ptp, []); upd_ipos cI 1 p;
|
wneuper@31
|
541 |
appendformulaOK2xml cI pos (if null c then pos
|
wneuper@31
|
542 |
else last_elem c) p)
|
wneuper@31
|
543 |
| (msg, _) => appendformulaERROR2xml cI msg)
|
wneuper@31
|
544 |
| (msg, cs') => appendformulaERROR2xml cI msg
|
wneuper@31
|
545 |
end)
|
wneuper@31
|
546 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
547 |
|
wneuper@31
|
548 |
|
wneuper@31
|
549 |
|
wneuper@31
|
550 |
(*.replace a formula with_in_ a calculation;
|
wneuper@31
|
551 |
this situation applies for initial CAS-commands, too.*)
|
wneuper@31
|
552 |
(* val (cI, ifo) = (2, "-1 + x = 0");
|
wneuper@31
|
553 |
val (cI, ifo) = (1, "-1 + x = 0");
|
wneuper@31
|
554 |
val (cI, ifo) = (1, "x - 1 = 0");
|
wneuper@31
|
555 |
val (cI, ifo) = (1, "x = 1");
|
wneuper@31
|
556 |
val (cI, ifo) = (1, "solve(x+1=2,x)");
|
wneuper@31
|
557 |
val (cI, ifo) = (1, "Simplify (2*a + 3*a)");
|
wneuper@31
|
558 |
val (cI, ifo) = (1, "Diff (x^2 + x + 1, x)");
|
wneuper@31
|
559 |
*)
|
wneuper@31
|
560 |
fun replaceFormula cI (ifo:cterm') =
|
wneuper@31
|
561 |
(let val ((pt, _), _) = get_calc cI
|
wneuper@31
|
562 |
val p = get_pos cI 1
|
wneuper@31
|
563 |
in case inform (([], [], (pt, p)): calcstate') (encode ifo) of
|
wneuper@31
|
564 |
("ok", (_(*tacs used for DG ?*), c, ptp' as (pt',p'))) =>
|
wneuper@31
|
565 |
(* val (str, (_,c, ptp' as (pt',p')))= inform ([], [], (pt, p)) (encode ifo);
|
wneuper@31
|
566 |
*)
|
wneuper@31
|
567 |
let val unc = if null (fst p) then p else move_up [] pt p
|
wneuper@31
|
568 |
val _ = upd_calc cI (ptp', [])
|
wneuper@31
|
569 |
val _ = upd_ipos cI 1 p'
|
wneuper@31
|
570 |
in replaceformulaOK2xml cI unc
|
wneuper@31
|
571 |
(if null c then unc
|
wneuper@31
|
572 |
else last_elem c) p'(*' NEW*) end
|
wneuper@31
|
573 |
| ("same-formula", _) =>
|
wneuper@31
|
574 |
(*TODO.WN0501 MESSAGE !*)
|
wneuper@31
|
575 |
replaceformulaERROR2xml cI "formula not changed"
|
wneuper@31
|
576 |
| (msg, _) => replaceformulaERROR2xml cI msg
|
wneuper@31
|
577 |
end)
|
wneuper@31
|
578 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
579 |
|
wneuper@31
|
580 |
|
wneuper@31
|
581 |
|
wneuper@31
|
582 |
(***. CalcIterator
|
wneuper@31
|
583 |
moveActive*: set the pos' of the active formula stored with the calctree
|
wneuper@31
|
584 |
could take pos' as argument for consistency checks
|
wneuper@31
|
585 |
move*: compute the new iterator from the old one on the fly
|
wneuper@31
|
586 |
|
wneuper@31
|
587 |
.***)
|
wneuper@31
|
588 |
|
wneuper@31
|
589 |
fun moveActiveRoot cI =
|
wneuper@31
|
590 |
(let val _ = upd_ipos cI 1 ([],Pbl)
|
wneuper@31
|
591 |
in iteratorOK2xml cI ([],Pbl) end)
|
wneuper@31
|
592 |
handle e => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
593 |
fun moveRoot cI =
|
wneuper@31
|
594 |
(iteratorOK2xml cI ([],Pbl))
|
wneuper@31
|
595 |
handle e => sysERROR2xml cI "";
|
wneuper@31
|
596 |
fun moveActiveRootTEST cI =
|
wneuper@31
|
597 |
(let val _ = upd_ipos cI 1 ([],Pbl)
|
wneuper@31
|
598 |
in (*iteratorOK2xml cI ([],Pbl)*)() end)
|
wneuper@31
|
599 |
handle e => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
600 |
|
wneuper@31
|
601 |
(* val (cI, uI) = (1,1);
|
wneuper@31
|
602 |
val (cI, uI) = (1,2);
|
wneuper@31
|
603 |
*)
|
wneuper@31
|
604 |
fun moveActiveDown cI =
|
wneuper@31
|
605 |
((let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
606 |
(* val (P, (Nd (_, ns)), (p::(ps as (_::_)), p_)) =([]:pos, pt, get_pos cI uI);
|
wneuper@31
|
607 |
val (P, (Nd (c, ns)), ([p], p_)) =([]:pos, pt, get_pos cI uI);
|
wneuper@31
|
608 |
|
wneuper@31
|
609 |
print_depth 7;pt
|
wneuper@31
|
610 |
*)
|
wneuper@31
|
611 |
val ip' = move_dn [] pt (get_pos cI 1)
|
wneuper@31
|
612 |
val _ = upd_ipos cI 1 ip'
|
wneuper@31
|
613 |
in iteratorOK2xml cI ip' end)
|
wneuper@31
|
614 |
handle (PTREE e) => iteratorERROR2xml cI)
|
wneuper@31
|
615 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
616 |
fun moveDown cI (p:pos') =
|
wneuper@31
|
617 |
((let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
618 |
(* val (P, (Nd (_, ns)), (p::(ps as (_::_)), p_)) =([]:pos, pt, get_pos cI uI);
|
wneuper@31
|
619 |
val (P, (Nd (c, ns)), ([p], p_)) =([]:pos, pt, get_pos cI uI);
|
wneuper@31
|
620 |
|
wneuper@31
|
621 |
print_depth 7;pt
|
wneuper@31
|
622 |
*)
|
wneuper@31
|
623 |
val ip' = move_dn [] pt p
|
wneuper@31
|
624 |
in iteratorOK2xml cI ip' end)
|
wneuper@31
|
625 |
handle (PTREE e) => iteratorERROR2xml cI)
|
wneuper@31
|
626 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
627 |
fun moveActiveDownTEST cI =
|
wneuper@31
|
628 |
let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
629 |
val ip = get_pos cI 1
|
wneuper@31
|
630 |
val ip' = (move_dn [] pt ip)
|
wneuper@31
|
631 |
handle _ => ip
|
wneuper@31
|
632 |
val _ = upd_ipos cI 1 ip'
|
wneuper@31
|
633 |
in (*iteratorOK2xml cI uI*)() end;
|
wneuper@31
|
634 |
|
wneuper@31
|
635 |
fun moveActiveLevelDown cI =
|
wneuper@31
|
636 |
((let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
637 |
val ip' = movelevel_dn [] pt (get_pos cI 1)
|
wneuper@31
|
638 |
val _ = upd_ipos cI 1 ip'
|
wneuper@31
|
639 |
in iteratorOK2xml cI ip' end)
|
wneuper@31
|
640 |
handle (PTREE e) => iteratorERROR2xml cI)
|
wneuper@31
|
641 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
642 |
fun moveLevelDown cI (p:pos') =
|
wneuper@31
|
643 |
((let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
644 |
val ip' = movelevel_dn [] pt p
|
wneuper@31
|
645 |
in iteratorOK2xml cI ip' end)
|
wneuper@31
|
646 |
handle (PTREE e) => iteratorERROR2xml cI)
|
wneuper@31
|
647 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
648 |
|
wneuper@31
|
649 |
fun moveActiveUp cI =
|
wneuper@31
|
650 |
((let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
651 |
val ip' = move_up [] pt (get_pos cI 1)
|
wneuper@31
|
652 |
val _ = upd_ipos cI 1 ip'
|
wneuper@31
|
653 |
in iteratorOK2xml cI ip' end)
|
wneuper@31
|
654 |
handle PTREE e => iteratorERROR2xml cI)
|
wneuper@31
|
655 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
656 |
fun moveUp cI (p:pos') =
|
wneuper@31
|
657 |
((let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
658 |
val ip' = move_up [] pt p
|
wneuper@31
|
659 |
in iteratorOK2xml cI ip' end)
|
wneuper@31
|
660 |
handle PTREE e => iteratorERROR2xml cI)
|
wneuper@31
|
661 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
662 |
|
wneuper@31
|
663 |
fun moveActiveLevelUp cI =
|
wneuper@31
|
664 |
((let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
665 |
val ip' = movelevel_up [] pt (get_pos cI 1)
|
wneuper@31
|
666 |
val _ = upd_ipos cI 1 ip'
|
wneuper@31
|
667 |
in iteratorOK2xml cI ip' end)
|
wneuper@31
|
668 |
handle PTREE e => iteratorERROR2xml cI)
|
wneuper@31
|
669 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
670 |
fun moveLevelUp cI (p:pos') =
|
wneuper@31
|
671 |
((let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
672 |
val ip' = movelevel_up [] pt p
|
wneuper@31
|
673 |
in iteratorOK2xml cI ip' end)
|
wneuper@31
|
674 |
handle PTREE e => iteratorERROR2xml cI)
|
wneuper@31
|
675 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
676 |
|
wneuper@31
|
677 |
fun moveActiveCalcHead cI =
|
wneuper@31
|
678 |
((let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
679 |
val ip' = movecalchd_up pt (get_pos cI 1)
|
wneuper@31
|
680 |
val _ = upd_ipos cI 1 ip'
|
wneuper@31
|
681 |
in iteratorOK2xml cI ip' end)
|
wneuper@31
|
682 |
handle PTREE e => iteratorERROR2xml cI)
|
wneuper@31
|
683 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
684 |
fun moveCalcHead cI (p:pos') =
|
wneuper@31
|
685 |
((let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
686 |
val ip' = movecalchd_up pt p
|
wneuper@31
|
687 |
in iteratorOK2xml cI ip' end)
|
wneuper@31
|
688 |
handle PTREE e => iteratorERROR2xml cI)
|
wneuper@31
|
689 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
690 |
|
wneuper@31
|
691 |
|
wneuper@31
|
692 |
(*.initContext Thy_ is conceptually impossible at [Pbl,Met]
|
wneuper@31
|
693 |
and at positions with Check_Postcond and End_Trans;
|
wneuper@31
|
694 |
at possible pos's there can be NO rewrite (returned as a context, too).*)
|
wneuper@31
|
695 |
(* val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([1], Frm));
|
wneuper@31
|
696 |
val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([], Res));
|
wneuper@31
|
697 |
val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([2], Res));
|
wneuper@31
|
698 |
val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([1,1], Frm));
|
wneuper@31
|
699 |
*)
|
wneuper@31
|
700 |
fun initContext (cI:calcID) Thy_ (pos as (p,p_):pos') =
|
wneuper@31
|
701 |
((if p_ mem [Pbl,Met] then message2xml cI "thy-context not to calchead"
|
wneuper@31
|
702 |
else if pos = ([],Res) then message2xml cI "no thy-context at result"
|
wneuper@31
|
703 |
else let val cs as (ptp as (pt,_),_) = get_calc cI
|
wneuper@31
|
704 |
in if exist_lev_on' pt pos
|
wneuper@31
|
705 |
then let val pos' = lev_on' pt pos
|
wneuper@31
|
706 |
val tac = get_tac_checked pt pos'
|
wneuper@31
|
707 |
in if is_rewtac tac
|
wneuper@31
|
708 |
then contextthyOK2xml cI (context_thy (pt,pos) tac)
|
wneuper@31
|
709 |
else message2xml cI ("no thy-context at tac '" ^
|
wneuper@31
|
710 |
tac2str tac ^ "'")
|
wneuper@31
|
711 |
end
|
wneuper@31
|
712 |
else if is_curr_endof_calc pt pos
|
wneuper@31
|
713 |
then case step pos cs of
|
wneuper@31
|
714 |
(* val (str, (tacis, _, (pt,_))) = step pos cs;
|
wneuper@31
|
715 |
val ("ok", (tacis, _, (pt,_))) = step pos cs;
|
wneuper@31
|
716 |
*)
|
wneuper@31
|
717 |
("ok", (tacis, _, (pt,_))) =>
|
wneuper@31
|
718 |
let val tac = fst3 (last_elem tacis)
|
wneuper@31
|
719 |
in if is_rewtac tac
|
wneuper@31
|
720 |
then contextthyOK2xml
|
wneuper@31
|
721 |
cI (context_thy ptp tac)
|
wneuper@31
|
722 |
else message2xml cI ("no thy-context at tac '" ^
|
wneuper@31
|
723 |
tac2str tac ^ "'")
|
wneuper@31
|
724 |
end
|
wneuper@31
|
725 |
| (msg, _) => message2xml cI msg
|
wneuper@31
|
726 |
else message2xml cI "no thy-context at this position"
|
wneuper@31
|
727 |
end)
|
wneuper@31
|
728 |
handle _ => sysERROR2xml cI "error in kernel")
|
wneuper@31
|
729 |
|
wneuper@31
|
730 |
(* val (cI, Pbl_, pos as (p,p_)) = (1, Pbl_, ([],Pbl));
|
wneuper@31
|
731 |
*)
|
wneuper@31
|
732 |
| initContext cI Pbl_ (pos as (p,p_):pos') =
|
wneuper@31
|
733 |
((let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
734 |
val pp = par_pblobj pt p
|
wneuper@31
|
735 |
val chd = initcontext_pbl pt (pp,p_)
|
wneuper@31
|
736 |
in matchpbl2xml cI chd end)
|
wneuper@31
|
737 |
handle _ => sysERROR2xml cI "error in kernel")
|
wneuper@31
|
738 |
|
wneuper@31
|
739 |
| initContext cI Met_ (pos as (p,p_):pos') =
|
wneuper@31
|
740 |
((let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
741 |
val pp = par_pblobj pt p
|
wneuper@31
|
742 |
val chd = initcontext_met pt (pp,p_)
|
wneuper@31
|
743 |
in matchmet2xml cI chd end)
|
wneuper@31
|
744 |
handle _ => sysERROR2xml cI "error in kernel");
|
wneuper@31
|
745 |
|
wneuper@31
|
746 |
|
wneuper@31
|
747 |
|
wneuper@31
|
748 |
(*.match a theorem, a ruleset (etc., selected in the knowledge-browser)
|
wneuper@31
|
749 |
with the formula in the focus on the worksheet;
|
wneuper@31
|
750 |
string contains the thy, thus it is unique as thmID, rlsID for this thy;
|
wneuper@31
|
751 |
take the substitution from the istate of the formula.*)
|
wneuper@31
|
752 |
(* use"../smltest/IsacKnowledge/poly.sml";
|
wneuper@31
|
753 |
val (cI, pos as (p,p_), guh) = (1, ([1,1,1], Frm),
|
wneuper@31
|
754 |
"thy_Poly-thm-real_diff_minus");
|
wneuper@31
|
755 |
val (cI, pos as (p,p_), guh) = (1, ([1,1], Frm), "norm_Poly");
|
wneuper@31
|
756 |
val (cI, pos as (p,p_), guh) =
|
wneuper@31
|
757 |
(1, ([1], Res), "thy_isac_Test-rls-Test_simplify");
|
wneuper@31
|
758 |
*)
|
wneuper@31
|
759 |
fun checkContext (cI:calcID) (pos:pos' as (p,p_)) (guh:guh) =
|
wneuper@31
|
760 |
(case (implode o (take_fromto 1 4) o explode) guh of
|
wneuper@31
|
761 |
"thy_" =>
|
wneuper@31
|
762 |
if p_ mem [Pbl,Met] then message2xml cI "thy-context not to calchead"
|
wneuper@31
|
763 |
else if pos = ([],Res) then message2xml cI "no thy-context at result"
|
wneuper@31
|
764 |
else if no_thycontext guh then message2xml cI ("no thy-context for '"^
|
wneuper@31
|
765 |
guh ^ "'")
|
wneuper@31
|
766 |
else let val (ptp as (pt,_),_) = get_calc cI
|
wneuper@31
|
767 |
val is = get_istate pt pos
|
wneuper@31
|
768 |
val subs = subs_from is "dummy" guh
|
wneuper@31
|
769 |
val tac = guh2rewtac guh subs
|
wneuper@31
|
770 |
in contextthyOK2xml cI (context_thy (pt, pos) tac) end
|
wneuper@31
|
771 |
|
wneuper@31
|
772 |
(*.match the model of a problem at pos p
|
wneuper@31
|
773 |
with the model-pattern of the problem with pblID.*)
|
wneuper@31
|
774 |
(* val (cI, pos:pos' as (p,p_), guh) =
|
wneuper@31
|
775 |
(1, p, kestoreID2guh Pbl_ ["univariate","equation"]);
|
wneuper@31
|
776 |
val (cI, pos:pos' as (p,p_), guh) =
|
wneuper@31
|
777 |
(1, ([],Pbl), kestoreID2guh Pbl_ ["univariate","equation"]);
|
wneuper@31
|
778 |
val (cI, pos:pos' as (p,p_), guh) =
|
wneuper@31
|
779 |
(1, ([],Pbl), "pbl_equ_univ");
|
wneuper@31
|
780 |
*)
|
wneuper@31
|
781 |
| "pbl_" =>
|
wneuper@31
|
782 |
let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
783 |
val pp = par_pblobj pt p
|
wneuper@31
|
784 |
val keID = guh2kestoreID guh
|
wneuper@31
|
785 |
val chd = context_pbl keID pt pp
|
wneuper@31
|
786 |
in matchpbl2xml cI chd end
|
wneuper@31
|
787 |
(* val (cI, pos:pos' as (p,p_), guh) =
|
wneuper@31
|
788 |
(1, ([],Pbl), kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
|
wneuper@31
|
789 |
*)
|
wneuper@31
|
790 |
| "met_" =>
|
wneuper@31
|
791 |
let val ((pt,_),_) = get_calc cI
|
wneuper@31
|
792 |
val pp = par_pblobj pt p
|
wneuper@31
|
793 |
val keID = guh2kestoreID guh
|
wneuper@31
|
794 |
val chd = context_met keID pt pp
|
wneuper@31
|
795 |
in matchmet2xml cI chd end)
|
wneuper@31
|
796 |
handle _ => sysERROR2xml cI "error in kernel";
|
wneuper@31
|
797 |
|
wneuper@31
|
798 |
|
wneuper@31
|
799 |
(*------------------------------------------------------------------*)
|
wneuper@31
|
800 |
end
|
wneuper@31
|
801 |
open interface;
|
wneuper@31
|
802 |
(*------------------------------------------------------------------*)
|