1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml	Thu Apr 23 15:48:31 2020 +0200
     1.3 @@ -0,0 +1,75 @@
     1.4 +(* Title: TODO/state-step.sml
     1.5 +   Author: Walther Neuper
     1.6 +   (c) due to copyright terms
     1.7 +
     1.8 +Deprecated; the idea was to hold steps complete such, that they can be replayed.
     1.9 +*)
    1.10 +
    1.11 +signature STATE_STEPS =
    1.12 +sig
    1.13 +  type single
    1.14 +  val single_empty : single
    1.15 +  type T
    1.16 +  val to_string : T -> string
    1.17 +  val result : single -> (term * term list)
    1.18 +  val make_single: Rewrite_Ord.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->
    1.19 +    Tactic.input * Tactic.T * (Pos.pos' * (Istate_Def.T * Proof.context))
    1.20 +  val insert_pos : Pos.pos -> T -> T
    1.21 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.22 +  (* NONE *)
    1.23 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.24 +  (* NONE *)
    1.25 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.26 +end
    1.27 +
    1.28 +(**)
    1.29 +structure State_Steps(**): STATE_STEPS(**) =
    1.30 +struct
    1.31 +(**)
    1.32 +
    1.33 +(*/------- to State_Steps from Generate -------\*)
    1.34 +(* a single holds alle information required to build a node in the calc-tree;
    1.35 +   a single is assumed to be used efficiently such that the calc-tree
    1.36 +   resulting from applying a single need not be stored separately;
    1.37 +   see "type calcstate" *)
    1.38 +(*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate"
    1.39 +  TODO.WN0512 ? redesign this _list_:
    1.40 +  # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs
    1.41 +  # the latter problem may be resolved automatically if "fun autocalc" is 
    1.42 +    not any more used for the specify-phase and for changing the phases*)
    1.43 +type single = 
    1.44 +  (Tactic.input *                     (* for comparison with input tac             *)      
    1.45 +   Tactic.T *                         (* for ctree generation                      *)
    1.46 +   (Pos.pos' *                            (* after applying tac_, for ctree generation *)
    1.47 +    (Istate_Def.T * Proof.context)))  (* after applying tac_, for ctree generation *)
    1.48 +val single_empty = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (Pos.e_pos', (Istate_Def.empty, ContextC.empty))): single
    1.49 +fun taci2str ((tac, tac_, (pos', (istate, _))):single) =
    1.50 +  "( " ^ Tactic.input_to_string tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ Pos.pos'2str pos' ^ ", " ^
    1.51 +  Istate_Def.string_of istate ^ " ))"
    1.52 +
    1.53 +type T = single list;
    1.54 +
    1.55 +fun to_string tacis = (strs2str o (map (linefeed o taci2str))) tacis
    1.56 +fun result (_, Tactic.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
    1.57 +  | result (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
    1.58 +  | result (_, tac_, _) = error ("result: called with" ^ Tactic.string_of tac_)
    1.59 +(*\------- to State_Steps from Generate -------/*)
    1.60 +(*/------- to State_Steps from Error_Pattern -------\*)
    1.61 +fun make_single ro erls (t, r as Rule.Thm (id, thm), (t', a)) = 
    1.62 +      (Tactic.Rewrite (id, thm), 
    1.63 +        Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, ThmC.from_rule r, t, (t', a)),
    1.64 +       (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
    1.65 +  | make_single _ _ (t, r as Rule.Rls_ rls, (t', a)) = 
    1.66 +      (Tactic.Rewrite_Set (Rule_Set.id_from_rule r), 
    1.67 +        Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
    1.68 +       (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
    1.69 +  | make_single _ _ (t, r, _) = error ("make_single: not impl. for " ^ Rule.to_string r ^ " at " ^ UnparseC.term t)
    1.70 +(*\------- to State_Steps from Error_Pattern -------/*)
    1.71 +
    1.72 +(* update pos in tacis for embedding by generate *)
    1.73 +fun insert_pos (_: Pos.pos) [] = []
    1.74 +  | insert_pos (p: Pos.pos) (((tac, tac_, (_, ist)): single) :: tacis) = 
    1.75 +    ((tac, tac_, ((p, Pos.Res), ist)): single) :: (insert_pos (Pos.lev_on p) tacis)
    1.76 +
    1.77 +(**)end(**)
    1.78 +