src/Tools/isac/MathEngBasic/state-steps.sml
author wneuper <Walther.Neuper@jku.at>
Sun, 08 Jan 2023 17:26:00 +0100
changeset 60643 376a1629989e
parent 60628 f54e20d9e6ee
child 60644 1cc81845432d
permissions -rw-r--r--
eliminate use of Thy_Info 6: improve ctxt in fetchProposedTactic, Error_Pattern, etc
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@60628
    13
  val to_string : Proof.context -> T -> string
walther@59908
    14
  val result : single -> (term * term list)
Walther@60643
    15
  val make_single: Proof.context -> Rewrite_Ord.id * '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
end
walther@59908
    19
walther@59908
    20
(**)
walther@59908
    21
structure State_Steps(**): STATE_STEPS(**) =
walther@59908
    22
struct
walther@59908
    23
(**)
walther@59908
    24
walther@59908
    25
(* a single holds alle information required to build a node in the calc-tree;
walther@59908
    26
   a single is assumed to be used efficiently such that the calc-tree
walther@59908
    27
   resulting from applying a single need not be stored separately;
walther@59981
    28
   see "type Calc.state_pre" *)
walther@59908
    29
(*TODO.WN0504 redesign ??? or redesign generate ?? see "fun generate"
walther@59908
    30
  TODO.WN0512 ? redesign this _list_:
walther@59908
    31
  # only used for [Apply_Method + (Take or Subproblem)], i.e. for initacs
walther@59908
    32
  # the latter problem may be resolved automatically if "fun autocalc" is 
walther@59908
    33
    not any more used for the specify-phase and for changing the phases*)
walther@59908
    34
type single = 
walther@59908
    35
  (Tactic.input *                     (* for comparison with input tac             *)      
walther@59908
    36
   Tactic.T *                         (* for ctree generation                      *)
Walther@60530
    37
   (Pos.pos' *                        (* after applying tac_, for ctree generation *)
walther@59908
    38
    (Istate_Def.T * Proof.context)))  (* after applying tac_, for ctree generation *)
walther@59908
    39
val single_empty = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (Pos.e_pos', (Istate_Def.empty, ContextC.empty))): single
Walther@60628
    40
fun taci2str ctxt ((tac, tac_, (pos', (istate, _))): single) =
Walther@60628
    41
  "( " ^ Tactic.input_to_string ctxt tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ Pos.pos'2str pos' ^ ", " ^
walther@59908
    42
  Istate_Def.string_of istate ^ " ))"
walther@59908
    43
walther@59908
    44
type T = single list;
walther@59908
    45
Walther@60628
    46
fun to_string ctxt tacis = (strs2str o (map (linefeed o (taci2str ctxt)))) tacis
walther@59908
    47
fun result (_, Tactic.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
walther@59908
    48
  | result (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
walther@59962
    49
  | result (_, tac_, _) = raise ERROR ("result: called with" ^ Tactic.string_of tac_)
walther@59914
    50
Walther@60643
    51
fun make_single _ ro asm_rls (t, r as Rule.Thm (id, thm), (t', a)) = 
walther@59908
    52
      (Tactic.Rewrite (id, thm), 
Walther@60586
    53
        Tactic.Rewrite' ("Isac_Knowledge", fst ro, asm_rls, false, ThmC.from_rule r, t, (t', a)),
walther@59908
    54
       (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
Walther@60643
    55
  | make_single ctxt _ _ (t, r as Rule.Rls_ rls, (t', a)) = 
Walther@60643
    56
      (Tactic.Rewrite_Set (Rule_Set.id_from_rule ctxt r), 
walther@59908
    57
        Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
walther@59908
    58
       (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
Walther@60643
    59
  | make_single ctxt _ _ (t, r, _) = raise ERROR ("make_single: not impl. for " ^ Rule.to_string r ^
Walther@60643
    60
      " at " ^ UnparseC.term_in_ctxt ctxt t)
walther@59908
    61
walther@59908
    62
(* update pos in tacis for embedding by generate *)
walther@59908
    63
fun insert_pos (_: Pos.pos) [] = []
walther@59908
    64
  | insert_pos (p: Pos.pos) (((tac, tac_, (_, ist)): single) :: tacis) = 
walther@59908
    65
    ((tac, tac_, ((p, Pos.Res), ist)): single) :: (insert_pos (Pos.lev_on p) tacis)
walther@59908
    66
walther@59908
    67
(**)end(**)
walther@59908
    68