wneuper/isa: comparison src/Tools/isac/Interpret/solve-step.sml

equal deleted inserted replaced

-:c06b7df89dcd
+:0f0718c61f68
 *)
 signature SOLVE_STEP =
 sig
 val check: Tactic.input -> Calc.T -> Applicable.T
-val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
+val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T
-val add_general: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
+val add_general: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T
 val s_add_general: State_Steps.T ->
 Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'
 val add_hard:
-theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Generate.test_out
+theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Test_Out.T
 val get_ruleset: 'a -> Pos.pos -> Ctree.ctree ->
 string * ThyC.id * Rule_Def.rew_ord' * Rule_Def.rule_set * bool
 val get_eval: string -> Pos.pos ->Ctree.ctree ->
 string * ThyC.id * (string * Rule_Def.eval_fn)
 fun add (Tactic.Apply_Method' (_, topt, is, _)) (_, ctxt) (pt, pos as (p, _)) =
 (case topt of
 SOME t =>
 let val (pt, c) = Ctree.cappend_form pt p (is, ctxt) t
-in (pos, c, Generate.EmptyMout, pt) end
+in (pos, c, Test_Out.EmptyMout, pt) end
-| NONE => (pos, [], Generate.EmptyMout, pt))
+| NONE => (pos, [], Test_Out.EmptyMout, pt))
 | add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)
 let
 val p =
 let val (ps, p') = split_last p (* no connex to prev.ppobj *)
 	      in if p' = 0 then ps @ [1] else p end
 val (pt, c) = Ctree.cappend_form pt p l t
 in
-((p, Pos.Frm), c, Generate.FormKF (UnparseC.term t), pt)
+((p, Pos.Frm), c, Test_Out.FormKF (UnparseC.term t), pt)
 end
 | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Frm)) =
 let
 val (pt, c) = Ctree.cappend_form pt p l t
 val pt = Ctree.update_branch pt p Ctree.TransitiveB (*040312*)
 (* replace the old PrfOjb ~~~~~ *)
 val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
 val (pt, c') = Ctree.cappend_form pt p l t (*FIXME.0402 same istate ???*)
 in
-((p, Pos.Frm), c @ c', Generate.FormKF (UnparseC.term t), pt)
+((p, Pos.Frm), c @ c', Test_Out.FormKF (UnparseC.term t), pt)
 end
 | add (Tactic.Begin_Trans' t) l (pt, (p, Pos.Res)) =
 (*append after existing PrfObj    vvvvvvvvvvvvv*)
 add (Tactic.Begin_Trans' t) l (pt, (Pos.lev_on p, Pos.Frm))
 | add (Tactic.End_Trans' tasm) l (pt, (p, _)) =
 let
 val p' = Pos.lev_up p
 val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete
 in
-((p', Pos.Res), c, Generate.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
+((p', Pos.Res), c, Test_Out.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
 end
 | add (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
 let
 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
 (Tactic.Rewrite_Inst (Subst.T_to_input subs', thm')) (f',asm) Ctree.Complete;
 val pt = Ctree.update_branch pt p Ctree.TransitiveB
 in
-((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
+((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
 end
 | add (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
 let
 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Ctree.Complete
 val pt = Ctree.update_branch pt p Ctree.TransitiveB
 in
-((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
+((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
 end
 | add (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
 let
 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
 (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Ctree.Complete
 val pt = Ctree.update_branch pt p Ctree.TransitiveB
 in
-((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
+((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
 end
 | add (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
 let
 val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
 (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
 val pt = Ctree.update_branch pt p Ctree.TransitiveB
 in
-((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
+((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
 end
 | add (Tactic.Check_Postcond' (_, scval)) l (pt, (p, _)) =
 let
 val (pt, c) = Ctree.append_result pt p l (scval, []) Ctree.Complete
 in
-((p, Pos.Res), c, Generate.FormKF (UnparseC.term scval), pt)
+((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term scval), pt)
 end
 | add (Tactic.Calculate' (_, op_, f, (f', _))) l (pt, (p, _)) =
 let
 val (pt,c) = Ctree.cappend_atomic pt p l f (Tactic.Calculate op_) (f', []) Ctree.Complete
 in
-((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
+((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
 end
 | add (Tactic.Check_elementwise' (consts, pred, (f', asm))) l (pt, (p, _)) =
 let
 val (pt,c) = Ctree.cappend_atomic pt p l consts (Tactic.Check_elementwise pred) (f', asm) Ctree.Complete
 in
-((p, Pos.Res), c, Generate.FormKF (UnparseC.term f'), pt)
+((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term f'), pt)
 end
 | add (Tactic.Or_to_List' (ors, list)) l (pt, (p, _)) =
 let
 val (pt,c) = Ctree.cappend_atomic pt p l ors Tactic.Or_to_List (list, []) Ctree.Complete
 in
-((p, Pos.Res), c, Generate.FormKF (UnparseC.term list), pt)
+((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term list), pt)
 end
 | add (Tactic.Substitute' (_, _, subte, t, t')) l (pt, (p, _)) =
 let
 val (pt,c) =
 Ctree.cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Ctree.Complete
-in ((p, Pos.Res), c, Generate.FormKF (UnparseC.term t'), pt)
+in ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term t'), pt)
 end
 | add (Tactic.Tac_ (_, f, id, f')) l (pt, (p, _)) =
 let
 val (pt, c) = Ctree.cappend_atomic pt p l (TermC.str2term f) (Tactic.Tac id) (TermC.str2term f', []) Ctree.Complete
 in
-((p,Pos.Res), c, Generate.FormKF f', pt)
+((p,Pos.Res), c, Test_Out.FormKF f', pt)
 end
 | add (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f))
 (l as (_, ctxt)) (pt, (p, _)) =
 let
 	    val (pt, c) = Ctree.cappend_problem pt p l (fmz_, (domID, pblID, metID))
 	      (oris, (domID, pblID, metID), hdl, ctxt_specify)
 	    val f = Syntax.string_of_term (ThyC.to_ctxt (Proof_Context.theory_of ctxt)) f
 in
-((p, Pos.Pbl), c, Generate.FormKF f, pt)
+((p, Pos.Pbl), c, Test_Out.FormKF f, pt)
 end
 | add m' _ (_, pos) =
 raise ERROR ("Solve_Step.add: not impl.for " ^ Tactic.string_of m' ^ " at " ^ Pos.pos'2str pos)
 (* LI switches between solve-phase and specify-phase *)

changeset 59959	0f0718c61f68
parent 59943	4816df44437f
child 59962	6a59d252345d