test/Tools/isac/Interpret/lucas-interpreter.sml
author Walther Neuper <walther.neuper@jku.at>
Tue, 19 Nov 2019 14:19:44 +0100
changeset 59712 be2ffb0248de
parent 59709 e49fb19892bd
child 59717 cc83c55e1c1c
permissions -rw-r--r--
lucin: improve naming for constructors in scans
wneuper@59561
     1
(* Title:  "Interpret/lucas-interpreter.sml"
wneuper@59561
     2
   Author: Walther Neuper
wneuper@59561
     3
   (c) due to copyright terms
wneuper@59561
     4
*)
wneuper@59561
     5
wneuper@59561
     6
"-----------------------------------------------------------------------------------------------";
wneuper@59561
     7
"table of contents -----------------------------------------------------------------------------";
wneuper@59561
     8
"-----------------------------------------------------------------------------------------------";
wneuper@59561
     9
"----------- Take as 1st stac in program -------------------------------------------------------";
walther@59670
    10
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
walther@59670
    11
"----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
walther@59670
    12
"----------- re-build: fun determine_next_tactic -----------------------------------------------";
wneuper@59564
    13
"----------- re-build: fun locate_input_formula ------------------------------------------------";
wneuper@59561
    14
"-----------------------------------------------------------------------------------------------";
wneuper@59561
    15
"-----------------------------------------------------------------------------------------------";
wneuper@59561
    16
"-----------------------------------------------------------------------------------------------";
wneuper@59561
    17
wneuper@59561
    18
"----------- Take as 1st stac in program -------------------------------------------------------";
wneuper@59561
    19
"----------- Take as 1st stac in program -------------------------------------------------------";
wneuper@59561
    20
"----------- Take as 1st stac in program -------------------------------------------------------";
wneuper@59561
    21
val p = e_pos'; val c = []; 
wneuper@59561
    22
val (p,_,f,nxt,_,pt) = 
wneuper@59561
    23
    CalcTreeTEST 
wneuper@59561
    24
        [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
wneuper@59561
    25
          ("Integrate", ["integrate","function"], ["diff","integration"]))];
wneuper@59561
    26
val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
wneuper@59561
    27
val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59561
    28
val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59561
    29
val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59561
    30
val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59561
    31
val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59561
    32
val (p,_,f,nxt,_,pt) = me nxt p c pt;
wneuper@59561
    33
case nxt of (_, Apply_Method ["diff", "integration"]) => ()
wneuper@59561
    34
          | _ => error "integrate.sml -- me method [diff,integration] -- spec";
wneuper@59561
    35
"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
wneuper@59561
    36
wneuper@59561
    37
"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
wneuper@59561
    38
"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
wneuper@59561
    39
val (mI,m) = mk_tac'_ tac;
wneuper@59561
    40
val Appl m = applicable_in p pt m;
wneuper@59561
    41
member op = specsteps mI (*false*);
walther@59677
    42
"~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = ((mI,m), ptp);
walther@59686
    43
walther@59686
    44
"~~~~~ fun solve , args:"; val ((_, m as Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p,_)))) =
wneuper@59561
    45
                            (m, (pt, pos));
walther@59686
    46
      val {srls, ...} = get_met mI;
walther@59686
    47
      val itms = case get_obj I pt p of
walther@59686
    48
        PblObj {meth=itms, ...} => itms
walther@59686
    49
      | _ => error "solve Apply_Method: uncovered case get_obj"
walther@59686
    50
      val thy' = get_obj g_domID pt p;
walther@59686
    51
      val thy = Celem.assoc_thy thy';
walther@59686
    52
      val srls = Lucin.get_simplifier (pt, pos)
walther@59686
    53
      val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
walther@59686
    54
        (is as Istate.Pstate {env, ...}, ctxt, sc) =>  (is, env, ctxt, sc)
walther@59697
    55
      | _ => error "solve Apply_Method: uncovered case init_pstate";
walther@59696
    56
(*+*)scrstate2str (the_pstate is) = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, Aundef, AppUndef_, true)";
walther@59686
    57
      val ini = Lucin.init_form thy sc env;
walther@59686
    58
      val p = lev_dn p;
walther@59686
    59
walther@59686
    60
      val NONE = (*case*) ini (*of*);
walther@59686
    61
            val (m', (is', ctxt'), _) =
walther@59686
    62
              LucinNEW.determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
walther@59696
    63
(*+*)scrstate2str (the_pstate is') = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], e_rls, NONE, \nIntegral x ^^^ 2 + 1 D x, Aundef, AppUndef_, false)";
walther@59686
    64
  val Safe_Step (_, _, Take' _) = (*case*)
walther@59686
    65
           locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
walther@59692
    66
"~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)
walther@59686
    67
  = (sc, (pt, (p, Res)), is', ctxt', m');
walther@59686
    68
walther@59692
    69
    (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
walther@59692
    70
"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
walther@59692
    71
  = ((prog, (cstate, ctxt, tac)), istate);
walther@59686
    72
    (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
walther@59686
    73
walther@59712
    74
  val Ackn_Tac1 (_, _, Take' _) =
walther@59698
    75
       scan_dn1 cctt (ist |> set_path [R] |> set_or Aundef) (Program.body_of prog);
walther@59691
    76
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
walther@59698
    77
  = (cctt, (ist |> set_path [R] |> set_or Aundef), (Program.body_of prog));
walther@59686
    78
walther@59691
    79
(*+*) if term2str e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
walther@59686
    80
walther@59686
    81
    (*case*)
walther@59691
    82
           scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
walther@59686
    83
    (*======= end of scanning tacticals, a leaf =======*)
walther@59691
    84
"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
walther@59686
    85
  = (xxx, (ist |> path_down [L, R]), e);
walther@59686
    86
val (a', STac stac) = handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t;
wneuper@59561
    87
wneuper@59561
    88
walther@59670
    89
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
walther@59670
    90
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
walther@59670
    91
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
wneuper@59562
    92
val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
walther@59670
    93
val (dI',pI',mI') = ("Test", ["sqroot-test","univariate","equation","test"],
wneuper@59562
    94
   ["Test","squ-equ-test-subpbl1"]);
wneuper@59562
    95
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
wneuper@59562
    96
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59562
    97
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59562
    98
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59562
    99
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59562
   100
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
wneuper@59562
   101
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59670
   102
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
walther@59670
   103
(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
wneuper@59562
   104
walther@59670
   105
(*// relevant call --------------------------------------------------------------------------\\*)
walther@59686
   106
(*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
wneuper@59562
   107
walther@59670
   108
"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, [], pt);
wneuper@59562
   109
walther@59670
   110
    (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **)  (*case*) locatetac tac (pt,p) (*of*);
walther@59670
   111
"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
walther@59670
   112
      val (mI, m) = Solve.mk_tac'_ tac;
walther@59670
   113
      val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
walther@59670
   114
      (*if*) member op = Solve.specsteps mI; (*else*)
walther@59670
   115
walther@59670
   116
      (** )val (***)xxxxx(***) ( *Updated (cs' as (_, _, (_, p'))) =( **) loc_solve_ (mI,m) ptp;
walther@59670
   117
"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);
walther@59670
   118
walther@59670
   119
    (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **) Solve.solve m (pt, pos);
walther@59670
   120
"~~~~~ fun solve , args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos));
walther@59670
   121
(*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
walther@59670
   122
    (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)
walther@59670
   123
	      val thy' = get_obj g_domID pt (par_pblobj pt p);
walther@59670
   124
	      val (_, is, sc) = Lucin.from_pblobj' thy' (p,p_) pt;
walther@59670
   125
walther@59670
   126
     locate_input_tactic sc (pt, po) (fst is) (snd is) m;
walther@59692
   127
"~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
walther@59670
   128
    = (sc, (pt, po), (fst is), (snd is), m);
walther@59670
   129
      val srls = get_simplifier cstate;
walther@59670
   130
walther@59712
   131
 (** )val Ackn_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
walther@59692
   132
  (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
walther@59692
   133
"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
walther@59692
   134
  = ((prog, (cstate, ctxt, tac)), istate);
walther@59686
   135
    (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
walther@59670
   136
walther@59670
   137
    (** )val xxxxx_xx = ( **)
walther@59698
   138
           scan_dn1 cctt (ist |> set_path [R] |> set_or Aundef) (Program.body_of prog);
walther@59691
   139
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
walther@59698
   140
  = (cctt, (ist |> set_path [R] |> set_or Aundef), (Program.body_of prog));
walther@59670
   141
walther@59691
   142
  (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
walther@59691
   143
"~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a))
walther@59686
   144
  = (xxx, (ist |> path_down [L, R]), e);
walther@59670
   145
walther@59691
   146
  (*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
walther@59691
   147
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
walther@59686
   148
  = (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
walther@59670
   149
walther@59691
   150
  (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
walther@59670
   151
    (*======= end of scanning tacticals, a leaf =======*)
walther@59691
   152
"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
walther@59686
   153
  = (xxx, (ist |> path_down [R]), e);
walther@59686
   154
    val (a', Celem.STac stac) =
walther@59686
   155
      (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
walther@59686
   156
    val Lucin.Ass (m, v', ctxt) =
walther@59686
   157
      (*case*) associate pt ctxt (m, stac) (*of*);
walther@59670
   158
walther@59712
   159
       Ackn_Tac1 (ist |> set_subst_true  (a', v'), ctxt, m)  (*return value*);
walther@59691
   160
"~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
walther@59712
   161
  = (Ackn_Tac1 (ist |> set_subst_true  (a', v'), ctxt, m));
walther@59670
   162
walther@59712
   163
"~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Ackn_Tac1 ((ist as {assoc, ...}), ctxt, tac')
walther@59712
   164
  = (Ackn_Tac1 (ist |> set_subst_true  (a', v'), ctxt, m));
walther@59686
   165
        (*if*) LibraryC.assoc (*then*);
walther@59670
   166
walther@59686
   167
       Safe_Step (Istate.Pstate ist, ctxt, tac')  (*return value*);
walther@59686
   168
"~~~~~ from locate_input_tactic to fun solve return:"; val Safe_Step (istate, ctxt, tac)
walther@59686
   169
  = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
walther@59670
   170
walther@59670
   171
(*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of solve *)
walther@59686
   172
                  val (p'', _, _,pt') =
walther@59686
   173
                    Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
walther@59686
   174
                    (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
walther@59686
   175
                      (istate, ctxt) (lev_on p, Pbl) pt;
walther@59686
   176
            (*in*)
walther@59670
   177
walther@59704
   178
         	  	    ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
walther@59686
   179
                    [(*ctree NOT cut*)], (pt', p'')))  (*return value*);
walther@59670
   180
"~~~~~ from solve to loc_solve_ return:"; val ((msg, cs' : calcstate'))
walther@59704
   181
  =                    ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )], [(*ctree NOT cut*)], (pt', p'')));
walther@59670
   182
walther@59670
   183
"~~~~~ from loc_solve_ to locatetac return:"; val (Updated (cs' as (_, _, (_, p'))))
walther@59670
   184
   = (*** )xxxxx( ***) (Updated (cs'));
walther@59694
   185
          (*if*) p' = ([], Pos.Res); (*else*)
walther@59670
   186
          ("ok", cs');
walther@59670
   187
"~~~~~ from locatetac to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
wneuper@59562
   188
	  val (_, ts) =
walther@59694
   189
	    (case step p ((pt, Pos.e_pos'), []) of
wneuper@59562
   190
		    ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
wneuper@59562
   191
	    | ("helpless", _) => ("helpless: cannot propose tac", [])
wneuper@59562
   192
	    | ("no-fmz-spec", _) => error "no-fmz-spec"
wneuper@59562
   193
	    | ("end-of-calculation", (ts, _, _)) => ("", ts)
wneuper@59562
   194
	    | _ => error "me: uncovered case")
wneuper@59562
   195
	      handle ERROR msg => raise ERROR msg
wneuper@59562
   196
	  val tac = 
wneuper@59562
   197
      case ts of 
wneuper@59562
   198
        tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end 
walther@59694
   199
		  | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
wneuper@59562
   200
walther@59675
   201
   (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt);
walther@59670
   202
"~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
walther@59675
   203
   = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt);
walther@59670
   204
walther@59670
   205
(*//--------------------- check results from modified me ----------------------------------\\*)
walther@59686
   206
if p = ([2], Res) andalso
walther@59686
   207
  pr_ctree pr_short pt = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 = 2\n"
walther@59670
   208
then
walther@59670
   209
  (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
walther@59670
   210
   | _ => error "")
walther@59670
   211
else error "check results from modified me CHANGED";
walther@59670
   212
(*\\--------------------- check results from modified me ----------------------------------//*)
walther@59670
   213
walther@59670
   214
"~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
walther@59670
   215
(*\\------------------ end of modified "fun me" ---------------------------------------------//*)
walther@59686
   216
walther@59686
   217
(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
walther@59670
   218
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
walther@59670
   219
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*)
walther@59670
   220
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
walther@59670
   221
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
walther@59670
   222
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
walther@59670
   223
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
walther@59670
   224
(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
walther@59670
   225
(*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
walther@59670
   226
(*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
walther@59670
   227
(*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
walther@59670
   228
(*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
wneuper@59562
   229
(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
wneuper@59562
   230
(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
wneuper@59562
   231
(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
wneuper@59562
   232
walther@59670
   233
(*/--------------------- final test ----------------------------------\\*)
walther@59670
   234
if p = ([], Res) andalso f2str f = "[x = 1]" andalso fst nxt = "End_Proof'"
walther@59670
   235
  andalso pr_ctree pr_short pt =
walther@59670
   236
  ".    ----- pblobj -----\n" ^
walther@59670
   237
  "1.   x + 1 = 2\n" ^
walther@59670
   238
  "2.   x + 1 + -1 * 2 = 0\n" ^
walther@59670
   239
  "3.    ----- pblobj -----\n" ^
walther@59670
   240
  "3.1.   -1 + x = 0\n" ^
walther@59670
   241
  "3.2.   x = 0 + -1 * -1\n" ^
walther@59670
   242
  "4.   [x = 1]\n"
walther@59670
   243
then () else error "re-build: fun locate_input_tactic changed";
wneuper@59562
   244
walther@59670
   245
walther@59670
   246
"----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
walther@59670
   247
"----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
walther@59670
   248
"----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
walther@59670
   249
(*cp from -- try fun applyTactics ------- *)
walther@59670
   250
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
walther@59670
   251
	    "normalform N"],
walther@59670
   252
	   ("PolyMinus",["plus_minus","polynom","vereinfachen"],
walther@59670
   253
	    ["simplification","for_polynomials","with_minus"]))];
walther@59670
   254
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59670
   255
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59670
   256
val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
walther@59670
   257
(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
walther@59670
   258
(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
walther@59670
   259
walther@59686
   260
(*+*)if map tac2str (sel_appl_atomic_tacs pt p) =
walther@59670
   261
   ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
walther@59686
   262
    "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"]
walther@59686
   263
  then () else error "sel_appl_atomic_tacs ([1], Res) CHANGED";
walther@59670
   264
(*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
walther@59670
   265
walther@59686
   266
(*+*)if map tac2str (sel_appl_atomic_tacs pt p) =
walther@59670
   267
   ["Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")", "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \<Longrightarrow> ?a + ?c - ?b = ?a - ?b + ?c\")",
walther@59670
   268
    "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
walther@59686
   269
    "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", "Calculate MINUS"]
walther@59686
   270
  then () else error "sel_appl_atomic_tacs ([1], Res) CHANGED";
walther@59670
   271
(* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
walther@59670
   272
walther@59670
   273
(*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
walther@59670
   274
(** )val ("ok", (_, _, ptp as (pt, p))) =( **) locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
walther@59670
   275
"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (hd (sel_appl_atomic_tacs pt p), (pt, p));
walther@59670
   276
      val (mI, m) = Solve.mk_tac'_ tac;
walther@59670
   277
      val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
walther@59670
   278
      (*if*) member op = Solve.specsteps mI (*else*);
walther@59670
   279
walther@59670
   280
      loc_solve_ (mI, m) ptp;
walther@59670
   281
"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI, m), ptp);
walther@59670
   282
      solve m (pt, pos);
walther@59670
   283
  (* ======== general case ======== *)
walther@59670
   284
"~~~~~ fun solve , args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos));
walther@59670
   285
    (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
walther@59670
   286
	      val thy' = get_obj g_domID pt (par_pblobj pt p);
walther@59670
   287
	      val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
walther@59670
   288
walther@59686
   289
  (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
walther@59692
   290
"~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
walther@59670
   291
  = (sc, (pt, po), (fst is), (snd is), m);
walther@59670
   292
      val srls = Lucin.get_simplifier cstate (*TODO: shift into Istate.T*);
walther@59670
   293
walther@59692
   294
  (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
walther@59692
   295
"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
walther@59692
   296
  = ((prog, (cstate, ctxt, tac)), istate);
walther@59686
   297
    (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
walther@59670
   298
walther@59692
   299
           go_scan_up1 (prog, cctt) ist;
walther@59692
   300
"~~~~~ and go_scan_up1 , args:"; val ((yyy as (prog, _)), (ist as {path, ...}))
walther@59692
   301
  = ((prog, cctt), ist);
walther@59686
   302
  (*if*) 1 < length path (*then*);
walther@59670
   303
walther@59692
   304
           scan_up1 yyy (ist |> path_up) (go (path_up' path) prog);
walther@59691
   305
"~~~~~ fun scan_up1 , args:"; val (yyy, ist, (Const ("Tactical.Try"(*2*), _) $ _))
walther@59692
   306
  = (yyy, (ist |> path_up), (go (path_up' path) prog));
walther@59670
   307
walther@59691
   308
           go_scan_up1 yyy ist;
walther@59692
   309
"~~~~~ and go_scan_up1 , args:"; val ((yyy as (prog, _)), (ist as {path, ...}))
walther@59686
   310
  = (yyy, ist);
walther@59686
   311
  (*if*) 1 < length path (*then*);
walther@59670
   312
walther@59692
   313
           scan_up1 yyy (ist |> path_up) (go (path_up' path) prog);
walther@59692
   314
"~~~~~ fun scan_up1 , args:"; val ((yyy as (prog, xxx as (cstate, _, _))), ist,
walther@59688
   315
    (Const ("Tactical.Chain"(*3*), _) $ _ ))
walther@59692
   316
  = (yyy, (ist |> path_up), (go (path_up' path) prog));
walther@59692
   317
       val e2 = check_Seq_up ist prog
walther@59686
   318
;
walther@59698
   319
  (*case*) scan_dn1 xxx (ist |> path_up_down [R] |> set_or Aundef) e (*of*);
walther@59691
   320
"~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
walther@59698
   321
  = (xxx, (ist |> path_up_down [R] |> set_or Aundef), e2);
walther@59670
   322
walther@59691
   323
  (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e1 (*of*);
walther@59691
   324
"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
walther@59686
   325
  = (xxx, (ist |> path_down [L, R]), e1);
walther@59670
   326
walther@59691
   327
  (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
walther@59686
   328
    (*======= end of scanning tacticals, a leaf =======*)
walther@59709
   329
"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, act_arg, or, ...}), t)
walther@59686
   330
  = (xxx, (ist |> path_down [R]), e);
walther@59686
   331
    val (a', STac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
walther@59686
   332
      val NotAss = (*case*) associate pt ctxt (tac, stac) (*of*);
walther@59686
   333
      val Aundef = (*case*) or (*of*);
walther@59686
   334
  val Notappl "norm_equation not applicable" =    
walther@59686
   335
      (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*);
walther@59670
   336
walther@59712
   337
   (Term_Val1 act_arg) (* return value *);
walther@59670
   338
walther@59670
   339
val Rewrite' ("PolyMinus", "tless_true", _, _, ("tausche_minus",_ (*"?b ist_monom \<Longrightarrow> ?a kleiner ?b \<Longrightarrow> ?b - ?a = - ?a + ?b"*)),
walther@59670
   340
   t, (res, asm)) = m;
walther@59686
   341
walther@59686
   342
if scrstate2str ist =
walther@59686
   343
  "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,L,R,R], e_rls, SOMEt_t, \n" ^
walther@59686
   344
  "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, Aundef, AppUndef_, false)"
walther@59670
   345
andalso
walther@59670
   346
  term2str t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g"
walther@59670
   347
andalso
walther@59670
   348
  term2str res = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f) + 10 * g"
walther@59670
   349
andalso
walther@59670
   350
  terms2str asm = "[\"4 kleiner 6\",\"6 ist_monom\"]"
walther@59670
   351
then () else error "locate_input_tactic Helpless, but applicable CHANGED";
wneuper@59562
   352
walther@59680
   353
wneuper@59564
   354
"----------- re-build: fun determine_next_tactic -----------------------------------------------";
wneuper@59564
   355
"----------- re-build: fun determine_next_tactic -----------------------------------------------";
wneuper@59564
   356
"----------- re-build: fun determine_next_tactic -----------------------------------------------";
wneuper@59575
   357
wneuper@59575
   358
wneuper@59575
   359
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
wneuper@59575
   360
"----------- re-build: fun locate_input_tactic -------------------------------------------------";
wneuper@59575
   361
"----------- re-build: fun locate_input_tactic -------------------------------------------------";