(* Title:  Interpret/lucas-interpreter.sml

    Author: Walther Neuper 2019

    (c) due to copyright terms

 *)

 signature LUCAS_INTERPRETER =

 sig

   datatype next_step_result =

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

     | Helpless | End_Program of Istate.T (*TODO ?needed when..*)* Tactic.T

   val find_next_step: Program.T -> Calc.T -> Istate.T -> Proof.context

     -> next_step_result

   datatype input_tactic_result =

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

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

     | Not_Locatable (*TODO rm..*) of string

   val locate_input_tactic: Program.T -> Calc.T -> Istate.T -> Proof.context

       -> Tactic.T -> input_tactic_result

   datatype input_term_result = Found_Step of Calc.T | Not_Derivable (**)

   val locate_input_term: Calc.T -> term -> input_term_result (**)

   (* must reside here:

      find_next_step calls do_next and is called by by_tactic;

      by_tactic and do_next are mutually recursive via by_tactic..Apply_Method'

    *)

   val by_tactic: Tactic.T -> Istate.T * Proof.context -> Calc.T -> string * Chead.calcstate'

   val do_next: Calc.T -> string * Chead.calcstate'

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

   datatype expr_val1 =

       Accept_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

 (* ---- for Doc/Lucas-Interpreter ------------------------------------------------------------- *)

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

   datatype expr_val = Accept_Tac of Tactic.T * Istate.pstate * Proof.context

     | Reject_Tac | Term_Val of term

   val scan_dn: Calc.T * Proof.context -> Istate.pstate -> term -> expr_val

   val scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> term -> expr_val

   val go_scan_up: term * (Calc.T * Proof.context) -> Istate.pstate -> expr_val

   val scan_to_tactic: term * (Calc.T * Proof.context) -> Istate.T -> expr_val

   val check_tac: Calc.T * Proof.context -> Istate.pstate -> term * term option -> expr_val

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

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

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

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

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

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

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

   val check_tac1: Calc.T * Proof.context * Tactic.T -> Istate.pstate -> term * term option -> expr_val1

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

 end

 (**)

 structure LI(**): LUCAS_INTERPRETER(**) =

 struct

 (**)

 open Ctree

 open Pos

 open TermC

 open Istate

 (*** auxiliary functions ***)

 fun at_location [] t = t

   | at_location (D :: p) (Abs(_, _, body)) = at_location (p : TermC.path) body

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

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

   | at_location l _ = error ("at_location: no " ^ TermC.string_of_path l);

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

   case at_location (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 at_location (drop_last path) prog of

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

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

 (*** determine a next tactic within a program ***)

   datatype next_step_result = Next_Step of Istate.T * Proof.context * Tactic.T

     | Helpless | End_Program of Istate.T * Tactic.T (*contains prog_result, without asms*)

 (** scan to a Prog_Tac **)

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

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

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

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

     Istate.pstate * (* created by application of Tactic.T, for resuming execution *)

     Proof.context   (* created by application of Tactic.T                         *)

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

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

 (* check if a prog_tac found in a program is applicable_in *)

 fun check_tac ((pt, p), ctxt) ist (prog_tac, form_arg) =

   let

     val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac

   in

     case m of

       Tactic.Subproblem _ => (*might involve problem refinement etc*)

         let

           val m' = snd (Sub_Problem.tac_from_prog pt prog_tac)

         in

           Accept_Tac (m', ist |> set_subst_found (form_arg, Tactic.result m'), ctxt)

         end

     | _ =>

       (case Applicable.applicable_in p pt m of

         Applicable.Appl m' => 

           Accept_Tac (m', ist |> set_subst_found (form_arg, Tactic.result m'),

             Tactic.insert_assumptions m' ctxt)

       | _ => Reject_Tac)

   end

 (*

   scan_dn, go_scan_up, scan_up scan for find_next_step.

   (1) scan_dn is recursive descent depth first strictly from L to R;

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

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

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

 *)

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

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

       Reject_Tac => Term_Val act_arg

     | (*Accept_Tac*) goback => goback)

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

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

       Reject_Tac => Term_Val act_arg

     | (*Accept_Tac*) goback => goback)

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

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

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

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

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

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

 	    Term_Val v => scan_dn cc (ist |> path_down_form ([L, R], a) |> set_act v) e2

     | (*Accept_Tac*) goback => goback)

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

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

 	    Term_Val v => scan_dn cc (ist |> path_down [R] |> set_act v) e2

     | (*Accept_Tac*) goback => goback)

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

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

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

     | (*Accept_Tac*) goback => goback)

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

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

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

     else Term_Val act_arg

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

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

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

     else Term_Val act_arg

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

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

 	    Accept_Tac lme => Accept_Tac lme

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

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

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

 	    Accept_Tac lme => Accept_Tac lme

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

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

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

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

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

   | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) t =

     if Tactical.contained_in t

     then raise TERM ("scan_dn expects Prog_Tac or Prog_Expr", [t])

     else

       case LItool.check_leaf "next  " ctxt eval (get_subst ist) t of

   	    (Program.Expr s, _) => Term_Val s (*TODO?: include set_found here and drop those after call*)

       | (Program.Tac prog_tac, form_arg) =>

           check_tac cc ist (prog_tac, form_arg)

 fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept, ...}) = 

     if path = [R] (*root of the program body*)

     then

       if found_accept

       then Term_Val act_arg

       else raise ERROR "LItool.find_next_step without result"

     else scan_up pcc (ist |> path_up) (go_up path sc)

 (* scan is strictly to R, because at L there was an \<open>expr_val\<close> *)

 and scan_up pcc ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up pcc ist

   | scan_up pcc ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up pcc ist

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

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

       Accept_Tac ict => Accept_Tac ict

     | Reject_Tac =>  go_scan_up pcc ist

     | Term_Val v =>  go_scan_up pcc (ist |> set_act v |> set_found))

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

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

       Accept_Tac ict => Accept_Tac ict

     | Reject_Tac => go_scan_up pcc ist

     | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found))

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

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

   | scan_up (pcc as (sc, cc)) ist (Const ("Tactical.Chain"(*3*), _) $ _) =

       let 

         val e2 = check_Seq_up ist sc

       in

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

           Accept_Tac ict => Accept_Tac ict

         | Reject_Tac => go_scan_up pcc (ist |> path_up)

         | Term_Val v => go_scan_up pcc (ist |> path_up |> set_act v |> set_found)

       end

   | scan_up (pcc as (sc, cc)) ist (Const ("HOL.Let"(*1*), _) $ _) =

 	    let

         val (i, body) = check_Let_up ist sc

       in

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

 	        Accept_Tac ict => Accept_Tac ict

 	      | Reject_Tac => go_scan_up pcc (ist |> path_up)

 	      | Term_Val v => go_scan_up pcc (ist |> path_up |> set_act v |> set_found)

 	    end

   | scan_up pcc ist (Abs _(*2*)) = go_scan_up pcc ist

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

   | scan_up (pcc as (_, cc as (_, ctxt)))  (ist as {eval, ...})

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

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

     then

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

   	     Accept_Tac ict => Accept_Tac ict

   	  | Reject_Tac => go_scan_up pcc ist

   	  | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found)

     else

       go_scan_up pcc (ist (*|> set_found*))

   | scan_up  (pcc as (_, cc as (_, ctxt))) (ist as {eval, ...})

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

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

     then

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

   	    Accept_Tac ict => Accept_Tac ict

   	  | Reject_Tac => go_scan_up pcc ist

   	  | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found)

     else

       go_scan_up pcc ist

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

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

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

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

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

 (* scan program until an applicable tactic is found *)

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

   if path = []

   then scan_dn cc (trans_scan_dn ist) (Program.body_of prog)

   else go_scan_up (prog, cc) (trans_scan_up ist)

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

 (* find the next applicable Prog_Tac in a prog *)

 fun find_next_step (Rule.Prog prog) (ptp as(pt, (p, _))) (Pstate ist) ctxt =

    (case scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) of

       Accept_Tac (tac, ist, ctxt) =>

         Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac)

     | Term_Val prog_result =>

         (case par_pbl_det pt p of

           (true, p', _) => 

             let

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

             in

               End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, (prog_result, [(*???*)])))

             end

         | _ => End_Program (Pstate ist, Tactic.End_Detail' (Rule.e_term,[])))

     | Reject_Tac => Helpless)

   | find_next_step _ _ ist _ =

     raise ERROR ("find_next_step: not impl for " ^ istate2str ist);

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

 (*all functions ending with "1" are supposed to be replaced by those without "1"*)

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

 | Accept_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 (Accept_Tac1 _) = "Accept_Tac1"                                         

   | assoc2str (Term_Val1 _) = "Term_Val1"

   | assoc2str (Reject_Tac1 _) = "Reject_Tac1";

 (** check a Prog_Tac: is it associated to Tactic ? **)

 fun check_tac1 ((pt, p), ctxt, tac) (ist as {act_arg, or, ...}) (prog_tac, form_arg) =

   case LItool.associate pt ctxt (tac, prog_tac) of

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

       LItool.Ass      (m, v', ctxt)

         => Accept_Tac1 (ist |> set_subst_true  (form_arg, v') |> set_found, ctxt, m)

     | LItool.Ass_Weak (m, v', ctxt) (*the ONLY ones in locate_tac ^v^v^v^v^ *)

         => Accept_Tac1 (ist |> set_subst_false (form_arg, v') |> set_found, ctxt, m)

     | LItool.NotAss =>

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

          AssOnly => Term_Val1 act_arg

        | _(*ORundef*) =>

           case Applicable.applicable_in p pt (LItool.tac_from_prog pt (Celem.assoc_thy "Isac_Knowledge") prog_tac) of

              Applicable.Appl m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)

            | Applicable.Notappl _ => Term_Val1 act_arg)

 (** scan to a Prog_Tac **)

 (* scan is strictly first L, then R; tacticals have 2 args at maximum *)

 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 as (_, ctxt, _)) (ist as {eval, act_arg, ...})

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

     if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) 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 as (_, ctxt, _)) (ist as {eval, act_arg, ...})

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

     if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) 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 = ORundef, ...}) (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 as (_, ctxt, _)) (ist as {eval, ...}) (Const ("Tactical.If", _) $ c $ e1 $ e2) =

     if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) 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 (cct as (_, ctxt, _)) (ist as {eval, ...}) t =

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

     else

       case LItool.check_leaf "locate" ctxt eval (get_subst ist) t of

   	    (Program.Expr _, form_arg) => 

   	      Term_Val1 (Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) eval

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

       | (Program.Tac prog_tac, form_arg) =>

           check_tac1 cct ist (prog_tac, form_arg)

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

     if 1 < length path

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

     else Term_Val1 act_arg

 (* scan is strictly to R, because at L there was a expr_val *)

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

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

      let 

        val e2 = check_Seq_up ist prog (*comes from e1, goes to e2*)

      in

        case scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) 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 ORundef) body of

 	       Accept_Tac1 iss => Accept_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, ctxt, _))) (ist as {eval, ...})

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

     if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) 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 ORundef) 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, ctxt, _))) (ist as {eval, ...})

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

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

     then

       case scan_dn1 cct (ist |> path_down [R] |> set_or ORundef) 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)

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

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

     then scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (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

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

           if assoc

           then Safe_Step (Pstate ist, ctxt, tac')

  	        else Unsafe_Step (Pstate ist, ctxt, tac')

       | Reject_Tac1 _ => Not_Locatable (Tactic.string_of 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"

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

 datatype input_term_result = Found_Step of Calc.T | Not_Derivable

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

 (*OLD*)let

  (*OLD*)   val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of

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

  (*OLD*)   | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj"

  (*OLD*)   val {ppc, ...} = Specify.get_met mI;

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

  (*OLD*)   val itms = Specify.hack_until_review_Specify_1 mI itms

  (*OLD*)   val thy = Celem.assoc_thy (get_obj g_domID pt p);

  (*OLD*)   val srls = LItool.get_simplifier (pt, pos)

  (*OLD*)   val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of

  (*OLD*)     (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)

  (*OLD*)   | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate"

  (*OLD*)  val ini = LItool.init_form thy prog env;

  (*OLD*)in 

  (*OLD*)  case ini of

  (*OLD*)    SOME t =>

  (*OLD*)    let

  (*OLD*)      val pos = start_new_level pos

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

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

  (*OLD*)    in

  (*OLD*)     ("ok", ([(Tactic.Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)))

  (*OLD*)    end

  (*OLD*)  | NONE =>

 (*OLD*)    let

 (*NEW* )      val (tac', ist', ctxt') = 

 (*NEW*)        case find_next_step prog (pt, (lev_dn p, Res)) is ctxt of

 (*NEW*)          Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)

 (*NEW*)        | _ => raise ERROR ("LI.by_tactic..Apply_Method " ^ strs2str' mI)

 (*NEW*)    in

 (*NEW*)      case tac' of

 (*NEW*)        Tactic.Take' t =>

 (*NEW*)          let

 (*NEW*)            val pos = start_new_level pos

 (*NEW*)            val tac_ = Tactic.Apply_Method' (mI, SOME t, ist', ctxt');

 (*NEW*)            val (pos, c, _, pt) = Generate.generate1 tac_ (ist', ctxt') (pt, pos) (* explicit Take *)

 (*NEW*)          in

 (*NEW*)           ("ok", ([(Tactic.Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)))

 (*NEW*)          end

 (*NEW*)      | tac as Tactic.Subproblem' (_, _, headline, _, _, _) =>

 (*NEW*)          let

 (*NEW*)            val pos = start_new_level pos

 (*NEW*)            val tac_ = Tactic.Apply_Method' (mI, SOME headline, ist', ctxt');

 (*NEW*)            val (pos, c, _, pt) = Generate.generate1 tac (ist', ctxt') (pt, pos) (* Subproblem *)

 (*NEW*)            (**)

 (*NEW*)          in

 (*NEW*)           ("ok", ([(Tactic.Apply_Method mI, tac_, (pos, (ist', ctxt')))], c, (pt, pos)))

 (*NEW*)          end

 (*NEW*)      | tac =>

 (*NEW*)          raise ERROR ("LI.by_tactic..Apply_Method' does NOT expect " ^ Tactic.string_of tac)

 (*NEW*)    end

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

 (*OLD*)      val (_, (tacis, c, ptp)) = do_next (pt, pos)

 (*OLD*)    in ("ok", (tacis @ [(Tactic.Apply_Method mI,

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

 (*OLD*)    end

 (*OLD*)end

   | by_tactic (Tactic.Check_Postcond' (pI, _)) _ (pt, pos as (p, _))  =

     let

       val (ist, ctxt) = get_loc pt pos

       val parent_pos = par_pblobj pt p

       val {scr, ...} = Specify.get_met (get_obj g_metID pt parent_pos);

       val prog_res =

          case find_next_step scr (pt, pos) ist ctxt of

            Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res

          | End_Program (_, Tactic.Check_Postcond' (_, (prog_res, _))) => prog_res

          | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)

       val asm = (*?!? Rfun,Rrls rm case*)(case get_obj g_tac pt p of

           Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p

         | _ => get_assumptions_ pt pos)

 	    val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))

     in

       if parent_pos = []

       then 

 	      let

           val is = Pstate (ist |> the_pstate |> set_act prog_res |> set_found)

 	        val ((p, p_), ps, _, pt) = Generate.generate1 tac (is, ctxt) (pt, (parent_pos, Res))

 	      in

 	        ("ok", ([(Tactic.Check_Postcond pI, tac, ((parent_pos, Res), (is, ctxt)))], ps, (pt, (p, p_))))

 	      end

       else

         let (*resume program of parent PblObj, transfer value of Subproblem-program*)

           val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of

             (Pstate i, c) => (i, c)

           | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc"

 	        val ctxt' = ContextC.from_subpbl_to_caller ctxt prog_res ctxt_parent

 	        val is' = Pstate (ist_parent |> set_act prog_res |> set_found)

           val ((p, p_), ps, _, pt) = Generate.generate1 tac (is', ctxt') (pt, (parent_pos, Res))

         in

           ("ok", ([(Tactic.Check_Postcond pI, tac, ((parent_pos, Res), (is', ctxt')))], ps, (pt, (p, p_))))

         end

     end

   | by_tactic (Tactic.End_Proof'') _ ptp = ("end-of-calculation", ([], [], ptp))

   | by_tactic tac_ is (pt, pos) =

     let

       val pos = next_in_prog' pos

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

     in

       ("ok", ([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos')))

     end

 (*find_next_step from program, by_tactic will update Ctree*)

 and do_next (ptp as (pt, pos as (p, p_))) =

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

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

     else 

       let 

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

 	      val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;

       in

         case find_next_step sc (pt, pos) ist ctxt of

            Next_Step (ist, ctxt, tac) =>

              by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp

          | End_Program (ist, tac) =>

              (case tac of

                Tactic.End_Detail' res =>

                  ("ok", ([(Tactic.End_Detail, 

                    Tactic.End_Detail' res, (pos, (ist, ctxt)))], [], ptp))

              | _ => by_tactic tac (ist, ctxt) ptp

              )

          | Helpless => ("helpless", Chead.e_calcstate')

       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_))) 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) = Error_Pattern.concat_deriv rew_ord erls rules fo ifo; (*<---------------*)

   in

     if found

     then

        let

          val tacis' = map (Error_Pattern.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 msg_cs' as (_, (tacis, c', ptp)) = do_next 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

 			           by_tactic (Tactic.Apply_Method' (mI, NONE, e_istate, ContextC.e_ctxt))

 			             (e_istate, ContextC.e_ctxt) ptp

                end

 			     | _ => msg_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

 *)

 fun locate_input_term (pt, pos) tm =

      let                                                          

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

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

      in

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

    		  ("no derivation found", _) => Not_Derivable

        | ("ok", (_, _, cstate)) => 

            Found_Step cstate

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

      end

 (**)end(**)