neuper@41985: (* Title:  300-init-subpbl.sml
neuper@41985:    Author: Walther Neuper 1105
neuper@41985:    (c) copyright due to lincense terms.
neuper@41985: *)
neuper@41985: 
neuper@42011: "----------- Minisubplb/300-init-subpbl.sml ----------------------";
neuper@42011: "----------- Minisubplb/300-init-subpbl.sml ----------------------";
neuper@42011: "----------- Minisubplb/300-init-subpbl.sml ----------------------";
neuper@41985: val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
neuper@41985: val (dI',pI',mI') =
neuper@41985:   ("Test", ["sqroot-test","univariate","equation","test"],
neuper@41985:    ["Test","squ-equ-test-subpbl1"]);
neuper@41985: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@41985: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@41986: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
neuper@41986: "~~~~~ fun me, args:"; val (_,tac) = nxt;
neuper@41986: "~~~~~ fun locatetac, args:"; val (tac, ptp as (pt, p)) = (tac, (pt,p));
neuper@41986: val (mI,m) = mk_tac'_ tac;
neuper@41986: val Appl m = applicable_in p pt m;
neuper@42092: member op = specsteps mI; (*false*)
neuper@42092: (*val Updated (cs' as (_,_,(_,p'))) =  loc_solve_ (mI,m) ptp;*)
neuper@42092: "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
neuper@42092: (*val (msg, cs') = solve m (pt, pos);*)
neuper@42092: "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
neuper@42092: e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
neuper@42092: 	      val thy' = get_obj g_domID pt (par_pblobj pt p);
neuper@42092: 	      val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
neuper@42092: 		      val d = e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)
neuper@42092: (*val Steps (is', ss as (m',f',pt',p',c')::_) = locate_gen (thy',srls) m  (pt,(p,p_)) (sc,d) is;*)
wneuper@59279: "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), 
neuper@48790: 	                   (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
neuper@42092:                    ((thy',srls), m,  (pt,(p,p_)), (sc,d), is);
neuper@42092: val thy = assoc_thy thy';
neuper@42092: l = [] orelse ((*init.in solve..Apply_Method...*)
neuper@42092: 			         (last_elem o fst) p = 0 andalso snd p = Res) (*false*);
neuper@42092: (*val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =
neuper@42092:     (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) );*)
neuper@48790: "~~~~~ fun astep_up, args:"; val ((ys as (_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
neuper@42092:                      ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) );
neuper@42092: 1 < length l (*true*);
neuper@42092: val up = drop_last l;
neuper@42092: (*ass_up ys ((E,up,a,v,S,b),ss) (go up sc);*)
neuper@42092: "~~~~~ fun ass_up, args:"; val (ysa, iss, (Const ("Script.Try",_) $ e)) =
neuper@42092:                                              (ys, ((E,up,a,v,S,b),ss), (go up sc));
neuper@42092: (* STOPPED stepping into HERE due to type problem:  Can't unify _a to pos * pos_
neuper@42092: astep_up ysa iss;
neuper@42092: 
neuper@42092: at bottom of | assy we see:
neuper@42092:                  :
neuper@42092:                  case assod pt d m stac of
neuper@42092: "~~~~~ fun assod, args:"; val (...Subproblem'...) = ();
neuper@48761: 	      val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global 
neuper@42092:           |> declare_constraints' vals
neuper@42092: *)
neuper@41986: 
neuper@41985: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@41986: case nxt of ("Model_Problem", _) => ()
neuper@41986: | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem";
neuper@41986: