(* Title:  "Minisubpbl/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, (p:pos'), (_:NEW), (pt:ctree)) = (nxt, p, [], pt);

    val (pt, p) = 

      (*ERROR nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt ... see 100-init-rootpbl.sml*)

	    case Step.by_tactic tac (pt,p) of

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

    (*case*)

      Step.do_next p ((pt, Pos.e_pos'), []) (*of*);

"~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =

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

    val pIopt = get_pblID (pt,ip);

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

      val _ = (*case*) tacis (*of*);

      val SOME _ = (*case*) pIopt (*of*);

   val (_, ([(Add_Given "equality (x + 1 = 2)", _, _)], _, _)) =

           switch_specify_solve p_ (pt, ip);

"~~~~~ fun switch_specify_solve , 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 = Problem.id_empty then pI' else pI;

		    val cmI = if mI = Method.id_empty then mI' else mI;

		    val {ppc, prls, where_, ...} = Problem.from_store cpI;

		    val pre = Pre_Conds.check' "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 Method.from_store) cmI) (dI, pI, mI);

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

"~~~~~ fun nxt_spec, args:"; val (Pbl, preok, (oris : O_Model.T), ((dI', pI', mI') : References.T),

  ((pbl : I_Model.T), (met : I_Model.T)), (pbt, mpc), ((dI, pI, mI) : References.T)) = 

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

			    (ppc, (#ppc o Method.from_store) cmI), (dI, pI, mI));

dI' = ThyC.id_empty andalso dI = ThyC.id_empty; (* = false*)

pI' = Problem.id_empty andalso pI = Problem.id_empty; (* = false*)

find_first (I_Model.is_error o #5) (pbl:I_Model.T); (* = NONE*)

(* nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl; 

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

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

  ((ThyC.get_theory (if dI = ThyC.id_empty 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:O_Model.single))

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

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

    fun test_id ids r = curry (op mem) (#1 (r:O_Model.single)) ids;

    fun test_subset (itm:I_Model.single) ((_,_,_,d,ts):O_Model.single) = 

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

    fun false_and_not_Sup((i,v,false,f,I_Model.Sup _):I_Model.single) = false

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

      | false_and_not_Sup  _ = false;

end

    val v = if itms = [] then 1 else I_Model.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) : O_Model.single), ((_, _, _, fd, itm_) : I_Model.single)) =

  (thy, ori, (hd icl));

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

  ( fd, 

    ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (I_Model.ts_in itm_) ts) : TermC.as_string

  );

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";