(* Title:  Interpret/lucas-interpreter.sml

   Author: Walther Neuper 2019

   (c) due to copyright terms

*)

signature LUCAS_INTERPRETER =

sig

  datatype input_tactic_result =

      Safe_Step of Istate.T * Proof.context * Tactic.T

    | Unsafe_Step of Istate.T * Proof.context * Tactic.T

    | Not_Locatable of string

  val locate_input_tactic : Rule.program -> Ctree.state -> Istate.T -> Proof.context -> Tactic.T

    -> input_tactic_result

(*datatype input_formula_result = FStep of calcstate' | Not_Derivable *)

  datatype input_formula_result =

    Step of Ctree.state * Istate.T * Proof.context

  | Not_Derivable of Chead.calcstate'

(*val locate_input_formula : Ctree.state -> term -> input_formula_result *)

  val locate_input_formula : Rule.program -> Ctree.state -> Istate.T -> Proof.context -> term

    -> input_formula_result

(*val begin_end_prog : ???*)

  val begin_end_prog : Tactic.T -> Istate.T * Proof.context -> Ctree.state ->

    (Tactic.input * Tactic.T * (Ctree.pos' * (Istate.T * Proof.context))) list * Ctree.pos' list * Ctree.state

(*val do_solve_step : Ctree.state -> Ctree.state ???*)

  val do_solve_step : Ctree.state ->

    (Tactic.input * Tactic.T * (Ctree.pos' * (Istate.T * Proof.context))) list * Ctree.pos' list * Ctree.state

  datatype next_tactic_result =

      NStep of Ctree.state * Istate.T * Proof.context * tactic

    | Helpless | End_Program

(*val determine_next_tactic :

    Rule.program -> Ctree.state -> Istate.T -> Proof.context -> next_tactic_result *)

  val determine_next_tactic : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.T * 'a ->

    Tactic.T * (Istate.T * 'a) * (term * Telem.safe)

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

  datatype assoc =

      Assoc of Istate.pstate * Proof.context * Tactic.T

    | NasApp of Istate.pstate * Proof.context * Tactic.T

    | NasNap of  term * Env.T;

  val assoc2str : assoc -> string

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

  datatype appy = Appy of Tactic.T * Istate.pstate | Napp of Env.T | Skip of term * Env.T

  val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'

(*old* )val appy: Rule.theory' * Rule.rls -> Ctree.state -> Istate.pstate -> term -> appy( *old*)

(*new*)val appy: Ctree.state * Rule.theory'(*Proof.context*) -> Istate.pstate -> term -> appy(*new*)

(*old* )val nxt_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> term -> appy( *old*)

(*new*)val nxt_up: Rule.program * (Ctree.state * Rule.theory') -> Istate.pstate -> term -> appy(*new*)

(*old* )val nstep_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> appy( *old*)

(*new*)val nstep_up: Rule.program * (Ctree.state * Rule.theory') -> Istate.pstate -> appy(*new*)

  val go : Celem.loc_ -> term -> term

  val go_up: Celem.loc_ -> term -> term

  val execute_progr_1 : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.T -> appy

  val execute_progr_2 : Rule.rls -> Tactic.T -> Ctree.state -> Rule.program * 'a -> Istate.T * Proof.context -> assoc

  val check_Let_up : Celem.loc_ -> term -> term * term

  val check_Seq_up: Celem.loc_ -> term -> term

(*old* )val assy :  Proof.context * Rule.rls * Ctree.state * Istate.asap -> Istate.pstate * Tactic.T -> term -> assoc( *old*)

(*new*)val assy: (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> assoc(*new*)

(*old* )val ass_up : Proof.context * Rule.rls * Rule.program * Ctree.state -> Istate.pstate * Tactic.T -> term -> assoc( *old*)

(*new*)val ass_up: Rule.program * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> assoc;(*new*)

(*old* )val astep_up : Proof.context * Rule.rls * Rule.program * Ctree.state -> Istate.pstate * Tactic.T -> assoc( *old*)

(*new*)val astep_up: Rule.program * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> assoc;(*new*)

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

end

(**)

structure LucinNEW(**): LUCAS_INTERPRETER(**) = (*LucinNEW \<rightarrow> Lucin after code re-arrangement*)

struct

(**)

open Ctree

open Celem

open Istate

type program = term

(*go to 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);

fun go_up l t =

  if length l > 1 then go (drop_last l) t else raise ERROR ("go_up [] " ^ Rule.term2str t)

fun check_Let_up path prog =

  case go (drop_last path) prog of

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

  | t => raise ERROR ("ass_up..\"HOL.Let $ _\" with: \"" ^ Rule.term2str t ^ "\"")

fun check_Seq_up path prog =

  case go (drop_last path) prog of

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

  | t => raise ERROR ("ass_up..\"Tactical.Seq $ _\" with: \"" ^ Rule.term2str t ^ "\"")

(**** find the next tactic by executing the program ****)

  datatype next_tactic_result = NStep of Ctree.state * Istate.T * Proof.context * tactic

    | Helpless | End_Program

(*appy, nxt_up, nstep_up scanning for determine_next_tactic.

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

    Tactic.T *     (* tac_ associated (fun associate) with stac       *)

    Istate.pstate (* after determination of stac WN.180803          *)

  | Napp of        (* stac found was not applicable; 

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

    Env.T      (* 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 *         (* ???*) 

    Env.T      (* TODO: a stack of env for nested let?            *);

fun appy xxx ist (Const ("HOL.Let"(*1*), _) $ e $ (Abs (i, T, b))) =

     (case appy xxx (ist |> path_down [L, R]) e of

       Skip (res, E) => appy xxx (ist |> path_down [R, D] |> upd_env'' (E , (Free (i, T), res))) b

     | rrr => rrr)

  | appy (xxx as (_, ctxt)) ist (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =

    if Rewrite.eval_true_ ctxt (get_rls ist) (subst_atomic (ist |> get_act_env |> Env.upd_env' a) c)

    then appy xxx (ist |> path_down_form ([L, R], a)) e

    else Skip (get_act_env ist)

  | appy (xxx as (_, ctxt)) ist (Const ("Tactical.While"(*2*), _) $ c $ e) =

    if Rewrite.eval_true_ ctxt (get_rls ist) (subst_atomic (Env.upd_env_opt' (get_subst ist)) c)

    then appy xxx (ist |> path_down [R]) e

    else Skip (get_act_env ist)

  | appy (xxx as (_, ctxt)) ist (Const ("Tactical.If"(*1*), _) $ c $ e1 $ e2) =

    if Rewrite.eval_true_ ctxt (get_rls ist) (subst_atomic (Env.upd_env_opt' (get_subst ist)) c)

    then appy xxx (ist |> path_down [L, R]) e1

    else appy xxx (ist |> path_down [R]) e2

  | appy xxx ist (Const ("Tactical.Repeat"(*1*), _) $ e $ a) = 

    appy xxx (ist |> path_down_form ([L, R], a)) e

  | appy xxx ist (Const ("Tactical.Repeat"(*2*), _) $ e) =

    appy xxx (ist |> path_down [R]) e

  | appy xxx ist (Const ("Tactical.Try"(*1*), _) $ e $ a) =

    (case appy xxx (ist|> path_down_form ([L, R], a)) e of

      Napp E => (Skip (get_act ist, E))

    | ay => ay)

  | appy xxx ist (Const ("Tactical.Try"(*2*), _) $ e) =

    (case appy xxx (ist |> path_down [R]) e of

      Napp E => (Skip (get_act ist, E))

    | ay => ay)

  | appy xxx ist (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =

    (case appy xxx (ist |> path_down_form ([L, L, R], a)) e1 of

	    Appy lme => Appy lme

    | _ => appy xxx (ist |> path_down_form ([L, R], a)) e2)

 | appy xxx ist (Const ("Tactical.Or"(*2*), _) $e1 $ e2) =

    (case appy xxx (ist |> path_down [L, R]) e1 of

	    Appy lme => Appy lme

    | _ => appy xxx (ist |> path_down [R]) e2)

  | appy xxx ist (Const ("Tactical.Seq"(*1*), _) $ e1 $ e2 $ a) =

    (case appy xxx (ist |> path_down_form ([L, L, R], a)) e1 of

	    Skip (v, E) => appy xxx (ist |> path_down_form ([L, R], a) |> upd_act_env (v, E)) e2 (*UPD*)

    | ay => ay)

  | appy xxx ist (Const ("Tactical.Seq"(*2*), _) $ e1 $ e2) =

    (case appy xxx (ist |> path_down [L, R]) e1 of

	    Skip (v, E) => appy xxx (ist |> path_down [R] |> upd_act_env (v, E)) e2

    | ay => ay)

    (*========== a leaf has been found ==========*)   

  | appy ((pt, p), ctxt) ist t =

    case Lucin.handle_leaf "next  " ctxt (get_rls ist) (get_subst ist) t of

	    (_, Celem.Expr s) => Skip (s, get_env ist)

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

	    let

	      val (m, m') = Lucin.stac2tac_ pt (Celem.assoc_thy ctxt) stac

      in

        case m of (*TODO?: make applicable_in..Subproblem analogous to other tacs ?refine problem?*)

  	      Tactic.Subproblem _ => Appy (m', ist |> upd_subst_reset (a', Lucin.tac_2res m'))

  	    | _ =>

          (case Applicable.applicable_in p pt m of

  		      Chead.Appl m' => (Appy (m', ist |> upd_subst_reset (a', Lucin.tac_2res m')))

  		    | _ => Napp (get_env ist))

	    end

fun nxt_up (yyy as (Rule.Prog sc, xxx)) ist (Const ("HOL.Let"(*1a*), _) $ _) =

    if get_fini ist = Napp_

    then nstep_up yyy (ist |> path_up)

    else (*Skip_*)

	    let

        val (i, body) = check_Let_up (get_path ist) sc

      in

        case appy xxx (ist |> path_up_down [R, D] |> upd_env' i) body of

	        Appy lre => Appy lre

	      | Napp E => nstep_up yyy (ist |> path_up |> upd_env E)

	      | Skip (v, E) => nstep_up yyy (ist |> path_up |> upd_act_env (v, E) |> upd_appy Skip_)

	    end

  | nxt_up yyy ist (Abs _(*2*)) =  nstep_up yyy ist

  | nxt_up yyy ist (Const ("HOL.Let"(*3*),_) $ _ $ (Abs _)) =

    nstep_up yyy ist

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

  | nxt_up (yyy as (_, xxx as (_, ctxt))) ist (Const ("Tactical.While"(*1*), _) $ c $ e $ _) = 

    if Rewrite.eval_true_ ctxt (get_rls ist) (subst_atomic (Env.upd_env_opt' (get_subst ist)) c) 

    then

      case appy xxx (ist |> path_down [L, R]) e of

  	     Appy lr => Appy lr

  	  | Napp E => nstep_up yyy (ist |> upd_env E |> upd_appy Skip_)

  	  | Skip (v, E) => nstep_up yyy (ist |> upd_act_env (v, E) |> upd_appy Skip_)

    else

      nstep_up yyy (ist |> upd_appy Skip_)

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

  | nxt_up  (yyy as (_, xxx as (_, ctxt))) ist (Const ("Tactical.While"(*2*), _) $ c $ e) = 

    if Rewrite.eval_true_ ctxt (get_rls ist) (subst_atomic (Env.upd_env_opt' (get_subst ist)) c) 

    then

      case appy xxx (ist |> path_down [R]) e of

  	    Appy lr => Appy lr

  	  | Napp E => nstep_up yyy (ist |> upd_env E |> upd_appy Skip_)

  	  | Skip (v, E) => nstep_up yyy (ist |> upd_act_env (v, E) |> upd_appy Skip_)

    else

      nstep_up yyy (ist |> upd_appy Skip_)

  | nxt_up yyy ist (Const ("Tactical.If"(*1*), _) $ _ $ _ $ _) = nstep_up yyy ist

    (* no appy_: there was already a stac below *)

  | nxt_up (yyy as (_, xxx)) (ist) (Const ("Tactical.Repeat"(*1*), _) $ e $ _) =

    (case appy xxx (ist |> path_down [L, R]) e of

      Appy lr => Appy lr

    | Napp E =>  nstep_up yyy (ist |> upd_env E |> upd_appy Skip_)

    | Skip (v, E) =>  nstep_up yyy (ist |> upd_act_env (v, E) |> upd_appy Skip_))

    (* no appy_: there was already a stac below *)

  | nxt_up  (yyy as (_, xxx)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) =

    (case appy xxx (ist |> path_down [R]) e of

      Appy lr => Appy lr

    | Napp E => nstep_up yyy (ist |> upd_env E |> upd_appy Skip_)

    | Skip (v, E) => nstep_up yyy (ist |> upd_act_env (v, E) |> upd_appy Skip_))

    (* makes Napp to Skip *)

  | nxt_up yyy ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = nstep_up yyy (ist |> upd_appy Skip_)

  | nxt_up yyy ist (Const ("Tactical.Try"(*2*), _) $ _) = nstep_up yyy (ist |> upd_appy Skip_)

  | nxt_up yyy ist (Const ("Tactical.Or"(*1*), _) $ _ $ _ $ _) = nstep_up yyy ist

  | nxt_up yyy ist (Const ("Tactical.Or"(*2*), _) $ _ $ _) = nstep_up yyy ist

  | nxt_up yyy ist (Const ("Tactical.Or"(*3*), _) $ _ ) = nstep_up yyy ist

  | nxt_up yyy ist (Const ("Tactical.Seq"(*1*), _) $ _ $ _ $ _) = nstep_up yyy ist

  | nxt_up yyy ist (Const ("Tactical.Seq"(*2*), _) $ _ $ _) = nstep_up yyy ist

  | nxt_up (yyy as (Rule.Prog sc, xxx)) ist (Const ("Tactical.Seq"(*3*), _) $ _) =

    if get_fini ist = Napp_

    then nstep_up yyy (ist |> path_up)

    else (*Skip_*)

      let 

        val e2 = check_Seq_up (get_path ist) sc

      in

        case appy xxx (ist |> path_up_down [R]) e2 of

          Appy lr => Appy lr

        | Napp E => nstep_up yyy (ist |> path_up |> upd_env E)

        | Skip (v, E) => nstep_up yyy (ist |> path_up |> upd_act_env (v, E) |> upd_appy Skip_)

      end

  | nxt_up _ _ t = error ("nxt_up not impl for " ^ Rule.term2str t)

and nstep_up (yyy as (Rule.Prog sc, _)) ist = 

    if 1 < length (get_path ist)

    then 

      nxt_up yyy (ist |> path_up) (go_up (get_path ist) sc)

    else (*interpreted to end*)

      if (get_fini ist) = Skip_ then Skip (get_act_env ist) else Napp (get_env ist) 

  | nstep_up _ ist = error ("nstep_up: uncovered fun-def at " ^ Celem.loc_2str (get_path ist))

        fun execute_progr_1 thy ptp (sc as Rule.Prog prog) (Istate.Pstate ist) =

          if 0 = length (get_path ist)

(*old* )   then appy thy ptp (trans_scan_down2 ist) (Program.body_of prog)( *old*)

(*new*)   then appy (ptp, (fst thy)) (trans_scan_down2 ist)(*sets AppUndef?!?*) (Program.body_of prog)(*new*)

(*old* )   else nstep_up thy ptp sc (trans_scan_up2 ist) Skip_( *old*)

(*new*)   else nstep_up (sc, (ptp, (fst thy))) (trans_scan_up2 ist |> upd_appy Skip_)(*sets AppUndef?!?*)(*new*)

        | execute_progr_1 _ _ _ _ = raise ERROR "execute_progr_1: uncovered pattern";

(* decide for the next applicable Prog_Tac in the program *)

fun determine_next_tactic thy (ptp as (pt, (p, _))) sc (Istate.Pstate ist, ctxt) =

   (case execute_progr_1 thy ptp sc (Istate.Pstate ist) of

      Skip (v, _) =>                                                        (* program finished *)

        (case par_pbl_det pt p of

	        (true, p', _) => 

	          let

	            val (_, pblID, _) = get_obj g_spec pt p';

	          in

              (Tactic.Check_Postcond' (pblID, (v, [(*assigned in next step*)])), 

	              (Istate.e_istate, ctxt), (v, Telem.Safe)) 

            end

	      | _ =>

          (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ctxt), (v, Telem.Safe)))

    | Napp _ =>

        (Tactic.Empty_Tac_, (Istate.e_istate, ctxt), (Rule.e_term, Telem.Helpless_))(* helpless *)

    | Appy (m', ist) =>

        (m', (Pstate ist, ctxt), (get_act ist, Telem.Safe)))                  (* found next tac *)

  | determine_next_tactic _ _ _ (is, _) =

    error ("determine_next_tactic: not impl for " ^ (Istate.istate2str is));

(**** locate an input tactic within a program ****)

datatype input_tactic_result =

    Safe_Step of Istate.T * Proof.context * Tactic.T

  | Unsafe_Step of Istate.T * Proof.context * Tactic.T

  | Not_Locatable of string

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

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

  Istate.pstate * (* the current; returned for determine_next_tactic etc. outside ass      *)

  Proof.context *   (* carry from assy via Ass: T * term * Proof.context -> ass to fun solve *)

  Tactic.T          (* the tactic located in the program                                     *)

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

  Istate.pstate * Proof.context *  Tactic.T

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

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

		                   evaluate Prog_Expr                                                    *)

  term * Env.T;

fun assoc2str (Assoc _) = "Assoc"

  | assoc2str (NasNap _) = "NasNap"

  | assoc2str (NasApp _) = "NasApp";

fun assy xxx ist (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))) =

    (case assy xxx (ist |> path_down [L, R]) e of

       NasApp (ist', ctxt, ss) =>

         assy xxx (ist' |> path_down [R, D] |> upd_env' (TermC.mk_Free (id, T)) |> trans_ass ist) b

     | NasNap (v, E) =>

         assy xxx (ist |> path_down [R, D] |> upd_env (Env.upd_env E (TermC.mk_Free (id, T), v))) b

     | ay => ay)

  | assy xxx ist (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =

    if Rewrite.eval_true_ "Isac_Knowledge" (get_rls ist)

      (subst_atomic (ist |> get_act_env |> Env.upd_env' a) c)

    then assy xxx (ist |> path_down [L, R] |> upd_form a) e

    else NasNap (ist |> get_act_env)

  | assy xxx ist (Const ("Tactical.While"(*2*),_) $ c $ e) =

    if Rewrite.eval_true_ "Isac_Knowledge" (get_rls ist) (subst_atomic (Env.upd_env_opt' (get_subst ist)) c) 

    then assy xxx (ist |> path_down [R]) e

    else NasNap (ist |> get_act_env)

  | assy xxx ist (Const ("Tactical.Try"(*1*), _) $ e $ a) =

    (case assy xxx (ist |> path_down_form ([L, R], a)) e of ay => ay) 

  | assy xxx ist (Const ("Tactical.Try"(*2*), _) $ e) =

    (case assy xxx (ist |> path_down [R]) e of ay => ay)

  | assy (xxx as (cstate, _, _)) ist (Const ("Tactical.Seq"(*1*), _) $ e1 $ e2 $ a) =

    (case assy xxx (ist |> path_down_form ([L, L, R], a)) e1 of

	     NasNap (v, E)

        => assy xxx (ist |> path_down [L, R] |> upd_subst E (a, v)) e2

     | NasApp (ist', ctxt', tac')

       => assy (cstate, ctxt', tac')  (ist |> path_down [L, R] |> trans_env_act ist' |> upd_form a) e2

     | ay => ay)

  | assy (xxx as (cstate, _, _)) ist (Const ("Tactical.Seq"(*2*), _) $e1 $ e2) =

    (case assy xxx (ist |> path_down [L, R]) e1 of

	     NasNap (v, E) => assy xxx (ist |> path_down [R] |> upd_act_env (v, E)) e2

     | NasApp (ist', ctxt', tac')

        => assy (cstate, ctxt', tac') (ist |> path_down [R] |> trans_env_act ist') e2

     | ay => ay)

  | assy xxx ist (Const ("Tactical.Repeat"(*1*), _) $ e $ a) =

    assy xxx (ist |> path_down [L, R] |> upd_form a) e

  | assy xxx ist (Const ("Tactical.Repeat"(*2*), _) $ e) =

    assy xxx (ist |> path_down [R]) e

  | assy xxx (ist as {or = Aundef, ...}) (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =

    (case assy xxx (ist |> path_down_form ([L, L, R], a) |> upd_or AssOnly) e1 of

	     NasNap (v, E) =>

	       (case assy xxx (ist |> path_down [L, R] |> upd_subst E (a, v) |> upd_or AssOnly) e2 of

	          NasNap (v, E) => 

	            (case assy xxx (ist |> path_down [L, L, R] |> upd_subst E (a, v) |> upd_or AssGen) e1 of

	               NasNap (v, E) => 

	                 assy xxx (ist |> path_down [L, R] |> upd_subst E (a, v) |> upd_or AssGen) e2

	             | ay => ay)

	        | ay =>ay)

     | NasApp _ => raise ERROR ("assy Tactical.Or(*1*): must not return NasApp")

     | ay => (ay))

  | assy xxx ist (Const ("Tactical.Or"(*2*), _) $e1 $ e2) =

    (case assy xxx (ist |> path_down [L, R]) e1 of

	     NasNap (v, E) => assy xxx (ist |> path_down [R] |> upd_act_env (v, E)) e2

     | ay => (ay))

    (*======= end of scanning tacticals, a leaf =======*)

  | assy ((pt, p), ctxt, tac) ist t =

    (case Lucin.handle_leaf "locate" (Context.theory_name (Rule.Isac"")) (get_rls ist) (get_subst ist) t of

	     (a', Celem.Expr _) => 

	       (NasNap (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac_Knowledge") (get_rls ist)

		       (subst_atomic (Env.upd_env_opt'' (get_act_env ist, a')) t), get_env ist))

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

         (case Lucin.associate pt ctxt (tac, stac) of

            (* HERE ----------------vvvv ContextC.insert_assumptions asm ctxt DONE *)

	           Lucin.Ass      (m, v', ctxt) => Assoc (ist |> upd_subst_true  (a', v'), ctxt, m)

           | Lucin.Ass_Weak (m, v', ctxt) => Assoc (ist |> upd_subst_false (a', v'), ctxt, m)

           | Lucin.NotAss =>

             (case get_or ist  of (* switch for Tactical.Or: 1st AssOnly, 2nd AssGen *)

                AssOnly => (NasNap (ist |> get_act_env))

              | _(*Aundef*) =>

                 case Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) of

                    Chead.Appl m' => NasApp (ist |> upd_subst_false (a', Lucin.tac_2res m'), ctxt, tac)

                  | Chead.Notappl _ => (NasNap (ist |> get_act_env)))

    ));

fun ass_up (yyy as (prog as Rule.Prog p, xxx as (cstate, ctxt, tac))) ist (Const ("HOL.Let"(*1*), _) $ _) =

    let 

      val (i, body) = check_Let_up (get_path ist) p

    in case assy xxx (ist |> path_up_down [R, D] |> upd_env' i |> upd_or Aundef) body of

	       Assoc iss => Assoc iss

	     | NasApp (ist', ctxt', tac') => astep_up (prog, (cstate, ctxt', tac')) ist'

	     | NasNap (v, E) => astep_up yyy (ist |> path_up |> upd_act_env (v, E)) 

	  end

  | ass_up yyy ist (Abs(*2*) _) = astep_up yyy ist

  | ass_up yyy ist (Const ("HOL.Let"(*3*), _) $ _ $ (Abs _)) = astep_up yyy ist

    (*all has been done in (*2*) below*)

  | ass_up yyy ist (Const ("Tactical.Seq"(*1*), _) $ _ $ _ $ _) = astep_up yyy ist 

  | ass_up yyy ist (Const ("Tactical.Seq"(*2*), _) $ _ $ _) = astep_up yyy ist (*2*: comes from e2*)

    (* comes from e1, goes to e2 *)

  | ass_up (yyy as (prog as Rule.Prog p, xxx as (cstate, _, _))) ist (Const ("Tactical.Seq"(*3*), _) $ _ ) =

     let 

       val e2 = check_Seq_up (get_path ist) p

     in

       case assy xxx (ist |> path_up_down[R] |> upd_or Aundef) e2 of

         NasNap (v, E) => astep_up yyy (ist |> path_up |> upd_act_env (v, E))

       | NasApp (ist', ctxt', tac') => astep_up (prog, (cstate, ctxt', tac')) ist'

       | zzz => zzz 

     end

  | ass_up yyy ist (Const ("Tactical.Try"(*1*),_) $ _ $ _) = astep_up yyy ist

  | ass_up yyy ist (Const ("Tactical.Try"(*2*),_) $ _) = astep_up yyy ist

  | ass_up (yyy as (prog, xxx as (cstate, _, _))) ist (t as Const ("Tactical.While"(*1*),_) $ c $ e $ a) =

    if Rewrite.eval_true_ "Isac_Knowledge" (get_rls ist) (subst_atomic (Env.upd_env' a (get_act_env ist)) c)

    then

      case assy xxx (ist |> path_down_form ([L, R], a) |> upd_or Aundef) e of 

        NasNap (v, E') => astep_up yyy (ist |> upd_act_env (v, E') |> upd_form a)

      | NasApp (ist', ctxt', tac') => ass_up (prog, (cstate, ctxt', tac')) ist' t

      | ay => ay

    else astep_up yyy (ist |> upd_form a)

  | ass_up (yyy as (prog, xxx as (cstate, _, _))) ist (t as Const ("Tactical.While"(*2*), _) $ c $ e) =

    if Rewrite.eval_true_ "Isac_Knowledge" (get_rls ist) (subst_atomic (Env.upd_env_opt' (get_subst ist)) c)

    then

      case assy xxx (ist |> path_down [R] |> upd_or Aundef) e of 

        NasNap (v, E') => astep_up yyy (ist |> upd_act_env (v, E'))

       | NasApp (ist', ctxt', tac') => ass_up (prog, (cstate, ctxt', tac')) ist' t

       | ay => ay

    else astep_up yyy ist

  | ass_up yyy ist (Const ("If", _) $ _ $ _ $ _) = astep_up yyy ist

  | ass_up (yyy as (prog, xxx as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*1*), _) $ e $ a) =

    (case assy xxx (ist |> path_down_form ([L, R], a) |> upd_or Aundef) e of 

      NasNap (v, E') => astep_up yyy (ist |> upd_form_env (v, E') |> upd_form a)

    | NasApp (ist', ctxt', tac') => ass_up (prog, (cstate, ctxt', tac')) ist' t

    | zzz => zzz)

  | ass_up (yyy as (prog, xxx as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*2*), _) $ e) =

    (case assy xxx (ist |> path_down [R] |> upd_or Aundef) e of

       NasNap (v', E') => astep_up yyy (ist |> upd_act_env (v', E'))

     | NasApp (ist', ctxt', tac') => ass_up (prog, (cstate, ctxt', tac')) ist' t

     | ay => ay)

  | ass_up yyy ist (Const ("Tactical.Or"(*1*), _) $ _ $ _ $ _) = astep_up yyy ist

  | ass_up yyy ist (Const ("Tactical.Or"(*2*), _) $ _ $ _) = astep_up yyy ist

  | ass_up yyy ist (Const ("Tactical.Or"(*3*), _) $ _ ) = astep_up yyy (ist |> path_up)

  | ass_up _ _ t = error ("ass_up not impl for t= " ^ Rule.term2str t)

and astep_up (yyy as (Rule.Prog sc, _)) ist =

    if 1 < length (get_path ist)

    then ass_up yyy (ist |> path_up) (go (get_path_up ist) sc)

    else (NasNap (get_act_env ist))

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

   fun execute_progr_2 _ m (pt, p) (scr as Rule.Prog sc, _) (Istate.Pstate ist, ctxt) =

       if get_path ist = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res)

(*old* )then assy (ctxt,Rule.e_rls, (pt, p), Aundef(*\<rightarrow> Istate*)) (ist |> upd_path [R], m) (Program.body_of sc)( *old*)

(*new*)then assy ((pt, p), ctxt, m) (ist |> upd_path [R] |> upd_or Aundef) (Program.body_of sc)(*new*)

(*old* )else astep_up (ctxt,Rule.e_rls,scr, (pt, p)) (ist, m)( *old*)

(*new*)else astep_up (scr, ((pt, p), ctxt, m)) ist(*new*)

  | execute_progr_2 _ _ _ _ _ = raise ERROR "execute_progr_2: uncovered pattern in fun.def"

fun locate_input_tactic (progr as Rule.Prog _) cstate istate ctxt tac =

    let

      val _ = Lucin.get_simplifier cstate (*TODO: shift into Istate.T*)

    in

      (case execute_progr_2 Rule.e_rls tac cstate (progr, Rule.e_rls) (istate, ctxt) of

         Assoc (ist, ctxt, tac') =>

          if get_assoc ist

          then Safe_Step (Istate.Pstate ist, ctxt, tac')

 	        else Unsafe_Step (Istate.Pstate ist, ctxt, tac')

      | NasApp _ => Not_Locatable (Tactic.tac_2str tac ^ " not locatable")

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

    end

  | locate_input_tactic _ _ _ _ _ = raise ERROR "locate_input_tactic: uncovered case in definition"

(**** locate an input formula in the program ****)

datatype input_formula_result =

    Step of Ctree.state * Istate.T * Proof.context

  | Not_Derivable of Chead.calcstate'

(* FIXME.WN050821 compare fun solve ... fun begin_end_prog

   begin_end_prog (Apply_Method'     vvv FIXME: get args in applicable_in *)

fun begin_end_prog (Tactic.Apply_Method' (mI, _, _, ctxt)) _ (pt, pos as (p, _)) =

    let

      val {ppc, ...} = Specify.get_met mI;

      val (itms, oris, probl) = case get_obj I pt p of

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

      | _ => error "begin_end_prog Apply_Method': uncovered case get_obj"

      val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc

      val thy' = get_obj g_domID pt p;

      val thy = Celem.assoc_thy thy';

      val srls = Lucin.get_simplifier (pt, pos)

(*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)

val itms =

  if mI = ["Biegelinien", "ausBelastung"]

  then itms @

    [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),

        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

      (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),

    (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),

        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

      (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]

  else itms

(*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)

     val (is, env, ctxt, scr) = case Lucin.init_pstate srls ctxt itms mI of

         (is as Istate.Pstate pst, ctxt, scr) => (is, Istate.get_env pst, ctxt, scr)

       | _ => error "begin_end_prog Apply_Method': uncovered case init_pstate"

     val ini = Lucin.init_form thy scr env;

   in 

     case ini of

       SOME t =>

       let

         val pos = ((lev_on o lev_dn) p, Frm)

	       val tac_ = Tactic.Apply_Method' (mI, SOME t, is, ctxt);

	       val (pos, c, _, pt) = Generate.generate1 thy tac_ (is, ctxt) pos pt (* implicit Take *)

       in

        ([(Tactic.Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos))

       end

     | NONE =>

       let

         val pt = update_env pt (fst pos) (SOME (is, ctxt))

	       val (tacis, c, ptp) = do_solve_step (pt, pos)

       in (tacis @ [(Tactic.Apply_Method mI,

            Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt), (pos, (is, ctxt)))], c, ptp)

       end

    end

  | begin_end_prog (Tactic.Check_Postcond' (pI, _)) _ (pt, (p, p_))  =

    let

      val pp = par_pblobj pt p

      val asm = (case get_obj g_tac pt p of

		    Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p (*collects and instantiates asms*)

		  | _ => get_assumptions_ pt (p, p_))

      val metID = get_obj g_metID pt pp;

      val {srls = srls, scr = sc, ...} = Specify.get_met metID;

      val (loc, pst, ctxt) = case get_loc pt (p, p_) of

        loc as (Istate.Pstate pst, ctxt) => (loc, pst, ctxt)

      | _ => error "begin_end_prog Check_Postcond': uncovered case get_loc"

      val thy' = get_obj g_domID pt pp;

      val thy = Celem.assoc_thy thy';

      val (_, _, (scval, _(*scsaf*))) = determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc;

      (*                 Telem.safe should go on to Check_Postcond'   vvvvv *)

    in

      if pp = []

      then 

	      let

          val is = Istate.Pstate (pst |> Istate.upd_act scval |> Istate.upd_appy Istate.Skip_)

	        val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))

	          (*extend Tactic.Check_Postcond' (pI, (scval, asm), scsaf) ^^^^^ *)

	        val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt) (pp, Res) pt;

	      in ([(Tactic.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, (p, p_))) end

      else

        let (*resume script of parent PblObj, transfer value of subpbl-script*)

          val ppp = par_pblobj pt (lev_up p);

	        val thy' = get_obj g_domID pt ppp;

          val thy = Celem.assoc_thy thy';

          val (pst', ctxt') = case get_loc pt (pp, Frm) of

            (Istate.Pstate pst', ctxt') => (pst', ctxt')

          | _ => error "begin_end_prog Check_Postcond' script of parpbl: uncovered case get_loc"

	        val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt'

          val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))

	        val is = Istate.Pstate (pst' |> Istate.upd_act scval |> Istate.upd_appy Istate.Skip_)

          val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt'') (pp, Res) pt;

        in ([(Tactic.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p, p_))) end

    end

  | begin_end_prog (Tactic.End_Proof'') _ ptp = ([], [], ptp)

  | begin_end_prog tac_ is (pt, pos) =

    let

      val pos = case pos of

 		   (p, Met) => ((lev_on o lev_dn) p, Frm) (* begin script        *)

 		  | (p, Res) => (lev_on p, Res)            (* somewhere in script *)

 		  | _ => pos

 	    val (pos', c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac_ is pos pt;

    in

      ([(Lucin.tac_2tac tac_, tac_, (pos, is))], c, (pt, pos'))

    end

(* find the next tac from the script, begin_end_prog will update the ctree *)

and do_solve_step (ptp as (pt, pos as (p, p_))) = (* WN1907: ?only for Begin_/End_Detail' DEL!!!*)

    if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)

    then ([], [], (pt, (p, p_)))

    else 

      let 

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

	      val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;

	      val (tac_, is, (t, _)) = determine_next_tactic (thy', srls) (pt, pos) sc is;

	      (* TODO here  ^^^  return finished/helpless/ok ?*)

	    in case tac_ of

		    Tactic.End_Detail' _ => ([(Tactic.End_Detail,

          Tactic.End_Detail' (t, [(*FIXME.04*)]), (pos, is))], [], (pt, pos))

	    | _ => begin_end_prog tac_ is ptp

      end;

(* compare inform with ctree.form at current pos by nrls;

   if found, embed the derivation generated during comparison

   if not, let the mat-engine compute the next ctree.form *)

(* code's structure is copied from complete_solve

   CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --

            all_modspec etc. has to be inserted at Subproblem'*)

fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): Chead.calcstate') ifo =

  let

    val fo =

      case p_ of

        Ctree.Frm => Ctree.get_obj Ctree.g_form pt p

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

			| _ => Rule.e_term (*on PblObj is fo <> ifo*);

	  val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))

	  val {rew_ord, erls, rules, ...} = Rule.rep_rls nrls

	  val (found, der) = Inform.concat_deriv rew_ord erls rules fo ifo; (*<---------------*)

  in

    if found

    then

       let

         val tacis' = map (Inform.mk_tacis rew_ord erls) der;

		     val (c', ptp) = Generate.embed_deriv tacis' ptp;

	     in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end

     else 

	     if pos = ([], Ctree.Res) (*TODO: we should stop earlier with trying subproblems *)

	     then ("no derivation found", (tacis, c, ptp): Chead.calcstate') 

	     else

         let

           val cs' as (tacis, c', ptp) = do_solve_step ptp; (*<---------------------*)

		       val (tacis, c'', ptp) = case tacis of

			       ((Tactic.Subproblem _, _, _)::_) => 

			         let

                 val ptp as (pt, (p,_)) = Chead.all_modspec ptp (*<--------------------*)

				         val mI = Ctree.get_obj Ctree.g_metID pt p

			         in

			           begin_end_prog (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) (Istate.e_istate, ContextC.e_ctxt) ptp

               end

			     | _ => cs';

		     in compare_step (tacis, c @ c' @ c'', ptp) ifo end

  end

(*.handle a user-input formula, which may be a CAS-command, too.

CAS-command:

   create a calchead, and do 1 step

   TOOODO.WN0602 works only for the root-problem !!!

formula, which is no CAS-command:

   compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;

   collect all the tacs applied by the way;

   if "no derivation found" then check_error_patterns.

   ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*)

(*                       vvvv           vvvvvv vvvv    NEW args for compare_step *)

fun locate_input_formula (Rule.Prog _)  ((pt, pos) : Ctree.state) (_ : Istate.T) (_ : Proof.context) tm =

     let                                                          

   		val pos_pred = Ctree.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)

   		val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred)

     in

       (*TODO: use prog, istate, ctxt in compare_step ...*)

   		case compare_step ([], [], (pt, pos_pred)) tm of

   		  ("no derivation found", calcstate') => Not_Derivable calcstate'

       | ("ok", (_, _, cstate as (pt', pos'))) => 

           Step (cstate, get_istate pt' pos', get_ctxt pt' pos')

       | _ => raise ERROR "compare_step: uncovered case"

     end

  | locate_input_formula _ _ _ _ _ = error ""

(**)end(**)