# HG changeset patch # User Walther Neuper # Date 1561459704 -7200 # Node ID f25ce1922b607e95a97177a183047a13cbd22b3a # Parent 0422e662c30400e0eb9c35c5e905b04bfdd800da lucin: rename 3 main functions of lucase-interpreter.sml diff -r 0422e662c304 -r f25ce1922b60 src/Tools/isac/Frontend/interface.sml --- a/src/Tools/isac/Frontend/interface.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/src/Tools/isac/Frontend/interface.sml Tue Jun 25 12:48:24 2019 +0200 @@ -443,7 +443,7 @@ in case Math_Engine.step pos cs of ("ok", cs') => - (case LucinNEW.inform cs' (encode ifo) of + (case LucinNEW.locate_input_formula cs' (encode ifo) of ("ok", (_(*use in DG !!!*), c, ptp as (_, p))) => (upd_calc cI (ptp, []); upd_ipos cI 1 p; appendformulaOK2xml cI pos (if null c then pos else last_elem c) p) @@ -463,7 +463,7 @@ val ((pt, _), _) = get_calc cI val p = get_pos cI 1 in - case LucinNEW.inform (([], [], (pt, p)): Chead.calcstate') (encode ifo) of + case LucinNEW.locate_input_formula (([], [], (pt, p)): Chead.calcstate') (encode ifo) of ("ok", (_(*tacs used for DG ?*), c, ptp' as (_, p'))) => let val unc = if null (fst p) then p else move_up [] pt p diff -r 0422e662c304 -r f25ce1922b60 src/Tools/isac/Interpret/appl.sml --- a/src/Tools/isac/Interpret/appl.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/src/Tools/isac/Interpret/appl.sml Tue Jun 25 12:48:24 2019 +0200 @@ -116,7 +116,7 @@ in ((scan []) o Symbol.explode) str end; (* applicability of a tacic wrt. a calc-state (ctree,pos'). - additionally used by next_tac in the script-interpreter for script-tacs. + additionally used by determine_next_tactic. tests for applicability are so expensive, that results (rewrites!) are kept in the return-value of 'type tac_' *) fun applicable_in _ _ (Tac.Init_Proof (ct', spec)) = Chead.Appl (Tac.Init_Proof' (ct', spec)) @@ -425,7 +425,7 @@ end | applicable_in _ _ (Tac.Apply_Assumption cts') = error ("applicable_in: not impl. for " ^ Tac.tac2str (Tac.Apply_Assumption cts')) - (* 'logical' applicability wrt. script in locate: Inconsistent? *) + (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *) | applicable_in _ _ (Tac.Take_Inst ct') = error ("applicable_in: not impl. for " ^ Tac.tac2str (Tac.Take_Inst ct')) | applicable_in (p, p_) pt (m as Tac.Subproblem (domID, pblID)) = diff -r 0422e662c304 -r f25ce1922b60 src/Tools/isac/Interpret/ctree-basic.sml --- a/src/Tools/isac/Interpret/ctree-basic.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/src/Tools/isac/Interpret/ctree-basic.sml Tue Jun 25 12:48:24 2019 +0200 @@ -192,7 +192,7 @@ # generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn exceptions: Begin/End_Trans # thus generate(1) called in -.# assy, locate_gen +.# assy, locate_input_tactic .# nxt_solv (tac_ -cases); general case: val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos' # WN050220, S(604): diff -r 0422e662c304 -r f25ce1922b60 src/Tools/isac/Interpret/ctree-navi.sml --- a/src/Tools/isac/Interpret/ctree-navi.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/src/Tools/isac/Interpret/ctree-navi.sml Tue Jun 25 12:48:24 2019 +0200 @@ -49,7 +49,7 @@ fun lev_up [] = raise PTREE "lev_up []" | lev_up p = (drop_last p):pos; -(*040216: for inform --> embed_deriv: remains on same level TODO.WN120517 compare lev_pred*) +(*040216: for locate_input_formula --> embed_deriv: remains on same level TODO.WN120517 compare lev_pred*) fun lev_back' ([], _) = raise PTREE "lev_back': called by ([],_)" | lev_back' (p, _) = if last_elem p <= 1 then (p, Frm) diff -r 0422e662c304 -r f25ce1922b60 src/Tools/isac/Interpret/inform.sml --- a/src/Tools/isac/Interpret/inform.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/src/Tools/isac/Interpret/inform.sml Tue Jun 25 12:48:24 2019 +0200 @@ -438,7 +438,7 @@ | _ => error "find_fillpatterns: uncovered case of get_met" val env = case Ctree.get_istate pt pos of Selem.ScrState (env, _, _, _, _, _) => env - | _ => error "inform: uncovered case of get_istate" + | _ => error "locate_input_formula: uncovered case of get_istate" val subst = Rtools.get_bdv_subst prog env val errpatthms = errpats |> filter ((curry op = errpatID) o (#1: Rule.errpat -> Rule.errpatID)) diff -r 0422e662c304 -r f25ce1922b60 src/Tools/isac/Interpret/lucas-interpreter.sml --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Jun 25 12:48:24 2019 +0200 @@ -5,16 +5,18 @@ signature LUCAS_INTERPRETER = sig - val next_tac : Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> Selem.istate * 'a -> Tac.tac_ * (Selem.istate * 'a) * (term * Selem.safe) + val determine_next_tactic : Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> Selem.istate * 'a -> + Tac.tac_ * (Selem.istate * 'a) * (term * Selem.safe) datatype locate = Steps of Selem.istate * Lucin.step list | NotLocatable - val locate_gen : Rule.theory' * Rule.rls -> Tac.tac_ -> Ctree.state -> Rule.scr * 'a -> Selem.istate * Proof.context -> locate + val locate_input_tactic : Rule.theory' * Rule.rls -> Tac.tac_ -> Ctree.state -> Rule.scr * 'a -> + Selem.istate * Proof.context -> locate - val inform : Chead.calcstate' -> string -> string * Chead.calcstate' - val nxt_solv : Tac.tac_ -> Selem.istate * Proof.context -> Ctree.ctree * (Ctree.pos') -> (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * Ctree.pos' list * (Ctree.ctree * Ctree.pos') - val nxt_solve_ : Ctree.ctree * Ctree.pos' -> - (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * - Ctree.pos' list * Ctree.state + val locate_input_formula : Chead.calcstate' -> string -> string (*..drop*)* Chead.calcstate' + val nxt_solv : Tac.tac_ -> Selem.istate * Proof.context -> Ctree.state -> + (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * Ctree.pos' list * Ctree.state + val nxt_solve_ : Ctree.state -> + (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * Ctree.pos' list * Ctree.state (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) type assoc @@ -49,7 +51,7 @@ (** find the next tactic by executing the program **) -(*appy, nxt_up, nstep_up scanning for next_tac. +(*appy, nxt_up, nstep_up scanning for determine_next_tactic. search is clearly separated into (1)-(2): (1) appy is recursive descent; (2) nxt_up resumes interpretation at a location somewhere in the script; @@ -233,18 +235,18 @@ (.. not true for other details ..PrfObj ?????????????????? 20.8.02: do NOT return safe (is only changed in locate !!!) *) -fun next_tac (thy,_) _ (Rule.Rfuns {next_rule, ...}) (Selem.RrlsState(f, f', rss, _), ctxt) = +fun determine_next_tactic (thy,_) _ (Rule.Rfuns {next_rule, ...}) (Selem.RrlsState(f, f', rss, _), ctxt) = if f = f' then (Tac.End_Detail' (f',[])(*8.6.03*), (Selem.Uistate, ctxt), - (f', Selem.Sundef(*FIXME is no value of next_tac! vor 8.6.03*))) (*finished*) + (f', Selem.Sundef(*FIXME is no value of determine_next_tactic! vor 8.6.03*))) (*finished*) else (case next_rule rss f of NONE => (Tac.Empty_Tac_, (Selem.Uistate, ctxt), (Rule.e_term, Selem.Sundef)) (*helpless*) | SOME (Rule.Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) => (Tac.Rewrite' (thy, "e_rew_ord", Rule.e_rls, false, thm'', f, (Rule.e_term, [(*!?!8.6.03*)])), (Selem.Uistate, ctxt), (Rule.e_term, Selem.Sundef)) (*next stac*) - | _ => error "next_tac: uncovered case next_rule") - | next_tac thy (ptp as (pt, (p, _))) (sc as Rule.Prog prog) + | _ => error "determine_next_tactic: uncovered case next_rule") + | determine_next_tactic thy (ptp as (pt, (p, _))) (sc as Rule.Prog prog) (Selem.ScrState (E,l,a,v,s,_), ctxt) = (case if l = [] then appy thy ptp E [Celem.R] (LTool.body_of prog) NONE v else nstep_up thy ptp sc E l Skip_ a v of @@ -260,13 +262,13 @@ | Napp _ => (Tac.Empty_Tac_, (Selem.e_istate, ctxt), (Rule.e_term, Selem.Sundef)) (*helpless*) | Appy (m', scrst as (_,_,_,v,_,_)) => (m', (Selem.ScrState scrst, ctxt), (v, Selem.Sundef))) (*next stac*) - | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (Selem.istate2str is)); + | determine_next_tactic _ _ _ (is, _) = error ("determine_next_tactic: not impl for " ^ (Selem.istate2str is)); (** locate an input tactic in the program **) datatype assoc = (* ExprVal in the sense of denotational semantics *) Assoc of (* the stac is associated, strongly or weakly *) - Selem.scrstate * (* the current; returned for next_tac etc. outside ass* *) + Selem.scrstate * (* the current; returned for determine_next_tactic etc. outside ass* *) (Lucin.step list) (* list of steps done until associated stac found; initiated with the data for doing the 1st step, thus the head holds these data further on, @@ -289,7 +291,7 @@ search for _applicable_ stacs, execute and generate pt *) (*this constructions doesnt allow arbitrary nesting of Or !!! *) -(* assy, ass_up, astep_up scan for locate_gen in a script. +(* assy, ass_up, astep_up scan for locate_input_tactic in a script. search is clearly separated into (1)-(2): (1) assy is recursive descent; (2) ass_up resumes interpretation at a location somewhere in the script; @@ -484,12 +486,12 @@ datatype locate = Steps of Selem.istate (* producing hd of step list (which was latest) - for next_tac, for reporting Safe|Unsafe to DG *) + for determine_next_tactic, for reporting Safe|Unsafe to DG *) * Lucin.step (* (scrstate producing this step is in ctree !) *) - list (* locate_gen may produce intermediate steps *) + list (* locate_input_tactic may produce intermediate steps *) | NotLocatable; (* no (m Ass m') or (m AssWeak m') found *) -(* locate_gen tries to locate an input tac m in the script. +(* locate_input_tactic tries to locate an input tac m in the script. pursuing this goal the script is executed until an (m' equiv m) is found, or the end of the script args @@ -509,12 +511,12 @@ NOT IMPL. -- "error: do other step before" NotLocatable: thus generate_hard *) -fun locate_gen (thy', _) (Tac.Rewrite' (_, ro, er, pa, thm, f, _)) (pt, p) (*TODO-LucinNEW del in script.sml*) +fun locate_input_tactic (thy', _) (Tac.Rewrite' (_, ro, er, pa, thm, f, _)) (pt, p) (*TODO-LucinNEW del in script.sml*) (Rule.Rfuns {locate_rule=lo,...}, _) (Selem.RrlsState (_,f'',rss,rts), _) = (case lo rss f (Rule.Thm thm) of [] => NotLocatable | rts' => Steps (Lucin.rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts')) - | locate_gen (thy', srls) m (pt, p) + | locate_input_tactic (thy', srls) m (pt, p) (scr as Rule.Prog sc, d) (Selem.ScrState (E,l,a,v,S,b), ctxt) = let val thy = Celem.assoc_thy thy'; in case if l = [] orelse ( @@ -530,7 +532,7 @@ then let val (po,p_) = p - val po' = case p_ of Frm => po | Res => lev_on po | _ => error ("locate_gen " ^ pos_2str p_) + val po' = case p_ of Frm => po | Res => lev_on po | _ => error ("locate_input_tactic " ^ pos_2str p_) val (p'',c'',f'',pt'') = Generate.generate1 thy m (Selem.ScrState is, ctxt) (po',p_) pt in Steps (Selem.ScrState is, [(m, f'',pt'',p'',c'')]) end else Steps (Selem.ScrState is, ss)) @@ -538,8 +540,8 @@ | NasApp _ => NotLocatable | err => error ("not-found-in-script: NotLocatable from " ^ @{make_string} err) end - | locate_gen _ m _ (sc,_) (is, _) = - error ("locate_gen: wrong arguments,\n tac= " ^ Tac.tac_2str m ^ ",\n " ^ + | locate_input_tactic _ m _ (sc,_) (is, _) = + error ("locate_input_tactic: wrong arguments,\n tac= " ^ Tac.tac_2str m ^ ",\n " ^ "scr= " ^ Rule.scr2str sc ^ ",\n istate= " ^ Selem.istate2str is); (** locate an input formula in the program **) @@ -605,7 +607,7 @@ | _ => error "nxt_solv Check_Postcond': uncovered case get_loc" val thy' = get_obj g_domID pt pp; val thy = Celem.assoc_thy thy'; - val (_, _, (scval, scsaf)) = next_tac (thy', srls) (pt, (p, p_)) sc loc; + val (_, _, (scval, scsaf)) = determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc; in if pp = [] then @@ -647,14 +649,14 @@ let val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; - val (tac_, is, (t, _)) = next_tac (thy', srls) (pt, pos) sc is; + val (tac_, is, (t, _)) = determine_next_tactic (thy', srls) (pt, pos) sc is; (* TODO here ^^^ return finished/helpless/ok !*) in case tac_ of Tac.End_Detail' _ => ([(Tac.End_Detail, Tac.End_Detail' (t, [(*FIXME.04*)]), (pos, is))], [], (pt, pos)) | _ => nxt_solv tac_ is ptp end; -(* compare inform with ctree.form at current pos by nrls; +(* compare locate_input_formula with ctree.form at current pos by nrls; if found, embed the derivation generated during comparison if not, let the mat-engine compute the next ctree.form *) (* code's structure is copied from complete_solve @@ -704,7 +706,7 @@ collect all the tacs applied by the way; if "no derivation found" then check_error_patterns. ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*) -fun inform (cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr = +fun locate_input_formula (cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr = case TermC.parse (Celem.assoc_thy "Isac") istr of SOME f_in => let @@ -729,10 +731,10 @@ val pp = Ctree.par_pblobj pt p val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog) - | _ => error "inform: uncovered case of get_met" + | _ => error "locate_input_formula: uncovered case of get_met" val env = case Ctree.get_istate pt pos of Selem.ScrState (env, _, _, _, _, _) => env - | _ => error "inform: uncovered case of get_istate" + | _ => error "locate_input_formula: uncovered case of get_istate" in case Inform.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate') diff -r 0422e662c304 -r f25ce1922b60 src/Tools/isac/Interpret/script.sml --- a/src/Tools/isac/Interpret/script.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/src/Tools/isac/Interpret/script.sml Tue Jun 25 12:48:24 2019 +0200 @@ -45,7 +45,7 @@ end -(* traces the leaves (ie. non-tactical nodes) of Prog found by next_tac, see "and scr" *) +(* traces the leaves (ie. non-tactical nodes) of Prog found by determine_next_tactic, see "and scr" *) val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *) structure Lucin(**): LUCAS_INTERPRETER_DEL(**) = @@ -638,7 +638,7 @@ val metID = get_obj g_metID pt p' val {srls,...} = Specify.get_met metID in (srls, get_loc pt (p,p_), (#scr o Specify.get_met) metID) end - else (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in locate_gen, next_tac*) (* 3 *) + else (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in locate_input_formula, determine_next_tactic*) (* 3 *) (Rule.e_rls, get_loc pt (p,p_), case rls' of Rule.Rls {scr = scr,...} => scr diff -r 0422e662c304 -r f25ce1922b60 src/Tools/isac/Interpret/solve.sml --- a/src/Tools/isac/Interpret/solve.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/src/Tools/isac/Interpret/solve.sml Tue Jun 25 12:48:24 2019 +0200 @@ -134,10 +134,10 @@ end | NONE => (*execute the first tac in the Script, compare solve m*) let - val (m', (is', ctxt'), _) = LucinNEW.next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt); + val (m', (is', ctxt'), _) = LucinNEW.determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt); val d = Rule.e_rls (*FIXME: get simplifier from domID*); in - case LucinNEW.locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') of + case LucinNEW.locate_input_tactic (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') of LucinNEW.Steps (_, ss as (_, _, pt', p', c') :: _) => ("ok", (map step2taci ss, c', (pt', p'))) | _ => (* NotLocatable *) @@ -170,7 +170,7 @@ | _ => error "solve Check_Postcond: uncovered case get_loc" val thy' = get_obj g_domID pt pp; val thy = Celem.assoc_thy thy'; - val (_, _, (scval, scsaf)) = LucinNEW.next_tac (thy', srls) (pt, (p, p_)) sc loc; + val (_, _, (scval, scsaf)) = LucinNEW.determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc; in if pp = [] then @@ -218,10 +218,10 @@ val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; val d = Rule.e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*) in - case LucinNEW.locate_gen (thy', srls) m (pt, (p, p_)) (sc, d) is of + case LucinNEW.locate_input_tactic (thy', srls) m (pt, (p, p_)) (sc, d) is of LucinNEW.Steps (_, ss as (_, _, pt', p', c') :: _) => ("ok", (map step2taci ss, c', (pt', p'))) - (*27.8.02:next_tac may change to other branches in pt FIXXXXME*) + (*27.8.02:determine_next_tactic may change to other branches in pt FIXXXXME*) | _ => (* NotLocatable *) let val (p,ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac") m (p, p_) pt; diff -r 0422e662c304 -r f25ce1922b60 src/Tools/isac/ThydataC/rule.sml --- a/src/Tools/isac/ThydataC/rule.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/src/Tools/isac/ThydataC/rule.sml Tue Jun 25 12:48:24 2019 +0200 @@ -202,7 +202,7 @@ | Rfuns of (* for Rrls, usage see rational.sml ----- reverse rewrite ----- *) {init_state : (* initialise for reverse rewriting by the Interpreter *) term -> (* for this the rrlsstate is initialised: *) - term * (* the current formula: goes locate_gen -> next_tac via istate *) + term * (* the current formula: goes locate_input_tactic -> determine_next_tactic via istate *) term * (* the final formula *) rule list (* of reverse rewrite set (#1#) *) list * (* may be serveral, eg. in norm_rational *) diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/Interpret/inform.sml --- a/test/Tools/isac/Interpret/inform.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/Interpret/inform.sml Tue Jun 25 12:48:24 2019 +0200 @@ -24,7 +24,7 @@ "CAS-command:"; "--------- CAS-command on ([],Pbl) -------------------------------"; "--------- CAS-command on ([],Pbl) FE-interface ------------------"; -"--------- inform [rational,simplification] ----------------------"; +"--------- locate_input_formula [rational,simplification] ----------------------"; "--------- Take as 1st tac, start with (CAS input) ---------"; "--------- Take as 1st tac, start from exp -----------------------"; "--------- init_form, start with (CAS input) ---------------"; @@ -469,7 +469,7 @@ val (p,_,f,nxt,_,pt) = CalcTreeTEST [([], ("e_domID", ["e_pblID"], ["e_metID"]))]; val ifo = "solve(x+1=2,x)"; -val (_,(_,c,(pt,p))) = inform ([],[],(pt,p)) "solve(x+1=2,x)"; +val (_,(_,c,(pt,p))) = locate_input_formula ([],[],(pt,p)) "solve(x+1=2,x)"; show_pt pt; val nxt = ("Apply_Method",Apply_Method ["Test","squ-equ-test-subpbl1"]); val (p,_,f,nxt,_,pt) = me nxt p [] pt; @@ -492,9 +492,9 @@ else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface"; DEconstrCalcTree 1; -"--------- inform [rational,simplification] ----------------------"; -"--------- inform [rational,simplification] ----------------------"; -"--------- inform [rational,simplification] ----------------------"; +"--------- locate_input_formula [rational,simplification] ----------------------"; +"--------- locate_input_formula [rational,simplification] ----------------------"; +"--------- locate_input_formula [rational,simplification] ----------------------"; reset_states (); CalcTree [(["Term (a * x / (b * x) + c * x / (d * x) + e / f)", "normalform N"], ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))]; @@ -1021,7 +1021,7 @@ (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))), <<=== input follos: "...+ cos(4.x^3)" (([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4))] *) -"~~~~~ fun inform, args:"; val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) = +"~~~~~ fun locate_input_formula , args:"; val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) = (cs', (encode ifo)); val SOME f_in = parse (assoc_thy "Isac") istr val f_in = Thm.term_of f_in @@ -1044,15 +1044,15 @@ SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate') | NONE => msg_calcstate'; -"~~~~~ from inform return val:"; val () = (); +"~~~~~ from locate_input_formula return val:"; val () = (); case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of SOME errpatID => () | NONE => error "check_error_patterns broken"; "--- final check:"; -case inform cs' (encode ifo) of +case locate_input_formula cs' (encode ifo) of ("error pattern #chain-rule-diff-both#", calcstate') => () -| _ => error "inform with (positive) check_error_patterns broken" +| _ => error "locate_input_formula with (positive) check_error_patterns broken" "--------- build fun get_fillpats --------------------------------"; "--------- build fun get_fillpats --------------------------------"; diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/Interpret/mathengine.sml --- a/test/Tools/isac/Interpret/mathengine.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/Interpret/mathengine.sml Tue Jun 25 12:48:24 2019 +0200 @@ -144,7 +144,7 @@ val ("ok", cs' as (_,_,(pt,p))) = step p cs; val ifo = (* encode "4^^^2" \*) "4^2"; (* - val ("no derivation found", (_,_,(pt, p))) = inform cs' ((*encode*) ifo); + val ("no derivation found", (_,_,(pt, p))) = locate_input_formula cs' ((*encode*) ifo); here ^^^^^^^^^^^^^^^^^^^^^ should be "ok" *) @@ -511,7 +511,7 @@ e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*) val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; -val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; (*WAS Empty_Tac_: tac_*) +val (tac_,is,(t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is; (*WAS Empty_Tac_: tac_*) case tac_ of Or_to_List' _ => () | _ => error "Or_to_List broken ?" @@ -615,13 +615,13 @@ e_metID = get_obj g_metID pt (par_pblobj pt p) = false; val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; - val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; + val (tac_,is,(t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is; (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*) -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); l = [] = false; nstep_up thy ptp sc E l Skip_ a v (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...) - BUT WE FIND IN THE CODE ABOVE IN next_tac:*) + BUT WE FIND IN THE CODE ABOVE IN determine_next_tactic:*) ; (*----------------------------------------------------------------------------------------------*) if string_of_thmI @{thm rnorm_equation_add} = "\ ?b =!= 0 \ (?a = ?b) = (?a + - 1 * ?b = 0)" @@ -716,8 +716,8 @@ (* val cs = get_calc cI (* we improve from the calcstate here [*] *); val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);*) val ("ok", cs') = step pos cs; -(*val ("ok", (_, c, ptp as (_,p))) = *)inform cs' (encode ifo); -"~~~~~ fun inform, args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) = +(*val ("ok", (_, c, ptp as (_,p))) = *)locate_input_formula cs' (encode ifo); +"~~~~~ fun locate_input_formula , args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) = (cs', (encode ifo)); val SOME f_in = parse (assoc_thy "Isac") istr val f_in = Thm.term_of f_in diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/Interpret/script.sml --- a/test/Tools/isac/Interpret/script.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/Interpret/script.sml Tue Jun 25 12:48:24 2019 +0200 @@ -152,7 +152,7 @@ (*WAS stac2tac_ TODO: no match for SubProblem*) val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); l; (*= [R, L, R, L, R, R]*) val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v; @@ -201,9 +201,9 @@ val ini = init_form thy sc env; val p = lev_dn p; ini = NONE; (*true*) - val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt); + val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt); val d = e_rls (*FIXME: get simplifier from domID*); -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), +"~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt')); val thy = assoc_thy thy'; diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/Knowledge/biegelinie-3.sml --- a/test/Tools/isac/Knowledge/biegelinie-3.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/Knowledge/biegelinie-3.sml Tue Jun 25 12:48:24 2019 +0200 @@ -105,13 +105,13 @@ val ini = Lucin.init_form thy sc env; val p = lev_dn p; val NONE = (*case*) ini (*of*); - val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt); + val (m', (is', ctxt'), _) = determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt); val d = Rule.e_rls (*FIXME: get simplifier from domID*); val Steps (_, ss as (_, _, pt', p', c') :: _) = -(*case*) locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') (*of*); +(*case*) locate_input_tactic (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') (*of*); (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt' (fst p'); -(*+*)(*MISSING after locate_gen:*) +(*+*)(*MISSING after locate_input_tactic:*) (*+*)writeln (oris2str oris); (*[ (1, ["1"], #Given,Streckenlast, ["q_0"]), (2, ["1"], #Given,FunktionsVariable, ["x"]), @@ -120,7 +120,7 @@ Biegelinie AbleitungBiegelinie *) -"~~~~~ fun locate_gen , args:"; val ((thy', srls), m, (pt, p), +"~~~~~ fun locate_input_tactic , args:"; val ((thy', srls), m, (pt, p), (scr as Rule.Prog sc, d), (Selem.ScrState (E,l,a,v,S,b), ctxt)) = ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt')); val thy = Celem.assoc_thy thy'; diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/Knowledge/diff.sml --- a/test/Tools/isac/Knowledge/diff.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/Knowledge/diff.sml Tue Jun 25 12:48:24 2019 +0200 @@ -20,7 +20,7 @@ "----------- autoCalculate diff after_simplification ----"; "----------- autoCalculate differentiate_equality -------"; "----------- tests for examples -------------------------"; -"------------inform for x^2+x+1 -------------------------"; +"------------locate_input_formula for x^2+x+1 -------------------------"; "--------------------------------------------------------"; "--------------------------------------------------------"; "--------------------------------------------------------"; @@ -409,9 +409,9 @@ val subs = [(str2term "bdv", str2term "l")]; val f = str2term "G' = d_d l (l * sqrt (7 * s ^^^ 2 - l ^^^ 2))"; -"------------inform for x^2+x+1 -------------------------"; -"------------inform for x^2+x+1 -------------------------"; -"------------inform for x^2+x+1 -------------------------"; +"------------locate_input_formula for x^2+x+1 -------------------------"; +"------------locate_input_formula for x^2+x+1 -------------------------"; +"------------locate_input_formula for x^2+x+1 -------------------------"; reset_states (); CalcTree [(["functionTerm (x^2 + x + 1)", diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/Knowledge/inssort.sml --- a/test/Tools/isac/Knowledge/inssort.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/Knowledge/inssort.sml Tue Jun 25 12:48:24 2019 +0200 @@ -118,7 +118,7 @@ "----------- insertion sort: CAS-command -------------------------------------"; "----------- insertion sort: CAS-command -------------------------------------"; val (p,_,f,nxt,_,pt) = CalcTreeTEST [([], ("e_domID", ["e_pblID"], ["e_metID"]))]; -val (_,(_,c,(pt,p))) = inform ([],[],(pt,p)) "Sort {||1, 3, 2||}"; +val (_,(_,c,(pt,p))) = locate_input_formula ([],[],(pt,p)) "Sort {||1, 3, 2||}"; show_pt pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Apply_Method",..*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/Knowledge/polyeq.sml --- a/test/Tools/isac/Knowledge/polyeq.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/Knowledge/polyeq.sml Tue Jun 25 12:48:24 2019 +0200 @@ -192,11 +192,11 @@ val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; val d = e_rls; -(*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is; +(*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is; WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*) -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), +"~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = - ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *) + ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_input_tactic 2nd pattern *) val thy = assoc_thy thy'; l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*); (*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/Knowledge/rateq.sml --- a/test/Tools/isac/Knowledge/rateq.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/Knowledge/rateq.sml Tue Jun 25 12:48:24 2019 +0200 @@ -103,7 +103,7 @@ "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*) -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); "~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = @@ -292,7 +292,7 @@ e_metID = get_obj g_metID pt (par_pblobj pt p); (* = false*) val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); l = []; (* = false*) "~~~~~ and nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = @@ -318,7 +318,7 @@ nstep_up thy ptp scr E l ay a v; nxt_up thy ptp (Prog sc) E up ay (go up sc) a v; nstep_up thy ptp sc E l Skip_ a v; -next_tac (thy',srls) (pt,pos) sc is; +determine_next_tactic (thy',srls) (pt,pos) sc is; nxt_solve_ (pt,ip); step p ((pt, e_pos'),[]); *) diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/Minisubpbl/200-start-method.sml --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Tue Jun 25 12:48:24 2019 +0200 @@ -130,7 +130,7 @@ Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false*); val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)), +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)), (Selem.ScrState (E,l,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is); l = [] (* = true*); "~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) = diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue Jun 25 12:48:24 2019 +0200 @@ -44,8 +44,8 @@ val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; val d = Rule.e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*) -locate_gen (thy',srls) m (pt,(p, p_)) (sc,d) is; (* assy: call by ([3], Pbl)*) -"~~~~~ fun locate_gen, args:"; val ((thy', srls), m, (pt, p), +locate_input_tactic (thy',srls) m (pt,(p, p_)) (sc,d) is; (* assy: call by ([3], Pbl)*) +"~~~~~ fun locate_input_tactic, args:"; val ((thy', srls), m, (pt, p), (scr as Rule.Prog (_ $ body),d), (Selem.ScrState (E,l,a,v,S,b), ctxt)) = ((thy',srls), m, (pt,(p, p_)), (sc,d), is); val thy = Celem.assoc_thy thy'; @@ -109,9 +109,9 @@ val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; -(* isabisac17: val (tac_, is, (t, _)) = Lucin.next_tac (thy', srls) (pt, pos) sc is; +(* isabisac17: val (tac_, is, (t, _)) = determine_next_tactic (thy', srls) (pt, pos) sc is; go: no [L,L,R] *) -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Prog (_ $ body)), +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Prog (_ $ body)), (ScrState (E,l,a,v,s,_), ctxt) ) = ((thy', srls), (pt, pos), sc, is); (*if*) l = [] = false; diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/Minisubpbl/300-init-subpbl.sml --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Tue Jun 25 12:48:24 2019 +0200 @@ -34,8 +34,8 @@ val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; val d = e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*) -(*val Steps (is', ss as (m',f',pt',p',c')::_) = locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;*) -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), +(*val Steps (is', ss as (m',f',pt',p',c')::_) = locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is;*) +"~~~~~ fun locate_input_tactic, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = ((thy',srls), m, (pt,(p,p_)), (sc,d), is); val thy = assoc_thy thy'; diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Tue Jun 25 12:48:24 2019 +0200 @@ -64,7 +64,7 @@ "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); val ctxt = get_ctxt pt pos; val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Tue Jun 25 12:48:24 2019 +0200 @@ -46,7 +46,7 @@ e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*) val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*) -val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; +val (tac_,is,(t,_)) = determine_next_tactic (thy',srls) (pt,pos) sc is; ;tac_; (* = Check_Postcond' *) "~~~~~ fun nxt_solv, args:"; val ((Check_Postcond' (pI,_)), _, (pt, pos as (p,p_))) = (tac_, is, ptp); @@ -62,7 +62,7 @@ val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_); val thy' = get_obj g_domID pt pp; val thy = assoc_thy thy'; - val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc; + val (_,_,(scval,scsaf)) = determine_next_tactic (thy',srls) (pt,(p,p_)) sc loc; ;pp = []; (*false*) val ppp = par_pblobj pt (lev_up p); val thy' = get_obj g_domID pt ppp; diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Tue Jun 25 12:48:24 2019 +0200 @@ -55,7 +55,7 @@ "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*) -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)), +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); val ctxt = get_ctxt pt pos val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/Minisubpbl/700-interSteps.sml --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Tue Jun 25 12:48:24 2019 +0200 @@ -110,9 +110,9 @@ (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false isabisac = ?*); val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; -(* val (tac_, is, (t, _)) =*) next_tac (thy', srls) (pt, pos) sc is; +(* val (tac_, is, (t, _)) =*) determine_next_tactic (thy', srls) (pt, pos) sc is; ; -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)), +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)), (Selem.ScrState (E,l,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is); (*if*) l = [] (* = true *); appy thy ptp E [Celem.R] body NONE v; diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/OLDTESTS/root-equ.sml --- a/test/Tools/isac/OLDTESTS/root-equ.sml Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Tue Jun 25 12:48:24 2019 +0200 @@ -566,9 +566,9 @@ val thy = assoc_thy thy'; val d = e_rls; val Steps [(m',f',pt',p',c',s')] = - locate_gen thy' m (pt,(p,p_)) (sc,d) is; + locate_input_tactic thy' m (pt,(p,p_)) (sc,d) is; val is' = get_istate pt' p'; - next_tac thy' (pt'(*'*),p') sc is'; + determine_next_tactic thy' (pt'(*'*),p') sc is'; diff -r 0422e662c304 -r f25ce1922b60 test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Tue Jun 25 10:46:20 2019 +0200 +++ b/test/Tools/isac/Test_Isac.thy Tue Jun 25 12:48:24 2019 +0200 @@ -93,7 +93,8 @@ in case of errors here consider ~~/./xtest-to-coding.sh *) open Kernel; open Math_Engine; CalcTreeTEST; - open Lucin; appy; + open Lucin; itms2args; + open LucinNEW; appy; open Inform; cas_input; open Rtools; trtas2str; open Chead; pt_extract; @@ -242,13 +243,13 @@ ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml" ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml" ML \"%%%%%%%%%%%%%%%%% end ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%%%";\ -ML \ -\ ML \ -\ ML \ -\ ML \"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\ ML \"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\ ML \"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\ +ML \ +\ ML \ +\ ML \ +\ section \history of tests\ text \