1.1 --- a/src/Tools/isac/Interpret/script.sml	Tue May 17 09:55:30 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Tue May 17 14:56:54 2011 +0200
     1.3 @@ -1709,7 +1709,7 @@
     1.4  			      "formals: " ^ terms2str formals ^ "\n" ^
     1.5  			      "actuals: " ^ terms2str actuals)
     1.6       val env = relate_args [] formals actuals;
     1.7 -   in (ScrState (env,[],NONE,e_term,Safe,true), e_ctxt, scr):istate * Proof.context * scr end;
     1.8 +   in (ScrState (env,[],NONE,e_term,Safe,true), (*FIXME.WN170511 remove*)e_ctxt, scr):istate * Proof.context * scr end;
     1.9  
    1.10  (* decide, where to get script/istate from:
    1.11     (*1*) from PblObj.env: at begin of script if no init_form

     2.1 --- a/src/Tools/isac/Interpret/solve.sml	Tue May 17 09:55:30 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/solve.sml	Tue May 17 14:56:54 2011 +0200
     2.3 @@ -232,140 +232,120 @@
     2.4  
     2.5    | solve (_,End_Proof'') (pt, (p,p_)) =
     2.6        ("end-proof",
     2.7 -       ((*(([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe,*)
     2.8 -       [(Empty_Tac,Empty_Tac_,(([],Res),(Uistate, e_ctxt)))],[],(pt,(p,p_))))
     2.9 +       ([(Empty_Tac,Empty_Tac_,(([],Res),(Uistate, e_ctxt)))],[],(pt,(p,p_))))
    2.10  
    2.11  (*-----------vvvvvvvvvvv could be done by generate1 ?!?*)
    2.12 -  | solve (_,End_Detail' t) (pt,(p,p_)) =
    2.13 -    let val pr as (p',_) = (lev_up p, Res)
    2.14 -	val pp = par_pblobj pt p
    2.15 -	val r = (fst o (get_obj g_result pt)) p' 
    2.16 -	(*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
    2.17 -	val thy' = get_obj g_domID pt pp
    2.18 -	val (srls, is, sc) = from_pblobj' thy' pr pt
    2.19 -	val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
    2.20 -    in ("ok", ((*((pp,Frm(*???*)),is,tac_), 
    2.21 -	Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
    2.22 -	tac_2tac tac_, Sundef,*)
    2.23 -	[(End_Detail, End_Detail' t , 
    2.24 -	  ((p,p_), get_loc pt (p,p_)))], [], (pt,pr))) end
    2.25 +  | solve (_,End_Detail' t) (pt, (p,p_)) =
    2.26 +      let
    2.27 +        val pr as (p',_) = (lev_up p, Res)
    2.28 +	      val pp = par_pblobj pt p
    2.29 +	      val r = (fst o (get_obj g_result pt)) p' 
    2.30 +	      (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
    2.31 +	      val thy' = get_obj g_domID pt pp
    2.32 +	      val (srls, is, sc) = from_pblobj' thy' pr pt
    2.33 +	      val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
    2.34 +      in ("ok", ([(End_Detail, End_Detail' t , 
    2.35 +	      ((p,p_), get_loc pt (p,p_)))], [], (pt,pr)))
    2.36 +      end
    2.37  
    2.38    | solve (mI,m) (pt, po as (p,p_)) =
    2.39 -(* val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
    2.40 -   *)
    2.41 -    if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02:
    2.42 -						      could be detail, too !!*)
    2.43 -    then let val ((p,p_),ps,f,pt) = 
    2.44 -		 generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) 
    2.45 -			   m (e_istate, e_ctxt) (p,p_) pt;
    2.46 -	 in ("no-method-specified", (*Free_Solve*)
    2.47 -	     ((*((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*)
    2.48 -	     [(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, e_ctxt)))], ps, (pt,(p,p_)))) end
    2.49 -    else
    2.50 -	let 
    2.51 -	    val thy' = get_obj g_domID pt (par_pblobj pt p);
    2.52 -	    val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    2.53 -(*val _= tracing("### solve, before locate_gen p="^(pos'2str(p,p_)));*)
    2.54 -		val d = e_rls; (*FIXME: canon.simplifier for domain is missing
    2.55 -				8.01: generate from domID?*)
    2.56 -	in case locate_gen (thy',srls) m  (pt,(p,p_)) (sc,d) is of 
    2.57 -	       Steps (is', ss as (m',f',pt',p',c')::_) =>
    2.58 -(* val Steps (is', ss as (m',f',pt',p',c')::_) =
    2.59 -       locate_gen (thy',srls) m  (pt,(p,p_)) (sc,d) is;
    2.60 - *)
    2.61 -	       let (*val _= tracing("### solve, after locate_gen: is= ")
    2.62 -		       val _= tracing(istate2str is')*)
    2.63 -		   (*val nxt_ = 
    2.64 -		       case p' of (*change from solve to model subpbl*)
    2.65 -			   (_,Pbl) => nxt_model_pbl m' (pt',p')
    2.66 -			 | _ => fst3 (next_tac (thy',srls) (pt',p') sc is');*) 
    2.67 -	       (*27.8.02:next_tac may change to other branches in pt FIXXXXME*)
    2.68 -	       in ("ok", ((*(p',is',nxt_), f', tac_2tac nxt_, safe is',*)
    2.69 -		   map step2taci ss, c', (pt',p'))) end
    2.70 -	     | NotLocatable =>  
    2.71 -	       let val (p,ps,f,pt) = 
    2.72 -		       generate_hard (assoc_thy "Isac") m (p,p_) pt;
    2.73 -	       in ("not-found-in-script",
    2.74 -		   ((*(p,Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*) 
    2.75 -		   [(tac_2tac m, m, (po,is))], ps, (pt,p))) end
    2.76 -	end;
    2.77 +      if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02: could be detail, too !!*)
    2.78 +      then
    2.79 +        let val ((p,p_),ps,f,pt) = 
    2.80 +		      generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) 
    2.81 +			      m (e_istate, e_ctxt) (p,p_) pt;
    2.82 +	      in ("no-method-specified", (*Free_Solve*)
    2.83 +	        ([(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, e_ctxt)))], ps, (pt,(p,p_))))
    2.84 +        end
    2.85 +      else
    2.86 +	      let 
    2.87 +	        val thy' = get_obj g_domID pt (par_pblobj pt p);
    2.88 +	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
    2.89 +		      val d = e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)
    2.90 +	      in
    2.91 +          case locate_gen (thy',srls) m  (pt,(p,p_)) (sc,d) is of 
    2.92 +	          Steps (is', ss as (m',f',pt',p',c')::_) =>
    2.93 +	            let 
    2.94 +	              (*27.8.02:next_tac may change to other branches in pt FIXXXXME*)
    2.95 +	            in ("ok", (map step2taci ss, c', (pt',p'))) end
    2.96 +	        | NotLocatable =>  
    2.97 +	            let val (p,ps,f,pt) = 
    2.98 +		            generate_hard (assoc_thy "Isac") m (p,p_) pt;
    2.99 +	            in ("not-found-in-script",
   2.100 +		            ([(tac_2tac m, m, (po,is))], ps, (pt,p)))
   2.101 +              end
   2.102 +	      end;
   2.103  
   2.104 -
   2.105 -(*FIXME.WN050821 compare solve ... nxt_solv*)
   2.106 +(*FIXME.WN050821 compare fun solve ... fun nxt_solv*)
   2.107  (* nxt_solv (Apply_Method'     vvv FIXME: get args in applicable_in *)
   2.108  fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) =
   2.109 -(* val ((Apply_Method' (mI,_,_)),             _,    (pt:ptree, pos as (p,_))) =
   2.110 -       ((Apply_Method' (mI, NONE, e_istate)), e_istate, ptp);
   2.111 -   *)
   2.112 -  let val {srls,ppc,...} = get_met mI;
   2.113 -    val PblObj{meth=itms,origin=(oris,_,_),probl,...} = get_obj I pt p;
   2.114 -    val itms = if itms <> [] then itms
   2.115 -	       else complete_metitms oris probl [] ppc
   2.116 -    val thy' = get_obj g_domID pt p;
   2.117 -    val thy = assoc_thy thy';
   2.118 -    val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = init_scrstate thy itms mI;
   2.119 -    val ini = init_form thy scr env;
   2.120 -  in 
   2.121 -    case ini of
   2.122 -    SOME t => (* val SOME t = ini; 
   2.123 -	         *)
   2.124 -    let val pos = ((lev_on o lev_dn) p, Frm)
   2.125 -	val tac_ = Apply_Method' (mI, SOME t, is, ctxt);
   2.126 -	val (pos,c,_,pt) = (*implicit Take*)
   2.127 -	    generate1 thy tac_ (is, ctxt) pos pt
   2.128 -      (*val _= ("### nxt_solv Apply_Method, pos= "^pos'2str (lev_on p,Frm));*)
   2.129 -    in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)):calcstate' end
   2.130 -  | NONE =>
   2.131 -    let val pt = update_env pt (fst pos) (SOME (is, ctxt))
   2.132 -	val (tacis, c, ptp) = nxt_solve_ (pt, pos)
   2.133 -    in (tacis @ 
   2.134 -	[(Apply_Method mI, Apply_Method' (mI, NONE, e_istate, e_ctxt), (pos, (is, ctxt)))],
   2.135 -	c, ptp) end
   2.136 -  end
   2.137 -(* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m);
   2.138 -   val (Check_Postcond' (pI,_), _, (pt, pos as (p,p_))) = 
   2.139 -       (tac_,                  is,  ptp);
   2.140 -   *)
   2.141 -  (*TODO.WN050913 remove unnecessary code below*)
   2.142 +      let
   2.143 +        val {srls,ppc,...} = get_met mI;
   2.144 +        val PblObj{meth=itms,origin=(oris,_,_),probl,...} = get_obj I pt p;
   2.145 +        val itms = if itms <> [] then itms else complete_metitms oris probl [] ppc
   2.146 +        val thy' = get_obj g_domID pt p;
   2.147 +        val thy = assoc_thy thy';
   2.148 +        val ctxt = get_ctxt pt pos
   2.149 +        val (is as ScrState (env,_,_,_,_,_), _, scr) = init_scrstate thy itms mI;
   2.150 +        val ini = init_form thy scr env;
   2.151 +      in 
   2.152 +        case ini of
   2.153 +          SOME t =>
   2.154 +            let
   2.155 +              val pos = ((lev_on o lev_dn) p, Frm)
   2.156 +	            val tac_ = Apply_Method' (mI, SOME t, is, ctxt);
   2.157 +	            val (pos,c,_,pt) = (*implicit Take*)
   2.158 +	              generate1 thy tac_ (is, ctxt) pos pt
   2.159 +            in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)):calcstate' end
   2.160 +        | NONE =>
   2.161 +            let
   2.162 +              val pt = update_env pt (fst pos) (SOME (is, ctxt))
   2.163 +	            val (tacis, c, ptp) = nxt_solve_ (pt, pos)
   2.164 +            in (tacis @ 
   2.165 +	              [(Apply_Method mI, Apply_Method' (mI, NONE, e_istate, ctxt), (pos, (is, ctxt)))],
   2.166 +	             c, ptp)
   2.167 +            end
   2.168 +      end
   2.169 +
   2.170 +    (*TODO.WN050913 remove unnecessary code below*)
   2.171    | nxt_solv (Check_Postcond' (pI,_)) _ (pt, pos as (p,p_))  =
   2.172 -    let (*val _=tracing"###solve Check_Postcond";*)
   2.173 -      val pp = par_pblobj pt p
   2.174 -      val asm = (case get_obj g_tac pt p of
   2.175 -		    Check_elementwise _ => (*collects and instantiates asms*)
   2.176 -		    (snd o (get_obj g_result pt)) p
   2.177 -		  | _ => get_assumptions_ pt (p,p_))
   2.178 -	  handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
   2.179 -      val metID = get_obj g_metID pt pp;
   2.180 -      val {srls=srls,scr=sc,...} = get_met metID;
   2.181 -      val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_); 
   2.182 -     (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
   2.183 -      val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
   2.184 -      val thy' = get_obj g_domID pt pp;
   2.185 -      val thy = assoc_thy thy';
   2.186 -      val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
   2.187 -      (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
   2.188 -    in if pp = [] then 
   2.189 -	   let val is = ScrState (E,l,a,scval,scsaf,b)
   2.190 -	       val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
   2.191 -	       val ((p,p_),ps,f,pt) = 
   2.192 -		   generate1 thy tac_ (is, ctxt) (pp,Res) pt;
   2.193 -	   in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end
   2.194 -       else
   2.195 -        let
   2.196 -	  (*resume script of parpbl, transfer value of subpbl-script*)
   2.197 -        val ppp = par_pblobj pt (lev_up p);
   2.198 -	val thy' = get_obj g_domID pt ppp;
   2.199 +      let
   2.200 +        val pp = par_pblobj pt p
   2.201 +        val asm =
   2.202 +          (case get_obj g_tac pt p of
   2.203 +		         Check_elementwise _ => (*collects and instantiates asms*)
   2.204 +		           (snd o (get_obj g_result pt)) p
   2.205 +		       | _ => get_assumptions_ pt (p,p_))
   2.206 +	        handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*)
   2.207 +        val metID = get_obj g_metID pt pp;
   2.208 +        val {srls=srls,scr=sc,...} = get_met metID;
   2.209 +        val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_); 
   2.210 +        val thy' = get_obj g_domID pt pp;
   2.211          val thy = assoc_thy thy';
   2.212 -	val metID = get_obj g_metID pt ppp;
   2.213 -	val {scr,...} = get_met metID;
   2.214 -        val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
   2.215 -	      val ctxt'' = transfer_from_subproblem ctxt ctxt'
   2.216 -        val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
   2.217 -	val is = ScrState (E,l,a,scval,scsaf,b)
   2.218 -        val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
   2.219 -	(*val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) scr is;WN050913*)
   2.220 -       in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p,p_))) end
   2.221 -    end
   2.222 +        val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
   2.223 +      in
   2.224 +        if pp = []
   2.225 +        then 
   2.226 +	        let
   2.227 +            val is = ScrState (E,l,a,scval,scsaf,b)
   2.228 +	          val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
   2.229 +	          val ((p,p_),ps,f,pt) = 
   2.230 +		          generate1 thy tac_ (is, ctxt) (pp,Res) pt;
   2.231 +	        in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end
   2.232 +        else
   2.233 +          let (*resume script of parpbl, transfer value of subpbl-script*)
   2.234 +            val ppp = par_pblobj pt (lev_up p);
   2.235 +	          val thy' = get_obj g_domID pt ppp;
   2.236 +            val thy = assoc_thy thy';
   2.237 +	          val metID = get_obj g_metID pt ppp;
   2.238 +	          val {scr,...} = get_met metID;
   2.239 +            val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
   2.240 +	          val ctxt'' = transfer_from_subproblem ctxt ctxt'
   2.241 +            val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
   2.242 +	          val is = ScrState (E,l,a,scval,scsaf,b)
   2.243 +            val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
   2.244 +          in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p,p_))) end
   2.245 +      end
   2.246  
   2.247    | nxt_solv (End_Proof'') _ ptp = ([], [], ptp)
   2.248  
   2.249 @@ -428,104 +408,110 @@
   2.250  (* val (auto, c, (ptp as (_, p))) = (auto, (c@c'), ptp);
   2.251     *)
   2.252  fun complete_solve auto c (ptp as (_, p): ptree * pos') =
   2.253 -    if p = ([], Res) then ("end-of-calculation", [], ptp) else
   2.254 +  if p = ([], Res)
   2.255 +  then ("end-of-calculation", [], ptp)
   2.256 +  else
   2.257      case nxt_solve_ ptp of
   2.258 -	((Subproblem _, tac_, (_, is))::_, c', ptp') =>
   2.259 -(* val ptp' = ptp''';
   2.260 -   *)
   2.261 -	if autoord auto < 5 then ("ok", c@c', ptp)
   2.262 -	else let val ptp = all_modspec ptp';
   2.263 -	         val (_, c'', ptp) = all_solve auto (c@c') ptp;
   2.264 -	     in complete_solve auto (c@c'@c'') ptp end
   2.265 -      | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
   2.266 -	if autoord auto < 6 orelse p' = ([],Res) then ("ok", c@c', ptp')
   2.267 -	else complete_solve auto (c@c') ptp'
   2.268 -      | ((End_Detail, _, _)::_, c', ptp') => 
   2.269 -	if autoord auto < 6 then ("ok", c@c', ptp')
   2.270 -	else complete_solve auto (c@c') ptp'
   2.271 -      | (_, c', ptp') => complete_solve auto (c@c') ptp'
   2.272 -(* val (tacis, c', ptp') = nxt_solve_ ptp;
   2.273 -   val (tacis, c', ptp'') = nxt_solve_ ptp';
   2.274 -   val (tacis, c', ptp''') = nxt_solve_ ptp'';
   2.275 -   val (tacis, c', ptp'''') = nxt_solve_ ptp''';
   2.276 -   val (tacis, c', ptp''''') = nxt_solve_ ptp'''';
   2.277 -   *)
   2.278 -and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') = 
   2.279 -(* val (ptp as (pt, (p,_))) = ptp;
   2.280 -   val (ptp as (pt, (p,_))) = ptp';
   2.281 -   val (ptp as (pt, (p,_))) = (pt, pos);
   2.282 -   *)
   2.283 -    let val (_,_,mI) = get_obj g_spec pt p;
   2.284 -        val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
   2.285 -				(e_istate, e_ctxt) ptp;
   2.286 -    in complete_solve auto (c@c') ptp end;
   2.287 -(*@@@ vvv @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
   2.288 +	    ((Subproblem _, tac_, (_, is))::_, c', ptp') =>
   2.289 +	      if autoord auto < 5
   2.290 +        then ("ok", c@c', ptp)
   2.291 +	      else
   2.292 +          let
   2.293 +            val ptp = all_modspec ptp';
   2.294 +	          val (_, c'', ptp) = all_solve auto (c@c') ptp;
   2.295 +	        in complete_solve auto (c@c'@c'') ptp end
   2.296 +    | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
   2.297 +	      if autoord auto < 6 orelse p' = ([],Res)
   2.298 +        then ("ok", c @ c', ptp')
   2.299 +	      else complete_solve auto (c @ c') ptp'
   2.300 +    | ((End_Detail, _, _)::_, c', ptp') => 
   2.301 +	      if autoord auto < 6
   2.302 +        then ("ok", c @ c', ptp')
   2.303 +	      else complete_solve auto (c @ c') ptp'
   2.304 +    | (_, c', ptp') => complete_solve auto (c @ c') ptp'
   2.305 +
   2.306 +and all_solve auto c (ptp as (pt, pos as (p,_)): ptree * pos') = 
   2.307 +   let
   2.308 +     val (_,_,mI) = get_obj g_spec pt p;
   2.309 +     val ctxt = get_ctxt pt pos
   2.310 +     val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt))
   2.311 +			 (e_istate, ctxt) ptp;
   2.312 +   in complete_solve auto (c @ c') ptp end;
   2.313 +
   2.314  fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') =
   2.315 -    if p = ([], Res) then ("end-of-calculation", [], ptp) else
   2.316 +  if p = ([], Res)
   2.317 +  then ("end-of-calculation", [], ptp)
   2.318 +  else
   2.319      if member op = [Pbl,Met] p_
   2.320 -    then let val ptp = all_modspec ptp
   2.321 -	     val (_, c', ptp) = all_solve auto c ptp
   2.322 -	 in complete_solve auto (c@c') ptp end
   2.323 -    else case nxt_solve_ ptp of
   2.324 -	     ((Subproblem _, tac_, (_, is))::_, c', ptp') =>
   2.325 -	     if autoord auto < 5 then ("ok", c@c', ptp)
   2.326 -	     else let val ptp = all_modspec ptp'
   2.327 -		      val (_, c'', ptp) = all_solve auto (c@c') ptp
   2.328 -		  in complete_solve auto (c@c'@c'') ptp end
   2.329 -	   | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
   2.330 -	     if autoord auto < 6 orelse p' = ([],Res) then ("ok", c@c', ptp')
   2.331 -	     else complete_solve auto (c@c') ptp'
   2.332 -	   | ((End_Detail, _, _)::_, c', ptp') => 
   2.333 -	     if autoord auto < 6 then ("ok", c@c', ptp')
   2.334 -	     else complete_solve auto (c@c') ptp'
   2.335 -	   | (_, c', ptp') => complete_solve auto (c@c') ptp'
   2.336 -and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') = 
   2.337 -    let val (_,_,mI) = get_obj g_spec pt p
   2.338 -        val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
   2.339 -				    (e_istate, e_ctxt) ptp
   2.340 -    in complete_solve auto (c@c') ptp end;
   2.341 +    then
   2.342 +      let
   2.343 +        val ptp = all_modspec ptp
   2.344 +	      val (_, c', ptp) = all_solve auto c ptp
   2.345 +	    in complete_solve auto (c @ c') ptp end
   2.346 +    else
   2.347 +      case nxt_solve_ ptp of
   2.348 +	      ((Subproblem _, tac_, (_, is))::_, c', ptp') =>
   2.349 +	        if autoord auto < 5
   2.350 +          then ("ok", c @ c', ptp)
   2.351 +	        else
   2.352 +            let
   2.353 +              val ptp = all_modspec ptp'
   2.354 +	           val (_, c'', ptp) = all_solve auto (c @ c') ptp
   2.355 +	         in complete_solve auto (c @ c'@ c'') ptp end
   2.356 +	    | ((Check_Postcond _, tac_, (_, is))::_, c', ptp' as (_, p')) =>
   2.357 +	        if autoord auto < 6 orelse p' = ([],Res)
   2.358 +          then ("ok", c @ c', ptp')
   2.359 +	        else complete_solve auto (c @ c') ptp'
   2.360 +	    | ((End_Detail, _, _)::_, c', ptp') => 
   2.361 +	        if autoord auto < 6
   2.362 +          then ("ok", c @ c', ptp')
   2.363 +	        else complete_solve auto (c @ c') ptp'
   2.364 +	    | (_, c', ptp') => complete_solve auto (c @ c') ptp'
   2.365  
   2.366 -(*.aux.fun for detailrls with Rrls, reverse rewriting.*)
   2.367 -(* val (nds, t, ((rule, (t', asm)) :: rts)) = ([], t, rul_terms);
   2.368 -   *)
   2.369 +and all_solve auto c (ptp as (pt, pos as (p,_)): ptree * pos') = 
   2.370 +  let
   2.371 +    val (_,_,mI) = get_obj g_spec pt p
   2.372 +    val ctxt = get_ctxt pt pos
   2.373 +    val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt))
   2.374 +			(e_istate, ctxt) ptp
   2.375 +  in complete_solve auto (c @ c') ptp end;
   2.376 +
   2.377 +(* aux.fun for detailrls with Rrls, reverse rewriting *)
   2.378  fun rul_terms_2nds nds t [] = nds
   2.379    | rul_terms_2nds nds t ((rule, res as (t', _)) :: rts) =
   2.380      (append_atomic [] (e_istate, e_ctxt) t (rule2tac [] rule) res Complete EmptyPtree) ::
   2.381      (rul_terms_2nds nds t' rts);
   2.382  
   2.383 -
   2.384 -(*. detail steps done internally by Rewrite_Set* 
   2.385 -    into ctree by use of a script .*)
   2.386 -(* val (pt, (p,p_)) = (pt, pos);
   2.387 -   *)
   2.388 -fun detailrls pt ((p,p_):pos') = 
   2.389 -    let val t = get_obj g_form pt p
   2.390 -	val tac = get_obj g_tac pt p
   2.391 -	val rls = (assoc_rls o rls_of) tac
   2.392 -    in case rls of
   2.393 -(* val Rrls {scr = Rfuns {init_state,...},...} = rls;
   2.394 -   *)
   2.395 -	   Rrls {scr = Rfuns {init_state,...},...} => 
   2.396 -	   let val (_,_,_,rul_terms) = init_state t
   2.397 -	       val newnds = rul_terms_2nds [] t rul_terms
   2.398 -	       val pt''' = ins_chn newnds pt p 
   2.399 -	   in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
   2.400 -	 | _ =>
   2.401 -	   let val is = init_istate tac t
   2.402 -	(*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
   2.403 -				      is wrong for simpl, but working ?!? *)
   2.404 -	       val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), 
   2.405 -					 SOME t, is, e_ctxt)
   2.406 -	       val pos' = ((lev_on o lev_dn) p, Frm)
   2.407 -	       val thy = assoc_thy "Isac"
   2.408 -	       val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, e_ctxt) pos' pt
   2.409 -	       val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
   2.410 -	       val newnds = children (get_nd pt'' p)
   2.411 -	       val pt''' = ins_chn newnds pt p 
   2.412 -	   (*complete_solve cuts branches after*)
   2.413 -	   in ("detailrls", pt'''(*, get_formress [] ((lev_on o lev_dn) p)cn*),
   2.414 -	       (p @ [length newnds], Res):pos') end
   2.415 -    end;
   2.416 +(* detail steps done internally by Rewrite_Set* into ctree by use of a script *)
   2.417 +fun detailrls pt (pos as (p,p_):pos') = 
   2.418 +  let
   2.419 +    val t = get_obj g_form pt p
   2.420 +	  val tac = get_obj g_tac pt p
   2.421 +	  val rls = (assoc_rls o rls_of) tac
   2.422 +    val ctxt = get_ctxt pt pos
   2.423 +  in
   2.424 +    case rls of
   2.425 +	    Rrls {scr = Rfuns {init_state,...},...} => 
   2.426 +	      let
   2.427 +          val (_,_,_,rul_terms) = init_state t
   2.428 +	        val newnds = rul_terms_2nds [] t rul_terms
   2.429 +	        val pt''' = ins_chn newnds pt p 
   2.430 +	      in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
   2.431 +	  | _ =>
   2.432 +	      let
   2.433 +          val is = init_istate tac t
   2.434 +	        (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
   2.435 +				    is wrong for simpl, but working ?!? *)
   2.436 +	        val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
   2.437 +	        val pos' = ((lev_on o lev_dn) p, Frm)
   2.438 +	        val thy = assoc_thy "Isac"
   2.439 +	        val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, ctxt) pos' pt
   2.440 +	        val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
   2.441 +	        val newnds = children (get_nd pt'' p)
   2.442 +	        val pt''' = ins_chn newnds pt p 
   2.443 +	        (*complete_solve cuts branches after*)
   2.444 +	     in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
   2.445 +  end;
   2.446  
   2.447  
   2.448  

     3.1 --- a/test/Tools/isac/Test_Isac.thy	Tue May 17 09:55:30 2011 +0200
     3.2 +++ b/test/Tools/isac/Test_Isac.thy	Tue May 17 14:56:54 2011 +0200
     3.3 @@ -98,8 +98,41 @@
     3.4    use "Minisubpbl/150-add-given.sml"
     3.5    use "Minisubpbl/200-start-method.sml"
     3.6    use "Minisubpbl/300-init-subpbl.sml"
     3.7 +  use "Minisubpbl/400-start-meth-subpbl.sml"
     3.8 +  use "Minisubpbl/500-postcond.sml"
     3.9 +
    3.10  ML {*
    3.11 -
    3.12 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    3.13 +val (dI',pI',mI') =
    3.14 +   ("Test", ["sqroot-test","univariate","equation","test"],
    3.15 +    ["Test","squ-equ-test-subpbl1"]);
    3.16 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    3.17 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.18 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.19 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.20 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.21 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.22 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.23 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.24 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.26 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
    3.27 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.28 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.30 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.31 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.32 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.33 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.34 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.35 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*);
    3.36 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
    3.37 +*}
    3.38 +ML {*
    3.39 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
    3.40 +*}
    3.41 +ML {*
    3.42 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.43  *}
    3.44  ML {*
    3.45  *}
    3.46 @@ -107,12 +140,8 @@
    3.47  *}
    3.48  ML {*
    3.49  *}
    3.50 -ML {*
    3.51 -*}
    3.52 -ML {*
    3.53 -*}
    3.54 -  use "Minisubpbl/400-start-meth-subpbl.sml"
    3.55 -  use "Minisubpbl/500-postcond.sml"
    3.56 +
    3.57 +
    3.58    ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*}
    3.59    ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
    3.60    use "Interpret/mstools.sml"       (*new 2010*)
    3.61 @@ -188,11 +217,25 @@
    3.62  insert_assumptions am
    3.63  *}
    3.64  ML {*
    3.65 -get_ctxt pt p |> insert_assumptions am
    3.66 +val ctxt = get_ctxt pt p |> insert_assumptions am
    3.67  *}
    3.68  ML {*
    3.69  from_pblobj_or_detail'
    3.70  *}
    3.71 +ML {*
    3.72 +from_pblobj'
    3.73 +*}
    3.74 +ML {*
    3.75 +*}
    3.76 +ML {*
    3.77 +*}
    3.78 +ML {*
    3.79 +*}
    3.80 +ML {*
    3.81 +*}
    3.82 +ML {*
    3.83 +*}
    3.84 +
    3.85  end
    3.86  
    3.87  (*=== inhibit exn ?=============================================================