walther@59908
|
1 |
(* Title: TODO/state-step.sml
|
walther@59908
|
2 |
Author: Walther Neuper
|
walther@59908
|
3 |
(c) due to copyright terms
|
walther@59908
|
4 |
|
walther@59908
|
5 |
Deprecated; the idea was to hold steps complete such, that they can be replayed.
|
walther@59908
|
6 |
*)
|
walther@59908
|
7 |
|
walther@59908
|
8 |
signature STATE_STEPS =
|
walther@59908
|
9 |
sig
|
walther@59908
|
10 |
type single
|
walther@59908
|
11 |
val single_empty : single
|
walther@59908
|
12 |
type T
|
walther@59908
|
13 |
val to_string : T -> string
|
walther@59908
|
14 |
val result : single -> (term * term list)
|
walther@59908
|
15 |
val make_single: Rewrite_Ord.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->
|
walther@59931
|
16 |
single
|
walther@59908
|
17 |
val insert_pos : Pos.pos -> T -> T
|
walther@59908
|
18 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
walther@59908
|
19 |
(* NONE *)
|
walther@59908
|
20 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
walther@59908
|
21 |
(* NONE *)
|
walther@59908
|
22 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
walther@59908
|
23 |
end
|
walther@59908
|
24 |
|
walther@59908
|
25 |
(**)
|
walther@59908
|
26 |
structure State_Steps(**): STATE_STEPS(**) =
|
walther@59908
|
27 |
struct
|
walther@59908
|
28 |
(**)
|
walther@59908
|
29 |
|
walther@59908
|
30 |
(* a single holds alle information required to build a node in the calc-tree;
|
walther@59908
|
31 |
a single is assumed to be used efficiently such that the calc-tree
|
walther@59908
|
32 |
resulting from applying a single need not be stored separately;
|
walther@59908
|
33 |
see "type calcstate" *)
|
walther@59908
|
34 |
(*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate"
|
walther@59908
|
35 |
TODO.WN0512 ? redesign this _list_:
|
walther@59908
|
36 |
# only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs
|
walther@59908
|
37 |
# the latter problem may be resolved automatically if "fun autocalc" is
|
walther@59908
|
38 |
not any more used for the specify-phase and for changing the phases*)
|
walther@59908
|
39 |
type single =
|
walther@59908
|
40 |
(Tactic.input * (* for comparison with input tac *)
|
walther@59908
|
41 |
Tactic.T * (* for ctree generation *)
|
walther@59908
|
42 |
(Pos.pos' * (* after applying tac_, for ctree generation *)
|
walther@59908
|
43 |
(Istate_Def.T * Proof.context))) (* after applying tac_, for ctree generation *)
|
walther@59908
|
44 |
val single_empty = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (Pos.e_pos', (Istate_Def.empty, ContextC.empty))): single
|
walther@59908
|
45 |
fun taci2str ((tac, tac_, (pos', (istate, _))):single) =
|
walther@59908
|
46 |
"( " ^ Tactic.input_to_string tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ Pos.pos'2str pos' ^ ", " ^
|
walther@59908
|
47 |
Istate_Def.string_of istate ^ " ))"
|
walther@59908
|
48 |
|
walther@59908
|
49 |
type T = single list;
|
walther@59908
|
50 |
|
walther@59908
|
51 |
fun to_string tacis = (strs2str o (map (linefeed o taci2str))) tacis
|
walther@59908
|
52 |
fun result (_, Tactic.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
|
walther@59908
|
53 |
| result (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
|
walther@59962
|
54 |
| result (_, tac_, _) = raise ERROR ("result: called with" ^ Tactic.string_of tac_)
|
walther@59914
|
55 |
|
walther@59908
|
56 |
fun make_single ro erls (t, r as Rule.Thm (id, thm), (t', a)) =
|
walther@59908
|
57 |
(Tactic.Rewrite (id, thm),
|
walther@59908
|
58 |
Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, ThmC.from_rule r, t, (t', a)),
|
walther@59908
|
59 |
(Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
|
walther@59908
|
60 |
| make_single _ _ (t, r as Rule.Rls_ rls, (t', a)) =
|
walther@59908
|
61 |
(Tactic.Rewrite_Set (Rule_Set.id_from_rule r),
|
walther@59908
|
62 |
Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
|
walther@59908
|
63 |
(Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
|
walther@59962
|
64 |
| make_single _ _ (t, r, _) = raise ERROR ("make_single: not impl. for " ^ Rule.to_string r ^ " at " ^ UnparseC.term t)
|
walther@59908
|
65 |
|
walther@59908
|
66 |
(* update pos in tacis for embedding by generate *)
|
walther@59908
|
67 |
fun insert_pos (_: Pos.pos) [] = []
|
walther@59908
|
68 |
| insert_pos (p: Pos.pos) (((tac, tac_, (_, ist)): single) :: tacis) =
|
walther@59908
|
69 |
((tac, tac_, ((p, Pos.Res), ist)): single) :: (insert_pos (Pos.lev_on p) tacis)
|
walther@59908
|
70 |
|
walther@59908
|
71 |
(**)end(**)
|
walther@59908
|
72 |
|