(* Title: "ProgLang/scrtools.sml"

           tests on tools for scripts

   Author: Walther Neuper 060605

   (c) due to copyright terms

*)

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

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

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

"-------- test the same called by interSteps norm_Poly -----------";

"-------- test the same called by interSteps norm_Rational -------";

"-------- check auto-gen.script for Rewrite_Set_Inst -------------";

"-------- distinguish input to Model -----------------------------------------";

"-------- fun subpbl, fun pblterm --------------------------------------------";

"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";

"-------- fun is_calc, fun op_of_calc ----------------------------------------";

"-------- fun rule2stac, fun rule2stac_inst ----------------------------------";

"-------- fun op #> ----------------------------------------------------------";

"-------- fun get_fun_id -----------------------------------------------------";

"-------- fun rules2scr_Rls --------------------------------------------------";

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

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

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

"-------- test the same called by interSteps norm_Poly -----------";

"-------- test the same called by interSteps norm_Poly -----------";

"-------- test the same called by interSteps norm_Poly -----------";

val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";

writeln(term2str auto_script);

(*Program Stepwise t_t   =

 (Try (Rewrite_Set discard_minus) #>

  Try (Rewrite_Set expand_poly_) #>

  Try (Repeat (Calculate TIMES)) #>

  Try (Rewrite_Set order_mult_rls_) #>

  Try (Rewrite_Set simplify_power_) #>

  Try (Rewrite_Set calc_add_mult_pow_) #>

  Try (Rewrite_Set reduce_012_mult_) #>

  Try (Rewrite_Set order_add_rls_) #>

  Try (Rewrite_Set collect_numerals_) #>

  Try (Rewrite_Set reduce_012_) #>

  Try (Rewrite_Set discard_parentheses1))

  ??.empty                                          ..WORKS, NEVERTHELESS *)

atomty auto_script;

reset_states (); (*<-- evaluate, if ML-blocks are edited below*)

CalcTree

[(["Term (b + a - b)", "normalform N"], 

  ("Poly",["polynomial","simplification"],

  ["simplification","for_polynomials"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

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

show_pt pt;

(* isabisac17 = 15 [

(([], Frm), Simplify (b + a - b)),

(([1], Frm), b + a - b),

(([1], Res), a),

(([], Res), a)] *)

interSteps 1 ([], Res);

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

show_pt pt;

(* isabisac17 = 15 [

(([], Frm), Simplify (b + a - b)),

(([1], Frm), b + a - b),

(([1], Res), a),

(([], Res), a)] *)

interSteps 1 ([1], Res);(*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 8</ERROR></SYSERROR>*)

"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res));

 val ((pt, p), tacis) = get_calc cI;

(*if*) (not o is_interpos) ip = false;

val ip' = lev_pred' pt ip;

(*Math_Engine.detailstep pt ip      ..ERROR interSteps>..>init_istate: "norm_Poly" has EmptyScr*)

val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Math_Engine.detailstep pt ip;

"~~~~~ fun detailstep, args:"; val (pt, (pos as (p, _))) = (pt, ip);

    val nd = Ctree.get_nd pt p

    val cn = Ctree.children nd;

(*if*) null cn = false;

"~~~~~ to detailrls return val:";

(*else*) 

val return_val = ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Ctree.Res));

if p @ [length (Ctree.children (Ctree.get_nd pt p))] = [1, 4]

then () else error "detailrls: auto-generated norm_Poly doesnt work";

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

show_pt pt; (*[

(([], Frm), Simplify (b + a - b)),

(([1], Frm), b + a - b),

(([1,1], Frm), b + a - b),

(([1,1], Res), b + a + -1 * b),

(([1,2], Res), a + b + -1 * b),

(([1,3], Res), a + 0 * b),

(([1,4], Res), a),

(([1], Res), a),

(([], Res), a)]  *)

if existpt' ([1,4], Res) pt then ()

else error  "auto-generated norm_Poly doesnt work";

"-------- test the same called by interSteps norm_Rational -------";

"-------- test the same called by interSteps norm_Rational -------";

"-------- test the same called by interSteps norm_Rational -------";

val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Rational";

writeln(term2str auto_script);

atomty auto_script;

(*** 

*** Const (Program.Stepwise, 'z => 'z => 'z)

*** . Free (t_t, 'z)

*** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)

*** . . Const (Program.Try, ('a => 'a) => 'a => 'a)

*** . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)

*** . . . . Free (discard_minus, ID)

*** . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)

*** . . . Const (Program.Try, ('a => 'a) => 'a => 'a)

*** . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)

*** . . . . . Free (rat_mult_poly, ID)

*** . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)

*** . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)

*** . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)

*** . . . . . . Free (make_rat_poly_with_parentheses, ID)

*** . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)

*** . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)

*** . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)

*** . . . . . . . Free (cancel_p_rls, ID)

*** . . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)

*** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)

*** . . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)

*** . . . . . . . . Free (norm_Rational_rls, ID)

*** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)

*** . . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)

*** . . . . . . . . Free (discard_parentheses1, ID)

*** . . Const (empty, 'a)

***)

reset_states ();

CalcTree

[(["Term (b + a - b)", "normalform N"], 

  ("Poly",["polynomial","simplification"],

  ["simplification","of_rationals"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

interSteps 1 ([], Res);

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

interSteps 1 ([1], Res);

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

(*with "Program SimplifyScript (t_::real) =                \

       \  ((Rewrite_Set norm_Rational) t_)"

val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));

*)

val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));

case (term2str form, tac, terms2strs asm) of

    ("a", Check_Postcond ["polynomial", "simplification"], []) => ()

  | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";

"-------- check auto-gen.script for Rewrite_Set_Inst -------------";

"-------- check auto-gen.script for Rewrite_Set_Inst -------------";

"-------- check auto-gen.script for Rewrite_Set_Inst -------------";

val rls = assoc_rls "integration";

val Seq {scr = Prog auto_script,...} = rls;

writeln(term2str auto_script);

if contain_bdv (get_rules rls) then ()

else error "scrtools.sml: contain_bdv doesnt work for 'integration'";

if terms2str (formal_args auto_script) = "[\"t_t\",\"v\"]"

then () else error "formal_args of auto-gen.script changed";

init_istate (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) 

			      (str2term "someTermWithBdv");

"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";

"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";

"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";

val {scr, ...} = get_met ["Test","sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;

case stacpbls sc of

  [Const ("Prog_Tac.Rewrite", _) $ square_equation_left,

   Const ("Prog_Tac.Rewrite'_Set", _) $ Test_simplify,

   Const ("Prog_Tac.Rewrite'_Set", _) $ rearrange_assoc,

   Const ("Prog_Tac.Rewrite'_Set", _) $ isolate_root,

   Const ("Prog_Tac.Rewrite'_Set", _) $ norm_equation,

   Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $

     (Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ bdv $ Free ("v_v", _)) $

       Const ("List.list.Nil", _))] => 

     if HOLogic.dest_string square_equation_left = "square_equation_left" andalso

       HOLogic.dest_string Test_simplify = "Test_simplify" andalso

       HOLogic.dest_string rearrange_assoc = "rearrange_assoc" andalso

       HOLogic.dest_string isolate_root = "isolate_root" andalso

       HOLogic.dest_string norm_equation = "norm_equation" andalso

       HOLogic.dest_string bdv = "bdv" andalso

       HOLogic.dest_string isolate_bdv = "isolate_bdv"

     then () else error "stacpbls (Test.Solve_root_equation) changed 2"

| _  => error "stacpbls (Test.Solve_root_equation) changed 1";

(* inappropriate input is skipped *)

val t = @{term "(a::real) = (rhs (NTH 1 sol_a))"};

case stacpbls t of [] => () | _ => error "stacpbls rhs (NTH 1 sol_a) changed";

@{term "(SubProblem (BiegelinieX,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};

case stacpbls t of [] => () | _ => error "stacpbls (SubProblem ...) changed";

(* --- fun subst_stacexpr *)

case  subst_stacexpr [] NONE e_term  sc of

(NONE, Expr (Const ("HOL.eq", _) $

 (Const ("Test.solve_root_equ", _) $ Free ("e_e", _) $ Free ("v_v", _)) $

  (Const ("HOL.Let", _) $

    (Const ("Tactical.Seq", _) $

      (Const ("Tactical.While", _) $ _ $

        _ ) $

      (_) $

      Free ("e_e", _)) $

    Abs ("e_e", _, Const ("List.list.Cons", _) $ Free ("e_e", _) $ Const ("List.list.Nil", _)) )

)) => ()

| _ => error "subst_stacexpr [] NONE e_term";

"-------- fun is_calc, fun op_of_calc ----------------------------------------";

"-------- fun is_calc, fun op_of_calc ----------------------------------------";

"-------- fun is_calc, fun op_of_calc ----------------------------------------";

val rls = prep_rls @{theory} Test_simplify; (* adds the Program *)

val Prog sc = (#scr o rep_rls) rls;

val stacs = stacpbls sc;

val calcs = filter is_calc stacs;

val ids = map op_of_calc calcs;

case ids of

  ["PLUS", "TIMES", "DIVIDE", "POWER"] => ()

| _ => error "op_of_calc";

val calcs = ((assoc_calc' @{theory} |> map) o (map LTool.op_of_calc) o

  (filter LTool.is_calc) o LTool.stacpbls) sc;

case calcs of

  [("PLUS", ("Groups.plus_class.plus", _)), ("TIMES", ("Groups.times_class.times", _)), 

  ("DIVIDE", ("Rings.divide_class.divide", _)), ("POWER", ("Prog_Expr.pow", _))] => ()

| _ => error "get_calcs changed"

"-------- fun rule2stac, fun rule2stac_inst ----------------------------------";

"-------- fun rule2stac, fun rule2stac_inst ----------------------------------";

"-------- fun rule2stac, fun rule2stac_inst ----------------------------------";

val t = rule2stac @{theory} (Thm ("real_diff_minus", num_str @{thm real_diff_minus}));

if term2str t = "Try (Repeat (Rewrite ''real_diff_minus''))" then ()

else error "rule2stac Thm.. changed";

val t = rule2stac @{theory} (Calc ("Groups.plus_class.plus", eval_binop "#add_"));

if term2str t = "Try (Repeat (Calculate ''PLUS''))" then ()

else error "rule2stac Calc.. changed";

val t = rule2stac @{theory} (Rls_ rearrange_assoc);

if term2str t = "Try (Rewrite_Set ''rearrange_assoc'')" then ()

else error "rule2stac Rls_.. changed";

val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", num_str @{thm risolate_bdv_add}));

if term2str t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''))" then ()

else error "rule2stac_inst Thm.. changed";

case t of

  (Const ("Tactical.Try", _) $

    (Const ("Tactical.Repeat", _) $

      (Const ("Prog_Tac.Rewrite'_Inst", _) $

        (Const ("List.list.Cons", _) $

          (Const ("Product_Type.Pair", _) $

            bdv $

            Free ("v", _)) $

          Const ("List.list.Nil", _)) $

        risolate_bdv_add))) => 

      (if HOLogic.dest_string bdv = "bdv" andalso 

        HOLogic.dest_string risolate_bdv_add = "risolate_bdv_add" then ()

      else error "rule2stac_inst changed 1")

| _ => error "rule2stac_inst changed 2"

"-------- fun op #> ----------------------------------------------------------";

"-------- fun op #> ----------------------------------------------------------";

"-------- fun op #> ----------------------------------------------------------";

 val rules = (#rules o rep_rls) isolate_root;

 val rs = map (rule2stac @{theory}) rules;

 val t = #> rs;

if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) #>\n" ^ 

  "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) #>\n" ^ 

  "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) #>\n" ^ 

  "Try (Repeat (Rewrite ''risolate_root_add'')) #>\n" ^ 

  "Try (Repeat (Rewrite ''risolate_root_mult'')) #>\n" ^ 

  "Try (Repeat (Rewrite ''risolate_root_div''))"

then () else error "fun #> changed"

"-------- fun get_fun_id -----------------------------------------------------";

"-------- fun get_fun_id -----------------------------------------------------";

"-------- fun get_fun_id -----------------------------------------------------";

(* fun_id is nested into arguments, compare ... *)

val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $

      (((((((Const (const_id, const_typ) $ _) $ _) $ _) $ _) $ _) $ _) $ _) $ _) =

  Thm.prop_of @{thm biegelinie.simps};

(* ... to: *)

val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $

      (Const (const_id, const_typ) $ _) $ _) =

  Thm.prop_of @{thm simplify.simps};

(* get fun_id out of nesting *)

val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $

      nested $ _) =

  Thm.prop_of @{thm biegelinie.simps};

val (Const ("Biegelinie.biegelinie", _) $ 

      Var (("l", 0), _) $

        Var (("q", 0), _) $

          Var (("v", 0), _) $

            Var (("b", 0), _) $

              Var (("s", 0), _) $

                Var (("vs", 0), _) $

                Var (("id_abl", 0), _)) = nested;

strip_comb nested;

(*val it =

   (Const ("Biegelinie.biegelinie", "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool")

    ,

    [Var (("l", 0), "real"), Var (("q", 0), "real"), Var (("v", 0), "real"),

     Var (("b", 0), "real \<Rightarrow> real"), Var (("s", 0), "bool list")]):

   term * term list*)

case get_fun_id (prep_program @{thm biegelinie.simps}) of

  ("Biegelinie.biegelinie", _) => ()

| _ => error "get_fun_id changed";

case get_fun_id (prep_program @{thm simplify.simps}) of

  ("PolyMinus.simplify", _) => ()

| _ => error "get_fun_id changed";

"-------- fun rules2scr_Rls --------------------------------------------------";

"-------- fun rules2scr_Rls --------------------------------------------------";

"-------- fun rules2scr_Rls --------------------------------------------------";

(*compare Prog_Expr.*)

val prog = LTool.rules2scr_Rls @{theory} [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})]

;

writeln (t2str @{theory} prog);

(*auto_generated t_t =

Repeat

 ((Try (Repeat (Rewrite ''thm111'')) #>

   Try (Repeat (Rewrite ''refl'')))

   ??.empty)*)

;

if t2str @{theory} prog =

"auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''thm111'')) #>\n   Try (Repeat (Rewrite ''refl'')))\n   ??.empty)"

then () else error "rules2scr_Rls auto_generated changed"