93 type ctr = (loc * pos) list; |
93 type ctr = (loc * pos) list; |
94 val ops = [("PLUS","op +"),("minus","op -"),("TIMES","op *"), |
94 val ops = [("PLUS","op +"),("minus","op -"),("TIMES","op *"), |
95 ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")]; |
95 ("cancel","cancel"),("pow","pow"),("sqrt","sqrt")]; |
96 fun op_intern op_ = |
96 fun op_intern op_ = |
97 case assoc (ops,op_) of |
97 case assoc (ops,op_) of |
98 Some op' => op' | None => raise error ("op_intern: no op= "^op_); |
98 SOME op' => op' | NONE => raise error ("op_intern: no op= "^op_); |
99 -----------------------*) |
99 -----------------------*) |
100 |
100 |
101 |
101 |
102 |
102 |
103 (* use"ME/solve.sml"; |
103 (* use"ME/solve.sml"; |
137 val (is as ScrState (env,_,_,_,_,_), sc) = init_scrstate thy itms mI; |
137 val (is as ScrState (env,_,_,_,_,_), sc) = init_scrstate thy itms mI; |
138 val ini = init_form thy sc env; |
138 val ini = init_form thy sc env; |
139 val p = lev_dn p; |
139 val p = lev_dn p; |
140 in |
140 in |
141 case ini of |
141 case ini of |
142 Some t => (* val Some t = ini; |
142 SOME t => (* val SOME t = ini; |
143 *) |
143 *) |
144 let val (pos,c,_,pt) = |
144 let val (pos,c,_,pt) = |
145 generate1 thy (Apply_Method' (mI, Some t, is)) |
145 generate1 thy (Apply_Method' (mI, SOME t, is)) |
146 is (lev_on p, Frm)(*implicit Take*) pt; |
146 is (lev_on p, Frm)(*implicit Take*) pt; |
147 in ("ok",([(Apply_Method mI, Apply_Method' (mI, Some t, is), |
147 in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is), |
148 ((lev_on p, Frm), is))], c, (pt,pos)):calcstate') |
148 ((lev_on p, Frm), is))], c, (pt,pos)):calcstate') |
149 end |
149 end |
150 | None => (*execute the first tac in the Script, compare solve m*) |
150 | NONE => (*execute the first tac in the Script, compare solve m*) |
151 let val (m', is', _) = next_tac (thy', srls) (pt, (p, Res)) sc is; |
151 let val (m', is', _) = next_tac (thy', srls) (pt, (p, Res)) sc is; |
152 val d = e_rls (*FIXME: get simplifier from domID*); |
152 val d = e_rls (*FIXME: get simplifier from domID*); |
153 in |
153 in |
154 case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) is' of |
154 case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) is' of |
155 Steps (is'', ss as (m'',f',pt',p',c')::_) => |
155 Steps (is'', ss as (m'',f',pt',p',c')::_) => |
161 let val (p,ps,f,pt) = |
161 let val (p,ps,f,pt) = |
162 generate_hard (assoc_thy "Isac.thy") m (p,Frm) pt; |
162 generate_hard (assoc_thy "Isac.thy") m (p,Frm) pt; |
163 in ("not-found-in-script", |
163 in ("not-found-in-script", |
164 ([(tac_2tac m, m, (pos, is))], ps, (pt,p))) end |
164 ([(tac_2tac m, m, (pos, is))], ps, (pt,p))) end |
165 (*just-before------------------------------------------------------ |
165 (*just-before------------------------------------------------------ |
166 ("ok",([(Apply_Method mI,Apply_Method'(mI,None,e_istate), |
166 ("ok",([(Apply_Method mI,Apply_Method'(mI,NONE,e_istate), |
167 (pos, is))], |
167 (pos, is))], |
168 [], (update_env pt (fst pos) (Some is),pos))) |
168 [], (update_env pt (fst pos) (SOME is),pos))) |
169 -----------------------------------------------------------------*) |
169 -----------------------------------------------------------------*) |
170 end |
170 end |
171 end |
171 end |
172 |
172 |
173 | solve ("Free_Solve", Free_Solve') (pt,po as (p,_)) = |
173 | solve ("Free_Solve", Free_Solve') (pt,po as (p,_)) = |
302 |
302 |
303 (*FIXME.WN050821 compare solve ... nxt_solv*) |
303 (*FIXME.WN050821 compare solve ... nxt_solv*) |
304 (* nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *) |
304 (* nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *) |
305 fun nxt_solv (Apply_Method' (mI,_,_)) _ (pt:ptree, pos as (p,_)) = |
305 fun nxt_solv (Apply_Method' (mI,_,_)) _ (pt:ptree, pos as (p,_)) = |
306 (* val ((Apply_Method' (mI,_,_)), _, (pt:ptree, pos as (p,_))) = |
306 (* val ((Apply_Method' (mI,_,_)), _, (pt:ptree, pos as (p,_))) = |
307 ((Apply_Method' (mI, None, e_istate)), e_istate, ptp); |
307 ((Apply_Method' (mI, NONE, e_istate)), e_istate, ptp); |
308 *) |
308 *) |
309 let val {srls,ppc,...} = get_met mI; |
309 let val {srls,ppc,...} = get_met mI; |
310 val PblObj{meth=itms,origin=(oris,_,_),probl,...} = get_obj I pt p; |
310 val PblObj{meth=itms,origin=(oris,_,_),probl,...} = get_obj I pt p; |
311 val itms = if itms <> [] then itms |
311 val itms = if itms <> [] then itms |
312 else complete_metitms oris probl [] ppc |
312 else complete_metitms oris probl [] ppc |
314 val thy = assoc_thy thy'; |
314 val thy = assoc_thy thy'; |
315 val (is as ScrState (env,_,_,_,_,_), scr) = init_scrstate thy itms mI; |
315 val (is as ScrState (env,_,_,_,_,_), scr) = init_scrstate thy itms mI; |
316 val ini = init_form thy scr env; |
316 val ini = init_form thy scr env; |
317 in |
317 in |
318 case ini of |
318 case ini of |
319 Some t => (* val Some t = ini; |
319 SOME t => (* val SOME t = ini; |
320 *) |
320 *) |
321 let val pos = ((lev_on o lev_dn) p, Frm) |
321 let val pos = ((lev_on o lev_dn) p, Frm) |
322 val tac_ = Apply_Method' (mI, Some t, is); |
322 val tac_ = Apply_Method' (mI, SOME t, is); |
323 val (pos,c,_,pt) = (*implicit Take*) |
323 val (pos,c,_,pt) = (*implicit Take*) |
324 generate1 thy tac_ is pos pt |
324 generate1 thy tac_ is pos pt |
325 (*val _= ("### nxt_solv Apply_Method, pos= "^pos'2str (lev_on p,Frm));*) |
325 (*val _= ("### nxt_solv Apply_Method, pos= "^pos'2str (lev_on p,Frm));*) |
326 in ([(Apply_Method mI, tac_, (pos, is))], c, (pt, pos)):calcstate' end |
326 in ([(Apply_Method mI, tac_, (pos, is))], c, (pt, pos)):calcstate' end |
327 | None => |
327 | NONE => |
328 let val pt = update_env pt (fst pos) (Some is) |
328 let val pt = update_env pt (fst pos) (SOME is) |
329 val (tacis, c, ptp) = nxt_solve_ (pt, pos) |
329 val (tacis, c, ptp) = nxt_solve_ (pt, pos) |
330 in (tacis @ |
330 in (tacis @ |
331 [(Apply_Method mI, Apply_Method' (mI, None, e_istate), (pos, is))], |
331 [(Apply_Method mI, Apply_Method' (mI, NONE, e_istate), (pos, is))], |
332 c, ptp) end |
332 c, ptp) end |
333 end |
333 end |
334 (* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m); |
334 (* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m); |
335 val (Check_Postcond' (pI,_), _, (pt, pos as (p,p_))) = |
335 val (Check_Postcond' (pI,_), _, (pt, pos as (p,p_))) = |
336 (tac_, is, ptp); |
336 (tac_, is, ptp); |
487 (* val (ptp as (pt, (p,_))) = ptp; |
487 (* val (ptp as (pt, (p,_))) = ptp; |
488 val (ptp as (pt, (p,_))) = ptp'; |
488 val (ptp as (pt, (p,_))) = ptp'; |
489 val (ptp as (pt, (p,_))) = (pt, pos); |
489 val (ptp as (pt, (p,_))) = (pt, pos); |
490 *) |
490 *) |
491 let val (_,_,mI) = get_obj g_spec pt p; |
491 let val (_,_,mI) = get_obj g_spec pt p; |
492 val (_, c', ptp) = nxt_solv (Apply_Method' (mI, None, e_istate)) |
492 val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate)) |
493 e_istate ptp; |
493 e_istate ptp; |
494 in complete_solve auto (c@c') ptp end; |
494 in complete_solve auto (c@c') ptp end; |
495 (*@@@ vvv @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*) |
495 (*@@@ vvv @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*) |
496 fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') = |
496 fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') = |
497 if p = ([], Res) then ("end-of-calculation", [], ptp) else |
497 if p = ([], Res) then ("end-of-calculation", [], ptp) else |
512 if autoord auto < 6 then ("ok", c@c', ptp') |
512 if autoord auto < 6 then ("ok", c@c', ptp') |
513 else complete_solve auto (c@c') ptp' |
513 else complete_solve auto (c@c') ptp' |
514 | (_, c', ptp') => complete_solve auto (c@c') ptp' |
514 | (_, c', ptp') => complete_solve auto (c@c') ptp' |
515 and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') = |
515 and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') = |
516 let val (_,_,mI) = get_obj g_spec pt p |
516 let val (_,_,mI) = get_obj g_spec pt p |
517 val (_, c', ptp) = nxt_solv (Apply_Method' (mI, None, e_istate)) |
517 val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate)) |
518 e_istate ptp |
518 e_istate ptp |
519 in complete_solve auto (c@c') ptp end; |
519 in complete_solve auto (c@c') ptp end; |
520 |
520 |
521 (*.aux.fun for detailrls with Rrls, reverse rewriting.*) |
521 (*.aux.fun for detailrls with Rrls, reverse rewriting.*) |
522 (* val (nds, t, ((rule, (t', asm)) :: rts)) = ([], t, rul_terms); |
522 (* val (nds, t, ((rule, (t', asm)) :: rts)) = ([], t, rul_terms); |
546 | _ => |
546 | _ => |
547 let val is = init_istate tac t |
547 let val is = init_istate tac t |
548 (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"] |
548 (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"] |
549 is wrong for simpl, but working ?!? *) |
549 is wrong for simpl, but working ?!? *) |
550 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), |
550 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), |
551 Some t, is) |
551 SOME t, is) |
552 val pos' = ((lev_on o lev_dn) p, Frm) |
552 val pos' = ((lev_on o lev_dn) p, Frm) |
553 val thy = assoc_thy "Isac.thy" |
553 val thy = assoc_thy "Isac.thy" |
554 val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ is pos' pt |
554 val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ is pos' pt |
555 val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos') |
555 val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos') |
556 val newnds = children (get_nd pt'' p) |
556 val newnds = children (get_nd pt'' p) |