1.1 --- a/src/Tools/isac/TODO.thy	Wed Jul 24 18:22:15 2019 +0200
     1.2 +++ b/src/Tools/isac/TODO.thy	Fri Jul 26 16:34:41 2019 +0200
     1.3 @@ -14,8 +14,8 @@
     1.4  text \<open>
     1.5    \begin{itemize}
     1.6    \item xxx
     1.7 -  \item xxx
     1.8 -  \item xxx
     1.9 +  \item introduce simple type names to LUCAS_INTERPRETER <-?-> readable paper
    1.10 +  \item check in states: length ?? > 1 with tracing these cases
    1.11    \item xxx
    1.12    \item xxx
    1.13    \item xxx

     2.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Wed Jul 24 18:22:15 2019 +0200
     2.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Fri Jul 26 16:34:41 2019 +0200
     2.3 @@ -9,6 +9,7 @@
     2.4  "----------- Take as 1st stac in program -------------------------------------------------------";
     2.5  "----------- re-build: fun locate_input_formula ------------------------------------------------";
     2.6  "----------- re-build: fun determine_next_tactic -----------------------------------------------";
     2.7 +"----------- re-build: fun locate_input_tactic -------------------------------------------------";
     2.8  "-----------------------------------------------------------------------------------------------";
     2.9  "-----------------------------------------------------------------------------------------------";
    2.10  "-----------------------------------------------------------------------------------------------";
    2.11 @@ -44,14 +45,14 @@
    2.12          val PblObj {meth=itms, ...} = get_obj I pt p;
    2.13          val thy' = get_obj g_domID pt p;
    2.14          val thy = assoc_thy thy';
    2.15 -        val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
    2.16 +        val (is as Istate.ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
    2.17          val ini = init_form thy sc env;
    2.18          val p = lev_dn p;
    2.19  ini = NONE; (*true*)
    2.20              val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
    2.21  	            val d = e_rls (*FIXME: get simplifier from domID*);
    2.22  "~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:Tactic.T), ((pt,p):ctree * pos'), 
    2.23 -	                     (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = 
    2.24 +	                     (scr as Prog (h $ body),d), (Istate.ScrState (E,l,a,v,S,b), ctxt)) = 
    2.25                     ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
    2.26  val thy = assoc_thy thy';
    2.27  l = [] orelse ((*init.in solve..Apply_Method...*)
    2.28 @@ -215,3 +216,114 @@
    2.29  "----------- re-build: fun determine_next_tactic -----------------------------------------------";
    2.30  "----------- re-build: fun determine_next_tactic -----------------------------------------------";
    2.31  "----------- re-build: fun determine_next_tactic -----------------------------------------------";
    2.32 +
    2.33 +
    2.34 +"----------- re-build: fun locate_input_tactic -------------------------------------------------";
    2.35 +"----------- re-build: fun locate_input_tactic -------------------------------------------------";
    2.36 +"----------- re-build: fun locate_input_tactic -------------------------------------------------";
    2.37 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    2.38 +val (dI',pI',mI') = ("Test", ["sqroot-test","univariate","equation","test"],
    2.39 +   ["Test","squ-equ-test-subpbl1"]);
    2.40 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    2.41 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    2.42 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    2.43 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    2.44 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    2.45 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    2.46 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    2.47 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
    2.48 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
    2.49 +
    2.50 +(*// relevant call --------------------------------------------------------------------------\\*)
    2.51 +(*[1], Res* )val (*** )xxx( ***) (p,_,f,nxt,_,pt) =*) me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
    2.52 +
    2.53 +"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, [], pt);
    2.54 +
    2.55 +    (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **)  (*case*) locatetac tac (pt,p) (*of*);
    2.56 +"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
    2.57 +      val (mI, m) = Solve.mk_tac'_ tac;
    2.58 +      val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
    2.59 +      (*if*) member op = Solve.specsteps mI; (*else*)
    2.60 +
    2.61 +      (** )val (***)xxxxx(***) ( *Updated (cs' as (_, _, (_, p'))) =( **) loc_solve_ (mI,m) ptp;
    2.62 +"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);
    2.63 +
    2.64 +    (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **) Solve.solve m (pt, pos);
    2.65 +"~~~~~ fun solve , args:"; val ((_, m), (pt, po as (p, p_))) = (m, (pt, pos));
    2.66 +    (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)
    2.67 +	      val thy' = get_obj g_domID pt (par_pblobj pt p);
    2.68 +	      val (_, is, sc) = Lucin.from_pblobj' thy' (p,p_) pt;
    2.69 +
    2.70 +     locate_input_tactic sc (pt, po) (fst is) (snd is) m;
    2.71 +"~~~~~ fun locate_input_tactic , args:"; val (progr, cstate, istate, ctxt, tac)
    2.72 +    = (sc, (pt, po), (fst is), (snd is), m);
    2.73 +      val srls = get_simplifier cstate
    2.74 +      val Assoc ((is as (_,_,_,_,_,strong_ass), ss as((tac', _, ctree, pos', _) :: _))) =
    2.75 +        (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
    2.76 +        (*if*) strong_ass; (*then*)
    2.77 +
    2.78 +    Safe_Step ((ctree, pos'), Istate.ScrState is, get_ctxt ctree pos', tac'); (*return value*)
    2.79 +"~~~~~ from locate_input_tactic to solve return:"; val Safe_Step (cstate, istate, ctxt, tac)
    2.80 +  = (*xxxxx_xx*)(**)Safe_Step ((ctree, pos'), Istate.ScrState is, get_ctxt ctree pos', tac')(**);
    2.81 +
    2.82 +    ([(tac_2tac tac, tac, (snd cstate, (istate, ctxt)))], [(*ctree NOT cut*)], cstate); (*return value*)
    2.83 +"~~~~~ from solve to loc_solve_ return:"; val ((msg, cs' : calcstate'))
    2.84 +   = (*** )xxxxx_x( ***)("ok", ([(Lucin.tac_2tac m, m, (snd cstate, (istate, ctxt)))], [(*ctree NOT cut*)], cstate));
    2.85 +"~~~~~ from loc_solve_ to locatetac return:"; val (Updated (cs' as (_, _, (_, p'))))
    2.86 +   = (*** )xxxxx( ***) (Updated (cs'));
    2.87 +          (*if*) p' = ([], Ctree.Res); (*else*)
    2.88 +          ("ok", cs');
    2.89 +"~~~~~ from locatetac to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
    2.90 +	  val (_, ts) =
    2.91 +	    (case step p ((pt, Ctree.e_pos'), []) of
    2.92 +		    ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
    2.93 +	    | ("helpless", _) => ("helpless: cannot propose tac", [])
    2.94 +	    | ("no-fmz-spec", _) => error "no-fmz-spec"
    2.95 +	    | ("end-of-calculation", (ts, _, _)) => ("", ts)
    2.96 +	    | _ => error "me: uncovered case")
    2.97 +	      handle ERROR msg => raise ERROR msg
    2.98 +	  val tac = 
    2.99 +      case ts of 
   2.100 +        tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end 
   2.101 +		  | _ => if p = ([], Ctree.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
   2.102 +
   2.103 +   (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Istate.Sundef, pt);
   2.104 +"~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
   2.105 +   = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Istate.Sundef, pt);
   2.106 +
   2.107 +(*check results from modified me*)
   2.108 +if p = ([1], Res) andalso
   2.109 +  pr_ctree pr_short pt = ".    ----- pblobj -----\n1.   x + 1 = 2\n"
   2.110 +then
   2.111 +  (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
   2.112 +   | _ => error "")
   2.113 +else error "check results from modified me CHANGED";
   2.114 +
   2.115 +"~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
   2.116 +(*\\------------------ end of modified "fun me" ---------------------------------------------//*)
   2.117 +(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
   2.118 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
   2.119 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*)
   2.120 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
   2.121 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
   2.122 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
   2.123 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
   2.124 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
   2.125 +(*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
   2.126 +(*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
   2.127 +(*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
   2.128 +(*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
   2.129 +(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
   2.130 +(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
   2.131 +(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
   2.132 +(*/--------------------- final test ----------------------------------\\*)
   2.133 +if p = ([], Res) andalso f2str f = "[x = 1]" andalso fst nxt = "End_Proof'"
   2.134 +  andalso pr_ctree pr_short pt =
   2.135 +  ".    ----- pblobj -----\n" ^
   2.136 +  "1.   x + 1 = 2\n" ^
   2.137 +  "2.   x + 1 + -1 * 2 = 0\n" ^
   2.138 +  "3.    ----- pblobj -----\n" ^
   2.139 +  "3.1.   -1 + x = 0\n" ^
   2.140 +  "3.2.   x = 0 + -1 * -1\n" ^
   2.141 +  "4.   [x = 1]\n"
   2.142 +then () else error "re-build: fun locate_input_tactic changed";

     3.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Wed Jul 24 18:22:15 2019 +0200
     3.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Fri Jul 26 16:34:41 2019 +0200
     3.3 @@ -216,11 +216,11 @@
     3.4    ML_file "Knowledge/root.sml"
     3.5    ML_file "Knowledge/lineq.sml"
     3.6  (*ML_file "Knowledge/rooteq.sml"    some complicated equations not recovered from 2002 *)
     3.7 -  ML_file "Knowledge/rateq.sml"   (*some complicated equations not recovered from 2002 *)
     3.8 +(*ML_file "Knowledge/rateq.sml"  ( *some complicated equations not rec.f.2002   Test_Isac_Short*)
     3.9    ML_file "Knowledge/rootrat.sml"
    3.10    ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
    3.11    ML_file "Knowledge/partial_fractions.sml"
    3.12 -  ML_file "Knowledge/polyeq.sml"
    3.13 +(*ML_file "Knowledge/polyeq.sml"                                                 Test_Isac_Short*)
    3.14  (*ML_file "Knowledge/rlang.sml"     much to clean up, similar tests in other files     *)
    3.15    ML_file "Knowledge/calculus.sml"
    3.16    ML_file "Knowledge/trig.sml"

     4.1 --- a/test/Tools/isac/Test_Some.thy	Wed Jul 24 18:22:15 2019 +0200
     4.2 +++ b/test/Tools/isac/Test_Some.thy	Fri Jul 26 16:34:41 2019 +0200
     4.3 @@ -18,7 +18,7 @@
     4.4    open Solve;                  (* NONE *)
     4.5    open Selem;                  e_fmz;
     4.6    open Stool;                  transfer_asms_from_to;
     4.7 -  open Tac;                    (* NONE *)
     4.8 +  open Tactic;                 (* NONE *)
     4.9    open Model;                  (* NONE *)
    4.10    open LTool;                  rule2stac;
    4.11    open Rewrite;                mk_thm;
    4.12 @@ -29,7 +29,7 @@
    4.13    open Tools;                  eval_lhs;
    4.14  (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    4.15  \<close>
    4.16 -ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml" 
    4.17 +ML_file "Interpret/lucas-interpreter.sml" 
    4.18  
    4.19  section \<open>code for copy & paste ===============================================================\<close>
    4.20  ML \<open>