193 autoCalculate 1 CompleteCalcHead; |
193 autoCalculate 1 CompleteCalcHead; |
194 autoCalculate 1 (Step 1); |
194 autoCalculate 1 (Step 1); |
195 autoCalculate 1 (Step 1); |
195 autoCalculate 1 (Step 1); |
196 val ((pt, p), _) = get_calc 1; show_pt pt; |
196 val ((pt, p), _) = get_calc 1; show_pt pt; |
197 val appltacs = sel_appl_atomic_tacs pt p; |
197 val appltacs = sel_appl_atomic_tacs pt p; |
198 |
|
199 (*========== inhibit exn AK110721 ================================================ |
|
200 (*(*These SHOULD be the same*) |
|
201 print_depth(999); |
|
202 appltacs; |
|
203 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"), |
|
204 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"), |
|
205 Calculate "TIMES"];*) |
|
206 |
|
207 if appltacs = |
198 if appltacs = |
208 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"), |
199 (* WN130613 |
209 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"), |
200 [Rewrite ("radd_commute", "Test.radd_commute") (*"?m + ?n = ?n + ?m"*), |
210 Calculate "TIMES"] then () |
201 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"), Calculate "TIMES"] *) |
211 else error "script.sml fun sel_appl_atomic_tacs diff.behav."; |
202 [Rewrite ("radd_commute", "Test.radd_commute"), |
212 ========== inhibit exn AK110721 ================================================*) |
203 Rewrite ("add_assoc", "Groups.semigroup_add_class.add_assoc"), Calculate "TIMES"] |
|
204 then () else error "script.sml fun sel_appl_atomic_tacs diff.behav."; |
213 |
205 |
214 trace_script := true; |
206 trace_script := true; |
215 trace_script := false; |
207 trace_script := false; |
216 applyTactic 1 p (hd appltacs); |
208 applyTactic 1 p (hd appltacs); |
217 val ((pt, p), _) = get_calc 1; show_pt pt; |
209 val ((pt, p), _) = get_calc 1; show_pt pt; |
218 val appltacs = sel_appl_atomic_tacs pt p; |
210 val appltacs = sel_appl_atomic_tacs pt p; |
219 |
|
220 (*(* AK110722 Debugging start*) |
|
221 (*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*) |
211 (*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*) |
|
212 |
222 "~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs)); |
213 "~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs)); |
223 val ((pt, _), _) = get_calc cI; |
214 val ((pt, _), _) = get_calc cI; |
224 val p = get_pos cI 1; |
215 val p = get_pos cI 1; |
225 |
|
226 locatetac; |
216 locatetac; |
227 locatetac tac; |
|
228 locatetac tac; |
217 locatetac tac; |
229 |
218 |
230 (*locatetac tac (pt, ip); (*WAS assy: call by ([3], Pbl)*)*) |
219 (*locatetac tac (pt, ip); (*WAS assy: call by ([3], Pbl)*)*) |
231 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip)); |
220 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip)); |
232 val (mI,m) = mk_tac'_ tac; |
221 val (mI,m) = mk_tac'_ tac; |
233 |
|
234 applicable_in p pt m ; (*Appl*) |
222 applicable_in p pt m ; (*Appl*) |
235 |
|
236 member op = specsteps mI; (*false*) |
223 member op = specsteps mI; (*false*) |
237 |
|
238 (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*) |
224 (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*) |
239 loc_solve_; (*without _ ??? result is -> lOc writing error ???*) |
225 loc_solve_; (*without _ ??? result is -> lOc writing error ???*) |
240 (*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*) |
226 (*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*) |
241 (mI,m); (*string * tac*) |
227 (mI,m); (*string * tac*) |
242 ptp (*ptree * pos'*); |
228 ptp (*ptree * pos'*); |
243 |
|
244 "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp); |
229 "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp); |
245 (*val (msg, cs') = solve m (pt, pos); |
230 (*val (msg, cs') = solve m (pt, pos); |
246 (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*) |
231 (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*) |
247 |
|
248 m; |
232 m; |
249 (pt, pos); |
233 (pt, pos); |
250 |
|
251 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos)); |
234 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos)); |
252 (*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*) |
235 (*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*) |
253 |
236 |
254 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*) |
237 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*) |
255 val ctxt = get_ctxt pt po; |
238 val ctxt = get_ctxt pt po; |
256 |
239 |
257 (*generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt; |
240 (*generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt; |
258 (*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*) |
241 (*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*) |
259 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))); |
242 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))); |
260 assoc_thy; |
243 assoc_thy; |
261 |
|
262 (*not finished - error continues in fun generate1*) |
|
263 (* AK110722 Debugging end*)*) |
|
264 (*========== inhibit exn AK110721 ================================================ |
|
265 "----- WN080102 these vvv do not work, because locatetac starts the search" ^ |
|
266 "1 stac too low"; |
|
267 (* AK110722 ERROR: assy: call by ([3], Pbl) *) |
|
268 applyTactic 1 p (hd appltacs); |
|
269 ============ inhibit exn AK110721 ==============================================*) |
|
270 |
244 |
271 autoCalculate 1 CompleteCalc; |
245 autoCalculate 1 CompleteCalc; |
272 |
246 |
273 "----------- fun init_form, fun get_stac -------------------------"; |
247 "----------- fun init_form, fun get_stac -------------------------"; |
274 "----------- fun init_form, fun get_stac -------------------------"; |
248 "----------- fun init_form, fun get_stac -------------------------"; |