1.1 --- a/src/sml/ME/modspec.sml Thu Feb 10 18:56:48 2005 +0100
1.2 +++ b/src/sml/ME/modspec.sml Thu Feb 10 18:56:48 2005 +0100
1.3 @@ -1776,22 +1776,20 @@
1.4
1.5 | pt_extract (pt,(p,Res)) =
1.6 let val (f, asm) = get_obj g_result pt p
1.7 - val tac = Empty_Tac
1.8 -(*
1.9 val tac = if last_onlev pt p
1.10 then if is_pblobj' pt p
1.11 then let val (PblObj{spec=(_,pI,_),...})= get_obj I pt p
1.12 in if pI = e_pblID then None
1.13 else Some (Check_Postcond pI) end
1.14 - else Some End_Trans
1.15 - else
1.16 -
1.17 -
1.18 -@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
1.19 -
1.20 -
1.21 -*)
1.22 - in (Form f, Some tac, asm) end
1.23 + else Some End_Trans (*WN0502 TODO for other branches*)
1.24 + else let val p' = lev_on p
1.25 + in if is_pblobj' pt p'
1.26 + then let val (PblObj{origin = (_,(dI,pI,_),_),...}) =
1.27 + get_obj I pt p'
1.28 + in Some (Subproblem (dI, pI)) end
1.29 + else Some (get_obj g_tac pt p') end
1.30 + (*because this Frm is not on worksheet ~~~*)
1.31 + in (Form f, tac, asm) end
1.32
1.33 | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =
1.34 (* val (pt, pos as (p,p_(*Frm,Pbl*))) = ptp;
1.35 @@ -1799,6 +1797,7 @@
1.36 let val ppobj = get_obj I pt p
1.37 val f = if is_pblobj ppobj then pt_model ppobj p_
1.38 else get_obj pt_form pt p
1.39 + val tac = g_tac ppobj
1.40 in (f, Some Empty_Tac, []) end;
1.41
1.42
2.1 --- a/src/sml/systest/ctree.sml Thu Feb 10 18:56:48 2005 +0100
2.2 +++ b/src/sml/systest/ctree.sml Thu Feb 10 18:56:48 2005 +0100
2.3 @@ -29,6 +29,12 @@
2.4 (******************************************************************)
2.5 (* val get_trace = SAVE_get_trace; *)
2.6 (******************************************************************)
2.7 +
2.8 +"=====new ptree 4 ratequation ====================================";
2.9 +"-------------- pt_extract form, tac, asm<>[] --------------------";
2.10 +"=====new ptree 5 minisubpbl =====================================";
2.11 +"-------------- pt_extract form, tac, asm ------------------------";
2.12 +
2.13 "-----------------------------------------------------------------";
2.14
2.15
2.16 @@ -670,9 +676,62 @@
2.17 | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1e";
2.18 *)
2.19
2.20 -
2.21 -
2.22 -
2.23 (******************************************************************)
2.24 (**) val get_trace = SAVE_get_trace; (**)
2.25 (******************************************************************)
2.26 +
2.27 +
2.28 +"=====new ptree 4 ratequation ====================================";
2.29 +"=====new ptree 4 ratequation ====================================";
2.30 +"=====new ptree 4 ratequation ====================================";
2.31 +states:=[];
2.32 +CalcTree
2.33 +[(["equality (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)",
2.34 + "solveFor x","solutions L"],
2.35 + ("RatEq.thy",["univariate","equation"],["no_met"]))];
2.36 +Iterator 1; moveActiveRoot 1;
2.37 +autoCalculate 1 CompleteCalc;
2.38 +val ((pt,_),_) = get_calc 1;
2.39 +show_pt pt;
2.40 +
2.41 +"-------------- pt_extract form, tac, asm<>[] --------------------";
2.42 +"-------------- pt_extract form, tac, asm<>[] --------------------";
2.43 +"-------------- pt_extract form, tac, asm<>[] --------------------";
2.44 +val (Form form, Some tac, asm) = pt_extract (pt, ([3], Res));
2.45 +case (term2str form, tac, terms2strs asm) of
2.46 + ("(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))",
2.47 + Subproblem
2.48 + ("PolyEq.thy",
2.49 + ["normalize", "polynomial", "univariate", "equation"]),
2.50 + ["9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0"]) => ()
2.51 + | _ => raise error "diff.behav.in ctree.sml: pt_extract asm<>[]";
2.52 +
2.53 +
2.54 +"=====new ptree 5 minisubpbl =====================================";
2.55 +"=====new ptree 5 minisubpbl =====================================";
2.56 +"=====new ptree 5 minisubpbl =====================================";
2.57 +states:=[];
2.58 +CalcTree
2.59 + [(["equality (x+1=2)", "solveFor x","solutions L"],
2.60 + ("Test.thy",
2.61 + ["sqroot-test","univariate","equation","test"],
2.62 + ["Test","squ-equ-test-subpbl1"]))];
2.63 +Iterator 1; moveActiveRoot 1;
2.64 +autoCalculate 1 CompleteCalc;
2.65 +val ((pt,_),_) = get_calc 1;
2.66 +show_pt pt;
2.67 +
2.68 +"-------------- pt_extract form, tac, asm ------------------------";
2.69 +"-------------- pt_extract form, tac, asm ------------------------";
2.70 +"-------------- pt_extract form, tac, asm ------------------------";
2.71 +val (ModSpec (_,_,form,_,_,_), Some tac, asm) = pt_extract (pt, ([], Pbl));
2.72 +case (term2str form, tac, terms2strs asm) of
2.73 + ("solve (x + 1 = 2, x)",
2.74 + Empty_Tac, (*?????????????????????????????????????????????????*)
2.75 + []) => ()
2.76 + | _ => raise error "diff.behav.in ctree.sml: pt_extract ([], Pbl)";
2.77 +
2.78 +val (Form form, Some tac, asm) = pt_extract (pt, ([1], Frm));
2.79 +case (term2str form, tac, terms2strs asm) of
2.80 + ("x + 1 = 2", Empty_Tac, []) => ()
2.81 + | _ => raise error "diff.behav.in ctree.sml: pt_extract ([1], Frm)";