1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Thu Dec 12 10:09:29 2019 +0100
     1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Fri Dec 13 15:56:10 2019 +0100
     1.3 @@ -20,15 +20,13 @@
     1.4    val locate_input_formula : Rule.program -> Ctree.state -> Istate.T -> Proof.context -> term
     1.5      -> input_formula_result
     1.6  (*val begin_end_prog : ???*)
     1.7 -  val begin_end_prog : Tactic.T -> Istate.T * Proof.context -> Ctree.state ->
     1.8 -    (Tactic.input * Tactic.T * (Ctree.pos' * (Istate.T * Proof.context))) list * Ctree.pos' list * Ctree.state
     1.9 +  val begin_end_prog : Tactic.T -> Istate.T * Proof.context -> Ctree.state -> Chead.calcstate'
    1.10  (*val do_solve_step : Ctree.state -> Ctree.state ???*)
    1.11 -  val do_solve_step : Ctree.state ->
    1.12 -    (Tactic.input * Tactic.T * (Ctree.pos' * (Istate.T * Proof.context))) list * Ctree.pos' list * Ctree.state
    1.13 +  val do_solve_step : Ctree.state -> Chead.calcstate'
    1.14  
    1.15    datatype next_tactic_result =
    1.16        Next_Step of Istate.T * Proof.context * Tactic.T
    1.17 -    | Helpless | End_Program
    1.18 +    | Helpless | End_Program (*of Istate.T * Tactic.T*)
    1.19    val determine_next_tactic: Rule.program -> Ctree.state -> Istate.T -> Proof.context
    1.20      -> Tactic.T * (Istate.T * Proof.context) * (term * Telem.safe)
    1.21  
    1.22 @@ -198,11 +196,11 @@
    1.23      if Tactical.contained_in t then raise TERM ("scan_dn1 expects Prog_Tac or Prog_Expr", [t])
    1.24      else
    1.25        case Lucin.interpret_leaf "locate" ctxt eval (get_subst ist) t of
    1.26 -  	     (Program.Expr _, form_arg) => 
    1.27 -  	       Term_Val1 (Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) eval
    1.28 -  		       (subst_atomic (Env.update_opt'' (get_act_env ist, form_arg)) t))
    1.29 -       | (Program.Tac prog_tac, form_arg) =>
    1.30 -           interpret_tac1 cct ist (form_arg, prog_tac)
    1.31 +  	    (Program.Expr _, form_arg) => 
    1.32 +  	      Term_Val1 (Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) eval
    1.33 +  		      (subst_atomic (Env.update_opt'' (get_act_env ist, form_arg)) t))
    1.34 +      | (Program.Tac prog_tac, form_arg) =>
    1.35 +          interpret_tac1 cct ist (form_arg, prog_tac)
    1.36  
    1.37  fun go_scan_up1 (pcct as (prog, _)) (ist as {path, act_arg, ...}) =
    1.38      if 1 < length path
    1.39 @@ -469,6 +467,7 @@
    1.40  
    1.41    | scan_up2 _ _ t = error ("scan_up2 not impl for " ^ Rule.term2str t)
    1.42  
    1.43 +(* scan program until an applicable tactic is found *)
    1.44  fun scan_to_tactic2 (prog, cc) (Istate.Pstate (ist as {path, ...})) =
    1.45    if path = []
    1.46    then scan_dn2 cc (trans_scan_down2 ist) (Program.body_of prog)
    1.47 @@ -592,14 +591,14 @@
    1.48    | begin_end_prog tac_ is (pt, pos) =
    1.49      let
    1.50        val pos = case pos of
    1.51 - 		   (p, Met) => ((lev_on o lev_dn) p, Frm) (* begin script        *)
    1.52 - 		  | (p, Res) => (lev_on p, Res)            (* somewhere in script *)
    1.53 + 		   (p, Met) => ((lev_on o lev_dn) p, Frm) (* begin program        *)
    1.54 + 		  | (p, Res) => (lev_on p, Res)           (* somewhere in program *)
    1.55   		  | _ => pos
    1.56   	    val (pos', c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac_ is pos pt;
    1.57      in
    1.58        ([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos'))
    1.59      end
    1.60 -(*find the next tac from the script, begin_end_prog will update the ctree*)
    1.61 +(*determine_next_tactic from program, begin_end_prog will update the ctree*)
    1.62  and do_solve_step (ptp as (pt, pos as (p, p_))) = (* WN1907: ?only for Begin_/End_Detail' DEL!!!*)
    1.63      if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)
    1.64      then ([], [], (pt, (p, p_)))

     2.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml	Thu Dec 12 10:09:29 2019 +0100
     2.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml	Fri Dec 13 15:56:10 2019 +0100
     2.3 @@ -216,7 +216,7 @@
     2.4                        else (LucinNEW.do_solve_step (pt, ip))
     2.5    	                    handle ERROR msg => (writeln ("*** " ^ msg);
     2.6    	                      ([],[],ptp)) (*e.g. Add_Given "equality///"*) of
     2.7 -  	               cs as ([],_,_) =>("helpless", cs) (*FIXXME del.handle*)
     2.8 +  	               cs as ([], _, _) => ("helpless", cs) (*FIXXME del.handle*)
     2.9    		           | cs => ("ok", cs)))
    2.10    end
    2.11  

     3.1 --- a/src/Tools/isac/TODO.thy	Thu Dec 12 10:09:29 2019 +0100
     3.2 +++ b/src/Tools/isac/TODO.thy	Fri Dec 13 15:56:10 2019 +0100
     3.3 @@ -76,12 +76,35 @@
     3.4  text \<open>
     3.5    \begin{itemize}
     3.6    \item xxx
     3.7 -  \item improve naming? shift show_pt, pr_ctree --> Ctree: REQUIRES Chead.pt_mdel etc.
     3.8 +  \item decompose do_solve_step, begin_end_prog: mutual recursion only avoids multiple generate1
     3.9 +    ! ^^^ in determine_next_tactic --- ? ? ? in locate_input_tactic ?
    3.10 +  \item xxx
    3.11 +  \item Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec
    3.12 +  \item xxx
    3.13 +  \item NEW structure Step.applicable     Step.add
    3.14 +                          ^applicable_in      ^generate1
    3.15 +  \item xxx
    3.16    \item revise Pstate {or, ...}; strange occurrence in program without Tactical.Or documented here
    3.17    \item xxx
    3.18    \item shift tests into NEW model.sml (upd, upds_envv, ..)
    3.19    \item xxx
    3.20 -  \item xxx
    3.21 +  \item NEW structures
    3.22 +    \begin{itemize}
    3.23 +    \item Step
    3.24 +      \begin{itemize}
    3.25 +      \item Applicable.applicable_in --> Step.applicable
    3.26 +      \item Generate.generate1       --> Step.add        ?-->? Calculation.add_step 
    3.27 +      \item xxx
    3.28 +      \end{itemize}
    3.29 +    \item Calculation ("Calc" is occupied ?!?)           ?^^^? Calculation
    3.30 +      \begin{itemize}
    3.31 +      \item Ctree.state ?-->? Calculation.T
    3.32 +      \item Chead.calcstate   --> Calculation.prestate
    3.33 +      \item Chead.calcstate'  --> Calculation.poststate
    3.34 +      \item e_calcstate, e_calcstate' -"-
    3.35 +      \item xxx
    3.36 +      \end{itemize}
    3.37 +    \end{itemize}
    3.38    \item xxx
    3.39    \item clarify handling of contexts
    3.40      \begin{itemize}
    3.41 @@ -168,7 +191,8 @@
    3.42      \item 
    3.43      \item xxx
    3.44      \end{itemize}
    3.45 -  \item concentrate "insert_assumptions" in "associate" ?for determine_next_tactic ?where?
    3.46 +  \item concentrate "insert_assumptions" for locate_input_tactic in "associate", ?OR? Tactic.insert_assumptions
    3.47 +                                   DONE  for determine_next_tactic by Tactic.insert_assumptions m' ctxt 
    3.48      \begin{itemize}
    3.49      \item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?)
    3.50      \item shift from "applicable_in..Apply_Method" to ? ? ? (is ONLY use-case in appl.sml))

     4.1 --- a/test/Tools/isac/Test_Some.thy	Thu Dec 12 10:09:29 2019 +0100
     4.2 +++ b/test/Tools/isac/Test_Some.thy	Fri Dec 13 15:56:10 2019 +0100
     4.3 @@ -46,7 +46,7 @@
     4.4  "~~~~~ fun xxx , args:"; val () = ();
     4.5  "~~~~~ and xxx , args:"; val () = ();
     4.6  "~~~~~ from fun xxx\<longrightarrow>fun yyy\<longrightarrow>fun zzz, return:"; val () = ();
     4.7 -(*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*);
     4.8 +(*if*) (*then*); (*else*);   (*case*) (*of*);  (*return from xxx*);
     4.9  "xx"
    4.10  ^ "xxx"   (*+*) (*!for return!*) (*isa*) (*REP*)
    4.11  \<close> ML \<open>
    4.12 @@ -123,7 +123,7 @@
    4.13    	                    andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*else*);
    4.14  
    4.15  \<close> ML \<open>
    4.16 -  val cs''''' = (*..interpret "if member op ="..*)
    4.17 +(**)val cs''''' = (*..interpret "if member op ="..*)
    4.18    (*case*) do_solve_step (pt, ip) (*of*);
    4.19  \<close> ML \<open>
    4.20  "~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
    4.21 @@ -131,43 +131,73 @@
    4.22          val thy' = get_obj g_domID pt (par_pblobj pt p);
    4.23  	      val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
    4.24  \<close> ML \<open>
    4.25 -        val ptp'''''_' = ptp
    4.26 +        val ptp'''''_' = ptp (*1*)
    4.27  	      val (tac_'''''_', is'''''_', (t'''''_', _)) = determine_next_tactic sc (pt, pos) ist ctxt;
    4.28  \<close> ML \<open>
    4.29 -"~~~~~ fun determine_next_tactic , args:"; val (Rule.Prog prog, ptp as(pt, (p, _)), Istate.Pstate ist, ctxt)
    4.30 +"~~~~~ fun determine_next_tactic , args:"; val (Rule.Prog prog, ptp as (pt, (p, _)), Istate.Pstate ist, ctxt)
    4.31    = (sc, (pt, pos), ist, ctxt);
    4.32  \<close> ML \<open>
    4.33  (*OLD*)val Accept_Tac2 (m', ist as {act_arg, ...}, ctxt) =
    4.34  (*OLD*)  (*case*) scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
    4.35 -(*NEW*)
    4.36 -(*NEW*)
    4.37 +(*NEW* )
    4.38 +(*NEW*)  Accept_Tac2 (m', ist, ctxt) => Next_Step (ist, Tactic.insert_assumptions m'  ctxt, m')
    4.39 +(*NEW*)| Term_Val2 prog_result => End_Program (ist, Check_Postcond' ...prog_result...)
    4.40 +(*NEW*)    (* ist indicates ^^\<Or>?, ctxt already updated, ^^^*)
    4.41 +(*NEW*)| Reject_Tac2 => Helpless
    4.42 +( *NEW*)
    4.43  \<close> ML \<open>
    4.44 -(*OLD   Tactic.T * (Istate.T  * Proof.context) * (term   * Telem.safe) OLD*)
    4.45  (*OLD*)(m',        (Pstate ist, ctxt),           (act_arg, Telem.Safe))  (*return value*);
    4.46 -(*NEW*)
    4.47 -(*NEW*)
    4.48 +(*OLD*)
    4.49 +(*NEW* ) Next_Step (ist, Tactic.insert_assumptions m'  ctxt, m')  (*return value*);
    4.50 +( *NEW*)
    4.51  \<close> ML \<open>
    4.52  "~~~~~ from fun determine_next_tactic\<longrightarrow>and do_solve_step , return:"; val (tac_, is, (t, _))
    4.53    = (m', (Pstate ist, ctxt), (act_arg, Telem.Safe));
    4.54  \<close> ML \<open>
    4.55 +(*NEW* ) Next_Step (ist, Tactic.insert_assumptions m'  ctxt, m')
    4.56 +( *NEW*)
    4.57 +(*NEW* ) case  determine_next_tactic sc (pt, pos) ist ctxt of
    4.58 +(*NEW*)    Next_Step (ist, ctxt, tac) => begin_end_prog tac (ist, ctxt) ptp
    4.59 +(*NEW*)      (*^^^vvv here was case tac_ of End_Detail' _ => ..special handling *)
    4.60 +(*NEW*)  | End_Program (ist, tac) => begin_end_prog tac (ist, ctxt) ptp
    4.61 +(*NEW*)  | Helpless => Chead.e_calcstate'
    4.62 +( *NEW*)
    4.63 +\<close> ML \<open>
    4.64  (*+*)val Rewrite_Set' ("Test", false, Rls {id = "Test_simplify", ...}, _, _) =
    4.65  (*+*)  m'
    4.66  \<close> ML \<open>
    4.67 -(*OLD*)  val _ = (*case*) tac_'''''_' (*of*);
    4.68 -(*OLD*)begin_end_prog tac_'''''_' is'''''_' ptp'''''_'  (*return value*);
    4.69 -(*NEW*)
    4.70 -(*NEW*)                                                                                                                                
    4.71 +(*OLD skip* )  val _ = (*case*) tac_'''''_' (*of*);
    4.72 +(*OLD skip*)begin_end_prog tac_'''''_' is'''''_' ptp'''''_'  (*return value*);
    4.73 +( *OLD*)
    4.74 +(*use*)  val _ = (*case*) tac_ (*of*);
    4.75 +(*use*)begin_end_prog tac_ is ptp (*return value*);
    4.76 +(*use*)
    4.77  \<close> ML \<open>
    4.78 -"~~~~~ from and do_solve_step\<longrightarrow>fun step , return:"; val (tac_'''''_')
    4.79 -  = (begin_end_prog tac_'''''_' is ptp);
    4.80 +"~~~~~ fun begin_end_prog , args:"; val (tac_, is, (pt, pos))
    4.81 +(*skip*)= (tac_'''''_', is, ptp);(*skip*)
    4.82 +(*use* )( *use*)
    4.83  \<close> ML \<open>
    4.84 -(*/---------------------- check results from modified "fun step" -----------------------------\*)
    4.85 +      val pos = case pos of
    4.86 + 		   (p, Met) => ((lev_on o lev_dn) p, Frm) (* begin script        *)
    4.87 + 		  | (p, Res) => (lev_on p, Res)           (* somewhere in script *)
    4.88 + 		  | _ => pos
    4.89  \<close> ML \<open>
    4.90 + 	    val (pos', c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac_ is pos pt;
    4.91  \<close> ML \<open>
    4.92 -(*\---------------------- check results from modified "fun step" -----------------------------/*)
    4.93 +      ([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos')) (*return from do_solve_step*);
    4.94  \<close> ML \<open>
    4.95 -"~~~~~ from fun step\<longrightarrow>TOPLEVEL return:"; val (_, ([(tac'''', _, _)], _, (pt'''', p'''')))
    4.96 -  = (*** )xxx( ***) (**)("ok", cs''''')(**);
    4.97 +"~~~~~ from and do_solve_step\<longrightarrow>fun step , return:"; 
    4.98 +(*OLD skip* )val (tac_'''''_')
    4.99 +(*OLD skip*)  = (begin_end_prog tac_'''''_' is ptp);( **)
   4.100 +(*use*)val cs =
   4.101 +(*use*)([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos'))
   4.102 +(*use*)
   4.103 +\<close> ML \<open>
   4.104 +"~~~~~ from fun step\<longrightarrow>TOPLEVEL return:";
   4.105 +(*OLD skip* )val (_, ([(tac'''', _, _)], _, (pt'''', p'''')))  = ("ok", cs''''')( **);
   4.106 +(*OLD skip*)
   4.107 +(*use*)val ([(tac, _, (_, _))], _, (pt'''', p'''')) = cs
   4.108 +(*use*)
   4.109  \<close> ML \<open>
   4.110  (*\\------------------ end of modified "fun step" -------------------------------------------//*)
   4.111  \<close> ML \<open>
   4.112 @@ -187,14 +217,14 @@
   4.113  (*/--------------------- final test ----------------------------------\\*)
   4.114  val (res, asm) = (get_obj g_result pt (fst p));
   4.115  
   4.116 -\<close> ML \<open>
   4.117 +\<close> ML \<open> (*--- final test ---*)
   4.118  if term2str res = "[x = 1]" andalso terms2str asm = "[\"precond_rootmet 1\"]"
   4.119  then () else error "re-build: fun determine_next_tactic CHANGED 1";
   4.120  
   4.121 -if p = ([], Und)
   4.122 +if p = ([], Und)  (*.. should be ([], Res) *)
   4.123  then
   4.124    case get_obj g_tac pt (fst p) of
   4.125 -    Apply_Method ["Test", "squ-equ-test-subpbl1"] => ()
   4.126 +    Apply_Method ["Test", "squ-equ-test-subpbl1"] => ((*ok, further tactics are level down*))
   4.127    | _ => error "re-build: fun determine_next_tactic CHANGED 3"
   4.128  else error "re-build: fun determine_next_tactic CHANGED 2";
   4.129  \<close> ML \<open>