(* Title:  ProgLang/auto_prog.sml

   Author: Walther Neuper 190922

   (c) due to copyright terms

*)

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

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

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

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

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

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

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

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

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

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

"-------- fun stacpbls, fun eval_leaf -----------------------------------";

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

"-------- fun subst_typ ------------------------------------------------------------------------";

"-------- fun subst_typs -----------------------------------------------------------------------";

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

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

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

"-------- 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 = get_rls @{context} "integration";

val thy' = @{theory "Integrate"}

val ctxt = Proof_Context.init_global thy'

val t = @{term "ttt :: real"};

 Auto_Prog.gen thy' t rls;

"~~~~~ fun gen , args:"; val (thy, t, rls) = (thy', t, rls);

    val prog = case rls of

	      Rule_Set.Repeat {rules, ...} => rules2scr_Rls thy rules

	    | Rule_Set.Sequence {rules, ...} => rules2scr_Seq thy rules

    val auto_script = subst_typs prog (type_of t) (TermC.guess_bdv_typ t) (*return from generate*);

if UnparseC.term auto_script =

  "auto_generated_inst t_t v =\n" ^

  "(Try (Rewrite_Set_Inst [(''bdv'', v)] ''integration_rules'') #>\n" ^

  " Try (Rewrite_Set_Inst [(''bdv'', v)] ''add_new_c'') #>\n" ^

  " Try (Rewrite_Set_Inst [(''bdv'', v)] ''simplify_Integral''))\n" ^

  " ??.empty"

then () else error "Auto_Prog.gen integration CHANGED";

if contain_bdv (get_rules rls) then ()

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

if UnparseC.terms (formal_args auto_script) = "[\"t_t\", \"v\"]"

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

    Istate.init_detail ctxt (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) (TermC.parse_test @{context} "someTermWithBdv");

"~~~~~ fun init_detail , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t)

  = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), TermC.parse_test @{context} "someTermWithBdv");

      val v = case Tactic.subst_adapt_to_type ctxt subs of

        (_, v) :: _ => v;

    (*case*) get_rls ctxt rls (*of*);

"-------- 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 thy' = @{theory "Poly"}

val ctxt = Proof_Context.init_global thy'

val rls = get_rls ctxt "norm_Poly";

val t = @{term "ttt :: real"}

val auto_script = Auto_Prog.gen thy' t rls;

if UnparseC.term auto_script =

  "auto_generated t_t =\n" ^

  "(Try (Rewrite_Set ''discard_minus'') #>\n" ^

  " Try (Rewrite_Set ''expand_poly_'') #>\n" ^

  " Try (Repeat (Calculate ''TIMES'')) #>\n" ^

  " Try (Rewrite_Set ''order_mult_rls_'') #>\n" ^

  " Try (Rewrite_Set ''simplify_power_'') #>\n" ^

  " Try (Rewrite_Set ''calc_add_mult_pow_'') #>\n" ^

  " Try (Rewrite_Set ''reduce_012_mult_'') #>\n" ^

  " Try (Rewrite_Set ''order_add_rls_'') #>\n" ^

  " Try (Rewrite_Set ''collect_numerals_'') #>\n" ^

  " Try (Rewrite_Set ''reduce_012_'') #>\n" ^

  " Try (Rewrite_Set ''discard_parentheses1''))\n" ^

  " ??.empty"  (*                          ..WORKS, NEVERTHELESS*)

then () else error "Auto_Prog.gen norm_Poly CHANGED";

States.reset (); (*<-- evaluate, if ML-blocks are edited below*)

CalcTree @{context}

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

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

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

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

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

Test_Tool.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),_) = States.get_calc 1; Test_Tool.show_pt pt;

Test_Tool.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) = States.get_calc cI;

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

val ip' = lev_pred' pt ip;

(*Detail_Step.go pt ip      ..ERROR interSteps>..>init_detail: "norm_Poly" has Empty_Prog*)

val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Detail_Step.go pt ip;

"~~~~~ fun go, 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))], Pos.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),_) = States.get_calc 1; Test_Tool.show_pt pt;

Test_Tool.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 thy = @{theory (** )"Poly" ( **) Rational(**) (*required for rls "norm_Rational"*)}

val ctxt = Proof_Context.init_global thy

val auto_script = 

  Auto_Prog.gen thy @{term "ttt :: real"} (get_rls ctxt "norm_Rational");

writeln(UnparseC.term auto_script);

TermC.atom_trace_detail @{context} 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 => '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  => '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  => '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  => '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  => 'a => 'a)

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

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

*** . . . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)

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

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

***)

States.reset ();

CalcTree @{context}

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

  ((** )"Poly"( **)"Rational"(**),["polynomial", "simplification"],

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

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

interSteps 1 ([], Res);

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

interSteps 1 ([1], Res);

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

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

       \  ((Rewrite_Set norm_Rational) t_)"

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

*)

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

case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of

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

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

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

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

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

 val rules = (#rules o Rule_Set.rep) isolate_root;

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

 val t = #> rs;

if UnparseC.term 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 rules2scr_Rls --------------------------------------------------------------------";

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

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

(*compare Prog_Expr.*)

val prog = Auto_Prog.rules2scr_Rls @{theory} [\<^rule_thm>\<open>thm111\<close>, \<^rule_thm>\<open>refl\<close>]

;

writeln (UnparseC.term_in_thy @{theory} prog);

(*auto_generated t_t =

Repeat

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

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

   ??.empty)*)

;

if UnparseC.term_in_thy @{theory} prog =

  "auto_generated t_t =\n" ^

  "Repeat\n" ^

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

  "   ??.empty)"

then () else error "rules2scr_Rls auto_generated changed";

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

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

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

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

if UnparseC.term t = "Try (Repeat (Rewrite ''real_diff_minus''))" then ()

else error "rule2stac Thm.. changed";

val t = rule2stac @{theory} (Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"));

if UnparseC.term t = "Try (Repeat (Calculate ''PLUS''))" then ()

else error "rule2stac Eval.. changed";

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

if UnparseC.term t = "Try (Rewrite_Set ''rearrange_assoc'')" then ()

else error "rule2stac Rls_.. changed";

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

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

else error "rule2stac_inst Thm.. changed";

case t of

  (Const (\<^const_name>\<open>Try\<close>, _) $

    (Const (\<^const_name>\<open>Repeat\<close>, _) $

      (Const (\<^const_name>\<open>Rewrite_Inst\<close>, _) $

        (Const (\<^const_name>\<open>Cons\<close>, _) $

          (Const (\<^const_name>\<open>Pair\<close>, _) $

            bdv $

            Free ("v", _)) $

          Const (\<^const_name>\<open>Nil\<close>, _)) $

        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 stacpbls, fun eval_leaf -----------------------------------";

"-------- fun stacpbls, fun eval_leaf -----------------------------------";

"-------- fun stacpbls, fun eval_leaf -----------------------------------";

val {program, ...} = MethodC.from_store ctxt ["Test", "sqrt-equ-test"]; val Prog sc = program; val ts = stacpbls sc;

case stacpbls sc of

  [Const (\<^const_name>\<open>Rewrite\<close>, _) $ square_equation_left,

   Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ Test_simplify,

   Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ rearrange_assoc,

   Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ isolate_root,

   Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ norm_equation,

   Const (\<^const_name>\<open>Rewrite_Set_Inst\<close>, _) $

     (Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ bdv $ Free ("v_v", _)) $

       Const (\<^const_name>\<open>Nil\<close>, _)) $ isolate_bdv] => 

     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 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 sc = Auto_Prog.gen thy' t 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 = ((get_calc (@{theory} |> Proof_Context.init_global) |> map) o (map Auto_Prog.op_of_calc) o

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

case calcs of

  [("PLUS", (\<^const_name>\<open>plus\<close>, _)), ("TIMES", (\<^const_name>\<open>times\<close>, _)), 

  ("DIVIDE", (\<^const_name>\<open>divide\<close>, _)), ("POWER", (\<^const_name>\<open>realpow\<close>, _))] => ()

| _ => error "get_calcs changed"

"-------- fun subst_typ ------------------------------------------------------------------------";

"-------- fun subst_typ ------------------------------------------------------------------------";

"-------- fun subst_typ ------------------------------------------------------------------------";

val thy = @{theory "Isac_Knowledge"}

val ctxt = Proof_Context.init_global thy

val prog = Auto_Prog.gen thy t (get_rls ctxt "isolate_bdv");

(* UnparseC.term prog |> writeln

auto_generated_inst t_t v =

Repeat

 ((Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'')) #>

   Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult_add'')) #>

   Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult'')) #>

   Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''mult_square'')) #>

   Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_square'')) #>

   Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_mult_square'')))

   ??.empty) 

*)

val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)

if length frees = 2 then () else error "test setup Auto_Prog.subst_typ changed 1";

val args = formal_args prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)

if length args = 2 then () else error "test setup Auto_Prog.subst_typ changed 2";

val typ_t = HOLogic.realT

val typ_bdv = HOLogic.realT

val vars_v = (* = [Free ("v", "real"), Free ("v", "'a")]*)

  filter (fn t => curry op = (t |> dest_Free |> fst) "v") frees

val typs_v = (* = ["real", "'a"]*)

  map (fn t => (t |> dest_Free |> snd)) vars_v;

val subst_ty = subst_typ "v" HOLogic.realT frees; (* = [("real", "real")]*)

if length subst_ty = 1 then () else error "Auto_Prog.subst_typ changed";

"-------- fun subst_typs -----------------------------------------------------------------------";

"-------- fun subst_typs -----------------------------------------------------------------------";

"-------- fun subst_typs -----------------------------------------------------------------------";

val prog = Auto_Prog.gen thy' t (get_rls ctxt "isolate_bdv");

val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real"), Free ("v", "'a")]*)

if length frees = 2 then () else error "test setup Auto_Prog.subst_typs changed 1";

val args = formal_args prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)

if length args = 2 then () else error "test setup Auto_Prog.subst_typs changed 2";

val prog' = subst_typs prog HOLogic.realT HOLogic.realT

val frees' = vars prog'; (* = [Free ("t_t", "'z"), Free ("v", "real")]*);

if length frees' = 2 then () else error "Auto_Prog.subst_typs changed 2"