58 val Const (\<^const_name>\<open>SubProblem\<close>,_) $ |
58 val Const (\<^const_name>\<open>SubProblem\<close>,_) $ |
59 (Const (\<^const_name>\<open>Pair\<close>,_) $ |
59 (Const (\<^const_name>\<open>Pair\<close>,_) $ |
60 Free (dI',_) $ |
60 Free (dI',_) $ |
61 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' = |
61 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' = |
62 (*...copied from LItool.tac_from_prog*) |
62 (*...copied from LItool.tac_from_prog*) |
63 TermC.str2term ( |
63 TermC.parse_test @{context} ( |
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 \<up> 2 / 2]," ^ |
65 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L \<up> 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 (\<^const_name>\<open>SubProblem\<close>,_) $ |
83 val Const (\<^const_name>\<open>SubProblem\<close>,_) $ |
84 (Const (\<^const_name>\<open>Pair\<close>,_) $ |
84 (Const (\<^const_name>\<open>Pair\<close>,_) $ |
85 Free (dI',_) $ |
85 Free (dI',_) $ |
86 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' = |
86 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' = |
87 (*...copied from LItool.tac_from_prog*) |
87 (*...copied from LItool.tac_from_prog*) |
88 TermC.str2term ( |
88 TermC.parse_test @{context} ( |
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 \<up> 2 / 2]," ^ |
90 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L \<up> 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 (\<^const_name>\<open>SubProblem\<close>,_) $ |
109 val stac as Const (\<^const_name>\<open>SubProblem\<close>,_) $ |
110 (Const (\<^const_name>\<open>Pair\<close>,_) $ |
110 (Const (\<^const_name>\<open>Pair\<close>,_) $ |
111 Free (dI',_) $ |
111 Free (dI',_) $ |
112 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' = |
112 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' = |
113 (*...copied from LItool.tac_from_prog*) |
113 (*...copied from LItool.tac_from_prog*) |
114 TermC.str2term ( |
114 TermC.parse_test @{context} ( |
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 @{context}) pI; |
119 val pats = (#ppc o Problem.from_store @{context}) pI; |
149 val Const (\<^const_name>\<open>SubProblem\<close>,_) $ |
149 val Const (\<^const_name>\<open>SubProblem\<close>,_) $ |
150 (Const (\<^const_name>\<open>Pair\<close>,_) $ |
150 (Const (\<^const_name>\<open>Pair\<close>,_) $ |
151 Free (dI',_) $ |
151 Free (dI',_) $ |
152 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' = |
152 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' = |
153 (*...copied from LItool.tac_from_prog*) |
153 (*...copied from LItool.tac_from_prog*) |
154 TermC.str2term ( |
154 TermC.parse_test @{context} ( |
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 \<up> 2 / 2]," ^ |
156 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L \<up> 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 (\<^const_name>\<open>SubProblem\<close>,_) $ |
174 val Const (\<^const_name>\<open>SubProblem\<close>,_) $ |
175 (Const (\<^const_name>\<open>Pair\<close>,_) $ |
175 (Const (\<^const_name>\<open>Pair\<close>,_) $ |
176 Free (dI',_) $ |
176 Free (dI',_) $ |
177 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' = |
177 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' = |
178 (*...copied from LItool.tac_from_prog*) |
178 (*...copied from LItool.tac_from_prog*) |
179 TermC.str2term ( |
179 TermC.parse_test @{context} ( |
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 \<up> 2 / 2]," ^ |
181 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L \<up> 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 (\<^const_name>\<open>SubProblem\<close>,_) $ |
200 val stac as Const (\<^const_name>\<open>SubProblem\<close>,_) $ |
201 (Const (\<^const_name>\<open>Pair\<close>,_) $ |
201 (Const (\<^const_name>\<open>Pair\<close>,_) $ |
202 Free (dI',_) $ |
202 Free (dI',_) $ |
203 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' = |
203 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' = |
204 (*...copied from LItool.tac_from_prog*) |
204 (*...copied from LItool.tac_from_prog*) |
205 TermC.str2term ( |
205 TermC.parse_test @{context} ( |
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 @{context}) pI; |
210 val pats = (#ppc o Problem.from_store @{context}) pI; |
245 val stac as Const (\<^const_name>\<open>SubProblem\<close>,_) $ |
245 val stac as Const (\<^const_name>\<open>SubProblem\<close>,_) $ |
246 (Const (\<^const_name>\<open>Pair\<close>,_) $ |
246 (Const (\<^const_name>\<open>Pair\<close>,_) $ |
247 Free (dI',_) $ |
247 Free (dI',_) $ |
248 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' = |
248 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' = |
249 (*...copied from LItool.tac_from_prog*) |
249 (*...copied from LItool.tac_from_prog*) |
250 TermC.str2term ( |
250 TermC.parse_test @{context} ( |
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 (\<^const_name>\<open>SubProblem\<close>, _) $ |
263 val stac as Const (\<^const_name>\<open>SubProblem\<close>, _) $ |
264 (Const (\<^const_name>\<open>Pair\<close>,_) $ |
264 (Const (\<^const_name>\<open>Pair\<close>,_) $ |
265 Free (dI',_) $ |
265 Free (dI',_) $ |
266 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' = |
266 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' = |
267 (*...copied from LItool.tac_from_prog*) |
267 (*...copied from LItool.tac_from_prog*) |
268 TermC.str2term ( |
268 TermC.parse_test @{context} ( |
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 @{context}) pI; |
273 val PATS = (#ppc o Problem.from_store @{context}) pI; |