(* 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

   val applicable_in : Ctree.pos' -> Ctree.ctree -> Tac.tac -> Chead.appl

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

   val tac2tac_ : Ctree.ctree -> Ctree.pos' -> Tac.tac -> Tac.tac_

 (*/-------------------------------------------------------- ! 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

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

     (rew_ord', erls, ca)

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

     (rew_ord', erls, ca)

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

     (rew_ord', erls, ca)

   | rew_info rls = error ("rew_info called with '" ^ Celem.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 ^ "'", "", ("", Celem.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 ^ "'", "", ("", Celem.e_evalfn))

 		  end

   end;

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

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

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

     (Celem.e_term, if pred <> Const ("Script.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 ("Script.Assumptions", HOLogic.boolT)

   		  then [pred] 

   	    else get_assumptions_ pt (p, Res)

     in (bdv, pred) end

   | mk_set _ _ _ l _ = 

     error ("check_elementwise: no set " ^ Celem.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;

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

    additionally used by next_tac in the script-interpreter for script-tacs.

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

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

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

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

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

       then Chead.Notappl ((Tac.tac2str Tac.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 Chead.Appl (Tac.Model_Problem' (pI', pbl, [])) end

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

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

       then Chead.Notappl ((Tac.tac2str (Tac.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 => 

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

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

         end

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

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

     then Chead.Notappl ((Tac.tac2str (Tac.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' = Celem.e_domID then dI else dI';

       in

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

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

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

       	   if pI' = pI

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

       	   else Chead.Appl (Tac.Refine_Problem' rf)

     end

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

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

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

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

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

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

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

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

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

     else Chead.Appl (Tac.Del_Given' ct')

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

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

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

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

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

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

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

     else Chead.Appl (Tac.Del_Find' ct')

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

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

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

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

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

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

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

     else Chead.Appl (Tac.Del_Relation' ct')

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

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

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

     else Chead.Appl (Tac.Specify_Theory' dI)

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

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

     then Chead.Notappl ((Tac.tac2str (Tac.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' = Celem.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

         Chead.Appl (Tac.Specify_Problem' (pID, pbl))

       end

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

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

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

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

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

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

     then Chead.Notappl ((Tac.tac2str (Tac.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 is_e_ctxt ctxt

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

           else ctxt

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

        and then decide on Chead.Notappl/Appl accordingly once more.

        Implement after all tests are running, since this changes

        overall system behavior*)

     in

       Chead.Appl (Tac.Apply_Method' (mI, NONE, Selem.e_istate (*filled in solve*), ctxt))

     end

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

       if member op = [Pbl, Met] p_                  

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

       else Chead.Appl (Tac.Check_Postcond' (pI, (Celem.e_term, [(*fun solve assigns returnvalue of scr*)])))

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

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

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

     if member op = [Pbl, Met] p_ 

     then Chead.Notappl ((Tac.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 (Celem.assoc_rew_ord ro') erls false subst (snd thm'') f of

             SOME (f',asm) =>

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

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

         end

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

       end

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

     if member op = [Pbl, Met] p_ 

     then Chead.Notappl ((Tac.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 (Celem.assoc_rew_ord ro) rls' false (snd thm'') f of

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

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

         else Chead.Notappl msg

       end

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

     if member op = [Pbl, Met] p_ 

     then Chead.Notappl ((Tac.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 (Celem.assoc_rew_ord ro') erls false (snd thm'') f of

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

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

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

     if member op = [Pbl, Met] p_ 

     then Chead.Notappl ((Tac.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)

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

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

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

       end

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

     if member op = [Pbl, Met] p_ 

     then Chead.Notappl ((Tac.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)

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

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

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

       end

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

     if member op = [Pbl, Met] p_ 

     then Chead.Notappl (Tac.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)

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

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

       end

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

     if member op = [Pbl, Met] p_ 

     then Chead.Notappl (Tac.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) => Chead.Appl (Tac.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))

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

     	end

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

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

     if member op = [Pbl, Met] p_

     then Chead.Notappl ((Tac.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))

     	        => Chead.Appl (Tac.Calculate' (thy', op_, f, (f', (id, Celem.string_of_thmI thm))))

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

         else Chead.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 Tac.Substitute sube) = 

       if member op = [Pbl, Met] p_ 

       then Chead.Notappl (Tac.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 = Celem.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 Chead.Notappl (Selem.sube2str sube^" not applicable")

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

 		        end

 		      else (*2*)

 		        case Rewrite.rewrite_terms_ thy ro erls subte f of

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

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

 		    end

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

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

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

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

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

   | applicable_in (p, p_) pt (m as Tac.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 _ => 

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

 					    Celem.e_term, [], Selem.e_ctxt(*FIXME.WN150511*), LTool.subpbl domID pblID))

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

      else (*somewhere later in the script*)

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

 			   Celem.e_term, [], Selem.e_ctxt, LTool.subpbl domID pblID))

   | applicable_in _ _ (Tac.End_Subproblem) =

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

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

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

   | applicable_in _ _ (Tac.Split_And) = 

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

   | applicable_in _ _ (Tac.Conclude_And) = 

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

   | applicable_in _ _ (Tac.Split_Or) = 

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

   | applicable_in _ _ (Tac.Conclude_Or) = 

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

   | applicable_in (p, p_) pt (Tac.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 (Chead.Appl (Tac.Begin_Trans' f))

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

     end

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

     if p_ = Res 

 	  then Chead.Appl (Tac.End_Trans' (get_obj g_result pt p))

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

   | applicable_in _ _ (Tac.Begin_Sequ) = 

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

   | applicable_in _ _ (Tac.End_Sequ) = 

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

   | applicable_in _ _ (Tac.Split_Intersect) = 

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

   | applicable_in _ _ (Tac.End_Intersect) = 

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

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

     if member op = [Pbl,Met] p_ 

     then Chead.Notappl ((Tac.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 = (Celem.thy2ctxt thy, pred) |-> TermC.parseNEW |> the |> mk_set thy pt p f;

       in case f of

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

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

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

           Chead.Appl (Tac.Check_elementwise' (f, pred, (f,asm)))

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

           Chead.Appl (Tac.Check_elementwise' (f, pred, (f, asm)))

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

       end

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

     if member op = [Pbl, Met] p_ 

     then Chead.Notappl ((Tac.tac2str Tac.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 = or2list f

           in Chead.Appl (Tac.Or_to_List' (f, ls)) end) 

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

       end

   | applicable_in _ _ Tac.Collect_Trues = 

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

   | applicable_in _ _ Tac.Empty_Tac = Chead.Notappl "Empty_Tac is not applicable"

   | applicable_in (p, p_) pt (Tac.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 Chead.Appl (Tac.Tac_ (thy, Celem.term2str f, id, "subproblem_equation_dummy (" ^ Celem.term2str f ^ ")"))

   	  else Chead.Notappl "applicable only to equations made explicit"

     | "solve_equation_dummy" =>

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

   	  in

   	    if id' <> "subproblem_equation_dummy"

   	    then Chead.Notappl "no subproblem"

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

   		    then Chead.Appl (Tac.Tac_ (thy, Celem.term2str f, id, "[" ^ f' ^ "]"))

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

       end

     | _ => Chead.Appl (Tac.Tac_ (thy, Celem.term2str f, id, Celem.term2str f))

     end

   | applicable_in _ _ Tac.End_Proof' = Chead.Appl Tac.End_Proof''

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

 fun tac2tac_ pt p m = 

   case applicable_in p pt m of

 	  Chead.Appl m' => m' 

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

 end;