neuper@42279: (* Title:  tests for Interpret/mathengine.sml
neuper@42279:    Author: Walther Neuper 2000, 2006
neuper@37906:    (c) due to copyright terms
neuper@37906: *)
neuper@38065: "--------------------------------------------------------";
neuper@38065: "table of contents --------------------------------------";
neuper@38065: "--------------------------------------------------------";
neuper@41940: "----------- change to parse ctxt -----------------------";
neuper@38065: "----------- debugging setContext..pbl_ -----------------";
neuper@38065: "----------- tryrefine ----------------------------------";
neuper@41982: "----------- fun step: Apply_Method without init_form ---";
neuper@38065: "----------- fun step -----------------------------------";
neuper@38065: "----------- fun autocalc -------------------------------";
neuper@38065: "----------- fun autoCalculate --------------------------";
neuper@42067: "----------- fun autoCalculate..CompleteCalc ------------";
t@42225: "----------- search for Or_to_List ----------------------";
neuper@42279: "----------- check thy in CalcTreeTEST ------------------";
neuper@38065: "--------------------------------------------------------";
neuper@38065: "--------------------------------------------------------";
neuper@38065: "--------------------------------------------------------";
neuper@37906: 
neuper@41940: "----------- change to parse ctxt -----------------------";
neuper@41940: "----------- change to parse ctxt -----------------------";
neuper@41940: "----------- change to parse ctxt -----------------------";
neuper@41940: "===== start calculation: from problem description (fmz) to origin";
neuper@41940: val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
neuper@41940: val (thyID, pblID, metID) =
neuper@41940:   ("Test", ["calculate", "test"], ["Test", "test_calculate"]);
neuper@41940: val (p,_,_,nxt,_,pt) = CalcTreeTEST [(fmz, (thyID, pblID, metID))];
neuper@41940: "----- ";
neuper@41940: (* call sequence: CalcTreeTEST 
neuper@41940:                 > nxt_specify_init_calc 
neuper@41940:                 > prep_ori
neuper@41940: *)
neuper@41940: val (thy, pbt) = (Thy_Info.get_theory thyID, (#ppc o get_pbt) pblID);
neuper@41940: "----- in  prep_ori";
neuper@41940: val ctxt = ProofContext.init_global thy;
neuper@41940: 
bonzai@41952: val ctopts = map (parseNEW ctxt) fmz;
bonzai@41952: val dts = map (split_dts o the) ctopts;
neuper@41940: (*split_dts:
neuper@41940: (term * term list) list
neuper@41940:         formulas: e.g. ((1+2)*4/3)^^^2
neuper@41940:  description: e.g. realTestGiven
neuper@41940: *)
neuper@41940:  prep_ori;
neuper@41940: (* FROM
neuper@41940: val it = fn:
neuper@41940:    string list -> theory -> (string * (term * 'a)) list -> ori list
neuper@41940: TO
neuper@41940: val it = fn:
neuper@41940:    string list -> theory -> (string * (term * 'a)) list -> (ori list * ctxt)
neuper@41940: AND
neuper@41940: FROM val oris = prep_ori...
neuper@41940: TO   val (oris, _) = prep_ori...
neuper@41940: *)
neuper@41940: "----- insert ctxt in ptree";
neuper@41940: (* datatype ppobj
neuper@41940: FROM loc   : istate option * istate option,
neuper@41940: TO   loc   : (istate * ctxt) option * (istate * ctxt) option,
neuper@41940: e.g.
neuper@41940: FROM val pt = Nd (PblObj
neuper@41940:        {.., loc = (SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)),
neuper@41940:           NONE),
neuper@41940: TO   val pt = Nd (PblObj
neuper@41940:        {.., loc = 
neuper@41940:         ((SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)), ctxt),
neuper@41940:           NONE),
neuper@41940: *)
neuper@41940: 
neuper@41940: "===== interactive specification: from origin to specification (probl)";
neuper@41940: val (p,_,_,nxt,_,pt) = me nxt p [1] pt; 
neuper@41940:   (*nxt =("Add_Given", Model_Problem)*)
neuper@41940: val (p,_,_,nxt,_,pt) = me nxt p [1] pt;
neuper@41940:   (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
neuper@41940: "----- ";
neuper@41940: (* call sequence: me Model_Problem 
neuper@41940:                 > me ("Add_Given", Add_Given "realTestGiven (((1 + 2) * 4 / 3) ^^^ 2)")
neuper@41940:                 > locatetac tac
neuper@41940:                 > loc_specify_
neuper@41940:                 > specify          GET ctxt (stored in ctree)
neuper@41940:                 > specify_additem
neuper@41940:                 > appl_add
neuper@41940: 
neuper@41940: *)
neuper@41940: "----- in appl_add";
neuper@41940: (* FROM appl_add thy
neuper@41940:    TO   appl_add ctxt
neuper@41940:    FROM parse thy str
neuper@41940:    TO   parseNEW ctxt str
neuper@41940: *)
neuper@41940: val (p,_,_,nxt,_,pt) = me nxt p [1] pt; 
neuper@41940:   (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
neuper@41940: val (p,_,_,nxt,_,pt) = me nxt p [1] pt; 
neuper@41940:   (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
neuper@41940: 
neuper@41940: "===== end specify: from specification (probl) to guard (method)";
neuper@41940: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@41940:   (*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
neuper@41940: 
neuper@41940: "===== start interpretation: from guard to environment";
neuper@41940: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@41940:   (*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
neuper@41940: "----- ";
neuper@41940: (* call sequence: me ("Apply_Method",...
neuper@41940:                 > locatetac
neuper@41940:                 > loc_solve_
neuper@41940:                 > solve ("Apply_Method",...
neuper@41940: *)
neuper@41940: val ((_,tac), ptp) = (nxt, (pt, p));
neuper@41940: locatetac tac (pt,p);
neuper@41940:   val (mI, m) = mk_tac'_ tac;
neuper@41940:   val Appl m = applicable_in p pt m;
neuper@41940:   member op = specsteps mI;
neuper@41940:   loc_solve_ (mI,m) ptp;
neuper@41940:     val (m, (pt, pos)) = ((mI,m), ptp);
neuper@41940:     solve m (pt, pos);
bonzai@41949:       val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) = 
neuper@41940:         (m, (pt, pos));
neuper@41940:       val {srls,...} = get_met mI;
neuper@41940:       val PblObj{meth=itms,...} = get_obj I pt p;
neuper@41940:       val thy' = get_obj g_domID pt p;
neuper@41940:       val thy = assoc_thy thy';
bonzai@41949:       val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
neuper@41940: 
neuper@41940: "----- go on in the calculation";
neuper@41940: val (p,_,f,nxt,_,pt) = me nxt pos [1] pt;
neuper@41940:   (*nxt = ("Calculate",Calculate "PLUS")*)
neuper@41940: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@41940:   (*nxt = ("Calculate",Calculate "TIMES")*)
neuper@41940: 
neuper@41940: "===== input a formula to be derived from previous istate";
neuper@41940: "----- appendFormula TODO: first repair error";
neuper@41940:   val cs = ((pt,p),[]);
neuper@41940:   val ("ok", cs' as (_,_,(pt,p))) = step p cs;
neuper@41943:   val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2";
neuper@41940: (*
neuper@41943:   val ("no derivation found", (_,_,(pt, p))) = inform cs' ((*encode*) ifo);
neuper@41940:   here ^^^^^^^^^^^^^^^^^^^^^ should be "ok"
neuper@41940: *)
neuper@41940: 
neuper@41940: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@41940: (*nxt = ("Calculate",Calculate "DIVIDE")*)
neuper@41940: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@41940: (*nxt = ("Calculate",Calculate "POWER")*)
neuper@41940: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@41940: (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
neuper@41940: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@41940: (*nxt = ("End_Proof'",End_Proof')*)
neuper@41940: if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()
neuper@41940: else error "calculate.sml: script test_calculate changed behaviour";
neuper@41940: 
neuper@41940: "===== tactic Subproblem: from environment to origin";
neuper@41940: "----- TODO";
neuper@41940: 
neuper@37906: 
neuper@38065: "----------- debugging setContext..pbl_ -----------------";
neuper@38065: "----------- debugging setContext..pbl_ -----------------";
neuper@38065: "----------- debugging setContext..pbl_ -----------------";
neuper@37906: states:=[];
neuper@41970: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
neuper@41970:   ("Test", ["sqroot-test","univariate","equation","test"],
neuper@37906:    ["Test","squ-equ-test-subpbl1"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1; modelProblem 1;
neuper@37906: 
neuper@37906: val pos as (p,_) = ([],Pbl);
neuper@37906: val guh = "pbl_equ_univ";
neuper@37906: checkContext 1 pos guh;
neuper@37906: val ((pt,_),_) = get_calc 1;
neuper@37906: val pp = par_pblobj pt p;
neuper@37906: val keID = guh2kestoreID guh;
neuper@37906: case context_pbl keID pt pp of (true,["univariate", "equation"],_,_,_)=>()
neuper@38031: | _ => error "mathengine.sml: context_pbl .. pbl_equ_univ checked";
neuper@37906: 
neuper@37906: case get_obj g_spec pt p of (_, ["e_pblID"], _) => ()
neuper@38031: | _ => error "mathengine.sml: context_pbl .. pbl still empty";
neuper@37906: setContext 1 pos guh;
neuper@37906: val ((pt,_),_) = get_calc 1;
neuper@37906: case get_obj g_spec pt p of (_, ["univariate", "equation"], _) => ()
neuper@38031: | _ => error "mathengine.sml: context_pbl .. pbl set";
neuper@37906: 
neuper@37906: 
neuper@37906: setContext 1 pos "met_eq_lin";
neuper@37906: val ((pt,_),_) = get_calc 1;
neuper@37906: case get_obj g_spec pt p of (_,  _, ["LinEq", "solve_lineq_equation"]) => ()
neuper@38031: | _ => error "mathengine.sml: context_pbl .. pbl set";
neuper@37906: 
neuper@37906: 
neuper@38065: "----------- tryrefine ----------------------------------";
neuper@38065: "----------- tryrefine ----------------------------------";
neuper@38065: "----------- tryrefine ----------------------------------";
neuper@37906: states:=[];
neuper@37906: CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", 
neuper@37906: 	    "solveFor x", "solutions L"],
neuper@38058: 	   ("RatEq",["univariate","equation"],["no_met"]))];
neuper@37906: Iterator 1;
neuper@37906: moveActiveRoot 1; autoCalculate 1 CompleteCalc;
neuper@37906: 
neuper@37906: refineProblem 1 ([1],Res) "pbl_equ_univ" 
neuper@37906: (*gives "pbl_equ_univ_rat" correct*);
neuper@37906: 
neuper@37906: refineProblem 1 ([1],Res) (pblID2guh ["linear","univariate","equation"])
neuper@38065: (*gives "pbl_equ_univ_lin" incorrect*);
neuper@38065: 
neuper@38065: 
neuper@41982: "----------- fun step: Apply_Method without init_form ---";
neuper@41982: "----------- fun step: Apply_Method without init_form ---";
neuper@41982: "----------- fun step: Apply_Method without init_form ---";
neuper@41982: val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
neuper@41982: val (dI',pI',mI') =
neuper@41982:   ("Test", ["sqroot-test","univariate","equation","test"],
neuper@41982:    ["Test","squ-equ-test-subpbl1"]);
neuper@41982: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@41982: "~~~~~ fun me, args:"; val (_,tac) = nxt;
neuper@41982: val ("ok", (_, _, (pt, p))) = locatetac tac (pt,p);
neuper@41982: "~~~~~ fun step, args:"; val (ip as (_,p_), ptp as (pt,p), tacis) = (p, (pt, e_pos'), []);
neuper@41982: val pIopt = get_pblID (pt,ip);
neuper@41982: ip = ([],Res) (*false*);
neuper@41982: val SOME pI = pIopt;
akargl@42108: (*=== inhibit exn 110718 ? =============================================================
akargl@42108: 
neuper@41982: member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p))
neuper@41982: 			                          (*^^^^^^^^: Apply_Method without init_form*)
akargl@42108: 
akargl@42108: ===== inhibit exn 110718 ? ===========================================================*)
neuper@38065: 
neuper@38065: "----------- fun step -----------------------------------";
neuper@38065: "----------- fun step -----------------------------------";
neuper@38065: "----------- fun step -----------------------------------";
neuper@38065: val p = e_pos'; val c = []; 
neuper@38065: val (p,_,f,nxt,_,pt) = 
neuper@38065:     CalcTreeTEST 
neuper@38065:         [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"], 
neuper@38065:           ("Integrate", ["integrate","function"], ["diff","integration"]))];
neuper@38065: "----- step 1: returns tac = Model_Problem ---";
neuper@38065: val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
neuper@38065: "----- step 2: returns tac =  ---";
neuper@38065: val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
neuper@38065: "----- step 3: returns tac =  ---";
neuper@38065: val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
neuper@38065: "----- step 4: returns tac =  ---";
neuper@38065: val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
neuper@38065: "----- step 5: returns tac =  ---";
neuper@38065: 
akargl@42108: (*========== inhibit exn 110718 =======================================================
neuper@38066: 2002 stops here as well: TODO review actual arguments:
neuper@38065: val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
neuper@38065: "----- step 6: returns tac =  ---";
neuper@38065: val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
neuper@38065: "----- step 7: returns tac =  ---";
neuper@38065: val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
neuper@38065: "----- step 8: returns tac =  ---";
neuper@38065: val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []);
akargl@42108: ============ inhibit exn 110718 =====================================================*)
neuper@38065: 
neuper@38065: 
neuper@38065: "----------- fun autocalc -------------------------------";
neuper@38065: "----------- fun autocalc -------------------------------";
neuper@38065: "----------- fun autocalc -------------------------------";
neuper@38065: val p = e_pos'; val c = []; 
neuper@38065: val (p,_,f,nxt,_,pt) = 
neuper@38065:     CalcTreeTEST 
neuper@38065:         [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"], 
neuper@38065:           ("Integrate",["integrate","function"], ["diff","integration"]))];
neuper@38066: (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
neuper@38066: modeling is skipped FIXME 
neuper@38066:  *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
neuper@38065: tracing "----- step 1 ---";
neuper@38065: val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
neuper@38065: tracing "----- step 2 ---";
neuper@38065: val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
neuper@38065: tracing "----- step 3 ---";
neuper@38065: val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
neuper@38065: tracing "----- step 4 ---";
neuper@38065: val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
neuper@38065: tracing "----- step 5 ---";
neuper@38065: val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
neuper@38065: tracing "----- step 6 ---";
neuper@38065: val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
neuper@38065: tracing "----- step 7 ---";
neuper@38065: val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
neuper@38065: tracing "----- step 8 ---";
neuper@38065: val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt;
neuper@42067: (*========== inhibit exn 110628 ================================================
neuper@42067: WN110628: Integration does not work, see Knowledge/integrate.sml
neuper@42067: 
neuper@41929: if str = "end-of-calculation" andalso 
neuper@41929:    term2str (get_obj g_res pt (fst p)) = "c + x + 1 / 3 * x ^^^ 3" then ()
neuper@38065: else error "mathengine.sml -- fun autocalc -- end";
neuper@42067: ============ inhibit exn 110628 ==============================================*)
neuper@38065: 
neuper@38065: 
neuper@38065: "----------- fun autoCalculate -----------------------------------";
neuper@38065: "----------- fun autoCalculate -----------------------------------";
neuper@38065: "----------- fun autoCalculate -----------------------------------";
neuper@38065: states := [];
neuper@38065: CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)
neuper@38065:     [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
neuper@38065:       ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
neuper@38065: Iterator 1;
neuper@38065: moveActiveRoot 1;
neuper@38066: (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
neuper@38066: modeling is skipped FIXME 
neuper@38066: see test/../interface -- solve_linear as rootpbl FE -- for OTHER expl:
neuper@38066:  setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
neuper@38066:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
neuper@38066: 
neuper@38066:  fetchProposedTactic 1;
neuper@38066:  setNextTactic 1 (Add_Given "solveFor x");
neuper@38066:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@38066: 
neuper@38066:  fetchProposedTactic 1;
neuper@38066:  setNextTactic 1 (Add_Find "solutions L");
neuper@38066:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@38066: 
neuper@38066:  fetchProposedTactic 1;
neuper@38066:  setNextTactic 1 (Specify_Theory "Test");
neuper@38066:  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
neuper@38066: *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
neuper@38065: autoCalculate 1 (Step 1); 
neuper@38065: "----- step 1 ---";
neuper@38065: autoCalculate 1 (Step 1);
neuper@38065: "----- step 2 ---";
neuper@38065: autoCalculate 1 (Step 1);
neuper@38065: "----- step 3 ---";
neuper@38065: autoCalculate 1 (Step 1);
neuper@38065: "----- step 4 ---";
neuper@38065: autoCalculate 1 (Step 1);
neuper@38065: "----- step 5 ---";
neuper@38065: autoCalculate 1 (Step 1);
neuper@38065: "----- step 6 ---";
neuper@38065: autoCalculate 1 (Step 1);
neuper@38065: "----- step 7 ---";
neuper@38065: autoCalculate 1 (Step 1);
neuper@38065: "----- step 8 ---";
neuper@38065: autoCalculate 1 (Step 1);
neuper@38065: val (ptp as (_, p), _) = get_calc 1;
neuper@38065: val (Form t,_,_) = pt_extract ptp;
akargl@42108: 
neuper@38065: if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()
neuper@38065: else error "mathengine.sml -- fun autoCalculate -- end";
neuper@38065: 
neuper@42067: "----------- fun autoCalculate..CompleteCalc ------------";
neuper@42067: "----------- fun autoCalculate..CompleteCalc ------------";
neuper@42067: "----------- fun autoCalculate..CompleteCalc ------------";
neuper@42067:  states:=[];
neuper@42067:  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
neuper@42067:    ("Test", ["sqroot-test","univariate","equation","test"],
neuper@42067:     ["Test","squ-equ-test-subpbl1"]))];
neuper@42067:  Iterator 1;
neuper@42103:  moveActiveRoot 1; 
neuper@42103: (*autoCalculate 1 CompleteCalc; (*WAS <SYSERROR>..<ERROR> error in kernel </ERROR>*)*)
neuper@42103: "~~~~~ fun autoCalculate, args:"; val (cI, auto) = (1, CompleteCalc);
neuper@42103: val pold = get_pos cI 1;
neuper@42103: (*autocalc [] pold (get_calc cI) auto;  (*WAS Type unification failed
neuper@42103:   Type error in application: incompatible operand type
neuper@42103:   Operator:  solveFor :: real \<Rightarrow> una
neuper@42103:   Operand:   x :: 'a *)*)
neuper@42103: "~~~~~ fun autocalc, args:"; val (c, (pos as (_,p_)), ((pt,_), _), auto) 
neuper@42103:                                = ([] : pos' list, pold, (get_calc cI), auto);
neuper@42103: autoord auto > 3 andalso just_created (pt, pos); (*true*)
neuper@42103: val ptp = all_modspec (pt, pos);
neuper@42103: "TODO all_modspec: preconds for rootpbl";
neuper@42103: (*all_solve auto c ptp; (*WAS Type unification failed...*)*)
neuper@42103: "~~~~~ and all_solve, args:"; val (auto, c, (ptp as (pt, pos as (p,_)))) =
neuper@42103:                                                                   (auto, c, ptp);
neuper@42103:     val (_,_,mI) = get_obj g_spec pt p
neuper@42103:     val ctxt = get_ctxt pt pos
neuper@42103:     val (ttt, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
neuper@42103: (* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*) pos = ([], Met)*)
neuper@42103: "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
neuper@42103:                                                            (auto, (c @ c'), ptp);
neuper@42103: p = ([], Res) (*false p = ([1], Frm)*);
neuper@42103: member op = [Pbl,Met] p_ (*false*);
neuper@42103: val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "norm_equation"*)
neuper@42103: (* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
neuper@42103: "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
neuper@42103:                                                            (auto, (c @ c'), ptp');
neuper@42103: p = ([], Res) (*false p = ([1], Res)*);
neuper@42103: member op = [Pbl,Met] p_ (*false*);
neuper@42103: val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "Test_simplify"*)
neuper@42103: (* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*)
neuper@42103: "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
neuper@42103:                                                            (auto, (c @ c'), ptp');
neuper@42103: p = ([], Res) (*false p = ([2], Res)*);
neuper@42103: member op = [Pbl,Met] p_ (*false*);
neuper@42103: val ((Subproblem _, tac_, (_, is))::_, c', ptp') = nxt_solve_ ptp;
neuper@42103: autoord auto < 5 (*false*);
neuper@42103: (* val ptp = all_modspec ptp' (*WAS Type unification failed...*)*)
neuper@42103: "~~~~~ fun all_modspec, args:"; val (pt, pos as (p,_)) = (ptp');
neuper@42103:     val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
neuper@42103:     val thy = assoc_thy dI;
neuper@42103: 	    val {ppc, ...} = get_met mI;
neuper@42103: (*  val (mors, ctxt) = prep_ori fmz_ thy ppc; WAS Type unification failed because
neuper@42103: val ctxt' = dI |> Thy_Info.get_theory |> ProofContext.init_global;
neuper@42103: (parseNEW ctxt' "x" |> the |> type_of) = TFree ("'a",[]); 
neuper@42103:                                                ^^^^^ *)
neuper@42103: (*vvv from:  | assod pt _ (Subproblem'...*)
neuper@42103:     val (fmz_, vals) = oris2fmz_vals pors;
neuper@42103: (**)
neuper@42103:     val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global 
neuper@42103:       |> declare_constraints' vals
neuper@42103: (**)
neuper@42103: (*^^^ from:  | assod pt _ (Subproblem'...*)
neuper@42103: val [(1, [1], "#Given", dsc_eq, [equality]),
neuper@42103:      (2, [1], "#Given", dsc_solvefor, [xxx]),
neuper@42103:      (3, [1], "#Find", dsc_solutions, [x_i])] = pors;
neuper@42103: if term2str xxx = "x" andalso type_of xxx = HOLogic.realT then () 
neuper@42103: else error "autoCalculate..CompleteCalc: SubProblem broken 1";
neuper@42103:     val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
neuper@42103: 	    val pt = update_metppc pt p (map (ori2Coritm ppc) pors);
neuper@42103: 	    val pt = update_spec pt p (dI,pI,mI);
neuper@42103:     val pt = update_ctxt pt p ctxt;
neuper@42103: "~~~~~ return to complete_solve, args:"; val (ptp) = (pt, (p,Met));
neuper@42103: val (msg, c, (pt, p)) = complete_solve auto (c @ c') ptp;
neuper@42103: if msg = "end-of-calculation" andalso c = [] andalso p = ([], Res) then ()
neuper@42103: else error "autoCalculate..CompleteCalc: final result";
neuper@42103: if terms2strs (get_assumptions_ pt p) = 
neuper@42105:   ["matches (?a = ?b) (-1 + x = 0)", (*precond of submet*) 
neuper@42104:    "x = 1",                          (*result of subpbl and rootpbl*)
neuper@42104:    "precond_rootmet x"]              (*precond of rootmet*)
neuper@42103: then () else error "autoCalculate..CompleteCalc: ctxt at final result";
neuper@42067:  
akargl@42108: 
t@42225: "----------- search for Or_to_List ----------------------";
t@42225: "----------- search for Or_to_List ----------------------";
t@42225: "--------- search for Or_to_List ------------------------";
t@42225: val fmz = ["equality (x^^^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"];
t@42225: val (dI',pI',mI') = ("Isac", ["univariate","equation"], ["no_met"])
t@42225: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
t@42225: "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ptree)) = 
t@42225:                             (nxt, p, [], pt);
t@42225: val ("ok", (_, _, ptp))  = locatetac tac (pt,p)
t@42225: val (pt, p) = ptp;
t@42225: "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
t@42225:                           (p, ((pt, e_pos'),[]));
t@42225: val pIopt = get_pblID (pt,ip);
t@42225: ip = ([],Res); (*false*)
t@42225: ip = p; (*false*)
t@42225: member op = [Pbl,Met] p_; (*false*)
t@42225: "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
t@42225: e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
t@42225: val thy' = get_obj g_domID pt (par_pblobj pt p);
t@42225: val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
t@42225: val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; (*WAS Empty_Tac_: tac_*)
t@42225: case tac_ of Or_to_List' _ => ()
t@42225: | _ => error "Or_to_List broken ?"
akargl@42108: 
neuper@42279: "----------- check thy in CalcTreeTEST ------------------";
neuper@42279: "----------- check thy in CalcTreeTEST ------------------";
neuper@42279: "----------- check thy in CalcTreeTEST ------------------";
neuper@42279: "WN1109 with Inverse_Z_Transform.thy when starting tests with CalcTreeTEST \n" ^
neuper@42279: "we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^
neuper@42279: "Below there are the steps which found out the reason: \n" ^
neuper@42279: "store_pbt mistakenly stored that theory.";
neuper@42279: val ctxt = ProofContext.init_global @{theory Isac};
neuper@42279: val SOME t = parseNEW ctxt "filterExpression (X  = 3 / (z - 1/4 + -1/8 * (1/(z::real))))";
neuper@42279: val SOME t = parseNEW ctxt "stepResponse (x[n::real]::bool)";
akargl@42108: 
neuper@42279: val fmz = ["filterExpression (X  = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", 
neuper@42279:   "stepResponse (x[n::real]::bool)"];
neuper@42279: val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"], 
neuper@42279:   ["SignalProcessing","Z_Transform","inverse"]);
neuper@42279: 
neuper@42279: val (p,_,fb,nxt,_,pt)  = CalcTreeTEST [(fmz, (dI,pI,mI))]; 
neuper@42279: (*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
neuper@42279: 
neuper@42279: "~~~~~ T fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI,pI,mI))];
neuper@42279: "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
neuper@42279: 	      val thy = assoc_thy dI;
neuper@42279:     mI = ["no_met"]; (*false*)
neuper@42279: 		      val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
neuper@42279: 	      val {cas, ppc, thy=thy',...} = get_pbt pI; (*take dI from _refined_ pbl*)
neuper@42279: 	"tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
neuper@42279:       val dI = theory2theory' (maxthy thy thy');
neuper@42279: "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
neuper@42279:     cas = NONE; (*true*)
neuper@42279: 	      val hdl = pblterm dI pI;
neuper@42279:         val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
neuper@42279: 				  (pors, (dI, pI, mI), hdl)
neuper@42279:         val pt = update_ctxt pt [] pctxt;
neuper@42279: 
neuper@42279: "~~~~~ fun nxt_specif, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl)));
neuper@42279:       val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p;
neuper@42279: "tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*)
neuper@42279: 
neuper@42279: "~~~~~ fun some_spec, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);
neuper@42279: dI = e_domID; (*true*)
neuper@42279: odI = "Build_Inverse_Z_Transform"; (*true*)
neuper@42279: dI = "e_domID"; (*true*)
neuper@42279: "~~~~~ after fun some_spec:";
neuper@42279:       val (dI, pI, mI) = some_spec ospec spec;
neuper@42279: "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
neuper@42279:       val thy = assoc_thy dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
neuper@42279: