1.1 --- a/test/Tools/isac/Interpret/script.sml Fri May 25 16:30:15 2012 +0200
1.2 +++ b/test/Tools/isac/Interpret/script.sml Wed Jun 13 07:28:39 2012 +0200
1.3 @@ -12,11 +12,13 @@
1.4 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
1.5 "----------- Take as 1st stac in script --------------------------";
1.6 "----------- 'trace_script' from outside 'fun me '----------------";
1.7 +"----------- fun sel_rules ---------------------------------------";
1.8 +"----------- fun sel_appl_atomic_tacs ----------------------------";
1.9 "-----------------------------------------------------------------";
1.10 "-----------------------------------------------------------------";
1.11 "-----------------------------------------------------------------";
1.12
1.13 -val thy= @{theory Isac};
1.14 +val thy = @{theory Isac};
1.15
1.16 "----------- WN0509 why does next_tac doesnt find Substitute -----";
1.17 "----------- WN0509 why does next_tac doesnt find Substitute -----";
1.18 @@ -494,4 +496,105 @@
1.19 term2str res = "x = 0 + -1 * -1";(* scrstate after isolate_bdv, before Test_simplify *)
1.20 term2str (go loc_ sc) = "Rewrite_Set_Inst [(bdv, v_v)] isolate_bdv False";
1.21
1.22 +"----------- fun sel_rules ---------------------------------------";
1.23 +"----------- fun sel_rules ---------------------------------------";
1.24 +"----------- fun sel_rules ---------------------------------------";
1.25 +(* compare test/../interface.sml
1.26 +"--------- getTactic, fetchApplicableTactics ------------";
1.27 +*)
1.28 + states:=[];
1.29 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.30 + ("Test", ["sqroot-test","univariate","equation","test"],
1.31 + ["Test","squ-equ-test-subpbl1"]))];
1.32 + Iterator 1;
1.33 + moveActiveRoot 1;
1.34 + autoCalculate 1 CompleteCalc;
1.35 + val ((pt,_),_) = get_calc 1;
1.36 + show_pt pt;
1.37
1.38 +(*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
1.39 + val tacs = sel_rules pt ([],Pbl);
1.40 + if tacs = [Apply_Method ["Test", "squ-equ-test-subpbl1"]] then ()
1.41 + else error "script.sml: diff.behav. in sel_rules ([],Pbl)";
1.42 +
1.43 + val tacs = sel_rules pt ([1],Res);
1.44 + if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
1.45 + Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
1.46 + Check_elementwise "Assumptions"] then ()
1.47 + else error "script.sml: diff.behav. in sel_rules ([1],Res)";
1.48 +
1.49 + val tacs = sel_rules pt ([3],Pbl);
1.50 + if tacs = [Apply_Method ["Test", "solve_linear"]] then ()
1.51 + else error "script.sml: diff.behav. in sel_rules ([3],Pbl)";
1.52 +
1.53 + val tacs = sel_rules pt ([3,1],Res);
1.54 + if tacs = [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"),
1.55 + Rewrite_Set "Test_simplify"] then ()
1.56 + else error "script.sml: diff.behav. in sel_rules ([3,1],Res)";
1.57 +
1.58 + val tacs = sel_rules pt ([3],Res);
1.59 + if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
1.60 + Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
1.61 + Check_elementwise "Assumptions"] then ()
1.62 + else error "script.sml: diff.behav. in sel_rules ([3],Res)";
1.63 +
1.64 + val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str];
1.65 + if tacs = [Tac "no tactics applicable at the end of a calculation"] then ()
1.66 + else error "script.sml: diff.behav. in sel_rules ([],Res)";
1.67 +
1.68 +"----------- fun sel_appl_atomic_tacs ----------------------------";
1.69 +"----------- fun sel_appl_atomic_tacs ----------------------------";
1.70 +"----------- fun sel_appl_atomic_tacs ----------------------------";
1.71 + states:=[];
1.72 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.73 + ("Test", ["sqroot-test","univariate","equation","test"],
1.74 + ["Test","squ-equ-test-subpbl1"]))];
1.75 + Iterator 1;
1.76 + moveActiveRoot 1;
1.77 + autoCalculate 1 CompleteCalc;
1.78 +
1.79 +(*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
1.80 + fetchApplicableTactics 1 99999 ([],Pbl);
1.81 +
1.82 + fetchApplicableTactics 1 99999 ([1],Res);
1.83 +"~~~~~ fun fetchApplicableTactics, args:"; val (cI, (scope:int), (p:pos')) = (1, 99999, ([1],Res));
1.84 +val ((pt, _), _) = get_calc cI;
1.85 +(*version 1:*)
1.86 +if sel_rules pt p = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
1.87 + Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
1.88 + Check_elementwise "Assumptions"] then ()
1.89 +else error "fetchApplicableTactics ([1],Res) changed";
1.90 +(*version 2:*)
1.91 +(*WAS:
1.92 +sel_appl_atomic_tacs pt p;
1.93 +...
1.94 +### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["linear","univariate","equation","test"])'
1.95 +### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
1.96 +*)
1.97 +
1.98 +"~~~~~ fun sel_appl_atomic_tacs, args:"; val (pt, (p,p_)) = (pt, p);
1.99 +is_spec_pos p_ = false;
1.100 + val pp = par_pblobj pt p
1.101 + val thy' = (get_obj g_domID pt pp):theory'
1.102 + val thy = assoc_thy thy'
1.103 + val metID = get_obj g_metID pt pp
1.104 + val metID' =
1.105 + if metID = e_metID
1.106 + then (thd3 o snd3) (get_obj g_origin pt pp)
1.107 + else metID
1.108 + val {scr=Script sc,srls,erls,rew_ord'=ro,...} = get_met metID'
1.109 + val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
1.110 + val alltacs = (*we expect at least 1 stac in a script*)
1.111 + map ((stac2tac pt thy) o rep_stacexpr o #2 o
1.112 + (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
1.113 + val f =
1.114 + case p_ of
1.115 + Frm => get_obj g_form pt p
1.116 + | Res => (fst o (get_obj g_result pt)) p
1.117 +(*WN120611 stopped and took version 1 again for fetchApplicableTactics !
1.118 +(distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs
1.119 +...
1.120 +### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["linear","univariate","equation","test"])'
1.121 +### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
1.122 +*)
1.123 +