1.1 --- a/src/Tools/isac/Frontend/interface.sml Fri May 25 16:30:15 2012 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Wed Jun 13 07:28:39 2012 +0200
1.3 @@ -259,15 +259,16 @@
1.4 handle PTREE str => sysERROR2xml cI str
1.5 end)
1.6 handle _ => sysERROR2xml cI "error in kernel";
1.7 -(*.version 2: fetch _applicable_ _elementary_ (ie. recursively
1.8 - decompose rule-sets) Rewrite*, Calculate .*)
1.9 +(*WN120611 took version 1 again
1.10 + version 2: fetch _applicable_ _elementary_ (ie. recursively
1.11 + decompose rule-sets) Rewrite*, Calculate
1.12 fun fetchApplicableTactics cI (scope:int) (p:pos') =
1.13 (let val ((pt, _), _) = get_calc cI
1.14 in (applicabletacticsOK cI (sel_appl_atomic_tacs pt p))
1.15 handle PTREE str => sysERROR2xml cI str
1.16 end)
1.17 handle _ => sysERROR2xml cI "error in kernel";
1.18 -
1.19 +*)
1.20 fun getAssumptions cI (p:pos') =
1.21 (let val ((pt,_),_) = get_calc cI
1.22 val (_, _, asms) = pt_extract (pt, p)
2.1 --- a/src/Tools/isac/Interpret/script.sml Fri May 25 16:30:15 2012 +0200
2.2 +++ b/src/Tools/isac/Interpret/script.sml Wed Jun 13 07:28:39 2012 +0200
2.3 @@ -1657,24 +1657,26 @@
2.4 if is_spec_pos p_
2.5 then [get_obj g_tac pt p]
2.6 else
2.7 - let val pp = par_pblobj pt p
2.8 - val thy' = (get_obj g_domID pt pp):theory'
2.9 - val thy = assoc_thy thy'
2.10 - val metID = get_obj g_metID pt pp
2.11 - val metID' =if metID = e_metID
2.12 - then (thd3 o snd3) (get_obj g_origin pt pp)
2.13 - else metID
2.14 - val {scr=Script sc,srls,erls,rew_ord'=ro,...} = get_met metID'
2.15 - val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
2.16 - val alltacs = (*we expect at least 1 stac in a script*)
2.17 - map ((stac2tac pt thy) o rep_stacexpr o #2 o
2.18 - (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
2.19 - val f = case p_ of
2.20 - Frm => get_obj g_form pt p
2.21 - | Res => (fst o (get_obj g_result pt)) p
2.22 - (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
2.23 - in (distinct o flat o
2.24 - (map (atomic_appl_tacs thy ro erls f))) alltacs end;
2.25 + let
2.26 + val pp = par_pblobj pt p
2.27 + val thy' = (get_obj g_domID pt pp):theory'
2.28 + val thy = assoc_thy thy'
2.29 + val metID = get_obj g_metID pt pp
2.30 + val metID' =
2.31 + if metID = e_metID
2.32 + then (thd3 o snd3) (get_obj g_origin pt pp)
2.33 + else metID
2.34 + val {scr=Script sc,srls,erls,rew_ord'=ro,...} = get_met metID'
2.35 + val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
2.36 + val alltacs = (*we expect at least 1 stac in a script*)
2.37 + map ((stac2tac pt thy) o rep_stacexpr o #2 o
2.38 + (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
2.39 + val f =
2.40 + case p_ of
2.41 + Frm => get_obj g_form pt p
2.42 + | Res => (fst o (get_obj g_result pt)) p
2.43 + (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
2.44 + in (distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs end;
2.45
2.46
2.47 (*
3.1 --- a/src/Tools/isac/ROOT.ML Fri May 25 16:30:15 2012 +0200
3.2 +++ b/src/Tools/isac/ROOT.ML Wed Jun 13 07:28:39 2012 +0200
3.3 @@ -4,7 +4,7 @@
3.4 $ ls -l /home/neuper/.isabelle/heaps/polyml-5.4.0_x86-linux/Isac
3.5
3.6 Knowledge/Isac.thy
3.7 -ML {* val version_isac = "isac version 120504 15:33"; *}
3.8 +ML {* val version_isac = "isac version 120612 12:12"; *}
3.9 *)
3.10
3.11 use_thys ["Build_Isac"];
4.1 --- a/test/Tools/isac/Frontend/interface.sml Fri May 25 16:30:15 2012 +0200
4.2 +++ b/test/Tools/isac/Frontend/interface.sml Wed Jun 13 07:28:39 2012 +0200
4.3 @@ -1001,6 +1001,9 @@
4.4 "--------- getTactic, fetchApplicableTactics ------------";
4.5 "--------- getTactic, fetchApplicableTactics ------------";
4.6 "--------- getTactic, fetchApplicableTactics ------------";
4.7 +(* compare test/../script.sml
4.8 +"----------- fun sel_rules ---------------------------------------";
4.9 +*)
4.10 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
4.11 ("Test", ["sqroot-test","univariate","equation","test"],
4.12 ["Test","squ-equ-test-subpbl1"]))];
5.1 --- a/test/Tools/isac/Interpret/script.sml Fri May 25 16:30:15 2012 +0200
5.2 +++ b/test/Tools/isac/Interpret/script.sml Wed Jun 13 07:28:39 2012 +0200
5.3 @@ -12,11 +12,13 @@
5.4 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
5.5 "----------- Take as 1st stac in script --------------------------";
5.6 "----------- 'trace_script' from outside 'fun me '----------------";
5.7 +"----------- fun sel_rules ---------------------------------------";
5.8 +"----------- fun sel_appl_atomic_tacs ----------------------------";
5.9 "-----------------------------------------------------------------";
5.10 "-----------------------------------------------------------------";
5.11 "-----------------------------------------------------------------";
5.12
5.13 -val thy= @{theory Isac};
5.14 +val thy = @{theory Isac};
5.15
5.16 "----------- WN0509 why does next_tac doesnt find Substitute -----";
5.17 "----------- WN0509 why does next_tac doesnt find Substitute -----";
5.18 @@ -494,4 +496,105 @@
5.19 term2str res = "x = 0 + -1 * -1";(* scrstate after isolate_bdv, before Test_simplify *)
5.20 term2str (go loc_ sc) = "Rewrite_Set_Inst [(bdv, v_v)] isolate_bdv False";
5.21
5.22 +"----------- fun sel_rules ---------------------------------------";
5.23 +"----------- fun sel_rules ---------------------------------------";
5.24 +"----------- fun sel_rules ---------------------------------------";
5.25 +(* compare test/../interface.sml
5.26 +"--------- getTactic, fetchApplicableTactics ------------";
5.27 +*)
5.28 + states:=[];
5.29 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
5.30 + ("Test", ["sqroot-test","univariate","equation","test"],
5.31 + ["Test","squ-equ-test-subpbl1"]))];
5.32 + Iterator 1;
5.33 + moveActiveRoot 1;
5.34 + autoCalculate 1 CompleteCalc;
5.35 + val ((pt,_),_) = get_calc 1;
5.36 + show_pt pt;
5.37
5.38 +(*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
5.39 + val tacs = sel_rules pt ([],Pbl);
5.40 + if tacs = [Apply_Method ["Test", "squ-equ-test-subpbl1"]] then ()
5.41 + else error "script.sml: diff.behav. in sel_rules ([],Pbl)";
5.42 +
5.43 + val tacs = sel_rules pt ([1],Res);
5.44 + if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
5.45 + Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
5.46 + Check_elementwise "Assumptions"] then ()
5.47 + else error "script.sml: diff.behav. in sel_rules ([1],Res)";
5.48 +
5.49 + val tacs = sel_rules pt ([3],Pbl);
5.50 + if tacs = [Apply_Method ["Test", "solve_linear"]] then ()
5.51 + else error "script.sml: diff.behav. in sel_rules ([3],Pbl)";
5.52 +
5.53 + val tacs = sel_rules pt ([3,1],Res);
5.54 + if tacs = [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"),
5.55 + Rewrite_Set "Test_simplify"] then ()
5.56 + else error "script.sml: diff.behav. in sel_rules ([3,1],Res)";
5.57 +
5.58 + val tacs = sel_rules pt ([3],Res);
5.59 + if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
5.60 + Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
5.61 + Check_elementwise "Assumptions"] then ()
5.62 + else error "script.sml: diff.behav. in sel_rules ([3],Res)";
5.63 +
5.64 + val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str];
5.65 + if tacs = [Tac "no tactics applicable at the end of a calculation"] then ()
5.66 + else error "script.sml: diff.behav. in sel_rules ([],Res)";
5.67 +
5.68 +"----------- fun sel_appl_atomic_tacs ----------------------------";
5.69 +"----------- fun sel_appl_atomic_tacs ----------------------------";
5.70 +"----------- fun sel_appl_atomic_tacs ----------------------------";
5.71 + states:=[];
5.72 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
5.73 + ("Test", ["sqroot-test","univariate","equation","test"],
5.74 + ["Test","squ-equ-test-subpbl1"]))];
5.75 + Iterator 1;
5.76 + moveActiveRoot 1;
5.77 + autoCalculate 1 CompleteCalc;
5.78 +
5.79 +(*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
5.80 + fetchApplicableTactics 1 99999 ([],Pbl);
5.81 +
5.82 + fetchApplicableTactics 1 99999 ([1],Res);
5.83 +"~~~~~ fun fetchApplicableTactics, args:"; val (cI, (scope:int), (p:pos')) = (1, 99999, ([1],Res));
5.84 +val ((pt, _), _) = get_calc cI;
5.85 +(*version 1:*)
5.86 +if sel_rules pt p = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
5.87 + Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
5.88 + Check_elementwise "Assumptions"] then ()
5.89 +else error "fetchApplicableTactics ([1],Res) changed";
5.90 +(*version 2:*)
5.91 +(*WAS:
5.92 +sel_appl_atomic_tacs pt p;
5.93 +...
5.94 +### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["linear","univariate","equation","test"])'
5.95 +### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
5.96 +*)
5.97 +
5.98 +"~~~~~ fun sel_appl_atomic_tacs, args:"; val (pt, (p,p_)) = (pt, p);
5.99 +is_spec_pos p_ = false;
5.100 + val pp = par_pblobj pt p
5.101 + val thy' = (get_obj g_domID pt pp):theory'
5.102 + val thy = assoc_thy thy'
5.103 + val metID = get_obj g_metID pt pp
5.104 + val metID' =
5.105 + if metID = e_metID
5.106 + then (thd3 o snd3) (get_obj g_origin pt pp)
5.107 + else metID
5.108 + val {scr=Script sc,srls,erls,rew_ord'=ro,...} = get_met metID'
5.109 + val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
5.110 + val alltacs = (*we expect at least 1 stac in a script*)
5.111 + map ((stac2tac pt thy) o rep_stacexpr o #2 o
5.112 + (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
5.113 + val f =
5.114 + case p_ of
5.115 + Frm => get_obj g_form pt p
5.116 + | Res => (fst o (get_obj g_result pt)) p
5.117 +(*WN120611 stopped and took version 1 again for fetchApplicableTactics !
5.118 +(distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs
5.119 +...
5.120 +### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["linear","univariate","equation","test"])'
5.121 +### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
5.122 +*)
5.123 +
6.1 --- a/test/Tools/isac/OLDTESTS/script.sml Fri May 25 16:30:15 2012 +0200
6.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Wed Jun 13 07:28:39 2012 +0200
6.3 @@ -303,41 +303,6 @@
6.4 "--------- sel_rules ---------------------------------------------";
6.5 "--------- sel_rules ---------------------------------------------";
6.6 "--------- sel_rules ---------------------------------------------";
6.7 - states:=[];
6.8 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.9 - ("Test", ["sqroot-test","univariate","equation","test"],
6.10 - ["Test","squ-equ-test-subpbl1"]))];
6.11 - Iterator 1;
6.12 - moveActiveRoot 1;
6.13 - autoCalculate 1 CompleteCalc;
6.14 - val ((pt,_),_) = get_calc 1;
6.15 - show_pt pt;
6.16 +(* mv test/../script.sml: -----> *)
6.17 +"----------- fun sel_rules ---------------------------------------"
6.18
6.19 - val tacs = sel_rules pt ([],Pbl);
6.20 - if tacs = [Apply_Method ["Test", "squ-equ-test-subpbl1"]] then ()
6.21 - else error "script.sml: diff.behav. in sel_rules ([],Pbl)";
6.22 -
6.23 - val tacs = sel_rules pt ([1],Res);
6.24 - if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
6.25 - Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
6.26 - Check_elementwise "Assumptions"] then ()
6.27 - else error "script.sml: diff.behav. in sel_rules ([1],Res)";
6.28 -
6.29 - val tacs = sel_rules pt ([3],Pbl);
6.30 - if tacs = [Apply_Method ["Test", "solve_linear"]] then ()
6.31 - else error "script.sml: diff.behav. in sel_rules ([3],Pbl)";
6.32 -
6.33 - val tacs = sel_rules pt ([3,1],Res);
6.34 - if tacs = [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"),
6.35 - Rewrite_Set "Test_simplify"] then ()
6.36 - else error "script.sml: diff.behav. in sel_rules ([3,1],Res)";
6.37 -
6.38 - val tacs = sel_rules pt ([3],Res);
6.39 - if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
6.40 - Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
6.41 - Check_elementwise "Assumptions"] then ()
6.42 - else error "script.sml: diff.behav. in sel_rules ([3],Res)";
6.43 -
6.44 - val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str];
6.45 - if tacs = [Tac "no tactics applicable at the end of a calculation"] then ()
6.46 - else error "script.sml: diff.behav. in sel_rules ([],Res)";
7.1 --- a/test/Tools/isac/Test_Some.thy Fri May 25 16:30:15 2012 +0200
7.2 +++ b/test/Tools/isac/Test_Some.thy Wed Jun 13 07:28:39 2012 +0200
7.3 @@ -1,7 +1,7 @@
7.4
7.5 theory Test_Some imports Isac begin
7.6
7.7 -use"../../../test/Tools/isac/Frontend/interface.sml"
7.8 +use"../../../test/Tools/isac/Interpret/script.sml"
7.9
7.10 ML {*
7.11 val thy = @{theory "Isac"};