(* Title: \<open>\<close>

   Author: Walther Neuper 061019

   (c) due to copyright terms

*)

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

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

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

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

(*"----------- CAS-command Simplify -----------------------";*)

"----------- append inform with final result ------------";

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

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

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

val thy = @{theory "Simplify"};

(*

  This test is postponed within Isabelle/PIDE/isac development, 

  because respective user-requirements are not clarified.

  See test/../cas-command.sml --- start Calculation with CAS_Cmd ---

  and test/../Test_VSCode_Example.thy subsubsection \<open>Start Example with a CAS_Cmd\<close>

  "----------- CAS-command Simplify -----------------------";

  "----------- CAS-command Simplify -----------------------";

  "----------- CAS-command Simplify -----------------------";

  States.reset ();

  CalcTree [([], References.empty)];

  Iterator 1;

  moveActiveRoot 1;

  replaceFormula 1 "Simplify (2*a + 3*a)";

  autoCalculate 1 (Steps 1);

  autoCalculate 1 CompleteCalc;

  val ((pt,p),_) = States.get_calc 1;

  val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res)); Test_Tool.show_pt pt; UnparseC.term res;

  if p = ([], Res) andalso UnparseC.term res = "5 * a" then ()

  else error "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)";

*)

"----------- append inform with final result ------------";

"----------- append inform with final result ------------";

"----------- append inform with final result ------------";

States.reset ();

CalcTree [(["Term ((14 * x * y) / ( x * y ))", "normalform N"],

	("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

val ((pt,p),_) = States.get_calc 1; 

Test_Tool.show_pt pt; (*[

(([], Frm), Simplify (14 * x * y / (x * y)))] *)

ME_Misc.pt_extract (pt, p); (*determines SOME (Apply_Method ["simplification", "of_rationals"])*)

(*/------------------- step into autoCalculate 1 (Steps 1) \<longrightarrow> Apply_Method ----------------\*)

"~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, Steps 1);

     val pold = States.get_pos cI 1

(** )val ("ok", [], (_, ([], Met))) =    (*case*)                                      ( *isa*)

(**)val ("ok", [], (_, ([1], Frm))) =   (*case*)                                     (*isa2*)

Math_Engine.autocalc [] pold (States.get_calc cI) auto (*of*);

"~~~~~  fun autocalc , args:"; val (c, ip, cs, (Solve.Steps s)) = ([], pold, (States.get_calc cI), auto);

    (*if*) s <= 1 (*then*);

(** )  val ("ok", (                                                                    (*isa*)

        [(Specify_Method ["simplification", "of_rationals"], _, (([], Met), (Uistate, _)))],

           [], (_, ([], Met)))) = ( **)

(**)  val ("ok", (                                                                      (*isa2*)

        [(Apply_Method ["simplification", "of_rationals"], _, (([1], Frm), (pstate, _)))],

           [], (_, ([1], Frm)))) = (**)

      Step.do_next ip cs;

"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (ip, cs);

  (*if*) Pos.on_calc_end ip (*else*);

      val ("Rational", probl_id as ["rational", "simplification"], ["simplification", "of_rationals"]) =

  Calc.references (pt, p);                                                        (*isa == isa2*)

val _ =

      (*case*) tacis (*of*);

        (*if*) probl_id = Problem.id_empty (*else*);

(** )  val ("ok", (                                                                     (*isa*)

        [(Specify_Method ["simplification", "of_rationals"], _, (([], Met), (Uistate, _)))],

           [], (_, ([], Met)))) = ( **)

(**)  val ("ok", (                                                                      (*isa2*)

        [(Apply_Method ["simplification", "of_rationals"], _, (([1], Frm), (pstate, _)))],

           [], (_, ([1], Frm)))) = (**)

           switch_specify_solve p_ (pt, ip);

"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));

      (*if*) Pos.on_specification ([], state_pos) (*then*);

(** )  val ("ok", (                                                                     (*isa*)

        [(Specify_Method ["simplification", "of_rationals"], _, (([], Met), (Uistate, _)))],

           [], (_, ([], Met)))) = ( **)

(**)  val ("ok", (                                                                      (*isa2*)

        [(Apply_Method ["simplification", "of_rationals"], _, (([1], Frm), (pstate, _)))],

           [], (_, ([1], Frm)))) = (**)

           specify_do_next (pt, input_pos);

"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);

    val (_, (p_', tac)) = Specify.find_next_step ptp

(** ) val (_, (Met, Specify_Method ["simplification", "of_rationals"])) =             ( *isa*)

(**) val (_, (Met, Apply_Method ["simplification", "of_rationals"])) =               (*isa2*)

   Specify.find_next_step ptp;

"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);

    val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,

      spec = refs, ...} = Calc.specify_data (pt, pos);

      (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);

        (*if*) p_ = Pos.Pbl (*else*);

(** ) val (_, (Met, Specify_Method ["simplification", "of_rationals"])) =             ( *isa*)

(**) val (_, (Met, Apply_Method ["simplification", "of_rationals"])) =               (*isa2*)

           for_method_PIDE ctxt oris (o_refs, refs) (pbl, met);

"~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =

  (oris, (o_refs, refs), (pbl, met));

    val cmI = if mI = MethodC.id_empty then mI' else mI;

    val {ppc = mpc, prls, pre, ...} = MethodC.from_store ctxt cmI;    (*..MethodC ?*)

(** ) val (preok as false, _) = Pre_Conds.check prls pre pbl 0;                       ( *isa*)

(**) val (preok as true, _) = Pre_Conds.check prls pre pbl 0;                        (*isa2*)

 (*####  eval asms: "14 * x * y / (x * y) is_ratpolyexp = False"                       (*isa*)

                                                         True                        ( *isa2*)

(*\------------------- step into autoCalculate 1 (Steps 1) \<longrightarrow> Apply_Method ----------------/*)

val ((pt,p),_) = States.get_calc 1;  

Test_Tool.show_pt pt;

(*[

(([], Frm), Simplify (14 * x * y / (x * y))),

(([1], Frm), 14 * x * y / (x * y))] *)

appendFormula 1 "14::real" 

(* INPUT WITHOUT ^^^^^^^^ VARIABLES (WITH TYPE FROM  ctxt) WOULD REQUIRE ADDITIONAL ATTENTION*);

val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;

(*[

(([], Frm), Simplify (14 * x * y / (x * y))),

(([1], Frm), 14 * x * y / (x * y)),

(([1,1], Frm), 14 * x * y / (x * y)),

(([1,1], Res), 14 * (x * y) / (x * y)),

(([1,2], Res), 14 / 1),

(([1,3], Res), 14),

(([1], Res), 14)]*)

autoCalculate 1 (Steps 1);

val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;

(*[

(([], Frm), Simplify (14 * x * y / (x * y))),

(([1], Frm), 14 * x * y / (x * y)),

(([1,1], Frm), 14 * x * y / (x * y)),

(([1,1], Res), 14 * (x * y) / (x * y)),

(([1,2], Res), 14 / 1),

(([1,3], Res), 14),

(([1], Res), 14),

(([], Res), 14)] *)

val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res));

if p = ([], Res) andalso UnparseC.term res = "14" then ()

else error "simplify.sml: append inform with final result changed";