signature TACTIC =

sig

  datatype tac_ =

    Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list

  | Apply_Assumption' of term list * term

  | Apply_Method' of metID * term option * Selem.istate * Proof.context

  | Begin_Sequ' | Begin_Trans' of term

  | Split_And' of term | Split_Or' of term | Split_Intersect' of term

  | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term

  | End_Sequ' | End_Trans' of Selem.result

  | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''

  | CAScmd' of term

  | Calculate' of theory' * string * term * (term * thm')

  | Check_Postcond' of pblID * Selem.result

  | Check_elementwise' of term * cterm' * Selem.result

  | Del_Find' of cterm' | Del_Given' of cterm' | Del_Relation' of cterm'

  | Derive' of rls

  | Detail_Set' of theory' * bool * rls * term * Selem.result

  | Detail_Set_Inst' of theory' * bool * subst * rls * term * Selem.result

  | End_Detail' of Selem.result

  | Empty_Tac_

  | Free_Solve'

  | Init_Proof' of cterm' list * spec

  | Model_Problem' of pblID * itm list * itm list

  | Or_to_List' of term * term

  | Refine_Problem' of pblID * (itm list * (bool * term) list)

  | Refine_Tacitly' of pblID * pblID * domID * metID * itm list

  | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * Selem.result

  | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * Selem.result

  | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * Selem.result

  | Rewrite_Set' of theory' * bool * rls * term * Selem.result

  | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * Selem.result

  | Specify_Method' of metID * ori list * itm list

  | Specify_Problem' of pblID * (bool * (itm list * (bool * term) list))

  | Specify_Theory' of domID

  | Subproblem' of spec * ori list * term * Selem.fmz_ * Proof.context * term

  | Substitute' of rew_ord_ * rls * Selem.subte * term * term

  | Tac_ of theory * string * string * string

  | Take' of term | Take_Inst' of term

  val tac_2str : tac_ -> string

  datatype tac =

    Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm'

  | Apply_Assumption of cterm' list

  | Apply_Method of metID

  (*/--- TODO: re-design ? -----------------------------------------------------------------\*)

  | Begin_Sequ | Begin_Trans

  | Split_And | Split_Or | Split_Intersect

  | Conclude_And | Conclude_Or | Collect_Trues

  | End_Sequ | End_Trans

  | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'

  (*\--- TODO: re-design ? -----------------------------------------------------------------/*)

  | CAScmd of cterm'

  | Calculate of string

  | Check_Postcond of pblID

  | Check_elementwise of cterm'

  | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm'

  | Derive of rls'

  | Detail_Set of rls'

  | Detail_Set_Inst of Selem.subs * rls'

  | End_Detail

  | Empty_Tac

  | Free_Solve

  | Init_Proof of cterm' list * spec

  | Model_Problem

  | Or_to_List

  | Refine_Problem of pblID

  | Refine_Tacitly of pblID

  | Rewrite of thm''

  | Rewrite_Asm of thm''

  | Rewrite_Inst of Selem.subs * thm''

  | Rewrite_Set of rls'

  | Rewrite_Set_Inst of Selem.subs * rls'

  | Specify_Method of metID

  | Specify_Problem of pblID

  | Specify_Theory of domID

  | Subproblem of domID * pblID

  | Substitute of Selem.sube

  | Tac of string

  | Take of cterm' | Take_Inst of cterm'

  val tac2str : tac -> string

  val eq_tac : tac * tac -> bool                                              (* for script.sml *)

  val is_empty_tac : tac -> bool                                              (* also for tests *)

  val is_rewtac : tac -> bool                                              (* for interface.sml *)

  val is_rewset : tac -> bool                                             (* for mathengine.sml *)

  val rls_of : tac -> rls'                                                     (* for solve.sml *)

  val tac2IDstr : tac -> string

  val rule2tac : theory -> (term * term) list -> rule -> tac                (* for rewtools.sml *)

(* ---- for tests only: made visible in order to remove the warning --------------------------- *)

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

end

structure Tac(**): TACTIC(**) =

struct

(* tactics for user at front-end.

   tac propagates the construction of the calc-tree;

   there are

   (a) 'specsteps' for the specify-phase, and others for the solve-phase

   (b) those of the solve-phase are 'initac's and others;

       initacs start with a formula different from the preceding formula.

   see 'type tac_' for the internal representation of tactics

   TODO.WN161219: replace *every* cterm' by term

*)

datatype tac =

    Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm'

  | Apply_Assumption of cterm' list

  | Apply_Method of metID

    (* creates an "istate" in PblObj.env; in case of "init_form" 

      creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"

      a "SOME istate" at fst of "loc".

      As each step (in the solve-phase) has a resulting formula (at the front-end)

      Apply_Method also does the 1st step in the script (an "initac") if there is no "init_form" *)  

  (*/--- TODO: re-design ? -----------------------------------------------------------------\*)

  | Begin_Sequ | Begin_Trans

  | Split_And | Split_Or | Split_Intersect

  | Conclude_And | Conclude_Or | Collect_Trues

  | End_Sequ | End_Trans

  | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'

  (*\--- TODO: re-design ? -----------------------------------------------------------------/*)

  | CAScmd of cterm'

  | Calculate of string

  | Check_Postcond of pblID

  | Check_elementwise of cterm'

  | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm'

  | Derive of rls'                 (* WN0509 drop *)

  | Detail_Set of rls'             (* WN0509 drop *)

  | Detail_Set_Inst of Selem.subs * rls' (* WN0509 drop *)

  | End_Detail                     (* WN0509 drop *)

  | Empty_Tac

  | Free_Solve

  | Init_Proof of cterm' list * spec

  | Model_Problem

  | Or_to_List

  | Refine_Problem of pblID

  | Refine_Tacitly of pblID

   (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end

     because there all the thms are present with both (thmID, thm)

     (where user-views can show both or only one of (thmID, thm)),

     and thm is created from ThmID by assoc_thm'' when entering isabisac *)

  | Rewrite of thm''

  | Rewrite_Asm of thm''

  | Rewrite_Inst of Selem.subs * thm''

  | Rewrite_Set of rls'

  | Rewrite_Set_Inst of Selem.subs * rls'

  | Specify_Method of metID

  | Specify_Problem of pblID

  | Specify_Theory of domID

  | Subproblem of domID * pblID (* WN0509 drop *)

  | Substitute of Selem.sube

  | Tac of string               (* WN0509 drop *)

  | Take of cterm' | Take_Inst of cterm'

fun tac2str ma = case ma of

    Init_Proof (ppc, spec)  => 

      "Init_Proof "^(pair2str (strs2str ppc, spec2str spec))

  | Model_Problem           => "Model_Problem "

  | Refine_Tacitly pblID    => "Refine_Tacitly " ^ strs2str pblID 

  | Refine_Problem pblID    => "Refine_Problem " ^ strs2str pblID 

  | Add_Given cterm'        => "Add_Given " ^ cterm'

  | Del_Given cterm'        => "Del_Given " ^ cterm'

  | Add_Find cterm'         => "Add_Find " ^ cterm'

  | Del_Find cterm'         => "Del_Find " ^ cterm'

  | Add_Relation cterm'     => "Add_Relation " ^ cterm'

  | Del_Relation cterm'     => "Del_Relation " ^ cterm'

  | Specify_Theory domID    => "Specify_Theory " ^ quote domID

  | Specify_Problem pblID   => "Specify_Problem " ^ strs2str pblID

  | Specify_Method metID    => "Specify_Method " ^ strs2str metID

  | Apply_Method metID      => "Apply_Method " ^ strs2str metID

  | Check_Postcond pblID    => "Check_Postcond " ^ strs2str pblID

  | Free_Solve              => "Free_Solve"

  | Rewrite_Inst (subs, (id, thm)) =>

    "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> term2str)))

  | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> term2str)

  | Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm |> Thm.prop_of |> term2str)

  | Rewrite_Set_Inst (subs, rls) => 

    "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)

  | Rewrite_Set rls         => "Rewrite_Set " ^ quote rls

  | Detail_Set rls          => "Detail_Set " ^ quote rls

  | Detail_Set_Inst (subs, rls) =>  "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)

  | End_Detail              => "End_Detail"

  | Derive rls'             => "Derive " ^ rls' 

  | Calculate op_           => "Calculate " ^ op_ 

  | Substitute sube         => "Substitute " ^ Selem.sube2str sube	     

  | Apply_Assumption ct's   => "Apply_Assumption " ^ strs2str ct's

  | Take cterm'             => "Take " ^ quote cterm'

  | Take_Inst cterm'        => "Take_Inst " ^ quote cterm'

  | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)

  | End_Subproblem          => "End_Subproblem"

  | CAScmd cterm'           => "CAScmd " ^ quote cterm'

  | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'

  | Or_to_List              => "Or_to_List "

  | Collect_Trues           => "Collect_Trues"

  | Empty_Tac               => "Empty_Tac"

  | Tac string              => "Tac " ^ string

  | End_Proof'              => "tac End_Proof'"

  | _                       => "tac2str not impl. for ?!";

fun is_empty_tac tac = case tac of Empty_Tac => true | _ => false

fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2

  | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2

  | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2

  | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2

  | eq_tac (Calculate id1, Calculate id2) = id1 = id2

  | eq_tac _ = false

fun is_rewset (Rewrite_Set_Inst _) = true

  | is_rewset (Rewrite_Set _) = true 

  | is_rewset _ = false;

fun is_rewtac (Rewrite _) = true

  | is_rewtac (Rewrite_Inst _) = true

  | is_rewtac (Rewrite_Asm _) = true

  | is_rewtac tac = is_rewset tac;

fun tac2IDstr ma = case ma of

    Model_Problem => "Model_Problem"

  | Refine_Tacitly _ => "Refine_Tacitly"

  | Refine_Problem _ => "Refine_Problem"

  | Add_Given _ => "Add_Given"

  | Del_Given _ => "Del_Given"

  | Add_Find _ => "Add_Find"

  | Del_Find _ => "Del_Find"

  | Add_Relation _ => "Add_Relation"

  | Del_Relation _ => "Del_Relation"

  | Specify_Theory _ => "Specify_Theory"

  | Specify_Problem _ => "Specify_Problem"

  | Specify_Method _ => "Specify_Method"

  | Apply_Method _ => "Apply_Method"

  | Check_Postcond _ => "Check_Postcond"

  | Free_Solve => "Free_Solve"

  | Rewrite_Inst _ => "Rewrite_Inst"

  | Rewrite _ => "Rewrite"

  | Rewrite_Asm _ => "Rewrite_Asm"

  | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"

  | Rewrite_Set _ => "Rewrite_Set"

  | Detail_Set _ => "Detail_Set"

  | Detail_Set_Inst _ => "Detail_Set_Inst"

  | Derive _ => "Derive "

  | Calculate _ => "Calculate "

  | Substitute _ => "Substitute" 

  | Apply_Assumption _ => "Apply_Assumption"

  | Take _ => "Take"

  | Take_Inst _ => "Take_Inst"

  | Subproblem _ => "Subproblem"

  | End_Subproblem => "End_Subproblem"

  | CAScmd _ => "CAScmd"

  | Check_elementwise _ => "Check_elementwise"

  | Or_to_List => "Or_to_List "

  | Collect_Trues => "Collect_Trues"

  | Empty_Tac => "Empty_Tac"

  | Tac _ => "Tac "

  | End_Proof' => "End_Proof'"

  | _ => "tac2str not impl. for ?!";

fun rls_of (Rewrite_Set_Inst (_, rls)) = rls

  | rls_of (Rewrite_Set rls) = rls

  | rls_of tac = error ("rls_of: called with tac \"" ^ tac2IDstr tac ^ "\"");

fun rule2tac thy _ (Calc (opID, thm)) = Calculate (assoc_calc thy opID)

  | rule2tac _ [] (Thm thm'') = Rewrite thm''

  | rule2tac _ subst (Thm thm'') = 

    Rewrite_Inst (Selem.subst2subs subst, thm'')

  | rule2tac _ [] (Rls_ rls) = Rewrite_Set (id_rls rls)

  | rule2tac _ subst (Rls_ rls) = 

    Rewrite_Set_Inst (Selem.subst2subs subst, (id_rls rls))

  | rule2tac _ _ rule = 

    error ("rule2tac: called with \"" ^ rule2str rule ^ "\"");

(* tactics for for internal use, compare "tac" for user at the front-end.

  tac_ contains results from check in 'fun applicable_in'.

  This is useful for costly results, e.g. from rewriting;

  however, these results might be changed by Scripts like

      "      eq = (Rewrite_Set ansatz_rls False) eql;" ^

      "      eq = drop_questionmarks eq;" ^

      "      eq = (Rewrite_Set equival_trans False) eq;" ^

  TODO.WN120106 ANALOGOUSLY TO Substitute':

  So tac_ contains the term t the result was calculated from

  in order to compare t with t' possibly changed by "Expr "

  and re-calculate result if t<>t'

  TODO.WN161219: replace *every* cterm' by term

*)

  datatype tac_ =

    Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list

  | Apply_Assumption' of term list * term

  | Apply_Method' of metID * term option * Selem.istate * Proof.context

  (*/--- TODO: re-design ? -----------------------------------------------------------------\*)

  | Begin_Sequ' | Begin_Trans' of term

  | Split_And' of term | Split_Or' of term | Split_Intersect' of term

  | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term

  | End_Sequ' | End_Trans' of Selem.result

  | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''

  (*\--- TODO: re-design ? -----------------------------------------------------------------/*)

  | CAScmd' of term

  | Calculate' of theory' * string * term * (term * thm')

  | Check_Postcond' of pblID *

    Selem.result (* returnvalue of script in solve *)

  | Check_elementwise' of (*special case:*)

    term *       (* (1) the current formula: [x=1,x=...]     *)

    string *     (* (2) the pred from Check_elementwise      *)

    Selem.result (* (3) composed from (1) and (2): {x. pred} *)

  | Del_Find' of cterm' | Del_Given' of cterm' | Del_Relation' of cterm'

  | Derive' of rls

  | Detail_Set' of theory' * bool * rls * term * Selem.result

  | Detail_Set_Inst' of theory' * bool * subst * rls * term * Selem.result

  | End_Detail' of Selem.result

  | Empty_Tac_

  | Free_Solve'

  | Init_Proof' of cterm' list * spec

  | Model_Problem' of pblID * 

    itm list *  (* the 'untouched' pbl        *)

    itm list    (* the casually completed met *)

  | Or_to_List' of term * term

  | Refine_Problem' of pblID * (itm list * (bool * term) list)

  | Refine_Tacitly' of

    pblID *     (* input*)

    pblID *     (* the refined from applicable_in                                       *)

    domID *     (* from new pbt?! filled in specify                                     *)

    metID *     (* from new pbt?! filled in specify                                     *)

    itm list    (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)

  | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * Selem.result

  | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * Selem.result

  | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * Selem.result

  | Rewrite_Set' of theory' * bool * rls * term * Selem.result

  | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * Selem.result

  | Specify_Method' of metID * ori list * itm list

  | Specify_Problem' of pblID * 

    (bool *                  (* matches	      *)

      (itm list *            (* ppc	          *)

        (bool * term) list)) (* preconditions *)

  | Specify_Theory' of domID

  | Subproblem' of

    spec * 

		(ori list) *    (* filled in assod Subproblem'        *)

		term *          (* -"-, headline of calc-head         *)

		Selem.fmz_ * 

    Proof.context * (* transported from assod to generate1*)

		term            (* Subproblem(dom,pbl) OR cascmd      *)  

  | Substitute' of

    rew_ord_ *  (* for re-calculation                      *)

    rls *       (* for re-calculation                      *)

    Selem.subte *     (* the 'substitution': terms of type bool  *)

    term *      (* to be substituted in                    *)

    term        (* resulting from the substitution         *)

  | Tac_ of theory * string * string * string

  | Take' of term | Take_Inst' of term

fun tac_2str ma = case ma of

    Init_Proof' (ppc, spec)  => "Init_Proof' " ^ pair2str (strs2str ppc, spec2str spec)

  | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID

  | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^

    strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"

  | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"

  | Add_Given' _ => "Add_Given' "(*^cterm'*)

  | Del_Given' _ => "Del_Given' "(*^cterm'*)

  | Add_Find' _ => "Add_Find' "(*^cterm'*)

  | Del_Find' _ => "Del_Find' "(*^cterm'*)

  | Add_Relation' _ => "Add_Relation' "(*^cterm'*)

  | Del_Relation' _ => "Del_Relation' "(*^cterm'*)

  | Specify_Theory' domID => "Specify_Theory' " ^ quote domID

  | Specify_Problem' (pI, (ok, _)) =>  "Specify_Problem' " ^ 

    spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))

  | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^ 

    metID2str pI ^ ", " ^ oris2str oris ^ ", )"

  | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID

  | Check_Postcond' (pblID, (scval, asm)) => "Check_Postcond' " ^

      (spair2str (strs2str pblID, spair2str (term2str scval, terms2str asm)))

  | Free_Solve' => "Free_Solve'"

  | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)

  | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)

  | Rewrite_Asm' _(*thm'*) => "Rewrite_Asm' "(*^(spair2str thm')*)

  | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)

  | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^

    "," ^ id_rls rls' ^ "," ^ term2str f ^ ",(" ^ term2str f' ^ "," ^ terms2str asm ^ "))"

  | End_Detail' _ => "End_Detail' xxx"

  | Detail_Set' _ => "Detail_Set' xxx"

  | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"

  | Derive' rls => "Derive' " ^ id_rls rls

  | Calculate'  _ => "Calculate' "

  | Substitute' _ => "Substitute' "(*^(subs2str subs)*)    

  | Apply_Assumption' _(* ct's*) => "Apply_Assumption' "(*^(strs2str ct's)*)

  | Take' _(*cterm'*) => "Take' "(*^(quote cterm'	)*)

  | Take_Inst' _(*cterm'*) => "Take_Inst' "(*^(quote cterm' )*)

  | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) => 

    "Subproblem' "(*^(pair2str (domID, strs2str ,))*)

  | End_Subproblem' _ => "End_Subproblem'"

  | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)

  | Empty_Tac_ => "Empty_Tac_"

  | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"

  | _  => "tac_2str not impl. for arg";

end