(* Title:  150-add-given.sml

    Author: Walther Neuper 1105

    (c) copyright due to lincense terms.

 *)

 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];

 val (dI',pI',mI') =

   ("Test", ["sqroot-test","univariate","equation","test"],

    ["Test","squ-equ-test-subpbl1"]);

 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = ("Model_Problem"*)

 (*for resuming after stepping into code*)

 val (p''',f''',nxt''',pt''') = (p,f,nxt,pt);

 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW), (pt:ctree)) = (nxt, p, [], pt);

     val (pt, p) = 

 	    case locatetac tac (pt,p) of

 		    ("ok", (_, _, ptp)) => ptp;

 (*  val (_, ts) =

 	    (case step p ((pt, e_pos'),[]) of

 		    ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts))

 ERROR: ts = [(Tac "appl_add: syntax error in 'equality (<markup> + <markup> = <markup>)'", ...*)

 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =

   (p, ((pt, e_pos'),[]));

  val pIopt = get_pblID (pt,ip);

 ip = ([],Res); (* = false*)

 tacis; (* = []*)

 pIopt; (* = SOME ["sqroot-test", "univariate", "equation", "test"]*)

 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (* = true*)

 (* nxt_specify_ (pt, ip)

 ERROR:  = ([(Tac "appl_add: syntax error in 'equality (<markup> + <markup> = <markup>)'",...*)

 "~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt, ip);

 val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),

 			  probl,spec=(dI,pI,mI), ...}) = get_obj I pt p;

 just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (* = false*)

         val cpI = if pI = e_pblID then pI' else pI;

 		    val cmI = if mI = e_metID then mI' else mI;

 		    val {ppc, prls, where_, ...} = get_pbt cpI;

 		    val pre = check_preconds "thy 100820" prls where_ probl;

 		    val pb = foldl and_ (true, map fst pre);

 (*    val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) 

 			    (ppc, (#ppc o get_met) cmI) (dI, pI, mI);

 ERROR: val tac = Add_Given "equality (<markup> + <markup> = <markup>)"*)

 "~~~~~ fun nxt_spec, args:"; val (Pbl, preok, (oris : ori list), ((dI', pI', mI') : spec),

   ((pbl : itm list), (met : itm list)), (pbt, mpc), ((dI, pI, mI) : spec)) = 

   (p_, pb, oris, (dI',pI',mI'), (probl, meth), 

 			    (ppc, (#ppc o get_met) cmI), (dI, pI, mI));

 dI' = e_domID andalso dI = e_domID; (* = false*)

 pI' = e_pblID andalso pI = e_pblID; (* = false*)

 find_first (is_error o #5) (pbl:itm list); (* = NONE*)

 (* nxt_add (assoc_thy (if dI = e_domID then dI' else dI)) oris pbt pbl; 

 = SOME ("#Given", "equality (<markup> + <markup> = <markup>)") *)

 "~~~~~ fun nxt_add, args:"; val (thy, oris, pbt, itms) =

   ((assoc_thy (if dI = e_domID then dI' else dI)), oris, pbt, pbl);

 local infix mem;

 fun x mem [] = false

   | x mem (y :: ys) = x = y orelse x mem ys;

 in 

     fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))

       andalso (#3 ori) <>"#undef";

     fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));

     fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;

     fun test_subset (itm:itm) ((_,_,_,d,ts):ori) = 

 	(d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);

     fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false

       | false_and_not_Sup (i,v,false,f, _) = true

       | false_and_not_Sup  _ = false;

 end

     val v = if itms = [] then 1 else max_vt itms;

     val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)

     val vits = if v = 0 then itms (*because of dsc without dat*)

 	       else filter (testi_vt v) itms;                   (*itms..vat*)

     val icl = filter false_and_not_Sup vits; (* incomplete *)

 icl = []; (* = false*)

 val SOME ori = find_first (test_subset (hd icl)) vors;

 (* SOME (geti_ct thy ori (hd icl))

 ERROR: SOME (geti_ct thy ori (hd icl))*)

 "~~~~~ fun geti_ct, args:"; val (thy, ((_, _, _, d, ts) : ori), ((_, _, _, fd, itm_) : itm)) =

   (thy, ori, (hd icl));

 "~~~~~ to  return val:"; val xxx = 

   ( fd, 

     ((term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : cterm'

   );

 if xxx = ("#Given", "equality (x + 1 = 2)") then () else error "";

 (* resuming after stepping into code*)

 val (p,f,nxt,pt) = (p''',f''',nxt''',pt''');

 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_,Add_Given "equality (x + 1 = 2)*)

 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = (_,Add_Given "solveFor x"*)

 case nxt of (_, Add_Given "solveFor x") => ()

 | _ => error "minisubpbl: Add_Given is broken in root-problem";