90 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
90 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
92 val (p''',_,f,nxt''',_,pt''') = me nxt p [1] pt; |
92 val (p''',_,f,nxt''',_,pt''') = me nxt p [1] pt; |
93 f2str f = "[x = 1 / 5]"; |
93 f2str f = "[x = 1 / 5]"; |
94 case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => () | _ => ((*not checked before*)); |
94 case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => () | _ => ((*not checked before*)); |
95 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt); |
95 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt); |
96 val (pt, p) = case locatetac tac (pt,p) of |
96 val (pt, p) = case locatetac tac (pt,p) of |
97 ("ok", (_, _, ptp)) => ptp | _ => error "--- solve (1/x = 5.. locatetac"; |
97 ("ok", (_, _, ptp)) => ptp | _ => error "--- solve (1/x = 5.. locatetac"; |
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 nxt_solve_, 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 next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), |
106 "~~~~~ fun next_tac, 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); |
109 "~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = |
109 "~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = |
110 (thy, ptp, sc, E, l, Skip_, a, v); |
110 (thy, ptp, sc, E, l, Skip_, a, v); |
111 1 < length l; (*true*) |
111 1 < length l; (*true*) |
277 |
277 |
278 The step-into-source contains an error; this error can be detected by |
278 The step-into-source contains an error; this error can be detected by |
279 test --- 'trace_script' from outside 'fun me '--- |
279 test --- 'trace_script' from outside 'fun me '--- |
280 *) |
280 *) |
281 val (pt''', p''') = (pt, p); |
281 val (pt''', p''') = (pt, p); |
282 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt); |
282 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt); |
283 val (pt, p) = case locatetac tac (pt,p) of |
283 val (pt, p) = case locatetac tac (pt,p) of |
284 ("ok", (_, _, ptp)) => ptp | _ => error "error in test setup"; |
284 ("ok", (_, _, ptp)) => ptp | _ => error "error in test setup"; |
285 "~~~~~ step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = |
285 "~~~~~ step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = |
286 (p, ((pt, e_pos'),[])); |
286 (p, ((pt, e_pos'),[])); |
287 val pIopt = get_pblID (pt,ip); |
287 val pIopt = get_pblID (pt,ip); |
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 nxt_solve_, 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 next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), |
295 "~~~~~ fun next_tac, 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); |
297 l = []; (* = false*) |
297 l = []; (* = false*) |
298 "~~~~~ and nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = |
298 "~~~~~ and nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = |
299 (thy, ptp, sc, E, l, Skip_, a, v); |
299 (thy, ptp, sc, E, l, Skip_, a, v); |
300 1 < length l; (* = true*) |
300 1 < length l; (* = true*) |