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@59260
|
12 |
signature KERNEL =
|
neuper@37906
|
13 |
sig
|
walther@59905
|
14 |
val appendFormula : calcID -> TermC.as_string -> XML.tree (*unit future*)
|
walther@59905
|
15 |
val autoCalculate : calcID -> Solve.auto -> XML.tree (*unit future*)
|
walther@59905
|
16 |
val applyTactic : calcID -> Pos.pos' -> Tactic.input -> XML.tree
|
walther@59941
|
17 |
val CalcTree : Formalise.T list -> XML.tree
|
walther@59905
|
18 |
val checkContext : calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
|
walther@59905
|
19 |
val DEconstrCalcTree : calcID -> XML.tree
|
walther@59905
|
20 |
val fetchApplicableTactics : calcID -> int -> Pos.pos' -> XML.tree
|
walther@59905
|
21 |
val fetchProposedTactic : calcID -> XML.tree
|
walther@59909
|
22 |
val findFillpatterns : calcID -> Error_Pattern_Def.id -> XML.tree
|
walther@59905
|
23 |
val getAccumulatedAsms : calcID -> Pos.pos' -> XML.tree
|
walther@59905
|
24 |
val getActiveFormula : calcID -> XML.tree
|
walther@59905
|
25 |
val getAssumptions : calcID -> Pos.pos' -> XML.tree
|
walther@59905
|
26 |
val getFormulaeFromTo : calcID -> Pos.pos' -> Pos.pos' -> int -> bool -> XML.tree
|
walther@59905
|
27 |
val getTactic : calcID -> Pos.pos' -> XML.tree
|
walther@59974
|
28 |
val initContext : calcID -> Ptool.ketype -> Pos.pos' -> XML.tree
|
walther@59905
|
29 |
val inputFillFormula: calcID -> string -> XML.tree
|
walther@59905
|
30 |
val interSteps : calcID -> Pos.pos' -> XML.tree
|
walther@59905
|
31 |
val Iterator : calcID -> XML.tree
|
walther@59905
|
32 |
val IteratorTEST : calcID -> iterID
|
walther@59905
|
33 |
val modelProblem : calcID -> XML.tree
|
walther@59984
|
34 |
val modifyCalcHead : calcID -> P_Spec.icalhd -> XML.tree
|
walther@59905
|
35 |
val moveActiveCalcHead : calcID -> XML.tree
|
walther@59905
|
36 |
val moveActiveDown : calcID -> XML.tree
|
walther@59905
|
37 |
val moveActiveFormula : calcID -> Pos.pos' -> XML.tree
|
walther@59905
|
38 |
val moveActiveLevelDown : calcID -> XML.tree
|
walther@59905
|
39 |
val moveActiveLevelUp : calcID -> XML.tree
|
walther@59905
|
40 |
val moveActiveRoot : calcID -> XML.tree
|
walther@59905
|
41 |
val moveActiveRootTEST : calcID -> XML.tree
|
walther@59905
|
42 |
val moveActiveUp : calcID -> XML.tree
|
walther@59905
|
43 |
val moveCalcHead : calcID -> Pos.pos' -> XML.tree
|
walther@59905
|
44 |
val moveDown : calcID -> Pos.pos' -> XML.tree
|
walther@59905
|
45 |
val moveLevelDown : calcID -> Pos.pos' -> XML.tree
|
walther@59905
|
46 |
val moveLevelUp : calcID -> Pos.pos' -> XML.tree
|
walther@59905
|
47 |
val moveRoot : calcID -> XML.tree
|
walther@59905
|
48 |
val moveUp : calcID -> Pos.pos' -> XML.tree
|
walther@59905
|
49 |
val refFormula : calcID -> Pos.pos' -> XML.tree
|
walther@59905
|
50 |
val refineProblem : calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
|
walther@59905
|
51 |
val replaceFormula : calcID -> TermC.as_string -> XML.tree
|
walther@59909
|
52 |
val requestFillformula : calcID -> Error_Pattern_Def.id * Error_Pattern_Def.fill_in_id -> XML.tree
|
walther@59905
|
53 |
val resetCalcHead : calcID -> XML.tree
|
walther@59905
|
54 |
val setContext : calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
|
walther@59905
|
55 |
val setMethod : calcID -> Method.id -> XML.tree
|
walther@59905
|
56 |
val setNextTactic : calcID -> Tactic.input -> XML.tree
|
walther@59905
|
57 |
val setProblem : calcID -> Problem.id -> XML.tree
|
walther@59905
|
58 |
val setTheory : calcID -> ThyC.id -> XML.tree
|
walther@59886
|
59 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
wneuper@59260
|
60 |
(* NONE *)
|
walther@59886
|
61 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
neuper@37906
|
62 |
end
|
neuper@37906
|
63 |
|
wneuper@59260
|
64 |
(**)
|
wneuper@59260
|
65 |
structure Kernel(**): KERNEL(**) =
|
neuper@37906
|
66 |
struct
|
walther@59613
|
67 |
(**)
|
wneuper@59276
|
68 |
open Ctree
|
walther@59695
|
69 |
open Pos
|
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@59600
|
74 |
+ see "fun en/decode" in /mathml.sml *)
|
walther@59822
|
75 |
fun encode_imodel imodel =
|
walther@59984
|
76 |
let fun enc (P_Spec.Given ifos) = P_Spec.Given (map encode ifos)
|
walther@59984
|
77 |
| enc (P_Spec.Find ifos) = P_Spec.Find (map encode ifos)
|
walther@59984
|
78 |
| enc (P_Spec.Relate ifos) = P_Spec.Relate (map encode ifos)
|
walther@59984
|
79 |
in map enc imodel:P_Spec.imodel end;
|
walther@59984
|
80 |
fun encode_icalhd ((pos', headl, imodel, pos_, spec) : P_Spec.icalhd) =
|
walther@59984
|
81 |
(pos', encode headl, encode_imodel imodel, pos_, spec) : P_Spec.icalhd;
|
wneuper@59298
|
82 |
fun encode_fmz (ifos, spec) = (map encode ifos, spec);
|
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 .*)
|
wneuper@59405
|
94 |
fun Iterator cI = (*returned ID unnecessary after WN.0411*)
|
wneuper@59405
|
95 |
(adduserOK2xml cI (add_user cI ))
|
wneuper@59260
|
96 |
handle _ => sysERROR2xml cI "error in kernel 1";
|
wneuper@59405
|
97 |
fun IteratorTEST cI = add_user cI;
|
neuper@37906
|
98 |
|
neuper@37906
|
99 |
(*.create a calc-tree; for calls from java: thus ^^^ decoded to ^;
|
neuper@37906
|
100 |
compare "fun CalcTreeTEST" which does NOT decode.*)
|
wneuper@59298
|
101 |
fun CalcTree [(fmz, sp)] (*for several variants lateron*) =
|
wneuper@59260
|
102 |
((let
|
walther@59946
|
103 |
val cs = Step_Specify.nxt_specify_init_calc (encode_fmz (fmz, sp))
|
wneuper@59260
|
104 |
val cI = add_calc cs (*FIXME.WN.8.03: error-handling missing*)
|
wneuper@59260
|
105 |
in calctreeOK2xml cI end)
|
wneuper@59260
|
106 |
handle _ => sysERROR2xml 0 "error in kernel 2")
|
wneuper@59260
|
107 |
| CalcTree [] = error "CalcTree: called with []"
|
neuper@37906
|
108 |
|
wneuper@59405
|
109 |
fun DEconstrCalcTree cI = deconstructcalctreeOK2xml (del_calc cI);
|
wneuper@59405
|
110 |
fun getActiveFormula cI = iteratorOK2xml cI (get_pos cI 1);
|
neuper@37906
|
111 |
|
wneuper@59405
|
112 |
fun moveActiveFormula cI p =
|
wneuper@59260
|
113 |
let val ((pt,_),_) = get_calc cI
|
wneuper@59260
|
114 |
in
|
wneuper@59260
|
115 |
if existpt' p pt
|
wneuper@59260
|
116 |
then (upd_ipos cI 1 p; iteratorOK2xml cI p)
|
wneuper@59260
|
117 |
else sysERROR2xml cI "frontend sends a non-existing pos"
|
wneuper@59260
|
118 |
end
|
neuper@37906
|
119 |
|
neuper@37906
|
120 |
(*. set the next tactic to be applied: dont't change the calc-tree,
|
neuper@37906
|
121 |
but remember the envisaged changes for fun autoCalculate;
|
neuper@37906
|
122 |
compare force NextTactic .*)
|
wneuper@59405
|
123 |
fun setNextTactic cI tac =
|
s1210629013@55402
|
124 |
let
|
walther@59981
|
125 |
val ((pt, _), _) = get_calc cI (* retrieve Calc.state_pre from states *)
|
wneuper@59254
|
126 |
val ip = get_pos cI 1 (* retrieve position from states *)
|
wneuper@59260
|
127 |
in
|
walther@59804
|
128 |
case Step.by_tactic tac (pt, ip) of
|
walther@59981
|
129 |
("ok", (tacis, _, _)) => (* update Calc.state_pre in states *)
|
wneuper@59260
|
130 |
(upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")
|
wneuper@59260
|
131 |
| ("unsafe-ok", (tacis, _, _)) =>
|
wneuper@59260
|
132 |
(upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "unsafe-ok")
|
wneuper@59260
|
133 |
| ("not-applicable", _) => setnexttactic2xml cI "not-applicable"
|
wneuper@59260
|
134 |
| ("end-of-calculation", _) => setnexttactic2xml cI "end-of-calculation"
|
walther@59804
|
135 |
| (msg, _) => sysERROR2xml cI ("setNextTactic: Step.by_tactic returns " ^ msg)
|
wneuper@59260
|
136 |
end;
|
neuper@37906
|
137 |
|
neuper@37906
|
138 |
(*. apply a tactic at a position and update the calc-tree if applicable .*)
|
neuper@37947
|
139 |
(*WN080226 java-code is missing, errors smltest/Knowledge/polyminus.sml*)
|
wneuper@59405
|
140 |
fun applyTactic cI ip tac =
|
neuper@42437
|
141 |
let
|
neuper@42437
|
142 |
val ((pt, _), _) = get_calc cI
|
neuper@42437
|
143 |
val p = get_pos cI 1
|
s1210629013@55402
|
144 |
in
|
walther@59804
|
145 |
case Step.by_tactic tac (pt, ip) of
|
wneuper@59260
|
146 |
("ok", (_, c, ptp as (_, p'))) =>
|
neuper@42437
|
147 |
(upd_calc cI (ptp, []);
|
neuper@42437
|
148 |
upd_ipos cI 1 p';
|
neuper@42437
|
149 |
autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
|
wneuper@59260
|
150 |
| ("unsafe-ok", (_, c, ptp as (_, p'))) =>
|
neuper@42437
|
151 |
(upd_calc cI (ptp, []);
|
neuper@42437
|
152 |
upd_ipos cI 1 p';
|
neuper@42437
|
153 |
autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
|
wneuper@59260
|
154 |
| ("end-of-calculation", (_, c, ptp as (_, p'))) =>
|
neuper@42437
|
155 |
(upd_calc cI (ptp, []);
|
neuper@42437
|
156 |
upd_ipos cI 1 p';
|
neuper@42437
|
157 |
autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
|
walther@59804
|
158 |
| (str, _) => autocalculateERROR2xml cI ("applyTactic: Step.by_tactic returns " ^ str)
|
neuper@42437
|
159 |
end;
|
neuper@37906
|
160 |
|
wneuper@59405
|
161 |
fun fetchProposedTactic cI =
|
walther@59765
|
162 |
(case Step.do_next (get_pos cI 1) (get_calc cI) of
|
wneuper@59260
|
163 |
("ok", (tacis, _, _)) =>
|
wneuper@59260
|
164 |
let
|
wneuper@59260
|
165 |
val _= upd_tacis cI tacis
|
wneuper@59260
|
166 |
val (tac, _, _) = last_elem tacis
|
walther@59909
|
167 |
in fetchproposedtacticOK2xml cI tac (Error_Pattern.from_store tac) end
|
wneuper@59260
|
168 |
| ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless"
|
wneuper@59260
|
169 |
| ("no-fmz-spec", _) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
|
wneuper@59260
|
170 |
| ("end-of-calculation", _) =>
|
wneuper@59260
|
171 |
fetchproposedtacticERROR2xml cI "end-of-calculation")
|
wneuper@59260
|
172 |
handle _ => sysERROR2xml cI "error in kernel 3";
|
neuper@42412
|
173 |
|
wneuper@59405
|
174 |
fun autoCalculate cI auto = (*Future.fork
|
wneuper@59260
|
175 |
(fn () => (( *)let
|
wneuper@59260
|
176 |
val pold = get_pos cI 1
|
wneuper@59260
|
177 |
in
|
wneuper@59569
|
178 |
case Math_Engine.autocalc [] pold (get_calc cI) auto of
|
wneuper@59260
|
179 |
("ok", c, ptp as (_,p)) =>
|
wneuper@59260
|
180 |
(upd_calc cI (ptp, []); upd_ipos cI 1 p;
|
wneuper@59260
|
181 |
autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
|
walther@59762
|
182 |
| ("dummy", c, ptp as (_,p)) => (*prelim. until \<open>Review modelling- + specification-phase\<close>*)
|
walther@59762
|
183 |
(upd_calc cI (ptp, []); upd_ipos cI 1 p;
|
walther@59762
|
184 |
autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
|
wneuper@59260
|
185 |
| ("end-of-calculation", c, ptp as (_,p)) =>
|
wneuper@59260
|
186 |
(upd_calc cI (ptp, []); upd_ipos cI 1 p;
|
wneuper@59260
|
187 |
autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
|
wneuper@59260
|
188 |
| (str, _, _) => autocalculateERROR2xml cI str
|
wneuper@59260
|
189 |
end (* ) *)
|
wneuper@59260
|
190 |
handle ERROR msg => sysERROR2xml cI ("error in kernel 4: " ^ msg)(* )) *);
|
s1210629013@55402
|
191 |
|
neuper@37906
|
192 |
fun getTactic cI (p:pos') =
|
wneuper@59260
|
193 |
(let
|
wneuper@59260
|
194 |
val ((pt, _), _) = get_calc cI
|
walther@59983
|
195 |
val (_, tac, _) = ME_Misc.pt_extract (pt, p)
|
wneuper@59260
|
196 |
in
|
wneuper@59260
|
197 |
case tac of
|
wneuper@59260
|
198 |
SOME ta => gettacticOK2xml cI ta
|
wneuper@59260
|
199 |
| NONE => gettacticERROR2xml cI ("no tactic at position " ^ pos'2str p)
|
wneuper@59260
|
200 |
end)
|
wneuper@59137
|
201 |
handle _ => sysERROR2xml cI "syserror in getTactic";
|
neuper@37906
|
202 |
|
wneuper@59260
|
203 |
(* Fetch tactics to be applied to a particular step.
|
wneuper@59260
|
204 |
Requirements are not yet implemented, see ICalcIterator#fetchApplicableTactics"
|
wneuper@59260
|
205 |
@see #TACTICS_ALL
|
wneuper@59260
|
206 |
@see #TACTICS_CURRENT_THEORY
|
wneuper@59260
|
207 |
@see #TACTICS_CURRENT_METHOD ..the only impl.WN040307
|
walther@59823
|
208 |
LItool.specific_from_prog waits to be used here
|
neuper@42438
|
209 |
*)
|
wneuper@59260
|
210 |
fun fetchApplicableTactics cI (_(*scope*): int) (p : pos') =
|
wneuper@59260
|
211 |
(let val ((pt, _), _) = get_calc cI
|
walther@59823
|
212 |
in (applicabletacticsOK cI (Fetch_Tacs.from_prog pt p))
|
wneuper@59260
|
213 |
handle PTREE str => sysERROR2xml cI str
|
wneuper@59260
|
214 |
end)
|
wneuper@59140
|
215 |
handle _ => sysERROR2xml cI "error in kernel 5";
|
wneuper@59134
|
216 |
|
neuper@37906
|
217 |
fun getAssumptions cI (p:pos') =
|
wneuper@59260
|
218 |
(let
|
wneuper@59260
|
219 |
val ((pt, _), _) = get_calc cI
|
walther@59983
|
220 |
val (_, _, asms) = ME_Misc.pt_extract (pt, p)
|
wneuper@59260
|
221 |
in getasmsOK2xml cI asms end)
|
wneuper@59260
|
222 |
handle _ => sysERROR2xml cI "syserror in getAssumptions"
|
neuper@37906
|
223 |
|
neuper@37906
|
224 |
(*WN0502 @see ME/ctree: type asms: illdesigned, thus no positions returned*)
|
neuper@37906
|
225 |
fun getAccumulatedAsms cI (p:pos') =
|
wneuper@59260
|
226 |
(let
|
wneuper@59260
|
227 |
val ((pt, _), _) = get_calc cI
|
walther@59844
|
228 |
val ass = Ctree.get_assumptions pt p
|
wneuper@59260
|
229 |
in getasmsOK2xml cI ass end)
|
wneuper@59260
|
230 |
handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms"
|
neuper@37906
|
231 |
|
wneuper@59260
|
232 |
fun refFormula cI (p: pos') = (*WN0501 rename to "fun getElement" !*)
|
wneuper@59152
|
233 |
(let
|
wneuper@59152
|
234 |
val ((pt, _), _) = get_calc cI
|
walther@59983
|
235 |
val (form, _, _) = ME_Misc.pt_extract (pt, p)
|
wneuper@59152
|
236 |
in refformulaOK2xml cI p form end)
|
wneuper@59260
|
237 |
handle _ => sysERROR2xml cI ("error in kernel 6: refFormula " ^ int2str cI ^ " " ^ pos'2str p)
|
neuper@37906
|
238 |
|
wneuper@59260
|
239 |
(* get formulae "from" "to" w.r.t. ordering in Position#compareTo(Position p);
|
wneuper@59260
|
240 |
"level" is adjusted such that an "interval" of formulae is returned;
|
wneuper@59260
|
241 |
"from" "to" are designed for use by iterators of calcChangedEvent,
|
wneuper@59260
|
242 |
thus "from" is the last unchanged position *)
|
wneuper@59260
|
243 |
fun getFormulaeFromTo cI (([], Pbl) : pos') (to as ([], Pbl) : pos') _ false =
|
wneuper@59127
|
244 |
((let
|
wneuper@59260
|
245 |
val ((pt,_),_) = get_calc cI
|
wneuper@59516
|
246 |
val headline =
|
walther@59983
|
247 |
case ME_Misc.pt_extract (pt, to) of
|
wneuper@59516
|
248 |
(ModSpec (_, _, headline, _, _, _), _, _) => headline
|
walther@59983
|
249 |
| _ => raise ERROR "getFormulaeFromTo: uncovered case of ME_Misc.pt_extract"
|
wneuper@59516
|
250 |
in getintervalOK cI [(to, headline, NONE)] end)
|
wneuper@59260
|
251 |
handle _ => sysERROR2xml cI "error in kernel 7")
|
wneuper@59260
|
252 |
| getFormulaeFromTo cI ([], Pbl) ([], Met) _ false =
|
wneuper@59260
|
253 |
getFormulaeFromTo cI ([], Pbl) ([], Pbl) (~00000) false
|
wneuper@59260
|
254 |
(* ^^^ separated cases, because "from" is _before_ the first elements to be returned*)
|
wneuper@59260
|
255 |
| getFormulaeFromTo cI from to level false =
|
wneuper@59260
|
256 |
(if from = to
|
wneuper@59260
|
257 |
then sysERROR2xml cI "getFormulaeFromTo: From = To"
|
wneuper@59260
|
258 |
else
|
wneuper@59260
|
259 |
(case from of
|
wneuper@59260
|
260 |
([], Res) => sysERROR2xml cI ("getFormulaeFromTo does: moveDown " ^
|
wneuper@59260
|
261 |
"from=([],Res) .. goes beyond result")
|
wneuper@59260
|
262 |
| _ =>
|
wneuper@59260
|
263 |
let
|
wneuper@59260
|
264 |
val ((pt,_),_) = get_calc cI
|
wneuper@59260
|
265 |
val f = move_dn [] pt from
|
wneuper@59260
|
266 |
fun max (a,b) = if a < b then b else a
|
wneuper@59260
|
267 |
val lev = max (level, max (lev_of from, lev_of to)) (*... must reach margins *)
|
walther@59983
|
268 |
in getintervalOK cI (ME_Misc.get_interval f to lev pt) end)
|
wneuper@59137
|
269 |
handle _ => sysERROR2xml cI "error in getFormulaeFromTo")
|
neuper@37906
|
270 |
| getFormulaeFromTo cI from to level true =
|
wneuper@59137
|
271 |
sysERROR2xml cI ("getFormulaeFromTo impl.for formulae only, " ^
|
wneuper@59127
|
272 |
"i.e. last arg only impl. for false, _NOT_ true");
|
neuper@37906
|
273 |
|
neuper@37906
|
274 |
fun interSteps cI ip =
|
wneuper@59260
|
275 |
(let val ((pt, p), tacis) = get_calc cI
|
neuper@55471
|
276 |
in
|
neuper@55471
|
277 |
if (not o is_interpos) ip
|
neuper@55471
|
278 |
then interStepsERROR cI ("only formulae with position (_,Res) " ^
|
neuper@55471
|
279 |
"may have intermediate steps above them")
|
neuper@55471
|
280 |
else
|
neuper@55471
|
281 |
let val ip' = lev_pred' pt ip
|
walther@59833
|
282 |
in case Detail_Step.go pt ip of
|
wneuper@59260
|
283 |
("detailrls", pt, lastpos) =>
|
wneuper@59260
|
284 |
(upd_calc cI ((pt, p), tacis); interStepsOK cI ip' ip' lastpos)
|
wneuper@59260
|
285 |
| ("no-Rewrite_Set...", _, _) => sysERROR2xml cI "no Rewrite_Set..."
|
wneuper@59260
|
286 |
| (_, _, lastpos) => interStepsOK cI ip' ip' lastpos
|
neuper@55471
|
287 |
end
|
neuper@55471
|
288 |
end)
|
wneuper@59260
|
289 |
handle _ => sysERROR2xml cI "error in kernel 8";
|
neuper@37906
|
290 |
|
walther@59984
|
291 |
fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_) : P_Spec.icalhd) =
|
wneuper@59260
|
292 |
(let
|
wneuper@59260
|
293 |
val ((pt,_),_) = get_calc cI
|
walther@59984
|
294 |
val (pt, chd as (_,p_,_,_,_,_)) = P_Spec.input_icalhd pt ichd
|
wneuper@59260
|
295 |
in (upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end)
|
wneuper@59140
|
296 |
handle _ => sysERROR2xml cI "error in kernel 9";
|
neuper@37906
|
297 |
|
wneuper@59260
|
298 |
(* at the activeFormula set the Model, the Guard and the Specification to empty
|
wneuper@59260
|
299 |
and return a CalcHead; the 'origin' remains (for reconstructing all that) *)
|
wneuper@59260
|
300 |
fun resetCalcHead cI =
|
wneuper@59260
|
301 |
(let
|
wneuper@59260
|
302 |
val (ptp,_) = get_calc cI
|
walther@60097
|
303 |
val ptp = SpecificationC.reset ptp
|
walther@60097
|
304 |
in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end)
|
wneuper@59140
|
305 |
handle _ => sysERROR2xml cI "error in kernel 10";
|
neuper@37906
|
306 |
|
wneuper@59260
|
307 |
(* at the activeFormula insert all the Descriptions in the Model and return a CalcHead;
|
wneuper@59260
|
308 |
the Descriptions are for user-guidance; the rest of the items are left empty for user-input *)
|
wneuper@59260
|
309 |
fun modelProblem cI =
|
wneuper@59260
|
310 |
(let val (ptp, _) = get_calc cI
|
walther@60097
|
311 |
val ptp = SpecificationC.reset ptp
|
walther@60020
|
312 |
val (_, (_, _, ptp)) = Step_Specify.by_tactic_input Tactic.Model_Problem ptp
|
walther@60097
|
313 |
in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end)
|
wneuper@59140
|
314 |
handle _ => sysERROR2xml cI "error in kernel 11";
|
neuper@37906
|
315 |
|
wneuper@59166
|
316 |
(* set the UContext determined on a knowledgebrowser to the current calc
|
wneuper@59166
|
317 |
WN0825: not implemented in isac-java.
|
wneuper@59166
|
318 |
Recalling the state of development after summer-term 2006 (Robert Koenishofer et.al.):
|
wneuper@59260
|
319 |
Main success was showing UContext from Worksheet to the Example/Method/Problem/TheoryBrowser,
|
wneuper@59166
|
320 |
while the buttons on these browsers <To Worksheet> <Try Refine> have no
|
wneuper@59166
|
321 |
code in isac-java (and only partial, untested code in isabisac).
|
wneuper@59166
|
322 |
*)
|
wneuper@59405
|
323 |
fun setContext cI (ip as (_,p_)) guh =
|
wneuper@59128
|
324 |
case (implode o (take_fromto 1 4) o Symbol.explode) guh of
|
wneuper@59260
|
325 |
"thy_" =>
|
wneuper@59260
|
326 |
if member op = [Pbl, Met] p_
|
wneuper@59260
|
327 |
then message2xml cI "thy-context not to calchead"
|
wneuper@59260
|
328 |
else if ip = ([], Res) then message2xml cI "no thy-context at result"
|
walther@59917
|
329 |
else if Thy_Present.no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
|
wneuper@59260
|
330 |
else
|
wneuper@59260
|
331 |
((let
|
wneuper@59260
|
332 |
val (ptp as (pt, pold), _) = get_calc cI
|
walther@59807
|
333 |
val is = get_istate_LI pt ip
|
walther@59917
|
334 |
val subs = Thy_Present.subs_from is "dummy" guh
|
walther@59917
|
335 |
val tac = Thy_Present.guh2rewtac guh subs
|
wneuper@59260
|
336 |
in
|
walther@59804
|
337 |
case Step.by_tactic tac (pt, ip) of (*='fun setNextTactic'+step*)
|
wneuper@59260
|
338 |
("ok", (tacis, c, ptp as (_, p))) =>
|
wneuper@59260
|
339 |
(upd_calc cI ((pt, p), []);
|
wneuper@59260
|
340 |
autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
|
wneuper@59260
|
341 |
| ("unsafe-ok", (tacis, c, ptp as (_ ,p))) =>
|
wneuper@59260
|
342 |
(upd_calc cI ((pt, p), []);
|
wneuper@59260
|
343 |
autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
|
wneuper@59260
|
344 |
| ("end-of-calculation", _) => message2xml cI "end-of-calculation"
|
wneuper@59260
|
345 |
| ("failure", _) => sysERROR2xml cI "failure"
|
wneuper@59260
|
346 |
| ("not-applicable", _) => (*the rule comes from anywhere..*)
|
walther@59921
|
347 |
(case Step.check tac (pt, ip) of
|
walther@59920
|
348 |
Applicable.No e => message2xml cI ("'" ^ Tactic.input_to_string tac ^ "' not-applicable")
|
walther@59920
|
349 |
| Applicable.Yes m =>
|
wneuper@59260
|
350 |
let
|
wneuper@59260
|
351 |
val ctxt = get_ctxt pt pold
|
wneuper@59260
|
352 |
val (p, c, _, pt) =
|
walther@59932
|
353 |
Step.add m (Istate.Uistate, ctxt) (pt, ip)
|
wneuper@59260
|
354 |
in upd_calc cI ((pt, p), []);
|
neuper@41993
|
355 |
autocalculateOK2xml cI pold (if null c then pold else last_elem c) p
|
wneuper@59260
|
356 |
end)
|
wneuper@59260
|
357 |
end
|
wneuper@59260
|
358 |
) handle _ => sysERROR2xml cI "setContext: thy_ ???")
|
wneuper@59260
|
359 |
| "pbl_" =>
|
wneuper@59260
|
360 |
((let
|
walther@59974
|
361 |
val pI = Ptool.guh2kestoreID guh
|
wneuper@59260
|
362 |
val ((pt, _), _) = get_calc cI
|
wneuper@59260
|
363 |
in
|
wneuper@59260
|
364 |
if member op = [Pbl, Met] p_
|
wneuper@59260
|
365 |
then
|
wneuper@59261
|
366 |
let val (pt, chd) = Math_Engine.set_problem pI (pt, ip)
|
wneuper@59260
|
367 |
in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
|
wneuper@59260
|
368 |
else sysERROR2xml cI "setContext for pbl requires ActiveFormula on CalcHead"
|
wneuper@59260
|
369 |
end
|
wneuper@59260
|
370 |
) handle _ => sysERROR2xml cI "setContext: pbl_ ???")
|
wneuper@59260
|
371 |
| "met_" =>
|
wneuper@59260
|
372 |
((let
|
walther@59974
|
373 |
val mI = Ptool.guh2kestoreID guh
|
wneuper@59260
|
374 |
val ((pt, _), _) = get_calc cI
|
wneuper@59260
|
375 |
in
|
wneuper@59260
|
376 |
if member op = [Pbl, Met] p_
|
wneuper@59260
|
377 |
then
|
walther@60010
|
378 |
let
|
walther@60010
|
379 |
val (pt, chd) = Math_Engine.set_method mI (pt, ip)
|
walther@60010
|
380 |
in
|
walther@60010
|
381 |
(upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd)
|
walther@60010
|
382 |
end
|
wneuper@59260
|
383 |
else sysERROR2xml cI "setContext for met requires ActiveFormula on CalcHead"
|
wneuper@59260
|
384 |
end
|
wneuper@59260
|
385 |
) handle _ => sysERROR2xml cI "setContext: met_ ???")
|
neuper@37906
|
386 |
|
neuper@37906
|
387 |
|
wneuper@59260
|
388 |
(* specify the Method at the activeFormula and return a CalcHead containing the Guard.
|
wneuper@59260
|
389 |
WN0512 impl.incomplete, see "nxt_specif (Specify_Method" *)
|
wneuper@59260
|
390 |
fun setMethod cI mI =
|
wneuper@59129
|
391 |
(let
|
wneuper@59129
|
392 |
val ((pt, _), _) = get_calc cI
|
wneuper@59129
|
393 |
val ip as (_, p_) = get_pos cI 1
|
wneuper@59260
|
394 |
in
|
wneuper@59260
|
395 |
if member op = [Pbl,Met] p_
|
wneuper@59260
|
396 |
then
|
wneuper@59261
|
397 |
let val (pt, chd) = Math_Engine.set_method mI (pt, ip)
|
wneuper@59260
|
398 |
in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
|
wneuper@59260
|
399 |
else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead"
|
wneuper@59260
|
400 |
end
|
wneuper@59260
|
401 |
) handle _ => sysERROR2xml cI "error in kernel 12";
|
neuper@37906
|
402 |
|
wneuper@59260
|
403 |
(* specify the Problem at the activeFormula and return a CalcHead containing the Model;
|
wneuper@59260
|
404 |
special case of checkContext; WN0512 impl.incomplete, see "nxt_specif (Specify_Problem" *)
|
wneuper@59260
|
405 |
fun setProblem cI pI =
|
wneuper@59129
|
406 |
(let
|
wneuper@59129
|
407 |
val ((pt, _), _) = get_calc cI
|
wneuper@59129
|
408 |
val ip as (_, p_) = get_pos cI 1
|
wneuper@59129
|
409 |
in
|
wneuper@59129
|
410 |
if member op = [Pbl,Met] p_
|
wneuper@59129
|
411 |
then
|
wneuper@59261
|
412 |
let val (pt, chd) = Math_Engine.set_problem pI (pt, ip)
|
wneuper@59129
|
413 |
in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
|
wneuper@59137
|
414 |
else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
|
wneuper@59129
|
415 |
end
|
wneuper@59140
|
416 |
) handle _ => sysERROR2xml cI "error in kernel 13";
|
neuper@37906
|
417 |
|
wneuper@59260
|
418 |
(* specify the Theory at the activeFormula and return a CalcHead;
|
wneuper@59260
|
419 |
special case of checkContext; WN0512 impl.incomplete, see "nxt_specif (Specify_Method" *)
|
wneuper@59260
|
420 |
fun setTheory cI tI =
|
wneuper@59129
|
421 |
(let
|
wneuper@59129
|
422 |
val ((pt, _), _) = get_calc cI
|
wneuper@59129
|
423 |
val ip as (_, p_) = get_pos cI 1
|
wneuper@59260
|
424 |
in
|
wneuper@59260
|
425 |
if member op = [Pbl,Met] p_
|
wneuper@59260
|
426 |
then
|
wneuper@59261
|
427 |
let val (pt, chd) = Math_Engine.set_theory tI (pt, ip)
|
wneuper@59260
|
428 |
in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
|
wneuper@59260
|
429 |
else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
|
wneuper@59129
|
430 |
end
|
wneuper@59140
|
431 |
) handle _ => sysERROR2xml cI "error in kernel 14";
|
neuper@37906
|
432 |
|
wneuper@59260
|
433 |
(* refinement for the parent-problem of the position,
|
wneuper@59260
|
434 |
Not used in isac-java (see comment WN0825 for setContext) but tryrefine is used within isabisac *)
|
wneuper@59260
|
435 |
fun refineProblem cI (p, p_) guh =
|
wneuper@59260
|
436 |
(let
|
walther@59974
|
437 |
val pblID = Ptool.guh2kestoreID guh
|
wneuper@59260
|
438 |
val ((pt,_),_) = get_calc cI
|
wneuper@59260
|
439 |
val pp = par_pblobj pt p
|
wneuper@59261
|
440 |
val chd = Math_Engine.tryrefine pblID pt (pp, p_)
|
wneuper@59260
|
441 |
in contextpblOK2xml cI chd end)
|
wneuper@59140
|
442 |
handle _ => sysERROR2xml cI "error in kernel 16";
|
neuper@37906
|
443 |
|
neuper@42423
|
444 |
(* append a formula to the calculation *)
|
walther@59865
|
445 |
fun appendFormula' cI (ifo: TermC.as_string) =
|
neuper@42423
|
446 |
(let
|
neuper@42423
|
447 |
val cs = get_calc cI
|
wneuper@59260
|
448 |
val pos = get_pos cI 1
|
neuper@42423
|
449 |
in
|
walther@59765
|
450 |
case Step.do_next pos cs of
|
walther@59798
|
451 |
("ok", cs' as (_, _, ptp)) =>
|
walther@59798
|
452 |
(case Step_Solve.by_term ptp (encode ifo) of
|
wneuper@59260
|
453 |
("ok", (_(*use in DG !!!*), c, ptp as (_, p))) =>
|
neuper@42423
|
454 |
(upd_calc cI (ptp, []); upd_ipos cI 1 p;
|
neuper@42423
|
455 |
appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)
|
wneuper@59260
|
456 |
| ("same-formula", (_, c, ptp as (_, p))) =>
|
neuper@42423
|
457 |
(upd_calc cI (ptp, []); upd_ipos cI 1 p;
|
neuper@42423
|
458 |
appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)
|
neuper@42423
|
459 |
| (msg, _) => appendformulaERROR2xml cI msg)
|
wneuper@59260
|
460 |
| (msg, _) => appendformulaERROR2xml cI msg
|
neuper@42423
|
461 |
end)
|
wneuper@59140
|
462 |
handle ERROR msg => sysERROR2xml cI ("error in kernel 17: " ^ msg);
|
neuper@37906
|
463 |
|
wneuper@59123
|
464 |
fun appendFormula cI ifo = (*Future.fork (fn () => *)appendFormula' cI ifo(* ) *);
|
s1210629013@55402
|
465 |
|
wneuper@59260
|
466 |
(* replace a formula with_in_ a calculation; this applies for initial CAS-commands, too *)
|
wneuper@59405
|
467 |
fun replaceFormula cI ifo =
|
wneuper@59260
|
468 |
(let
|
neuper@42437
|
469 |
val ((pt, _), _) = get_calc cI
|
neuper@42437
|
470 |
val p = get_pos cI 1
|
neuper@42437
|
471 |
in
|
walther@59798
|
472 |
case Step_Solve.by_term (pt, p) (encode ifo) of
|
wneuper@59260
|
473 |
("ok", (_(*tacs used for DG ?*), c, ptp' as (_, p'))) =>
|
neuper@42437
|
474 |
let
|
neuper@42437
|
475 |
val unc = if null (fst p) then p else move_up [] pt p
|
neuper@42437
|
476 |
val _ = upd_calc cI (ptp', [])
|
neuper@42437
|
477 |
val _ = upd_ipos cI 1 p'
|
neuper@42437
|
478 |
in replaceformulaOK2xml cI unc (if null c then unc else last_elem c) p' end
|
neuper@42437
|
479 |
| ("same-formula", _) => replaceformulaERROR2xml cI "formula not changed"
|
neuper@42437
|
480 |
| (msg, _) => replaceformulaERROR2xml cI msg
|
neuper@42437
|
481 |
end)
|
wneuper@59140
|
482 |
handle _ => sysERROR2xml cI "error in kernel 18";
|
neuper@37906
|
483 |
|
wneuper@59260
|
484 |
(*** CalcIterator
|
neuper@37906
|
485 |
moveActive*: set the pos' of the active formula stored with the calctree
|
neuper@37906
|
486 |
could take pos' as argument for consistency checks
|
neuper@37906
|
487 |
move*: compute the new iterator from the old one on the fly
|
wneuper@59260
|
488 |
***)
|
neuper@37906
|
489 |
|
neuper@37906
|
490 |
fun moveActiveRoot cI =
|
wneuper@59260
|
491 |
(let val _ = upd_ipos cI 1 ([], Pbl)
|
wneuper@59260
|
492 |
in iteratorOK2xml cI ([], Pbl) end)
|
wneuper@59260
|
493 |
handle _ => sysERROR2xml cI "error in kernel 19"
|
neuper@37906
|
494 |
fun moveRoot cI =
|
wneuper@59260
|
495 |
(iteratorOK2xml cI ([], Pbl))
|
wneuper@59260
|
496 |
handle _ => sysERROR2xml cI "";
|
neuper@37906
|
497 |
fun moveActiveRootTEST cI =
|
wneuper@59260
|
498 |
(let val _ = upd_ipos cI 1 ([], Pbl)
|
wneuper@59260
|
499 |
in iteratorOK2xml cI ([], Pbl) end)
|
wneuper@59260
|
500 |
handle _ => sysERROR2xml cI "error in kernel 20"
|
neuper@37906
|
501 |
|
neuper@37906
|
502 |
fun moveActiveDown cI =
|
wneuper@59260
|
503 |
((let
|
wneuper@59260
|
504 |
val ((pt, _), _) = get_calc cI
|
neuper@37906
|
505 |
val ip' = move_dn [] pt (get_pos cI 1)
|
neuper@37906
|
506 |
val _ = upd_ipos cI 1 ip'
|
wneuper@59260
|
507 |
in iteratorOK2xml cI ip' end)
|
wneuper@59260
|
508 |
handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 21"
|
wneuper@59260
|
509 |
fun moveDown cI p =
|
wneuper@59260
|
510 |
((let
|
wneuper@59260
|
511 |
val ((pt, _), _) = get_calc cI
|
neuper@37906
|
512 |
val ip' = move_dn [] pt p
|
wneuper@59260
|
513 |
in iteratorOK2xml cI ip' end)
|
wneuper@59260
|
514 |
handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 22"
|
neuper@37906
|
515 |
|
neuper@37906
|
516 |
fun moveActiveLevelDown cI =
|
wneuper@59260
|
517 |
((let
|
wneuper@59260
|
518 |
val ((pt, _) ,_) = get_calc cI
|
neuper@37906
|
519 |
val ip' = movelevel_dn [] pt (get_pos cI 1)
|
neuper@37906
|
520 |
val _ = upd_ipos cI 1 ip'
|
wneuper@59260
|
521 |
in iteratorOK2xml cI ip' end)
|
wneuper@59260
|
522 |
handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 23"
|
wneuper@59260
|
523 |
fun moveLevelDown cI p =
|
wneuper@59260
|
524 |
((let
|
wneuper@59260
|
525 |
val ((pt, _), _) = get_calc cI
|
wneuper@59260
|
526 |
val ip' = movelevel_dn [] pt p
|
wneuper@59260
|
527 |
in iteratorOK2xml cI ip' end)
|
wneuper@59260
|
528 |
handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 24"
|
neuper@37906
|
529 |
|
neuper@37906
|
530 |
fun moveActiveUp cI =
|
wneuper@59260
|
531 |
((let
|
wneuper@59260
|
532 |
val ((pt, _), _) = get_calc cI
|
neuper@37906
|
533 |
val ip' = move_up [] pt (get_pos cI 1)
|
neuper@37906
|
534 |
val _ = upd_ipos cI 1 ip'
|
wneuper@59260
|
535 |
in iteratorOK2xml cI ip' end)
|
wneuper@59260
|
536 |
handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 25"
|
wneuper@59260
|
537 |
fun moveUp cI p =
|
wneuper@59260
|
538 |
((let
|
wneuper@59260
|
539 |
val ((pt, _), _) = get_calc cI
|
neuper@37906
|
540 |
val ip' = move_up [] pt p
|
wneuper@59260
|
541 |
in iteratorOK2xml cI ip' end)
|
wneuper@59260
|
542 |
handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 26"
|
neuper@37906
|
543 |
|
neuper@37906
|
544 |
fun moveActiveLevelUp cI =
|
wneuper@59260
|
545 |
((let
|
wneuper@59260
|
546 |
val ((pt, _), _) = get_calc cI
|
wneuper@59260
|
547 |
val ip' = movelevel_up [] pt (get_pos cI 1)
|
wneuper@59260
|
548 |
val _ = upd_ipos cI 1 ip'
|
wneuper@59260
|
549 |
in iteratorOK2xml cI ip' end)
|
wneuper@59260
|
550 |
handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 27"
|
wneuper@59260
|
551 |
fun moveLevelUp cI p =
|
wneuper@59260
|
552 |
((let
|
wneuper@59260
|
553 |
val ((pt, _), _) = get_calc cI
|
neuper@37906
|
554 |
val ip' = movelevel_up [] pt p
|
wneuper@59260
|
555 |
in iteratorOK2xml cI ip' end)
|
wneuper@59260
|
556 |
handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 28"
|
neuper@37906
|
557 |
|
neuper@37906
|
558 |
fun moveActiveCalcHead cI =
|
wneuper@59260
|
559 |
((let
|
wneuper@59260
|
560 |
val ((pt, _), _) = get_calc cI
|
neuper@37906
|
561 |
val ip' = movecalchd_up pt (get_pos cI 1)
|
neuper@37906
|
562 |
val _ = upd_ipos cI 1 ip'
|
wneuper@59260
|
563 |
in iteratorOK2xml cI ip' end)
|
wneuper@59260
|
564 |
handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 29"
|
wneuper@59260
|
565 |
fun moveCalcHead cI p =
|
wneuper@59260
|
566 |
((let
|
wneuper@59260
|
567 |
val ((pt, _), _) = get_calc cI
|
neuper@37906
|
568 |
val ip' = movecalchd_up pt p
|
wneuper@59260
|
569 |
in iteratorOK2xml cI ip' end)
|
wneuper@59260
|
570 |
handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 30"
|
neuper@37906
|
571 |
|
s1210629013@55402
|
572 |
(*.initContext Thy_ is conceptually impossible at [Pbl,Met]
|
neuper@37906
|
573 |
and at positions with Check_Postcond and End_Trans;
|
neuper@37906
|
574 |
at possible pos's there can be NO rewrite (returned as a context, too).*)
|
walther@59974
|
575 |
fun initContext cI Ptool.Thy_ (pos as (p, p_):pos') =
|
walther@59905
|
576 |
((if member op = [Pos.Pbl, Pos.Met] p_
|
wneuper@59138
|
577 |
then message2xml cI "thy-context not to calchead"
|
wneuper@59138
|
578 |
else if pos = ([], Res) then message2xml cI "no thy-context at result"
|
wneuper@55499
|
579 |
else
|
wneuper@55499
|
580 |
let val cs as (ptp as (pt, _), _) = get_calc cI
|
wneuper@55499
|
581 |
in
|
wneuper@55499
|
582 |
if exist_lev_on' pt pos
|
wneuper@55499
|
583 |
then
|
wneuper@55499
|
584 |
let
|
wneuper@55499
|
585 |
val pos' = lev_on' pt pos
|
walther@59917
|
586 |
val tac = Thy_Present.get_tac_checked pt pos'
|
wneuper@55499
|
587 |
in
|
wneuper@59571
|
588 |
if Tactic.is_rewtac tac
|
walther@59917
|
589 |
then contextthyOK2xml cI (Thy_Present.context_thy (pt, pos) tac)
|
walther@59846
|
590 |
else message2xml cI ("no thy-context at tac '" ^ Tactic.input_to_string tac ^ "'")
|
wneuper@55499
|
591 |
end
|
wneuper@55499
|
592 |
else if is_curr_endof_calc pt pos
|
wneuper@55499
|
593 |
then
|
walther@59765
|
594 |
case Step.do_next pos cs of
|
wneuper@55499
|
595 |
("ok", (tacis, _, (pt, _))) =>
|
wneuper@55499
|
596 |
let val tac = fst3 (last_elem tacis)
|
wneuper@55499
|
597 |
in
|
wneuper@59571
|
598 |
if Tactic.is_rewtac tac
|
walther@59917
|
599 |
then contextthyOK2xml cI (Thy_Present.context_thy ptp tac)
|
walther@59846
|
600 |
else message2xml cI ("no thy-context at tac '" ^ Tactic.input_to_string tac ^ "'")
|
wneuper@55499
|
601 |
end
|
wneuper@59138
|
602 |
| (msg, _) => message2xml cI msg
|
wneuper@59138
|
603 |
else message2xml cI "no thy-context at this position"
|
wneuper@55499
|
604 |
end)
|
wneuper@59140
|
605 |
handle _ => sysERROR2xml cI "error in kernel 31")
|
walther@59974
|
606 |
| initContext cI Ptool.Pbl_ (p, p_) =
|
wneuper@59260
|
607 |
((let
|
wneuper@59260
|
608 |
val ((pt, _), _) = get_calc cI
|
wneuper@59260
|
609 |
val pp = par_pblobj pt p
|
wneuper@59261
|
610 |
val chd = Math_Engine.initcontext_pbl pt (pp,p_)
|
wneuper@59260
|
611 |
in contextpblOK2xml cI chd end)
|
wneuper@59260
|
612 |
handle _ => sysERROR2xml cI "error in kernel 32")
|
walther@59974
|
613 |
| initContext cI Ptool.Met_ (p, p_) =
|
wneuper@59260
|
614 |
((let
|
wneuper@59260
|
615 |
val ((pt,_),_) = get_calc cI
|
wneuper@59260
|
616 |
val pp = par_pblobj pt p
|
wneuper@59261
|
617 |
val chd = Math_Engine.initcontext_met pt (pp,p_)
|
wneuper@59260
|
618 |
in contextmetOK2xml cI chd end)
|
wneuper@59260
|
619 |
handle _ => sysERROR2xml cI "error in kernel 33");
|
neuper@37906
|
620 |
|
neuper@42430
|
621 |
(* match a theorem, a ruleset (etc., selected in the knowledge-browser)
|
neuper@42430
|
622 |
with the formula in the focus on the worksheet;
|
neuper@42430
|
623 |
string contains the thy, thus it is unique as thmID, rlsID for this thy;
|
neuper@42430
|
624 |
take the substitution from the istate of the formula *)
|
wneuper@59260
|
625 |
fun checkContext cI (pos as (p, p_)) guh =
|
wneuper@59132
|
626 |
case (implode o (take_fromto 1 4) o Symbol.explode) guh of
|
wneuper@59132
|
627 |
"thy_" =>
|
wneuper@59260
|
628 |
if member op = [Pbl, Met] p_
|
wneuper@59138
|
629 |
then message2xml cI "thy-context not to calchead"
|
wneuper@59138
|
630 |
else if pos = ([],Res) then message2xml cI "no thy-context at result"
|
walther@59917
|
631 |
else if Thy_Present.no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
|
wneuper@59132
|
632 |
else
|
wneuper@59132
|
633 |
((let
|
wneuper@59260
|
634 |
val ((pt,_),_) = get_calc cI
|
walther@59807
|
635 |
val is = get_istate_LI pt pos
|
walther@59917
|
636 |
val subs = Thy_Present.subs_from is "dummy" guh
|
walther@59917
|
637 |
val tac = Thy_Present.guh2rewtac guh subs
|
walther@59917
|
638 |
in contextthyOK2xml cI (Thy_Present.context_thy (pt, pos) tac) end
|
wneuper@59140
|
639 |
) handle _ => sysERROR2xml cI "error in kernel 34")
|
wneuper@59132
|
640 |
(*.match the model of a problem at pos p
|
wneuper@59132
|
641 |
with the model-pattern of the problem with pblID.*)
|
wneuper@59132
|
642 |
| "pbl_" =>
|
wneuper@59132
|
643 |
((let
|
wneuper@59260
|
644 |
val ((pt, _), _) = get_calc cI
|
wneuper@59132
|
645 |
val pp = par_pblobj pt p
|
walther@59974
|
646 |
val keID = Ptool.guh2kestoreID guh
|
wneuper@59261
|
647 |
val chd = Math_Engine.context_pbl keID pt pp
|
wneuper@59172
|
648 |
in contextpblOK2xml cI chd end
|
wneuper@59140
|
649 |
) handle _ => sysERROR2xml cI "error in kernel 35")
|
wneuper@59132
|
650 |
| "met_" =>
|
wneuper@59132
|
651 |
((let
|
wneuper@59260
|
652 |
val ((pt, _), _) = get_calc cI
|
wneuper@59132
|
653 |
val pp = par_pblobj pt p
|
walther@59974
|
654 |
val keID = Ptool.guh2kestoreID guh
|
wneuper@59261
|
655 |
val chd = Math_Engine.context_met keID pt pp
|
wneuper@59172
|
656 |
in contextmetOK2xml cI chd end
|
wneuper@59140
|
657 |
) handle _ => sysERROR2xml cI "error in kernel 36")
|
wneuper@59137
|
658 |
| str => sysERROR2xml cI ("checkContext: str = " ^ str)
|
neuper@37906
|
659 |
|
walther@59909
|
660 |
(*
|
walther@59909
|
661 |
for an Error_Pattern.id find "(fill_in_id * fill_in) list"
|
walther@59909
|
662 |
which is applicable to the current formula.
|
walther@59909
|
663 |
*)
|
s1210629013@55402
|
664 |
fun findFillpatterns cI errpatID =
|
neuper@42430
|
665 |
let
|
neuper@42430
|
666 |
val ((pt, _), _) = get_calc cI
|
wneuper@59260
|
667 |
val pos = get_pos cI 1;
|
walther@59909
|
668 |
val fillpats = Error_Pattern.find_fill_patterns (pt, pos) errpatID
|
wneuper@59260
|
669 |
in findFillpatterns2xml cI (map #1 fillpats) end
|
neuper@42432
|
670 |
|
neuper@42432
|
671 |
(* given a fillpatID propose a fillform to the learner on the worksheet;
|
neuper@42433
|
672 |
the "ctree" is extended with fillpat and "ostate Inconsistent",
|
neuper@42433
|
673 |
the "istate" is copied and NOT updated;
|
neuper@42432
|
674 |
returns CalcChanged.
|
neuper@42432
|
675 |
arg errpatID: required because there is no dialog-related state in the math-kernel.
|
neuper@42432
|
676 |
*)
|
neuper@42432
|
677 |
fun requestFillformula cI (errpatID, fillpatID) =
|
neuper@42432
|
678 |
let
|
neuper@42432
|
679 |
val ((pt, _), _) = get_calc cI
|
neuper@42436
|
680 |
val pos = get_pos cI 1
|
walther@59909
|
681 |
val fillforms = Error_Pattern.find_fill_patterns (pt, pos) errpatID
|
neuper@42432
|
682 |
in
|
s1210629013@55402
|
683 |
case filter ((curry op = fillpatID) o
|
walther@59911
|
684 |
(#1: (Error_Pattern_Def.fill_in_id * term * thm * (Subst.input option) -> Error_Pattern_Def.fill_in_id))) fillforms of
|
neuper@42434
|
685 |
(_, fillform, thm, sube_opt) :: _ =>
|
neuper@42432
|
686 |
let
|
walther@59959
|
687 |
val (pt, pos') = Step.inconsistent (sube_opt, ThmC.of_thm thm)
|
neuper@42437
|
688 |
fillform (get_loc pt pos) pos pt
|
neuper@42432
|
689 |
in
|
neuper@42432
|
690 |
(upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
|
neuper@42432
|
691 |
autocalculateOK2xml cI pos pos' pos')
|
neuper@42432
|
692 |
end
|
s1210629013@55402
|
693 |
| _ => autocalculateERROR2xml cI "no fillpattern found"
|
s1210629013@55402
|
694 |
end;
|
neuper@37906
|
695 |
|
neuper@42437
|
696 |
(* input a formula which exactly fills the gaps in a "fillformula"
|
neuper@42437
|
697 |
presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":
|
neuper@42437
|
698 |
errpatID: lhs of the respective thm = lhs of fillformula with fillpatID.
|
neuper@42437
|
699 |
The respective thm is stored in the ctree. *)
|
neuper@42437
|
700 |
fun inputFillFormula cI ifo =
|
neuper@42437
|
701 |
let
|
neuper@42437
|
702 |
val ((pt, _), _) = get_calc cI
|
neuper@42437
|
703 |
val pos = get_pos cI 1;
|
neuper@42437
|
704 |
in
|
walther@59909
|
705 |
case Error_Pattern.filled_exactly (pt, pos) ifo of
|
neuper@42437
|
706 |
("ok", tac) =>
|
neuper@42437
|
707 |
let
|
neuper@42437
|
708 |
in (* cp from applyTactic *)
|
walther@59804
|
709 |
case Step.by_tactic tac (pt, pos) of
|
neuper@42437
|
710 |
("ok", (_, c, ptp as (_,p'))) =>
|
neuper@42437
|
711 |
(upd_calc cI (ptp, []);
|
neuper@42437
|
712 |
upd_ipos cI 1 p';
|
neuper@42437
|
713 |
autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
|
neuper@42437
|
714 |
| ("unsafe-ok", (_, c, ptp as (_,p'))) =>
|
neuper@42437
|
715 |
(upd_calc cI (ptp, []);
|
neuper@42437
|
716 |
upd_ipos cI 1 p';
|
neuper@42437
|
717 |
autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
|
neuper@42437
|
718 |
| ("end-of-calculation", (_, c, ptp as (_,p'))) =>
|
neuper@42437
|
719 |
(upd_calc cI (ptp, []);
|
neuper@42437
|
720 |
upd_ipos cI 1 p';
|
neuper@42437
|
721 |
autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
|
wneuper@59260
|
722 |
| _ => autocalculateERROR2xml cI "failure"
|
neuper@42437
|
723 |
end
|
wneuper@59138
|
724 |
| (msg, _) => message2xml cI msg
|
wneuper@59260
|
725 |
end
|
walther@59613
|
726 |
|
walther@59613
|
727 |
(**)end(**)
|