(* Title:  Is a tacitc applicable ?

           TODO: allocate these functions in appropriate structures

   Author: Walther Neuper

   (c) due to copyright terms

*)

signature APPLICABLE =

sig

  exception PTREE of string

  datatype appl = Appl of Tactic.T | Notappl of string

  val applicable_in : Ctree.pos' -> Ctree.ctree -> Tactic.input -> appl

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  val tac2tac_ : Ctree.ctree -> Ctree.pos' -> Tactic.input -> Tactic.T

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

  val mk_set : 'a -> ctree -> pos -> term -> term -> term * term list

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

end

(**)

structure Applicable(**): APPLICABLE(**) =

struct

(**)

open Ctree

open Pos

fun rew_info (Rule.Rls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =

    (rew_ord', erls, ca)

  | rew_info (Rule.Seq {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =

    (rew_ord', erls, ca)

  | rew_info (Rule.Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =

    (rew_ord', erls, ca)

  | rew_info rls = error ("rew_info called with '" ^ Rule.rls2str rls ^ "'");

(*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*)

fun from_pblobj_or_detail_thm _ p pt = 

  let 

    val (pbl, p', rls') = par_pbl_det pt p

  in 

    if pbl

    then 

      let 

        val thy' = get_obj g_domID pt p'

        val {rew_ord', erls, ...} = Specify.get_met (get_obj g_metID pt p')              

	    in ("OK", thy', rew_ord', erls, false) end

     else 

      let

        val thy' = get_obj g_domID pt (par_pblobj pt p)

		    val (rew_ord', erls, _) = rew_info rls'

		  in ("OK", thy', rew_ord', erls, false) end

  end;

(*FIXME.3.4.03:re-organize from_pblobj_or_detail_calc after rls' --> rls*)

fun from_pblobj_or_detail_calc scrop p pt = 

  let

    val (pbl, p', rls') = par_pbl_det pt p

  in

    if pbl

    then

      let

        val thy' = get_obj g_domID pt p'

        val {calc = scr_isa_fns, ...} = Specify.get_met (get_obj g_metID pt p')

        val opt = assoc (scr_isa_fns, scrop)

	    in

	      case opt of

	        SOME isa_fn => ("OK", thy', isa_fn)

	      | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Rule.e_evalfn))

	    end

    else 

		  let

		    val thy' = get_obj g_domID pt (par_pblobj pt p);

		    val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)

		  in

		    case assoc (scr_isa_fns, scrop) of

		      SOME isa_fn => ("OK",thy',isa_fn)

		    | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Rule.e_evalfn))

		  end

  end;

(*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*)

fun mk_set _(*thy*) _ _ (Const ("List.list.Nil", _)) _ = (Rule.e_term, [])

  | mk_set _ pt p (Const ("ListC.UniversalList", _)) pred =

    (Rule.e_term, if pred <> Const ("Prog_Tac.Assumptions", HOLogic.boolT)

	     then [pred] 

	     else get_assumptions_ pt (p, Res))

  | mk_set _ pt p (Const ("List.list.Cons",_) $ eq $ _) pred =

    let

      val (bdv,_) = HOLogic.dest_eq eq;

      val pred = if pred <> Const ("Prog_Tac.Assumptions", HOLogic.boolT)

  		  then [pred] 

  	    else get_assumptions_ pt (p, Res)

    in (bdv, pred) end

  | mk_set _ _ _ l _ = 

    error ("check_elementwise: no set " ^ Rule.term2str l);

(* check a list (/set) of constants [c_1,..,c_n] for c_i:set (: in)*)

fun check_elementwise thy erls all_results (bdv, asm) =

  let   (*bdv extracted from ~~~~~~~~~~~ in mk_set already*)

	  fun check sub =

	    let val inst_ = map (subst_atomic [sub]) asm

	    in case Rewrite.eval__true thy 1 inst_ [] erls of

		    (asm', true) => ([HOLogic.mk_eq sub], asm')

		  | (_, false) => ([],[])

	    end;

  	val c' = TermC.isalist2list all_results

  	val c'' = map (snd o HOLogic.dest_eq) c' (*assumes [x=1,x=2,..]*)

  	val subs = map (pair bdv) c''

  in

    if asm = []

    then (all_results, [])

    else ((apfst ((TermC.list2isalist HOLogic.boolT) o flat)) o (apsnd flat) o split_list o (map check)) subs

  end;

(* for Tac-dummies in root-equ only: skip str until "("*)

fun split_dummy str = 

  let

    fun scan s' [] = (implode s', "")

      | scan s' (s :: ss) = if s = " " then (implode s', implode  ss)

			  else scan (s' @ [s]) ss;

  in ((scan []) o Symbol.explode) str end;

datatype appl =

  Appl of Tactic.T      (* tactic is applicable at a certain position in the Ctree *)

| Notappl of string     (* tactic is NOT applicable                                *)

(* applicability of a tacic wrt. a calc-state (ctree, pos').

   additionally used by determine_next_tactic.

   tests for applicability are so expensive, that results (rewrites!)

   are kept in the return-value of 'type tac_'                            *)

fun applicable_in _ _ (Tactic.Init_Proof (ct', spec)) = Appl (Tactic.Init_Proof' (ct', spec))

  | applicable_in (p, p_) pt Tactic.Model_Problem = 

      if not (is_pblobj (get_obj I pt p)) orelse p_ = Res

      then Notappl ((Tactic.tac2str Tactic.Model_Problem) ^ " not for pos " ^ (pos'2str (p, p_)))

      else 

        let 

          val pI' = case get_obj I pt p of

            PblObj {origin = (_, (_, pI', _),_), ...} => pI'

          | _ => error "applicable_in Init_Proof: uncovered case get_obj"

	        val {ppc, ...} = Specify.get_pbt pI'

	        val pbl = Generate.init_pbl ppc

        in Appl (Tactic.Model_Problem' (pI', pbl, [])) end

  | applicable_in (p, p_) pt (Tactic.Refine_Tacitly pI) = 

      if not (is_pblobj (get_obj I pt p)) orelse p_ = Res

      then Notappl ((Tactic.tac2str (Tactic.Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p, p_)))

      else 

        let 

          val oris = case get_obj I pt p of

            PblObj {origin = (oris, _, _), ...} => oris

          | _ => error "applicable_in Refine_Tacitly: uncovered case get_obj"

        in

          case Specify.refine_ori oris pI of

	          SOME pblID => 

	            Appl (Tactic.Refine_Tacitly' (pI, pblID, Rule.e_domID, Celem.e_metID, [](*filled in specify*)))

	        | NONE => Notappl ((Tactic.tac2str (Tactic.Refine_Tacitly pI)) ^ " not applicable")

        end

  | applicable_in (p, p_) pt (Tactic.Refine_Problem pI) = 

    if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

    then Notappl ((Tactic.tac2str (Tactic.Refine_Problem pI)) ^ " not for pos "^(pos'2str (p, p_)))

    else

      let

        val (dI, dI', itms) = case get_obj I pt p of

            PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...}

              => (dI, dI', itms)

          | _ => error "applicable_in Refine_Problem: uncovered case get_obj"

      	val thy = if dI' = Rule.e_domID then dI else dI';

      in

        case Specify.refine_pbl (Celem.assoc_thy thy) pI itms of

          NONE => Notappl ((Tactic.tac2str (Tactic.Refine_Problem pI)) ^ " not applicable")

	      | SOME (rf as (pI', _)) =>

      	   if pI' = pI

      	   then Notappl ((Tactic.tac2str (Tactic.Refine_Problem pI)) ^ " not applicable")

      	   else Appl (Tactic.Refine_Problem' rf)

    end

  (*the specify-tacs have cterm' instead term: parse+error here!!!: see appl_add*)  

  | applicable_in (p, p_) pt (Tactic.Add_Given ct') = 

    if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

    then Notappl ((Tactic.tac2str (Tactic.Add_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))

    else Appl (Tactic.Add_Given' (ct', [(*filled in specify_additem*)]))

      (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)

  | applicable_in (p, p_) pt (Tactic.Del_Given ct') =

    if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

    then Notappl ((Tactic.tac2str (Tactic.Del_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))

    else Appl (Tactic.Del_Given' ct')

  | applicable_in (p, p_) pt (Tactic.Add_Find ct') =                   

    if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

    then Notappl ((Tactic.tac2str (Tactic.Add_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))

    else Appl (Tactic.Add_Find' (ct', [(*filled in specify_additem*)]))

  | applicable_in (p, p_) pt (Tactic.Del_Find ct') =

    if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

    then Notappl ((Tactic.tac2str (Tactic.Del_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))

    else Appl (Tactic.Del_Find' ct')

  | applicable_in (p, p_) pt (Tactic.Add_Relation ct') =               

    if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

    then Notappl ((Tactic.tac2str (Tactic.Add_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))

    else Appl (Tactic.Add_Relation' (ct', [(*filled in specify_additem*)]))

  | applicable_in (p, p_) pt (Tactic.Del_Relation ct') =

    if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

    then Notappl ((Tactic.tac2str (Tactic.Del_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))

    else Appl (Tactic.Del_Relation' ct')

  | applicable_in (p, p_) pt (Tactic.Specify_Theory dI) =              

    if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

    then Notappl ((Tactic.tac2str (Tactic.Specify_Theory dI)) ^ " not for pos " ^ pos'2str (p, p_))

    else Appl (Tactic.Specify_Theory' dI)

  | applicable_in (p, p_) pt (Tactic.Specify_Problem pID) = 

    if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

    then Notappl ((Tactic.tac2str (Tactic.Specify_Problem pID)) ^ " not for pos " ^ pos'2str (p, p_))

    else

      let

		    val (oris, dI, pI, dI', pI', itms) = case get_obj I pt p of

		      PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}

		        => (oris, dI, pI, dI', pI', itms)

        | _ => error "applicable_in Specify_Problem: uncovered case get_obj"

	      val thy = Celem.assoc_thy (if dI' = Rule.e_domID then dI else dI');

        val {ppc, where_, prls, ...} = Specify.get_pbt pID;

        val pbl = if pI' = Celem.e_pblID andalso pI = Celem.e_pblID

          then (false, (Generate.init_pbl ppc, []))

          else Specify.match_itms_oris thy itms (ppc, where_, prls) oris;

       in

        Appl (Tactic.Specify_Problem' (pID, pbl))

      end

  | applicable_in (p, p_) pt (Tactic.Specify_Method mID) =              

    if not (is_pblobj (get_obj I pt p)) orelse p_ = Res               

    then Notappl ((Tactic.tac2str (Tactic.Specify_Method mID)) ^ " not for pos " ^ pos'2str (p, p_))

    else Appl (Tactic.Specify_Method' (mID, [(*filled in specify*)], [(*filled in specify*)]))

  | applicable_in (p, p_) pt (Tactic.Apply_Method mI) =                

    if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

    then Notappl ((Tactic.tac2str (Tactic.Apply_Method mI)) ^ " not for pos " ^ pos'2str (p, p_))

    else

      let

        val (dI, pI, probl, ctxt) = case get_obj I pt p of

          PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)

        | _ => error "applicable_in Apply_Method: uncovered case get_obj"

        val {where_, ...} = Specify.get_pbt pI

        val pres = map (Model.mk_env probl |> subst_atomic) where_

        val ctxt = if ContextC.is_e_ctxt ctxt

          then Celem.assoc_thy dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres

          else ctxt

       (*TODO.WN110416 here do evalprecond according to fun check_preconds'

       and then decide on Notappl/Appl accordingly once more.

       Implement after all tests are running, since this changes

       overall system behavior*)

    in

      Appl (Tactic.Apply_Method' (mI, NONE, Istate_Def.e_istate (*filled in solve*), ctxt))

    end

  | applicable_in (p, p_) _ (Tactic.Check_Postcond pI) =

      if member op = [Pbl, Met] p_                  

      then Notappl ((Tactic.tac2str (Tactic.Check_Postcond pI)) ^ " not for pos " ^ pos'2str (p, p_))

      else Appl (Tactic.Check_Postcond' (pI, (Rule.e_term, [(*fun solve assigns returnvalue of scr*)])))

  | applicable_in _ _ (Tactic.Take str) = Appl (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)

  | applicable_in _ _ (Tactic.Free_Solve) = Appl (Tactic.Free_Solve')        (* always applicable *)

  | applicable_in (p, p_) pt (m as Tactic.Rewrite_Inst (subs, thm'')) = 

    if member op = [Pbl, Met] p_ 

    then Notappl ((Tactic.tac2str m)^" not for pos " ^ pos'2str (p, p_))

    else

      let 

        val pp = par_pblobj pt p;

        val thy' = get_obj g_domID pt pp;

        val thy = Celem.assoc_thy thy';

        val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (get_obj g_metID pt pp);

        val (f, _) = case p_ of (*p 12.4.00 unnecessary*)

                      Frm => (get_obj g_form pt p, p)

                    | Res => ((fst o (get_obj g_result pt)) p, lev_on p)

                    | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));

      in 

        let

          val subst = Selem.subs2subst thy subs;

        in

          case Rewrite.rewrite_inst_ thy (Rule.assoc_rew_ord ro') erls false subst (snd thm'') f of

            SOME (f',asm) =>

              Appl (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))

          | NONE => Notappl ((fst thm'')^" not applicable")

        end

        handle _ => Notappl ("syntax error in "^(subs2str subs))

      end

  | applicable_in (p, p_) pt (m as Tactic.Rewrite thm'') = 

    if member op = [Pbl, Met] p_ 

    then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p, p_)))

    else

      let

        val (msg, thy', ro, rls', _)= from_pblobj_or_detail_thm thm'' p pt;

        val thy = Celem.assoc_thy thy';

        val f = case p_ of

          Frm => get_obj g_form pt p

	      | Res => (fst o (get_obj g_result pt)) p

	      | _ => error ("applicable_in Rewrite: call by " ^ pos'2str (p, p_));

      in

        if msg = "OK" 

        then

          case Rewrite.rewrite_ thy (Rule.assoc_rew_ord ro) rls' false (snd thm'') f of

            SOME (f',asm) => Appl (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))

          | NONE => Notappl ("'" ^ fst thm'' ^"' not applicable") 

        else Notappl msg

      end

  | applicable_in (p, p_) pt (m as Tactic.Rewrite_Asm thm'') = 

    if member op = [Pbl, Met] p_ 

    then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p,p_)))

    else

      let 

        val pp = par_pblobj pt p; 

        val thy' = get_obj g_domID pt pp;

        val thy = Celem.assoc_thy thy';

        val {rew_ord'=ro',erls=erls,...} = Specify.get_met (get_obj g_metID pt pp);

        val (f, _) = case p_ of

          Frm => (get_obj g_form pt p, p)

	      | Res => ((fst o (get_obj g_result pt)) p, lev_on p)

	      | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));

      in

        case Rewrite.rewrite_ thy (Rule.assoc_rew_ord ro') erls false (snd thm'') f of

          SOME (f',asm) => Appl (Tactic.Rewrite' (thy', ro', erls, false, thm'', f, (f', asm)))

        | NONE => Notappl ("'" ^ fst thm'' ^ "' not applicable") end

  | applicable_in (p, p_) pt (m as Tactic.Detail_Set_Inst (subs, rls)) = 

    if member op = [Pbl, Met] p_ 

    then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p, p_)))

    else

      let 

        val pp = par_pblobj pt p;

        val thy' = get_obj g_domID pt pp;

        val thy = Celem.assoc_thy thy';

        val f = case p_ of Frm => get_obj g_form pt p

    		| Res => (fst o (get_obj g_result pt)) p

    		| _ => error ("applicable_in: call by " ^ pos'2str (p, p_));

        val subst = Selem.subs2subst thy subs

      in 

        case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of

          SOME (f', asm)

            => Appl (Tactic.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))

        | NONE => Notappl (rls ^ " not applicable")

        handle _ => Notappl ("syntax error in " ^ subs2str subs)

      end

  | applicable_in (p, p_) pt (m as Tactic.Rewrite_Set_Inst (subs, rls)) = 

    if member op = [Pbl, Met] p_ 

    then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p,p_)))

    else

      let 

        val pp = par_pblobj pt p;

        val thy' = get_obj g_domID pt pp;

        val thy = Celem.assoc_thy thy';

        val (f, _) = case p_ of

          Frm => (get_obj g_form pt p, p)

    	  | Res => ((fst o (get_obj g_result pt)) p, lev_on p)

    	  | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));

    	  val subst = Selem.subs2subst thy subs;

      in 

        case Rewrite.rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of

          SOME (f',asm)

            => Appl (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))

        | NONE => Notappl (rls ^ " not applicable")

        handle _ => Notappl ("syntax error in " ^(subs2str subs))

      end

  | applicable_in (p, p_) pt (m as Tactic.Rewrite_Set rls) = 

    if member op = [Pbl, Met] p_ 

    then Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))

    else

      let 

        val pp = par_pblobj pt p; 

        val thy' = get_obj g_domID pt pp;

        val (f, _) = case p_ of

          Frm => (get_obj g_form pt p, p)

    	  | Res => ((fst o (get_obj g_result pt)) p, lev_on p)

    	  | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));

      in

        case Rewrite.rewrite_set_ (Celem.assoc_thy thy') false (assoc_rls rls) f of

          SOME (f', asm)

            => Appl (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))

          | NONE => Notappl (rls ^ " not applicable")

      end

  | applicable_in (p, p_) pt (m as Tactic.Detail_Set rls) =

    if member op = [Pbl, Met] p_ 

    then Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))

    else

    	let

    	  val pp = par_pblobj pt p 

    	  val thy' = get_obj g_domID pt pp

    	  val f = case p_ of

    			Frm => get_obj g_form pt p

    		| Res => (fst o (get_obj g_result pt)) p

    		| _ => error ("applicable_in: call by " ^ pos'2str (p, p_));

    	in

    	  case Rewrite.rewrite_set_ (Celem.assoc_thy thy') false (assoc_rls rls) f of

    	    SOME (f',asm) => Appl (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))

    	  | NONE => Notappl (rls^" not applicable")

    	end

  | applicable_in _ _ Tactic.End_Ruleset = error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.End_Ruleset)

  | applicable_in (p, p_) pt (m as Tactic.Calculate op_) = 

    if member op = [Pbl, Met] p_

    then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p,p_)))

    else

      let 

        val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;

        val f = case p_ of

          Frm => get_obj g_form pt p

    	  | Res => (fst o (get_obj g_result pt)) p

      	| _ => error ("applicable_in: call by " ^ pos'2str (p, p_));

      in

        if msg = "OK"

        then

    	    case Rewrite.calculate_ (Celem.assoc_thy thy') isa_fn f of

    	      SOME (f', (id, thm))

    	        => Appl (Tactic.Calculate' (thy', op_, f, (f', (id, Rule.string_of_thmI thm))))

    	    | NONE => Notappl ("'calculate "^op_^"' not applicable") 

        else Notappl msg

      end

    (*Substitute combines two different kind of "substitution":

      (1) subst_atomic: for ?a..?z

      (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)

  | applicable_in (p, p_) pt (m as Tactic.Substitute sube) = 

      if member op = [Pbl, Met] p_ 

      then Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))

      else 

        let

          val pp = par_pblobj pt p

          val thy = Celem.assoc_thy (get_obj g_domID pt pp)

          val f = case p_ of

		        Frm => get_obj g_form pt p

		      | Res => (fst o (get_obj g_result pt)) p

      	  | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));

		      val {rew_ord',erls,...} = Specify.get_met (get_obj g_metID pt pp)

		      val subte = Selem.sube2subte sube

		      val subst = Selem.sube2subst thy sube

		      val ro = Rule.assoc_rew_ord rew_ord'

		    in

		      if foldl and_ (true, map TermC.contains_Var subte)

		      then (*1*)

		        let val f' = subst_atomic subst f

		        in if f = f'

		          then Notappl (Selem.sube2str sube^" not applicable")

		          else Appl (Tactic.Substitute' (ro, erls, subte, f, f'))

		        end

		      else (*2*)

		        case Rewrite.rewrite_terms_ thy ro erls subte f of

		          SOME (f', _) =>  Appl (Tactic.Substitute' (ro, erls, subte, f, f'))

		        | NONE => Notappl (Selem.sube2str sube ^ " not applicable")

		    end

  | applicable_in _ _ (Tactic.Apply_Assumption cts') = 

    error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.Apply_Assumption cts'))

    (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *)

  | applicable_in _ _ (Tactic.Take_Inst ct') =

    error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.Take_Inst ct'))

  | applicable_in (p, p_) pt (m as Tactic.Subproblem (domID, pblID)) = 

     if member op = [Pbl,Met] p_

     then (*maybe Apply_Method has already been done FIXME.WN150511: declare_constraints*)

	      case get_obj g_env pt p of

	        SOME _ => 

            Appl (Tactic.Subproblem' ((domID, pblID, Celem.e_metID), [], 

					    Rule.e_term, [], ContextC.e_ctxt(*init. in Subproblem'*), Auto_Prog.subpbl domID pblID))

	      | NONE => Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p,p_))

     else (*somewhere later in the script*)

       Appl (Tactic.Subproblem' ((domID, pblID, Celem.e_metID), [], 

			   Rule.e_term, [], ContextC.e_ctxt, Auto_Prog.subpbl domID pblID))

  | applicable_in _ _ (Tactic.End_Subproblem) =

    error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.End_Subproblem)

  | applicable_in _ _ (Tactic.CAScmd ct') = 

    error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.CAScmd ct'))  

  | applicable_in _ _ (Tactic.Split_And) = 

    error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.Split_And)

  | applicable_in _ _ (Tactic.Conclude_And) = 

    error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.Conclude_And)

  | applicable_in _ _ (Tactic.Split_Or) = 

    error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.Split_Or)

  | applicable_in _ _ (Tactic.Conclude_Or) = 

    error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.Conclude_Or)

  | applicable_in (p, p_) pt (Tactic.Begin_Trans) =

    let

      val (f, _) = case p_ of   (*p 12.4.00 unnecessary, implizit Take in gen*)

        Frm => (get_obj g_form pt p, (lev_on o lev_dn) p)

      | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p)

      | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));

    in (Appl (Tactic.Begin_Trans' f))

      handle _ => error ("applicable_in: Begin_Trans finds  syntaxerror in '" ^ Rule.term2str f ^ "'")

    end

  | applicable_in (p, p_) pt (Tactic.End_Trans) = (*TODO: check parent branches*)

    if p_ = Res 

	  then Appl (Tactic.End_Trans' (get_obj g_result pt p))

    else Notappl "'End_Trans' is not applicable at the beginning of a transitive sequence"

  | applicable_in _ _ (Tactic.Begin_Sequ) = 

    error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.Begin_Sequ))

  | applicable_in _ _ (Tactic.End_Sequ) = 

    error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.End_Sequ))

  | applicable_in _ _ (Tactic.Split_Intersect) = 

    error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.Split_Intersect))

  | applicable_in _ _ (Tactic.End_Intersect) = 

    error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.End_Intersect))

  | applicable_in (p, p_) pt (m as Tactic.Check_elementwise pred) = 

    if member op = [Pbl, Met] p_ 

    then Notappl ((Tactic.tac2str m) ^ " not for pos " ^ pos'2str (p, p_))

    else

      let 

        val pp = par_pblobj pt p; 

        val thy' = get_obj g_domID pt pp;

        val thy = Celem.assoc_thy thy'

        val metID = (get_obj g_metID pt pp)

        val {crls, ...} =  Specify.get_met metID

        val (f, asm) = case p_ of

          Frm => (get_obj g_form pt p , [])

        | Res => get_obj g_result pt p

        | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));

        val vp = (Rule.thy2ctxt thy, pred) |-> TermC.parseNEW |> the |> mk_set thy pt p f;

      in case f of

        Const ("List.list.Cons", _) $ _ $ _ =>

          Appl (Tactic.Check_elementwise' (f, pred, check_elementwise thy crls f vp))

      | Const ("ListC.UniversalList", _) => 

          Appl (Tactic.Check_elementwise' (f, pred, (f,asm)))

      | Const ("List.list.Nil", _) => 

          Appl (Tactic.Check_elementwise' (f, pred, (f, asm)))

      | _ => Notappl ("Check_elementwise not appl.: " ^ Rule.term2str f ^ " should be constants")

      end

  | applicable_in (p, p_) pt Tactic.Or_to_List = 

    if member op = [Pbl, Met] p_ 

    then Notappl ((Tactic.tac2str Tactic.Or_to_List)^" not for pos "^(pos'2str (p,p_)))

    else

      let 

        val f = case p_ of

          Frm => get_obj g_form pt p

    	  | Res => (fst o (get_obj g_result pt)) p

        | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));

      in (let val ls = Prog_Expr.or2list f

          in Appl (Tactic.Or_to_List' (f, ls)) end) 

         handle _ => Notappl ("'Or_to_List' not applicable to " ^ Rule.term2str f)

      end

  | applicable_in _ _ Tactic.Collect_Trues = 

    error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.Collect_Trues)

  | applicable_in _ _ Tactic.Empty_Tac = Notappl "Empty_Tac is not applicable"

  | applicable_in (p, p_) pt (Tactic.Tac id) =

    let 

      val pp = par_pblobj pt p; 

      val thy' = get_obj g_domID pt pp;

      val thy = Celem.assoc_thy thy';

      val f = case p_ of

         Frm => get_obj g_form pt p

      | Pbl => error "applicable_in (p,Pbl) pt (Tac id): not at Pbl"

  	  | Res => (fst o (get_obj g_result pt)) p

      | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));

    in case id of

      "subproblem_equation_dummy" =>

  	  if TermC.is_expliceq f

  	  then Appl (Tactic.Tac_ (thy, Rule.term2str f, id, "subproblem_equation_dummy (" ^ Rule.term2str f ^ ")"))

  	  else Notappl "applicable only to equations made explicit"

    | "solve_equation_dummy" =>

  	  let val (id', f') = split_dummy (Rule.term2str f);

  	  in

  	    if id' <> "subproblem_equation_dummy"

  	    then Notappl "no subproblem"

  	    else if (Rule.thy2ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq

  		    then Appl (Tactic.Tac_ (thy, Rule.term2str f, id, "[" ^ f' ^ "]"))

  		    else error ("applicable_in: f= " ^ f')

      end

    | _ => Appl (Tactic.Tac_ (thy, Rule.term2str f, id, Rule.term2str f))

    end

  | applicable_in _ _ Tactic.End_Proof' = Appl Tactic.End_Proof''

  | applicable_in _ _ m = error ("applicable_in called for " ^ Tactic.tac2str m);

fun tac2tac_ pt p m = 

  case applicable_in p pt m of

	  Appl m' => m' 

  | Notappl _ => error ("tac2mstp': fails with" ^ Tactic.tac2str m);

end;