1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Wed Jul 03 15:30:31 2019 +0200
     1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Wed Jul 03 17:17:55 2019 +0200
     1.3 @@ -5,20 +5,32 @@
     1.4  
     1.5  signature LUCAS_INTERPRETER =
     1.6  sig
     1.7 +(*datatype next_tactic_result = NStep of Ctree.state * Selem.istate * Proof.context * tactic
     1.8 +    | NHelpless | End_Program *)
     1.9 +(*val determine_next_tactic :
    1.10 +    Rule.program -> Ctree.state -> Selem.istate -> Proof.context -> next_tactic_result *)
    1.11    val determine_next_tactic : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Selem.istate * 'a ->
    1.12      Tac.tac_ * (Selem.istate * 'a) * (term * Selem.safe)
    1.13  
    1.14 +(*datatype input_tactic_result = TStep of Ctree.state * Selem.istate * Proof.context
    1.15 +    | THelpless *)
    1.16    datatype locate = Steps of Selem.istate * Lucin.step list | NotLocatable
    1.17 +(*val locate_input_tactic :
    1.18 +    Rule.program -> Ctree.state -> Selem.istate -> Proof.context -> tactic -> input_formula_result*)
    1.19    val locate_input_tactic : Rule.theory' * Rule.rls -> Tac.tac_ -> Ctree.state -> Rule.program * 'a ->
    1.20      Selem.istate * Proof.context -> locate
    1.21  
    1.22 +(*datatype input_formula_result = FStep of calcstate' | Not_Derivable *)
    1.23    datatype input_formula_result =
    1.24      Step of Ctree.state * Selem.istate * Proof.context
    1.25    | Not_Derivable of Chead.calcstate'
    1.26 +(*val locate_input_formula : calcstate -> term -> input_formula_result *)
    1.27    val locate_input_formula : Rule.program -> Ctree.state -> Selem.istate -> Proof.context -> term
    1.28      -> input_formula_result
    1.29 +(*val do_solve_step : calcstate -> calcstate' ???*)
    1.30    val do_solve_step : Ctree.state ->
    1.31      (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * Ctree.pos' list * Ctree.state
    1.32 +(*val begin_end_prog : ???*)
    1.33    val begin_end_prog : Tac.tac_ -> Selem.istate * Proof.context -> Ctree.state ->
    1.34      (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * Ctree.pos' list * Ctree.state
    1.35  
    1.36 @@ -244,19 +256,19 @@
    1.37        (Selem.RrlsState(f, f', rss, _), ctxt) =
    1.38      if f = f'
    1.39      then (Tac.End_Detail' (f',[])(*8.6.03*), (Selem.Uistate, ctxt), 
    1.40 -    	(f', Selem.Sundef(*FIXME is no value of determine_next_tactic! vor 8.6.03*)))        (*finished*)
    1.41 +    	(f', Selem.Sundef(*FIXME is no value of determine_next_tactic! vor 8.6.03*)))    (*finished*)
    1.42      else
    1.43        (case next_rule rss f of
    1.44 -    	  NONE => (Tac.Empty_Tac_, (Selem.Uistate, ctxt), (Rule.e_term, Selem.Sundef))       (*helpless*)
    1.45 +    	  NONE => (Tac.Empty_Tac_, (Selem.Uistate, ctxt), (Rule.e_term, Selem.Sundef))   (*helpless*)
    1.46      	| SOME (Rule.Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) => 
    1.47      	    (Tac.Rewrite' (thy, "e_rew_ord", Rule.e_rls, false, thm'', f, (Rule.e_term, [(*!?!8.6.03*)])),
    1.48 -  	         (Selem.Uistate, ctxt), (Rule.e_term, Selem.Sundef))                          (*next stac*)
    1.49 +  	         (Selem.Uistate, ctxt), (Rule.e_term, Selem.Sundef))                      (*next stac*)
    1.50        | _ => error "determine_next_tactic: uncovered case next_rule")
    1.51    | determine_next_tactic thy (ptp as (pt, (p, _))) (sc as Rule.Prog prog) 
    1.52  	    (Selem.ScrState (E,l,a,v,s,_), ctxt) =
    1.53      (case if l = [] then appy thy ptp E [Celem.R] (LTool.body_of prog) NONE v
    1.54            else nstep_up thy ptp sc E l Skip_ a v of
    1.55 -       Skip (v, _) =>                                                                 (*finished*)
    1.56 +       Skip (v, _) =>                                                                  (*finished*)
    1.57           (case par_pbl_det pt p of
    1.58  	          (true, p', _) => 
    1.59  	             let
    1.60 @@ -519,7 +531,7 @@
    1.61            NOT IMPL. -- "error: do other step before"
    1.62     NotLocatable: thus generate_hard
    1.63  *)
    1.64 -fun locate_input_tactic (thy', _) (Tac.Rewrite' (_, ro, er, pa, thm, f, _)) (pt, p) (*TODO-LucinNEW del in script.sml*)
    1.65 +fun locate_input_tactic (thy', _) (Tac.Rewrite' (_, ro, er, pa, thm, f, _)) (pt, p)
    1.66  	    (Rule.Rfuns {locate_rule=lo,...}, _) (Selem.RrlsState (_,f'',rss,rts), _) = 
    1.67      (case lo rss f (Rule.Thm thm) of
    1.68  	    [] => NotLocatable

     2.1 --- a/src/Tools/isac/TODO.thy	Wed Jul 03 15:30:31 2019 +0200
     2.2 +++ b/src/Tools/isac/TODO.thy	Wed Jul 03 17:17:55 2019 +0200
     2.3 @@ -29,9 +29,12 @@
     2.4    \item language definition: use (f #> g) x = x |> f |> g instead of @
     2.5      see implementation.pdf p.16
     2.6    \item xxx
     2.7 -  \item xxx
     2.8 -  \item xxx
     2.9 -  \item rename type scr --> type program   + rename field scr in meth
    2.10 +  \item shift replaceFormula, appendFormula test/../inform.sml --> solve.sml
    2.11 +  \item for determine_next_tactic, locate_input_tactic adopt signature from ..
    2.12 +    locate_input_formula: program -> state -> istate -> Proof.context -> term -> input_formula_result;
    2.13 +  \item switch signature of locate_input_formula (back) to calcstate',  cf.
    2.14 +      + change signature of do_solve_step, begin_end_prog accordingly
    2.15 +  \item rename rename field scr in meth
    2.16    \item inform:
    2.17      TermC.parse (Celem.assoc_thy "Isac") istr --> parseNEW context istr
    2.18    \item lucin: test/../partial_fractions: repair different behaviour of

     3.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Wed Jul 03 15:30:31 2019 +0200
     3.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Wed Jul 03 17:17:55 2019 +0200
     3.3 @@ -7,7 +7,8 @@
     3.4  "table of contents -----------------------------------------------------------------------------";
     3.5  "-----------------------------------------------------------------------------------------------";
     3.6  "----------- Take as 1st stac in program -------------------------------------------------------";
     3.7 -"----------- build: fun locate_input_formula ---------------------------------------------------";
     3.8 +"----------- re-build: fun locate_input_formula ------------------------------------------------";
     3.9 +"----------- re-build: fun determine_next_tactic -----------------------------------------------";
    3.10  "-----------------------------------------------------------------------------------------------";
    3.11  "-----------------------------------------------------------------------------------------------";
    3.12  "-----------------------------------------------------------------------------------------------";
    3.13 @@ -67,9 +68,9 @@
    3.14  (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*)
    3.15  
    3.16  
    3.17 -"----------- build: fun locate_input_formula ---------------------------------------------------";
    3.18 -"----------- build: fun locate_input_formula ---------------------------------------------------";
    3.19 -"----------- build: fun locate_input_formula ---------------------------------------------------";
    3.20 +"----------- re-build: fun locate_input_formula ------------------------------------------------";
    3.21 +"----------- re-build: fun locate_input_formula ------------------------------------------------";
    3.22 +"----------- re-build: fun locate_input_formula ------------------------------------------------";
    3.23  (*co from ---input.sml: ------ appendFormula: on Res + late deriv ----*)
    3.24  val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    3.25  val (dI',pI',mI') =
    3.26 @@ -211,3 +212,6 @@
    3.27  ([], Res), [x = 1]] 
    3.28  val it = (): unit*)
    3.29  
    3.30 +"----------- re-build: fun determine_next_tactic -----------------------------------------------";
    3.31 +"----------- re-build: fun determine_next_tactic -----------------------------------------------";
    3.32 +"----------- re-build: fun determine_next_tactic -----------------------------------------------";

     4.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Wed Jul 03 15:30:31 2019 +0200
     4.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml	Wed Jul 03 17:17:55 2019 +0200
     4.3 @@ -3,9 +3,9 @@
     4.4     (c) copyright due to lincense terms.
     4.5  *)
     4.6  
     4.7 -"----------- Minisubplb/250-Rewrite_Set-from-method.sml ----------";
     4.8 -"----------- Minisubplb/250-Rewrite_Set-from-method.sml ----------";
     4.9 -"----------- Minisubplb/250-Rewrite_Set-from-method.sml ----------";
    4.10 +"----------- Minisubpbl/250-Rewrite_Set-from-method.sml ----------";
    4.11 +"----------- Minisubpbl/250-Rewrite_Set-from-method.sml ----------";
    4.12 +"----------- Minisubpbl/250-Rewrite_Set-from-method.sml ----------";
    4.13  val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    4.14  val (dI',pI',mI') =
    4.15    ("Test", ["sqroot-test","univariate","equation","test"],

     5.1 --- a/test/Tools/isac/Test_Some.thy	Wed Jul 03 15:30:31 2019 +0200
     5.2 +++ b/test/Tools/isac/Test_Some.thy	Wed Jul 03 17:17:55 2019 +0200
     5.3 @@ -6,7 +6,8 @@
     5.4                           in case of errors here consider ~~/./xtest-to-coding.sh      *)
     5.5    open Kernel;
     5.6    open Math_Engine;            CalcTreeTEST;
     5.7 -  open Lucin;                  appy;
     5.8 +  open Lucin;                  itms2args;
     5.9 +  open LucinNEW;               appy;
    5.10    open Inform;                 cas_input;
    5.11    open Rtools;                 trtas2str;
    5.12    open Chead;                  pt_extract;