5 |
5 |
6 theory Test_Some imports Isac begin |
6 theory Test_Some imports Isac begin |
7 |
7 |
8 ML{* writeln "**** run the test ***************************************" *} |
8 ML{* writeln "**** run the test ***************************************" *} |
9 |
9 |
10 use"../../../test/Tools/isac/Frontend/interface.sml" |
10 use"../../../test/Tools/isac/Frontend/interface.sml" |
11 |
11 |
12 ML{* |
12 ML{* |
13 |
13 |
14 |
14 |
15 "--------- rat-eq + subpbl: no_met, NO solution dropped -"; |
|
16 states:=[]; |
|
17 CalcTree |
|
18 [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"], |
|
19 ("RatEq", ["univariate","equation"], ["no_met"]))]; |
|
20 Iterator 1; |
|
21 moveActiveRoot 1; |
|
22 fetchProposedTactic 1; |
|
23 |
|
24 (*ERROR: setNextTactic 1 produces "get_calc 1 not existent"*) |
|
25 setNextTactic 1 (Model_Problem ); |
|
26 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
27 |
|
28 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----* |
|
29 setNextTactic 1 (Add_Given "equality (5 * x / (x - 2) - x / (x + 2) = 4)"); |
|
30 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
31 setNextTactic 1 (Add_Given "solveFor x"); |
|
32 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
33 setNextTactic 1 (Add_Find "solutions L"); |
|
34 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
35 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*) |
|
36 setNextTactic 1 (Specify_Theory "RatEq"); |
|
37 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
38 setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]); |
|
39 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
40 setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]); |
|
41 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
42 setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]); |
|
43 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
44 setNextTactic 1 (Rewrite_Set "RatEq_simplify"); |
|
45 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
46 setNextTactic 1 (Rewrite_Set "norm_Rational"); |
|
47 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
48 setNextTactic 1 (Rewrite_Set "RatEq_eliminate"); |
|
49 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
50 (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*) |
|
51 setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial", |
|
52 "univariate","equation"])); |
|
53 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
54 setNextTactic 1 (Model_Problem ); |
|
55 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
56 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----* |
|
57 setNextTactic 1 (Add_Given |
|
58 "equality (12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2))"); |
|
59 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
60 setNextTactic 1 (Add_Given "solveFor x"); |
|
61 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
62 setNextTactic 1 (Add_Find "solutions x_i"); |
|
63 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
64 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*) |
|
65 setNextTactic 1 (Specify_Theory "PolyEq"); |
|
66 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
67 setNextTactic 1 (Specify_Problem ["normalize","polynomial", |
|
68 "univariate","equation"]); |
|
69 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
70 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]); |
|
71 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
72 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]); |
|
73 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
74 setNextTactic 1 (Rewrite ("all_left","")); |
|
75 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
76 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in")); |
|
77 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
78 (* __________ for "16 + 12 * x = 0"*) |
|
79 setNextTactic 1 (Subproblem ("PolyEq", |
|
80 ["degree_1","polynomial","univariate","equation"])); |
|
81 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
82 setNextTactic 1 (Model_Problem ); |
|
83 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
84 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----* |
|
85 setNextTactic 1 (Add_Given |
|
86 "equality (16 + 12 * x = 0)"); |
|
87 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
88 setNextTactic 1 (Add_Given "solveFor x"); |
|
89 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
90 setNextTactic 1 (Add_Find "solutions x_i"); |
|
91 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
92 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*) |
|
93 setNextTactic 1 (Specify_Theory "PolyEq"); |
|
94 (*------------- some trials in the problem-hierarchy ---------------*) |
|
95 setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]); |
|
96 autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*) |
|
97 setNextTactic 1 (Refine_Problem ["univariate","equation"]); |
|
98 (*------------------------------------------------------------------*) |
|
99 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
100 setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]); |
|
101 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
102 setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]); |
|
103 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
104 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify")); |
|
105 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
106 setNextTactic 1 (Rewrite_Set "polyeq_simplify"); |
|
107 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
108 (*==================================================================*) |
|
109 setNextTactic 1 Or_to_List; |
|
110 autoCalculate 1 (Step 1); fetchProposedTactic 1; |
|
111 (* setNextTactic 1 (Check_elementwise "Assumptions"); |
|
112 WAS: exception Match raised (line 1218 of ".../script.sml")*) |
|
113 "~~~~~ fun setNextTactic, args:"; val ((cI:calcID), tac) = (1, (Check_elementwise "Assumptions")); |
|
114 val ((pt, _), _) = get_calc cI; |
|
115 val ip = get_pos cI 1; |
|
116 (*locatetac tac (pt, ip) WAS: exception Match raised (line 1218 of ".../script.sml")*) |
|
117 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip)); |
|
118 val (mI,m) = mk_tac'_ tac; |
|
119 val Appl m = applicable_in p pt m; |
|
120 member op = specsteps mI (*false*); |
|
121 (* loc_solve_ (mI,m) ptp WAS: exception Match raised (line 1218 of ".../script.sml")*) |
|
122 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp); |
|
123 (*solve m (pt, pos); WAS: exception Match raised (line 1218 of ".../script.sml")*) |
|
124 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos)); |
|
125 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*); |
|
126 val thy' = get_obj g_domID pt (par_pblobj pt p); |
|
127 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
|
128 val d = e_rls; |
|
129 *} |
15 *} |
130 ML{* |
16 ML{* |
131 (*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is; |
|
132 WAS: exception Match raised (line 1218 of "isabisac/src/Tools/isac/Interpret/script.sml"*) |
|
133 "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'), |
|
134 (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = |
|
135 ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *) |
|
136 val thy = assoc_thy thy'; |
|
137 |
|
138 *} |
|
139 ML{* |
|
140 *} |
|
141 ML{* |
|
142 (*case (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) |
|
143 of |
|
144 (Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_)))) |
|
145 => |
|
146 "nix";*) |
|
147 (*ERROR: |
|
148 Value identifier (c') has not been referenced. |
|
149 Value identifier (p') has not been referenced. |
|
150 Value identifier (pt') has not been referenced. |
|
151 Value identifier (f') has not been referenced. |
|
152 Value identifier (m') has not been referenced. |
|
153 Value identifier (ss) has not been referenced. |
|
154 Value identifier (bb) has not been referenced. |
|
155 Value identifier (is) has not been referenced. |
|
156 Value identifier (iss) has not been referenced. |
|
157 Matches are not exhaustive. |
|
158 exception Match raised*) |
|
159 *} |
|
160 ML{* |
|
161 (*case (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) |
|
162 of |
|
163 (Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_)))) |
|
164 => (iss,is,bb,ss,m',f',pt',p',c');*) |
|
165 (*ERROR: |
|
166 Matches are not exhaustive. |
|
167 exception Match raised*) |
|
168 *} |
|
169 ML{* |
|
170 *} |
|
171 ML{* |
|
172 *} |
|
173 ML{* |
|
174 (*========== inhibit exn 110719 ================================================ |
|
175 ========== inhibit exn 110719 XXX=============================================*) |
|
176 |
|
177 |
|
178 *} |
|
179 ML{* |
|
180 |
|
181 *} |
17 *} |
182 ML{* |
18 ML{* |
183 *} |
19 *} |
184 ML{* |
20 ML{* |
185 *} |
21 *} |