164 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
164 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
165 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
165 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
166 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
166 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
167 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*) |
167 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*) |
168 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*) |
168 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*) |
169 "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt); |
169 "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt); |
170 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p)); |
170 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p)); |
171 val (mI,m) = mk_tac'_ tac; |
171 val (mI,m) = mk_tac'_ tac; |
172 val Appl m = applicable_in p pt m; |
172 val Appl m = applicable_in p pt m; |
173 val Check_elementwise' (trm1, str, (trm2, trms)) = m; |
173 val Check_elementwise' (trm1, str, (trm2, trms)) = m; |
174 term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]"; |
174 term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]"; |
192 val thy' = get_obj g_domID pt (par_pblobj pt p); |
192 val thy' = get_obj g_domID pt (par_pblobj pt p); |
193 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
193 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
194 val d = e_rls; |
194 val d = e_rls; |
195 (*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is; |
195 (*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is; |
196 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*) |
196 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*) |
197 "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'), |
197 "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), |
198 (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = |
198 (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = |
199 ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *) |
199 ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *) |
200 val thy = assoc_thy thy'; |
200 val thy = assoc_thy thy'; |
201 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*); |
201 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*); |
202 (*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) |
202 (*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) |
214 val l = drop_last l; (*comes from e, goes to Abs*) |
214 val l = drop_last l; (*comes from e, goes to Abs*) |
215 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc; |
215 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc; |
216 val i = mk_Free (i, T); |
216 val i = mk_Free (i, T); |
217 val E = upd_env E (i, v); |
217 val E = upd_env E (i, v); |
218 (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*) |
218 (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*) |
219 val [(tac_, mout, ptree, pos', xxx)] = ss; |
219 val [(tac_, mout, ctree, pos', xxx)] = ss; |
220 val ss = [(tac_, mout, ptree, pos', []:(pos * pos_) list)]; |
220 val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)]; |
221 (*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body |
221 (*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body |
222 ... Assoc ... is correct*) |
222 ... Assoc ... is correct*) |
223 "~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) = |
223 "~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) = |
224 ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body); |
224 ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body); |
225 val (a', STac stac) = handle_leaf "locate" thy' sr E a v t |
225 val (a', STac stac) = handle_leaf "locate" thy' sr E a v t |