(* Title: TODO/state-step.sml

    Author: Walther Neuper

    (c) due to copyright terms

 Deprecated; the idea was to hold steps complete such, that they can be replayed.

 *)

 signature STATE_STEPS =

 sig

   type single

   val single_empty : single

   type T

   val to_string : T -> string

   val result : single -> (term * term list)

   val make_single: Rewrite_Ord.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->

     single

   val insert_pos : Pos.pos -> T -> T

 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

   (* NONE *)

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

   (* NONE *)

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

 end

 (**)

 structure State_Steps(**): STATE_STEPS(**) =

 struct

 (**)

 (* a single holds alle information required to build a node in the calc-tree;

    a single is assumed to be used efficiently such that the calc-tree

    resulting from applying a single need not be stored separately;

    see "type calcstate" *)

 (*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate"

   TODO.WN0512 ? redesign this _list_:

   # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs

   # the latter problem may be resolved automatically if "fun autocalc" is 

     not any more used for the specify-phase and for changing the phases*)

 type single = 

   (Tactic.input *                     (* for comparison with input tac             *)      

    Tactic.T *                         (* for ctree generation                      *)

    (Pos.pos' *                            (* after applying tac_, for ctree generation *)

     (Istate_Def.T * Proof.context)))  (* after applying tac_, for ctree generation *)

 val single_empty = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (Pos.e_pos', (Istate_Def.empty, ContextC.empty))): single

 fun taci2str ((tac, tac_, (pos', (istate, _))):single) =

   "( " ^ Tactic.input_to_string tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ Pos.pos'2str pos' ^ ", " ^

   Istate_Def.string_of istate ^ " ))"

 type T = single list;

 fun to_string tacis = (strs2str o (map (linefeed o taci2str))) tacis

 fun result (_, Tactic.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)

   | result (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)

   | result (_, tac_, _) = raise ERROR ("result: called with" ^ Tactic.string_of tac_)

 fun make_single ro erls (t, r as Rule.Thm (id, thm), (t', a)) = 

       (Tactic.Rewrite (id, thm), 

         Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, ThmC.from_rule r, t, (t', a)),

        (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))

   | make_single _ _ (t, r as Rule.Rls_ rls, (t', a)) = 

       (Tactic.Rewrite_Set (Rule_Set.id_from_rule r), 

         Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),

        (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))

   | make_single _ _ (t, r, _) = raise ERROR ("make_single: not impl. for " ^ Rule.to_string r ^ " at " ^ UnparseC.term t)

 (* update pos in tacis for embedding by generate *)

 fun insert_pos (_: Pos.pos) [] = []

   | insert_pos (p: Pos.pos) (((tac, tac_, (_, ist)): single) :: tacis) = 

     ((tac, tac_, ((p, Pos.Res), ist)): single) :: (insert_pos (Pos.lev_on p) tacis)

 (**)end(**)