1.1 --- a/src/Tools/isac/Interpret/script.sml Wed May 18 09:45:45 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Wed May 18 10:20:11 2011 +0200
1.3 @@ -1218,72 +1218,40 @@
1.4 NotLocatable: thus generate_hard
1.5 *)
1.6 fun locate_gen (thy',_) (Rewrite'(_,ro,er,pa,(id,str),f,_)) (pt,p)
1.7 - (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts), ctxt) =
1.8 - (case lo rss f (Thm (id, mk_thm (assoc_thy thy') str)) of
1.9 - [] => NotLocatable
1.10 + (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts), ctxt) =
1.11 + (case lo rss f (Thm (id, mk_thm (assoc_thy thy') str)) of
1.12 + [] => NotLocatable
1.13 | rts' =>
1.14 - Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
1.15 + Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
1.16
1.17 | locate_gen (ts as (thy',srls)) (m:tac_) ((pt,p):ptree * pos')
1.18 - (scr as Script (h $ body),d) (ScrState (E,l,a,v,S,b), ctxt) =
1.19 - let (*val _= tracing("### locate_gen-----------------: is=");
1.20 - val _= tracing( istate2str (ScrState (E,l,a,v,S,b)));
1.21 - val _= tracing("### locate_gen: l= "^loc_2str l^", p= "^pos'2str p)*)
1.22 - val thy = assoc_thy thy';
1.23 - in case if l=[] orelse ((*init.in solve..Apply_Method...*)
1.24 - (last_elem o fst) p = 0 andalso snd p = Res)
1.25 - then (assy ((ts,d),Aundef) ((E,[R],a,v,S,b),
1.26 - [(m,EmptyMout,pt,p,[])]) body)
1.27 -(* val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =
1.28 - (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b),[(m,EmptyMout,pt,p,[])]));
1.29 - (assy ((ts,d),Aundef) ((E,[R],a,v,S,b),[(m,EmptyMout,pt,p,[])]) body);
1.30 - *)
1.31 - else (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b),
1.32 - [(m,EmptyMout,pt,p,[])]) ) of
1.33 - Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =>
1.34 -(* val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =
1.35 - (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b),
1.36 - [(m,EmptyMout,pt,p,[])]) );
1.37 - *)
1.38 - ((*tracing("### locate_gen Assoc: p'="^(pos'2str p'));*)
1.39 - if bb then Steps (ScrState is, ss)
1.40 - else if rew_only ss (*andalso 'not bb'= associated weakly*)
1.41 - then let val (po,p_) = p
1.42 + (scr as Script (h $ body),d) (ScrState (E,l,a,v,S,b), ctxt) =
1.43 + let val thy = assoc_thy thy';
1.44 + in
1.45 + case if l = [] orelse ((*init.in solve..Apply_Method...*)
1.46 + (last_elem o fst) p = 0 andalso snd p = Res)
1.47 + then (assy ((ts,d),Aundef) ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]) body)
1.48 + else (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) of
1.49 + Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =>
1.50 + (if bb
1.51 + then Steps (ScrState is, ss)
1.52 + else
1.53 + if rew_only ss (*andalso 'not bb'= associated weakly*)
1.54 + then
1.55 + let
1.56 + val (po,p_) = p
1.57 val po' = case p_ of Frm => po | Res => lev_on po
1.58 - (*WN.12.03: noticed, that pos is also updated in assy !?!
1.59 - instead take p' from Assoc ?????????????????????????????*)
1.60 - val (p'',c'',f'',pt'') =
1.61 - generate1 thy m (ScrState is, ctxt) (po',p_) pt;
1.62 - (*val _=tracing("### locate_gen, aft g1: p''="^(pos'2str p''));*)
1.63 - (*drop the intermediate steps !*)
1.64 - in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
1.65 - else Steps (ScrState is, ss))
1.66 + val (p'',c'',f'',pt'') =
1.67 + generate1 thy m (ScrState is, ctxt) (po',p_) pt;
1.68 + in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
1.69 + else Steps (ScrState is, ss))
1.70
1.71 - | NasApp _ (*[((E,l,a,v,S,bb),(m',f',pt',p',c'))] =>
1.72 - error ("locate_gen: should not have got NasApp, ets =")*)
1.73 - => NotLocatable
1.74 - | NasNap (_,_) =>
1.75 - if l=[] then NotLocatable
1.76 - else (*scan from begin of script for rew_only*)
1.77 - (case assy ((ts,d),Aundef) ((E,[R],a,v,Unsafe,b),
1.78 - [(m,EmptyMout,pt,p,[])]) body of
1.79 - Assoc (iss as (is as (_,_,_,_,_,bb),
1.80 - ss as ((m',f',pt',p',c')::_))) =>
1.81 - ((*tracing"4### locate_gen Assoc after Fini";*)
1.82 - if rew_only ss
1.83 - then let val(p'',c'',f'',pt'') =
1.84 - generate1 thy m (ScrState is, ctxt) p' pt;
1.85 - (*drop the intermediate steps !*)
1.86 - in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
1.87 - else NotLocatable)
1.88 - | _ => ((*tracing ("#### locate_gen: after Fini");*)
1.89 - NotLocatable))
1.90 - end
1.91 + | NasApp _ => NotLocatable
1.92 + end
1.93 +
1.94 | locate_gen _ m _ (sc,_) (is, _) =
1.95 - error ("locate_gen: wrong arguments,\n tac= "^(tac_2str m)^
1.96 - ",\n scr= "^(scr2str sc)^",\n istate= "^(istate2str is));
1.97 -
1.98 -
1.99 + error ("locate_gen: wrong arguments,\n tac= " ^ tac_2str m ^ ",\n " ^
1.100 + "scr= " ^ scr2str sc ^ ",\n istate= " ^ istate2str is);
1.101
1.102 (** find the next stactic in a script **)
1.103