(* Title:  interpreter for scripts

   Author: Walther Neuper 2000

   (c) due to copyright terms

12345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80

*)

signature INTERPRETER =

sig

  (*type ets (list of executed tactics) see sequent.sml*)

  datatype locate

    = NotLocatable

    | Steps of (tac_ * mout * ptree * pos' * cid * safe (* ets*)) list

(*    | ToDo of ets 28.4.02*)

  (*diss: next-tactic-function*)

  val next_tac : theory' -> ptree * pos' -> metID -> scr -> ets -> tac_

  (*diss: locate-function*)

  val locate_gen : theory'

                   -> tac_

                      -> ptree * pos' -> scr * rls -> ets -> loc_ -> locate

  val sel_rules : ptree -> pos' -> tac list

  val init_form : scr -> ets -> loc_ * term option (*FIXME not up to date*)

  val formal_args : term -> term list

  (*shift to library ...*)

  val inst_abs : theory' -> term -> term

  val itms2args : metID -> itm list -> term list

  val user_interrupt : loc_ * (tac_ * env * env * term * term * safe)

  (*val empty : term*) 

end 

(*

structure Interpreter : INTERPRETER =

struct

*)

(*.traces the leaves (ie. non-tactical nodes) of the script

   found by next_tac.

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

   where 'exp' does not contain a tactic.*)   

val trace_script = Unsynchronized.ref false;

type step =     (*data for creating a new node in the ptree;

		 designed for use:

               	 fun ass* scrstate steps =

               	 ... case ass* scrstate steps of

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

    tac_       (*transformed from associated tac*)

    * mout       (*result with indentation etc.*)

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

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

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

val e_step = (Empty_Tac_, EmptyMout, EmptyPtree, e_pos',[]:pos' list):step;

fun rule2thm' (Thm (id, thm)) = (id, string_of_thmI thm):thm'

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

fun rule2rls' (Rls_ rls) = id_rls rls

  | rule2rls' r = error ("rule2rls': not defined for "^(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 = assoc_thy thy'

        val ctxt = get_ctxt pt p |> insert_assumptions am

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

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

	      val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)

	      val (p', cid, mout, pt') = 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 = assoc_thy thy'

        val ctxt = get_ctxt pt p |> insert_assumptions am

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

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

	      val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)

	      val (p', cid, mout, pt') = 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;

(*. functions for the environment stack .*)

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

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

fun updateenv id vl (es:env stack) = 

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

fun pushenv id vl (es:env stack) = 

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

val popenv = pop:env stack -> 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;

(*

> val str = "Rewrite_Set_Inst";

> val esc = esc_underscore str;

val it = "Rewrite'_Set'_Inst" : string

> val des = de_esc_underscore esc;

 val des = de_esc_underscore esc;*)

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

fun go [] t = t

  | go (D::p) (Abs(s,ty,t0)) = go (p:loc_) t0

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

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

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

(*

> val t = (term_of o the o (parse thy)) "a+b";

val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term

> val plus_a = go [L] t; 

> val b = go [R] t; 

> val plus = go [L,L] t; 

> val a = go [L,R] t;

> val t = (term_of o the o (parse thy)) "a+b+c";

val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term

> val pl_pl_a_b = go [L] t; 

> val c = go [R] t; 

> val a = go [L,R,L,R] t; 

> val b = go [L,R,R] t; 

*)

(* get a subterm t with test t, and record location *)

fun get l test (t as Const (s,T)) = 

    if test t then SOME (l,t) else NONE

  | get l test (t as Free (s,T)) = 

    if test t then SOME (l,t) else NONE 

  | get l test (t as Bound n) =

    if test t then SOME (l,t) else NONE 

  | get l test (t as Var (s,T)) =

    if test t then SOME (l,t) else NONE

  | get l test (t as Abs (s,T,body)) =

    if test t then SOME (l:loc_,t) else get ((l@[D]):loc_) test body

  | get l test (t as t1 $ t2) =

    if test t then SOME (l,t) 

    else case get (l@[L]) test t1 of 

      NONE => get (l@[R]) test t2

    | SOME (l',t') => SOME (l',t');

(*18.6.00

> val sss = ((term_of o the o (parse thy))

  "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\

   \ (let e_ = Try (Rewrite square_equation_left True eq_) \

   \  in [e_])");

          ______ compares head_of !!

> get [] (eq_str "HOL.Let") sss;            [R]

> get [] (eq_str "Script.Try") sss;     [R,L,R]

> get [] (eq_str "Script.Rewrite") sss; [R,L,R,R]

> get [] (eq_str "HOL.True") sss;           [R,L,R,R,L,R]

> get [] (eq_str "e_") sss;             [R,R]

*)

fun test_negotiable t = 

    member op = (!negotiable) 

           ((strip_thy o (term_str (Thy_Info.get_theory "Script")) o head_of) t);

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

fun get_stac thy (h $ 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",_) $ c $ e) a = get_t y e a

      | get_t y (Const ("Script.While",_) $ c $ 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 (_,_,e2)) a =

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

      | get_t y (Const ("If",_) $ c $ e1 $ e2) a = NONE

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      | get_t y x _ =  

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

	 NONE)

in get_t thy body e_term end;

fun init_form thy (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";

(*the 'iteration-argument' of a stac (args not eval)*)

fun itr_arg _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ v) = v

  | itr_arg _ (Const ("Script.Rewrite",_) $ _ $ _ $ v) = v

  | itr_arg _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $ v) = v

  | itr_arg _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ v) = v

  | itr_arg _ (Const ("Script.Calculate",_) $ _ $ v) = v

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

  | itr_arg _ (Const ("Script.Or'_to'_List",_) $ _) = e_term

  | itr_arg _ (Const ("Script.Tac",_) $ _) = e_term

  | itr_arg _ (Const ("Script.SubProblem",_) $ _ $ _) = e_term

  | itr_arg thy t = error ("itr_arg not impl. for " ^ term_to_string'' thy t);

(* val t = (term_of o the o (parse thy))"Rewrite rroot_square_inv False e_";

> itr_arg "Script" t;

val it = Free ("e_","RealDef.real") : term 

> val t = (term_of o the o (parse thy))"xxx";

> itr_arg "Script" t;

*** itr_arg not impl. for xxx

uncaught exception ERROR

  raised at: library.ML:1114.35-1114.40*)

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

(*

> formal_args scr;

  [Free ("f_","RealDef.real"),Free ("v_","RealDef.real"),

   Free ("eqs_","bool List.list")] : term list

*)

(*.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 eva-_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) = upd_env env (a,v)

  | upd_env_opt env (NONE, v) = 

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

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

fun typ_str (Type (s,_)) = s

  | typ_str (TFree(s,_)) = s

  | typ_str (TVar ((s,i),_)) = s ^ (string_of_int i);

(*get the _result_-type of a description*)

fun dsc_valT (Const (_,(Type (_,[_,T])))) = (strip_thy o typ_str) T;

(*> val t = (term_of o the o (parse thy)) "equality";

> val T = type_of t;

val T = "bool => Tools.una" : typ

> val dsc = dsc_valT t;

val dsc = "una" : string

> val t = (term_of o the o (parse thy)) "fixedValues";

> val T = type_of t;

val T = "bool List.list => Tools.nam" : typ

> val dsc = dsc_valT t;

val dsc = "nam" : string*)

(*.from penv in itm_ make args for script depending on type of description.*)

(*6.5.03 TODO: push penv into script -- and drop mk_arg here || drop penv

  9.5.03 penv postponed: penv = env for script at the moment, (*mk_arg*)*)

fun mk_arg thy d [] = 

    error ("mk_arg: no data for " ^ term_to_string''' thy d)

  | mk_arg thy d [t] = 

    (case dsc_valT d of

	     "una" => [t]

     | "nam" => 

	     [case t of

	        r as (Const ("HOL.eq",_) $ _ $ _) => r

	      | _ => error ("mk_arg: dsc-typ 'nam' applied to non-equality " ^ term_to_string''' thy t)]

        | s => error ("mk_arg: not impl. for "^s))

  | mk_arg thy d (t::ts) = (mk_arg thy d [t]) @ (mk_arg thy d ts);

(* 

 val d = d_in itm_;

 val [t] = ts_in itm_;

mk_arg 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);

   *)

fun itms2args thy mI (itms:itm list) =

    let val mvat = 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 = d_in itm_)

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

	    case find_first (test_dsc d) itms of

		NONE => 

		error ("itms2args: '"^term2str d^"' not in itms")

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

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

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

	fun sel_given_find (s,_) = (s = "#Given") orelse (s = "#Find")

	val pats = (#ppc o get_met) mI

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

(*

> val sc = ... Solve_root_equation ...

> val mI = ("Script","sqrt-equ-test");

> val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];

> val ts = itms2args thy mI itms;

> map (term_to_string''' thy) ts;

["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list

*)

(*detour necessary, because generate1 delivers a string-result*)

fun mout2term thy (Form' (FormKF (_,_,_,_,res))) = 

  (term_of o the o (parse (assoc_thy thy))) res

  | mout2term thy (Form' (PpcKF _)) = e_term;(*3.8.01: res of subpbl 

					   at time of detection in script*)

(*.convert a script-tac 'stac' to a tactic 'tac'; if stac is an initac,

   then convert to a 'tac_' (as required in appy).

   arg pt:ptree for pushing the thy specified in rootpbl into subpbls.*)

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

      let

        val tid = (de_esc_underscore o strip_thy) thmID

      in (Rewrite (tid, (string_of_thmI o (assoc_thm' thy)) (tid,"")), Empty_Tac_)

      end

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

      let

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

        val subStr = subst2subs subML

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

      in (Rewrite_Inst (subStr, (tid, (string_of_thmI o (assoc_thm' thy)) (tid,""))), Empty_Tac_)

      end

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

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

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

      let

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

        val subStr = subst2subs subML;

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

  | stac2tac_ pt thy (Const ("Script.Calculate",_) $ Free (op_,_) $ f) =

      (Calculate op_, Empty_Tac_)

  | stac2tac_ pt thy (Const ("Script.Take",_) $ t) =

      (Take (term2str t), Empty_Tac_)

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

      (Substitute ((subte2sube o isalist2list) isasub), Empty_Tac_)

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

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

        (Check_elementwise (term_to_string''' thy pred), (*set*)Empty_Tac_)

  | stac2tac_ pt thy (Const("Script.Or'_to'_List",_) $ _ ) = 

      (Or_to_List, Empty_Tac_)

    (*12.1.01.for subproblem_equation_dummy in root-equation *)

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

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

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

  | stac2tac_ pt thy (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 = maxthy (assoc_thy dI) (rootthy pt);

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

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

	      val ags = isalist2list ags';

	      val (pI, pors, mI) = 

	        if mI = ["no_met"] 

	        then

            let

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

			          handle ERROR "actual args do not match formal args" 

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

		          val pI' = refine_ori' pors pI;

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

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

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

		        handle ERROR "actual args do not match formal args"

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

        val (fmz_, vals) = oris2fmz_vals pors;

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

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

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

        val ctxt = Proof_Context.init_global 

        val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global 

          |> declare_constraints' vals

	      val hdl =

          case cas of

		        NONE => pblterm dI pI

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

        val f = subpbl (strip_thy dI) pI

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

      end

  | stac2tac_ pt thy t = error 

      ("stac2tac_ TODO: no match for " ^ term_to_string''' thy t);

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

(*test a term for being a _list_ (set ?) of constants; could be more rigorous*)

fun list_of_consts (Const ("List.list.Cons",_) $ _ $ _) = true

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

  | list_of_consts _ = false;

(*val ttt = (term_of o the o (parse thy)) "[x=#1,x=#2,x=#3]";

> list_of_consts ttt;

val it = true : bool

> val ttt = (term_of o the o (parse thy)) "[]";

> list_of_consts ttt;

val it = true : bool*)

datatype ass = 

    Ass of

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

  	  term     (* for itr_arg, result in ets *)

  | AssWeak of

      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     : ptree 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 pt d (m as Rewrite_Inst' (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm))) stac =

      (case stac of

	       (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$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",_) $ sub_ $ Free (rls_,_) $_$f_) =>

	          if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_)

            then 

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

	          else NotAss

       | _ => NotAss)

  | assod pt d (m as Rewrite' (thy,rod,rls,put,(thmID,thm),f,(f',asm))) stac =

      (case stac of

	       (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ 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 contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_)

            then

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

	          else NotAss

       | _ => NotAss)

  | assod pt d (m as Rewrite_Set_Inst' (thy',put,sub,rls,f,(f',asm))) 

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

      if id_rls rls = rls_ 

      then 

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

      else NotAss

  | assod pt d (m as Detail_Set_Inst' (thy',put,sub,rls,f,(f',asm))) 

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

      if id_rls rls = rls_

      then 

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

      else NotAss

  | assod pt d (m as Rewrite_Set' (thy,put,rls,f,(f',asm))) 

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

      if id_rls rls = rls_

      then 

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

      else NotAss

  | assod pt d (m as Detail_Set' (thy,put,rls,f,(f',asm))) 

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

      if id_rls rls = rls_

      then 

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

      else NotAss

  | assod pt d (m as Calculate' (thy',op_,f,(f',thm'))) 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",_) $ sub_ $ Free(rls_,_) $_$f_)  => 

	         if contains_rule (Calc (assoc_calc' op_ |> snd)) (assoc_rls rls_)

           then

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

	         else NotAss

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

	         if contains_rule (Calc (assoc_calc' op_ |> snd)) (assoc_rls rls_)

           then

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

	         else NotAss

       | _ => NotAss)

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

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

      if consts = consts'

      then Ass (m, consts_chkd)

      else NotAss

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

	    Ass (m, list) 

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

	    Ass (m, term)

  | assod pt _ (m as 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 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 (Substitute' (ro, erls, subte, t, t'), t')

		      end

		    else (case rewrite_terms_ (Isac()) ro erls subte t of

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

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

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

      if id = id'

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

      else NotAss

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

  | assod pt _ (Subproblem' ((domID,pblID,metID),_,_,_,_,f))

	  (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 = maxthy (assoc_thy dI) (rootthy pt);

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

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

	      val ags = isalist2list ags';

	      val (pI, pors, mI) = 

	        if mI = ["no_met"] 

	        then

            let

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

			          handle ERROR "actual args do not match formal args"

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

		          val pI' = refine_ori' pors pI;

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

		            (hd o #met o get_pbt) pI')

            end

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

		        handle ERROR "actual args do not match formal args"

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

        val (fmz_, vals) = oris2fmz_vals pors;

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

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

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

	      val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global 

          |> declare_constraints' vals

	      val hdl = 

          case cas of

		        NONE => pblterm dI pI

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

        val f = subpbl (strip_thy dI) pI

      in 

        if domID = dI andalso pblID = pI

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

        else NotAss

      end

  | assod pt d m t = 

      (if (!trace_script) 

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

		     "@@@ tac_ = "^(tac_2str m))

       else ();

       NotAss);

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

  | tac_2tac (Model_Problem' (pI,_,_))      = Model_Problem

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

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

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

  | tac_2tac (Specify_Theory' dI)           = Specify_Theory dI

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

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

  | tac_2tac (Rewrite' (thy,rod,erls,put,(thmID,thm),f,(f',asm))) = Rewrite (thmID,thm)

  | tac_2tac (Rewrite_Inst' (thy,rod,erls,put,sub,(thmID,thm),f,(f',asm)))=

      Rewrite_Inst (subst2subs sub,(thmID,thm))

  | tac_2tac (Rewrite_Set' (thy,put,rls,f,(f',asm))) = Rewrite_Set (id_rls rls)

  | tac_2tac (Detail_Set' (thy,put,rls,f,(f',asm))) = Detail_Set (id_rls rls)

  | tac_2tac (Rewrite_Set_Inst' (thy,put,sub,rls,f,(f',asm))) = 

      Rewrite_Set_Inst (subst2subs sub,id_rls rls)

  | tac_2tac (Detail_Set_Inst' (thy,put,sub,rls,f,(f',asm))) = 

      Detail_Set_Inst (subst2subs sub,id_rls rls)

  | tac_2tac (Calculate' (thy,op_,t,(t',thm'))) = Calculate (op_)

  | tac_2tac (Check_elementwise' (consts,pred,consts')) = Check_elementwise pred

  | tac_2tac (Or_to_List' _) = Or_to_List

  | tac_2tac (Take' term) = Take (term2str term)

  | tac_2tac (Substitute' (_, _, subte, t, res)) = Substitute (subte2sube subte) 

  | tac_2tac (Tac_ (_,f,id,f')) = Tac id

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

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

  | tac_2tac Empty_Tac_ = Empty_Tac

  | tac_2tac m = 

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

(** decompose tac_ to a rule and to (lhs,rhs)

    unly needed                          --- **)

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

(*val tt = (term_of o the o (parse thy)) "square_equation_left::ID";

type_of tt = idT;

val it = true : bool

*)

fun make_rule thy t =

  let val ct = cterm_of thy (Trueprop $ t)

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

(* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m;

   *)

(*decompose tac_ to a rule and to (lhs,rhs) for ets FIXME.12.03: obsolete!

 NOTE.12.03: also used for msg 'not locatable' ?!: 'Subproblem' missing !!!

WN0508 only use in tac_2res, which uses only last return-value*)

fun rep_tac_ (Rewrite_Inst' 

		 (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm))) = 

  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' = list2isalist (HOLogic.mk_prodT (sT, sT))

      (map HOLogic.mk_prod subs);

    val sT' = type_of subs';

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

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

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

(*Fehlersuche 25.4.01

(a)----- als String zusammensetzen:

ML> term2str f; 

val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string

ML> term2str f'; 

val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string

ML> subs;

val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst

> val tt = (term_of o the o (parse thy))

  "(Rewrite_Inst[(bdv,x)]diff_const False(d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))";

> atomty tt;

ML> tracing (term2str tt); 

(Rewrite_Inst [(bdv,x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =

 #0 + d_d x (x ^^^ #2 + #3 * x)

(b)----- laut rep_tac_:

> val ttt=HOLogic.mk_eq (lhs,f');

> atomty ttt;

(*Fehlersuche 1-2Monate vor 4.01:*)

> val tt = (term_of o the o (parse thy))

  "Rewrite_Inst[(bdv,x)]square_equation_left True(x=#1+#2)";

> atomty tt;

> val f = (term_of o the o (parse thy)) "x=#1+#2";

> val f' = (term_of o the o (parse thy)) "x=#3";

> val subs = [((term_of o the o (parse thy)) "bdv",

	       (term_of o the o (parse thy)) "x")];

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

> val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))

			      (map HOLogic.mk_prod subs);

> val sT' = type_of subs';

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

  $ subs' $ Free (thmID,idT) $ @{term True} $ f;

> lhs = tt;

val it = true : bool

> rep_tac_ (Rewrite_Inst' 

	       ("Script","tless_true","eval_rls",false,subs,

		("square_equation_left",""),f,(f',[])));

*)

  | rep_tac_ (Rewrite' (thy',rod,rls,put,(thmID,thm),f,(f',asm)))=

  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 (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end

(* 

> val tt = (term_of o the o (parse thy)) (*____   ____..test*)

  "Rewrite square_equation_left True (x=#1+#2) = (x=#3)";

> val f = (term_of o the o (parse thy)) "x=#1+#2";

> val f' = (term_of o the o (parse thy)) "x=#3";

> val Thm (id,thm) = 

  rep_tac_ (Rewrite' 

   ("Script","tless_true","eval_rls",false,

    ("square_equation_left",""),f,(f',[])));

> val SOME ct = parse thy   

  "Rewrite square_equation_left True (x=#1+#2)"; 

> rewrite_ Script.thy tless_true eval_rls true thm ct;

val it = SOME ("x = #3",[]) : (cterm * cterm list) option

*)

  | rep_tac_ (Rewrite_Set_Inst' 

		 (thy',put,subs,rls,f,(f',asm))) =

    (e_rule, (e_term, f'))

(*WN050824: type error ...

  let val fT = type_of f;

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

    val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))

      (map HOLogic.mk_prod subs);

    val sT' = type_of subs';

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

    val lhs = Const ("Script.Rewrite'_Set'_Inst",

		     [sT',idT,fT,fT] ---> fT) 

      $ subs' $ Free (id_rls rls,idT) $ b $ f;

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

(* ... vals from Rewrite_Inst' ...

> rep_tac_ (Rewrite_Set_Inst' 

	       ("Script",false,subs,

		"isolate_bdv",f,(f',[])));

*)

(* val (Rewrite_Set' (thy',put,rls,f,(f',asm)))=m;

*)

  | rep_tac_ (Rewrite_Set' (thy',put,rls,f,(f',asm)))=

  let val fT = type_of f;

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

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

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

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

(* 13.3.01:

val thy = assoc_thy thy';

val t = HOLogic.mk_eq (lhs,f');

make_rule thy t;

--------------------------------------------------

val lll = (term_of o the o (parse thy)) 

  "Rewrite_Set SqRoot_simplify False (d_d x (x ^^^ #2 + #3 * x) + d_d x #4)";

--------------------------------------------------

> val f = (term_of o the o (parse thy)) "x=#1+#2";

> val f' = (term_of o the o (parse thy)) "x=#3";

> val Thm (id,thm) = 

  rep_tac_ (Rewrite_Set' 

   ("Script",false,"SqRoot_simplify",f,(f',[])));

val id = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : string

val thm = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : thm

*)

  | rep_tac_ (Calculate' (thy',op_,f,(f',thm')))=

  let val fT = type_of f;

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

      $ Free (op_,idT) $ f

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

(*

> val lhs'=(term_of o the o (parse thy))"Calculate plus (#1+#2)";

  ... test-root-equ.sml: calculate ...

> val Appl m'=applicable_in p pt (Calculate "PLUS");

> val (lhs,_)=tac_2etac m';

> lhs'=lhs;

val it = true : bool*)

  | rep_tac_ (Check_elementwise' (t,str,(t',asm)))  = (Erule, (e_term, t'))

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

  | rep_tac_ (Take' (t'))  = (Erule, (e_term, t'))

  | rep_tac_ (Substitute' (_, _, subst,t,t'))  = (Erule, (t, t'))

  | rep_tac_ (Or_to_List' (t, t'))  = (Erule, (t, t'))

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

				 (tac_2str m));

(*"N.3.6.03------

fun tac_2rule m = (fst o rep_tac_) m;

fun tac_2etac m = (snd o rep_tac_) m;

fun tac_2tac m = (fst o snd o rep_tac_) m;*)

fun tac_2res m = (snd o snd o rep_tac_) m;(*ONLYuse of rep_tac_

					        FIXXXXME: simplify rep_tac_*)

(* 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 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 subst_stacexpr E a v t of

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

	         let val stac' =

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

	         in

             (if (!trace_script) 

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

	            else ();

	            (a', STac stac'))

	         end

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

	         let val lexpr' =

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

	         in

             (if (!trace_script) 

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

	            else ();

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

	         end;

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

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

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

  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 ptree)*)

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

  scrstate * (step list)

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

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

		 evaluate scriptexpressions*)

  term * 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.

*)

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

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

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

	         let

             val id' = mk_Free (id, T);

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

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

       | NasNap (v,E) =>

	         let

             val id' = mk_Free (id, T);

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

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

       | ay => ay)

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

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

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

       else NasNap (v, E))   

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

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

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

       else NasNap (v, E)) 

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

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

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

       else assy ya ((E, l@[  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@[L,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@[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@[L,L,R], SOME a,v,S,b),ss) e1 of

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

       | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l@[L,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@[L,R], a,v,S,b),ss) e1 of

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

       | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l@[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@[L,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@[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@[L,L,R]),SOME a,v,S,b),ss) e1 of

	       NasNap (v, E) => 

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

	            NasNap (v, E) => 

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

	                 NasNap (v, E) => 

	                   assy (y,x,s,sc,AssGen) ((E, (l@[L,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@[L,R]),a,v,S,b),ss) e1 of

	       NasNap (v, E) => assy ya ((E,(l@[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) (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =

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

	       (a', Expr s) => 

	          (NasNap (eval_listexpr_ (assoc_thy thy') sr

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

       | (a', 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') =

                     generate1 (assoc_thy thy') m (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') =

                   generate1 (assoc_thy thy') m (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 =>