29 Given = [ |
29 Given = [ |
30 Correct "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))", |
30 Correct "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))", |
31 Correct "solveFor x", |
31 Correct "solveFor x", |
32 Superfl "errorBound (eps = 0)"], |
32 Superfl "errorBound (eps = 0)"], |
33 Relate = [], |
33 Relate = [], |
34 Where = [Correct "matches (?a = ?b) (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"], |
34 Where = [Correct "TermC.matches (?a = ?b) (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"], |
35 With = []} => () |
35 With = []} => () |
36 | _ => error "M_Match.match_pbl CHANGED"; |
36 | _ => error "M_Match.match_pbl CHANGED"; |
37 |
37 |
38 |
38 |
39 "----------- fun match_oris --------------------------------------------------------------------"; |
39 "----------- fun match_oris --------------------------------------------------------------------"; |
58 val Const ("Prog_Tac.SubProblem",_) $ |
58 val Const ("Prog_Tac.SubProblem",_) $ |
59 (Const ("Product_Type.Pair",_) $ |
59 (Const ("Product_Type.Pair",_) $ |
60 Free (dI',_) $ |
60 Free (dI',_) $ |
61 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = |
61 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = |
62 (*...copied from LItool.tac_from_prog*) |
62 (*...copied from LItool.tac_from_prog*) |
63 str2term ( |
63 TermC.str2term ( |
64 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^ |
64 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^ |
65 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^ |
65 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^ |
66 " REAL_LIST [c, c_2]]"); |
66 " REAL_LIST [c, c_2]]"); |
67 val ags = isalist2list ags'; |
67 val ags = isalist2list ags'; |
68 val pI = ["LINEAR", "system"]; |
68 val pI = ["LINEAR", "system"]; |
83 val Const ("Prog_Tac.SubProblem",_) $ |
83 val Const ("Prog_Tac.SubProblem",_) $ |
84 (Const ("Product_Type.Pair",_) $ |
84 (Const ("Product_Type.Pair",_) $ |
85 Free (dI',_) $ |
85 Free (dI',_) $ |
86 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = |
86 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = |
87 (*...copied from LItool.tac_from_prog*) |
87 (*...copied from LItool.tac_from_prog*) |
88 str2term ( |
88 TermC.str2term ( |
89 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^ |
89 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^ |
90 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^ |
90 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^ |
91 " REAL_LIST [c, c_2], BOOL_LIST ss''']"); |
91 " REAL_LIST [c, c_2], BOOL_LIST ss''']"); |
92 val ags = isalist2list ags'; |
92 val ags = isalist2list ags'; |
93 val pI = ["LINEAR", "system"]; |
93 val pI = ["LINEAR", "system"]; |
109 val stac as Const ("Prog_Tac.SubProblem",_) $ |
109 val stac as Const ("Prog_Tac.SubProblem",_) $ |
110 (Const ("Product_Type.Pair",_) $ |
110 (Const ("Product_Type.Pair",_) $ |
111 Free (dI',_) $ |
111 Free (dI',_) $ |
112 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = |
112 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = |
113 (*...copied from LItool.tac_from_prog*) |
113 (*...copied from LItool.tac_from_prog*) |
114 str2term ( |
114 TermC.str2term ( |
115 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^ |
115 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^ |
116 " [REAL_LIST [c, c_2]]"); |
116 " [REAL_LIST [c, c_2]]"); |
117 val ags = isalist2list ags'; |
117 val ags = isalist2list ags'; |
118 val pI = ["LINEAR", "system"]; |
118 val pI = ["LINEAR", "system"]; |
119 val pats = (#ppc o Problem.from_store) pI; |
119 val pats = (#ppc o Problem.from_store) pI; |
149 val Const ("Prog_Tac.SubProblem",_) $ |
149 val Const ("Prog_Tac.SubProblem",_) $ |
150 (Const ("Product_Type.Pair",_) $ |
150 (Const ("Product_Type.Pair",_) $ |
151 Free (dI',_) $ |
151 Free (dI',_) $ |
152 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = |
152 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = |
153 (*...copied from LItool.tac_from_prog*) |
153 (*...copied from LItool.tac_from_prog*) |
154 str2term ( |
154 TermC.str2term ( |
155 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^ |
155 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^ |
156 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^ |
156 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^ |
157 " REAL_LIST [c, c_2]]"); |
157 " REAL_LIST [c, c_2]]"); |
158 val ags = isalist2list ags'; |
158 val ags = isalist2list ags'; |
159 val pI = ["LINEAR", "system"]; |
159 val pI = ["LINEAR", "system"]; |
174 val Const ("Prog_Tac.SubProblem",_) $ |
174 val Const ("Prog_Tac.SubProblem",_) $ |
175 (Const ("Product_Type.Pair",_) $ |
175 (Const ("Product_Type.Pair",_) $ |
176 Free (dI',_) $ |
176 Free (dI',_) $ |
177 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = |
177 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = |
178 (*...copied from LItool.tac_from_prog*) |
178 (*...copied from LItool.tac_from_prog*) |
179 str2term ( |
179 TermC.str2term ( |
180 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^ |
180 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^ |
181 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^ |
181 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^ |
182 " REAL_LIST [c, c_2], BOOL_LIST ss''']"); |
182 " REAL_LIST [c, c_2], BOOL_LIST ss''']"); |
183 val ags = isalist2list ags'; |
183 val ags = isalist2list ags'; |
184 val pI = ["LINEAR", "system"]; |
184 val pI = ["LINEAR", "system"]; |
200 val stac as Const ("Prog_Tac.SubProblem",_) $ |
200 val stac as Const ("Prog_Tac.SubProblem",_) $ |
201 (Const ("Product_Type.Pair",_) $ |
201 (Const ("Product_Type.Pair",_) $ |
202 Free (dI',_) $ |
202 Free (dI',_) $ |
203 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = |
203 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = |
204 (*...copied from LItool.tac_from_prog*) |
204 (*...copied from LItool.tac_from_prog*) |
205 str2term ( |
205 TermC.str2term ( |
206 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^ |
206 "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^ |
207 " [REAL_LIST [c, c_2]]"); |
207 " [REAL_LIST [c, c_2]]"); |
208 val ags = isalist2list ags'; |
208 val ags = isalist2list ags'; |
209 val pI = ["LINEAR", "system"]; |
209 val pI = ["LINEAR", "system"]; |
210 val pats = (#ppc o Problem.from_store) pI; |
210 val pats = (#ppc o Problem.from_store) pI; |
245 val stac as Const ("Prog_Tac.SubProblem",_) $ |
245 val stac as Const ("Prog_Tac.SubProblem",_) $ |
246 (Const ("Product_Type.Pair",_) $ |
246 (Const ("Product_Type.Pair",_) $ |
247 Free (dI',_) $ |
247 Free (dI',_) $ |
248 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = |
248 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = |
249 (*...copied from LItool.tac_from_prog*) |
249 (*...copied from LItool.tac_from_prog*) |
250 str2term ( |
250 TermC.str2term ( |
251 "SubProblem (TestX,[univariate,equation,test]," ^ |
251 "SubProblem (TestX,[univariate,equation,test]," ^ |
252 " [no_met]) [BOOL (x+1=2), REAL x]"); |
252 " [no_met]) [BOOL (x+1=2), REAL x]"); |
253 val AGS = isalist2list ags'; |
253 val AGS = isalist2list ags'; |
254 val pI = ["univariate", "equation", "test"]; |
254 val pI = ["univariate", "equation", "test"]; |
255 |
255 |
263 val stac as Const ("Prog_Tac.SubProblem",_) $ |
263 val stac as Const ("Prog_Tac.SubProblem",_) $ |
264 (Const ("Product_Type.Pair",_) $ |
264 (Const ("Product_Type.Pair",_) $ |
265 Free (dI',_) $ |
265 Free (dI',_) $ |
266 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = |
266 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' = |
267 (*...copied from LItool.tac_from_prog*) |
267 (*...copied from LItool.tac_from_prog*) |
268 str2term ( |
268 TermC.str2term ( |
269 "SubProblem (TestX,[univariate,equation,test]," ^ |
269 "SubProblem (TestX,[univariate,equation,test]," ^ |
270 " [no_met]) [BOOL (x+1=2), REAL x]"); |
270 " [no_met]) [BOOL (x+1=2), REAL x]"); |
271 val AGS = isalist2list ags'; |
271 val AGS = isalist2list ags'; |
272 val pI = ["univariate", "equation", "test"]; |
272 val pI = ["univariate", "equation", "test"]; |
273 val PATS = (#ppc o Problem.from_store) pI; |
273 val PATS = (#ppc o Problem.from_store) pI; |