(* Title:  test/../generate.sml

   Author: Walther Neuper 110320

   (c) copyright due to lincense terms.

*)

"-----------------------------------------------------------------";

"table of contents -----------------------------------------------";

"-----------------------------------------------------------------";

"--------- embed fun generate_inconsistent_rew -------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"--------- embed fun generate_inconsistent_rew -------------------";

"--------- embed fun generate_inconsistent_rew -------------------";

"--------- embed fun generate_inconsistent_rew -------------------";

reset_states ();

CalcTree

[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], 

  ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

autoCalculate 1 (Step 1);

autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)

appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*);

(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),

  would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.

  results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>

  instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)

(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================

findFillpatterns 1 "chain-rule-diff-both";

(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =

  d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)

"~~~~~ fun requestFillformula, args:"; val (cI, (errpatID, fillpatID)) =

  (1, ("chain-rule-diff-both", "fill-both-args"));

    val ((pt, _), _) = get_calc cI

		    val pos as (p, _) = get_pos cI 1;

    val fillforms = find_fillpatterns (pt, pos) errpatID;

if pos = ([1], Res) then () else error "generate_inconsistent_rew changed 1";

 val (_, fillform, thm, sube_opt) :: _ = filter ((curry op = fillpatID) o 

        (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms;

"~~~~~ fun generate_inconsistent_rew, args:";

  val ((subs_opt, thm'), f', (is, ctxt), pos, pt) =

    ((sube_opt, thm'_of_thm thm), fillform, (get_loc pt pos), pos, pt);

    val f = get_curr_formula (pt, pos);

    val pos' as (p', _) = (lev_on p, Res);

if pos = ([1], Res) then () else error "generate_inconsistent_rew changed 2a";

if term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"

  then () else error "generate_inconsistent_rew changed 2b";

    val (pt,c) = 

      case subs_opt of

        NONE => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f

          (Rewrite thm') (f', []) Inconsistent

      | SOME subs => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f

          (Rewrite_Inst (subs, thm')) (f', []) Inconsistent

    val pt = update_branch pt p' TransitiveB;

if get_obj g_tac pt p' = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))

  andalso pos = ([1], Res) andalso pos' = ([2], Res) andalso p' = [2]

then () else error "generate_inconsistent_rew changed 3";

"~~~~~ to requestFillformula return val:"; val (pt, pos') = (pt, pos');

(*val (pt, pos') = generate_inconsistent_rew (sube_opt, thm'_of_thm thm)

            (fillform, []) (get_loc pt pos) pos' pt*)

upd_calc cI ((pt, pos'), []); upd_ipos cI 1 pos';

"~~~~~ final check:";

val ((pt, _),_) = get_calc 1;

val p = get_pos 1 1;

val (Form f, _, asms) = pt_extract (pt, p);

if p = ([2], Res) andalso 

  get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "")) andalso

  term2str f =

  "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?u * d_d x ?_dummy_2"

  (*WAS with old findFillpatterns:

  "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3"

  WN120731 replaced 

  "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?u * d_d x ?_dummy_2"

  WN120804 replaced

  "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos ?_dummy_1 * d_d x ?_dummy_2"*)

then () else error "generate_inconsistent_rew changed: fill-formula?";

show_pt pt; (*ATTENTION: omits the last step, if pt is incomplete, ([2], Res) EXISTS !*)

============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)