1.1 --- a/src/Tools/isac/Interpret/solve-step.sml Sat May 02 16:55:14 2020 +0200
1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Sat May 02 17:39:04 2020 +0200
1.3 @@ -8,6 +8,7 @@
1.4 signature SOLVE_STEP =
1.5 sig
1.6 val check: Tactic.input -> Calc.T -> Applicable.T
1.7 + val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
1.8 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.9 (*NONE*)
1.10 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.11 @@ -162,4 +163,111 @@
1.12 | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof''
1.13 | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m);
1.14
1.15 +fun add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)
1.16 + let
1.17 + val p =
1.18 + let val (ps, p') = split_last p (* no connex to prev.ppobj *)
1.19 + in if p' = 0 then ps @ [1] else p end
1.20 + val (pt, c) = Ctree.cappend_form pt p l t
1.21 + in
1.22 + ((p, Pos.Frm), c, Generate.FormKF (UnparseC.term t), pt)
1.23 + end
1.24 + | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Frm)) =
1.25 + let
1.26 + val (pt, c) = Ctree.cappend_form pt p l t
1.27 + val pt = Ctree.update_branch pt p Ctree.TransitiveB (*040312*)
1.28 + (* replace the old PrfOjb ~~~~~ *)
1.29 + val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
1.30 + val (pt, c') = Ctree.cappend_form pt p l t (*FIXME.0402 same istate ???*)
1.31 + in
1.32 + ((p, Pos.Frm), c @ c', Generate.FormKF (UnparseC.term t), pt)
1.33 + end
1.34 + | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Res)) =
1.35 + (*append after existing PrfObj vvvvvvvvvvvvv*)
1.36 + add (Tactic.Begin_Trans' t) l (pt, (Pos.lev_on p, Pos.Frm))
1.37 + | add (Tactic.End_Trans' tasm) l (pt, (p, _)) =
1.38 + let
1.39 + val p' = Pos.lev_up p
1.40 + val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete
1.41 + in
1.42 + ((p', Pos.Res), c, Generate.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
1.43 + end
1.44 + | add (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
1.45 + let
1.46 + val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
1.47 + (Tactic.Rewrite_Inst (Subst.T_to_input subs', thm')) (f',asm) Ctree.Complete;
1.48 + val pt = Ctree.update_branch pt p Ctree.TransitiveB
1.49 + in
1.50 + ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
1.51 + end
1.52 + | add (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
1.53 + let
1.54 + val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Ctree.Complete
1.55 + val pt = Ctree.update_branch pt p Ctree.TransitiveB
1.56 + in
1.57 + ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
1.58 + end
1.59 + | add (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
1.60 + let
1.61 + val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
1.62 + (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Ctree.Complete
1.63 + val pt = Ctree.update_branch pt p Ctree.TransitiveB
1.64 + in
1.65 + ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
1.66 + end
1.67 + | add (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
1.68 + let
1.69 + val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
1.70 + (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
1.71 + val pt = Ctree.update_branch pt p Ctree.TransitiveB
1.72 + in
1.73 + ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
1.74 + end
1.75 + | add (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) =
1.76 + let
1.77 + val (pt, c) = Ctree.append_result pt p l (scval, []) Ctree.Complete
1.78 + in
1.79 + ((p, Pos.Res), c, Generate.FormKF (UnparseC.term scval), pt)
1.80 + end
1.81 + | add (Tactic.Calculate' (_, op_, f, (f', _))) l (pt, (p, _)) =
1.82 + let
1.83 + val (pt,c) = Ctree.cappend_atomic pt p l f (Tactic.Calculate op_) (f', []) Ctree.Complete
1.84 + in
1.85 + ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
1.86 + end
1.87 + | add (Tactic.Check_elementwise' (consts, pred, (f', asm))) l (pt, (p, _)) =
1.88 + let
1.89 + val (pt,c) = Ctree.cappend_atomic pt p l consts (Tactic.Check_elementwise pred) (f', asm) Ctree.Complete
1.90 + in
1.91 + ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
1.92 + end
1.93 + | add (Tactic.Or_to_List' (ors, list)) l (pt, (p, _)) =
1.94 + let
1.95 + val (pt,c) = Ctree.cappend_atomic pt p l ors Tactic.Or_to_List (list, []) Ctree.Complete
1.96 + in
1.97 + ((p, Pos.Res), c, Generate.FormKF (UnparseC.term list), pt)
1.98 + end
1.99 + | add (Tactic.Substitute' (_, _, subte, t, t')) l (pt, (p, _)) =
1.100 + let
1.101 + val (pt,c) =
1.102 + Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete
1.103 + in ((p, Pos.Res), c, Generate.FormKF (UnparseC.term t'), pt)
1.104 + end
1.105 + | add (Tactic.Tac_ (_, f, id, f')) l (pt, (p, _)) =
1.106 + let
1.107 + val (pt, c) = Ctree.cappend_atomic pt p l (TermC.str2term f) (Tactic.Tac id) (TermC.str2term f', []) Ctree.Complete
1.108 + in
1.109 + ((p,Pos.Res), c, Generate.FormKF f', pt)
1.110 + end
1.111 + | add (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f))
1.112 + (l as (_, ctxt)) (pt, (p, _)) =
1.113 + let
1.114 + val (pt, c) = Ctree.cappend_problem pt p l (fmz_, (domID, pblID, metID))
1.115 + (oris, (domID, pblID, metID), hdl, ctxt_specify)
1.116 + val f = Syntax.string_of_term (ThyC.to_ctxt (Proof_Context.theory_of ctxt)) f
1.117 + in
1.118 + ((p, Pos.Pbl), c, Generate.FormKF f, pt)
1.119 + end
1.120 + | add m' _ _ = raise ERROR ("add: not impl.for " ^ Tactic.string_of m')
1.121 +
1.122 (**)end(**);