(* Title:  interpreter for scripts

   Author: Walther Neuper 2000

   (c) due to copyright terms

*)

signature LUCAS_INTERPRETER =

sig

  type step = Tac.tac_ * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list

  datatype locate = NotLocatable | Steps of Selem.istate * step list

  val next_tac : (*diss: next-tactic-function*)

    Celem.theory' * Celem.rls -> Ctree.state -> Celem.scr -> Selem.istate * 'a -> Tac.tac_ * (Selem.istate * 'a) * (term * Selem.safe)

  val locate_gen : (*diss: locate-function*)

    Celem.theory' * Celem.rls -> Tac.tac_ -> Ctree.state -> Celem.scr * 'a -> Selem.istate * Proof.context -> locate

(* can these functions be local to Lucin or part of LItools ? *)

  val sel_rules : Ctree.ctree -> Ctree.pos' -> Tac.tac list 

  val init_form : 'a -> Celem.scr -> (term * term) list -> term option

  val tac_2tac : Tac.tac_ -> Tac.tac

  val init_scrstate : theory -> Model.itm list -> Celem.metID -> Selem.istate * Proof.context * Celem.scr

  val from_pblobj' : Celem.theory' -> Ctree.pos' -> Ctree.ctree -> Celem.rls * (Selem.istate * Proof.context) * Celem.scr

  val from_pblobj_or_detail' : Celem.theory' -> Ctree.pos' -> Ctree.ctree -> 

    Celem.rls * (Selem.istate * Proof.context) * Celem.scr

  val rule2thm'' : Celem.rule -> Celem.thm''

  val rule2rls' : Celem.rule -> string

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

  val sel_appl_atomic_tacs : Ctree.ctree -> Ctree.pos' -> Tac.tac list

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

  datatype asap = Aundef | AssOnly | AssGen

  datatype appy = Appy of Tac.tac_ * Selem.scrstate | Napp of LTool.env | Skip of term * LTool.env

  datatype appy_ = Napp_ | Skip_

  val appy : theory' * rls -> Ctree.state -> LTool.env -> lrd list -> term -> term option -> term -> appy

  val formal_args : term -> term list

  val get_stac : 'a -> term -> term option 

  val go : loc_ -> term -> term

  val handle_leaf : string -> theory' -> rls -> LTool.env -> term option -> term -> term -> 

    term option * LTool.stacexpr

  val id_of_scr : term -> string

   val is_spec_pos : Ctree.pos_ -> bool

  val itms2args : 'a -> metID -> Model.itm list -> term list

  val nstep_up : theory' * rls -> Ctree.state -> scr -> LTool.env -> lrd list -> appy_ -> 

    term option -> term -> appy

  val stac2tac : Ctree.ctree -> theory -> term -> Tac.tac

  val stac2tac_ : Ctree.ctree -> theory -> term -> Tac.tac * Tac.tac_

  val upd_env_opt : LTool.env -> term option * term -> LTool.env

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

(*----- unused code, kept as hints to design ideas ---------------------------------------------*)

  type assoc

  val assoc2str : assoc -> string

end 

(* traces the leaves (ie. non-tactical nodes) of Prog found by next_tac, see "and scr" *)   

val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)

structure Lucin(**): LUCAS_INTERPRETER(**) =

struct

open Ctree

(**)

(* data for creating a new node in ctree; designed for use as:

   fun ass* scrstate steps = / ... case ass* scrstate steps of /

   Assoc (scrstate, steps) => ... ass* scrstate steps *)

type step =

    Tac.tac_        (*transformed from associated tac                   *)

    * Generate.mout (*result with indentation etc.                      *)

    * ctree         (*containing node created by tac_ + resp. scrstate  *)

    * pos'          (*position in ctree; ctree * pos' is the proofstate *)

    * pos' list;    (*of ctree-nodes probably cut (by fst tac_)         *)

fun rule2thm'' (Celem.Thm (id, thm)) = (id, thm)

  | rule2thm'' r = error ("rule2thm': not defined for " ^ Celem.rule2str r);

fun rule2rls' (Celem.Rls_ rls) = Celem.id_rls rls

  | rule2rls' r = error ("rule2rls': not defined for " ^ Celem.rule2str r);

(*.makes a (rule,term) list to a Step (m, mout, pt', p', cid) for solve;

   complicated with current t in rrlsstate.*)

fun rts2steps steps ((pt, p), (f, f'', rss, rts), (thy', ro, er, pa)) [(r, (f', am))] =

      let

        val thy = Celem.assoc_thy thy'

        val ctxt = get_ctxt pt p |> Stool.insert_assumptions am

	      val m = Tac.Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))

	      val is = Selem.RrlsState (f', f'', rss, rts)

	      val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1"

	      val (p', cid, mout, pt') = Generate.generate1 thy m (is, ctxt) p pt

      in (is, (m, mout, pt', p', cid) :: steps) end

  | rts2steps steps ((pt, p) ,(f, f'', rss, rts), (thy', ro, er, pa)) ((r, (f', am)) :: rts') =

      let

        val thy = Celem.assoc_thy thy'

        val ctxt = get_ctxt pt p |> Stool.insert_assumptions am

	      val m = Tac.Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))

	      val is = Selem.RrlsState (f', f'', rss, rts)

	      val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1"

	      val (p', cid, mout, pt') = Generate.generate1 thy m (is, ctxt) p pt

      in rts2steps ((m, mout, pt', p', cid)::steps) 

		    ((pt', p'), (f', f'', rss, rts), (thy', ro, er, pa)) rts'

		  end

  | rts2steps _ _ _ = error "rts2steps: uncovered fun-def"

(* functions for the environment stack: NOT YET IMPLEMENTED

fun accessenv id es = the (assoc ((top es) : LTool.env, id))

    handle _ => error ("accessenv: " ^ free2str id ^ " not in LTool.env");

fun updateenv id vl (es : LTool.env stack) = 

    (push (overwrite(top es, (id, vl))) (pop es)) : LTool.env stack;

fun pushenv id vl (es : LTool.env stack) = 

    (push (overwrite(top es, (id, vl))) es) : LTool.env stack;

val popenv = pop : LTool.env stack -> LTool.env stack;

*)

fun de_esc_underscore str =

  let

    fun scan [] = []

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

  in (implode o scan o Symbol.explode) str end;

(*go at a location in a script and fetch the contents*)

fun go [] t = t

  | go (D::p) (Abs(_, _, t0)) = go (p : Celem.loc_) t0

  | go (L::p) (t1 $ _) = go p t1

  | go (R::p) (_ $ t2) = go p t2

  | go l _ = error ("go: no " ^ Celem.loc_2str l);

(*.get argument of first stactic in a script for init_form.*)

fun get_stac thy (_ $ body) =

  let

    fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a = 

    	  (case get_t y e1 a of NONE => get_t y e2 a | la => la)

      | get_t y (Const ("Script.Seq",_) $ e1 $ e2 $ a) _ = 

    	  (case get_t y e1 a of NONE => get_t y e2 a | la => la)

      | get_t y (Const ("Script.Try",_) $ e) a = get_t y e a

      | get_t y (Const ("Script.Try",_) $ e $ a) _ = get_t y e a

      | get_t y (Const ("Script.Repeat",_) $ e) a = get_t y e a

      | get_t y (Const ("Script.Repeat",_) $ e $ a) _ = get_t y e a

      | get_t y (Const ("Script.Or",_) $e1 $ e2) a =

    	  (case get_t y e1 a of NONE => get_t y e2 a | la => la)

      | get_t y (Const ("Script.Or",_) $e1 $ e2 $ a) _ =

    	  (case get_t y e1 a of NONE => get_t y e2 a | la => la)

      | get_t y (Const ("Script.While",_) $ _ $ e) a = get_t y e a

      | get_t y (Const ("Script.While",_) $ _ $ e $ a) _ = get_t y e a

      | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_, _, e2)) a = 

    	  (case get_t y e1 a of NONE => get_t y e2 a | la => la)

    (*| get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =

	      (case get_t y e1 a of NONE => get_t y e2 a | la => la)

      | get_t y (Abs (_,_,e)) a = get_t y e a*)

      | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_, _, _)) a =

    	get_t y e1 a (*don't go deeper without evaluation !*)

      | get_t _ (Const ("If", _) $ _ $ _ $ _) _ = NONE

    	(*(case get_t y e1 a of NONE => get_t y e2 a | la => la)*)

      | get_t _ (Const ("Script.Rewrite",_) $ _ $ _ $ a) _ = SOME a

      | get_t _ (Const ("Script.Rewrite",_) $ _ $ _    ) a = SOME a

      | get_t _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a

      | get_t _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ )    a = SOME a

      | get_t _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ a) _ = SOME a

      | get_t _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ )    a = SOME a

      | get_t _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a

      | get_t _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ )  a =SOME a

      | get_t _ (Const ("Script.Calculate",_) $ _ $ a) _ = SOME a

      | get_t _ (Const ("Script.Calculate",_) $ _ )    a = SOME a

      | get_t _ (Const ("Script.Substitute",_) $ _ $ a) _ = SOME a

      | get_t _ (Const ("Script.Substitute",_) $ _ )    a = SOME a

      | get_t _ (Const ("Script.SubProblem",_) $ _ $ _) _ = NONE

      | get_t _ _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)

    in get_t thy body Celem.e_term end

  | get_stac _ t = error ("get_stac: no fun-def. for " ^ Celem.term2str t);

fun init_form thy (Celem.Prog sc) env =

    (case get_stac thy sc of NONE => NONE | SOME stac => SOME (subst_atomic env stac))

  | init_form _ _ _ = error "init_form: no match";

(* get the arguments of the script out of the scripts parsetree *)

fun formal_args scr = (fst o split_last o snd o strip_comb) scr;

(* get the identifier of the script out of the scripts parsetree *)

fun id_of_scr sc = (id_of o fst o strip_comb) sc;

(*WN020526: not clear, when a is available in ass_up for eval_true*)

(*WN060906: in "fun handle_leaf" eg. uses "SOME M__"(from some PREVIOUS

  curried Rewrite) for CURRENT value (which may be different from PREVIOUS);

  thus "NONE" must be set at the end of currying (ill designed anyway)*)

fun upd_env_opt env (SOME a, v) = LTool.upd_env env (a, v)

  | upd_env_opt env (NONE, _) = 

      ((*tracing ("*** upd_env_opt: (NONE," ^ term2str v ^ ")");*) env);

type dsc = typ; (* <-> nam..unknow in Descript.thy *)

(*.create the actual parameters (args) of script: their order 

  is given by the order in met.pat .*)

(*WN.5.5.03: ?: does this allow for different descriptions ???

             ?: why not taken from formal args of script ???

!: FIXXXME penv: push it here in itms2args into script-evaluation*)

(* val (thy, mI, itms) = (thy, metID, itms);

   *)

val errmsg = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."

fun itms2args _ mI itms =

  let

    val mvat = Model.max_vt itms

    fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b

    val itms = filter (okv mvat) itms

    fun test_dsc d (_, _, _, _, itm_) = (d = Model.d_in itm_)

    fun itm2arg itms (_,(d,_)) =

        case find_first (test_dsc d) itms of

          NONE => error ("itms2args: '" ^ Celem.term2str d ^ "' not in itms")

        | SOME (_, _, _, _, itm_) => Model.penvval_in itm_

      (*| SOME (_,_,_,_,itm_) => mk_arg thy (Model.d_in itm_) (ts_in itm_);

            penv postponed; presently penv holds already LTool.env for script*)

    val pats = (#ppc o Specify.get_met) mI

    val _ = if pats = [] then raise ERROR errmsg else ()

  in (flat o (map (itm2arg itms))) pats end;

(* convert a script-tac 'stac' to a tactic 'tac';

   if stac is an initac, then convert to a 'tac_' (as required in appy).

   arg ctree for pushing the thy specified in rootpbl into subpbls    *)

fun stac2tac_ _ thy (Const ("Script.Rewrite", _) $ Free (thmID, _) $ _ $ _) =

    let

      val tid = (de_esc_underscore o strip_thy) thmID

    in (Tac.Rewrite (tid, Rewrite.assoc_thm'' thy tid), Tac.Empty_Tac_) end

  | stac2tac_ _ thy (Const ("Script.Rewrite'_Inst", _) $ sub $ Free (thmID, _) $ _ $ _) =

    let

      val subML = ((map TermC.isapair2pair) o TermC.isalist2list) sub

      val subStr = Selem.subst2subs subML

      val tid = (de_esc_underscore o strip_thy) thmID (*4.10.02 unnoetig*)

    in (Tac.Rewrite_Inst (subStr, (tid, Rewrite.assoc_thm'' thy tid)), Tac.Empty_Tac_) end

  | stac2tac_ _ _ (Const ("Script.Rewrite'_Set",_) $ Free (rls, _) $ _ $ _) =

     (Tac.Rewrite_Set ((de_esc_underscore o strip_thy) rls), Tac.Empty_Tac_)

  | stac2tac_ _ _ (Const ("Script.Rewrite'_Set'_Inst", _) $ sub $ Free (rls, _) $ _ $ _) =

    let

      val subML = ((map TermC.isapair2pair) o TermC.isalist2list) sub;

      val subStr = Selem.subst2subs subML;

    in (Tac.Rewrite_Set_Inst (subStr, rls), Tac.Empty_Tac_) end

  | stac2tac_ _ _ (Const ("Script.Calculate", _) $ Free (op_, _) $ _) = (Tac.Calculate op_, Tac.Empty_Tac_)

  | stac2tac_ _ _ (Const ("Script.Take", _) $ t) = (Tac.Take (Celem.term2str t), Tac.Empty_Tac_)

  | stac2tac_ _ _ (Const ("Script.Substitute", _) $ isasub $ _) =

    (Tac.Substitute ((Selem.subte2sube o TermC.isalist2list) isasub), Tac.Empty_Tac_)

  | stac2tac_ _ thy (Const("Script.Check'_elementwise", _) $ _ $ 

    (Const ("Set.Collect", _) $ Abs (_, _, pred))) =

      (Tac.Check_elementwise (Celem.term_to_string''' thy pred), Tac.Empty_Tac_)

  | stac2tac_ _ _ (Const("Script.Or'_to'_List", _) $ _ ) = (Tac.Or_to_List, Tac.Empty_Tac_)

  | stac2tac_ _ _ (Const ("Script.Tac", _) $ Free (str, _)) = 

    (Tac.Tac ((de_esc_underscore o strip_thy) str),  Tac.Empty_Tac_) 

    (*compare "| assod _ (Subproblem'"*)

  | stac2tac_ pt _ (stac as Const ("Script.SubProblem",_) $

	  (Const ("Product_Type.Pair",_) $Free (dI', _) $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ 

	    ags') =

    let

      val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);

      val thy = Celem.maxthy (Celem.assoc_thy dI) (rootthy pt);

	    val pI = ((map (de_esc_underscore o TermC.free2str)) o TermC.isalist2list) pI';

	    val mI = ((map (de_esc_underscore o TermC.free2str)) o TermC.isalist2list) mI';

	    val ags = TermC.isalist2list ags';

	    val (pI, pors, mI) = 

	      if mI = ["no_met"] 

	      then

          let

            val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)

		          handle ERROR "actual args do not match formal args" 

			        => (Chead.match_ags_msg pI stac ags(*raise exn*); [])

		        val pI' = Specify.refine_ori' pors pI;

		      in (pI', pors (* refinement over models with diff.prec only *), 

		          (hd o #met o Specify.get_pbt) pI') end

	      else (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)

		      handle ERROR "actual args do not match formal args"

		      => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);

      val (fmz_, vals) = Chead.oris2fmz_vals pors;

	    val {cas,ppc,thy,...} = Specify.get_pbt pI

	    val dI = Celem.theory2theory' thy (*.take dI from _refined_ pbl.*)

	    val dI = Celem.theory2theory' (Celem.maxthy (Celem.assoc_thy dI) (rootthy pt));

      val ctxt = dI |> Celem.Thy_Info_get_theory |> Proof_Context.init_global |> Stool.declare_constraints' vals

	    val hdl =

        case cas of

		      NONE => LTool.pblterm dI pI

		    | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t

      val f = LTool.subpbl (strip_thy dI) pI

    in (Tac.Subproblem (dI, pI),	Tac.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))

    end

  | stac2tac_ _ thy t = error ("stac2tac_ TODO: no match for " ^ Celem.term_to_string''' thy t);

fun stac2tac pt thy t = (fst o stac2tac_ pt thy) t;

datatype ass = 

    Ass of

      Tac.tac_ *  (* SubProblem gets args instantiated in assod *)

  	  term        (* for itr_arg, result in ets *)

  | AssWeak of

      Tac.tac_ *

  	  term     (*for itr_arg,result in ets*)

  | NotAss;

(* check if tac_ is associated with stac.

   Additional task: check if term t (the result has been calculated from) in tac_

   has been changed (see "datatype tac_"); if yes, recalculate result

   TODO.WN120106 recalculate impl.only for Substitute'

args

  pt     : ctree for pushing the thy specified in rootpbl into subpbls

  d      : unused (planned for data for comparison)

  tac_   : from user (via applicable_in); to be compared with ...

  stac   : found in Script

returns

  Ass    : associated: e.g. thmID in stac = thmID in m

                       +++ arg   in stac = arg   in m

  AssWeak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//

  NotAss :             e.g. thmID in stac/=/thmID in m (not =)

*)

fun assod _ _ (m as Tac.Rewrite_Inst' (_, _, _, _, _, thm'' as (thmID, _), f, (f', _))) stac =

    (case stac of

	    (Const ("Script.Rewrite'_Inst", _) $ _ $ Free (thmID_, _) $ _ $ f_) =>

	      if thmID = thmID_

        then 

	        if f = f_ 

          then ((*tracing"3### assod ..Ass";*) Ass (m,f')) 

	        else ((*tracing"3### assod ..AssWeak";*) AssWeak(m, f'))

	      else ((*tracing"3### assod ..NotAss";*) NotAss)

    | (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ Free (rls_, _) $ _ $ f_) =>

	      if Rtools.contains_rule (Celem.Thm thm'') (assoc_rls rls_)

        then if f = f_ then Ass (m,f') else AssWeak (m,f')

	      else NotAss

    | _ => NotAss)

  | assod _ _ (m as Tac.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', _))) stac =

    (case stac of

	    (Const ("Script.Rewrite", _) $ Free (thmID_, _) $ _ $ f_) =>

	      ((*tracing ("3### assod: stac = " ^ ter2str t);

	       tracing ("3### assod: f(m)= " ^ term2str f);*)

	      if thmID = thmID_

        then 

	        if f = f_

          then ((*tracing"3### assod ..Ass";*) Ass (m,f')) 

	        else 

            ((*tracing"### assod ..AssWeak";

		         tracing("### assod: f(m)  = " ^ term2str f);

		         tracing("### assod: f(stac)= " ^ term2str f_)*)

		         AssWeak (m,f'))

	      else ((*tracing"3### assod ..NotAss";*) NotAss))

    | (Const ("Script.Rewrite'_Set", _) $ Free (rls_, _) $ _ $ f_) =>

	       if Rtools.contains_rule (Celem.Thm thm'') (assoc_rls rls_)

         then if f = f_ then Ass (m, f') else AssWeak (m, f')

	       else NotAss

    | _ => NotAss)

  | assod _ _ (m as Tac.Rewrite_Set_Inst' (_, _, _, rls, f, (f', _))) 

      (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ Free (rls_, _) $ _ $ f_) = 

    if Celem.id_rls rls = rls_ 

    then if f = f_ then Ass (m, f') else AssWeak (m ,f')

    else NotAss

  | assod _ _ (m as Tac.Detail_Set_Inst' (_, _, _, rls, f, (f',_))) 

      (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ Free (rls_, _) $ _ $ f_) = 

    if Celem.id_rls rls = rls_

    then if f = f_ then Ass (m, f') else AssWeak (m, f')

    else NotAss

  | assod _ _ (m as Tac.Rewrite_Set' (_, _, rls, f, (f', _))) 

      (Const ("Script.Rewrite'_Set", _) $ Free (rls_, _) $ _ $ f_) = 

    if Celem.id_rls rls = rls_

    then if f = f_ then Ass (m, f') else AssWeak (m, f')

    else NotAss

  | assod _ _ (m as Tac.Detail_Set' (_, _, rls, f, (f', _))) 

      (Const ("Script.Rewrite'_Set", _) $ Free (rls_, _) $ _ $ f_) = 

    if Celem.id_rls rls = rls_

    then if f = f_ then Ass (m, f') else AssWeak (m, f')

    else NotAss

  | assod _ _ (m as Tac.Calculate' (_, op_, f, (f', _))) stac =

    (case stac of

	    (Const ("Script.Calculate",_) $ Free (op__,_) $ f_) =>

	      if op_ = op__

        then if f = f_ then Ass (m, f') else AssWeak (m, f')

	      else NotAss

    | (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ Free(rls_,_) $_$f_)  =>

        let val thy = Celem.assoc_thy "Isac";

        in

          if Rtools.contains_rule (Celem.Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)

          then if f = f_ then Ass (m, f') else AssWeak (m, f')

          else NotAss

        end

    | (Const ("Script.Rewrite'_Set",_) $ Free (rls_, _) $ _ $ f_) =>

        let val thy = Celem.assoc_thy "Isac";

        in

          if Rtools.contains_rule (Celem.Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)

          then if f = f_ then Ass (m,f') else AssWeak (m,f')

          else NotAss

        end

    | _ => NotAss)

  | assod _ _ (m as Tac.Check_elementwise' (consts, _, (consts_chkd, _)))

      (Const ("Script.Check'_elementwise",_) $ consts' $ _) =

    if consts = consts'

    then Ass (m, consts_chkd)

    else NotAss

  | assod _ _ (m as Tac.Or_to_List' (_, list)) (Const ("Script.Or'_to'_List", _) $ _) = Ass (m, list) 

  | assod _ _ (m as Tac.Take' term) (Const ("Script.Take", _) $ _) = Ass (m, term)

  | assod _ _ (m as Tac.Substitute' (ro, erls, subte, f, f')) (Const ("Script.Substitute", _) $ _ $ t) =

	  if f = t then Ass (m, f')

	  else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)

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

		  then

		    let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t

		    in if t = t' then error "assod: Substitute' not applicable to val of Expr"

		       else Ass (Tac.Substitute' (ro, erls, subte, t, t'), t')

		    end

		  else (case Rewrite.rewrite_terms_ (Celem.Isac ()) ro erls subte t of

		         SOME (t', _) =>  Ass (Tac.Substitute' (ro, erls, subte, t, t'), t')

		       | NONE => error "assod: Substitute' not applicable to val of Expr")

  | assod _ _ (m as Tac.Tac_ (thy, _, id, f')) (Const ("Script.Tac",_) $ Free (id', _)) =

    if id = id'

    then Ass (m, ((Thm.term_of o the o (TermC.parse thy)) f'))

    else NotAss

    (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)

  | assod pt _ (Tac.Subproblem' ((domID, pblID, _), _, _, _, _, _))

	    (stac as Const ("Script.SubProblem",_) $ (Const ("Product_Type.Pair",_) $

		    Free (dI',_) $ (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =

    let 

      val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);

      val thy = Celem.maxthy (Celem.assoc_thy dI) (rootthy pt);

	    val pI = ((map (de_esc_underscore o TermC.free2str)) o TermC.isalist2list) pI';

	    val mI = ((map (de_esc_underscore o TermC.free2str)) o TermC.isalist2list) mI';

	    val ags = TermC.isalist2list ags';

	    val (pI, pors, mI) = 

	      if mI = ["no_met"] 

	      then

          let

            val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)

		          handle ERROR "actual args do not match formal args"

			          => (Chead.match_ags_msg pI stac ags(*raise exn*);[]);

		        val pI' = Specify.refine_ori' pors pI;

		      in (pI', pors (*refinement over models with diff.prec only*), (hd o #met o Specify.get_pbt) pI')

          end

	      else (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)

		      handle ERROR "actual args do not match formal args"

		      => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);

      val (fmz_, vals) = Chead.oris2fmz_vals pors;

	    val {cas, ppc, thy, ...} = Specify.get_pbt pI

	    val dI = Celem.theory2theory' thy (*take dI from _refined_ pbl*)

	    val dI = Celem.theory2theory' (Celem.maxthy (Celem.assoc_thy dI) (rootthy pt))

	    val ctxt = dI |> Celem.Thy_Info_get_theory |> Proof_Context.init_global |> Stool.declare_constraints' vals

	    val hdl = 

        case cas of

		      NONE => LTool.pblterm dI pI

		    | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t

      val f = LTool.subpbl (strip_thy dI) pI

    in 

      if domID = dI andalso pblID = pI

      then Ass (Tac.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f), f) 

      else NotAss

    end

  | assod _ _ m _ = 

    (if (!trace_script) 

     then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"

		   ^ "@@@ tac_ = " ^ Tac.tac_2str m)

     else ();

    NotAss);

fun tac_2tac (Tac.Refine_Tacitly' (pI, _, _, _, _)) = Tac.Refine_Tacitly pI

  | tac_2tac (Tac.Model_Problem' (_, _, _)) = Tac.Model_Problem

  | tac_2tac (Tac.Add_Given' (t, _)) = Tac.Add_Given t

  | tac_2tac (Tac.Add_Find' (t, _)) = Tac.Add_Find t

  | tac_2tac (Tac.Add_Relation' (t, _)) = Tac.Add_Relation t

  | tac_2tac (Tac.Specify_Theory' dI) = Tac.Specify_Theory dI

  | tac_2tac (Tac.Specify_Problem' (dI, _)) = Tac.Specify_Problem dI

  | tac_2tac (Tac.Specify_Method' (dI, _, _)) = Tac.Specify_Method dI

  | tac_2tac (Tac.Rewrite' (_, _, _, _, thm, _, _)) = Tac.Rewrite thm

  | tac_2tac (Tac.Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Tac.Rewrite_Inst (Selem.subst2subs sub, thm)

  | tac_2tac (Tac.Rewrite_Set' (_, _, rls, _, _)) = Tac.Rewrite_Set (Celem.id_rls rls)

  | tac_2tac (Tac.Detail_Set' (_, _, rls, _, _)) = Tac.Detail_Set (Celem.id_rls rls)

  | tac_2tac (Tac.Rewrite_Set_Inst' (_, _, sub, rls, _, _)) = 

    Tac.Rewrite_Set_Inst (Selem.subst2subs sub, Celem.id_rls rls)

  | tac_2tac (Tac.Detail_Set_Inst' (_, _, sub, rls, _, _)) = 

    Tac.Detail_Set_Inst (Selem.subst2subs sub, Celem.id_rls rls)

  | tac_2tac (Tac.Calculate' (_, op_, _, _)) = Tac.Calculate (op_)

  | tac_2tac (Tac.Check_elementwise' (_, pred, _)) = Tac.Check_elementwise pred

  | tac_2tac (Tac.Or_to_List' _) = Tac.Or_to_List

  | tac_2tac (Tac.Take' term) = Tac.Take (Celem.term2str term)

  | tac_2tac (Tac.Substitute' (_, _, subte, _, _)) = Tac.Substitute (Selem.subte2sube subte) 

  | tac_2tac (Tac.Tac_ (_, _, id, _)) = Tac.Tac id

  | tac_2tac (Tac.Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Tac.Subproblem (domID, pblID)

  | tac_2tac (Tac.Check_Postcond' (pblID, _)) = Tac.Check_Postcond pblID

  | tac_2tac Tac.Empty_Tac_ = Tac.Empty_Tac

  | tac_2tac m = error ("tac_2tac: not impl. for "^(Tac.tac_2str m));

val idT = Type ("Script.ID", []);

fun make_rule thy t =

  let val ct = Thm.global_cterm_of thy (HOLogic.Trueprop $ t)

  in Celem.Thm (Celem.term_to_string''' thy (Thm.term_of ct), Thm.make_thm ct) end;

fun rep_tac_ (Tac.Rewrite_Inst' (thy', _, _, put, subs, (thmID, _), f, (f', _))) = 

    let val fT = type_of f;

      val b = if put then @{term True} else @{term False};

      val sT = (type_of o fst o hd) subs;

      val subs' = TermC.list2isalist (HOLogic.mk_prodT (sT, sT)) (map HOLogic.mk_prod subs);

      val sT' = type_of subs';

      val lhs = Const ("Script.Rewrite'_Inst", [sT', idT, HOLogic.boolT, fT] ---> fT) 

        $ subs' $ Free (thmID, idT) $ b $ f;

    in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end

  | rep_tac_ (Tac.Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=

    let 

      val fT = type_of f;

      val b = if put then @{term True} else @{term False};

      val lhs = Const ("Script.Rewrite", [idT, HOLogic.boolT, fT] ---> fT)

        $ Free (thmID, idT) $ b $ f;

    in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end

  | rep_tac_ (Tac.Rewrite_Set_Inst' (_, _, _, _, _, (f', _))) = (Celem.e_rule, (Celem.e_term, f'))

  | rep_tac_ (Tac.Rewrite_Set' (thy', put, rls, f, (f', _))) =

    let 

      val fT = type_of f;

      val b = if put then @{term True} else @{term False};

      val lhs = Const ("Script.Rewrite'_Set", [idT, HOLogic.boolT, fT] ---> fT) 

        $ Free (Celem.id_rls rls, idT) $ b $ f;

    in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end

  | rep_tac_ (Tac.Calculate' (thy', op_, f, (f', _)))=

    let

      val fT = type_of f;

      val lhs = Const ("Script.Calculate",[idT,fT] ---> fT) $ Free (op_,idT) $ f

    in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end

  | rep_tac_ (Tac.Check_elementwise' (_, _, (t', _))) = (Celem.Erule, (Celem.e_term, t'))

  | rep_tac_ (Tac.Subproblem' (_, _, _, _, _, t')) = (Celem.Erule, (Celem.e_term, t'))

  | rep_tac_ (Tac.Take' t') = (Celem.Erule, (Celem.e_term, t'))

  | rep_tac_ (Tac.Substitute' (_, _, _, t, t')) = (Celem.Erule, (t, t'))

  | rep_tac_ (Tac.Or_to_List' (t, t')) = (Celem.Erule, (t, t'))

  | rep_tac_ m = error ("rep_tac_: not impl.for " ^ Tac.tac_2str m)

fun tac_2res m = (snd o snd o rep_tac_) m;

(* handle a leaf at the end of recursive descent:

   a leaf is either a tactic or an 'expr' in "let v = expr"

   where "expr" does not contain a tactic.

   Handling a leaf comprises

   (1) 'subst_stacexpr' substitute LTool.env and complete curried tactic

   (2) rewrite the leaf by 'srls'

*)

fun handle_leaf call thy srls E a v t =

      (*WN050916 'upd_env_opt' is a blind copy from previous version*)

    case LTool.subst_stacexpr E a v t of

	    (a', LTool.STac stac) => (*script-tactic*)

	      let val stac' =

            Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)

	      in

          (if (! trace_script) 

	         then tracing ("@@@ "^call^" leaf '" ^ Celem.term2str t^"' ---> STac '" ^ Celem.term2str stac ^"'")

	         else ();

	         (a', LTool.STac stac'))

	      end

    | (a', LTool.Expr lexpr) => (*leaf-expression*)

	      let val lexpr' =

            Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) lexpr)

	      in

          (if (! trace_script) 

	         then tracing("@@@ "^call^" leaf '" ^ Celem.term2str t^"' ---> Expr '" ^ Celem.term2str lexpr'^"'")

	         else ();

	         (a', LTool.Expr lexpr')) (*lexpr' is the value of the Expr*)

	      end;

(** locate an applicable stac in a script **)

datatype assoc =   (* ExprVal in the sense of denotational semantics               *)

  Assoc of         (* the stac is associated, strongly or weakly                   *)

  Selem.scrstate * (* the current; returned for next_tac etc. outside ass*         *)  

  (step list)      (* list of steps done until associated stac found;

	                    initiated with the data for doing the 1st step,

                      thus the head holds these data further on,

		                  while the tail holds steps finished (incl.scrstate in ctree) *)

| NasApp of        (* stac not associated, but applicable, ctree-node generated    *)

  Selem.scrstate * (step list)

| NasNap of        (* stac not associated, not applicable, nothing generated;

	                    for distinction in Or, for leaving iterations, leaving Seq,

		                  evaluate scriptexpressions                                   *)

  term * LTool.env;

fun assoc2str (Assoc _) = "Assoc"

  | assoc2str (NasNap _) = "NasNap"

  | assoc2str (NasApp _) = "NasApp";

datatype asap = (* arg. of assy _only_ for distinction w.r.t. Or                 *)

  Aundef        (* undefined: set only by (topmost) Or                           *)

| AssOnly       (* do not execute appl stacs - there could be an associated

	                 in parallel Or-branch                                         *)

| AssGen;       (* no Ass(Weak) found within Or, thus 

                   search for _applicable_ stacs, execute and generate pt        *)

(*this constructions doesnt allow arbitrary nesting of Or !!!                    *)

(* assy, ass_up, astep_up scan for locate_gen in a script.

   search is clearly separated into (1)-(2):

   (1) assy is recursive descent;

   (2) ass_up resumes interpretation at a location somewhere in the script;

       astep_up does only get to the parentnode of the scriptexpr.

   consequence:

   * call of (2) means _always_ that in this branch below

     there was an appl.stac (Repeat, Or e1, ...) found by the previous step.

*)

(*WN161112 blanks between list elements left as is until istate is introduced here*)

fun assy ya ((E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))) =

    (case assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e of

       NasApp ((E',l,a,v,S,_),ss) => 

         let

           val id' = TermC.mk_Free (id, T);

           val E' = LTool.upd_env E' (id', v);

         in assy ya ((E', l @ [Celem.R, Celem.D], a,v,S,b),ss) body end

     | NasNap (v,E) =>

         let

           val id' = TermC.mk_Free (id, T);

           val E' = LTool.upd_env E (id', v);

         in assy ya ((E', l @ [Celem.R, Celem.D], a,v,S,b),ss) body end

     | ay => ay)

  | assy (ya as (thy,_,srls,_,_)) ((E,l,_,v,S,b),ss) (Const ("Script.While",_) $ c $ e $ a) =

    if Rewrite.eval_true_ thy srls (subst_atomic (LTool.upd_env E (a,v)) c) 

    then assy ya ((E, l @ [Celem.L, Celem.R], SOME a,v,S,b),ss)  e

    else NasNap (v, E)

  | assy (ya as (thy,_,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("Script.While",_) $ c $ e) =

    if Rewrite.eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c) 

    then assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e

    else NasNap (v, E)

  | assy (ya as (thy,_,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("If",_) $ c $ e1 $ e2) =

    if Rewrite.eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c) 

    then assy ya ((E, l @ [Celem.L, Celem.R], a,v,S,b),ss) e1

    else assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e2 

  | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Try",_) $ e $ a) =

    (case assy ya ((E, l @ [Celem.L, Celem.R], SOME a,v,S,b),ss) e of ay => ay) 

  | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Try",_) $ e) =

    (case assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e of ay => ay)

  | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2 $ a) =

    (case assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss) e1 of

	     NasNap (v, E) => assy ya ((E, l @ [Celem.L, Celem.R], SOME a,v,S,b),ss) e2

     | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l @ [Celem.L, Celem.R], SOME a,v,S,b),ss) e2

     | ay => ay)

  | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2) =

    (case assy ya ((E, l @ [Celem.L, Celem.R], a,v,S,b),ss) e1 of

	     NasNap (v, E) => assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e2

     | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e2

     | ay => ay)

  | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Repeat",_) $ e $ a) =

    assy ya ((E,(l @ [Celem.L, Celem.R]),SOME a,v,S,b),ss) e

  | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Repeat",_) $ e) =

    assy ya ((E,(l @ [Celem.R]),a,v,S,b),ss) e

  | assy (y,x,s,sc,Aundef) ((E,l,_,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2 $ a) =

    (case assy (y,x,s,sc,AssOnly) ((E,(l @ [Celem.L, Celem.L, Celem.R]),SOME a,v,S,b),ss) e1 of

	     NasNap (v, E) => 

	       (case assy (y,x,s,sc,AssOnly) ((E,(l @ [Celem.L, Celem.R]),SOME a,v,S,b),ss) e2 of

	          NasNap (v, E) => 

	            (case assy (y,x,s,sc,AssGen) ((E,(l @ [Celem.L, Celem.L, Celem.R]),SOME a,v,S,b),ss) e1 of

	               NasNap (v, E) => 

	                 assy (y,x,s,sc,AssGen) ((E, (l @ [Celem.L, Celem.R]), SOME a,v,S,b),ss) e2

	             | ay => ay)

	        | ay =>ay)

     | NasApp _ => error ("assy: FIXXXME ///must not return NasApp///")

     | ay => (ay))

  | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2) =

    (case assy ya ((E, (l @ [Celem.L, Celem.R]),a,v,S,b), ss) e1 of

	     NasNap (v, E) => assy ya ((E,(l @ [Celem.R]),a,v,S,b), ss) e2

     | ay => (ay))

    (*here is not a tactical like TRY etc, but a tactic creating a step in calculation*)

  | assy (thy',ctxt,sr,d,ap) ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss) t =

    (case handle_leaf "locate" thy' sr E a v t of

	     (a', LTool.Expr _) => 

	        (NasNap (Rewrite.eval_listexpr_ (Celem.assoc_thy thy') sr

		     (subst_atomic (upd_env_opt E (a',v)) t), E))

     | (a', LTool.STac stac) =>

	       let

           val p' = 

             case p_ of Frm => p 

             | Res => lev_on p

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

	       in

           case assod pt d m stac of

	         Ass (m,v') =>

	           let val (p'',c',f',pt') =

                 Generate.generate1 (Celem.assoc_thy thy') m (Selem.ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;

	           in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end

           | AssWeak (m,v') => 

	           let val (p'',c',f',pt') =

               Generate.generate1 (Celem.assoc_thy thy') m (Selem.ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt;

	           in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end

           | NotAss =>

             (case ap of   (*switch for Or: 1st AssOnly, 2nd AssGen*)

                AssOnly => (NasNap (v, E))

              | _ =>

                  (case Applicable.applicable_in (p,p_) pt (stac2tac pt (Celem.assoc_thy thy') stac) of

		                 Chead.Appl m' =>

		                   let

                         val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*))

		                     val (p'',c',f',pt') =

		                       Generate.generate1 (Celem.assoc_thy thy') m' (Selem.ScrState is, ctxt) (p', p_) pt;

		                   in NasApp (is,(m,f',pt',p'',c @ c')::ss) end

		               | Chead.Notappl _ => (NasNap (v, E))

		              )

		         )

         end)

  | assy _ (_, []) t = error ("assy: uncovered fun-def with " ^ Celem.term2str t);

(*WN161112 blanks between list elements left as is until istate is introduced here*)

fun ass_up (ys as (y,ctxt,s,Celem.Prog sc,d)) ((E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ _) =

    let 

	    val l = drop_last l; (*comes from e, goes to Abs*)

      val (i, T, body) =

        (case go l sc of

           Const ("HOL.Let",_) $ _ $ (Abs (i, T, body)) => (i, T, body)

         | t => error ("ass_up..HOL.Let $ _ with " ^ Celem.term2str t))

      val i = TermC.mk_Free (i, T);

      val E = LTool.upd_env E (i, v);

    in case assy (y,ctxt,s,d,Aundef) ((E, l @ [Celem.R, Celem.D], a,v,S,b),ss) body of

	       Assoc iss => Assoc iss

	     | NasApp iss => astep_up ys iss 

	     | NasNap (v, E) => astep_up ys ((E,l,a,v,S,b),ss) 

	  end

  | ass_up ys iss (Abs (_,_,_)) = astep_up ys iss (*TODO 5.9.00: LTool.env ?*)

  | ass_up ys iss (Const ("HOL.Let",_) $ _ $ (Abs _)) = astep_up ys iss (*TODO 5.9.00: LTool.env ?*)

  | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _ $ _) =

    astep_up ysa iss (*all has been done in (*2*) below*)

  | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _) =

    astep_up ysa iss (*2*: comes from e2*)

  | ass_up (ysa as (y,ctxt,s,Celem.Prog sc,d)) ((E,l,a,v,S,b),ss)

	  (Const ("Script.Seq",_) $ _ ) = (*2*: comes from e1, goes to e2*)

     let 

       val up = drop_last l;

     val e2 =

       (case go up sc of

          Const ("Script.Seq",_) $ _ $ e2 => e2

        | t => error ("ass_up..Script.Seq $ _ with " ^ Celem.term2str t))

     in case assy (y,ctxt,s,d,Aundef) ((E, up @ [Celem.R], a,v,S,b),ss) e2 of

         NasNap (v,E) => astep_up ysa ((E,up,a,v,S,b),ss)

       | NasApp iss => astep_up ysa iss

       | ay => ay 

     end

  | ass_up ysa iss (Const ("Script.Try",_) $ _ $ _) = astep_up ysa iss

  | ass_up ysa iss (Const ("Script.Try",_) $ _) = astep_up ysa iss

  | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,_,v,S,b),ss)

	   (*(Const ("Script.While",_) $ c $ e $ a) = WN050930 blind fix*)

	    (t as Const ("Script.While",_) $ c $ e $ a) =

    if Rewrite.eval_true_ y s (subst_atomic (LTool.upd_env E (a,v)) c)

    then case assy (y,ctxt,s,d,Aundef) ((E, l @ [Celem.L, Celem.R], SOME a,v,S,b),ss) e of 

      NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss)

    | NasApp ((E',l,a,v,S,b),ss) =>

      ass_up ys ((E',l,a,v,S,b),ss) t (*WN050930 't' was not assigned*)

    | ay => ay

    else astep_up ys ((E,l, SOME a,v,S,b),ss)

  | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,a,v,S,b),ss)

	   (*(Const ("Script.While",_) $ c $ e) = WN050930 blind fix*)

	     (t as Const ("Script.While",_) $ c $ e) =

    if Rewrite.eval_true_ y s (subst_atomic (upd_env_opt E (a,v)) c)

    then case assy (y,ctxt,s,d,Aundef) ((E, l @ [Celem.R], a,v,S,b),ss) e of 

       NasNap (v,E') => astep_up ys ((E',l, a,v,S,b),ss)

     | NasApp ((E',l,a,v,S,b),ss) =>

       ass_up ys ((E',l,a,v,S,b),ss) t (*WN050930 't' was not assigned*)

     | ay => ay

    else astep_up ys ((E,l, a,v,S,b),ss)

  | ass_up y iss (Const ("If",_) $ _ $ _ $ _) = astep_up y iss

  | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,_,v,S,b),ss)

	    (t as Const ("Script.Repeat",_) $ e $ a) =

    (case assy (y,ctxt,s,d, Aundef) ((E, (l @ [Celem.L, Celem.R]), SOME a,v,S,b),ss) e of 

      NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss)

    | NasApp ((E',l,a,v,S,b),ss) =>

      ass_up ys ((E',l,a,v,S,b),ss) t

    | ay => ay)

  | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,a,v,S,b),ss)

	    (t as Const ("Script.Repeat",_) $ e) =

    (case assy (y,ctxt,s,d,Aundef) ((E, (l @ [Celem.R]), a,v,S,b),ss) e of 

       NasNap (v', E') => astep_up ys ((E',l,a,v',S,b),ss)

     | NasApp ((E',l,a,v',S,_),ss) => ass_up ys ((E',l,a,v',S,b),ss) t

     | ay => ay)

  | ass_up y iss (Const ("Script.Or",_) $ _ $ _ $ _) = astep_up y iss

  | ass_up y iss (Const ("Script.Or",_) $ _ $ _) = astep_up y iss

  | ass_up y ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $ _ ) = 

    astep_up y ((E, (drop_last l), a,v,S,b),ss)

  | ass_up _ _ t =

    error ("ass_up not impl for t= " ^ Celem.term2str t)

and astep_up (ys as (_,_,_,Celem.Prog sc,_)) ((E,l,a,v,S,b),ss) =

  if 1 < length l

  then 

    let val up = drop_last l;

    in ass_up ys ((E,up,a,v,S,b),ss) (go up sc) end

  else (NasNap (v, E))

  | astep_up _ ((_,l,_,_,_,_),_) = error ("astep_up: uncovered fun-def with " ^ Celem.loc_2str l)

(*check if there are tacs for rewriting only*)

fun rew_only ([]:step list) = true

  | rew_only (((Tac.Rewrite' _          ,_,_,_,_))::ss) = rew_only ss

  | rew_only (((Tac.Rewrite_Inst' _     ,_,_,_,_))::ss) = rew_only ss

  | rew_only (((Tac.Rewrite_Set' _      ,_,_,_,_))::ss) = rew_only ss

  | rew_only (((Tac.Rewrite_Set_Inst' _ ,_,_,_,_))::ss) = rew_only ss

  | rew_only (((Tac.Calculate' _        ,_,_,_,_))::ss) = rew_only ss

  | rew_only (((Tac.Begin_Trans' _      ,_,_,_,_))::ss) = rew_only ss

  | rew_only (((Tac.End_Trans' _        ,_,_,_,_))::ss) = rew_only ss

  | rew_only _ = false; 

datatype locate =

  Steps of Selem.istate (* producing hd of step list (which was latest)

	                         for next_tac, for reporting Safe|Unsafe to DG  *)

	   * step             (* (scrstate producing this step is in ctree !)   *) 

		 list               (* locate_gen may produce intermediate steps      *)

| NotLocatable;         (* no (m Ass m') or (m AssWeak m') found          *)

(* locate_gen tries to locate an input tac m in the script. 

   pursuing this goal the script is executed until an (m' equiv m) is found,

   or the end of the script

args

   m   : input by the user, already checked by applicable_in,

         (to be searched within Or; and _not_ an m doing the step on ctree !)

   p,pt: (incl ets) at the time of input

   scr : the script

   d   : canonical simplifier for locating Take, Substitute, Subproblems etc.

   ets : ets at the time of input

   l   : the location (in scr) of the stac which generated the current formula

returns

   Steps: pt,p (incl. ets) with m done

          pos' list of proofobjs cut (from generate)

          safe: implied from last proofobj

	  ets:

   ///ToDo : ets contains a list of tacs to be done before m can be done

          NOT IMPL. -- "error: do other step before"

   NotLocatable: thus generate_hard

*)

(*WN161112 blanks between list elements left as is until istate is introduced here*)

fun locate_gen (thy', _) (Tac.Rewrite' (_, ro, er, pa, thm, f, _)) (pt, p) 

	    (Celem.Rfuns {locate_rule=lo,...}, _) (Selem.RrlsState (_,f'',rss,rts), _) = 

    (case lo rss f (Celem.Thm thm) of

	    [] => NotLocatable

    | rts' => Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))

  | locate_gen (thy', srls) m (pt, p)

	    (scr as Celem.Prog (_ $ body),d) (Selem.ScrState (E,l,a,v,S,b), ctxt)  = 

    let val thy = Celem.assoc_thy thy';

    in case if l = [] orelse (

		       (*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res)

	       then (assy (thy',ctxt,srls,d,Aundef) ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]) body)

	       else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]) ) of

	    Assoc ((is as (_,_,_,_,_,strong_ass), ss as (_ :: _))) =>

	      (if strong_ass

         then (Steps (Selem.ScrState is, ss))

	       else

           if rew_only ss (*andalso 'not strong_ass'= associated weakly*)

	         then

             let

               val (po,p_) = p

               val po' = case p_ of Frm => po | Res => lev_on po | _ => error ("locate_gen " ^ pos_2str p_)

               val (p'',c'',f'',pt'') = Generate.generate1 thy m (Selem.ScrState is, ctxt) (po',p_) pt

	           in Steps (Selem.ScrState is, [(m, f'',pt'',p'',c'')]) end

	         else Steps (Selem.ScrState is, ss))

    | NasApp _ => NotLocatable

    | err => error ("not-found-in-script: NotLocatable from " ^ @{make_string} err)

    end

  | locate_gen _ m _ (sc,_) (is, _) = 

    error ("locate_gen: wrong arguments,\n tac= " ^ Tac.tac_2str m ^ ",\n " ^

      "scr= " ^ Celem.scr2str sc ^ ",\n istate= " ^ Selem.istate2str is);

(** find the next stactic in a script **)

(*appy, nxt_up, nstep_up scanning for next_tac.

  search is clearly separated into (1)-(2):

  (1) appy is recursive descent;

  (2) nxt_up resumes interpretation at a location somewhere in the script;

      nstep_up does only get to the parentnode of the scriptexpr.

  consequence:

  * call of (2) means _always_ that in this branch below

    there was an applicable stac (Repeat, Or e1, ...)

*)

datatype appy =    (* ExprVal in the sense of denotational semantics  *)

    Appy of        (* applicable stac found, search stalled           *)

    Tac.tac_ *     (* tac_ associated (fun assod) with stac           *)

    Selem.scrstate (* after determination of stac WN.18.8.03          *)

  | Napp of        (* stac found was not applicable; 

	                    this mode may become Skip in Repeat, Try and Or *)

    LTool.env      (* popped while nxt_up                             *)

  | Skip of        (* for restart after Appy, for leaving iterations,

	                    for passing the value of scriptexpressions,

		                  and for finishing the script successfully       *)

    term * LTool.env  (*a stack*);

datatype appy_ = (* as argument in nxt_up, nstep_up, from appy               *)

(*Appy              is only (final) returnvalue, not argument during search  *)

  Napp_          (* ev. detects 'script is not appropriate for this example' *)

| Skip_;         (* detects 'script successfully finished'

		                also used as init-value for resuming; this works,

	                  because 'nxt_up Or e1' treats as Appy                    *)

fun appy thy ptp E l (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =

    (case appy thy ptp E (l @ [Celem.L, Celem.R]) e a v of

      Skip (res, E) => 

        let val E' = LTool.upd_env E (Free (i,T), res);

        in appy thy ptp E' (l @ [Celem.R, Celem.D]) b a v end

    | ay => ay)

  | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*1*),_) $ c $ e $ a) _ v =

    (if Rewrite.eval_true_ th sr (subst_atomic (LTool.upd_env E (a,v)) c)

     then appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v

     else Skip (v, E))

  | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*2*),_) $ c $ e) a v =

    (if Rewrite.eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)

     then appy thy ptp E (l @ [Celem.R]) e a v

     else Skip (v, E))

  | appy (thy as (th,sr)) ptp E l (Const ("If",_) $ c $ e1 $ e2) a v =

    (if Rewrite.eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)

     then appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v

     else appy thy ptp E (l @ [Celem.R]) e2 a v)

  | appy thy ptp E l (Const ("Script.Repeat"(*1*),_) $ e $ a) _ v = 

    appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v

  | appy thy ptp E l (Const ("Script.Repeat"(*2*),_) $ e) a v = appy thy ptp E (l @ [Celem.R]) e a v

  | appy thy ptp E l (Const ("Script.Try",_) $ e $ a) _ v =

    (case appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v of

      Napp E => (Skip (v, E))

    | ay => ay)

  | appy thy ptp E l(Const ("Script.Try",_) $ e) a v =

    (case appy thy ptp E (l @ [Celem.R]) e a v of

      Napp E => (Skip (v, E))

    | ay => ay)

  | appy thy ptp E l (Const ("Script.Or"(*1*),_) $e1 $ e2 $ a) _ v =

    (case appy thy ptp E (l @ [Celem.L, Celem.L, Celem.R]) e1 (SOME a) v of

	    Appy lme => Appy lme

    | _ => appy thy ptp E (*LTool.env*) (l @ [Celem.L, Celem.R]) e2 (SOME a) v)

  | appy thy ptp E l (Const ("Script.Or"(*2*),_) $e1 $ e2) a v =

    (case appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v of

	    Appy lme => Appy lme

    | _ => appy thy ptp E (l @ [Celem.R]) e2 a v)

  | appy thy ptp E l (Const ("Script.Seq"(*1*),_) $ e1 $ e2 $ a) _ v =

    (case appy thy ptp E (l @ [Celem.L, Celem.L, Celem.R]) e1 (SOME a) v of

	    Skip (v,E) => appy thy ptp E (l @ [Celem.L, Celem.R]) e2 (SOME a) v

    | ay => ay)

  | appy thy ptp E l (Const ("Script.Seq",_) $ e1 $ e2) a v =

    (case appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v of

	    Skip (v,E) => appy thy ptp E (l @ [Celem.R]) e2 a v

    | ay => ay)

  (* a leaf has been found *)   

  | appy ((th,sr)) (pt, p) E l t a v =

    case handle_leaf "next  " th sr E a v t of

	    (_, LTool.Expr s) => Skip (s, E)

    | (a', LTool.STac stac) =>

	    let val (m,m') = stac2tac_ pt (Celem.assoc_thy th) stac

      in case m of 

	      Tac.Subproblem _ => Appy (m', (E,l,a',tac_2res m',Selem.Sundef,false))

	    | _ =>

        (case Applicable.applicable_in p pt m of

		       Chead.Appl m' => (Appy (m', (E,l,a',tac_2res m',Selem.Sundef,false)))

		     | _ => Napp E)

	    end

(*GOON*)

fun nxt_up thy ptp (scr as (Celem.Prog sc)) E l ay (Const ("HOL.Let", _) $ _) a v = (*comes from let=...*)

    if ay = Napp_

    then nstep_up thy ptp scr E (drop_last l) Napp_ a v

    else (*Skip_*)

	    let

        val up = drop_last l

        val (i, T, body) =

          (case go up sc of

             Const ("HOL.Let",_) $ _ $ (Abs aa) => aa

           | t => error ("nxt_up..HOL.Let $ _ with " ^ Celem.term2str t))

        val i = TermC.mk_Free (i, T)

        val E = LTool.upd_env E (i, v)

      in

        case appy thy ptp E (up @ [Celem.R, Celem.D]) body a v  of

	        Appy lre => Appy lre

	      | Napp E => nstep_up thy ptp scr E up Napp_ a v

	      | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v

	    end

  | nxt_up thy ptp scr E l ay (Abs _) a v =  nstep_up thy ptp scr E l ay a v

  | nxt_up thy ptp scr E l ay (Const ("HOL.Let",_) $ _ $ (Abs _)) a v =

    nstep_up thy ptp scr E l ay a v

  (*no appy_: never causes Napp -> Helpless*)

  | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Script.While"(*1*), _) $ c $ e $ _) a v = 

    if Rewrite.eval_true_ th sr (subst_atomic (upd_env_opt E (a, v)) c) 

    then case appy thy ptp E (l @ [Celem.L, Celem.R]) e a v of

	     Appy lr => Appy lr

	  | Napp E => nstep_up thy ptp scr E l Skip_ a v

	  | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v

    else nstep_up thy ptp scr E l Skip_ a v

  (*no appy_: never causes Napp - Helpless*)

  | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Script.While"(*2*), _) $ c $ e) a v = 

    if Rewrite.eval_true_ th sr (subst_atomic (upd_env_opt E (a, v)) c) 

    then case appy thy ptp E (l @ [Celem.R]) e a v of

	    Appy lr => Appy lr

	  | Napp E => nstep_up thy ptp scr E l Skip_ a v

	  | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v

    else nstep_up thy ptp scr E l Skip_ a v

  | nxt_up thy ptp scr E l ay (Const ("If", _) $ _ $ _ $ _) a v = nstep_up thy ptp scr E l ay a v

  | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)

      (Const ("Script.Repeat"(*1*), _) $ e $ _) a v =

    (case appy thy ptp (*upd_env*) E (*a,v)*) (l @ [Celem.L, Celem.R]) e a v  of

      Appy lr => Appy lr

    | Napp E =>  nstep_up thy ptp scr E l Skip_ a v

    | Skip (v,E) =>  nstep_up thy ptp scr E l Skip_ a v)

  | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)

      (Const ("Script.Repeat"(*2*), _) $ e) a v =

    (case appy thy ptp (*upd_env*) E (*a,v)*) (l @ [Celem.R]) e a v  of

      Appy lr => Appy lr

    | Napp E => nstep_up thy ptp scr E l Skip_ a v

    | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v)

  | nxt_up thy ptp scr E l _ (Const ("Script.Try",_) $ _ $ _) a v = (*makes Napp to Skip*)

    nstep_up thy ptp scr E l Skip_ a v

  | nxt_up thy ptp scr E l _ (Const ("Script.Try"(*2*), _) $ _) a v = (*makes Napp to Skip*)

    nstep_up thy ptp scr E l Skip_ a v