43 print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3; |
43 print_depth 99;map fst (get_interval ([],Pbl) ([],Res) 9999 pt);print_depth 3; |
44 if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) = |
44 if map fst (get_interval ([],Pbl) ([],Res) 9999 pt) = |
45 [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), |
45 [([], Pbl), ([1], Frm),([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), |
46 ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), |
46 ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), |
47 ([3, 2], Res)] then () else |
47 ([3, 2], Res)] then () else |
48 raise error "calchead.sml: diff.behav. get_interval after replace} other 2 a"; |
48 error "calchead.sml: diff.behav. get_interval after replace} other 2 a"; |
49 |
49 |
50 print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); |
50 print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); |
51 print_depth 3; |
51 print_depth 3; |
52 if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) = |
52 if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) = |
53 [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else |
53 [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else |
54 raise error "modspec.sml: diff.behav. get_interval after replace} other 2 b"; |
54 error "modspec.sml: diff.behav. get_interval after replace} other 2 b"; |
55 |
55 |
56 |
56 |
57 |
57 |
58 |
58 |
59 "--------- maximum example with 'specify' ------------------------"; |
59 "--------- maximum example with 'specify' ------------------------"; |
96 |
96 |
97 if ppc<>(Problem [], |
97 if ppc<>(Problem [], |
98 {Find=[Incompl "maximum",Incompl "valuesFor [a]"], |
98 {Find=[Incompl "maximum",Incompl "valuesFor [a]"], |
99 Given=[Correct "fixedValues [r = Arbfix]"], |
99 Given=[Correct "fixedValues [r = Arbfix]"], |
100 Relate=[Incompl "relations []"], Where=[],With=[]}) |
100 Relate=[Incompl "relations []"], Where=[],With=[]}) |
101 then raise error "test-maximum.sml: model stepwise - different behaviour" |
101 then error "test-maximum.sml: model stepwise - different behaviour" |
102 else (); (*different with show_types !!!*) |
102 else (); (*different with show_types !!!*) |
103 6.5.03---*) |
103 6.5.03---*) |
104 |
104 |
105 (*-----appl_add should not create Error', but accept as Sup,Syn |
105 (*-----appl_add should not create Error', but accept as Sup,Syn |
106 val nxt = tac2tac_ pt p (Add_Given "boundVariable a"); |
106 val nxt = tac2tac_ pt p (Add_Given "boundVariable a"); |
117 |
117 |
118 if ppc<>(Problem ["maximum_of","function"], |
118 if ppc<>(Problem ["maximum_of","function"], |
119 {Find=[Incompl "maximum",Incompl "valuesFor"], |
119 {Find=[Incompl "maximum",Incompl "valuesFor"], |
120 Given=[Correct "fixedValues [r = Arbfix]"], |
120 Given=[Correct "fixedValues [r = Arbfix]"], |
121 Relate=[Incompl "relations []"], Where=[],With=[]}) |
121 Relate=[Incompl "relations []"], Where=[],With=[]}) |
122 then raise error "diffappl.sml: Specify_Problem different behaviour" |
122 then error "diffappl.sml: Specify_Problem different behaviour" |
123 else (); |
123 else (); |
124 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly |
124 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly |
125 if ppc<>(Problem ["maximum_of","function"], |
125 if ppc<>(Problem ["maximum_of","function"], |
126 {Find=[Missing "maximum m_",Missing "valuesFor vs_"], |
126 {Find=[Missing "maximum m_",Missing "valuesFor vs_"], |
127 Given=[Correct "fixedValues [r = Arbfix]"], |
127 Given=[Correct "fixedValues [r = Arbfix]"], |
128 Relate=[Missing "relations rs_"],Where=[],With=[]}) |
128 Relate=[Missing "relations rs_"],Where=[],With=[]}) |
129 then raise error "diffappl.sml: Specify_Problem different behaviour" |
129 then error "diffappl.sml: Specify_Problem different behaviour" |
130 else ();*) |
130 else ();*) |
131 |
131 |
132 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]); |
132 val nxt = tac2tac_ pt p(Specify_Method ["DiffApp","max_by_calculus"]); |
133 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; |
133 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; |
134 (**) |
134 (**) |
136 if ppc<>(Method ["DiffApp","max_by_calculus"], |
136 if ppc<>(Method ["DiffApp","max_by_calculus"], |
137 {Find=[Incompl "maximum",Incompl "valuesFor"], |
137 {Find=[Incompl "maximum",Incompl "valuesFor"], |
138 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v", |
138 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v", |
139 Missing "interval itv_",Missing "errorBound err_"], |
139 Missing "interval itv_",Missing "errorBound err_"], |
140 Relate=[Incompl "relations []"],Where=[],With=[]}) |
140 Relate=[Incompl "relations []"],Where=[],With=[]}) |
141 then raise error "diffappl.sml: Specify_Method different behaviour" |
141 then error "diffappl.sml: Specify_Method different behaviour" |
142 else (); |
142 else (); |
143 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly |
143 (* WN.3.9.03 (#391) Model_Specify did init_pbl newly |
144 if ppc<>(Method ["DiffApp","max_by_calculus"], |
144 if ppc<>(Method ["DiffApp","max_by_calculus"], |
145 {Find=[Missing "maximum m_",Missing "valuesFor vs_"], |
145 {Find=[Missing "maximum m_",Missing "valuesFor vs_"], |
146 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v", |
146 Given=[Correct "fixedValues [r = Arbfix]",Missing "boundVariable v_v", |
147 Missing "interval itv_",Missing "errorBound err_"], |
147 Missing "interval itv_",Missing "errorBound err_"], |
148 Relate=[Missing "relations rs_"],Where=[],With=[]}) |
148 Relate=[Missing "relations rs_"],Where=[],With=[]}) |
149 then raise error "diffappl.sml: Specify_Method different behaviour" |
149 then error "diffappl.sml: Specify_Method different behaviour" |
150 else ();*) |
150 else ();*) |
151 |
151 |
152 |
152 |
153 |
153 |
154 "--------- maximum example with 'specify', fmz <> [] -------------"; |
154 "--------- maximum example with 'specify', fmz <> [] -------------"; |
202 (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!! |
202 (*---------------------------- FIXXXXME.meNEW !!! partial Add-Relation !!! |
203 nxt_specif <> specify ?! |
203 nxt_specif <> specify ?! |
204 |
204 |
205 if nxt<>(Add_Relation |
205 if nxt<>(Add_Relation |
206 "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]") |
206 "relations [(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]") |
207 then raise error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*) |
207 then error "test specify, fmz <> []: nxt <> Add_Relation (a/2)^2.." else (); (*different with show_types !!!*) |
208 |
208 |
209 val nxt = tac2tac_ pt p nxt; |
209 val nxt = tac2tac_ pt p nxt; |
210 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; |
210 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; |
211 ------------------------------ FIXXXXME.meNEW !!! ---*) |
211 ------------------------------ FIXXXXME.meNEW !!! ---*) |
212 |
212 |
236 |
236 |
237 val nxt = tac2tac_ pt p nxt; |
237 val nxt = tac2tac_ pt p nxt; |
238 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; |
238 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; |
239 (*val nxt = Apply_Method ("DiffApp.thy","max_by_calculus") *) |
239 (*val nxt = Apply_Method ("DiffApp.thy","max_by_calculus") *) |
240 if nxt<>(Apply_Method ["DiffApp","max_by_calculus"]) |
240 if nxt<>(Apply_Method ["DiffApp","max_by_calculus"]) |
241 then raise error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else (); |
241 then error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else (); |
242 |
242 |
243 |
243 |
244 "--------- maximum example with 'specify', fmz = [] --------------"; |
244 "--------- maximum example with 'specify', fmz = [] --------------"; |
245 "--------- maximum example with 'specify', fmz = [] --------------"; |
245 "--------- maximum example with 'specify', fmz = [] --------------"; |
246 "--------- maximum example with 'specify', fmz = [] --------------"; |
246 "--------- maximum example with 'specify', fmz = [] --------------"; |
284 (*val nxt = Add_Relation "relations" --- |
284 (*val nxt = Add_Relation "relations" --- |
285 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*) |
285 --- [b=Arbfix] KANN NICHT VERLANGT WERDEN !!!!*) |
286 |
286 |
287 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env .... |
287 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env .... |
288 if nxt<>(Add_Relation "relations []") |
288 if nxt<>(Add_Relation "relations []") |
289 then raise error "test specify, fmz <> []: nxt <> Add_Relation.." |
289 then error "test specify, fmz <> []: nxt <> Add_Relation.." |
290 else (); (*different with show_types !!!*) |
290 else (); (*different with show_types !!!*) |
291 *) |
291 *) |
292 |
292 |
293 val nxt = Add_Relation "relations [(A=a+b)]"; |
293 val nxt = Add_Relation "relations [(A=a+b)]"; |
294 val nxt = tac2tac_ pt p nxt; |
294 val nxt = tac2tac_ pt p nxt; |
314 val nxt = tac2tac_ pt p nxt; |
314 val nxt = tac2tac_ pt p nxt; |
315 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; |
315 val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; |
316 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *) |
316 (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *) |
317 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env .... |
317 (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env .... |
318 if nxt<>(Apply_Method ("DiffApp.thy","max_by_calculus")) |
318 if nxt<>(Apply_Method ("DiffApp.thy","max_by_calculus")) |
319 then raise error "test specify, fmz <> []: nxt <> Add_Relation.." |
319 then error "test specify, fmz <> []: nxt <> Add_Relation.." |
320 else (); |
320 else (); |
321 *) |
321 *) |
322 |
322 |
323 (* 2.4.00 nach Transfer specify -> hard_gen |
323 (* 2.4.00 nach Transfer specify -> hard_gen |
324 val nxt = Apply_Method ("DiffApp.thy","max_by_calculus"); |
324 val nxt = Apply_Method ("DiffApp.thy","max_by_calculus"); |
350 [(1, [1], "#Given", Const ("Descript.equalities", _), _), |
350 [(1, [1], "#Given", Const ("Descript.equalities", _), _), |
351 (2, [1], "#Given", Const ("EqSystem.solveForVars", _), |
351 (2, [1], "#Given", Const ("EqSystem.solveForVars", _), |
352 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]), |
352 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]), |
353 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])] |
353 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])] |
354 =>() |
354 =>() |
355 | _ => raise error "calchead.sml match_ags 2 args Nok ----------------"; |
355 | _ => error "calchead.sml match_ags 2 args Nok ----------------"; |
356 |
356 |
357 |
357 |
358 "-b------------------------------------------------------"; |
358 "-b------------------------------------------------------"; |
359 val Const ("Script.SubProblem",_) $ |
359 val Const ("Script.SubProblem",_) $ |
360 (Const ("Pair",_) $ |
360 (Const ("Pair",_) $ |
377 [_ $ Free ("c", _) $ _, |
377 [_ $ Free ("c", _) $ _, |
378 _ $ Free ("c_2", _) $ _]), |
378 _ $ Free ("c_2", _) $ _]), |
379 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])] |
379 (3, [1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)])] |
380 (* type of Find: [Free ("ss'''", "bool List.list")]*) |
380 (* type of Find: [Free ("ss'''", "bool List.list")]*) |
381 =>() |
381 =>() |
382 | _ => raise error "calchead.sml match_ags copy-named dropped --------"; |
382 | _ => error "calchead.sml match_ags copy-named dropped --------"; |
383 |
383 |
384 |
384 |
385 "-c---ERROR case: stac is missing #Given equalities e_s--"; |
385 "-c---ERROR case: stac is missing #Given equalities e_s--"; |
386 val stac as Const ("Script.SubProblem",_) $ |
386 val stac as Const ("Script.SubProblem",_) $ |
387 (Const ("Pair",_) $ |
387 (Const ("Pair",_) $ |
423 "-------------------------------------step through end---"; |
423 "-------------------------------------step through end---"; |
424 |
424 |
425 case ((match_ags (theory "EqSystem") pats ags) |
425 case ((match_ags (theory "EqSystem") pats ags) |
426 handle ERROR _ => []) of (*why not TYPE ?WN100920*) |
426 handle ERROR _ => []) of (*why not TYPE ?WN100920*) |
427 [] => match_ags_msg pI stac ags |
427 [] => match_ags_msg pI stac ags |
428 | _ => raise error "calchead.sml match_ags 1st arg missing --------"; |
428 | _ => error "calchead.sml match_ags 1st arg missing --------"; |
429 |
429 |
430 |
430 |
431 "-d------------------------------------------------------"; |
431 "-d------------------------------------------------------"; |
432 val stac as Const ("Script.SubProblem",_) $ |
432 val stac as Const ("Script.SubProblem",_) $ |
433 (Const ("Pair",_) $ |
433 (Const ("Pair",_) $ |
514 [Const ("op =", _) $ (Const ("Groups.plus_class.plus", _) $ |
514 [Const ("op =", _) $ (Const ("Groups.plus_class.plus", _) $ |
515 Free ("x", _) $ Free ("1", _)) $ Free ("2", _)]), |
515 Free ("x", _) $ Free ("1", _)) $ Free ("2", _)]), |
516 (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]), |
516 (2, [1], "#Given", Const ("Descript.solveFor", _), [Free ("x", _)]), |
517 (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])] |
517 (3, [1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)])] |
518 => () |
518 => () |
519 | _ => raise error "calchead.sml match_ags [univariate,equation,test]--"; |
519 | _ => error "calchead.sml match_ags [univariate,equation,test]--"; |
520 |
520 |
521 |
521 |
522 "--------- regression test fun is_copy_named ------------"; |
522 "--------- regression test fun is_copy_named ------------"; |
523 "--------- regression test fun is_copy_named ------------"; |
523 "--------- regression test fun is_copy_named ------------"; |
524 "--------- regression test fun is_copy_named ------------"; |
524 "--------- regression test fun is_copy_named ------------"; |
525 val trm = (1, (2, @{term "v'i'"})); |
525 val trm = (1, (2, @{term "v'i'"})); |
526 if is_copy_named trm then () else raise error "regr. is_copy_named 1"; |
526 if is_copy_named trm then () else error "regr. is_copy_named 1"; |
527 val trm = (1, (2, @{term "e_e"})); |
527 val trm = (1, (2, @{term "e_e"})); |
528 if is_copy_named trm then raise error "regr. is_copy_named 2" else (); |
528 if is_copy_named trm then error "regr. is_copy_named 2" else (); |
529 val trm = (1, (2, @{term "L'''"})); |
529 val trm = (1, (2, @{term "L'''"})); |
530 if is_copy_named trm then () else raise error "regr. is_copy_named 3"; |
530 if is_copy_named trm then () else error "regr. is_copy_named 3"; |
531 |
531 |
532 (* out-comment 'structure CalcHead'... |
532 (* out-comment 'structure CalcHead'... |
533 val trm = (1, (2, @{term "v'i'"})); |
533 val trm = (1, (2, @{term "v'i'"})); |
534 if is_copy_named_generating trm then () else raise error "regr. is_copy_named"; |
534 if is_copy_named_generating trm then () else error "regr. is_copy_named"; |
535 val trm = (1, (2, @{term "L'''"})); |
535 val trm = (1, (2, @{term "L'''"})); |
536 if is_copy_named_generating trm then raise error "regr. is_copy_named" else (); |
536 if is_copy_named_generating trm then error "regr. is_copy_named" else (); |
537 *) |
537 *) |
538 |
538 |
539 "--------- regr.test fun cpy_nam ------------------------"; |
539 "--------- regr.test fun cpy_nam ------------------------"; |
540 "--------- regr.test fun cpy_nam ------------------------"; |
540 "--------- regr.test fun cpy_nam ------------------------"; |
541 "--------- regr.test fun cpy_nam ------------------------"; |
541 "--------- regr.test fun cpy_nam ------------------------"; |
549 cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))]; |
549 cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))]; |
550 (*...all must be true*) |
550 (*...all must be true*) |
551 |
551 |
552 case cpy_nam pbt oris (hd cy) of |
552 case cpy_nam pbt oris (hd cy) of |
553 ([1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)]) => () |
553 ([1], "#Find", Const ("Descript.solutions", _), [Free ("x_i", _)]) => () |
554 | _ => raise error "calchead.sml regr.test cpy_nam-1-"; |
554 | _ => error "calchead.sml regr.test cpy_nam-1-"; |
555 |
555 |
556 (*new data: cpy_nam without changing the name*) |
556 (*new data: cpy_nam without changing the name*) |
557 @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"}; |
557 @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"}; |
558 @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"}; |
558 @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"}; |
559 @{term "solution"}; type_of @{term "ss''' :: bool list"}; |
559 @{term "solution"}; type_of @{term "ss''' :: bool list"}; |
566 val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"})) |
566 val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"})) |
567 (*could be more than 1*)]; |
567 (*could be more than 1*)]; |
568 |
568 |
569 case cpy_nam pbt oris (hd cy) of |
569 case cpy_nam pbt oris (hd cy) of |
570 ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => () |
570 ([1], "#Find", Const ("EqSystem.solution", _), [Free ("ss'''", _)]) => () |
571 | _ => raise error "calchead.sml regr.test cpy_nam-2-"; |
571 | _ => error "calchead.sml regr.test cpy_nam-2-"; |