88 fun tac'_2str ((ID,ms):tac'_) = ID ^ (tac2str ms); |
88 fun tac'_2str ((ID,ms):tac'_) = ID ^ (tac2str ms); |
89 (* TODO: tac2str, tac'_2str NOT tested *) |
89 (* TODO: tac2str, tac'_2str NOT tested *) |
90 |
90 |
91 |
91 |
92 |
92 |
93 type squ = ptree; (* TODO: safe etc. *) |
93 type squ = ctree; (* TODO: safe etc. *) |
94 |
94 |
95 (*13.9.02-------------- |
95 (*13.9.02-------------- |
96 type ctr = (loc * pos) list; |
96 type ctr = (loc * pos) list; |
97 val ops = [("PLUS","Groups.plus_class.plus"),("MINUS","Groups.minus_class.minus"),("TIMES","Groups.times_class.times"), |
97 val ops = [("PLUS","Groups.plus_class.plus"),("MINUS","Groups.minus_class.minus"),("TIMES","Groups.times_class.times"), |
98 ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")]; |
98 ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")]; |
142 |
142 |
143 (*FIXME.WN050821 compare solve ... nxt_solv*) |
143 (*FIXME.WN050821 compare solve ... nxt_solv*) |
144 (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m); |
144 (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m); |
145 val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos); |
145 val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos); |
146 *) |
146 *) |
147 fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ptree, (pos as (p,_))) = |
147 fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ctree, (pos as (p,_))) = |
148 let val {srls, ...} = Specify.get_met mI; |
148 let val {srls, ...} = Specify.get_met mI; |
149 val PblObj {meth=itms, ...} = get_obj I pt p; |
149 val PblObj {meth=itms, ...} = get_obj I pt p; |
150 val thy' = get_obj g_domID pt p; |
150 val thy' = get_obj g_domID pt p; |
151 val thy = assoc_thy thy'; |
151 val thy = assoc_thy thy'; |
152 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = Lucin.init_scrstate thy itms mI; |
152 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = Lucin.init_scrstate thy itms mI; |
232 | solve (_,End_Detail' t) (pt, (p,p_)) = |
232 | solve (_,End_Detail' t) (pt, (p,p_)) = |
233 let |
233 let |
234 val pr as (p',_) = (lev_up p, Res) |
234 val pr as (p',_) = (lev_up p, Res) |
235 val pp = par_pblobj pt p |
235 val pp = par_pblobj pt p |
236 val r = (fst o (get_obj g_result pt)) p' |
236 val r = (fst o (get_obj g_result pt)) p' |
237 (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*) |
237 (*Rewrite_Set* done at Detail_Set*: this result is already in ctree*) |
238 val thy' = get_obj g_domID pt pp |
238 val thy' = get_obj g_domID pt pp |
239 val (srls, is, sc) = Lucin.from_pblobj' thy' pr pt |
239 val (srls, is, sc) = Lucin.from_pblobj' thy' pr pt |
240 val (tac_,is',_) = Lucin.next_tac (thy',srls) (pt,pr) sc is |
240 val (tac_,is',_) = Lucin.next_tac (thy',srls) (pt,pr) sc is |
241 in ("ok", ([(End_Detail, End_Detail' t , |
241 in ("ok", ([(End_Detail, End_Detail' t , |
242 ((p,p_), get_loc pt (p,p_)))], [], (pt,pr))) |
242 ((p,p_), get_loc pt (p,p_)))], [], (pt,pr))) |
272 end |
272 end |
273 end; |
273 end; |
274 |
274 |
275 (*FIXME.WN050821 compare fun solve ... fun nxt_solv*) |
275 (*FIXME.WN050821 compare fun solve ... fun nxt_solv*) |
276 (* nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *) |
276 (* nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *) |
277 fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) = |
277 fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ctree, pos as (p,_)) = |
278 let |
278 let |
279 val {srls,ppc,...} = Specify.get_met mI; |
279 val {srls,ppc,...} = Specify.get_met mI; |
280 val PblObj{meth=itms,origin=(oris,_,_),probl, ...} = get_obj I pt p; |
280 val PblObj{meth=itms,origin=(oris,_,_),probl, ...} = get_obj I pt p; |
281 val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc |
281 val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc |
282 val thy' = get_obj g_domID pt p; |
282 val thy' = get_obj g_domID pt p; |
352 | (p, Res) => (lev_on p,Res) (*somewhere in script*) |
352 | (p, Res) => (lev_on p,Res) (*somewhere in script*) |
353 | _ => pos |
353 | _ => pos |
354 val (pos',c,_,pt) = Generate.generate1 (assoc_thy "Isac") tac_ is pos pt; |
354 val (pos',c,_,pt) = Generate.generate1 (assoc_thy "Isac") tac_ is pos pt; |
355 in ([(Lucin.tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end |
355 in ([(Lucin.tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end |
356 |
356 |
357 (* find the next tac from the script, nxt_solv will update the ptree *) |
357 (* find the next tac from the script, nxt_solv will update the ctree *) |
358 and nxt_solve_ (ptp as (pt, pos as (p,p_))) = |
358 and nxt_solve_ (ptp as (pt, pos as (p,p_))) = |
359 if e_metID = get_obj g_metID pt (par_pblobj pt p) |
359 if e_metID = get_obj g_metID pt (par_pblobj pt p) |
360 then ([], [], (pt, (p, p_))) : Chead.calcstate' |
360 then ([], [], (pt, (p, p_))) : Chead.calcstate' |
361 else |
361 else |
362 let |
362 let |
388 | autoord CompleteCalcHead = 3 |
388 | autoord CompleteCalcHead = 3 |
389 | autoord CompleteToSubpbl = 4 |
389 | autoord CompleteToSubpbl = 4 |
390 | autoord CompleteSubpbl = 5 |
390 | autoord CompleteSubpbl = 5 |
391 | autoord CompleteCalc = 6; |
391 | autoord CompleteCalc = 6; |
392 |
392 |
393 fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') = |
393 fun complete_solve auto c (ptp as (_, p as (_,p_)): ctree * pos') = |
394 if p = ([], Res) |
394 if p = ([], Res) |
395 then ("end-of-calculation", [], ptp) |
395 then ("end-of-calculation", [], ptp) |
396 else |
396 else |
397 if member op = [Pbl,Met] p_ |
397 if member op = [Pbl,Met] p_ |
398 then |
398 then |
418 if autoord auto < 6 |
418 if autoord auto < 6 |
419 then ("ok", c @ c', ptp') |
419 then ("ok", c @ c', ptp') |
420 else complete_solve auto (c @ c') ptp' |
420 else complete_solve auto (c @ c') ptp' |
421 | (_, c', ptp') => complete_solve auto (c @ c') ptp' |
421 | (_, c', ptp') => complete_solve auto (c @ c') ptp' |
422 |
422 |
423 and all_solve auto c (ptp as (pt, pos as (p,_)): ptree * pos') = |
423 and all_solve auto c (ptp as (pt, pos as (p,_)): ctree * pos') = |
424 let |
424 let |
425 val (_,_,mI) = get_obj g_spec pt p |
425 val (_,_,mI) = get_obj g_spec pt p |
426 val ctxt = get_ctxt pt pos |
426 val ctxt = get_ctxt pt pos |
427 val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp |
427 val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp |
428 in complete_solve auto (c @ c') ptp end; |
428 in complete_solve auto (c @ c') ptp end; |