1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Fri May 13 14:15:59 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Fri May 13 17:19:38 2011 +0200
     1.3 @@ -1000,13 +1000,12 @@
     1.4  fun specify_additem sel (ct,_) (p,Met) c pt = 
     1.5      let
     1.6        val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
     1.7 -		    probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
     1.8 +		    probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
     1.9        val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.10      (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
    1.11        val cpI = if pI = e_pblID then pI' else pI;
    1.12        val cmI = if mI = e_metID then mI' else mI;
    1.13        val {ppc,pre,prls,...} = get_met cmI;
    1.14 -      val ctxt = get_ctxt pt (p,Met);
    1.15      in case appl_add ctxt sel oris met ppc ct of
    1.16        Add itm (*..union old input *) =>
    1.17  	let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
    1.18 @@ -1043,12 +1042,11 @@
    1.19  | specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt = 
    1.20      let
    1.21        val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
    1.22 -		    probl=pbl,spec=(dI,pI,mI), ...}) = get_obj I pt p;
    1.23 +		    probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
    1.24        val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.25        val cpI = if pI = e_pblID then pI' else pI;
    1.26        val cmI = if mI = e_metID then mI' else mI;
    1.27        val {ppc,where_,prls,...} = get_pbt cpI;
    1.28 -      val ctxt = get_ctxt pt pos;
    1.29      in case appl_add ctxt sel oris pbl ppc ct of
    1.30        Add itm (*..union old input *) =>
    1.31        (* val Add itm = appl_add thy sel oris pbl ppc ct;
    1.32 @@ -1093,7 +1091,7 @@
    1.33  	    else pI' |> #ppc o get_pbt |> prep_ori fmz thy
    1.34      val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
    1.35  			(oris, (dI',pI',mI'),e_term)
    1.36 -      (*val pt = update_env pt [] (SOME (e_istate, ctxt)) FIXME.WN110511*)
    1.37 +      val pt = update_ctxt pt [] ctxt (*FIXME.WN110511*)
    1.38      val {ppc, prls, where_, ...} = get_pbt pI'
    1.39      val (pbl, pre, pb) = ([], [], false)
    1.40    in 
    1.41 @@ -1247,10 +1245,9 @@
    1.42  fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) = 
    1.43        let
    1.44          val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
    1.45 -		      probl=pbl,spec=(dI,pI,_), ...}) = get_obj I pt p;
    1.46 +		      probl=pbl,spec=(dI,pI,_), ctxt, ...}) = get_obj I pt p;
    1.47          val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.48          val cpI = if pI = e_pblID then pI' else pI;
    1.49 -        val ctxt = get_ctxt pt (p, Pbl); (*FIXME.WN110511 repair*)
    1.50        in
    1.51          case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
    1.52  	        Add itm (*..union old input *) =>
    1.53 @@ -1275,10 +1272,9 @@
    1.54    | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) = 
    1.55        let
    1.56          val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
    1.57 -		      probl=pbl,spec=(dI,pI,mI), ...}) = get_obj I pt p;
    1.58 +		      probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
    1.59          val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    1.60          val cmI = if mI = e_metID then mI' else mI;
    1.61 -        val ctxt = get_ctxt pt (p,Met); (*FIXME.WN110511 repair*)
    1.62        in 
    1.63          case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
    1.64            Add itm (*..union old input *) =>
    1.65 @@ -1553,7 +1549,7 @@
    1.66  		      | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
    1.67          val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
    1.68  				  (pors, (dI, pI, mI), hdl)
    1.69 -          (* val pt = update_env pt [] (SOME (e_istate, pctxt)) FIXME.WN110511*)
    1.70 +        val pt = update_ctxt pt [] pctxt (* FIXME.WN110511*)
    1.71        in ((pt, ([], Pbl)), 
    1.72          fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
    1.73        end;

     2.1 --- a/src/Tools/isac/Interpret/ctree.sml	Fri May 13 14:15:59 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Fri May 13 17:19:38 2011 +0200
     2.3 @@ -755,8 +755,7 @@
     2.4  	    env   : (istate * Proof.context) option,
     2.5                                  (* istate only for initac in script
     2.6                                     context for specify phase on this node NO..
     2.7 -..NO: this conflicts with init_form/initac: see Apply_Method without init_form
     2.8 -in fun step. Replaced by hack FIXME.WN110511 fun update_pbl_ctxt, see [*] below *)
     2.9 +..NO: this conflicts with init_form/initac: see Apply_Method without init_form *)
    2.10  	    loc   : (istate * Proof.context) option * (istate * (* like PrfObj *)
    2.11                  Proof.context) option, (* for spec-phase [*], NO..
    2.12  ..NO: raises errors not tracable on WN110513 [**]*)                               
    2.13 @@ -1284,60 +1283,18 @@
    2.14  fun update_pblID  pt pos x = appl_obj (repl_pblID  x) pt pos;
    2.15  fun update_metID  pt pos x = appl_obj (repl_metID  x) pt pos;
    2.16  fun update_spec   pt pos x = appl_obj (repl_spec   x) pt pos;
    2.17 -
    2.18  fun update_pbl    pt pos x = appl_obj (repl_pbl    x) pt pos;
    2.19  fun update_pblppc pt pos x = appl_obj (repl_pbl    x) pt pos;
    2.20 -
    2.21  fun update_met    pt pos x = appl_obj (repl_met    x) pt pos;
    2.22 -(*1.09.01 ----
    2.23 -fun update_metppc pt pos x = 
    2.24 -  let val {rew_ord'=od,rls'=rs,asm_thm=at,asm_rls=ar,...} =
    2.25 -    get_obj g_met pt pos
    2.26 -  in appl_obj (repl_met 
    2.27 -     {rew_ord'=od,rls'=rs,asm_thm=at,asm_rls=ar,ppc=x}) 
    2.28 -    pt pos end;*)
    2.29 -fun update_metppc pt pos x = appl_obj (repl_met    x) pt pos;
    2.30 -			 			   
    2.31 -(*fun union_cid     pt pos x = appl_obj (uni__cid    x) pt pos;*)
    2.32 -
    2.33 +fun update_metppc pt pos x = appl_obj (repl_met    x) pt pos;		   
    2.34  fun update_branch pt pos x = appl_obj (repl_branch x) pt pos;
    2.35 -fun update_tac  pt pos x = appl_obj (repl_tac  x) pt pos;
    2.36 -
    2.37 +fun update_tac    pt pos x = appl_obj (repl_tac    x) pt pos;
    2.38  fun update_oris   pt pos x = appl_obj (repl_oris   x) pt pos;
    2.39  fun update_orispec   pt pos x = appl_obj (repl_orispec   x) pt pos;
    2.40  
    2.41 -local
    2.42 -(* update_loc is done by append_*, see generate1.
    2.43 -   FIXME.WN110511 used for hack (which uses loc instead env in PblObj, see [*]*)
    2.44 -fun update_loc pt (p, _) ((ScrState ([],[],NONE,Const ("empty",_),Sundef,false)), _) = 
    2.45 -      appl_obj (repl_loc (NONE, NONE)) pt p
    2.46 -  | update_loc pt (p, Res) x =  
    2.47 -      let val (lform,_) = get_obj g_loc pt p
    2.48 -      in appl_obj (repl_loc (lform, SOME x)) pt p end
    2.49 -  | update_loc pt (p, _) x = 
    2.50 -      let val (_,lres) = get_obj g_loc pt p
    2.51 -      in appl_obj (repl_loc (SOME x, lres)) pt p end;
    2.52 -in
    2.53 -fun update_pbl_ctxt pt p ctxt = (*FIXME.WN110511 for hack *)
    2.54 -      let val (_, res) = get_obj g_loc pt  p
    2.55 -      in 
    2.56 -        case res of
    2.57 -          SOME (istate, _) => update_loc pt (p, Res) (istate, ctxt)
    2.58 -        | NONE => update_loc pt (p, Res) (e_istate, ctxt)
    2.59 -      end
    2.60 -end
    2.61 -
    2.62  (*WN050305 for handling cut_tree in cappend_atomic -- TODO redesign !*)
    2.63  fun update_loc' pt p iss = appl_obj (repl_loc iss) pt p;
    2.64  
    2.65 -(*13.8.02---------------------------
    2.66 -fun get_loc EmptyPtree _ = NONE
    2.67 -  | get_loc pt (p,Res) =
    2.68 -  let val (lfrm,lres) = get_obj g_loc pt p
    2.69 -  in if lres = e_istate then lfrm else lres end
    2.70 -  | get_loc pt (p,_) =
    2.71 -  let val (lfrm,lres) = get_obj g_loc pt p
    2.72 -  in if lfrm = e_istate then lres else lfrm end;  5.10.00: too liberal ?*)
    2.73  (*13.8.02: options, because istate is no equalitype any more*)
    2.74  fun get_loc EmptyPtree _ = (e_istate, e_ctxt)
    2.75    | get_loc pt (p,Res) =
    2.76 @@ -1351,7 +1308,10 @@
    2.77         | (NONE  , NONE) => (e_istate, e_ctxt)
    2.78         | (SOME i, _) => i);
    2.79  fun get_istate pt p = get_loc pt p |> #1;
    2.80 -fun get_ctxt pt p = get_loc pt p |> #2; (*FIXME.WN110511 delete*)
    2.81 +fun get_ctxt pt (pos as (p, p_)) =
    2.82 +  if member op = [Frm, Res] p_
    2.83 +  then get_loc pt pos |> #2 (*for script interpretation rely on fun get_loc*)
    2.84 +  else get_obj g_ctxt pt p (*for specify phase take ctx from PblObj*)
    2.85  
    2.86  fun get_assumptions_ pt p = get_ctxt pt p |> get_assumptions;
    2.87  
    2.88 @@ -1387,7 +1347,7 @@
    2.89  
    2.90  (**.development for extracting an 'interval' from ptree.**)
    2.91  
    2.92 -(*version 1 stopped 8.03 in favour of get_interval with !!!move_dn
    2.93 +(*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo
    2.94    actually used (inefficient) version with move_dn: see modspec.sml*)
    2.95  local
    2.96  
    2.97 @@ -1433,11 +1393,6 @@
    2.98      (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q))) 
    2.99  	(take_fromto (hdp p) (hdq q) (children pt));
   2.100  end;
   2.101 -(*WN0510 stoppde this development;
   2.102 - actually used (inefficient) version with move_dn: getFormulaeFromTo*)
   2.103 -
   2.104 -
   2.105 -
   2.106  
   2.107  fun get_somespec ((dI,pI,mI):spec) ((dI',pI',mI'):spec) =
   2.108      let val domID = if dI = e_domID

     3.1 --- a/src/Tools/isac/Interpret/generate.sml	Fri May 13 14:15:59 2011 +0200
     3.2 +++ b/src/Tools/isac/Interpret/generate.sml	Fri May 13 17:19:38 2011 +0200
     3.3 @@ -479,7 +479,7 @@
     3.4        let (*val _=tracing("###generate1 Subproblem': pos= "^pos'2str (p,p_))*)
     3.5  	      val (pt,c) =
     3.6            cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl);
     3.7 -        val pt = update_pbl_ctxt pt p ctxt (*FIXME.WN110511*)   
     3.8 +        val pt = update_ctxt pt p ctxt (*FIXME.WN110511*)   
     3.9  	      val f = Syntax.string_of_term (thy2ctxt thy) f;
    3.10        in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
    3.11  

     4.1 --- a/src/Tools/isac/Interpret/mstools.sml	Fri May 13 14:15:59 2011 +0200
     4.2 +++ b/src/Tools/isac/Interpret/mstools.sml	Fri May 13 17:19:38 2011 +0200
     4.3 @@ -82,6 +82,7 @@
     4.4      val d_in : itm_ -> term
     4.5      val de_item : item -> cterm'
     4.6      val declare_constraints : string -> Proof.context -> Proof.context
     4.7 +    val declare_constraints' : term list -> Proof.context -> Proof.context
     4.8      val dest_list : term * term list -> term list (* for testing *)
     4.9      val dest_list' : term -> term list
    4.10      val dts2str : term * term list -> string
    4.11 @@ -972,11 +973,14 @@
    4.12  fun check_preconds thy prls pres pbl = 
    4.13      check_preconds' prls pres pbl (max_vt pbl);
    4.14  
    4.15 +fun declare_constraints' ts ctxt =
    4.16 +      fold Variable.declare_constraints (flat (map vars ts)) ctxt;
    4.17 +(*WN110613 fun declare_constraints' shall replace fun declare_constraints*)
    4.18  fun declare_constraints t ctxt =
    4.19      let
    4.20        fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
    4.21                (_, _::_) => (Free (v,T)::get_vars vs)
    4.22 -            | (_, []  ) => get_vars vs)
    4.23 +            | (_, []  ) => get_vars vs) (*filter out nums as long as *)
    4.24          | get_vars [] = [];
    4.25        val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
    4.26      in fold Variable.declare_constraints ts ctxt end;

     5.1 --- a/src/Tools/isac/Interpret/ptyps.sml	Fri May 13 14:15:59 2011 +0200
     5.2 +++ b/src/Tools/isac/Interpret/ptyps.sml	Fri May 13 17:19:38 2011 +0200
     5.3 @@ -269,7 +269,7 @@
     5.4     *)
     5.5  
     5.6  fun prep_ori [] _ _ = ([], e_ctxt)
     5.7 -  | prep_ori fmz thy pbt = (*FIXME.WN110511 ?return ctxt?*)
     5.8 +  | prep_ori fmz thy pbt =
     5.9        let
    5.10          val ctxt = ProofContext.init_global thy |> fold declare_constraints fmz;
    5.11          val ori = map (add_field thy pbt o split_dts o the o parseNEW ctxt) fmz

     6.1 --- a/src/Tools/isac/Interpret/script.sml	Fri May 13 14:15:59 2011 +0200
     6.2 +++ b/src/Tools/isac/Interpret/script.sml	Fri May 13 17:19:38 2011 +0200
     6.3 @@ -410,10 +410,10 @@
     6.4    | stac2tac_ pt thy (Const ("Script.Tac",_) $ Free (str,_)) = 
     6.5        (Tac ((de_esc_underscore o strip_thy) str),  Empty_Tac_) 
     6.6  
     6.7 +    (*compare "| assod _ (Subproblem'"*)
     6.8    | stac2tac_ pt thy (stac as Const ("Script.SubProblem",_) $
     6.9  	  (Const ("Product_Type.Pair",_) $Free (dI',_) $ 
    6.10  		 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
    6.11 -      (*compare "| assod _ (Subproblem'"*)
    6.12        let
    6.13          val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
    6.14          val thy = maxthy (assoc_thy dI) (rootthy pt);
    6.15 @@ -441,8 +441,9 @@
    6.16            case cas of
    6.17  		        NONE => pblterm dI pI
    6.18  		      | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
    6.19 +        val ctxt = declare_constraints' vals (ProofContext.init_global thy)
    6.20          val f = subpbl (strip_thy dI) pI
    6.21 -      in (Subproblem (dI, pI),	Subproblem' ((dI, pI, mI), pors, hdl, fmz_, (*FIXME.WN110511*)e_ctxt, f))
    6.22 +      in (Subproblem (dI, pI),	Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
    6.23        end
    6.24  
    6.25    | stac2tac_ pt thy t = error 
    6.26 @@ -592,10 +593,10 @@
    6.27        then Ass (m, ((term_of o the o (parse thy)) f'))
    6.28        else NotAss
    6.29  
    6.30 +    (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
    6.31    | assod pt _ (Subproblem' ((domID,pblID,metID),_,_,_,_,f))
    6.32  	  (stac as Const ("Script.SubProblem",_) $ (Const ("Product_Type.Pair",_) $
    6.33  		 Free (dI',_) $ (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
    6.34 -      (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
    6.35        let 
    6.36          val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
    6.37          val thy = maxthy (assoc_thy dI) (rootthy pt);
    6.38 @@ -621,14 +622,16 @@
    6.39  	      val {cas, ppc, thy,...} = get_pbt pI
    6.40  	      val dI = theory2theory' thy (*take dI from _refined_ pbl*)
    6.41  	      val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
    6.42 +	      val thy' = (maxthy (assoc_thy dI) (rootthy pt))
    6.43  	      val hdl = 
    6.44            case cas of
    6.45  		        NONE => pblterm dI pI
    6.46  		      | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
    6.47 +        val ctxt = declare_constraints' vals (ProofContext.init_global thy')
    6.48          val f = subpbl (strip_thy dI) pI
    6.49        in 
    6.50          if domID = dI andalso pblID = pI
    6.51 -        then Ass (Subproblem' ((dI, pI, mI), pors, hdl, fmz_, (*FIXME.WN110511*)e_ctxt, f), f) 
    6.52 +        then Ass (Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f), f) 
    6.53          else NotAss
    6.54        end
    6.55  

     7.1 --- a/src/Tools/isac/ProgLang/scrtools.sml	Fri May 13 14:15:59 2011 +0200
     7.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml	Fri May 13 17:19:38 2011 +0200
     7.3 @@ -72,7 +72,7 @@
     7.4  val it = false : bool
     7.5  *)
     7.6  
     7.7 -(*WN110511  Const would be clearer !!! TODO combine both ...
     7.8 +(*WN110511  Const would be clearer !!! TODO combine both fun is_dsc ...
     7.9  fun is_dsc (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) = true
    7.10    | is_dsc (Const(_,Type("fun",[_,Type("Tools.una",_)]))) = true
    7.11    | is_dsc (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) = true

     8.1 --- a/test/Tools/isac/Interpret/ctree.sml	Fri May 13 14:15:59 2011 +0200
     8.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Fri May 13 17:19:38 2011 +0200
     8.3 @@ -10,6 +10,7 @@
     8.4  "table of contents -----------------------------------------------";
     8.5  "-----------------------------------------------------------------";
     8.6  "-----------------------------------------------------------------";
     8.7 +"-------------- fun get_ctxt -------------------------------------";
     8.8  "-------------- fun update_ctxt, fun g_ctxt ----------------------";
     8.9  "-------------- check positions in miniscript --------------------";
    8.10  "-------------- get_allpos' (from ptree above)--------------------";
    8.11 @@ -59,6 +60,20 @@
    8.12  "-----------------------------------------------------------------";
    8.13  
    8.14  
    8.15 +"-------------- fun get_ctxt -------------------------------------";
    8.16 +"-------------- fun get_ctxt -------------------------------------";
    8.17 +"-------------- fun get_ctxt -------------------------------------";
    8.18 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    8.19 +val (dI',pI',mI') =
    8.20 +  ("Test", ["sqroot-test","univariate","equation","test"],
    8.21 +   ["Test","squ-equ-test-subpbl1"]);
    8.22 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    8.23 +(get_ctxt pt p)
    8.24 +  handle _ => error "ctree.sml: not even some ctxt found in PblObj";
    8.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    8.26 +(get_ctxt pt p)
    8.27 +  handle _ => error "ctree.sml: not even some ctxt found in PrfObj";
    8.28 +
    8.29  "-------------- fun update_ctxt, fun g_ctxt ----------------------";
    8.30  "-------------- fun update_ctxt, fun g_ctxt ----------------------";
    8.31  "-------------- fun update_ctxt, fun g_ctxt ----------------------";

     9.1 --- a/test/Tools/isac/Interpret/mstools.sml	Fri May 13 14:15:59 2011 +0200
     9.2 +++ b/test/Tools/isac/Interpret/mstools.sml	Fri May 13 17:19:38 2011 +0200
     9.3 @@ -8,6 +8,7 @@
     9.4  "--------------------------------------------------------";
     9.5  "table of contents --------------------------------------";
     9.6  "--------------------------------------------------------";
     9.7 +"----------- fun declare_constraints' -------------------";
     9.8  "----------- fun declare_constraints --------------------";
     9.9  "----------- fun get_assumptions, fun get_environments --";
    9.10  "----------- fun transfer_from_subproblem ---------------";
    9.11 @@ -19,6 +20,21 @@
    9.12  "--------------------------------------------------------";
    9.13  
    9.14  
    9.15 +"----------- fun declare_constraints' -------------------";
    9.16 +"----------- fun declare_constraints' -------------------";
    9.17 +"----------- fun declare_constraints' -------------------";
    9.18 +val ctxt = ProofContext.init_global @{theory "Isac"};
    9.19 +val SOME ta = parseNEW ctxt "x";
    9.20 +if type_of ta = TFree ("'a",[]) then () else error "TODO";
    9.21 +
    9.22 +(*----- add a type constraint to ctxt *)
    9.23 +val SOME ti = parseNEW ctxt "x::int";
    9.24 +val ctxt = declare_constraints' [ti] ctxt;
    9.25 +
    9.26 +(*----- now parsing infers the type *)
    9.27 +val SOME t = parseNEW ctxt "x";
    9.28 +if type_of t = Type ("Int.int",[]) then () else error "TODO";
    9.29 +
    9.30  "----------- fun declare_constraints --------------------";
    9.31  "----------- fun declare_constraints --------------------";
    9.32  "----------- fun declare_constraints --------------------";
    9.33 @@ -153,7 +169,7 @@
    9.34  val (d, ts) = split_dts t;
    9.35  "~~~~~ fun split_dts, args:"; val (t as d $ arg) = t;
    9.36  (*if is_dsc d then () else error "TODO";*)
    9.37 -if not (is_dsc d) then () else error "TODO";
    9.38 +if is_dsc d then () else error "TODO";
    9.39  "----- these were the errors (call hierarchy from bottom up)";
    9.40  appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct;(*WAS
    9.41  Err "[error] appl_add: is_known: identifiers [equality] not in example"*)
    9.42 @@ -165,5 +181,3 @@
    9.43  Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
    9.44  (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS
    9.45  Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
    9.46 -
    9.47 -

    10.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Fri May 13 14:15:59 2011 +0200
    10.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Fri May 13 17:19:38 2011 +0200
    10.3 @@ -5,26 +5,34 @@
    10.4  
    10.5  val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    10.6  val (dI',pI',mI') =
    10.7 -  ("Test", ["sqroot-test","univariate","equation","test"],
    10.8 -   ["Test","squ-equ-test-subpbl1"]);
    10.9 +   ("Test", ["sqroot-test","univariate","equation","test"],
   10.10 +    ["Test","squ-equ-test-subpbl1"]);
   10.11  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
   10.12  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.13 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   10.14 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   10.15 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   10.16 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   10.17 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   10.18 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   10.19 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   10.20 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   10.21 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Subproblem"*)
   10.22 -(*
   10.23 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   10.24 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   10.25 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   10.26 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   10.27 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   10.28 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   10.29 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   10.30 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   10.31 -*)
   10.32 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.33 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.34 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.35 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.36 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.37 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.38 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.39 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.40 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
   10.41 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.42 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.43 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.44 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.45 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.46 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.47 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.48 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   10.49 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*);
   10.50 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
   10.51 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
   10.52 +(*-----nxt = ("Empty_Tac", Empty_Tac): tac'_
   10.53 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions *);
   10.54 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond["sqroot-test", "univariate", ...]) *);
   10.55 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("End_Proof'" *);
   10.56 +-----*)
   10.57 +
   10.58 +

    11.1 --- a/test/Tools/isac/Test_Isac.thy	Fri May 13 14:15:59 2011 +0200
    11.2 +++ b/test/Tools/isac/Test_Isac.thy	Fri May 13 17:19:38 2011 +0200
    11.3 @@ -97,52 +97,46 @@
    11.4    use "Minisubpbl/100-init-rootpbl.sml"
    11.5    use "Minisubpbl/150-add-given.sml"
    11.6    use "Minisubpbl/200-start-method.sml"
    11.7 +  use "Minisubpbl/300-init-subpbl.sml"
    11.8  ML {*
    11.9 +(*test/./400-start-meth-subpbl*)
   11.10 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
   11.11 +val (dI',pI',mI') =
   11.12 +   ("Test", ["sqroot-test","univariate","equation","test"],
   11.13 +    ["Test","squ-equ-test-subpbl1"]);
   11.14 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
   11.15 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.16 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.17 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.18 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.19 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.20 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.21 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.22 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.23 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.24 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
   11.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.26 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.27 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.28 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.30 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.31 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.32 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   11.33 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*);
   11.34 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
   11.35 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
   11.36 +(*-----nxt = ("Empty_Tac", Empty_Tac): tac'_
   11.37 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions *);
   11.38 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond["sqroot-test", "univariate", ...]) *);
   11.39 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("End_Proof'" *);
   11.40 +-----*)
   11.41  *}
   11.42 -ML {*
   11.43 -*}
   11.44 -ML {*
   11.45 -*}
   11.46 -ML {*
   11.47 -*}
   11.48 -ML {*
   11.49 -*}
   11.50 -ML {*
   11.51 -*}
   11.52 -ML {*
   11.53 -*}
   11.54 -  use "Minisubpbl/300-init-subpbl.sml"
   11.55    use "Minisubpbl/400-start-meth-subpbl.sml"
   11.56    use "Minisubpbl/500-postcond.sml"
   11.57    ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*}
   11.58    ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
   11.59    use "Interpret/mstools.sml"       (*new 2010*)
   11.60 -ML {*
   11.61 -*}
   11.62 -ML {*
   11.63 -*}
   11.64 -ML {*
   11.65 -*}
   11.66 -ML {*
   11.67 -*}
   11.68 -ML {*
   11.69 -*}
   11.70 -ML {*
   11.71 -
   11.72 -*}
   11.73 -ML {*
   11.74 -*}
   11.75 -ML {*
   11.76 -*}
   11.77 -ML {*
   11.78 -*}
   11.79 -ML {*
   11.80 -
   11.81 -*}
   11.82 -ML {*
   11.83 -*}
   11.84 -ML {*
   11.85 -*}
   11.86    use "Interpret/ctree.sml"         (*!...!see(25)*)
   11.87    use "Interpret/ptyps.sml"         (*    *)
   11.88  (*use "Interpret/generate.sml"        new 2011*)
   11.89 @@ -208,12 +202,12 @@
   11.90  (*=== inhibit exn ?=============================================================
   11.91  ===== inhibit exn ?===========================================================*)
   11.92  
   11.93 -(*========== inhibit exn 110503 ================================================
   11.94 +(*========== inhibit exn 110513 ================================================
   11.95  
   11.96  "########### testcode inserted vvv ###########################################";
   11.97  "########### testcode inserted ^^^ ###########################################";
   11.98  
   11.99 -============ inhibit exn 110503 ==============================================*)
  11.100 +============ inhibit exn 110513 ==============================================*)
  11.101  
  11.102  (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
  11.103  -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)