1 (* Title: TODO/state-step.sml
3 (c) due to copyright terms
5 Deprecated; the idea was to hold steps complete such, that they can be replayed.
8 signature STATE_STEPS =
11 val single_empty : single
13 val to_string : Proof.context -> T -> string
14 val result : Proof.context -> single -> (term * term list)
15 val make_single: Proof.context -> Rewrite_Ord.id * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->
17 val insert_pos : Pos.pos -> T -> T
21 structure State_Steps(**): STATE_STEPS(**) =
25 (* a single holds alle information required to build a node in the calc-tree;
26 a single is assumed to be used efficiently such that the calc-tree
27 resulting from applying a single need not be stored separately;
28 see "type Calc.state_pre" *)
29 (*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate"
30 TODO.WN0512 ? redesign this _list_:
31 # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs
32 # the latter problem may be resolved automatically if "fun autocalc" is
33 not any more used for the specify-phase and for changing the phases*)
35 (Tactic.input * (* for comparison with input tac *)
36 Tactic.T * (* for ctree generation *)
37 (Pos.pos' * (* after applying tac_, for ctree generation *)
38 (Istate_Def.T * Proof.context))) (* after applying tac_, for ctree generation *)
39 val single_empty = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (Pos.e_pos', (Istate_Def.empty, ContextC.empty))): single
40 fun taci2str ctxt ((tac, tac_, (pos', (istate, _))): single) =
41 "( " ^ Tactic.input_to_string ctxt tac ^ ", " ^ Tactic.string_of ctxt tac_ ^ ", ( " ^ Pos.pos'2str pos' ^ ", " ^
42 Istate_Def.string_of ctxt istate ^ " ))"
46 fun to_string ctxt tacis = (strs2str o (map (linefeed o (taci2str ctxt)))) tacis
47 fun result _ (_, Tactic.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
48 | result _ (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
49 | result ctxt (_, tac_, _) = raise ERROR ("result: called with" ^ Tactic.string_of ctxt tac_)
51 fun make_single ctxt ro asm_rls (t, r as Rule.Thm (id, thm), (t', a)) =
52 (Tactic.Rewrite (id, thm),
53 Tactic.Rewrite' ("Isac_Knowledge", fst ro, asm_rls, false, ThmC.from_rule ctxt r, t, (t', a)),
54 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
55 | make_single ctxt _ _ (t, r as Rule.Rls_ rls, (t', a)) =
56 (Tactic.Rewrite_Set (Rule_Set.id_from_rule ctxt r),
57 Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
58 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
59 | make_single ctxt _ _ (t, r, _) = raise ERROR ("State_Steps.make_single: not impl. for " ^
60 Rule.to_string ctxt r ^ " at " ^ UnparseC.term ctxt t)
62 (* update pos in tacis for embedding by generate *)
63 fun insert_pos (_: Pos.pos) [] = []
64 | insert_pos (p: Pos.pos) (((tac, tac_, (_, ist)): single) :: tacis) =
65 ((tac, tac_, ((p, Pos.Res), ist)): single) :: (insert_pos (Pos.lev_on p) tacis)