1.1 --- a/src/Tools/isac/Interpret/solve-step.sml Sun May 10 15:55:30 2020 +0200
1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Sun May 10 17:26:36 2020 +0200
1.3 @@ -8,13 +8,13 @@
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 + val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T
1.9
1.10 - val add_general: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
1.11 + val add_general: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T
1.12 val s_add_general: State_Steps.T ->
1.13 Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'
1.14 val add_hard:
1.15 - theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Generate.test_out
1.16 + theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Test_Out.T
1.17
1.18 val get_ruleset: 'a -> Pos.pos -> Ctree.ctree ->
1.19 string * ThyC.id * Rule_Def.rew_ord' * Rule_Def.rule_set * bool
1.20 @@ -238,8 +238,8 @@
1.21 (case topt of
1.22 SOME t =>
1.23 let val (pt, c) = Ctree.cappend_form pt p (is, ctxt) t
1.24 - in (pos, c, Generate.EmptyMout, pt) end
1.25 - | NONE => (pos, [], Generate.EmptyMout, pt))
1.26 + in (pos, c, Test_Out.EmptyMout, pt) end
1.27 + | NONE => (pos, [], Test_Out.EmptyMout, pt))
1.28 | add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)
1.29 let
1.30 val p =
1.31 @@ -247,7 +247,7 @@
1.32 in if p' = 0 then ps @ [1] else p end
1.33 val (pt, c) = Ctree.cappend_form pt p l t
1.34 in
1.35 - ((p, Pos.Frm), c, Generate.FormKF (UnparseC.term t), pt)
1.36 + ((p, Pos.Frm), c, Test_Out.FormKF (UnparseC.term t), pt)
1.37 end
1.38 | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Frm)) =
1.39 let
1.40 @@ -257,7 +257,7 @@
1.41 val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
1.42 val (pt, c') = Ctree.cappend_form pt p l t (*FIXME.0402 same istate ???*)
1.43 in
1.44 - ((p, Pos.Frm), c @ c', Generate.FormKF (UnparseC.term t), pt)
1.45 + ((p, Pos.Frm), c @ c', Test_Out.FormKF (UnparseC.term t), pt)
1.46 end
1.47 | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Res)) =
1.48 (*append after existing PrfObj vvvvvvvvvvvvv*)
1.49 @@ -267,7 +267,7 @@
1.50 val p' = Pos.lev_up p
1.51 val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete
1.52 in
1.53 - ((p', Pos.Res), c, Generate.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
1.54 + ((p', Pos.Res), c, Test_Out.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
1.55 end
1.56 | add (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
1.57 let
1.58 @@ -275,14 +275,14 @@
1.59 (Tactic.Rewrite_Inst (Subst.T_to_input subs', thm')) (f',asm) Ctree.Complete;
1.60 val pt = Ctree.update_branch pt p Ctree.TransitiveB
1.61 in
1.62 - ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
1.63 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
1.64 end
1.65 | add (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
1.66 let
1.67 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Ctree.Complete
1.68 val pt = Ctree.update_branch pt p Ctree.TransitiveB
1.69 in
1.70 - ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
1.71 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
1.72 end
1.73 | add (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
1.74 let
1.75 @@ -290,7 +290,7 @@
1.76 (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Ctree.Complete
1.77 val pt = Ctree.update_branch pt p Ctree.TransitiveB
1.78 in
1.79 - ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
1.80 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
1.81 end
1.82 | add (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
1.83 let
1.84 @@ -298,43 +298,43 @@
1.85 (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
1.86 val pt = Ctree.update_branch pt p Ctree.TransitiveB
1.87 in
1.88 - ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
1.89 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
1.90 end
1.91 | add (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) =
1.92 let
1.93 val (pt, c) = Ctree.append_result pt p l (scval, []) Ctree.Complete
1.94 in
1.95 - ((p, Pos.Res), c, Generate.FormKF (UnparseC.term scval), pt)
1.96 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term scval), pt)
1.97 end
1.98 | add (Tactic.Calculate' (_, op_, f, (f', _))) l (pt, (p, _)) =
1.99 let
1.100 val (pt,c) = Ctree.cappend_atomic pt p l f (Tactic.Calculate op_) (f', []) Ctree.Complete
1.101 in
1.102 - ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
1.103 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
1.104 end
1.105 | add (Tactic.Check_elementwise' (consts, pred, (f', asm))) l (pt, (p, _)) =
1.106 let
1.107 val (pt,c) = Ctree.cappend_atomic pt p l consts (Tactic.Check_elementwise pred) (f', asm) Ctree.Complete
1.108 in
1.109 - ((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
1.110 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
1.111 end
1.112 | add (Tactic.Or_to_List' (ors, list)) l (pt, (p, _)) =
1.113 let
1.114 val (pt,c) = Ctree.cappend_atomic pt p l ors Tactic.Or_to_List (list, []) Ctree.Complete
1.115 in
1.116 - ((p, Pos.Res), c, Generate.FormKF (UnparseC.term list), pt)
1.117 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term list), pt)
1.118 end
1.119 | add (Tactic.Substitute' (_, _, subte, t, t')) l (pt, (p, _)) =
1.120 let
1.121 val (pt,c) =
1.122 Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete
1.123 - in ((p, Pos.Res), c, Generate.FormKF (UnparseC.term t'), pt)
1.124 + in ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term t'), pt)
1.125 end
1.126 | add (Tactic.Tac_ (_, f, id, f')) l (pt, (p, _)) =
1.127 let
1.128 val (pt, c) = Ctree.cappend_atomic pt p l (TermC.str2term f) (Tactic.Tac id) (TermC.str2term f', []) Ctree.Complete
1.129 in
1.130 - ((p,Pos.Res), c, Generate.FormKF f', pt)
1.131 + ((p,Pos.Res), c, Test_Out.FormKF f', pt)
1.132 end
1.133 | add (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f))
1.134 (l as (_, ctxt)) (pt, (p, _)) =
1.135 @@ -343,7 +343,7 @@
1.136 (oris, (domID, pblID, metID), hdl, ctxt_specify)
1.137 val f = Syntax.string_of_term (ThyC.to_ctxt (Proof_Context.theory_of ctxt)) f
1.138 in
1.139 - ((p, Pos.Pbl), c, Generate.FormKF f, pt)
1.140 + ((p, Pos.Pbl), c, Test_Out.FormKF f, pt)
1.141 end
1.142 | add m' _ (_, pos) =
1.143 raise ERROR ("Solve_Step.add: not impl.for " ^ Tactic.string_of m' ^ " at " ^ Pos.pos'2str pos)