1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Mon May 09 10:43:43 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Wed May 11 07:28:13 2011 +0200
     1.3 @@ -1134,38 +1134,29 @@
     1.4  
     1.5      (*. called only if no_met is specified .*)     
     1.6    | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
     1.7 -  let (* val Refine_Tacitly' (pI,pIre,_,_,_) = m;
     1.8 -         *)
     1.9 -    val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) = 
    1.10 -	get_obj I pt p;
    1.11 -    val {prls,met,ppc,thy,where_,...} = get_pbt pIre
    1.12 -    (*val pbl = init_pbl ppc --- Model_Problem recognizes probl=[]*)
    1.13 -    (*val pt = update_pbl pt p pbl;
    1.14 -    val pt = update_orispec pt p 
    1.15 -		(string_of_thy thy, pIre, 
    1.16 -		 if length met = 0 then e_metID else hd met);*)
    1.17 -    val (domID, metID) = (string_of_thy thy, 
    1.18 -		      if length met = 0 then e_metID else hd met)
    1.19 -    val ((p,_),_,_,pt) = 
    1.20 -	generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[])) 
    1.21 -		  (Uistate, e_ctxt) pos pt
    1.22 -    (*val pre = check_preconds thy prls where_ pbl
    1.23 -    val pb = foldl and_ (true, map fst pre)*)
    1.24 -    val (pbl, pre, pb) = ([], [], false)
    1.25 -  in ((p,Pbl), (pos,Uistate),
    1.26 -      Form' (PpcKF (0,EdUndef,(length p),Nundef,
    1.27 -		    (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
    1.28 -      Model_Problem, Safe, pt) end
    1.29 +      let
    1.30 +        val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) = get_obj I pt p;
    1.31 +        val {prls,met,ppc,thy,where_,...} = get_pbt pIre
    1.32 +        val (domID, metID) = 
    1.33 +          (string_of_thy thy, if length met = 0 then e_metID else hd met)
    1.34 +        val ((p,_),_,_,pt) = 
    1.35 +	        generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[])) 
    1.36 +		        (Uistate, e_ctxt) pos pt
    1.37 +        val (pbl, pre, pb) = ([], [], false)
    1.38 +      in ((p, Pbl), (pos, Uistate),
    1.39 +        Form' (PpcKF (0,EdUndef,(length p),Nundef,
    1.40 +		      (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),
    1.41 +        Model_Problem, Safe, pt)
    1.42 +      end
    1.43  
    1.44    | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
    1.45 -    let val (pos,_,_,pt) = generate1 (assoc_thy "Isac") 
    1.46 -				     (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
    1.47 -    in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd), 
    1.48 -	Model_Problem, Safe, pt) end
    1.49 +      let 
    1.50 +        val (pos,_,_,pt) = generate1 (assoc_thy "Isac") 
    1.51 +				  (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
    1.52 +      in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd), 
    1.53 +	      Model_Problem, Safe, pt)
    1.54 +      end
    1.55  
    1.56 -(* val (Specify_Problem' (pI, (ok, (itms, pre)))) = nxt; val (p,_) = p;
    1.57 -   val (Specify_Problem' (pI, (ok, (itms, pre)))) = m; val (p,_) = p;
    1.58 -   *)
    1.59    | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
    1.60    let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI), 
    1.61  		   meth=met, ...}) = get_obj I pt p;
    1.62 @@ -1567,7 +1558,7 @@
    1.63                val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;
    1.64  		          val pI' = refine_ori' pors pI;
    1.65  		        in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
    1.66 -		           (hd o #met o get_pbt) pI') end
    1.67 +		          (hd o #met o get_pbt) pI') end
    1.68  	        else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
    1.69  	      val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
    1.70  	      val dI = theory2theory' (maxthy thy thy');
    1.71 @@ -1720,23 +1711,13 @@
    1.72  
    1.73  (* called only once, if a Subproblem has been located in the script*)
    1.74  fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_)) ptp =
    1.75 -(* val (Subproblem'((_,pblID,metID),_,_,_,_),ptp) = (m', (pt,(p,p_)));
    1.76 -   *)
    1.77 -    (case metID of
    1.78 -	 ["no_met"] => 
    1.79 -	 (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
    1.80 -       | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
    1.81 -  (*all stored in tac_ itms     ^^^^^^^^^^*)
    1.82 +     (case metID of
    1.83 +	      ["no_met"] => 
    1.84 +	        (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)
    1.85 +      | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))
    1.86 +        (*all stored in tac_ itms^^^^^^^^^^*)
    1.87    | nxt_model_pbl tac_ _ = 
    1.88 -    error ("nxt_model_pbl: called by tac= "^tac_2str tac_);
    1.89 -(* run subp_rooteq.sml ''
    1.90 -   until nxt=("Subproblem",Subproblem ("SqRoot",["univariate","equation"]))
    1.91 -> val (_, (Subproblem'((_,pblID,metID),_,_,_,_),_,_,_,_,_)) =
    1.92 -      (last_elem o drop_last) ets'';
    1.93 -> val mst = (last_elem o drop_last) ets'';
    1.94 -> nxt_model_pbl mst;
    1.95 -val it = Refine_Tacitly ["univariate","equation"] : tac
    1.96 -*)
    1.97 +      error ("nxt_model_pbl: called by tac= " ^ tac_2str tac_);
    1.98  
    1.99  (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
   1.100  fun eq4 v (_,vts,_,_,_) = member op = vts v;