160 then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p)) |
161 then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p)) |
161 else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence" |
162 else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence" |
162 | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof'' |
163 | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof'' |
163 | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m); |
164 | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m); |
164 |
165 |
|
166 fun add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *) |
|
167 let |
|
168 val p = |
|
169 let val (ps, p') = split_last p (* no connex to prev.ppobj *) |
|
170 in if p' = 0 then ps @ [1] else p end |
|
171 val (pt, c) = Ctree.cappend_form pt p l t |
|
172 in |
|
173 ((p, Pos.Frm), c, Generate.FormKF (UnparseC.term t), pt) |
|
174 end |
|
175 | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Frm)) = |
|
176 let |
|
177 val (pt, c) = Ctree.cappend_form pt p l t |
|
178 val pt = Ctree.update_branch pt p Ctree.TransitiveB (*040312*) |
|
179 (* replace the old PrfOjb ~~~~~ *) |
|
180 val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p |
|
181 val (pt, c') = Ctree.cappend_form pt p l t (*FIXME.0402 same istate ???*) |
|
182 in |
|
183 ((p, Pos.Frm), c @ c', Generate.FormKF (UnparseC.term t), pt) |
|
184 end |
|
185 | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Res)) = |
|
186 (*append after existing PrfObj vvvvvvvvvvvvv*) |
|
187 add (Tactic.Begin_Trans' t) l (pt, (Pos.lev_on p, Pos.Frm)) |
|
188 | add (Tactic.End_Trans' tasm) l (pt, (p, _)) = |
|
189 let |
|
190 val p' = Pos.lev_up p |
|
191 val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete |
|
192 in |
|
193 ((p', Pos.Res), c, Generate.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt) |
|
194 end |
|
195 | add (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) = |
|
196 let |
|
197 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f |
|
198 (Tactic.Rewrite_Inst (Subst.T_to_input subs', thm')) (f',asm) Ctree.Complete; |
|
199 val pt = Ctree.update_branch pt p Ctree.TransitiveB |
|
200 in |
|
201 ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt) |
|
202 end |
|
203 | add (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) = |
|
204 let |
|
205 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Ctree.Complete |
|
206 val pt = Ctree.update_branch pt p Ctree.TransitiveB |
|
207 in |
|
208 ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt) |
|
209 end |
|
210 | add (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) = |
|
211 let |
|
212 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f |
|
213 (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Ctree.Complete |
|
214 val pt = Ctree.update_branch pt p Ctree.TransitiveB |
|
215 in |
|
216 ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt) |
|
217 end |
|
218 | add (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) = |
|
219 let |
|
220 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f |
|
221 (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete |
|
222 val pt = Ctree.update_branch pt p Ctree.TransitiveB |
|
223 in |
|
224 ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt) |
|
225 end |
|
226 | add (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) = |
|
227 let |
|
228 val (pt, c) = Ctree.append_result pt p l (scval, []) Ctree.Complete |
|
229 in |
|
230 ((p, Pos.Res), c, Generate.FormKF (UnparseC.term scval), pt) |
|
231 end |
|
232 | add (Tactic.Calculate' (_, op_, f, (f', _))) l (pt, (p, _)) = |
|
233 let |
|
234 val (pt,c) = Ctree.cappend_atomic pt p l f (Tactic.Calculate op_) (f', []) Ctree.Complete |
|
235 in |
|
236 ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt) |
|
237 end |
|
238 | add (Tactic.Check_elementwise' (consts, pred, (f', asm))) l (pt, (p, _)) = |
|
239 let |
|
240 val (pt,c) = Ctree.cappend_atomic pt p l consts (Tactic.Check_elementwise pred) (f', asm) Ctree.Complete |
|
241 in |
|
242 ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt) |
|
243 end |
|
244 | add (Tactic.Or_to_List' (ors, list)) l (pt, (p, _)) = |
|
245 let |
|
246 val (pt,c) = Ctree.cappend_atomic pt p l ors Tactic.Or_to_List (list, []) Ctree.Complete |
|
247 in |
|
248 ((p, Pos.Res), c, Generate.FormKF (UnparseC.term list), pt) |
|
249 end |
|
250 | add (Tactic.Substitute' (_, _, subte, t, t')) l (pt, (p, _)) = |
|
251 let |
|
252 val (pt,c) = |
|
253 Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete |
|
254 in ((p, Pos.Res), c, Generate.FormKF (UnparseC.term t'), pt) |
|
255 end |
|
256 | add (Tactic.Tac_ (_, f, id, f')) l (pt, (p, _)) = |
|
257 let |
|
258 val (pt, c) = Ctree.cappend_atomic pt p l (TermC.str2term f) (Tactic.Tac id) (TermC.str2term f', []) Ctree.Complete |
|
259 in |
|
260 ((p,Pos.Res), c, Generate.FormKF f', pt) |
|
261 end |
|
262 | add (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f)) |
|
263 (l as (_, ctxt)) (pt, (p, _)) = |
|
264 let |
|
265 val (pt, c) = Ctree.cappend_problem pt p l (fmz_, (domID, pblID, metID)) |
|
266 (oris, (domID, pblID, metID), hdl, ctxt_specify) |
|
267 val f = Syntax.string_of_term (ThyC.to_ctxt (Proof_Context.theory_of ctxt)) f |
|
268 in |
|
269 ((p, Pos.Pbl), c, Generate.FormKF f, pt) |
|
270 end |
|
271 | add m' _ _ = raise ERROR ("add: not impl.for " ^ Tactic.string_of m') |
|
272 |
165 (**)end(**); |
273 (**)end(**); |