98 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) |
98 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) |
99 val pIopt = get_pblID (pt,ip); (*= SOME ["rational", "univariate", "equation"] |
99 val pIopt = get_pblID (pt,ip); (*= SOME ["rational", "univariate", "equation"] |
100 1-1 associated to metID ["RatEq", "solve_rat_equation"]*) |
100 1-1 associated to metID ["RatEq", "solve_rat_equation"]*) |
101 tacis; (*= []*) |
101 tacis; (*= []*) |
102 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*) |
102 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*) |
103 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); |
103 "~~~~~ fun do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); |
104 val thy' = get_obj g_domID pt (par_pblobj pt p); |
104 val thy' = get_obj g_domID pt (par_pblobj pt p); |
105 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*) |
105 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*) |
106 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), |
106 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), |
107 (sc as Prog (h $ body)), |
107 (sc as Prog (h $ body)), |
108 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); |
108 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); |
286 (p, ((pt, e_pos'),[])); |
286 (p, ((pt, e_pos'),[])); |
287 val pIopt = get_pblID (pt,ip); |
287 val pIopt = get_pblID (pt,ip); |
288 ip = ([],Res); (* = false*) |
288 ip = ([],Res); (* = false*) |
289 tacis; (* = []*) |
289 tacis; (* = []*) |
290 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (* = false*) |
290 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (* = false*) |
291 "~~~~~ and nxt_solve_, args:"; val ((ptp as (pt, pos as (p,p_)))) = ((pt,ip)); |
291 "~~~~~ and do_solve_step, args:"; val ((ptp as (pt, pos as (p,p_)))) = ((pt,ip)); |
292 e_metID = get_obj g_metID pt (par_pblobj pt p); (* = false*) |
292 e_metID = get_obj g_metID pt (par_pblobj pt p); (* = false*) |
293 val thy' = get_obj g_domID pt (par_pblobj pt p); |
293 val thy' = get_obj g_domID pt (par_pblobj pt p); |
294 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
294 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
295 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), |
295 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), |
296 (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); |
296 (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); |
317 nxt_up thy ptp (Prog sc) E up ay (go up sc) a v; |
317 nxt_up thy ptp (Prog sc) E up ay (go up sc) a v; |
318 nstep_up thy ptp scr E l ay a v; |
318 nstep_up thy ptp scr E l ay a v; |
319 nxt_up thy ptp (Prog sc) E up ay (go up sc) a v; |
319 nxt_up thy ptp (Prog sc) E up ay (go up sc) a v; |
320 nstep_up thy ptp sc E l Skip_ a v; |
320 nstep_up thy ptp sc E l Skip_ a v; |
321 determine_next_tactic (thy',srls) (pt,pos) sc is; |
321 determine_next_tactic (thy',srls) (pt,pos) sc is; |
322 nxt_solve_ (pt,ip); |
322 do_solve_step (pt,ip); |
323 step p ((pt, e_pos'),[]); |
323 step p ((pt, e_pos'),[]); |
324 *) |
324 *) |
325 val (p,_,f,nxt,_,pt) = me nxt p''' [1] pt'''; |
325 val (p,_,f,nxt,_,pt) = me nxt p''' [1] pt'''; |
326 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
326 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
327 |
327 |