53 tacis; (*= []*) |
53 tacis; (*= []*) |
54 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*) |
54 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*) |
55 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); |
55 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); |
56 val thy' = get_obj g_domID pt (par_pblobj pt p); |
56 val thy' = get_obj g_domID pt (par_pblobj pt p); |
57 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*) |
57 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*) |
58 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), (sc as Script (h $ body)), |
58 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), (sc as Prog (h $ body)), |
59 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); |
59 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); |
60 val ctxt = get_ctxt pt pos |
60 val ctxt = get_ctxt pt pos |
61 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; |
61 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; |
62 l; (*= [R, R, D, L, R]*) |
62 l; (*= [R, R, D, L, R]*) |
63 "~~~~~ fun nstep_up, args:"; val (thy, ptp, (Script sc), E, l, ay, a, v) = |
63 "~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = |
64 (thy, ptp, sc, E, l, Skip_, a, v); |
64 (thy, ptp, sc, E, l, Skip_, a, v); |
65 1 < length l; (*true*) |
65 1 < length l; (*true*) |
66 val up = drop_last l; |
66 val up = drop_last l; |
67 go up sc; (* = Const ("HOL.Let", *) |
67 go up sc; (* = Const ("HOL.Let", *) |
68 "~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Script sc)), E, l, ay, |
68 "~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Prog sc)), E, l, ay, |
69 (t as Const ("HOL.Let",_) $ _), a, v) = |
69 (t as Const ("HOL.Let",_) $ _), a, v) = |
70 (thy, ptp, (Script sc), E, up, ay, (go up sc), a, v); |
70 (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v); |
71 ay = Napp_; (*false*) |
71 ay = Napp_; (*false*) |
72 val up = drop_last l; |
72 val up = drop_last l; |
73 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc; |
73 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc; |
74 val i = mk_Free (i, T); |
74 val i = mk_Free (i, T); |
75 val E = upd_env E (i, v); |
75 val E = upd_env E (i, v); |