(* 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' * 'a -> Ctree.state -> Rule.program -> Istate.T * 'b

     -> Tactic.T * (Istate.T * Proof.context) * (term * Telem.safe)

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

   datatype expr_val1 =

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

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

     | Term_Val1 of term;

   val assoc2str : expr_val1 -> string

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

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

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

   val check_Let_up : Istate.pstate -> term -> term * term

   val check_Seq_up: Istate.pstate -> term -> term

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

   val scan_dn1: (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1

   val scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1;

   val go_scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> expr_val1;

   val scan_to_tactic1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.T -> expr_val1

   datatype expr_val2 = Ackn_Tac2 of Tactic.T * Istate.pstate | Reject_Tac2 | Term_Val2 of term

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

   val scan_up2: term * (Ctree.state * Rule.theory') -> Istate.pstate -> term -> expr_val2

   val go_scan_up2: term * (Ctree.state * Rule.theory') -> Istate.pstate -> expr_val2

   val scan_to_tactic2: term * (Ctree.state * Rule.theory') -> Istate.T -> expr_val2

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

 end

 (**)

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

 struct

 (**)

 open Ctree

 open Pos

 open Celem

 open Istate

 (*** auxiliary functions ***)

 (*go to a location in a program and fetch the resective sub-term*)

 fun go [] t = t

   | go (D :: p) (Abs(_, _, body)) = go (p : Celem.path) body

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

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

   | go l _ = error ("go: no " ^ Celem.path2str 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, ...}: pstate) prog =

   case go (drop_last path) prog of

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

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

 fun check_Seq_up  ({path, ...}: pstate) prog =

   case go (drop_last path) prog of

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

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

 (*** 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 expr_val1 = (* "ExprVal" in the sense of denotational semantics        *)

   Reject_Tac1 of     (* tactic is found but NOT acknowledged, scan is continued *)

     Istate.pstate * Proof.context * Tactic.T (*TODO: revise Pstate {or,...},no args as Reject_Tac2*)

 | Ackn_Tac1 of       (* tactic is found and acknowledged, scan is stalled       *)

     Istate.pstate *  (* the current state, returned for resuming execution      *)

     Proof.context *  (* updated according to evaluation of Prog_Tac             *)

     Tactic.T         (* Prog_Tac is associated to Tactic.input                  *)

 | Term_Val1 of       (* Prog_Expr is found and evaluated, scan is continued     *)

 	  term             (* value of Prog_Expr, for updating environment            *)

 fun assoc2str (Ackn_Tac1 _) = "Ackn_Tac1"                                         

   | assoc2str (Term_Val1 _) = "Term_Val1"

   | assoc2str (Reject_Tac1 _) = "Reject_Tac1";

 (** scan to a Prog_Tac **)

 fun scan_dn1 cct ist (Const ("Tactical.Try"(*1*), _) $ e $ a) =

     (case scan_dn1 cct (ist |> path_down_form ([L, R], a)) e of goback => goback) 

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

     (case scan_dn1 cct (ist |> path_down [R]) e of goback => goback)

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

     scan_dn1 cct (ist |> path_down_form ([L, R], a)) e

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

     scan_dn1 cct (ist |> path_down [R]) e

   | scan_dn1 (cct as (cstate, _, _)) ist (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a) =

     (case scan_dn1 cct (ist |> path_down_form ([L, L, R], a)) e1 of

 	     Term_Val1 v => scan_dn1 cct (ist |> path_down [L, R] |> set_subst' (a, v)) e2

      | Reject_Tac1 (ist', ctxt', tac') => scan_dn1 (cstate, ctxt', tac') (ist

         |> path_down_form ([L, R], a) |> trans_env_act ist') e2

      | goback => goback)

   | scan_dn1 (cct as (cstate, _, _)) ist (Const ("Tactical.Chain"(*2*), _) $e1 $ e2) =

     (case scan_dn1 cct (ist |> path_down [L, R]) e1 of

 	     Term_Val1 v => scan_dn1 cct (ist |> path_down [R] |> set_act v) e2

      | Reject_Tac1 (ist', ctxt', tac') =>

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

      | goback => goback)

   | scan_dn1 cct ist (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))) =

     (case scan_dn1 cct (ist |> path_down [L, R]) e of

        Reject_Tac1 (ist', _, _) =>

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

      | Term_Val1 v =>

          scan_dn1 cct (ist |> path_down [R, D] |> upd_env'' (TermC.mk_Free (id, T), v)) b

      | goback => goback)

   | scan_dn1 cct (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =

     if Rewrite.eval_true_ "Isac_Knowledge" eval

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

     then scan_dn1 cct (ist |> path_down_form ([L, R], a)) e

     else Term_Val1 act_arg

   | scan_dn1 cct (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*2*),_) $ c $ e) =

     if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update_opt' (get_subst ist)) c) 

     then scan_dn1 cct (ist |> path_down [R]) e

     else Term_Val1 act_arg

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

     (case scan_dn1 cct (ist |> path_down_form ([L, L, R], a) |> set_or AssOnly) e1 of

 	     Term_Val1 v =>

 	       (case scan_dn1 cct (ist |> path_down [L, R] |> set_subst' (a, v) |> set_or AssOnly) e2 of

 	          Term_Val1 v => 

 	            (case scan_dn1 cct (ist |> path_down [L, L, R] |> upd_env'' (a, v) |> set_or AssGen) e1 of

 	               Term_Val1 v => 

 	                 scan_dn1 cct (ist |> path_down [L, R] |> upd_env'' (a, v) |> set_or AssGen) e2

 	             | goback => goback)

 	        | goback => goback)

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

      | goback => goback)

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

     (case scan_dn1 cct (ist |> path_down [L, R]) e1 of

 	     Term_Val1 v => scan_dn1 cct (ist |> path_down [R] |> set_act v) e2

      | goback => goback)

   | scan_dn1 cct (ist as {eval, ...}) (Const ("Tactical.If", _) $ c $ e1 $ e2) =

     if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update_opt' (get_subst ist)) c)

     then scan_dn1 cct (ist |> path_down [L, R]) e1

     else scan_dn1 cct (ist |> path_down [R]) e2

   | scan_dn1 ((pt, p), ctxt, tac) (ist as {eval, act_arg, or, ...}) t =

     if Tactical.contained_in t then raise TERM ("scan_dn1 expects Prog_Tac or Prog_Expr", [t])

     else

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

   	     (a', Program.Expr _) => 

 (*--------------------------- eval_Prog_Expr -----*)

   	       Term_Val1 (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac_Knowledge") eval

   		       (subst_atomic (Env.update_opt'' (get_act_env ist, a')) t))

        | (a', Program.Tac stac) =>

 (*/------------ interprete_Prog_Tac -----*)

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

               (* HERE ----------------vvvv ContextC.insert_assumptions asm ctxt DONE -- 2nd in gen//*)

   	           Lucin.Ass      (m, v', ctxt) => Ackn_Tac1 (ist |> set_subst_true  (a', v'), ctxt, m)

              | Lucin.Ass_Weak (m, v', ctxt) => Ackn_Tac1 (ist |> set_subst_false (a', v'), ctxt, m)

              | Lucin.NotAss =>

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

                   AssOnly => Term_Val1 act_arg

                 | _(*Aundef*) =>

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

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

                     | Chead.Notappl _ => Term_Val1 act_arg)

 (*------------- interprete_tactic ---//*)

       ;

 fun scan_up1 pcct ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up1 pcct ist

   | scan_up1 pcct ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up1 pcct ist

   | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*1*), _) $ e $ a) =

     (case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or Aundef) e of 

       Term_Val1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)

     | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t

     | goback => goback)

   | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*2*), _) $ e) =

     (case scan_dn1 cct (ist |> path_down [R] |> set_or Aundef) e of

        Term_Val1 v' => go_scan_up1 pcct (ist |> set_act v')

      | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t

      | goback => goback)

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

   | scan_up1 pcct ist (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist

   | scan_up1 pcct ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = go_scan_up1 pcct ist (*comes from e2*)

     (*comes from e1, goes to e2*)

   | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (Const ("Tactical.Chain"(*3*), _) $ _ ) =

      let 

        val e2 = check_Seq_up ist prog

      in

        case scan_dn1 cct (ist |> path_up_down [R] |> set_or Aundef) e2 of

          Term_Val1 v => go_scan_up1 pcct (ist |> path_up |> set_act v)

        | Reject_Tac1 (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'

        | goback => goback 

      end

   | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (Const ("HOL.Let"(*1*), _) $ _) =

     let 

       val (i, body) = check_Let_up ist prog

     in case scan_dn1 cct (ist |> path_up_down [R, D] |> upd_env i |> set_or Aundef) body of

 	       Ackn_Tac1 iss => Ackn_Tac1 iss

 	     | Reject_Tac1 (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'

 	     | Term_Val1 v => go_scan_up1 pcct (ist |> path_up |> set_act v) 

 	  end

   | scan_up1 pcct ist (Abs(*2*) _) = go_scan_up1 pcct ist

   | scan_up1 pcct ist (Const ("HOL.Let"(*3*), _) $ _ $ (Abs _)) = go_scan_up1 pcct ist

   | scan_up1 (pcct as (prog, cct as (cstate, _, _))) (ist as {eval, ...})

       (t as Const ("Tactical.While"(*1*),_) $ c $ e $ a) =

     if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update' a (get_act_env ist)) c)

     then

       case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or Aundef) e of 

         Term_Val1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)

       | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t

       | goback => goback

     else go_scan_up1 pcct (ist |> set_form a)

   | scan_up1 (pcct as (prog, cct as (cstate, _, _))) (ist as {eval, ...})

       (t as Const ("Tactical.While"(*2*), _) $ c $ e) =

     if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update_opt' (get_subst ist)) c)

     then

       case scan_dn1 cct (ist |> path_down [R] |> set_or Aundef) e of 

         Term_Val1 v => go_scan_up1 pcct (ist |> set_act v)

        | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t

        | goback => goback

     else go_scan_up1 pcct ist

   | scan_up1 pcct ist (Const ("If", _) $ _ $ _ $ _) = go_scan_up1 pcct ist

   | scan_up1 pcct ist (Const ("Tactical.Or"(*1*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist

   | scan_up1 pcct ist (Const ("Tactical.Or"(*2*), _) $ _ $ _) = go_scan_up1 pcct ist

   | scan_up1 pcct ist (Const ("Tactical.Or"(*3*), _) $ _ ) = go_scan_up1 pcct (ist |> path_up)

   | scan_up1 pcct ist (Const ("Tactical.If",_) $ _ $ _ $ _) = go_scan_up1 pcct ist

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

 and go_scan_up1 (pcct as (prog, _)) (ist as {path, act_arg, ...}) =

     if 1 < length path

     then scan_up1 pcct (ist |> path_up) (go (path_up' path) prog)

     else Term_Val1 act_arg

 fun scan_to_tactic1 (prog, (cctt as ((_, p), _, _))) (Istate.Pstate (ist as {path, ...})) =

     if path = [] orelse Pos.at_first_tactic(*RM prog path RM WITH determine_next_tactic IN solve*)p

     then scan_dn1 cctt (ist |> set_path [R] |> set_or Aundef) (Program.body_of prog)

     else go_scan_up1 (prog, cctt) ist

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

 (*locate an input tactic within a program*)

 fun locate_input_tactic (Rule.Prog prog) cstate istate ctxt tac =

     (case scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate of

          Ackn_Tac1 ((ist as {assoc, ...}), ctxt, tac') =>

           if assoc

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

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

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

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

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

 (*** determine a next tactic by executing the program ***)

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

     | Helpless | End_Program

 (** scan to a Prog_Tac **)

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

   Reject_Tac2        (* tactic is found but NOT acknowledged, scan is continued *)

 | Ackn_Tac2 of       (* tactic is found and acknowledged, scan is stalled       *)

     Tactic.T *       (* Prog_Tac is applicable_in cstate                        *)

     Istate.pstate    (* the current state, returned for resuming execution      *)

 | Term_Val2 of       (* Prog_Expr is found and evaluated, scan is continued     *)

     term;            (* value of Prog_Expr, for updating environment            *)

 (*

   scan_dn2, go_scan_up2, scan_up2 scan for determine_next_tactic.

   (1) scan_dn2 is recursive descent;

   (2) go_scan_up2 goes to the parent node and calls (3);

   (3) scan_up2 resumes according to the interpreter-state.

   Call of (2) means that there was an applicable Prog_Tac below

 *)

 fun scan_dn2 cc (ist as {act_arg, ...}) (Const ("Tactical.Try"(*1*), _) $ e $ a) =

     (case scan_dn2 cc (ist|> path_down_form ([L, R], a)) e of

       Reject_Tac2 => Term_Val2 act_arg

     | goback => goback)

   | scan_dn2 cc (ist as {act_arg, ...}) (Const ("Tactical.Try"(*2*), _) $ e) =

     (case scan_dn2 cc (ist |> path_down [R]) e of

       Reject_Tac2 => Term_Val2 act_arg

     | goback => goback)

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

     scan_dn2 cc (ist |> path_down_form ([L, R], a)) e

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

     scan_dn2 cc (ist |> path_down [R]) e

   | scan_dn2 cc ist (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a) =

     (case scan_dn2 cc (ist |> path_down_form ([L, L, R], a)) e1 of

 	    Term_Val2 v => scan_dn2 cc (ist |> path_down_form ([L, R], a) |> set_act v) e2 (*UPD*)

     | goback => goback)

   | scan_dn2 cc ist (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2) =

     (case scan_dn2 cc (ist |> path_down [L, R]) e1 of

 	    Term_Val2 v => scan_dn2 cc (ist |> path_down [R] |> set_act v) e2

     | goback => goback)

   | scan_dn2 cc ist (Const ("HOL.Let"(*1*), _) $ e $ (Abs (i, T, b))) =

      (case scan_dn2 cc (ist |> path_down [L, R]) e of

        Term_Val2 res => scan_dn2 cc (ist |> path_down [R, D] |> upd_env'' (Free (i, T), res)) b

      | goback => goback)

   | scan_dn2 (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =

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

     then scan_dn2 cc (ist |> path_down_form ([L, R], a)) e

     else Term_Val2 act_arg

   | scan_dn2 (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*2*), _) $ c $ e) =

     if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)

     then scan_dn2 cc (ist |> path_down [R]) e

     else Term_Val2 act_arg

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

     (case scan_dn2 cc (ist |> path_down_form ([L, L, R], a)) e1 of

 	    Ackn_Tac2 lme => Ackn_Tac2 lme

     | _ => scan_dn2 cc (ist |> path_down_form ([L, R], a)) e2)

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

     (case scan_dn2 cc (ist |> path_down [L, R]) e1 of

 	    Ackn_Tac2 lme => Ackn_Tac2 lme

     | _ => scan_dn2 cc (ist |> path_down [R]) e2)

   |  scan_dn2 (cc as (_, ctxt)) (ist as {eval, ...}) (Const ("Tactical.If"(*1*), _) $ c $ e1 $ e2) =

     if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)

     then scan_dn2 cc (ist |> path_down [L, R]) e1

     else scan_dn2 cc (ist |> path_down [R]) e2

   | scan_dn2 ((pt, p), ctxt) (ist as {eval, ...}) t =

     if Tactical.contained_in t then raise TERM ("scan_dn2 expects Prog_Tac or Prog_Expr", [t])

     else

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

   	    (_, Program.Expr s) => Term_Val2 s

       | (a', Program.Tac 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 _ => Ackn_Tac2 (m', ist |> set_subst_reset (a', Lucin.tac_2res m'))

     	    | _ =>

             (case Applicable.applicable_in p pt m of

     		      Chead.Appl m' => Ackn_Tac2 (m', ist |> set_subst_reset (a', Lucin.tac_2res m'))

     		    | _ => Reject_Tac2)

   	    end

     (*makes Reject_Tac2 to Term_Val2*)

 fun scan_up2 pcc ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up2 pcc (ist |> set_appy Skip_)

   | scan_up2 pcc ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up2 pcc (ist |> set_appy Skip_)

   | scan_up2 (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*1*), _) $ e $ _) =

     (case scan_dn2 cc (ist |> path_down [L, R]) e of (* no appy_: there was already a stac below *)

       Ackn_Tac2 lr => Ackn_Tac2 lr

     | Reject_Tac2 =>  go_scan_up2 pcc (ist |> set_appy Skip_)

     | Term_Val2 v =>  go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_))

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

   | scan_up2  (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) =

     (case scan_dn2 cc (ist |> path_down [R]) e of

       Ackn_Tac2 lr => Ackn_Tac2 lr

     | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)

     | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_))

   | scan_up2 pcc ist (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _) = go_scan_up2 pcc ist

   | scan_up2 pcc ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = go_scan_up2 pcc ist

   | scan_up2 (pcc as (sc, cc)) (ist as {finish, ...}) (Const ("Tactical.Chain"(*3*), _) $ _) =

     if finish = Napp_

     then go_scan_up2 pcc (ist |> path_up)

     else (*Skip_*)

       let 

         val e2 = check_Seq_up ist sc

       in

         case scan_dn2 cc (ist |> path_up_down [R]) e2 of

           Ackn_Tac2 lr => Ackn_Tac2 lr

         | Reject_Tac2 => go_scan_up2 pcc (ist |> path_up)

         | Term_Val2 v => go_scan_up2 pcc (ist |> path_up |> set_act v |> set_appy Skip_)

       end

   | scan_up2 (pcc as (sc, cc)) (ist as {finish, ...}) (Const ("HOL.Let"(*1*), _) $ _) =

     if finish = Napp_

     then go_scan_up2 pcc (ist |> path_up)

     else (*Skip_*)

 	    let

         val (i, body) = check_Let_up ist sc

       in

         case scan_dn2 cc (ist |> path_up_down [R, D] |> upd_env i) body of

 	        Ackn_Tac2 lre => Ackn_Tac2 lre

 	      | Reject_Tac2 => go_scan_up2 pcc (ist |> path_up)

 	      | Term_Val2 v => go_scan_up2 pcc (ist |> path_up |> set_act v |> set_appy Skip_)

 	    end

   | scan_up2 pcc ist (Abs _(*2*)) =  go_scan_up2 pcc ist

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

     go_scan_up2 pcc ist

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

   | scan_up2 (pcc as (_, cc as (_, ctxt)))  (ist as {eval, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ _) = 

     if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c) 

     then

       case scan_dn2 cc (ist |> path_down [L, R]) e of

   	     Ackn_Tac2 lr => Ackn_Tac2 lr

   	  | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)

   	  | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_)

     else

       go_scan_up2 pcc (ist |> set_appy Skip_)

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

   | scan_up2  (pcc as (_, cc as (_, ctxt))) (ist as {eval, ...}) (Const ("Tactical.While"(*2*), _) $ c $ e) = 

     if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c) 

     then

       case scan_dn2 cc (ist |> path_down [R]) e of

   	    Ackn_Tac2 lr => Ackn_Tac2 lr

   	  | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)

   	  | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_)

     else

       go_scan_up2 pcc (ist |> set_appy Skip_)

   | scan_up2 pcc ist (Const ("Tactical.Or"(*1*), _) $ _ $ _ $ _) = go_scan_up2 pcc ist

   | scan_up2 pcc ist (Const ("Tactical.Or"(*2*), _) $ _ $ _) = go_scan_up2 pcc ist

   | scan_up2 pcc ist (Const ("Tactical.Or"(*3*), _) $ _ ) = go_scan_up2 pcc ist

   | scan_up2 pcc ist (Const ("Tactical.If"(*1*), _) $ _ $ _ $ _) = go_scan_up2 pcc ist

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

 and go_scan_up2 (pcc as (sc, _)) (ist as {path, act_arg, finish, ...}) = 

     if 1 < length path

     then 

       scan_up2 pcc (ist |> path_up) (go_up path sc)

     else (*interpreted to end*)

       if finish = Skip_ then Term_Val2 act_arg else Reject_Tac2

 fun scan_to_tactic2 (prog, cc) (Istate.Pstate (ist as {path, ...})) =

   if path = []

   then scan_dn2 cc (trans_scan_down2 ist) (Program.body_of prog)

   else go_scan_up2 (prog, cc) (trans_scan_up2 ist |> set_appy Skip_)

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

 (*decide for the next applicable Prog_Tac*)

 fun determine_next_tactic (thy, _) (ptp as (pt, (p, _))) (Rule.Prog prog) (Istate.Pstate ist, _(*ctxt*)) =

    (case scan_to_tactic2 (prog, (ptp, thy)) (Istate.Pstate ist) of

       Term_Val2 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, ContextC.e_ctxt), (v, Telem.Safe)) 

             end

 	      | _ =>

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

     | Reject_Tac2 =>

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

     | Ackn_Tac2 (m', (ist as {act_arg, ...})) =>

         (m', (Pstate ist, ContextC.e_ctxt), (act_arg, Telem.Safe)))                  (* found next tac *)

   | determine_next_tactic _ _ _ (is, _) =

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

 (*** 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 {env, ...}, ctxt, scr) => (is, env, 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, _)) = determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc;

     in

       if pp = []

       then 

 	      let

           val is = Istate.Pstate (pst |> Istate.set_act scval |> Istate.set_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.set_act scval |> Istate.set_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

       ([(Tactic.input_from_T 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

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

 			| Pos.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 = ([], Pos.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

  * formula, which is no CAS-command:

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

    collect all the Prog_Tac applied by the way; ...???TODO?

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