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

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

    | Helpless | End_Program of Istate.T * Tactic.T

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

    -> next_tactic_result

(*TODO      input_formula_result = Found_Step of  Ctree.state | Not_Derivable *)

  datatype input_formula_result =

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

  | Not_Derivable of Chead.calcstate'

(*TODOlocate_input_formula: Ctree.state -> term -> input_formula_result *)

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

    -> input_formula_result

  (* must reside here:

     find_next_tactic calls do_solve_step and is called by by_tactic;

     by_tactic and do_solve_step are mutually recursive via by_tactic Apply_Method'

   *)

  val by_tactic: Tactic.T -> Istate.T * Proof.context -> Ctree.state -> Chead.calcstate'

  val do_solve_step: Ctree.state -> 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

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

  val interpret_tac1: Ctree.state * Proof.context * Tactic.T -> Istate.pstate -> term option * term -> expr_val1

  datatype expr_val2 = Accept_Tac2 of Tactic.T * Istate.pstate * Proof.context

    | Reject_Tac2 | Term_Val2 of term

  val scan_dn2: Ctree.state * Proof.context -> Istate.pstate -> term -> expr_val2

  val scan_up2: term * (Ctree.state * Proof.context) -> Istate.pstate -> term -> expr_val2

  val go_scan_up2: term * (Ctree.state * Proof.context) -> Istate.pstate -> expr_val2

  val scan_to_tactic2: term * (Ctree.state * Proof.context) -> 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*)

| 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";

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

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

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

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

      Lucin.Ass      (m, v', ctxt) => Accept_Tac1 (ist |> set_subst_true  (form_arg, v'), ctxt, m)

    | Lucin.Ass_Weak (m, v', ctxt) => Accept_Tac1 (ist |> set_subst_false (form_arg, v'), ctxt, m)

    | Lucin.NotAss =>

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

         AssOnly => Term_Val1 act_arg

       | _(*ORundef*) =>

          case Applicable.applicable_in p pt (Lucin.stac2tac 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 **)

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 Lucin.interpret_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) =>

          interpret_tac1 cct ist (form_arg, prog_tac)

fun 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

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), _, _))) (Istate.Pstate (ist as {path, ...})) =

    if path = [] orelse Pos.at_first_tactic(*RM prog path RM WITH find_next_tactic 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 (Istate.Pstate ist, ctxt, tac')

 	        else Unsafe_Step (Istate.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"

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

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

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

| Accept_Tac2 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_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 find_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

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

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

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

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

    | (*Accept_Tac2*) goback => goback)

  | scan_dn2 (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_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_ (Proof_Context.theory_of 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

	    Accept_Tac2 lme => Accept_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

	    Accept_Tac2 lme => Accept_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_ (Proof_Context.theory_of 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.interpret_leaf "next  " ctxt eval (get_subst ist) t of

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

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

  	    let

  	      val (m, m') = Lucin.stac2tac_ pt (Proof_Context.theory_of ctxt) stac

        in

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

    	      Tactic.Subproblem _ =>

    	        Accept_Tac2 (m', ist |> set_subst_reset (a', Tactic.result m'), ctxt)

    	    | _ =>

            (case Applicable.applicable_in p pt m of

    		      Applicable.Appl m' => Accept_Tac2 (m',

    		        ist |> set_subst_reset (a', Tactic.result m'), Tactic.insert_assumptions m' ctxt)

    		    | _ => Reject_Tac2)

  	    end

    (*makes Reject_Tac2 to Term_Val2*)

fun 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

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

      Accept_Tac2 lr => Accept_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

      Accept_Tac2 lr => Accept_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

          Accept_Tac2 lr => Accept_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

	        Accept_Tac2 lre => Accept_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_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c) 

    then

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

  	     Accept_Tac2 lr => Accept_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_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c) 

    then

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

  	    Accept_Tac2 lr => Accept_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)

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

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 find_next_tactic (Rule.Prog prog) (ptp as(pt, (p, _))) (Istate.Pstate ist) ctxt =

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

      Accept_Tac2 (tac, ist, ctxt) =>

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

    | Term_Val2 prog_result =>

        (case par_pbl_det pt p of

          (true, p', _) => 

            let

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

            in

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

            end

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

    | Reject_Tac2 => Helpless)

  | find_next_tactic _ _ is _ =

    raise ERROR ("find_next_tactic: not impl for " ^ Istate.istate2str is);

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

datatype input_formula_result =

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

  | Not_Derivable of Chead.calcstate'

(* FIXME.WN050821 compare fun solve ... fun by_tactic *)

fun by_tactic (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 "by_tactic 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)

      val itms = Specify.hack_until_review_Specify_1 mI itms

      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 "by_tactic 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

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

    let

      val pp = par_pblobj pt p

      val thy = Celem.assoc_thy (get_obj g_domID pt pp);

      val (pst, ctxt) = case get_loc pt (p, p_) of (Istate.Pstate pst, ctxt) => (pst, ctxt)

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

      val asm = (case get_obj g_tac pt p of (*collects and instantiates asms*)

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

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

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

    in

      if pp = []

      then 

	      let

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

      else

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

          val thy = Celem.assoc_thy (get_obj g_domID pt (par_pblobj pt (lev_up p)));

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

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

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

	        val ctxt'' = ContextC.from_subpbl_to_caller ctxt prog_res ctxt'

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

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

  | by_tactic tac_ is (pt, pos) =

    let

      val pos = case pos of

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

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

 		  | _ => 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_next_tactic from program, by_tactic will update the ctree*)

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

    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 (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;

      in

        case find_next_tactic 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 =>

                 ([(Tactic.End_Detail, 

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

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

         | 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_))): 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

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

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

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

     end

  | locate_input_formula _ _ _ _ _ = error ""

(**)end(**)