1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Wed May 11 08:25:40 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Wed May 11 14:58:07 2011 +0200
     1.3 @@ -723,41 +723,37 @@
     1.4  (*. is the input term t known in oris ? 
     1.5      give feedback on all(?) strange input;
     1.6      return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
     1.7 -(*WN.11.03: from lists*)
     1.8  fun is_known ctxt sel ori t =
     1.9 -(* val (ori,t)=(oris,term_of ct);
    1.10 -   *)
    1.11    let
    1.12      val _ = tracing ("RM is_known: t=" ^ term2str t);
    1.13      val ots = (distinct o flat o (map #5)) (ori:ori list);
    1.14      val oids = ((map (fst o dest_Free)) o distinct o 
    1.15 -		flat o (map vars)) ots;
    1.16 -    val (d,ts(*,pval*)) = split_dts t;
    1.17 +		  flat o (map vars)) ots;
    1.18 +    val (d, ts) = split_dts t;
    1.19      val ids = map (fst o dest_Free) 
    1.20        ((distinct o (flat o (map vars))) ts);
    1.21    in if (subtract op = oids ids) <> []
    1.22 -     then (("identifiers "^(strs2str' (subtract op = oids ids))^
    1.23 -	    " not in example"), e_ori_, [])
    1.24 +     then (("identifiers "^(strs2str' (subtract op = oids ids)) ^
    1.25 +	     " not in example"), e_ori_, [])
    1.26       else 
    1.27 -	 if d = e_term 
    1.28 -	 then 
    1.29 -	     if not (subset op = (map typeless ts, map typeless ots))
    1.30 -	     then (("terms '"^
    1.31 -		    ((strs2str' o 
    1.32 -                      (map (Print_Mode.setmp [] (Syntax.string_of_term 
    1.33 -					             ctxt)))) ts)^
    1.34 -		    "' not in example (typeless)"), e_ori_, [])
    1.35 -	     else (case seek_orits ctxt sel ts ori of
    1.36 -		       ("", ori_ as (_,_,_,d,ts), all) =>
    1.37 -		       (case test_types ctxt (d,ts) of
    1.38 -			    "" => ("", ori_, all)
    1.39 -			  | msg => (msg, e_ori_, []))
    1.40 -		     | (msg,_,_) => (msg, e_ori_, []))
    1.41 -	 else 
    1.42 -	     if member op = (map #4 ori) d
    1.43 -	     then seek_oridts ctxt sel (d,ts) ori
    1.44 -	     else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
    1.45 -		   " not in example", (0, [], sel, d, ts), [])
    1.46 +	     if d = e_term 
    1.47 +	     then 
    1.48 +	       if not (subset op = (map typeless ts, map typeless ots))
    1.49 +	       then (("terms '" ^ ((strs2str' o 
    1.50 +           (map (Print_Mode.setmp [] (Syntax.string_of_term ctxt)))) ts) ^
    1.51 +		       "' not in example (typeless)"), e_ori_, [])
    1.52 +	       else 
    1.53 +           (case seek_orits ctxt sel ts ori of
    1.54 +		          ("", ori_ as (_,_,_,d,ts), all) =>
    1.55 +		             (case test_types ctxt (d,ts) of
    1.56 +			              "" => ("", ori_, all)
    1.57 +			            | msg => (msg, e_ori_, []))
    1.58 +		        | (msg,_,_) => (msg, e_ori_, []))
    1.59 +	     else 
    1.60 +	       if member op = (map #4 ori) d
    1.61 +	       then seek_oridts ctxt sel (d,ts) ori
    1.62 +	       else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
    1.63 +		       " not in example", (0, [], sel, d, ts), [])
    1.64    end;
    1.65  
    1.66  
    1.67 @@ -1097,7 +1093,7 @@
    1.68  	    else pI' |> #ppc o get_pbt |> prep_ori fmz thy
    1.69      val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
    1.70  			(oris, (dI',pI',mI'),e_term)
    1.71 -      (*val pt = update_env pt [] (SOME (e_istate, ctxt))  GOON.WN110506*)
    1.72 +      (*val pt = update_env pt [] (SOME (e_istate, ctxt)) FIXME.WN110511*)
    1.73      val {ppc, prls, where_, ...} = get_pbt pI'
    1.74      val (pbl, pre, pb) = ([], [], false)
    1.75    in 
    1.76 @@ -1250,75 +1246,58 @@
    1.77    | specify m' _ _ _ = 
    1.78      error ("specify: not impl. for "^tac_2str m');
    1.79  
    1.80 -(* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp);
    1.81 -   val (sel, Add_Find  ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp);
    1.82 -   *)
    1.83  fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) = 
    1.84 -    let
    1.85 -      val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
    1.86 -		  probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
    1.87 -      val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.88 -      val cpI = if pI = e_pblID then pI' else pI;
    1.89 -      val ctxt = get_ctxt pt (p, Pbl);
    1.90 -    in case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
    1.91 -	   Add itm (*..union old input *) =>
    1.92 -(* val Add itm = appl_add thy sel oris pbl ppc ct;
    1.93 -   *)
    1.94 -	   let
    1.95 -	       (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
    1.96 -	       val pbl' = insert_ppc thy itm pbl
    1.97 -	       val (tac,tac_) = 
    1.98 -		   case sel of
    1.99 -		       "#Given" => (Add_Given    ct, Add_Given'   (ct, pbl'))
   1.100 -		     | "#Find"  => (Add_Find     ct, Add_Find'    (ct, pbl'))
   1.101 -		     | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
   1.102 -	       val ((p,Pbl),c,_,pt') = 
   1.103 -		   generate1 thy tac_ (Uistate, e_ctxt) (p,Pbl) pt
   1.104 -	   in ([(tac,tac_,((p,Pbl),(Uistate, e_ctxt)))], c, (pt',(p,Pbl))):calcstate' end
   1.105 -	       
   1.106 -	 | Err msg => 
   1.107 -	   (*TODO.WN03 pass error-msgs to the frontend..
   1.108 -             FIXME ..and dont abuse a tactic for that purpose*)
   1.109 -	   ([(Tac msg,
   1.110 -	      Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
   1.111 -	      (e_pos', (e_istate, e_ctxt)))], [], ptp) 
   1.112 -    end
   1.113 +      let
   1.114 +        val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
   1.115 +		      probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
   1.116 +        val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
   1.117 +        val cpI = if pI = e_pblID then pI' else pI;
   1.118 +        val ctxt = get_ctxt pt (p, Pbl); (*FIXME.WN110511 repair*)
   1.119 +      in
   1.120 +        case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
   1.121 +	        Add itm (*..union old input *) =>
   1.122 +	          let
   1.123 +	            (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
   1.124 +	            val pbl' = insert_ppc thy itm pbl
   1.125 +	            val (tac,tac_) = 
   1.126 +		            case sel of
   1.127 +		              "#Given" => (Add_Given    ct, Add_Given'   (ct, pbl'))
   1.128 +		            | "#Find"  => (Add_Find     ct, Add_Find'    (ct, pbl'))
   1.129 +		            | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
   1.130 +	            val ((p,Pbl),c,_,pt') = 
   1.131 +		            generate1 thy tac_ (Uistate, e_ctxt) (p,Pbl) pt
   1.132 +	          in ([(tac,tac_,((p,Pbl),(Uistate, e_ctxt)))], c, (pt',(p,Pbl))):calcstate' 
   1.133 +            end	       
   1.134 +	      | Err msg => 
   1.135 +	          (*TODO.WN03 pass error-msgs to the frontend..
   1.136 +              FIXME ..and dont abuse a tactic for that purpose*)
   1.137 +	          ([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
   1.138 +	            (e_pos', (e_istate, e_ctxt)))], [], ptp) 
   1.139 +      end
   1.140 +  | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) = 
   1.141 +      let
   1.142 +        val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
   1.143 +		      probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
   1.144 +        val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
   1.145 +        val cmI = if mI = e_metID then mI' else mI;
   1.146 +        val ctxt = get_ctxt pt (p,Met); (*FIXME.WN110511 repair*)
   1.147 +      in 
   1.148 +        case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
   1.149 +          Add itm (*..union old input *) =>
   1.150 +	          let
   1.151 +	            val met' = insert_ppc thy itm met;
   1.152 +	            val (tac,tac_) = 
   1.153 +	              case sel of
   1.154 +		              "#Given" => (Add_Given    ct, Add_Given'   (ct, met'))
   1.155 +		            | "#Find"  => (Add_Find     ct, Add_Find'    (ct, met'))
   1.156 +		            | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
   1.157 +	            val ((p,Met),c,_,pt') = 
   1.158 +	              generate1 thy tac_ (Uistate, e_ctxt) (p,Met) pt
   1.159 +	          in ([(tac,tac_,((p,Met), (Uistate, e_ctxt)))], c, (pt',(p,Met))) end
   1.160 +        | Err msg => ([(*tacis*)], [], ptp) 
   1.161 +          (*nxt_me collects tacis until not hide; here just no progress*)
   1.162 +      end;
   1.163  
   1.164 -(* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
   1.165 -   val (_,_,f,nxt',_,pt')= nxt_specif_additem sel ct (p,Met) c pt;
   1.166 -  *)
   1.167 -  | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) = 
   1.168 -    let
   1.169 -      val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
   1.170 -		  probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
   1.171 -      val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
   1.172 -      val cmI = if mI = e_metID then mI' else mI;
   1.173 -      val ctxt = get_ctxt pt (p,Met);
   1.174 -    in case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
   1.175 -      Add itm (*..union old input *) =>
   1.176 -	let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
   1.177 -               *)
   1.178 -	  val met' = insert_ppc thy itm met;
   1.179 -	  val (tac,tac_) = 
   1.180 -	      case sel of
   1.181 -		  "#Given" => (Add_Given    ct, Add_Given'   (ct, met'))
   1.182 -		| "#Find"  => (Add_Find     ct, Add_Find'    (ct, met'))
   1.183 -		| "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
   1.184 -	  val ((p,Met),c,_,pt') = 
   1.185 -	      generate1 thy tac_ (Uistate, e_ctxt) (p,Met) pt
   1.186 -	in ([(tac,tac_,((p,Met), (Uistate, e_ctxt)))], c, (pt',(p,Met))) end
   1.187 -
   1.188 -    | Err msg => ([(*tacis*)], [], ptp) 
   1.189 -    (*nxt_me collects tacis until not hide; here just no progress*)
   1.190 -    end;
   1.191 -
   1.192 -(* ori
   1.193 -val (msg,itm) = appl_add thy sel oris ppc ct;
   1.194 -val (Cor(d,ts)) = #5 itm;
   1.195 -map (atomty) ts;
   1.196 -
   1.197 -pre
   1.198 -*)
   1.199  fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
   1.200      (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt) 
   1.201  			      handle _ => error ("ori2Coritm: dsc "^
   1.202 @@ -1394,22 +1373,22 @@
   1.203  (*WN.24.10.03        ~~~~~~~~~~~~~~   -> tac     -> tac_      -> -"- as arg*)
   1.204  (*WN.24.10.03        fun nxt_solv   = ...................................??*)
   1.205  fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
   1.206 -  let
   1.207 -    val PblObj {origin = (oris, ospec, _), probl, spec, ...} = get_obj I pt p
   1.208 -    val (dI, pI, mI) = some_spec ospec spec
   1.209 -    val thy = assoc_thy dI
   1.210 -    val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
   1.211 -    val {cas, ppc, ...} = get_pbt pI
   1.212 -    val pbl = init_pbl ppc (* fill in descriptions *)
   1.213 -    (*----------------if you think, this should be done by the Dialog 
   1.214 -     in the java front-end, search there for WN060225-modelProblem----*)
   1.215 -    val (pbl, met) = 
   1.216 -      case cas of NONE => (pbl, [])
   1.217 -			| _ => complete_mod_ (oris, mpc, ppc, probl)
   1.218 -    (*----------------------------------------------------------------*)
   1.219 -    val tac_ = Model_Problem' (pI, pbl, met)
   1.220 -    val (pos,c,_,pt) = generate1 thy tac_ (Uistate, e_ctxt) pos pt
   1.221 -  in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
   1.222 +    let
   1.223 +      val PblObj {origin = (oris, ospec, _), probl, spec, ...} = get_obj I pt p
   1.224 +      val (dI, pI, mI) = some_spec ospec spec
   1.225 +      val thy = assoc_thy dI
   1.226 +      val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
   1.227 +      val {cas, ppc, ...} = get_pbt pI
   1.228 +      val pbl = init_pbl ppc (* fill in descriptions *)
   1.229 +      (*----------------if you think, this should be done by the Dialog 
   1.230 +       in the java front-end, search there for WN060225-modelProblem----*)
   1.231 +      val (pbl, met) = 
   1.232 +        case cas of NONE => (pbl, [])
   1.233 +  			| _ => complete_mod_ (oris, mpc, ppc, probl)
   1.234 +      (*----------------------------------------------------------------*)
   1.235 +      val tac_ = Model_Problem' (pI, pbl, met)
   1.236 +      val (pos,c,_,pt) = generate1 thy tac_ (Uistate, e_ctxt) pos pt
   1.237 +    in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
   1.238  
   1.239    | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
   1.240    | nxt_specif (Add_Find  ct) ptp = nxt_specif_additem "#Find"  ct ptp
   1.241 @@ -1417,92 +1396,101 @@
   1.242  
   1.243      (*. called only if no_met is specified .*)     
   1.244    | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
   1.245 -    let val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
   1.246 -	val opt = refine_ori oris pI
   1.247 -    in case opt of
   1.248 -	   SOME pI' => 
   1.249 -	   let val {met,ppc,...} = get_pbt pI'
   1.250 -	       val pbl = init_pbl ppc
   1.251 -	       (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
   1.252 -	       val mI = if length met = 0 then e_metID else hd met
   1.253 -               val thy = assoc_thy dI
   1.254 -	       val (pos,c,_,pt) = 
   1.255 -		   generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[])) 
   1.256 -			     (Uistate, e_ctxt) pos pt
   1.257 -	   in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
   1.258 -		 (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
   1.259 -	 | NONE => ([], [], ptp)
   1.260 -    end
   1.261 +      let 
   1.262 +        val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
   1.263 +        val opt = refine_ori oris pI
   1.264 +      in 
   1.265 +        case opt of
   1.266 +	        SOME pI' => 
   1.267 +	          let 
   1.268 +              val {met,ppc,...} = get_pbt pI'
   1.269 +	            val pbl = init_pbl ppc
   1.270 +	            (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
   1.271 +	            val mI = if length met = 0 then e_metID else hd met
   1.272 +              val thy = assoc_thy dI
   1.273 +	            val (pos,c,_,pt) = 
   1.274 +		            generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[])) 
   1.275 +			            (Uistate, e_ctxt) pos pt
   1.276 +	          in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
   1.277 +		          (pos, (Uistate, e_ctxt)))], c, (pt,pos)) 
   1.278 +            end
   1.279 +	      | NONE => ([], [], ptp)
   1.280 +      end
   1.281  
   1.282    | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
   1.283 -    let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
   1.284 -		     probl, ...}) = get_obj I pt p
   1.285 -	val thy = if dI' = e_domID then dI else dI'
   1.286 -    in case refine_pbl (assoc_thy thy) pI probl of
   1.287 -	   NONE => ([], [], ptp)
   1.288 -	 | SOME (rfd as (pI',_)) => 
   1.289 -	   let val (pos,c,_,pt) = 
   1.290 -		   generate1 (assoc_thy thy) 
   1.291 -			     (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
   1.292 -	    in ([(Refine_Problem pI, Refine_Problem' rfd,
   1.293 -			    (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
   1.294 -    end
   1.295 +      let
   1.296 +        val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_), probl, ...}) = get_obj I pt p
   1.297 +	      val thy = if dI' = e_domID then dI else dI'
   1.298 +      in 
   1.299 +        case refine_pbl (assoc_thy thy) pI probl of
   1.300 +	        NONE => ([], [], ptp)
   1.301 +	      | SOME (rfd as (pI',_)) => 
   1.302 +	          let 
   1.303 +              val (pos,c,_,pt) = generate1 (assoc_thy thy) 
   1.304 +			          (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
   1.305 +	          in ([(Refine_Problem pI, Refine_Problem' rfd,
   1.306 +			        (pos, (Uistate, e_ctxt)))], c, (pt,pos))
   1.307 +            end
   1.308 +      end
   1.309  
   1.310    | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
   1.311 -    let val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_),
   1.312 -		     probl, ...}) = get_obj I pt p;
   1.313 -	val thy = assoc_thy (if dI' = e_domID then dI else dI');
   1.314 +      let
   1.315 +        val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ...}) = get_obj I pt p;
   1.316 +	      val thy = assoc_thy (if dI' = e_domID then dI else dI');
   1.317          val {ppc,where_,prls,...} = get_pbt pI
   1.318 -	val pbl as (_,(itms,_)) = 
   1.319 -	    if pI'=e_pblID andalso pI=e_pblID
   1.320 -	    then (false, (init_pbl ppc, []))
   1.321 -	    else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
   1.322 -	(*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
   1.323 -	val ((p,Pbl),c,_,pt)= 
   1.324 -	    generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, e_ctxt) pos pt
   1.325 -    in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
   1.326 -		    (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
   1.327 +	      val pbl as (_,(itms,_)) = 
   1.328 +	        if pI'=e_pblID andalso pI=e_pblID
   1.329 +	        then (false, (init_pbl ppc, []))
   1.330 +	        else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
   1.331 +	        (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
   1.332 +	      val ((p,Pbl),c,_,pt) = 
   1.333 +	        generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, e_ctxt) pos pt
   1.334 +      in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
   1.335 +		    (pos,(Uistate, e_ctxt)))], c, (pt,pos))
   1.336 +      end
   1.337  
   1.338    (*transfers oris (not required in pbl) to met-model for script-env
   1.339      FIXME.WN.8.03: application of several mIDs to SAME model?*)
   1.340    | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) = 
   1.341 -  let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI), 
   1.342 -		   meth=met, ...}) = get_obj I pt p;
   1.343 -    val {ppc,pre,prls,...} = get_met mID
   1.344 -    val thy = assoc_thy dI
   1.345 -    val oris = add_field' thy ppc oris;
   1.346 -    val dI'' = if dI=e_domID then dI' else dI;
   1.347 -    val pI'' = if pI = e_pblID then pI' else pI;
   1.348 -    val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
   1.349 -    val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
   1.350 -    val (pos,c,_,pt)= 
   1.351 -	generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
   1.352 -  in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
   1.353 -		  (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end    
   1.354 +      let
   1.355 +        val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI), meth=met, ...}) = get_obj I pt p;
   1.356 +        val {ppc,pre,prls,...} = get_met mID
   1.357 +        val thy = assoc_thy dI
   1.358 +        val oris = add_field' thy ppc oris;
   1.359 +        val dI'' = if dI=e_domID then dI' else dI;
   1.360 +        val pI'' = if pI = e_pblID then pI' else pI;
   1.361 +        val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
   1.362 +        val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
   1.363 +        val (pos,c,_,pt)= 
   1.364 +	        generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
   1.365 +      in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
   1.366 +		    (pos,(Uistate, e_ctxt)))], c, (pt,pos)) 
   1.367 +      end    
   1.368  
   1.369    | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
   1.370 -    let val (dI',_,_) = get_obj g_spec pt p
   1.371 -	val (pos,c,_,pt) = 
   1.372 -	    generate1 (assoc_thy "Isac") (Specify_Theory' dI) 
   1.373 -		      (Uistate, e_ctxt) pos pt
   1.374 -    in  (*FIXXXME: check if pbl can still be parsed*)
   1.375 -	([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
   1.376 -	 (pt, pos)) end
   1.377 +      let
   1.378 +        val (dI',_,_) = get_obj g_spec pt p
   1.379 +	      val (pos,c,_,pt) = 
   1.380 +	        generate1 (assoc_thy "Isac") (Specify_Theory' dI)  (Uistate, e_ctxt) pos pt
   1.381 +      in  (*FIXXXME: check if pbl can still be parsed*)
   1.382 +	      ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
   1.383 +	        (pt, pos))
   1.384 +      end
   1.385  
   1.386    | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
   1.387 -    let val (dI',_,_) = get_obj g_spec pt p
   1.388 -	val (pos,c,_,pt) = 
   1.389 -	    generate1 (assoc_thy "Isac") (Specify_Theory' dI) 
   1.390 -		      (Uistate, e_ctxt) pos pt
   1.391 -    in  (*FIXXXME: check if met can still be parsed*)
   1.392 -	([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
   1.393 -	 (pt, pos)) end
   1.394 +      let
   1.395 +        val (dI',_,_) = get_obj g_spec pt p
   1.396 +	      val (pos,c,_,pt) = 
   1.397 +	        generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, e_ctxt) pos pt
   1.398 +      in  (*FIXXXME: check if met can still be parsed*)
   1.399 +	      ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
   1.400 +	        (pt, pos))
   1.401 +      end
   1.402  
   1.403    | nxt_specif m' _ = 
   1.404      error ("nxt_specif: not impl. for "^tac2str m');
   1.405  
   1.406 -(*.get the values from oris; handle the term list w.r.t. penv.*)
   1.407 -
   1.408 +(* get the values from oris; handle the term list w.r.t. penv *)
   1.409  local infix mem;
   1.410  fun x mem [] = false
   1.411    | x mem (y :: ys) = x = y orelse x mem ys;
   1.412 @@ -1512,8 +1500,6 @@
   1.413       (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
   1.414  end;
   1.415  
   1.416 -
   1.417 -
   1.418  (* create a calc-tree with oris via an cas.refined pbl *)
   1.419  fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
   1.420        if pI <> [] 
   1.421 @@ -1568,7 +1554,7 @@
   1.422  		      | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
   1.423          val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
   1.424  				  (pors, (dI, pI, mI), hdl)
   1.425 -          (* val pt = update_env pt [] (SOME (e_istate, pctxt)) GOON.WN110506*)
   1.426 +          (* val pt = update_env pt [] (SOME (e_istate, pctxt)) FIXME.WN110511*)
   1.427        in ((pt, ([], Pbl)), 
   1.428          fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
   1.429        end;

     2.1 --- a/src/Tools/isac/Interpret/ctree.sml	Wed May 11 08:25:40 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Wed May 11 14:58:07 2011 +0200
     2.3 @@ -1344,7 +1344,7 @@
     2.4         | (NONE  , NONE) => (e_istate, e_ctxt)
     2.5         | (SOME i, _) => i);
     2.6  fun get_istate pt p = get_loc pt p |> #1;
     2.7 -fun get_ctxt pt p = get_loc pt p |> #2;
     2.8 +fun get_ctxt pt p = get_loc pt p |> #2; (*FIXME.WN110511 delete*)
     2.9  
    2.10  fun get_assumptions_ pt p = get_ctxt pt p |> get_assumptions;
    2.11  

     3.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Wed May 11 08:25:40 2011 +0200
     3.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Wed May 11 14:58:07 2011 +0200
     3.3 @@ -208,7 +208,7 @@
     3.4  		            (case (if member op = [Pbl,Met] p_
     3.5  			                   andalso is_none (get_obj g_env pt (fst p))
     3.6  			                        (*^^^^^^^^: Apply_Method without init_form*)
     3.7 -			                 then nxt_specify_ (pt,ip) 
     3.8 +			                 then nxt_specify_ (pt, ip) 
     3.9                         else nxt_solve_ (pt,ip) )
    3.10  			                handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality///"*) of
    3.11  		               cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*)

     4.1 --- a/src/Tools/isac/Interpret/ptyps.sml	Wed May 11 08:25:40 2011 +0200
     4.2 +++ b/src/Tools/isac/Interpret/ptyps.sml	Wed May 11 14:58:07 2011 +0200
     4.3 @@ -269,7 +269,7 @@
     4.4     *)
     4.5  
     4.6  fun prep_ori [] _ _ = ([], e_ctxt)
     4.7 -  | prep_ori fmz thy pbt =
     4.8 +  | prep_ori fmz thy pbt = (*FIXME.WN110511 ?return ctxt?*)
     4.9        let
    4.10          val ctxt = ProofContext.init_global thy |> fold declare_constraints fmz;
    4.11          val ori = map (add_field thy pbt o split_dts o the o parseNEW ctxt) fmz

     5.1 --- a/src/Tools/isac/ProgLang/scrtools.sml	Wed May 11 08:25:40 2011 +0200
     5.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml	Wed May 11 14:58:07 2011 +0200
     5.3 @@ -72,6 +72,7 @@
     5.4  val it = false : bool
     5.5  *)
     5.6  
     5.7 +(*WN110511  Const would be clearer !!! TODO combine both ...
     5.8  fun is_dsc (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) = true
     5.9    | is_dsc (Const(_,Type("fun",[_,Type("Tools.una",_)]))) = true
    5.10    | is_dsc (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true
    5.11 @@ -82,6 +83,7 @@
    5.12    | is_dsc (Const(_,Type("fun",[_,Type("Tools.unknow",_)])))= true
    5.13    | is_dsc (Const(_,Type("fun",[_,Type("Tools.cpy",_)])))= true
    5.14    | is_dsc _ = false;
    5.15 +*)
    5.16  fun is_dsc term = 
    5.17      (case (range_type o type_of) term of
    5.18  	Type("Tools.nam",_) => true

     6.1 --- a/test/Tools/isac/Interpret/mathengine.sml	Wed May 11 08:25:40 2011 +0200
     6.2 +++ b/test/Tools/isac/Interpret/mathengine.sml	Wed May 11 14:58:07 2011 +0200
     6.3 @@ -10,6 +10,7 @@
     6.4  "----------- change to parse ctxt -----------------------";
     6.5  "----------- debugging setContext..pbl_ -----------------";
     6.6  "----------- tryrefine ----------------------------------";
     6.7 +"----------- fun step: Apply_Method without init_form ---";
     6.8  "----------- fun step -----------------------------------";
     6.9  "----------- fun autocalc -------------------------------";
    6.10  "----------- fun autoCalculate --------------------------";
    6.11 @@ -209,6 +210,22 @@
    6.12  
    6.13  ===== inhibit exn ?===========================================================*)
    6.14  
    6.15 +"----------- fun step: Apply_Method without init_form ---";
    6.16 +"----------- fun step: Apply_Method without init_form ---";
    6.17 +"----------- fun step: Apply_Method without init_form ---";
    6.18 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    6.19 +val (dI',pI',mI') =
    6.20 +  ("Test", ["sqroot-test","univariate","equation","test"],
    6.21 +   ["Test","squ-equ-test-subpbl1"]);
    6.22 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    6.23 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
    6.24 +val ("ok", (_, _, (pt, p))) = locatetac tac (pt,p);
    6.25 +"~~~~~ fun step, args:"; val (ip as (_,p_), ptp as (pt,p), tacis) = (p, (pt, e_pos'), []);
    6.26 +val pIopt = get_pblID (pt,ip);
    6.27 +ip = ([],Res) (*false*);
    6.28 +val SOME pI = pIopt;
    6.29 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p))
    6.30 +			                          (*^^^^^^^^: Apply_Method without init_form*)
    6.31  
    6.32  "----------- fun step -----------------------------------";
    6.33  "----------- fun step -----------------------------------";

     7.1 --- a/test/Tools/isac/Interpret/mstools.sml	Wed May 11 08:25:40 2011 +0200
     7.2 +++ b/test/Tools/isac/Interpret/mstools.sml	Wed May 11 14:58:07 2011 +0200
     7.3 @@ -12,6 +12,7 @@
     7.4  "----------- fun get_assumptions, fun get_environments --";
     7.5  "----------- fun transfer_from_subproblem ---------------";
     7.6  "----------- all handling ctxt in minimsubpbl x+1=2 -----";
     7.7 +"----------- go through Model_Problem until nxt_tac -----";
     7.8  "--------------------------------------------------------";
     7.9  "--------------------------------------------------------";
    7.10  "--------------------------------------------------------";
    7.11 @@ -96,4 +97,73 @@
    7.12  (*nxt = Tac..ERROR*)
    7.13  ---------------------------GOON *)
    7.14  
    7.15 +"----------- go through Model_Problem until nxt_tac -----";
    7.16 +"----------- go through Model_Problem until nxt_tac -----";
    7.17 +"----------- go through Model_Problem until nxt_tac -----";
    7.18 +(*FIXME.WN110511 delete this test? (goes through "Model_Problem until nxt_tac)*)
    7.19 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    7.20 +val (dI',pI',mI') =
    7.21 +  ("Test", ["sqroot-test","univariate","equation","test"],
    7.22 +   ["Test","squ-equ-test-subpbl1"]);
    7.23 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    7.24 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    7.25 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    7.26 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    7.27 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    7.28 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    7.29 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    7.30 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    7.31 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    7.32 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    7.33 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Subproblem",*)
    7.34 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Model_Problem",*)
    7.35 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
    7.36 +val (pt, p) = case locatetac tac (pt,p) of
    7.37 +	("ok", (_, _, ptp))  => ptp | _ => error "script.sml locatetac";
    7.38 +"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
    7.39 +val pIopt = get_pblID (pt,ip);
    7.40 +tacis; (*= []*)
    7.41 +pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
    7.42 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= true*)
    7.43 +"~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt, ip);
    7.44 +val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
    7.45 +			  probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
    7.46 +just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false=oldNB*)
    7.47 +val cpI = if pI = e_pblID then pI' else pI;
    7.48 +		val cmI = if mI = e_metID then mI' else mI;
    7.49 +		val {ppc, prls, where_, ...} = get_pbt cpI;
    7.50 +		val pre = check_preconds "thy 100820" prls where_ probl;
    7.51 +		val pb = foldl and_ (true, map fst pre);
    7.52 +val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) 
    7.53 +			    (ppc, (#ppc o get_met) cmI) (dI, pI, mI); (*tac = Add_Given "equality (-1 + x = 0)"*)
    7.54 +"~~~~~ fun nxt_specif, args:"; val (Add_Given ct, ptp) = (tac, ptp);
    7.55 +"~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
    7.56 +val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
    7.57 +		  probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
    7.58 +val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    7.59 +val cpI = if pI = e_pblID then pI' else pI;
    7.60 +val ctxt = get_ctxt pt (p, Pbl);
    7.61 +"~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct);
    7.62 +val SOME t = parseNEW ctxt str;
    7.63 +is_known ctxt sel oris t;
    7.64 +"~~~~~ fun is_known, args:"; val (ctxt, sel, ori, t) = (ctxt, sel, oris, t);
    7.65 +val _ = tracing ("RM is_known: t=" ^ term2str t);
    7.66 +val ots = (distinct o flat o (map #5)) (ori:ori list);
    7.67 +val oids = ((map (fst o dest_Free)) o distinct o flat o (map vars)) ots;
    7.68 +val (d, ts) = split_dts t;
    7.69 +"~~~~~ fun split_dts, args:"; val (t as d $ arg) = t;
    7.70 +(*if is_dsc d then () else error "TODO";*)
    7.71 +if not (is_dsc d) then () else error "TODO";
    7.72 +"----- these were the errors (call hierarchy from bottom up)";
    7.73 +appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct;(*WAS
    7.74 +Err "[error] appl_add: is_known: identifiers [equality] not in example"*)
    7.75 +nxt_specif_additem "#Given" ct ptp;(*WAS
    7.76 +Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
    7.77 +nxt_specif tac ptp;(*WAS
    7.78 +Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
    7.79 +nxt_specify_ (pt,ip); (*WAS
    7.80 +Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
    7.81 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS
    7.82 +Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
    7.83  
    7.84 +

     8.1 --- a/test/Tools/isac/Interpret/script.sml	Wed May 11 08:25:40 2011 +0200
     8.2 +++ b/test/Tools/isac/Interpret/script.sml	Wed May 11 14:58:07 2011 +0200
     8.3 @@ -14,6 +14,7 @@
     8.4  "----------- fun sel_appl_atomic_tacs ----------------------------";
     8.5  "----------- fun init_form, fun get_stac -------------------------";
     8.6  "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
     8.7 +"----------- x+1=2 set ctxt in Subproblem ------------------------";
     8.8  "-----------------------------------------------------------------";
     8.9  "-----------------------------------------------------------------";
    8.10  "-----------------------------------------------------------------";
    8.11 @@ -328,3 +329,7 @@
    8.12  | _ => error "script.sml x+1=2 start SubProblem from script";
    8.13  
    8.14  
    8.15 +"----------- x+1=2 set ctxt in Subproblem ------------------------";
    8.16 +"----------- x+1=2 set ctxt in Subproblem ------------------------";
    8.17 +"----------- x+1=2 set ctxt in Subproblem ------------------------";
    8.18 +

     9.1 --- a/test/Tools/isac/Test_Isac.thy	Wed May 11 08:25:40 2011 +0200
     9.2 +++ b/test/Tools/isac/Test_Isac.thy	Wed May 11 14:58:07 2011 +0200
     9.3 @@ -85,44 +85,9 @@
     9.4  (*use "ProgLang/tools.sml"            2002*)
     9.5    ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
     9.6    ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
     9.7 -ML {*
     9.8 -*}
     9.9 -
    9.10    use "Interpret/mstools.sml"       (*new 2010*)
    9.11  
    9.12  ML {*
    9.13 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    9.14 -val (dI',pI',mI') =
    9.15 -  ("Test", ["sqroot-test","univariate","equation","test"],
    9.16 -   ["Test","squ-equ-test-subpbl1"]);
    9.17 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    9.18 -"~~~~~ fun me, args:"; val (_,tac) = nxt;
    9.19 -val ("ok", (_, _, (pt, p))) = locatetac tac (pt,p);
    9.20 -"~~~~~ fun step, args:"; val (ip as (_,p_), ptp as (pt,p), tacis) = (p, (pt, e_pos'), []);
    9.21 -*}
    9.22 -ML {*
    9.23 -val pIopt = get_pblID (pt,ip);
    9.24 -ip = ([],Res) (*false*);
    9.25 -val SOME pI = pIopt;
    9.26 -member op = [Pbl,Met] p_
    9.27 -			                   andalso is_none (get_obj g_env pt (fst p))
    9.28 -*}
    9.29 -ML {*
    9.30 -*}
    9.31 -ML {*
    9.32 -*}
    9.33 -ML {*
    9.34 -step p ((pt, e_pos'),[]);
    9.35 -*}
    9.36 -ML {*
    9.37 -*}
    9.38 -ML {*
    9.39 -*}
    9.40 -ML {*
    9.41 -*}
    9.42 -ML {*
    9.43 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    9.44 -
    9.45  *}
    9.46  
    9.47    use "Interpret/ctree.sml"         (*!...see(25)*)

    10.1 --- a/test/Tools/isac/Test_Some.thy	Wed May 11 08:25:40 2011 +0200
    10.2 +++ b/test/Tools/isac/Test_Some.thy	Wed May 11 14:58:07 2011 +0200
    10.3 @@ -1,43 +1,16 @@
    10.4 -(* Title: Run_Tests as long Isac is not available: REPLACE 'IMPORTS'
    10.5 +(* Title:  run tests on a particular test file
    10.6     Author: Walther Neuper 101001
    10.7     (c) copyright due to lincense terms.
    10.8 -
    10.9 -$ cd /usr/local/isabisac/test/Tools/isac
   10.10 -$ /usr/local/isabisac/bin/isabelle emacs Test_Some.thy &
   10.11  *)
   10.12  
   10.13  theory Test_Some imports Isac begin
   10.14 -(*..................................########..................................*)
   10.15  
   10.16  ML {*
   10.17 -get_loc;
   10.18 -g_loc;
   10.19 -get_obj;
   10.20 -specify_additem;
   10.21 -"====================== it ======================";
   10.22 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
   10.23 -val (_, ctxt) = prep_ori fmz @{theory} [];
   10.24 -val to_parse = "equality (x + 1 = 2)"; 
   10.25 -parseNEW ctxt to_parse |> the;
   10.26 -parse @{theory} to_parse |> the |> term_of;
   10.27 -parseNEW ctxt "x";
   10.28  *}
   10.29  
   10.30 -
   10.31  ML{* writeln "**** run the test ***************************************" *}
   10.32  
   10.33 -ML {*
   10.34 -fun term2st t = Print_Mode.setmp [] (Syntax.string_of_term
   10.35 -(ProofContext.init_global (Thy_Info.get_theory "Rational"))) t;
   10.36 -(*..............................................########......................*)
   10.37 -*}
   10.38 -
   10.39 -ML {*pos'2str;
   10.40 -
   10.41 -
   10.42 -*}
   10.43 -ML {*print_depth 999*}
   10.44 -use"../../../test/Tools/isac/Interpret/appl.sml"
   10.45 +use"../../../test/Tools/isac/Interpret/script.sml"
   10.46  
   10.47  end
   10.48