1.1 --- a/src/Tools/isac/Interpret/solve.sml Tue May 17 09:55:30 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/solve.sml Tue May 17 14:56:54 2011 +0200
1.3 @@ -232,140 +232,120 @@
1.4
1.5 | solve (_,End_Proof'') (pt, (p,p_)) =
1.6 ("end-proof",
1.7 - ((*(([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe,*)
1.8 - [(Empty_Tac,Empty_Tac_,(([],Res),(Uistate, e_ctxt)))],[],(pt,(p,p_))))
1.9 + ([(Empty_Tac,Empty_Tac_,(([],Res),(Uistate, e_ctxt)))],[],(pt,(p,p_))))
1.10
1.11 (*-----------vvvvvvvvvvv could be done by generate1 ?!?*)
1.12 - | solve (_,End_Detail' t) (pt,(p,p_)) =
1.13 - let val pr as (p',_) = (lev_up p, Res)
1.14 - val pp = par_pblobj pt p
1.15 - val r = (fst o (get_obj g_result pt)) p'
1.16 - (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
1.17 - val thy' = get_obj g_domID pt pp
1.18 - val (srls, is, sc) = from_pblobj' thy' pr pt
1.19 - val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
1.20 - in ("ok", ((*((pp,Frm(*???*)),is,tac_),
1.21 - Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
1.22 - tac_2tac tac_, Sundef,*)
1.23 - [(End_Detail, End_Detail' t ,
1.24 - ((p,p_), get_loc pt (p,p_)))], [], (pt,pr))) end
1.25 + | solve (_,End_Detail' t) (pt, (p,p_)) =
1.26 + let
1.27 + val pr as (p',_) = (lev_up p, Res)
1.28 + val pp = par_pblobj pt p
1.29 + val r = (fst o (get_obj g_result pt)) p'
1.30 + (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
1.31 + val thy' = get_obj g_domID pt pp
1.32 + val (srls, is, sc) = from_pblobj' thy' pr pt
1.33 + val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
1.34 + in ("ok", ([(End_Detail, End_Detail' t ,
1.35 + ((p,p_), get_loc pt (p,p_)))], [], (pt,pr)))
1.36 + end
1.37
1.38 | solve (mI,m) (pt, po as (p,p_)) =
1.39 -(* val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
1.40 - *)
1.41 - if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02:
1.42 - could be detail, too !!*)
1.43 - then let val ((p,p_),ps,f,pt) =
1.44 - generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
1.45 - m (e_istate, e_ctxt) (p,p_) pt;
1.46 - in ("no-method-specified", (*Free_Solve*)
1.47 - ((*((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*)
1.48 - [(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, e_ctxt)))], ps, (pt,(p,p_)))) end
1.49 - else
1.50 - let
1.51 - val thy' = get_obj g_domID pt (par_pblobj pt p);
1.52 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
1.53 -(*val _= tracing("### solve, before locate_gen p="^(pos'2str(p,p_)));*)
1.54 - val d = e_rls; (*FIXME: canon.simplifier for domain is missing
1.55 - 8.01: generate from domID?*)
1.56 - in case locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of
1.57 - Steps (is', ss as (m',f',pt',p',c')::_) =>
1.58 -(* val Steps (is', ss as (m',f',pt',p',c')::_) =
1.59 - locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
1.60 - *)
1.61 - let (*val _= tracing("### solve, after locate_gen: is= ")
1.62 - val _= tracing(istate2str is')*)
1.63 - (*val nxt_ =
1.64 - case p' of (*change from solve to model subpbl*)
1.65 - (_,Pbl) => nxt_model_pbl m' (pt',p')
1.66 - | _ => fst3 (next_tac (thy',srls) (pt',p') sc is');*)
1.67 - (*27.8.02:next_tac may change to other branches in pt FIXXXXME*)
1.68 - in ("ok", ((*(p',is',nxt_), f', tac_2tac nxt_, safe is',*)
1.69 - map step2taci ss, c', (pt',p'))) end
1.70 - | NotLocatable =>
1.71 - let val (p,ps,f,pt) =
1.72 - generate_hard (assoc_thy "Isac") m (p,p_) pt;
1.73 - in ("not-found-in-script",
1.74 - ((*(p,Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*)
1.75 - [(tac_2tac m, m, (po,is))], ps, (pt,p))) end
1.76 - end;
1.77 + if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02: could be detail, too !!*)
1.78 + then
1.79 + let val ((p,p_),ps,f,pt) =
1.80 + generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
1.81 + m (e_istate, e_ctxt) (p,p_) pt;
1.82 + in ("no-method-specified", (*Free_Solve*)
1.83 + ([(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, e_ctxt)))], ps, (pt,(p,p_))))
1.84 + end
1.85 + else
1.86 + let
1.87 + val thy' = get_obj g_domID pt (par_pblobj pt p);
1.88 + val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
1.89 + val d = e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)
1.90 + in
1.91 + case locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of
1.92 + Steps (is', ss as (m',f',pt',p',c')::_) =>
1.93 + let
1.94 + (*27.8.02:next_tac may change to other branches in pt FIXXXXME*)
1.95 + in ("ok", (map step2taci ss, c', (pt',p'))) end
1.96 + | NotLocatable =>
1.97 + let val (p,ps,f,pt) =
1.98 + generate_hard (assoc_thy "Isac") m (p,p_) pt;
1.99 + in ("not-found-in-script",
1.100 + ([(tac_2tac m, m, (po,is))], ps, (pt,p)))
1.101 + end
1.102 + end;
1.103
1.104 -
1.105 -(*FIXME.WN050821 compare solve ... nxt_solv*)
1.106 +(*FIXME.WN050821 compare fun solve ... fun nxt_solv*)
1.107 (* nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *)
1.108 fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) =
1.109 -(* val ((Apply_Method' (mI,_,_)), _, (pt:ptree, pos as (p,_))) =
1.110 - ((Apply_Method' (mI, NONE, e_istate)), e_istate, ptp);
1.111 - *)
1.112 - let val {srls,ppc,...} = get_met mI;
1.113 - val PblObj{meth=itms,origin=(oris,_,_),probl,...} = get_obj I pt p;
1.114 - val itms = if itms <> [] then itms
1.115 - else complete_metitms oris probl [] ppc
1.116 - val thy' = get_obj g_domID pt p;
1.117 - val thy = assoc_thy thy';
1.118 - val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = init_scrstate thy itms mI;
1.119 - val ini = init_form thy scr env;
1.120 - in
1.121 - case ini of
1.122 - SOME t => (* val SOME t = ini;
1.123 - *)
1.124 - let val pos = ((lev_on o lev_dn) p, Frm)
1.125 - val tac_ = Apply_Method' (mI, SOME t, is, ctxt);
1.126 - val (pos,c,_,pt) = (*implicit Take*)
1.127 - generate1 thy tac_ (is, ctxt) pos pt
1.128 - (*val _= ("### nxt_solv Apply_Method, pos= "^pos'2str (lev_on p,Frm));*)
1.129 - in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)):calcstate' end
1.130 - | NONE =>
1.131 - let val pt = update_env pt (fst pos) (SOME (is, ctxt))
1.132 - val (tacis, c, ptp) = nxt_solve_ (pt, pos)
1.133 - in (tacis @
1.134 - [(Apply_Method mI, Apply_Method' (mI, NONE, e_istate, e_ctxt), (pos, (is, ctxt)))],
1.135 - c, ptp) end
1.136 - end
1.137 -(* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m);
1.138 - val (Check_Postcond' (pI,_), _, (pt, pos as (p,p_))) =
1.139 - (tac_, is, ptp);
1.140 - *)
1.141 - (*TODO.WN050913 remove unnecessary code below*)
1.142 + let
1.143 + val {srls,ppc,...} = get_met mI;
1.144 + val PblObj{meth=itms,origin=(oris,_,_),probl,...} = get_obj I pt p;
1.145 + val itms = if itms <> [] then itms else complete_metitms oris probl [] ppc
1.146 + val thy' = get_obj g_domID pt p;
1.147 + val thy = assoc_thy thy';
1.148 + val ctxt = get_ctxt pt pos
1.149 + val (is as ScrState (env,_,_,_,_,_), _, scr) = init_scrstate thy itms mI;
1.150 + val ini = init_form thy scr env;
1.151 + in
1.152 + case ini of
1.153 + SOME t =>
1.154 + let
1.155 + val pos = ((lev_on o lev_dn) p, Frm)
1.156 + val tac_ = Apply_Method' (mI, SOME t, is, ctxt);
1.157 + val (pos,c,_,pt) = (*implicit Take*)
1.158 + generate1 thy tac_ (is, ctxt) pos pt
1.159 + in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)):calcstate' end
1.160 + | NONE =>
1.161 + let
1.162 + val pt = update_env pt (fst pos) (SOME (is, ctxt))
1.163 + val (tacis, c, ptp) = nxt_solve_ (pt, pos)
1.164 + in (tacis @
1.165 + [(Apply_Method mI, Apply_Method' (mI, NONE, e_istate, ctxt), (pos, (is, ctxt)))],
1.166 + c, ptp)
1.167 + end
1.168 + end
1.169 +
1.170 + (*TODO.WN050913 remove unnecessary code below*)
1.171 | nxt_solv (Check_Postcond' (pI,_)) _ (pt, pos as (p,p_)) =
1.172 - let (*val _=tracing"###solve Check_Postcond";*)
1.173 - val pp = par_pblobj pt p
1.174 - val asm = (case get_obj g_tac pt p of
1.175 - Check_elementwise _ => (*collects and instantiates asms*)
1.176 - (snd o (get_obj g_result pt)) p
1.177 - | _ => get_assumptions_ pt (p,p_))
1.178 - handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
1.179 - val metID = get_obj g_metID pt pp;
1.180 - val {srls=srls,scr=sc,...} = get_met metID;
1.181 - val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
1.182 - (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
1.183 - val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
1.184 - val thy' = get_obj g_domID pt pp;
1.185 - val thy = assoc_thy thy';
1.186 - val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
1.187 - (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
1.188 - in if pp = [] then
1.189 - let val is = ScrState (E,l,a,scval,scsaf,b)
1.190 - val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
1.191 - val ((p,p_),ps,f,pt) =
1.192 - generate1 thy tac_ (is, ctxt) (pp,Res) pt;
1.193 - in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end
1.194 - else
1.195 - let
1.196 - (*resume script of parpbl, transfer value of subpbl-script*)
1.197 - val ppp = par_pblobj pt (lev_up p);
1.198 - val thy' = get_obj g_domID pt ppp;
1.199 + let
1.200 + val pp = par_pblobj pt p
1.201 + val asm =
1.202 + (case get_obj g_tac pt p of
1.203 + Check_elementwise _ => (*collects and instantiates asms*)
1.204 + (snd o (get_obj g_result pt)) p
1.205 + | _ => get_assumptions_ pt (p,p_))
1.206 + handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*)
1.207 + val metID = get_obj g_metID pt pp;
1.208 + val {srls=srls,scr=sc,...} = get_met metID;
1.209 + val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
1.210 + val thy' = get_obj g_domID pt pp;
1.211 val thy = assoc_thy thy';
1.212 - val metID = get_obj g_metID pt ppp;
1.213 - val {scr,...} = get_met metID;
1.214 - val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
1.215 - val ctxt'' = transfer_from_subproblem ctxt ctxt'
1.216 - val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
1.217 - val is = ScrState (E,l,a,scval,scsaf,b)
1.218 - val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
1.219 - (*val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) scr is;WN050913*)
1.220 - in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p,p_))) end
1.221 - end
1.222 + val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
1.223 + in
1.224 + if pp = []
1.225 + then
1.226 + let
1.227 + val is = ScrState (E,l,a,scval,scsaf,b)
1.228 + val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
1.229 + val ((p,p_),ps,f,pt) =
1.230 + generate1 thy tac_ (is, ctxt) (pp,Res) pt;
1.231 + in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end
1.232 + else
1.233 + let (*resume script of parpbl, transfer value of subpbl-script*)
1.234 + val ppp = par_pblobj pt (lev_up p);
1.235 + val thy' = get_obj g_domID pt ppp;
1.236 + val thy = assoc_thy thy';
1.237 + val metID = get_obj g_metID pt ppp;
1.238 + val {scr,...} = get_met metID;
1.239 + val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
1.240 + val ctxt'' = transfer_from_subproblem ctxt ctxt'
1.241 + val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
1.242 + val is = ScrState (E,l,a,scval,scsaf,b)
1.243 + val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
1.244 + in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p,p_))) end
1.245 + end
1.246
1.247 | nxt_solv (End_Proof'') _ ptp = ([], [], ptp)
1.248
1.249 @@ -428,104 +408,110 @@
1.250 (* val (auto, c, (ptp as (_, p))) = (auto, (c@c'), ptp);
1.251 *)
1.252 fun complete_solve auto c (ptp as (_, p): ptree * pos') =
1.253 - if p = ([], Res) then ("end-of-calculation", [], ptp) else
1.254 + if p = ([], Res)
1.255 + then ("end-of-calculation", [], ptp)
1.256 + else
1.257 case nxt_solve_ ptp of
1.258 - ((Subproblem _, tac_, (_, is))::_, c', ptp') =>
1.259 -(* val ptp' = ptp''';
1.260 - *)
1.261 - if autoord auto < 5 then ("ok", c@c', ptp)
1.262 - else let val ptp = all_modspec ptp';
1.263 - val (_, c'', ptp) = all_solve auto (c@c') ptp;
1.264 - in complete_solve auto (c@c'@c'') ptp end
1.265 - | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
1.266 - if autoord auto < 6 orelse p' = ([],Res) then ("ok", c@c', ptp')
1.267 - else complete_solve auto (c@c') ptp'
1.268 - | ((End_Detail, _, _)::_, c', ptp') =>
1.269 - if autoord auto < 6 then ("ok", c@c', ptp')
1.270 - else complete_solve auto (c@c') ptp'
1.271 - | (_, c', ptp') => complete_solve auto (c@c') ptp'
1.272 -(* val (tacis, c', ptp') = nxt_solve_ ptp;
1.273 - val (tacis, c', ptp'') = nxt_solve_ ptp';
1.274 - val (tacis, c', ptp''') = nxt_solve_ ptp'';
1.275 - val (tacis, c', ptp'''') = nxt_solve_ ptp''';
1.276 - val (tacis, c', ptp''''') = nxt_solve_ ptp'''';
1.277 - *)
1.278 -and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') =
1.279 -(* val (ptp as (pt, (p,_))) = ptp;
1.280 - val (ptp as (pt, (p,_))) = ptp';
1.281 - val (ptp as (pt, (p,_))) = (pt, pos);
1.282 - *)
1.283 - let val (_,_,mI) = get_obj g_spec pt p;
1.284 - val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
1.285 - (e_istate, e_ctxt) ptp;
1.286 - in complete_solve auto (c@c') ptp end;
1.287 -(*@@@ vvv @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.288 + ((Subproblem _, tac_, (_, is))::_, c', ptp') =>
1.289 + if autoord auto < 5
1.290 + then ("ok", c@c', ptp)
1.291 + else
1.292 + let
1.293 + val ptp = all_modspec ptp';
1.294 + val (_, c'', ptp) = all_solve auto (c@c') ptp;
1.295 + in complete_solve auto (c@c'@c'') ptp end
1.296 + | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
1.297 + if autoord auto < 6 orelse p' = ([],Res)
1.298 + then ("ok", c @ c', ptp')
1.299 + else complete_solve auto (c @ c') ptp'
1.300 + | ((End_Detail, _, _)::_, c', ptp') =>
1.301 + if autoord auto < 6
1.302 + then ("ok", c @ c', ptp')
1.303 + else complete_solve auto (c @ c') ptp'
1.304 + | (_, c', ptp') => complete_solve auto (c @ c') ptp'
1.305 +
1.306 +and all_solve auto c (ptp as (pt, pos as (p,_)): ptree * pos') =
1.307 + let
1.308 + val (_,_,mI) = get_obj g_spec pt p;
1.309 + val ctxt = get_ctxt pt pos
1.310 + val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt))
1.311 + (e_istate, ctxt) ptp;
1.312 + in complete_solve auto (c @ c') ptp end;
1.313 +
1.314 fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') =
1.315 - if p = ([], Res) then ("end-of-calculation", [], ptp) else
1.316 + if p = ([], Res)
1.317 + then ("end-of-calculation", [], ptp)
1.318 + else
1.319 if member op = [Pbl,Met] p_
1.320 - then let val ptp = all_modspec ptp
1.321 - val (_, c', ptp) = all_solve auto c ptp
1.322 - in complete_solve auto (c@c') ptp end
1.323 - else case nxt_solve_ ptp of
1.324 - ((Subproblem _, tac_, (_, is))::_, c', ptp') =>
1.325 - if autoord auto < 5 then ("ok", c@c', ptp)
1.326 - else let val ptp = all_modspec ptp'
1.327 - val (_, c'', ptp) = all_solve auto (c@c') ptp
1.328 - in complete_solve auto (c@c'@c'') ptp end
1.329 - | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
1.330 - if autoord auto < 6 orelse p' = ([],Res) then ("ok", c@c', ptp')
1.331 - else complete_solve auto (c@c') ptp'
1.332 - | ((End_Detail, _, _)::_, c', ptp') =>
1.333 - if autoord auto < 6 then ("ok", c@c', ptp')
1.334 - else complete_solve auto (c@c') ptp'
1.335 - | (_, c', ptp') => complete_solve auto (c@c') ptp'
1.336 -and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') =
1.337 - let val (_,_,mI) = get_obj g_spec pt p
1.338 - val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
1.339 - (e_istate, e_ctxt) ptp
1.340 - in complete_solve auto (c@c') ptp end;
1.341 + then
1.342 + let
1.343 + val ptp = all_modspec ptp
1.344 + val (_, c', ptp) = all_solve auto c ptp
1.345 + in complete_solve auto (c @ c') ptp end
1.346 + else
1.347 + case nxt_solve_ ptp of
1.348 + ((Subproblem _, tac_, (_, is))::_, c', ptp') =>
1.349 + if autoord auto < 5
1.350 + then ("ok", c @ c', ptp)
1.351 + else
1.352 + let
1.353 + val ptp = all_modspec ptp'
1.354 + val (_, c'', ptp) = all_solve auto (c @ c') ptp
1.355 + in complete_solve auto (c @ c'@ c'') ptp end
1.356 + | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
1.357 + if autoord auto < 6 orelse p' = ([],Res)
1.358 + then ("ok", c @ c', ptp')
1.359 + else complete_solve auto (c @ c') ptp'
1.360 + | ((End_Detail, _, _)::_, c', ptp') =>
1.361 + if autoord auto < 6
1.362 + then ("ok", c @ c', ptp')
1.363 + else complete_solve auto (c @ c') ptp'
1.364 + | (_, c', ptp') => complete_solve auto (c @ c') ptp'
1.365
1.366 -(*.aux.fun for detailrls with Rrls, reverse rewriting.*)
1.367 -(* val (nds, t, ((rule, (t', asm)) :: rts)) = ([], t, rul_terms);
1.368 - *)
1.369 +and all_solve auto c (ptp as (pt, pos as (p,_)): ptree * pos') =
1.370 + let
1.371 + val (_,_,mI) = get_obj g_spec pt p
1.372 + val ctxt = get_ctxt pt pos
1.373 + val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt))
1.374 + (e_istate, ctxt) ptp
1.375 + in complete_solve auto (c @ c') ptp end;
1.376 +
1.377 +(* aux.fun for detailrls with Rrls, reverse rewriting *)
1.378 fun rul_terms_2nds nds t [] = nds
1.379 | rul_terms_2nds nds t ((rule, res as (t', _)) :: rts) =
1.380 (append_atomic [] (e_istate, e_ctxt) t (rule2tac [] rule) res Complete EmptyPtree) ::
1.381 (rul_terms_2nds nds t' rts);
1.382
1.383 -
1.384 -(*. detail steps done internally by Rewrite_Set*
1.385 - into ctree by use of a script .*)
1.386 -(* val (pt, (p,p_)) = (pt, pos);
1.387 - *)
1.388 -fun detailrls pt ((p,p_):pos') =
1.389 - let val t = get_obj g_form pt p
1.390 - val tac = get_obj g_tac pt p
1.391 - val rls = (assoc_rls o rls_of) tac
1.392 - in case rls of
1.393 -(* val Rrls {scr = Rfuns {init_state,...},...} = rls;
1.394 - *)
1.395 - Rrls {scr = Rfuns {init_state,...},...} =>
1.396 - let val (_,_,_,rul_terms) = init_state t
1.397 - val newnds = rul_terms_2nds [] t rul_terms
1.398 - val pt''' = ins_chn newnds pt p
1.399 - in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
1.400 - | _ =>
1.401 - let val is = init_istate tac t
1.402 - (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
1.403 - is wrong for simpl, but working ?!? *)
1.404 - val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*),
1.405 - SOME t, is, e_ctxt)
1.406 - val pos' = ((lev_on o lev_dn) p, Frm)
1.407 - val thy = assoc_thy "Isac"
1.408 - val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, e_ctxt) pos' pt
1.409 - val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
1.410 - val newnds = children (get_nd pt'' p)
1.411 - val pt''' = ins_chn newnds pt p
1.412 - (*complete_solve cuts branches after*)
1.413 - in ("detailrls", pt'''(*, get_formress [] ((lev_on o lev_dn) p)cn*),
1.414 - (p @ [length newnds], Res):pos') end
1.415 - end;
1.416 +(* detail steps done internally by Rewrite_Set* into ctree by use of a script *)
1.417 +fun detailrls pt (pos as (p,p_):pos') =
1.418 + let
1.419 + val t = get_obj g_form pt p
1.420 + val tac = get_obj g_tac pt p
1.421 + val rls = (assoc_rls o rls_of) tac
1.422 + val ctxt = get_ctxt pt pos
1.423 + in
1.424 + case rls of
1.425 + Rrls {scr = Rfuns {init_state,...},...} =>
1.426 + let
1.427 + val (_,_,_,rul_terms) = init_state t
1.428 + val newnds = rul_terms_2nds [] t rul_terms
1.429 + val pt''' = ins_chn newnds pt p
1.430 + in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
1.431 + | _ =>
1.432 + let
1.433 + val is = init_istate tac t
1.434 + (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
1.435 + is wrong for simpl, but working ?!? *)
1.436 + val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
1.437 + val pos' = ((lev_on o lev_dn) p, Frm)
1.438 + val thy = assoc_thy "Isac"
1.439 + val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, ctxt) pos' pt
1.440 + val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
1.441 + val newnds = children (get_nd pt'' p)
1.442 + val pt''' = ins_chn newnds pt p
1.443 + (*complete_solve cuts branches after*)
1.444 + in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
1.445 + end;
1.446
1.447
1.448