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