equal
deleted
inserted
replaced
81 |
81 |
82 autoCalculate 1 CompleteCalc; |
82 autoCalculate 1 CompleteCalc; |
83 |
83 |
84 val ((pt,p),_) = get_calc 1; show_pt pt; |
84 val ((pt,p),_) = get_calc 1; show_pt pt; |
85 if existpt' ([1], Frm) pt then () |
85 if existpt' ([1], Frm) pt then () |
86 else raise error "scrtools.sml: test-script test_interSteps_1 doesnt work"; |
86 else error "scrtools.sml: test-script test_interSteps_1 doesnt work"; |
87 |
87 |
88 |
88 |
89 "-------- test the same called by interSteps norm_Poly -----------"; |
89 "-------- test the same called by interSteps norm_Poly -----------"; |
90 "-------- test the same called by interSteps norm_Poly -----------"; |
90 "-------- test the same called by interSteps norm_Poly -----------"; |
91 "-------- test the same called by interSteps norm_Poly -----------"; |
91 "-------- test the same called by interSteps norm_Poly -----------"; |
106 val ((pt,p),_) = get_calc 1; show_pt pt; |
106 val ((pt,p),_) = get_calc 1; show_pt pt; |
107 |
107 |
108 interSteps 1 ([1], Res); |
108 interSteps 1 ([1], Res); |
109 val ((pt,p),_) = get_calc 1; show_pt pt; |
109 val ((pt,p),_) = get_calc 1; show_pt pt; |
110 if existpt' ([1,4], Res) pt then () |
110 if existpt' ([1,4], Res) pt then () |
111 else raise error "scrtools.sml: auto-generated norm_Poly doesnt work"; |
111 else error "scrtools.sml: auto-generated norm_Poly doesnt work"; |
112 |
112 |
113 |
113 |
114 |
114 |
115 "-------- test the same called by interSteps norm_Rational -------"; |
115 "-------- test the same called by interSteps norm_Rational -------"; |
116 "-------- test the same called by interSteps norm_Rational -------"; |
116 "-------- test the same called by interSteps norm_Rational -------"; |
172 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res)); |
172 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res)); |
173 *) |
173 *) |
174 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res)); |
174 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res)); |
175 case (term2str form, tac, terms2strs asm) of |
175 case (term2str form, tac, terms2strs asm) of |
176 ("a", Check_Postcond ["polynomial", "simplification"], []) => () |
176 ("a", Check_Postcond ["polynomial", "simplification"], []) => () |
177 | _ => raise error "scrtools.sml: auto-generated norm_Rational doesnt work"; |
177 | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work"; |
178 |
178 |
179 |
179 |
180 |
180 |
181 "-------- check auto-gen.script for Rewrite_Set_Inst -------------"; |
181 "-------- check auto-gen.script for Rewrite_Set_Inst -------------"; |
182 "-------- check auto-gen.script for Rewrite_Set_Inst -------------"; |
182 "-------- check auto-gen.script for Rewrite_Set_Inst -------------"; |
184 val rls = assoc_rls "integration"; |
184 val rls = assoc_rls "integration"; |
185 val Seq {scr = Script auto_script,...} = rls; |
185 val Seq {scr = Script auto_script,...} = rls; |
186 writeln(term2str auto_script); |
186 writeln(term2str auto_script); |
187 |
187 |
188 if contain_bdv (get_rules rls) then () |
188 if contain_bdv (get_rules rls) then () |
189 else raise error "scrtools.sml: contain_bdv doesnt work for 'integration'"; |
189 else error "scrtools.sml: contain_bdv doesnt work for 'integration'"; |
190 |
190 |
191 two_scr_arg auto_script; |
191 two_scr_arg auto_script; |
192 init_istate (Rewrite_Set_Inst (["(bdv, x)"], "integration_rules")) |
192 init_istate (Rewrite_Set_Inst (["(bdv, x)"], "integration_rules")) |
193 (str2term "someTermWithBdv"); |
193 (str2term "someTermWithBdv"); |