1.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml	Sun Jul 21 15:15:50 2013 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml	Mon Jul 22 13:52:18 2013 +0200
     1.3 @@ -8,8 +8,89 @@
     1.4    ("Test", ["sqroot-test","univariate","equation","test"],
     1.5     ["Test","squ-equ-test-subpbl1"]);
     1.6  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = ("Model_Problem"*)
     1.7 +(*for resuming after stepping into code*)
     1.8 +val (p''',f''',nxt''',pt''') = (p,f,nxt,pt);
     1.9 +
    1.10 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW), (pt:ptree)) = (nxt, p, [], pt);
    1.11 +    val (pt, p) = 
    1.12 +	    case locatetac tac (pt,p) of
    1.13 +		    ("ok", (_, _, ptp)) => ptp;
    1.14 +(*  val (_, ts) =
    1.15 +	    (case step p ((pt, e_pos'),[]) of
    1.16 +		    ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts))
    1.17 +ERROR: ts = [(Tac "appl_add: syntax error in 'equality (<markup> + <markup> = <markup>)'", ...*)
    1.18 +"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
    1.19 +  (p, ((pt, e_pos'),[]));
    1.20 + val pIopt = get_pblID (pt,ip);
    1.21 +ip = ([],Res); (* = false*)
    1.22 +tacis; (* = []*)
    1.23 +pIopt; (* = SOME ["sqroot-test", "univariate", "equation", "test"]*)
    1.24 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (* = true*)
    1.25 +
    1.26 +(* nxt_specify_ (pt, ip)
    1.27 +ERROR:  = ([(Tac "appl_add: syntax error in 'equality (<markup> + <markup> = <markup>)'",...*)
    1.28 +"~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt, ip);
    1.29 +val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
    1.30 +			  probl,spec=(dI,pI,mI), ...}) = get_obj I pt p;
    1.31 +just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (* = false*)
    1.32 +        val cpI = if pI = e_pblID then pI' else pI;
    1.33 +		    val cmI = if mI = e_metID then mI' else mI;
    1.34 +		    val {ppc, prls, where_, ...} = get_pbt cpI;
    1.35 +		    val pre = check_preconds "thy 100820" prls where_ probl;
    1.36 +		    val pb = foldl and_ (true, map fst pre);
    1.37 +
    1.38 +(*    val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) 
    1.39 +			    (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
    1.40 +ERROR: val tac = Add_Given "equality (<markup> + <markup> = <markup>)"*)
    1.41 +"~~~~~ fun nxt_spec, args:"; val (Pbl, preok, (oris : ori list), ((dI', pI', mI') : spec),
    1.42 +  ((pbl : itm list), (met : itm list)), (pbt, mpc), ((dI, pI, mI) : spec)) = 
    1.43 +  (p_, pb, oris, (dI',pI',mI'), (probl, meth), 
    1.44 +			    (ppc, (#ppc o get_met) cmI), (dI, pI, mI));
    1.45 +
    1.46 +dI' = e_domID andalso dI = e_domID; (* = false*)
    1.47 +pI' = e_pblID andalso pI = e_pblID; (* = false*)
    1.48 +find_first (is_error o #5) (pbl:itm list); (* = NONE*)
    1.49 +
    1.50 +(* nxt_add (assoc_thy (if dI = e_domID then dI' else dI)) oris pbt pbl; 
    1.51 += SOME ("#Given", "equality (<markup> + <markup> = <markup>)") *)
    1.52 +"~~~~~ fun nxt_add, args:"; val (thy, oris, pbt, itms) =
    1.53 +  ((assoc_thy (if dI = e_domID then dI' else dI)), oris, pbt, pbl);
    1.54 +local infix mem;
    1.55 +fun x mem [] = false
    1.56 +  | x mem (y :: ys) = x = y orelse x mem ys;
    1.57 +in 
    1.58 +    fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))
    1.59 +      andalso (#3 ori) <>"#undef";
    1.60 +    fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));
    1.61 +    fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;
    1.62 +    fun test_subset (itm:itm) ((_,_,_,d,ts):ori) = 
    1.63 +	(d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
    1.64 +    fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
    1.65 +      | false_and_not_Sup (i,v,false,f, _) = true
    1.66 +      | false_and_not_Sup  _ = false;
    1.67 +end
    1.68 +    val v = if itms = [] then 1 else max_vt itms;
    1.69 +    val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)
    1.70 +    val vits = if v = 0 then itms (*because of dsc without dat*)
    1.71 +	       else filter (testi_vt v) itms;                   (*itms..vat*)
    1.72 +    val icl = filter false_and_not_Sup vits; (* incomplete *)
    1.73 +icl = []; (* = false*)
    1.74 +val SOME ori = find_first (test_subset (hd icl)) vors;
    1.75 +
    1.76 +(* SOME (geti_ct thy ori (hd icl))
    1.77 +ERROR: SOME (geti_ct thy ori (hd icl))*)
    1.78 +"~~~~~ fun geti_ct, args:"; val (thy, ((_, _, _, d, ts) : ori), ((_, _, _, fd, itm_) : itm)) =
    1.79 +  (thy, ori, (hd icl));
    1.80 +"~~~~~ to  return val:"; val xxx = 
    1.81 +  ( fd, 
    1.82 +    ((term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : cterm'
    1.83 +  );
    1.84 +if xxx = ("#Given", "equality (x + 1 = 2)") then () else error "";
    1.85 +
    1.86 +(* resuming after stepping into code*)
    1.87 +val (p,f,nxt,pt) = (p''',f''',nxt''',pt''');
    1.88 +
    1.89  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_,Add_Given "equality (x + 1 = 2)*)
    1.90  val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = (_,Add_Given "solveFor x"*)
    1.91  case nxt of (_, Add_Given "solveFor x") => ()
    1.92  | _ => error "minisubpbl: Add_Given is broken in root-problem";
    1.93 -