61 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
61 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
62 |
62 |
63 case nxt of ("Rewrite_Set", Rewrite_Set "RatEq_eliminate") => () | _ => ((*not checked before*)); |
63 case nxt of ("Rewrite_Set", Rewrite_Set "RatEq_eliminate") => () | _ => ((*not checked before*)); |
64 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
64 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
65 (* |
65 (* |
66 WN120317.TODO dropped rateq: here "x ~= 0 should go to ctxt, but it does not: |
66 WN120317.TODO dropped rateq: here "x ~= 0 should at_location to ctxt, but it does not: |
67 --- repair NO asms from rls RatEq_eliminate --- shows why. |
67 --- repair NO asms from rls RatEq_eliminate --- shows why. |
68 so it needs more effort to find out, how Check_elementwise worked in 2002, see below. |
68 so it needs more effort to find out, how Check_elementwise worked in 2002, see below. |
69 *) |
69 *) |
70 |
70 |
71 (* val nxt = (_,Subproblem ("RatEq",["univariate","equation"] ======= *) |
71 (* val nxt = (_,Subproblem ("RatEq",["univariate","equation"] ======= *) |
107 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* ) |
107 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* ) |
108 "~~~~~ fun go_scan_up2, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = |
108 "~~~~~ fun go_scan_up2, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = |
109 (thy, ptp, sc, E, l, Skip_, a, v); |
109 (thy, ptp, sc, E, l, Skip_, a, v); |
110 1 < length l; (*true*) |
110 1 < length l; (*true*) |
111 val up = drop_last l; |
111 val up = drop_last l; |
112 go up sc; (* = Const ("HOL.Let", *) |
112 at_location up sc; (* = Const ("HOL.Let", *) |
113 "~~~~~ fun scan_up2, args:"; val (thy, ptp, (scr as (Prog sc)), E, l, ay, |
113 "~~~~~ fun scan_up2, args:"; val (thy, ptp, (scr as (Prog sc)), E, l, ay, |
114 (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v); |
114 (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Prog sc), E, up, ay, (at_location up sc), a, v); |
115 ay = Napp_; (*false*) |
115 ay = Napp_; (*false*) |
116 val up = drop_last l; |
116 val up = drop_last l; |
117 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc; (*Const ("Prog_Tac.SubProblem",..*) |
117 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = at_location up sc; (*Const ("Prog_Tac.SubProblem",..*) |
118 val i = mk_Free (i, T); |
118 val i = mk_Free (i, T); |
119 val E = Env.update E (i, v); |
119 val E = Env.update E (i, v); |
120 "~~~~~ fun scan_dn2, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v) = |
120 "~~~~~ fun scan_dn2, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v) = |
121 (thy, ptp, E, (up@[R,D]), body, a, v); |
121 (thy, ptp, E, (up@[R,D]), body, a, v); |
122 "~~~~~ fun interpret_leaf, args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (E, (a, v)), t); |
122 "~~~~~ fun interpret_leaf, args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (E, (a, v)), t); |
295 l = []; (* = false*) |
295 l = []; (* = false*) |
296 "~~~~~ and go_scan_up2, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = |
296 "~~~~~ and go_scan_up2, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = |
297 (thy, ptp, sc, E, l, Skip_, a, v); |
297 (thy, ptp, sc, E, l, Skip_, a, v); |
298 1 < length l; (* = true*) |
298 1 < length l; (* = true*) |
299 val up = drop_last l; |
299 val up = drop_last l; |
300 (*val (t as Abs (_,_,_)) = *)(go up sc); |
300 (*val (t as Abs (_,_,_)) = *)(at_location up sc); |
301 "~~~~~ fun scan_up2, args:"; val (thy, ptp, scr, E, l, ay, (t as Abs (_,_,_)), a, v) = |
301 "~~~~~ fun scan_up2, args:"; val (thy, ptp, scr, E, l, ay, (t as Abs (_,_,_)), a, v) = |
302 (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v); |
302 (thy, ptp, (Prog sc), E, up, ay, (at_location up sc), a, v); |
303 term2str t = "%L_La. Check_elementwise L_L {v_v. Assumptions}"; |
303 term2str t = "%L_La. Check_elementwise L_L {v_v. Assumptions}"; |
304 "~~~~~ and go_scan_up2, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = |
304 "~~~~~ and go_scan_up2, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = |
305 (thy, ptp, scr, E, l, ay, a, v); |
305 (thy, ptp, scr, E, l, ay, a, v); |
306 1 < length l; (* = true*) |
306 1 < length l; (* = true*) |
307 val up = drop_last l; |
307 val up = drop_last l; |
308 (*val (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) = *)(go up sc); |
308 (*val (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) = *)(at_location up sc); |
309 "~~~~~ fun scan_up2, args:"; val (thy, ptp, scr, E, l, ay, |
309 "~~~~~ fun scan_up2, args:"; val (thy, ptp, scr, E, l, ay, |
310 (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) = (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v); |
310 (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) = (thy, ptp, (Prog sc), E, up, ay, (at_location up sc), a, v); |
311 |
311 |
312 term2str t = "let L_La =\n SubProblem (RatEqX, [univariate, equation], [no_met])\n [BOOL e_e, REAL v_v]\nin Check_elementwise L_L {v_v. Assumptions}"; |
312 term2str t = "let L_La =\n SubProblem (RatEqX, [univariate, equation], [no_met])\n [BOOL e_e, REAL v_v]\nin Check_elementwise L_L {v_v. Assumptions}"; |
313 |
313 |
314 (* comment from BEFORE Isabelle2002 --> 2011: |
314 (* comment from BEFORE Isabelle2002 --> 2011: |
315 scan_up2 thy ptp (Prog sc) E up ay (go up sc) a v; |
315 scan_up2 thy ptp (Prog sc) E up ay (at_location up sc) a v; |
316 go_scan_up2 thy ptp scr E l ay a v; |
316 go_scan_up2 thy ptp scr E l ay a v; |
317 scan_up2 thy ptp (Prog sc) E up ay (go up sc) a v; |
317 scan_up2 thy ptp (Prog sc) E up ay (at_location up sc) a v; |
318 go_scan_up2 thy ptp sc E l Skip_ a v; |
318 go_scan_up2 thy ptp sc E l Skip_ a v; |
319 find_next_tactic sc (pt,pos) is (*is as (ist, ctxt) ---> ist ctxt*); |
319 find_next_tactic sc (pt,pos) is (*is as (ist, ctxt) ---> ist ctxt*); |
320 Step_Solve.do_next (pt,ip); |
320 Step_Solve.do_next (pt,ip); |
321 Step.do_next p ((pt, e_pos'),[]); |
321 Step.do_next p ((pt, e_pos'),[]); |
322 *) |
322 *) |