wneuper@59569
|
1 |
(* Title: "Minisubpbl/250-Rewrite_Set-from-method.sml"
|
wneuper@59569
|
2 |
Author: Walther Neuper 1105
|
wneuper@59411
|
3 |
(c) copyright due to lincense terms.
|
wneuper@59411
|
4 |
*)
|
Walther@60598
|
5 |
open Istate;
|
Walther@60598
|
6 |
open LI;
|
wneuper@59411
|
7 |
|
wneuper@59564
|
8 |
"----------- Minisubpbl/250-Rewrite_Set-from-method.sml ----------";
|
wneuper@59564
|
9 |
"----------- Minisubpbl/250-Rewrite_Set-from-method.sml ----------";
|
wneuper@59564
|
10 |
"----------- Minisubpbl/250-Rewrite_Set-from-method.sml ----------";
|
walther@59997
|
11 |
val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
|
wneuper@59411
|
12 |
val (dI',pI',mI') =
|
walther@59997
|
13 |
("Test", ["sqroot-test", "univariate", "equation", "test"],
|
walther@59997
|
14 |
["Test", "squ-equ-test-subpbl1"]);
|
Walther@60571
|
15 |
val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
|
wneuper@59411
|
16 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
wneuper@59411
|
17 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
wneuper@59411
|
18 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
wneuper@59411
|
19 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
wneuper@59411
|
20 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
wneuper@59411
|
21 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
Walther@60725
|
22 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Apply_Method ["Test", "squ-equ-test-subpbl1"] = nxt;
|
Walther@60725
|
23 |
(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Rewrite_Set "norm_equation" = nxt;
|
wneuper@59411
|
24 |
|
Walther@60725
|
25 |
(*[1], Res*)val return_me_Rewrite_Set_norm_equation = me nxt p [] pt;
|
Walther@60598
|
26 |
(*//------------------ step into Rewrite_Set "norm_equation" -------------------------------\\*)
|
Walther@60725
|
27 |
"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
|
walther@59806
|
28 |
val ("ok", (_, _, ptp''''')) = (*case*)
|
walther@59806
|
29 |
Step.by_tactic tac (pt, p) (*of*);
|
walther@59806
|
30 |
"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
|
walther@59921
|
31 |
val Applicable.Yes m = (*case*) Step.check tac (pt, p) (*of*);
|
walther@59755
|
32 |
(*if*) Tactic.for_specify' m; (*false*)
|
wneuper@59482
|
33 |
|
walther@59806
|
34 |
Step_Solve.by_tactic m ptp;
|
walther@59921
|
35 |
"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
|
walther@60154
|
36 |
(*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (* = else*);
|
wneuper@59482
|
37 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
Walther@60559
|
38 |
val (is, sc) = LItool.resume_prog (p,p_) pt;
|
wneuper@59482
|
39 |
|
walther@59851
|
40 |
val Safe_Step (_, _, Rewrite_Set' (_, _, Rule_Set.Repeat {id = "norm_equation", ...}, _, _)) = (*case*)
|
Walther@60598
|
41 |
locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
|
walther@59692
|
42 |
"~~~~~ fun locate_input_tactic , args:"; val (Rule.Prog progr, cstate, istate, ctxt, tac)
|
wneuper@59569
|
43 |
= (sc, (pt, po), (fst is), (snd is), m);
|
Walther@60598
|
44 |
val prog_rls = LItool.get_simplifier cstate;
|
wneuper@59569
|
45 |
|
Walther@60598
|
46 |
(*case*) scan_to_tactic1 (progr, (cstate, ctxt, tac)) istate (*of*);
|
Walther@60598
|
47 |
"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Pstate (ist as {path, ...})))
|
walther@59686
|
48 |
= ((progr, (cstate, ctxt, tac)), istate);
|
walther@59686
|
49 |
(*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
|
wneuper@59482
|
50 |
|
walther@59718
|
51 |
scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
|
wenzelm@60309
|
52 |
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
|
walther@59718
|
53 |
= (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
|
wneuper@59482
|
54 |
|
walther@59851
|
55 |
val Accept_Tac1 (_, _, Rewrite_Set' (_, _, Rule_Set.Repeat {id = "norm_equation", ...}, _, _)) = (*case*)
|
walther@59691
|
56 |
scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
|
walther@60336
|
57 |
"~~~~~ fun scan_dn1, args:"; val ((xxx as (cstate, _, _)), ist, (Const (\<^const_name>\<open>Chain\<close>(*1*),_) $e1 $ e2 $ a)) =
|
walther@59684
|
58 |
(xxx, (ist |> path_down [L, R]), e);
|
wneuper@59482
|
59 |
|
walther@59718
|
60 |
val Accept_Tac1 _ = (*case*)
|
walther@59691
|
61 |
scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
|
walther@60336
|
62 |
"~~~~~ fun scan_dn1, args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*1*),_) $ e)) =
|
walther@59684
|
63 |
(xxx, (ist |> path_down_form ([L, L, R], a)), e1);
|
wneuper@59482
|
64 |
|
Walther@60675
|
65 |
(*+*)UnparseC.term ctxt e1 = "Try (Rewrite_Set ''norm_equation'')" (*in isabisac*);
|
wneuper@59482
|
66 |
|
walther@59718
|
67 |
val Accept_Tac1 _ = (*case*)
|
Walther@60598
|
68 |
scan_dn1 xxx (ist |> path_down_form ([L, R], a)) e (*of*);
|
walther@59684
|
69 |
(*======= end of scanning tacticals, a leaf =======*)
|
walther@59722
|
70 |
"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) =
|
walther@59684
|
71 |
(xxx, (ist |> path_down_form ([L, R], a)), e);
|
Walther@60598
|
72 |
val (Program.Tac stac, a') = (*case*) LItool.check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
|
Walther@60598
|
73 |
val LItool.Associated (Rewrite_Set' _, _, _) = (*case*)
|
Walther@60609
|
74 |
LItool.associate (pt, p) ctxt (m, stac) (*of*);
|
wneuper@59578
|
75 |
"~~~~~ fun associate, args:"; val (_, ctxt, (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _))),
|
walther@60336
|
76 |
(Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ rls_ $ f_)) = (pt, ctxt, m, stac);
|
wneuper@59482
|
77 |
|
walther@59867
|
78 |
(*+*)if Rule_Set.id rls = HOLogic.dest_string rls_ then () else error "Prog_Tac.associate changed";
|
wneuper@59482
|
79 |
|
walther@59804
|
80 |
"~~~~~ continue me[1] after Step.by_tactic";
|
wneuper@59482
|
81 |
val (pt, p) = ptp''''';
|
walther@59765
|
82 |
(* isabisac17: val ("helpless", _) = (*case*) Step.do_next p ((pt, Pos.e_pos'),[]) (*of*)*)
|
wneuper@59411
|
83 |
"~~~~~ fun step, args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[]));
|
wneuper@59411
|
84 |
val pIopt = get_pblID (pt,ip);
|
walther@59694
|
85 |
(*if*) ip = ([], Pos.Res) = false;
|
wneuper@59411
|
86 |
val _ = (*case*) tacis (*of*);
|
wneuper@59411
|
87 |
(*if*) ip = p = false;
|
walther@60017
|
88 |
(*if*) member op = [Pbl, Met] p_ = false;
|
wneuper@59411
|
89 |
|
walther@59760
|
90 |
"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
|
walther@60154
|
91 |
MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;
|
walther@60154
|
92 |
(*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p)(*else*);
|
wneuper@59411
|
93 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
Walther@60559
|
94 |
val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
|
wneuper@59411
|
95 |
|
walther@59734
|
96 |
val Next_Step (_, _, _) =
|
Walther@60598
|
97 |
(*case*) find_next_step sc (pt, pos) ist ctxt (*of*);
|
walther@59772
|
98 |
"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
|
walther@59723
|
99 |
= (sc, (pt, pos), ist, ctxt);
|
wneuper@59411
|
100 |
|
walther@59770
|
101 |
val Accept_Tac (Rewrite_Set' _, _, _) = (*case*)
|
Walther@60598
|
102 |
scan_to_tactic (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
|
walther@59769
|
103 |
"~~~~~ fun scan_to_tactic , args:"; val ((prog, cct), (Istate.Pstate (ist as {path, ...})))
|
walther@59699
|
104 |
= ((prog, (ptp, ctxt)), (Istate.Pstate ist));
|
walther@59686
|
105 |
(*if*) 0 = length path (*else*);
|
wneuper@59411
|
106 |
|
walther@59770
|
107 |
val Accept_Tac (Rewrite_Set' _, _, _) =
|
walther@59785
|
108 |
go_scan_up (prog, cct) (trans_scan_up ist |> set_found);
|
walther@59784
|
109 |
"~~~~~ and go_scan_up , args:"; val ((yyy as (prog, _)), (ist as {env, path, found_accept, ...})) =
|
walther@59785
|
110 |
((prog, cct), (trans_scan_up ist |> set_found));
|
walther@59686
|
111 |
(*if*) 1 < length path (*then*);
|
wneuper@59411
|
112 |
|
Walther@60679
|
113 |
scan_up yyy (ist |> path_up) (go_up ctxt path prog);
|
walther@60336
|
114 |
"~~~~~ fun scan_up , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ _)) =
|
Walther@60679
|
115 |
(yyy, (ist |> path_up), (go_up ctxt path prog));
|
Walther@60598
|
116 |
(*\\------------------ step into Rewrite_Set "norm_equation" -------------------------------//*)
|
Walther@60725
|
117 |
val (p,_,f,nxt,_,pt) = return_me_Rewrite_Set_norm_equation; val Rewrite_Set "Test_simplify" = nxt;
|
Walther@60598
|
118 |
|
Walther@60725
|
119 |
(*[2], Res*)val return_Rewrite_Set_Test_simplify = me nxt p [] pt;
|
Walther@60598
|
120 |
(*//------------------ step into Rewrite_Set "Test_simplify" -------------------------------\\*)
|
walther@59921
|
121 |
(*+*)val p'''''_'' = p; (* keep for final test*)
|
Walther@60725
|
122 |
"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
|
wneuper@59582
|
123 |
val (pt, p) =
|
walther@59804
|
124 |
(*Step.by_tactic is here for testing by me; step would suffice in me*)
|
walther@59804
|
125 |
case Step.by_tactic tac (pt, p) of
|
wneuper@59582
|
126 |
("ok", (_, _, ptp)) => ptp
|
wneuper@59582
|
127 |
| ("unsafe-ok", (_, _, ptp)) => ptp
|
wneuper@59582
|
128 |
| ("not-applicable",_) => (pt, p)
|
wneuper@59582
|
129 |
| ("end-of-calculation", (_, _, ptp)) => ptp
|
wneuper@59582
|
130 |
| ("failure", _) => error "sys-error"
|
wneuper@59582
|
131 |
| _ => error "me: uncovered case"
|
wneuper@59582
|
132 |
|
walther@59765
|
133 |
(*case*) Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
|
wneuper@59582
|
134 |
"~~~~~ fun step , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis))
|
walther@59694
|
135 |
= (p, ((pt, Pos.e_pos'), []));
|
wneuper@59582
|
136 |
val pIopt = get_pblID (pt,ip);
|
walther@59694
|
137 |
(*if*) ip = ([], Pos.Res) (*else*);
|
wneuper@59582
|
138 |
val _ = (*case*) tacis (*of*);
|
wneuper@59582
|
139 |
val SOME _ = (*case*) pIopt (*of*);
|
walther@60017
|
140 |
(*if*) member op = [Pos.Pbl, Pos.Met] p_ (**else*);
|
wneuper@59582
|
141 |
|
walther@59760
|
142 |
Step_Solve.do_next (pt, ip);
|
walther@59760
|
143 |
"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
|
walther@60154
|
144 |
(*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
|
wneuper@59582
|
145 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
Walther@60559
|
146 |
val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
|
wneuper@59582
|
147 |
|
walther@59734
|
148 |
val Next_Step (_, _, _) =
|
walther@59791
|
149 |
(*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
|
walther@59772
|
150 |
"~~~~~ fun find_next_step , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
|
walther@59723
|
151 |
= (sc, (pt, pos), ist, ctxt);
|
Walther@60598
|
152 |
(** )val Accept_Tac (_, _, _) = ( *case*)
|
walther@59769
|
153 |
scan_to_tactic (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
|
walther@59921
|
154 |
"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Istate.Pstate (ist as {path, ...})))
|
walther@59699
|
155 |
= ((prog, (ptp, ctxt)), (Istate.Pstate ist));
|
walther@59686
|
156 |
(*if*) 0 = length path (*else*);
|
wneuper@59582
|
157 |
|
walther@59785
|
158 |
go_scan_up (prog, cc) (trans_scan_up ist |> set_found);
|
walther@59784
|
159 |
"~~~~~ fun go_scan_up , args:"; val ((yyy as (prog, _)), (ist as {env, path, found_accept, ...}))
|
walther@59785
|
160 |
= ((prog, cct), (trans_scan_up ist |> set_found));
|
walther@59686
|
161 |
(*if*) 1 < length path (*then*);
|
wneuper@59582
|
162 |
|
Walther@60679
|
163 |
scan_up yyy (ist |> path_up) (go_up ctxt path prog);
|
walther@60336
|
164 |
"~~~~~ and scan_up , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Try\<close>(*1*),_) $ _ ))
|
Walther@60679
|
165 |
= (yyy, (ist |> path_up), (go_up ctxt path prog));
|
wneuper@59582
|
166 |
|
walther@59785
|
167 |
go_scan_up yyy (ist |> set_found);
|
walther@59784
|
168 |
"~~~~~ fun go_scan_up , args:"; val ((yyy as (prog, _)), (ist as {env, path, found_accept, ...}))
|
walther@59785
|
169 |
= (yyy, (ist |> set_found));
|
walther@59686
|
170 |
(*if*) 1 < length path (*then*);
|
wneuper@59582
|
171 |
|
Walther@60679
|
172 |
scan_up yyy (ist |> path_up) (go_up ctxt path prog);
|
walther@60336
|
173 |
"~~~~~ and scan_up , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ _ $ _))
|
Walther@60679
|
174 |
= (yyy, (ist |> path_up), (go_up ctxt path prog));
|
wneuper@59582
|
175 |
|
walther@59769
|
176 |
go_scan_up yyy ist;
|
walther@59784
|
177 |
"~~~~~ and go_scan_up , args:"; val ((yyy as (prog, _)), (ist as {env, path, found_accept, ...}))
|
walther@59686
|
178 |
= (yyy, ist);
|
walther@59686
|
179 |
(*if*) 1 < length path (*then*);
|
wneuper@59582
|
180 |
|
Walther@60679
|
181 |
scan_up yyy (ist |> path_up) (go_up ctxt path prog);
|
walther@60336
|
182 |
"~~~~~ fun scan_up , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Chain\<close>(*1*), _) $ _ $ _ $ _))
|
Walther@60679
|
183 |
= (yyy, (ist |> path_up), (go_up ctxt path prog));
|
wneuper@59582
|
184 |
|
walther@59769
|
185 |
go_scan_up yyy ist;
|
walther@59784
|
186 |
"~~~~~ and go_scan_up , args:"; val ((yyy as (prog, _)), (ist as {env, path, found_accept, ...}))
|
walther@59686
|
187 |
= (yyy, ist);
|
walther@59686
|
188 |
(*if*) 1 < length path (*then*);
|
wneuper@59582
|
189 |
|
Walther@60679
|
190 |
scan_up yyy (ist |> path_up) (go_up ctxt path prog);
|
wenzelm@60309
|
191 |
"~~~~~ fun scan_up , args:"; val ((yyy as (prog, xxx)), (ist as {found_accept, ...}), (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _))
|
Walther@60679
|
192 |
= (yyy, (ist |> path_up), (go_up ctxt path prog));
|
walther@59784
|
193 |
(*if* ) found_accept = Napp_ ( *else*);
|
Walther@60725
|
194 |
|
Walther@60725
|
195 |
(*//------------------ revive with CS: push through ctxt to Tactic.Subproblem --------------\\* )
|
walther@59723
|
196 |
val (i, body) = check_Let_up ist prog;
|
wneuper@59582
|
197 |
|
walther@59769
|
198 |
(*case*) scan_dn xxx (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
|
Walther@60725
|
199 |
"~~~~~ fun scan_dn , args:"; val (xxx, ist, (Const (\ <^ const_name>\<open>Let\<close>(*1*),_) $ e $ (Abs (i,T,b))))
|
walther@59698
|
200 |
= (xxx, (ist |> path_up_down [R, D] |> upd_env i), body);
|
wneuper@59582
|
201 |
|
Walther@60598
|
202 |
(** )val Accept_Tac (Subproblem' _, _, _) = ( *case*)
|
walther@59769
|
203 |
scan_dn xxx (ist |> path_down [L, R]) e (*of*);
|
walther@59684
|
204 |
(*========== a leaf has been found ==========*)
|
walther@59769
|
205 |
"~~~~~ fun scan_dn , args:"; val (((pt, p), ctxt), (ist as {eval, ...}), t)
|
walther@59684
|
206 |
= (xxx, (ist |> path_down [L, R]), e);
|
walther@59790
|
207 |
val (Program.Tac stac, a') = (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
|
walther@59672
|
208 |
|
walther@59825
|
209 |
(*val m =*)
|
Walther@60725
|
210 |
Sub_Problem.tac_from_prog (pt, pos) stac;
|
Walther@60725
|
211 |
"~~~~~ fun tac_from_prog , args:"; val (pt, _, (stac as Const (\ <^const_name>\<open>SubProblem\<close>, _) $ spec' $ ags'))
|
walther@59722
|
212 |
= (pt, (Proof_Context.theory_of ctxt), stac);
|
walther@59618
|
213 |
val (dI, pI, mI) = Prog_Tac.dest_spec spec'
|
Walther@60609
|
214 |
val thy = Sub_Problem.common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt);
|
Walther@60609
|
215 |
val init_ctxt = Proof_Context.init_global thy
|
wneuper@59582
|
216 |
val ags = TermC.isalist2list ags';
|
wneuper@59582
|
217 |
val (pI, pors, mI) =
|
Walther@60609
|
218 |
if mI = ["no_met"]
|
Walther@60609
|
219 |
then
|
Walther@60609
|
220 |
let
|
Walther@60609
|
221 |
val pors = (M_Match.arguments thy ((#model o (Problem.from_store init_ctxt)) pI) ags): O_Model.T
|
Walther@60609
|
222 |
handle ERROR "actual args do not match formal args"
|
Walther@60609
|
223 |
=> (M_Match.arguments_msg init_ctxt pI stac ags (*raise exn*);[]);
|
Walther@60742
|
224 |
val pI' = Refine.by_o_model' init_ctxt pors pI;
|
Walther@60609
|
225 |
in (pI', pors (* refinement over models with diff.prec only *),
|
Walther@60609
|
226 |
(hd o #solve_mets o Problem.from_store init_ctxt) pI') end
|
Walther@60609
|
227 |
else (pI, (M_Match.arguments thy ((#model o Problem.from_store init_ctxt) pI) ags)
|
Walther@60609
|
228 |
handle ERROR "actual args do not match formal args"
|
Walther@60609
|
229 |
=> (M_Match.arguments_msg init_ctxt pI stac ags(*raise exn*); []), mI);
|
Walther@60609
|
230 |
val (fmz_, vals) = O_Model.values' init_ctxt pors;
|
Walther@60609
|
231 |
val {cas, model, thy, ...} = Problem.from_store init_ctxt pI
|
Walther@60609
|
232 |
val dI = Context.theory_name thy (*take dI from _refined_ pbl*)
|
Walther@60609
|
233 |
val dI = Context.theory_name
|
Walther@60609
|
234 |
(Sub_Problem.common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt))
|
Walther@60654
|
235 |
val ctxt = ContextC.init_for_prog init_ctxt vals
|
Walther@60725
|
236 |
( *\\------------------ revive with CS: push through ctxt to Tactic.Subproblem --------------//*)
|
Walther@60725
|
237 |
(*\\------------------ step into Rewrite_Set "Test_simplify" -------------------------------//*)
|
Walther@60725
|
238 |
val (p,_,f,nxt,_,pt) = return_Rewrite_Set_Test_simplify; val Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]) = nxt;
|
Walther@60598
|
239 |
|
Walther@60598
|
240 |
(* final test ... ----------------------------------------------------------------------------*)
|
Walther@60725
|
241 |
if pos = ([2], Res) andalso f2str f = "- 1 + x = 0" then
|
wneuper@59582
|
242 |
case nxt of
|
walther@59749
|
243 |
(Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])) => ()
|
wneuper@59582
|
244 |
| _ => error "Minisubpbl/250-Rewrite_Set-from-method changed 1"
|
wneuper@59582
|
245 |
else error "Minisubpbl/250-Rewrite_Set-from-method changed 2";
|