132 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
132 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
133 |
133 |
134 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
134 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
135 val Form' (FormKF (_,EdUndef,0,Nundef,res)) = f; |
135 val Form' (FormKF (_,EdUndef,0,Nundef,res)) = f; |
136 if (snd nxt)=End_Proof' andalso res="[x = 1]" then () |
136 if (snd nxt)=End_Proof' andalso res="[x = 1]" then () |
137 else raise error "subp-rooteq.sml: new.behav. in miniscript with mini-subpbl"; |
137 else error "subp-rooteq.sml: new.behav. in miniscript with mini-subpbl"; |
138 |
138 |
139 |
139 |
140 "---------------- solve_linear as rootpbl -----------------"; |
140 "---------------- solve_linear as rootpbl -----------------"; |
141 "---------------- solve_linear as rootpbl -----------------"; |
141 "---------------- solve_linear as rootpbl -----------------"; |
142 "---------------- solve_linear as rootpbl -----------------"; |
142 "---------------- solve_linear as rootpbl -----------------"; |
175 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
175 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
176 (*val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #1]")) : mout |
176 (*val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #1]")) : mout |
177 val nxt = ("End_Proof'",End_Proof') : string * tac*) |
177 val nxt = ("End_Proof'",End_Proof') : string * tac*) |
178 val Form' (FormKF (_,EdUndef,0,Nundef,res)) = f; |
178 val Form' (FormKF (_,EdUndef,0,Nundef,res)) = f; |
179 if (snd nxt)=End_Proof' andalso res="[x = 1]" then () |
179 if (snd nxt)=End_Proof' andalso res="[x = 1]" then () |
180 else raise error "subp-rooteq.sml: new.behav. in solve_linear as rootpbl"; |
180 else error "subp-rooteq.sml: new.behav. in solve_linear as rootpbl"; |
181 |
181 |
182 |
182 |
183 "---------------- solve_plain_square as rootpbl -----------"; |
183 "---------------- solve_plain_square as rootpbl -----------"; |
184 "---------------- solve_plain_square as rootpbl -----------"; |
184 "---------------- solve_plain_square as rootpbl -----------"; |
185 "---------------- solve_plain_square as rootpbl -----------"; |
185 "---------------- solve_plain_square as rootpbl -----------"; |
208 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
208 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
209 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
209 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
210 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
210 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
211 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; |
211 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; |
212 if snd nxt=End_Proof' andalso res="[x = -3, x = 3]" then () |
212 if snd nxt=End_Proof' andalso res="[x = -3, x = 3]" then () |
213 else raise error "subp-rooteq.sml: new.behav. in solve_plain_square as rootpbl"; |
213 else error "subp-rooteq.sml: new.behav. in solve_plain_square as rootpbl"; |
214 |
214 |
215 |
215 |
216 |
216 |
217 |
217 |
218 "---------------- root-eq + subpbl: solve_linear ----------"; |
218 "---------------- root-eq + subpbl: solve_linear ----------"; |
281 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
281 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
282 (*"[]", nxt Check_Postcond ["sqroot-test","univariate","equation","test"]*) |
282 (*"[]", nxt Check_Postcond ["sqroot-test","univariate","equation","test"]*) |
283 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
283 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
284 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; |
284 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; |
285 if (snd nxt)=End_Proof' andalso res="[x = 4]" then () |
285 if (snd nxt)=End_Proof' andalso res="[x = 4]" then () |
286 else raise error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_linear"; |
286 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_linear"; |
287 |
287 |
288 |
288 |
289 |
289 |
290 "---------------- root-eq + subpbl: solve_plain_square ----"; |
290 "---------------- root-eq + subpbl: solve_plain_square ----"; |
291 "---------------- root-eq + subpbl: solve_plain_square ----"; |
291 "---------------- root-eq + subpbl: solve_plain_square ----"; |
355 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
355 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
356 (*"[]", nxt Check_Postcond ["sqroot-test","univariate","equation","test"]*) |
356 (*"[]", nxt Check_Postcond ["sqroot-test","univariate","equation","test"]*) |
357 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
357 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
358 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; |
358 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; |
359 if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then () |
359 if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then () |
360 else raise error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_plain_square"; |
360 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_plain_square"; |
361 |
361 |
362 |
362 |
363 writeln (pr_ptree pr_short pt); |
363 writeln (pr_ptree pr_short pt); |
364 |
364 |
365 |
365 |
418 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
418 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
419 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
419 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
420 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
420 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
421 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
421 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
422 if p = ([13],Res) then () |
422 if p = ([13],Res) then () |
423 else raise error ("subp-rooteq.sml: new.behav. in \ |
423 else error ("subp-rooteq.sml: new.behav. in \ |
424 \root-eq + subpbl: solve_linear, p ="^(pos'2str p)); |
424 \root-eq + subpbl: solve_linear, p ="^(pos'2str p)); |
425 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
425 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
426 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; |
426 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; |
427 if (snd nxt)=End_Proof' andalso res="[x = 4]" then () |
427 if (snd nxt)=End_Proof' andalso res="[x = 4]" then () |
428 else raise error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_plain_square"; |
428 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_plain_square"; |
429 |
429 |
430 |
430 |
431 |
431 |
432 |
432 |
433 "---------------- root-eq + subpbl: no_met: square ----"; |
433 "---------------- root-eq + subpbl: no_met: square ----"; |
483 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
483 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
484 (*val nxt = ("Check_Postcond",Check_Postcond ["squareroot","univariate","equ*) |
484 (*val nxt = ("Check_Postcond",Check_Postcond ["squareroot","univariate","equ*) |
485 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
485 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
486 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; |
486 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; |
487 if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then () |
487 if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then () |
488 else raise error "subp-rooteq.sml: new.behav. in root-eq + subpbl: no_met: square"; |
488 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: no_met: square"; |
489 |
489 |
490 |
490 |
491 |
491 |
492 "---------------- no_met in rootpbl -> linear --------------"; |
492 "---------------- no_met in rootpbl -> linear --------------"; |
493 "---------------- no_met in rootpbl -> linear --------------"; |
493 "---------------- no_met in rootpbl -> linear --------------"; |
531 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
531 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
532 (*val nxt = ("Check_Postcond",Check_Postcond ["normalize","univariate","equa*) |
532 (*val nxt = ("Check_Postcond",Check_Postcond ["normalize","univariate","equa*) |
533 val (p,_,Form' (FormKF (_,_,_,_,f)),nxt,_,_) = |
533 val (p,_,Form' (FormKF (_,_,_,_,f)),nxt,_,_) = |
534 me nxt p c pt; |
534 me nxt p c pt; |
535 if f="[x = 5]" andalso nxt=("End_Proof'",End_Proof') then () |
535 if f="[x = 5]" andalso nxt=("End_Proof'",End_Proof') then () |
536 else raise error "subp-rooteq.sml: new.behav. in no_met in rootpbl -> linear ---"; |
536 else error "subp-rooteq.sml: new.behav. in no_met in rootpbl -> linear ---"; |
537 |
537 |
538 |
538 |
539 refine fmz ["univariate","equation","test"]; |
539 refine fmz ["univariate","equation","test"]; |
540 match_pbl fmz (get_pbt ["polynomial","univariate","equation","test"]); |
540 match_pbl fmz (get_pbt ["polynomial","univariate","equation","test"]); |
541 |
541 |