(* Title:  MathEngine/fetch-tactics.sml

   Author: Walther Neuper

   (c) due to copyright terms

Fetch tactics from a program in order to present them for selection by the user

*)

signature FETCH_TACTICS =

sig

  val from_prog : Ctree.ctree -> Pos.pos' -> Tactic.input list 

  val specific_from_prog : Ctree.ctree -> Pos.pos' -> Tactic.input list

end

(**)

structure Fetch_Tacs(**): FETCH_TACTICS(**) =

struct

(**)

open Ctree

open Pos

(* fetch _all_ tactics from a program *)

fun from_prog _ ([], Res) = 

    raise PTREE "no tactics applicable at the end of a calculation"

  | from_prog pt (pos as (p, p_)) =

    if Pos.on_specification pos 

    then [get_obj g_tac pt p]

    else

      let

        val pp = par_pblobj pt p;

        val thy' = get_obj g_domID pt pp;

        val thy = ThyC.get_theory thy';

        val metID = get_obj g_metID pt pp;

        val metID' = if metID = MethodC.id_empty then (thd3 o snd3) (get_obj g_origin pt pp) else metID

        val (sc, srls) = (case MethodC.from_store metID' of

            {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => raise ERROR "from_prog 1")

        val subst = get_istate_LI pt (p, p_) |> Istate.the_pstate |> Istate.get_subst

        val ctxt = get_ctxt pt (p, p_)

      in map ((LItool.tac_from_prog pt thy) o Program.rep_stacexpr o #1 o

  	    (LItool.check_leaf "selrul" ctxt srls subst)) (Auto_Prog.stacpbls sc)

  	  end;

(* fetch tactics from script and filter _applicable_ tactics;

   in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)

fun specific_from_prog _ (([], Res) : pos') = 

    raise PTREE "no tactics applicable at the end of a calculation"

  | specific_from_prog pt (pos as (p, p_)) =

    if Pos.on_specification pos 

    then [get_obj g_tac pt p]

    else

      let

        val pp = par_pblobj pt p

(*ctxt* )

        val thy' = get_obj g_domID pt pp

        val thy = ThyC.get_theory thy'

( **)

val ctxt = Ctree.get_loc pt pos |> snd

val thy = Proof_Context.theory_of ctxt

(**)

        val metID = get_obj g_metID pt pp

        val metID' =

          if metID = MethodC.id_empty 

          then (thd3 o snd3) (get_obj g_origin pt pp)

          else metID

        val (sc, srls, erls, ro) = (case MethodC.from_store metID' of

            {scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)

          | _ => raise ERROR "specific_from_prog 1")

        val (env, (a, v)) = (case get_istate_LI pt (p, p_) of

            Istate.Pstate pst => (Istate.get_subst pst) | _ => error "specific_from_prog 2")

        val ctxt = get_ctxt pt (p, p_)

        val alltacs = (*we expect at least 1 Prog_Tac in a program*)

          map ((LItool.tac_from_prog pt thy) o Program.rep_stacexpr o #1 o

           (LItool.check_leaf "selrul" ctxt srls (env, (a, v)))) (Auto_Prog.stacpbls sc)

        val f =

          (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p

          | _ => raise ERROR "specific_from_prog 2")

          (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)

      in

        ((distinct Tactic.eq_tac) o flat o 

          (map (Tactic.applicable (Proof_Context.init_global thy) ro erls f))) alltacs

      end;

(**)end(**)