(* tools for rewriting, reverse rewriting, context to thy concerning rewriting

   authors: Walther Neuper 2002, 2006

  (c) due to copyright terms

*)

signature REWRITE_TOOLS =

sig

  type deriv

  val contains_rule : rule -> rls -> bool

  val atomic_appl_tacs : theory -> string -> rls -> term -> tac -> tac list

  val thy_containing_rls : theory' -> rls' -> string * theory'

  val thy_containing_cal : theory' -> prog_calcID -> string * string

  datatype contthy

  = ContNOrew of {applto: term, thm_rls: guh, thyID: thyID}

     | ContNOrewInst of {applto: term, bdvs: subst, thm_rls: guh, thminst: term, thyID: thyID}

     | ContRls of {applto: term, asms: term list, result: term, rls: guh, thyID: thyID}

     | ContRlsInst of {applto: term, asms: term list, bdvs: subst, result: term, rls: guh, thyID: thyID}

     | ContThm of {applat: term, applto: term, asmrls: rls', asms: (term * term) list,

       lhs: term * term, resasms: term list, result: term, reword: rew_ord', rhs: term * term,

       thm: guh, thyID: thyID}

     | ContThmInst of {applat: term, applto: term, asmrls: rls', asms: (term * term) list,

       bdvs: subst, lhs: term * term, resasms: term list, result: term, reword: rew_ord',

       rhs: term * term, thm: guh, thminst: term, thyID: thyID}

     | EContThy

  val guh2filename : guh -> filename

  val is_sym : thmID -> bool

  val sym_drop : thmID -> thmID val sym_rls : rls -> rls

  val sym_rule : rule -> rule

  val thms_of_rls : rls -> rule list

  val theID2filename : theID -> filename

  val no_thycontext : guh -> bool

  val subs_from : istate -> 'a -> guh -> subs

  val guh2rewtac : guh -> subs -> tac

  val get_tac_checked : ptree -> pos' -> tac

  val context_thy : ptree * (pos * pos_) -> tac -> contthy

  val distinct_Thm : rule list -> rule list

  val eq_Thms : string list -> rule -> bool

  val make_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->

    term option -> term -> deriv

  val reverse_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->

    term option -> term -> (rule * (term * term list)) list

  val get_bdv_subst : term -> (term * term) list -> subs option * subst

  val thy_containing_thm : string -> string * string val thypart2filename : theID -> filename

  val guh2theID : guh -> theID

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

  val trtas2str : (term * rule * (term * term list)) list -> string

  val eq_Thm : rule * rule -> bool

  val deriv2str : (term * rule * (term * term list)) list -> string val deriv_of_thm'' : thm'' -> string

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

end 

(**)

structure Rtools(**): REWRITE_TOOLS(**) =

struct

(**)

(*** reverse rewriting ***)

(*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls       *

 *  of for connecting a user-input formula with the current calc-state.	     *

 *# It is somewhat incompatible with the rest of the math-engine:	     *

 *  (1) it is not created by a script					     *

 *  (2) thus there cannot be another user-input within a derivation	     *

 *# It suffers particularily from the not-well-foundedness of the math-engine*

 *  (1) FIXME other branchtyptes than Transitive will change 'embed_deriv'   *

 *  (2) FIXME and eventually 'compare_step' (ie. the script interpreter)     *

 *  (3) FIXME and eventually 'lev_back'                                      *

 *# SOME improvements are evident FIXME.040215 '_deriv'ation:	             *

 *  (1) FIXME nest Rls_ in 'make_deriv'					     *

 *  (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus    *

 *	user-input will become possible in this part of a derivation	     *

 *  (3) FIXME do (2) only if a derivation has been found -- for efficiency,  *

 *	while a non-derivable inform requires to step until End_Proof'	     *

 *  (4) FIXME find criteria on when _not_ to step until End_Proof'           *

 *  (5) FIXME 

.*)

type deriv =      (* derivation for insertin one level of nodes into the calctree *) 

  ( term *        (* where the rule is applied to                                 *)

    rule *        (* rule to be applied                                           *)

    ( term *      (* resulting from rule application                              *)

      term list)) (* assumptions resulting from rule application                  *)

  list            (*                                                              *) 

fun trta2str (t, r, (t', a)) =

  "\n(" ^ term2str t ^ ", " ^ rule2str' r ^ ", (" ^ term2str t' ^ ", " ^ terms2str a ^ "))"

fun trtas2str trtas = (strs2str o (map trta2str)) trtas

val deriv2str = trtas2str

fun rta2str (r, (t, a)) =

  "\n(" ^ rule2str' r ^ ", (" ^ term2str t ^ ", " ^ terms2str a ^ "))"

fun rtas2str rtas = (strs2str o (map rta2str)) rtas

val deri2str = rtas2str

(* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) 

  WN120320: reconsider the desing including the java front-end with html representation;

  see tests 

  --- OLD compute rlsthmsNOTisac by eq_thmID ---

  --- compute val rlsthmsNOTisac ---

*)

fun sym_thm thm =

  let 

    val (deriv,

      {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs, 

      prop = prop}) = Thm.rep_thm_G thm

    val (lhs, rhs) = (dest_equals' o strip_trueprop o Logic.strip_imp_concl) prop

    val prop' = case strip_imp_prems' prop of

        NONE => Trueprop $ (mk_equality (rhs, lhs))

      | SOME cs => ins_concl cs (Trueprop $ (mk_equality (rhs, lhs)))

  in Thm.assbl_thm deriv thy tags maxidx shyps hyps tpairs prop' end

(* WN100910 weaker than fun sym_thm for Theory.axioms_of in isa02 *)

fun sym_trm trm =

  let

    val (lhs, rhs) = (dest_equals' o strip_trueprop o Logic.strip_imp_concl) trm

    val trm' = case strip_imp_prems' trm of

	      NONE => mk_equality (rhs, lhs)

	    | SOME cs => ins_concl cs (mk_equality (rhs, lhs))

  in trm' end

(* derive normalform of a rls, or derive until SOME goal,

   and record rules applied and rewrites.

val it = fn

  : theory

    -> rls

    -> rule list

    -> rew_ord       : the order of this rls, which 1 theorem of is used 

                       for rewriting 1 single step (?14.4.03)

    -> term option   : 040214 ??? use for "derive until SOME goal" ??? 

    -> term 

    -> (term *       : to this term ...

        rule * 	     : ... this rule is applied yielding ...

        (term *      : ... this term ...

         term list)) : ... under these assumptions.

       list          :

returns empty list for a normal form

FIXME.WN040214: treats rules as in Rls, _not_ as in Seq

WN060825 too complicated for the intended use by cancel_, common_nominator_

and unreflectedly adapted to extension of rules by Rls_: returns Rls_("sym_simpl..

 -- replaced below *)

fun make_deriv thy erls (rs:rule list) ro goal tt = 

  let 

    datatype switch = Appl | Noap (* unify with version in rewrite.sml *)

    fun rew_once _ rts t Noap [] = 

        (case goal of NONE => rts | SOME _ => error ("make_deriv: no derivation for " ^ term2str t))

      | rew_once lim rts t Appl [] = rew_once lim rts t Noap rs

        (*| Seq _ => rts) FIXXXXXME 14.3.03*)

      | rew_once lim rts t apno rs' =

        (case goal of 

          NONE => rew_or_calc lim rts t apno rs'

        | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs')

    and rew_or_calc lim rts t apno (rrs' as (r :: rs')) =

      if lim < 0 

      then (tracing ("make_deriv exceeds " ^ int2str (! lim_deriv) ^ "with deriv =\n");

        tracing (deriv2str rts); rts)

      else

        (case r of

          Thm (thmid, tm) => 

            (if not (! trace_rewrite) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");

            case rewrite_ thy ro erls true tm t of

              NONE => rew_once lim rts t apno rs'

            | SOME (t', a') =>

              (if ! trace_rewrite then tracing ("### rewrites to: " ^ term2str t') else ();

              rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))

        | Calc (c as (op_, _)) => 

          let 

            val _ = if not (! trace_rewrite) then () else tracing ("### trying calc. \"" ^ op_^"\"")

            val t = uminus_to_string t

          in 

            case adhoc_thm thy c t of

              NONE => rew_once lim rts t apno rs'

            | SOME (thmid, tm) => 

              (let

                val (t', a') = case rewrite_ thy ro erls true tm t of

                  SOME ta => ta

                | NONE => error "adhoc_thm: NONE"

                val _ = if not (! trace_rewrite) then () else tracing("### calc. to: " ^term2str t')

                val r' = Thm (thmid, tm)

              in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end) 

                handle _ => error "derive_norm, Calc: no rewrite"

          end

      (*| Cal1 (cc as (op_,_)) => ... WN080222 see rewrite__set_: see 7df94616c1bd and earlier*)

        | Rls_ rls =>           (* WN060829: CREATES "sym_rlsID", see 7df94616c1bd and earlier*)

          (case rewrite_set_ thy true rls t of

            NONE => rew_once lim rts t apno rs'

          | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')

        | rule => error ("rew_once: uncovered case " ^ rule2str rule))

    | rew_or_calc _ _ _ _ [] = error "rew_or_calc: called with []"

  in rew_once (! lim_deriv) [] tt Noap rs : deriv end

fun sym_drop (thmID : thmID) =

  case Symbol.explode thmID of

	  "s" :: "y" :: "m" :: "_" :: id => implode id : thmID

  | _ => thmID

fun is_sym (thmID : thmID) =

  case Symbol.explode thmID of

	  "s" :: "y" :: "m" :: "_" :: _ => true

  | _ => false;

(*FIXXXXME.040219: detail has to handle Rls id="sym_..." 

  by applying make_deriv, rev_deriv'; see concat_deriv*)

fun sym_rls Erls = Erls

  | sym_rls (Rls {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =

    Rls {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls, 

      rules = rules, rew_ord = rew_ord, preconds = preconds}

  | sym_rls (Seq {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =

    Seq {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls, 

      rules = rules, rew_ord = rew_ord, preconds = preconds}

  | sym_rls (Rrls {id, scr, calc, errpatts, erls, prepat, rew_ord}) = 

    Rrls {id = "sym_" ^ id, scr = scr, calc = calc,  errpatts = errpatts, erls = erls,

      prepat = prepat, rew_ord = rew_ord}

(* toggles sym_* and keeps "#:" for ad-hoc calculations *)

fun sym_rule (Thm (thmID, thm)) =

  let

    val thm' = sym_thm thm

    val thmID' = case Symbol.explode thmID of

      "s" :: "y" :: "m" :: "_" :: id => implode id

    | "#" :: ":" :: _ => "#: " ^ string_of_thmI thm'

    | _ => "sym_" ^ thmID

  in Thm (thmID', thm') end

| sym_rule (Rls_ rls) = Rls_ (sym_rls rls) (* TODO? handle with interSteps ? *)

| sym_rule r = error ("sym_rule: not for " ^  rule2str r)

(*version for reverse rewrite used before 040214*)

fun rev_deriv (t, r, (_, a)) = (sym_rule r, (t, a));

fun reverse_deriv thy erls (rs:rule list) ro goal t =

    (rev o (map rev_deriv)) (make_deriv thy erls (rs:rule list) ro goal t)

fun eq_Thm (Thm (id1, _), Thm (id2,_)) = id1 = id2

  | eq_Thm (Thm (_, _), _) = false

  | eq_Thm (Rls_ r1, Rls_ r2) = id_rls r1 = id_rls r2

  | eq_Thm (Rls_ _, _) = false

  | eq_Thm (r1, r2) = error ("eq_Thm: called with '" ^ rule2str r1 ^ "' '"^ rule2str r2 ^ "'")

fun distinct_Thm r = gen_distinct eq_Thm r

fun eq_Thms thmIDs thm = (member op = thmIDs (id_of_thm thm))

  handle ERROR _ => false

(*** context to thy concerning rewriting ***)

(* create the unique handles and filenames for the theory-data *)

fun part2filename str = part2guh str ^ ".xml" : filename

fun thy2filename thy' = thy2guh thy' ^ ".xml" : filename

fun thypart2filename thy' = thypart2guh thy' ^ ".xml" : filename

fun thm2filename (isa_thyID: string * thyID) thmID = thm2guh isa_thyID thmID ^ ".xml" : filename

fun rls2filename (isa, thyID) rls' = rls2guh (isa, thyID) rls' ^ ".xml" : filename

fun cal2filename (isa, thyID:thyID) calID = cal2guh (isa, thyID : thyID) calID ^ ".xml" : filename

fun ord2filename (isa, thyID:thyID) (rew_ord' : rew_ord') =

  ord2guh (isa, thyID:thyID) (rew_ord' : rew_ord') ^ ".xml" : filename

fun rearrange (thyID : thyID, (thmID : thmID, thm)) = (thmID, (thyID, Thm.prop_of thm));

fun rearrange' (thmID : thmID, thm) =

  (thmID_of_derivation_name thmID,

    (thyID_of_derivation_name thmID, Thm.prop_of thm)) : (thmID * (thyID * term))

fun rearrange_inv (thmID, (thyID, term)) = (thyID, (thmID, term))

(* cheap version without sym_* thms *)

fun make_isab rlsthmsNOTisac = map rearrange' rlsthmsNOTisac;

fun thy_containing_thm thmDeriv =

  let

    val isabthys' = map Context.theory_name (isabthys ());

  in

    if member op= isabthys' (thyID_of_derivation_name thmDeriv)

    then ("Isabelle", thyID_of_derivation_name thmDeriv)

    else ("IsacKnowledge", thyID_of_derivation_name thmDeriv)

  end

(* which theory in ancestors of thy' contains a ruleset *)

fun thy_containing_rls (thy' : theory') (rls' : rls') =

  let

    val thy = Thy_Info.get_theory thy'

  in

    case AList.lookup op= (KEStore_Elems.get_rlss thy) rls' of

      SOME (thy'', _) => (partID' thy'', thy'')

    | _ => error ("thy_containing_rls : rls '" ^ rls' ^ "' not in ancestors of thy '" ^ thy' ^ "'")

  end

(* this function cannot work as long as the datastructure does not contain thy' *)

fun thy_containing_cal (thy' : theory') (sop : prog_calcID) =

  let

    val thy = Thy_Info.get_theory thy'

  in

    case AList.lookup op= (KEStore_Elems.get_calcs thy) sop of

      SOME (_(*"Groups.plus_class.plus"*), _) => ("IsacKnowledge", "Atools" (*FIXME*))

    | _ => error ("thy_containing_cal : rls '" ^ sop ^ "' not in ancestors of thy '" ^ thy' ^ "'")

  end

(* packing return-values to matchTheory, contextToThy for xml-generation *)

datatype contthy =  (*also an item from KEStore on Browser .....#*)

	EContThy   (* not from KEStore ..............................*)

  | ContThm of (* a theorem in contex ===========================*)

    {thyID   : thyID,     (* for *2guh in sub-elems here        .*)

     thm     : guh,       (* theorem in the context             .*)

     applto  : term,	  (* applied to formula ...             .*)

     applat  : term,	  (* ...  with lhs inserted             .*)

     reword  : rew_ord',  (* order used for rewrite             .*)

     asms    : (term      (* asumption instantiated             .*)

   	   * term) list,      (* asumption evaluated                .*)

     lhs     : term       (* lhs of the theorem ...             #*)

   	   * term,            (* ... instantiated                   .*)

     rhs     : term       (* rhs of the theorem ...             #*)

   	   * term,            (* ... instantiated                   .*)

     result  : term,	  (* resulting from the rewrite         .*)

     resasms : term list, (* ... with asms stored               .*)

     asmrls  : rls'       (* ruleset for evaluating asms        .*)

   	}						 

  | ContThmInst of (* a theorem with bdvs in contex ============ *)

    {thyID   : thyID,     (*for *2guh in sub-elems here         .*)

     thm     : guh,       (*theorem in the context              .*)

     bdvs    : subst,     (*bound variables to modify...        .*)

     thminst : term,      (*... theorem instantiated            .*)

     applto  : term,	  (*applied to formula ...              .*)

     applat  : term,	  (*...  with lhs inserted              .*)

     reword  : rew_ord',  (*order used for rewrite              .*)

     asms    : (term      (*asumption instantiated              .*)

   	   * term) list,      (*asumption evaluated                 .*)

     lhs     : term       (*lhs of the theorem ...              #*)

   	   * term,            (*... instantiated                    .*)

     rhs     : term       (*rhs of the theorem ...              #*)

   	   * term,            (*... instantiated                    .*)

     result  : term,	  (*resulting from the rewrite          .*)

     resasms : term list, (*... with asms stored                .*)

     asmrls  : rls'       (*ruleset for evaluating asms         .*)

    }						 

  | ContRls of (* a rule set in contex ========================= *)

    {thyID   : thyID,     (*for *2guh in sub-elems here         .*)

     rls     : guh,       (*rule set in the context             .*)

     applto  : term,	  (*rewrite this formula                .*)

     result  : term,	  (*resulting from the rewrite          .*)

     asms    : term list  (*... with asms stored                .*)

   	}						 

  | ContRlsInst of (* a rule set with bdvs in contex =========== *)

	{thyID   : thyID,     (*for *2guh in sub-elems here         .*)

	 rls     : guh,       (*rule set in the context             .*)

	 bdvs    : subst,     (*for bound variables in thms         .*)

	 applto  : term,	  (*rewrite this formula                .*)

	 result  : term,	  (*resulting from the rewrite          .*)

	 asms    : term list  (*... with asms stored                .*)

   	}						 

  | ContNOrew of (* no rewrite for thm or rls ================== *)

    {thyID   : thyID,     (*for *2guh in sub-elems here         .*)

     thm_rls : guh,       (*thm or rls in the context           .*)

     applto  : term	      (*rewrite this formula                .*)

   	}						 

  | ContNOrewInst of (* no rewrite for some instantiation ====== *)

    {thyID   : thyID,     (*for *2guh in sub-elems here         .*)

     thm_rls : guh,       (*thm or rls in the context           .*)

     bdvs    : subst,     (*for bound variables in thms         .*)

     thminst : term,      (*... theorem instantiated            .*)

     applto  : term	      (*rewrite this formula               .*)

   	}						 

(*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718

   pass other tacs unchanged.*)

fun get_tac_checked pt ((p, _) : pos') = get_obj g_tac pt p;

(* create a derivation-name, eg. ("refl", _) --> "HOL.refl"*)

fun deriv_of_thm'' ((thmID, _) : thm'') =

  thmID |> Global_Theory.get_thm (Isac ()) |> Thm.get_name_hint

(* get the formula f at ptp rewritten by the Rewrite_* already applied to f *)

fun context_thy (pt, pos as (p,p_)) (tac as Rewrite thm'') =

    let val thm_deriv = deriv_of_thm'' thm''

    in

    (case Applicable.applicable_in pos pt tac of

      Chead.Appl (Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>

        ContThm

         {thyID = theory'2thyID thy',

          thm = thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),

          applto = f, applat  = e_term, reword  = ord',

          asms = [](*asms ~~ asms'*), lhs = (e_term, e_term)(*(lhs, lhs')*), rhs = (e_term, e_term)(*(rhs, rhs')*),

          result = res, resasms = asm, asmrls  = id_rls erls}

     | Chead.Notappl _ =>

         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 "context_thy: uncovered position"

         in

           ContNOrew

            {thyID   = theory'2thyID thy',

             thm_rls = 

               thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),

             applto  = f}

		     end

     | _ => error "context_thy..Rewrite: uncovered case 2")

    end

  | context_thy (pt, pos as (p, p_)) (tac as Rewrite_Inst (subs, (thmID, _))) =

    let val thm = Global_Theory.get_thm (Isac ()) thmID

    in

	  (case Applicable.applicable_in pos pt tac of

	     Chead.Appl (Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>

	       let

           val thm_deriv = Thm.get_name_hint thm

           val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)

	       in

	         ContThmInst

	          {thyID = theory'2thyID thy',

	           thm = 

	             thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),

	           bdvs = subst, thminst = thminst, applto  = f, applat  = e_term, reword  = ord',

	           asms = [](*asms ~~ asms'*), lhs = (e_term, e_term)(*(lhs, lhs')*), rhs = (e_term, e_term)(*(rhs, rhs')*),

	           result = res, resasms = asm, asmrls  = id_rls erls}

	       end

     | Chead.Notappl _ =>

         let

           val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID

           val thm_deriv = Thm.get_name_hint thm

           val pp = par_pblobj pt p

           val thy' = get_obj g_domID pt pp

           val subst = subs2subst (assoc_thy thy') subs

           val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)

           val f = case p_ of

               Frm => get_obj g_form pt p

             | Res => (fst o (get_obj g_result pt)) p | _ => error "context_thy: uncovered case 3"

         in

           ContNOrewInst

            {thyID = theory'2thyID thy',

             thm_rls = thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),

             bdvs = subst, thminst = thminst, applto = f}

         end

      | _ => error "context_thy..Rewrite_Inst: uncovered case 4")

    end

  | context_thy (pt, p) (tac as Rewrite_Set rls') =

    (case Applicable.applicable_in p pt tac of

       Chead.Appl (Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>

         ContRls

          {thyID = theory'2thyID thy',

           rls = rls2guh (thy_containing_rls thy' rls') rls',

           applto = f, result = res, asms = asm}

     | _ => error ("context_thy Rewrite_Set: not for Chead.Notappl"))

  | context_thy (pt,p) (tac as Rewrite_Set_Inst (_(*subs*), rls')) = 

    (case Applicable.applicable_in p pt tac of

       Chead.Appl (Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>

         ContRlsInst

          {thyID = theory'2thyID thy',

           rls = rls2guh (thy_containing_rls thy' rls') rls',

           bdvs = subst, applto = f, result = res, asms = asm}

     | _ => error ("context_thy Rewrite_Set_Inst: not for Chead.Notappl"))

  | context_thy (_, p) tac =

      error ("context_thy: not for tac " ^ tac2str tac ^ " at " ^ pos'2str p)

(* get all theorems in a rule set (recursivley containing rule sets) *)

fun thm_of_rule Erule = []

  | thm_of_rule (thm as Thm _) = [thm]

  | thm_of_rule (Calc _) = []

  | thm_of_rule (Cal1 _) = []

  | thm_of_rule (Rls_ rls) = thms_of_rls rls

and thms_of_rls Erls = []

  | thms_of_rls (Rls {rules,...}) = (flat o (map  thm_of_rule)) rules

  | thms_of_rls (Seq {rules,...}) = (flat o (map  thm_of_rule)) rules

  | thms_of_rls (Rrls _) = []

(* check if a rule is contained in a rule-set (recursivley down in Rls_);

   this rule can even be a rule-set itself                             *)

fun contains_rule r rls = 

  let 

    fun (*find (_, Rls_ rls) = finds (get_rules rls)

      | find r12 = eq_rule r12

    and*) finds [] = false

    | finds (r1 :: rs) = if eq_rule (r, r1) then true else finds rs

  in 

    finds (get_rules rls) 

  end

(* try if a rewrite-rule is applicable to a given formula; 

   in case of rule-sets (recursivley) collect all _atomic_ rewrites *) 

fun try_rew thy ((_, ro) : rew_ord) erls (subst : subst) f (thm' as Thm (_, thm)) =

    if contains_bdv thm

    then case rewrite_inst_ thy ro erls false subst thm f of

	    SOME _ => [rule2tac thy subst thm']

	  | NONE => []

    else (case rewrite_ thy ro erls false thm f of

	    SOME _ => [rule2tac thy [] thm']

	  | NONE => [])

  | try_rew thy _ _ _ f (cal as Calc c) = 

    (case adhoc_thm thy c f of

	    SOME _ => [rule2tac thy [] cal]

    | NONE => [])

  | try_rew thy _ _ _ f (cal as Cal1 c) = 

    (case adhoc_thm thy c f of

	      SOME _ => [rule2tac thy [] cal]

      | NONE => [])

  | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls

  | try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"

and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules, ...}) = 

    gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))

  | filter_appl_rews thy subst f (Seq {rew_ord = ro, erls, rules,...}) = 

    gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))

  | filter_appl_rews _ _ _ (Rrls _) = []

  | filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case"

(* decide if a tactic is applicable to a given formula; 

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

fun atomic_appl_tacs thy _ _ f (Calculate scrID) =

    try_rew thy e_rew_ordX e_rls [] f (Calc (assoc_calc' thy scrID |> snd))

  | atomic_appl_tacs thy ro erls f (Rewrite thm'') =

    try_rew thy (ro, assoc_rew_ord ro) erls [] f (Thm thm'')

  | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm'')) =

    try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f (Thm thm'')

  | atomic_appl_tacs thy _ _ f (Rewrite_Set rls') =

    filter_appl_rews thy [] f (assoc_rls rls')

  | atomic_appl_tacs thy _ _ f (Rewrite_Set_Inst (subs, rls')) =

    filter_appl_rews thy (subs2subst thy subs) f (assoc_rls rls')

  | atomic_appl_tacs _ _ _ _ tac = 

    (tracing ("### atomic_appl_tacs: not impl. for tac = '" ^ tac2str tac ^ "'"); []);

(* filenames not only for thydata, but also for thy's etc *)

fun theID2filename (theID : theID) = theID2guh theID ^ ".xml" : filename

fun guh2theID (guh : guh) =

  let

    val guh' = Symbol.explode guh

    val part = implode (take_fromto 1 4 guh')

    val isa = implode (take_fromto 5 9 guh')

  in

    if not (member op = ["exp_", "thy_", "pbl_", "met_"] part)

    then raise ERROR ("guh '" ^ guh ^ "' does not begin with exp_ | thy_ | pbl_ | met_")

    else

      let

  	    val chap = case isa of

  		  "isab_" => "Isabelle"

  		| "scri_" => "IsacScripts"

  		| "isac_" => "IsacKnowledge"

  		| _ =>

  		  raise ERROR ("guh2theID: '" ^ guh ^ "' does not have isab_ | scri_ | isac_ at position 5..9")

        val rest = takerest (9, guh') 

        val thyID = takewhile [] (not o (curry op= "-")) rest

        val rest' = dropuntil (curry op = "-") rest

	    in case implode rest' of

		    "-part" => [chap] : theID

      | "" => [chap, implode thyID]

      | "-Theorems" => [chap, implode thyID, "Theorems"]

      | "-Rulesets" => [chap, implode thyID, "Rulesets"]

      | "-Operations" => [chap, implode thyID, "Operations"]

      | "-Orders" => [chap, implode thyID, "Orders"]

      | _ => 

		    let val sect = implode (take_fromto 1 5 rest')

		       val sect' = case sect of

			       "-thm-" => "Theorems"

			     | "-rls-" => "Rulesets"

			     | "-cal-" => "Operations"

			     | "-ord-" => "Orders"

			     | _ =>

			     raise ERROR ("guh2theID: '" ^ guh ^ "' has '" ^ sect ^ "' instead -thm- | -rls- | -cal- | -ord-")

		    in

		      [chap, implode thyID, sect', implode (takerest (5, rest'))]

		    end

	    end	

    end

fun guh2filename (guh : guh) = guh ^ ".xml" : filename;

fun guh2rewtac (guh : guh) ([] : subs) =

    let

      val (_, thy, sect, xstr) = case guh2theID guh of

        [isa, thy, sect, xstr] => (isa, thy, sect, xstr)

      | _ => error "guh2rewtac: uncovered case"

    in case sect of

      "Theorems" => Rewrite (xstr, assoc_thm'' (assoc_thy thy) xstr)

    | "Rulesets" => Rewrite_Set xstr

    | _ => error ("guh2rewtac: not impl. for '"^xstr^"'") 

    end

  | guh2rewtac guh subs =

    let

      val (_, thy, sect, xstr) = case guh2theID guh of

        [isa, thy, sect, xstr] => (isa, thy, sect, xstr)

      | _ => error "guh2rewtac: uncovered case"

    in case sect of

      "Theorems" => 

        Rewrite_Inst (subs, (xstr, assoc_thm'' (assoc_thy thy) xstr))

    | "Rulesets" => Rewrite_Set_Inst (subs,  xstr)

    | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'") 

    end

(* the front-end may request a context for any element of the hierarchy *)

fun no_thycontext (guh : guh) = (guh2theID guh; false)

  handle ERROR _ => true;

(* get the substitution of bound variables for matchTheory:

   # lookup the thm|rls' in the script

   # take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst

   # instantiate this subs with the istates env to [(bdv, x),..]

   # otherwise []

   WN060617 hack assuming that all scripts use only one bound variable

   and use 'v_' as the formal argument for this bound variable*)

fun subs_from (ScrState (env, _, _, _, _, _)) _ (guh : guh) =

    let

      val (_, _, thyID, sect, xstr) = case guh2theID guh of

        theID as [isa, thyID, sect, xstr] => (theID, isa, thyID, sect, xstr)

      | _ => error "subs_from: uncovered case"

    in

      case sect of

        "Theorems" => 

          let val thm = Global_Theory.get_thm (assoc_thy (thyID2theory' thyID)) xstr

          in

            if contains_bdv thm

            then

              let

                val formal_arg = str2term "v_"

                val value = subst_atomic env formal_arg

              in ["(bdv," ^ term2str value ^ ")"] : subs end

            else []

	        end

  	  | "Rulesets" => 

        let

          val rules = (get_rules o assoc_rls) xstr

        in

          if contain_bdv rules

          then

            let

              val formal_arg = str2term "v_"

              val value = subst_atomic env formal_arg

            in ["(bdv," ^ term2str value ^ ")"] : subs end

          else []

        end

      | str => error ("subs_from: uncovered case with " ^ str)

    end

  | subs_from _ _ (guh : guh) = error ("subs_from: uncovered case with " ^ guh)

(* get a substitution for "bdv*" from the current program and environment.

    returns a substitution: subst for rewriting and another: sube for Rewrite: *)

fun get_bdv_subst prog env =

  let

    fun scan (Const _) = NONE

      | scan (Free _) = NONE

      | scan (Var _) = NONE

      | scan (Bound _) = NONE

      | scan (t as Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ Free _$ _) $ _) =

        if is_bdv_subst t then SOME t else NONE

      | scan (Abs (_, _, body)) = scan body

      | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst

  in

    case scan prog of

      NONE => (NONE: subs option, []: subst)

    | SOME tm =>

        let val subst = tm |> subst_atomic env |> isalist2list |> map isapair2pair

          (* "[(bdv,v_v)]": term

                          |> "[(bdv,x)]": term |> ["(bdv,x)"]: term list

                                                         |> [("bdv","x")]: (term * term) list *)

        in (SOME (subst2subs subst), subst) end

          (*"SOME [(bdv,v_v)]": term --> ["(bdv,v_v)"]: string list*)

  end

end