(* 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 (p,p_) =

     if Pos.on_specification p_ 

     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 = Method.id_empty then (thd3 o snd3) (get_obj g_origin pt pp) else metID

         val (sc, srls) = (case Specify.get_met 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 (p, p_) =

     if Pos.on_specification p_ 

     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 = Method.id_empty 

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

           else metID

         val (sc, srls, erls, ro) = (case Specify.get_met 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

         ((gen_distinct Tactic.eq_tac) o flat o (map (Tactic.applicable thy ro erls f))) alltacs

       end;

 (**)end(**)