neuper@37906: (* test for sml/ME/mathengine.sml
neuper@37906:    authors: Walther Neuper 2000, 2006
neuper@37906:    (c) due to copyright terms
neuper@37906: 
neuper@37906: use"../smltest/ME/mathengine.sml";
neuper@37906: use"mathengine.sml";
neuper@37906: *)
neuper@37906: 
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "table of contents -----------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "----------- debugging setContext..pbl_ --------------------------";
neuper@37906: "----------- tryrefine -------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: "----------- debugging setContext..pbl_ --------------------------";
neuper@37906: "----------- debugging setContext..pbl_ --------------------------";
neuper@37906: "----------- debugging setContext..pbl_ --------------------------";
neuper@37906: states:=[];
neuper@37906: CalcTree
neuper@37906: [(["equality (x+1=2)", "solveFor x","solutions L"], 
neuper@37906:   ("Test.thy", 
neuper@37906:    ["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@37906: "----------- tryrefine -------------------------------------------";
neuper@37906: "----------- tryrefine -------------------------------------------";
neuper@37906: "----------- 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@37906: 	   ("RatEq.thy",["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@37906: (*ives "pbl_equ_univ_lin" incorrect*);