neuper@42279: (* Title: tests for Interpret/mathengine.sml neuper@42279: Author: Walther Neuper 2000, 2006 neuper@37906: (c) due to copyright terms neuper@55460: neuper@55460: theory Test_Some imports Build_Thydata begin neuper@55460: ML {* KEStore_Elems.set_ref_thy @{theory}; neuper@55460: fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join *} neuper@55460: ML_file "~~/test/Tools/isac/Interpret/mathengine.sml" neuper@37906: *) neuper@38065: "--------------------------------------------------------"; neuper@38065: "table of contents --------------------------------------"; neuper@38065: "--------------------------------------------------------"; neuper@41940: "----------- change to parse ctxt -----------------------"; neuper@38065: "----------- debugging setContext..pbl_ -----------------"; neuper@38065: "----------- tryrefine ----------------------------------"; neuper@55412: "---------- mini-subpbl isac-java 3992e3bd1948: initial ---------------"; neuper@41982: "----------- fun step: Apply_Method without init_form ---"; neuper@38065: "----------- fun step -----------------------------------"; neuper@38065: "----------- fun autocalc -------------------------------"; wneuper@59248: "----------- fun autoCalculate --------------------------"; neuper@42067: "----------- fun autoCalculate..CompleteCalc ------------"; t@42225: "----------- search for Or_to_List ----------------------"; neuper@42279: "----------- check thy in CalcTreeTEST ------------------"; neuper@55482: "----------- identified error in fun getTactic, string_of_thmI ---------------"; neuper@55486: "----------- improved fun getTactic for interSteps and numeral calculations --"; neuper@38065: "--------------------------------------------------------"; neuper@38065: "--------------------------------------------------------"; neuper@38065: "--------------------------------------------------------"; neuper@37906: neuper@41940: "----------- change to parse ctxt -----------------------"; neuper@41940: "----------- change to parse ctxt -----------------------"; neuper@41940: "----------- change to parse ctxt -----------------------"; neuper@41940: "===== start calculation: from problem description (fmz) to origin"; neuper@41940: val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"]; neuper@41940: val (thyID, pblID, metID) = neuper@41940: ("Test", ["calculate", "test"], ["Test", "test_calculate"]); wneuper@59116: (*======= Isabelle2013-2 --> Isabelle2014: unclear, why this test ever run ======================== neuper@41940: val (p,_,_,nxt,_,pt) = CalcTreeTEST [(fmz, (thyID, pblID, metID))]; neuper@41940: "----- "; neuper@41940: (* call sequence: CalcTreeTEST neuper@41940: > nxt_specify_init_calc neuper@41940: > prep_ori neuper@41940: *) neuper@41940: val (thy, pbt) = (Thy_Info.get_theory thyID, (#ppc o get_pbt) pblID); neuper@41940: "----- in prep_ori"; neuper@48761: val ctxt = Proof_Context.init_global thy; neuper@41940: bonzai@41952: val ctopts = map (parseNEW ctxt) fmz; bonzai@41952: val dts = map (split_dts o the) ctopts; neuper@41940: (*split_dts: neuper@41940: (term * term list) list neuper@41940: formulas: e.g. ((1+2)*4/3)^^^2 neuper@41940: description: e.g. realTestGiven neuper@41940: *) neuper@41940: prep_ori; neuper@41940: (* FROM neuper@41940: val it = fn: neuper@41940: string list -> theory -> (string * (term * 'a)) list -> ori list neuper@41940: TO neuper@41940: val it = fn: neuper@41940: string list -> theory -> (string * (term * 'a)) list -> (ori list * ctxt) neuper@41940: AND neuper@41940: FROM val oris = prep_ori... neuper@41940: TO val (oris, _) = prep_ori... neuper@41940: *) wneuper@59279: "----- insert ctxt in ctree"; neuper@41940: (* datatype ppobj neuper@41940: FROM loc : istate option * istate option, neuper@41940: TO loc : (istate * ctxt) option * (istate * ctxt) option, neuper@41940: e.g. neuper@41940: FROM val pt = Nd (PblObj neuper@41940: {.., loc = (SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)), neuper@41940: NONE), neuper@41940: TO val pt = Nd (PblObj neuper@41940: {.., loc = neuper@41940: ((SOME (ScrState ([], [], NONE, Const ("empty", "'a"), Sundef, false)), ctxt), neuper@41940: NONE), neuper@41940: *) neuper@41940: neuper@41940: "===== interactive specification: from origin to specification (probl)"; neuper@41940: val (p,_,_,nxt,_,pt) = me nxt p [1] pt; neuper@41940: (*nxt =("Add_Given", Model_Problem)*) neuper@41940: val (p,_,_,nxt,_,pt) = me nxt p [1] pt; neuper@41940: (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*) neuper@41940: "----- "; neuper@41940: (* call sequence: me Model_Problem neuper@41940: > me ("Add_Given", Add_Given "realTestGiven (((1 + 2) * 4 / 3) ^^^ 2)") neuper@41940: > locatetac tac neuper@41940: > loc_specify_ neuper@41940: > specify GET ctxt (stored in ctree) neuper@41940: > specify_additem neuper@41940: > appl_add neuper@41940: neuper@41940: *) neuper@41940: "----- in appl_add"; neuper@41940: (* FROM appl_add thy neuper@41940: TO appl_add ctxt neuper@41940: FROM parse thy str neuper@41940: TO parseNEW ctxt str neuper@41940: *) neuper@41940: val (p,_,_,nxt,_,pt) = me nxt p [1] pt; neuper@41940: (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*) neuper@41940: val (p,_,_,nxt,_,pt) = me nxt p [1] pt; neuper@41940: (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*) neuper@41940: neuper@41940: "===== end specify: from specification (probl) to guard (method)"; neuper@41940: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41940: (*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*) neuper@41940: neuper@41940: "===== start interpretation: from guard to environment"; neuper@41940: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41940: (*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*) neuper@41940: "----- "; neuper@41940: (* call sequence: me ("Apply_Method",... neuper@41940: > locatetac neuper@41940: > loc_solve_ neuper@41940: > solve ("Apply_Method",... neuper@41940: *) neuper@41940: val ((_,tac), ptp) = (nxt, (pt, p)); neuper@41940: locatetac tac (pt,p); neuper@41940: val (mI, m) = mk_tac'_ tac; neuper@41940: val Appl m = applicable_in p pt m; neuper@41940: member op = specsteps mI; neuper@41940: loc_solve_ (mI,m) ptp; neuper@41940: val (m, (pt, pos)) = ((mI,m), ptp); neuper@41940: solve m (pt, pos); bonzai@41949: val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) = neuper@41940: (m, (pt, pos)); neuper@41940: val {srls,...} = get_met mI; neuper@41940: val PblObj{meth=itms,...} = get_obj I pt p; neuper@41940: val thy' = get_obj g_domID pt p; neuper@41940: val thy = assoc_thy thy'; bonzai@41949: val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI; neuper@41940: neuper@41940: "----- go on in the calculation"; neuper@41940: val (p,_,f,nxt,_,pt) = me nxt pos [1] pt; neuper@41940: (*nxt = ("Calculate",Calculate "PLUS")*) neuper@41940: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41940: (*nxt = ("Calculate",Calculate "TIMES")*) neuper@41940: neuper@41940: "===== input a formula to be derived from previous istate"; neuper@41940: "----- appendFormula TODO: first repair error"; neuper@41940: val cs = ((pt,p),[]); neuper@41940: val ("ok", cs' as (_,_,(pt,p))) = step p cs; neuper@41943: val ifo = (* encode "4^^^2" \*) "4^2"; neuper@41940: (* neuper@41943: val ("no derivation found", (_,_,(pt, p))) = inform cs' ((*encode*) ifo); neuper@41940: here ^^^^^^^^^^^^^^^^^^^^^ should be "ok" neuper@41940: *) neuper@41940: neuper@41940: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41940: (*nxt = ("Calculate",Calculate "DIVIDE")*) neuper@41940: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41940: (*nxt = ("Calculate",Calculate "POWER")*) neuper@41940: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41940: (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*) neuper@41940: val (p,_,f,nxt,_,pt) = me nxt p [1] pt; neuper@41940: (*nxt = ("End_Proof'",End_Proof')*) neuper@41940: if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then () neuper@41940: else error "calculate.sml: script test_calculate changed behaviour"; neuper@41940: neuper@41940: "===== tactic Subproblem: from environment to origin"; neuper@41940: "----- TODO"; wneuper@59116: ======= Isabelle2013-2 --> Isabelle2014: unclear, why this test ever run ========================*) neuper@41940: neuper@37906: neuper@38065: "----------- debugging setContext..pbl_ -----------------"; neuper@38065: "----------- debugging setContext..pbl_ -----------------"; neuper@38065: "----------- debugging setContext..pbl_ -----------------"; s1210629013@55445: reset_states (); neuper@41970: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@41970: ("Test", ["sqroot-test","univariate","equation","test"], neuper@37906: ["Test","squ-equ-test-subpbl1"]))]; neuper@37906: Iterator 1; neuper@37906: moveActiveRoot 1; modelProblem 1; neuper@37906: neuper@37906: val pos as (p,_) = ([],Pbl); neuper@37906: val guh = "pbl_equ_univ"; neuper@37906: checkContext 1 pos guh; neuper@37906: val ((pt,_),_) = get_calc 1; neuper@37906: val pp = par_pblobj pt p; neuper@37906: val keID = guh2kestoreID guh; neuper@37906: case context_pbl keID pt pp of (true,["univariate", "equation"],_,_,_)=>() neuper@38031: | _ => error "mathengine.sml: context_pbl .. pbl_equ_univ checked"; neuper@37906: neuper@37906: case get_obj g_spec pt p of (_, ["e_pblID"], _) => () neuper@38031: | _ => error "mathengine.sml: context_pbl .. pbl still empty"; neuper@37906: setContext 1 pos guh; neuper@37906: val ((pt,_),_) = get_calc 1; neuper@37906: case get_obj g_spec pt p of (_, ["univariate", "equation"], _) => () neuper@38031: | _ => error "mathengine.sml: context_pbl .. pbl set"; neuper@37906: neuper@37906: neuper@37906: setContext 1 pos "met_eq_lin"; neuper@37906: val ((pt,_),_) = get_calc 1; neuper@37906: case get_obj g_spec pt p of (_, _, ["LinEq", "solve_lineq_equation"]) => () neuper@38031: | _ => error "mathengine.sml: context_pbl .. pbl set"; neuper@37906: neuper@37906: neuper@38065: "----------- tryrefine ----------------------------------"; neuper@38065: "----------- tryrefine ----------------------------------"; neuper@38065: "----------- tryrefine ----------------------------------"; s1210629013@55445: reset_states (); neuper@37906: CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", neuper@37906: "solveFor x", "solutions L"], neuper@38058: ("RatEq",["univariate","equation"],["no_met"]))]; neuper@37906: Iterator 1; wneuper@59248: moveActiveRoot 1; autoCalculate 1 CompleteCalc; neuper@37906: neuper@37906: refineProblem 1 ([1],Res) "pbl_equ_univ" neuper@37906: (*gives "pbl_equ_univ_rat" correct*); neuper@37906: neuper@55279: refineProblem 1 ([1],Res) (pblID2guh ["LINEAR","univariate","equation"]) neuper@38065: (*gives "pbl_equ_univ_lin" incorrect*); neuper@38065: neuper@55412: "---------- mini-subpbl isac-java 3992e3bd1948: initial ---------------"; neuper@55412: "---------- mini-subpbl isac-java 3992e3bd1948: initial ---------------"; neuper@55412: "---------- mini-subpbl isac-java 3992e3bd1948: initial ---------------"; s1210629013@55445: reset_states (); neuper@55412: (*this is the exact sequence of input provided by isac-java 3992e3bd1948; neuper@55412: Surrounding ML { * ... * } are omitted. neuper@55412: The multiple calls suggest to replicate the CalcTree in the Dialogue. neuper@55412: *) neuper@55412: CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], neuper@55412: ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))]; neuper@55412: Iterator 1; neuper@55412: moveActiveRoot 1; neuper@55412: getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false; neuper@55412: getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false; wneuper@59248: (*completeCalcHead*)autoCalculate 1 CompleteCalcHead; neuper@55412: (*completeCalcHead*)getActiveFormula 1 ; neuper@55412: (*completeCalcHead*)refFormula 1 ([],Met); neuper@55412: refFormula 1 ([],Pbl); neuper@55412: (* 1 *) neuper@55473: fetchProposedTactic 1; neuper@55473: (*-> neuper@55473: neuper@55473: Test neuper@55473: squ-equ-test-subpbl1 neuper@55473: WAS PREVIOUSLY: 1 error in kernel *) neuper@55412: "~~~~~ fun fetchProposedTactic, args:"; val (cI) = (1); neuper@55412: val ("ok", (tacis, _, _)) = step (get_pos cI 1) (get_calc cI) neuper@55412: val _= upd_tacis cI tacis neuper@55412: val (tac,_,_) = last_elem tacis; neuper@55412: (*fetchproposedtacticOK2xml cI tac (fetchErrorpatterns tac); neuper@55415: fetchErrorpatterns tac neuper@55473: WAS PREVIOUSLY ERROR: app_py: not found: ["IsacKnowledge","KEStore","Rulesets","e_rls"]*) neuper@55415: "~~~~~ fun fetchErrorpatterns, args:"; val (tac) = (tac); neuper@55415: val rlsID = "e_rls" neuper@55415: val (part, thyID) = thy_containing_rls "Build_Thydata" rlsID; neuper@55458: if part = "IsacScripts" andalso thyID = "KEStore" then () neuper@55415: else error "fetchErrorpatterns .. e_rls changed"; neuper@55473: val Hrls {thy_rls = (_, rls), ...} = get_the [part, thyID, "Rulesets", rlsID]; neuper@55473: (* WAS PREVIOUSLY ERROR app_py: not found: ["IsacKnowledge","KEStore","Rulesets","e_rls"]*) neuper@55473: case rls of neuper@55473: Rls {id = "e_rls", ...} => () neuper@55473: | _ => error "thy_containing_rls changed for e_rls" neuper@38065: neuper@41982: "----------- fun step: Apply_Method without init_form ---"; neuper@41982: "----------- fun step: Apply_Method without init_form ---"; neuper@41982: "----------- fun step: Apply_Method without init_form ---"; neuper@41982: val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; neuper@41982: val (dI',pI',mI') = neuper@41982: ("Test", ["sqroot-test","univariate","equation","test"], neuper@41982: ["Test","squ-equ-test-subpbl1"]); neuper@41982: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; neuper@41982: "~~~~~ fun me, args:"; val (_,tac) = nxt; neuper@41982: val ("ok", (_, _, (pt, p))) = locatetac tac (pt,p); neuper@41982: "~~~~~ fun step, args:"; val (ip as (_,p_), ptp as (pt,p), tacis) = (p, (pt, e_pos'), []); neuper@41982: val pIopt = get_pblID (pt,ip); neuper@41982: ip = ([],Res) (*false*); neuper@41982: val SOME pI = pIopt; neuper@55412: member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); neuper@41982: (*^^^^^^^^: Apply_Method without init_form*) neuper@38065: neuper@38065: "----------- fun step -----------------------------------"; neuper@38065: "----------- fun step -----------------------------------"; neuper@38065: "----------- fun step -----------------------------------"; neuper@38065: val p = e_pos'; val c = []; neuper@38065: val (p,_,f,nxt,_,pt) = neuper@38065: CalcTreeTEST neuper@38065: [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"], neuper@38065: ("Integrate", ["integrate","function"], ["diff","integration"]))]; neuper@38065: "----- step 1: returns tac = Model_Problem ---"; neuper@38065: val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []); neuper@38065: "----- step 2: returns tac = ---"; neuper@38065: val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []); neuper@38065: "----- step 3: returns tac = ---"; neuper@38065: val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []); neuper@38065: "----- step 4: returns tac = ---"; neuper@38065: val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []); neuper@38065: "----- step 5: returns tac = ---"; neuper@38065: neuper@48895: (*========== inhibit exn AK110718 ============================================== neuper@38066: 2002 stops here as well: TODO review actual arguments: neuper@38065: val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []); neuper@38065: "----- step 6: returns tac = ---"; neuper@38065: val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []); neuper@38065: "----- step 7: returns tac = ---"; neuper@38065: val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []); neuper@38065: "----- step 8: returns tac = ---"; neuper@38065: val (str, ([(tac, _, _)], _, (pt, p))) = step p ((pt, e_pos'), []); neuper@48895: ========== inhibit exn AK110718 ==============================================*) neuper@38065: neuper@38065: neuper@38065: "----------- fun autocalc -------------------------------"; neuper@38065: "----------- fun autocalc -------------------------------"; neuper@38065: "----------- fun autocalc -------------------------------"; neuper@38065: val p = e_pos'; val c = []; neuper@38065: val (p,_,f,nxt,_,pt) = neuper@38065: CalcTreeTEST neuper@38065: [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"], neuper@38065: ("Integrate",["integrate","function"], ["diff","integration"]))]; neuper@38066: (*-----since Model_Problem + complete_mod_ in case cas of SOME-----* neuper@38066: modeling is skipped FIXME neuper@38066: *-----since Model_Problem + complete_mod_ in case cas of SOME-----*) neuper@38065: tracing "----- step 1 ---"; neuper@38065: val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt; neuper@38065: tracing "----- step 2 ---"; neuper@38065: val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt; neuper@38065: tracing "----- step 3 ---"; neuper@38065: val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt; neuper@38065: tracing "----- step 4 ---"; neuper@38065: val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt; neuper@38065: tracing "----- step 5 ---"; neuper@38065: val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt; neuper@38065: tracing "----- step 6 ---"; neuper@38065: val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt; neuper@38065: tracing "----- step 7 ---"; neuper@38065: val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt; neuper@38065: tracing "----- step 8 ---"; neuper@38065: val (str, cut, (pt, p)) = autocalc [] p ((pt, e_pos'),[]) (Step 1); show_pt pt; neuper@48895: (*========== inhibit exn AK110718 ============================================== neuper@42067: WN110628: Integration does not work, see Knowledge/integrate.sml neuper@42067: neuper@41929: if str = "end-of-calculation" andalso neuper@41929: term2str (get_obj g_res pt (fst p)) = "c + x + 1 / 3 * x ^^^ 3" then () neuper@38065: else error "mathengine.sml -- fun autocalc -- end"; neuper@48895: ========== inhibit exn AK110718 ==============================================*) neuper@38065: neuper@38065: wneuper@59248: "----------- fun autoCalculate -----------------------------------"; wneuper@59248: "----------- fun autoCalculate -----------------------------------"; wneuper@59248: "----------- fun autoCalculate -----------------------------------"; s1210629013@55445: reset_states (); neuper@38065: CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*) neuper@38065: [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"], neuper@38065: ("Integrate", ["integrate", "function"], ["diff", "integration"]))]; neuper@38065: Iterator 1; neuper@38065: moveActiveRoot 1; neuper@38066: (*-----since Model_Problem + complete_mod_ in case cas of SOME-----* neuper@38066: modeling is skipped FIXME neuper@38066: see test/../interface -- solve_linear as rootpbl FE -- for OTHER expl: neuper@38066: setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*); neuper@38066: neuper@38066: fetchProposedTactic 1; neuper@38066: setNextTactic 1 (Add_Given "solveFor x"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@38066: neuper@38066: fetchProposedTactic 1; neuper@38066: setNextTactic 1 (Add_Find "solutions L"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@38066: neuper@38066: fetchProposedTactic 1; neuper@38066: setNextTactic 1 (Specify_Theory "Test"); wneuper@59248: autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); neuper@38066: *-----since Model_Problem + complete_mod_ in case cas of SOME-----*) wneuper@59248: autoCalculate 1 (Step 1); neuper@38065: "----- step 1 ---"; wneuper@59248: autoCalculate 1 (Step 1); neuper@38065: "----- step 2 ---"; wneuper@59248: autoCalculate 1 (Step 1); neuper@38065: "----- step 3 ---"; wneuper@59248: autoCalculate 1 (Step 1); neuper@38065: "----- step 4 ---"; wneuper@59248: autoCalculate 1 (Step 1); neuper@38065: "----- step 5 ---"; wneuper@59248: autoCalculate 1 (Step 1); neuper@38065: "----- step 6 ---"; wneuper@59248: autoCalculate 1 (Step 1); neuper@38065: "----- step 7 ---"; wneuper@59248: autoCalculate 1 (Step 1); neuper@38065: "----- step 8 ---"; wneuper@59248: autoCalculate 1 (Step 1); neuper@38065: val (ptp as (_, p), _) = get_calc 1; neuper@38065: val (Form t,_,_) = pt_extract ptp; akargl@42108: neuper@38065: if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then () wneuper@59248: else error "mathengine.sml -- fun autoCalculate -- end"; neuper@38065: neuper@42067: "----------- fun autoCalculate..CompleteCalc ------------"; neuper@42067: "----------- fun autoCalculate..CompleteCalc ------------"; neuper@42067: "----------- fun autoCalculate..CompleteCalc ------------"; s1210629013@55445: reset_states (); neuper@42067: CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], neuper@42067: ("Test", ["sqroot-test","univariate","equation","test"], neuper@42067: ["Test","squ-equ-test-subpbl1"]))]; neuper@42067: Iterator 1; neuper@42103: moveActiveRoot 1; wneuper@59248: (*autoCalculate 1 CompleteCalc; (*WAS .. error in kernel *)*) neuper@42103: "~~~~~ fun autoCalculate, args:"; val (cI, auto) = (1, CompleteCalc); neuper@42103: val pold = get_pos cI 1; neuper@42103: (*autocalc [] pold (get_calc cI) auto; (*WAS Type unification failed neuper@42103: Type error in application: incompatible operand type neuper@42103: Operator: solveFor :: real \ una neuper@42103: Operand: x :: 'a *)*) neuper@42103: "~~~~~ fun autocalc, args:"; val (c, (pos as (_,p_)), ((pt,_), _), auto) neuper@42103: = ([] : pos' list, pold, (get_calc cI), auto); neuper@42103: autoord auto > 3 andalso just_created (pt, pos); (*true*) neuper@42103: val ptp = all_modspec (pt, pos); neuper@42103: "TODO all_modspec: preconds for rootpbl"; neuper@42103: (*all_solve auto c ptp; (*WAS Type unification failed...*)*) neuper@42103: "~~~~~ and all_solve, args:"; val (auto, c, (ptp as (pt, pos as (p,_)))) = neuper@42103: (auto, c, ptp); neuper@42103: val (_,_,mI) = get_obj g_spec pt p neuper@42103: val ctxt = get_ctxt pt pos neuper@42103: val (ttt, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp; neuper@42103: (* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*) pos = ([], Met)*) neuper@42103: "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) = neuper@42103: (auto, (c @ c'), ptp); neuper@42103: p = ([], Res) (*false p = ([1], Frm)*); neuper@42103: member op = [Pbl,Met] p_ (*false*); neuper@42103: val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "norm_equation"*) neuper@42103: (* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*) neuper@42103: "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) = neuper@42103: (auto, (c @ c'), ptp'); neuper@42103: p = ([], Res) (*false p = ([1], Res)*); neuper@42103: member op = [Pbl,Met] p_ (*false*); neuper@42103: val (ttt, c', ptp') = nxt_solve_ ptp; (*ttt = Rewrite_Set "Test_simplify"*) neuper@42103: (* complete_solve auto (c @ c') ptp'; (*WAS Type unification failed...*) pos = ([], Met)*) neuper@42103: "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) = neuper@42103: (auto, (c @ c'), ptp'); neuper@42103: p = ([], Res) (*false p = ([2], Res)*); neuper@42103: member op = [Pbl,Met] p_ (*false*); neuper@42103: val ((Subproblem _, tac_, (_, is))::_, c', ptp') = nxt_solve_ ptp; neuper@42103: autoord auto < 5 (*false*); neuper@42103: (* val ptp = all_modspec ptp' (*WAS Type unification failed...*)*) neuper@42103: "~~~~~ fun all_modspec, args:"; val (pt, pos as (p,_)) = (ptp'); neuper@42103: val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p; neuper@42103: val thy = assoc_thy dI; neuper@42103: val {ppc, ...} = get_met mI; neuper@42103: (* val (mors, ctxt) = prep_ori fmz_ thy ppc; WAS Type unification failed because neuper@48761: val ctxt' = dI |> Thy_Info.get_theory |> Proof_Context.init_global; neuper@42103: (parseNEW ctxt' "x" |> the |> type_of) = TFree ("'a",[]); neuper@42103: ^^^^^ *) neuper@42103: (*vvv from: | assod pt _ (Subproblem'...*) neuper@42103: val (fmz_, vals) = oris2fmz_vals pors; neuper@42103: (**) neuper@48761: val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global neuper@42103: |> declare_constraints' vals neuper@42103: (**) neuper@42103: (*^^^ from: | assod pt _ (Subproblem'...*) neuper@42103: val [(1, [1], "#Given", dsc_eq, [equality]), neuper@42103: (2, [1], "#Given", dsc_solvefor, [xxx]), neuper@42103: (3, [1], "#Find", dsc_solutions, [x_i])] = pors; neuper@42103: if term2str xxx = "x" andalso type_of xxx = HOLogic.realT then () neuper@42103: else error "autoCalculate..CompleteCalc: SubProblem broken 1"; neuper@42103: val pt = update_pblppc pt p (map (ori2Coritm ppc) pors); neuper@42103: val pt = update_metppc pt p (map (ori2Coritm ppc) pors); neuper@42103: val pt = update_spec pt p (dI,pI,mI); neuper@42103: val pt = update_ctxt pt p ctxt; neuper@42103: "~~~~~ return to complete_solve, args:"; val (ptp) = (pt, (p,Met)); neuper@42103: val (msg, c, (pt, p)) = complete_solve auto (c @ c') ptp; neuper@42103: if msg = "end-of-calculation" andalso c = [] andalso p = ([], Res) then () neuper@42103: else error "autoCalculate..CompleteCalc: final result"; neuper@42103: if terms2strs (get_assumptions_ pt p) = neuper@42105: ["matches (?a = ?b) (-1 + x = 0)", (*precond of submet*) neuper@42104: "x = 1", (*result of subpbl and rootpbl*) neuper@42104: "precond_rootmet x"] (*precond of rootmet*) neuper@42103: then () else error "autoCalculate..CompleteCalc: ctxt at final result"; neuper@42067: akargl@42108: neuper@42394: "--------- search for Or_to_List ------------------------"; neuper@42394: "--------- search for Or_to_List ------------------------"; t@42225: "--------- search for Or_to_List ------------------------"; t@42225: val fmz = ["equality (x^^^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"]; t@42225: val (dI',pI',mI') = ("Isac", ["univariate","equation"], ["no_met"]) t@42225: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*) t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; t@42225: val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59279: "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ctree)) = t@42225: (nxt, p, [], pt); t@42225: val ("ok", (_, _, ptp)) = locatetac tac (pt,p) t@42225: val (pt, p) = ptp; t@42225: "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = t@42225: (p, ((pt, e_pos'),[])); t@42225: val pIopt = get_pblID (pt,ip); t@42225: ip = ([],Res); (*false*) t@42225: ip = p; (*false*) t@42225: member op = [Pbl,Met] p_; (*false*) t@42225: "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip); t@42225: e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*) t@42225: val thy' = get_obj g_domID pt (par_pblobj pt p); t@42225: val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; t@42225: val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; (*WAS Empty_Tac_: tac_*) t@42225: case tac_ of Or_to_List' _ => () t@42225: | _ => error "Or_to_List broken ?" akargl@42108: neuper@42394: neuper@42279: "----------- check thy in CalcTreeTEST ------------------"; neuper@42279: "----------- check thy in CalcTreeTEST ------------------"; neuper@42279: "----------- check thy in CalcTreeTEST ------------------"; neuper@42279: "WN1109 with Inverse_Z_Transform.thy when starting tests with CalcTreeTEST \n" ^ neuper@42279: "we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^ neuper@42279: "Below there are the steps which found out the reason: \n" ^ neuper@42279: "store_pbt mistakenly stored that theory."; neuper@48761: val ctxt = Proof_Context.init_global @{theory Isac}; neuper@42279: val SOME t = parseNEW ctxt "filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))"; neuper@42279: val SOME t = parseNEW ctxt "stepResponse (x[n::real]::bool)"; akargl@42108: neuper@42279: val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", neuper@42279: "stepResponse (x[n::real]::bool)"]; neuper@42405: val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"], neuper@42405: ["SignalProcessing","Z_Transform","Inverse"]); neuper@42279: neuper@42279: val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; neuper@42279: (*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*) neuper@42279: neuper@42279: "~~~~~ T fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI,pI,mI))]; neuper@42279: "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp); neuper@42279: val thy = assoc_thy dI; neuper@42279: mI = ["no_met"]; (*false*) neuper@42279: val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI) neuper@42279: val {cas, ppc, thy=thy',...} = get_pbt pI; (*take dI from _refined_ pbl*) neuper@42279: "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*) neuper@42279: val dI = theory2theory' (maxthy thy thy'); neuper@42279: "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*) neuper@42279: cas = NONE; (*true*) neuper@42279: val hdl = pblterm dI pI; wneuper@59279: val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) neuper@42279: (pors, (dI, pI, mI), hdl) neuper@42279: val pt = update_ctxt pt [] pctxt; neuper@42279: neuper@42279: "~~~~~ fun nxt_specif, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl))); neuper@42279: val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p; neuper@42279: "tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*) neuper@42279: neuper@42279: "~~~~~ fun some_spec, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec); neuper@42279: dI = e_domID; (*true*) neuper@42279: odI = "Build_Inverse_Z_Transform"; (*true*) neuper@42279: dI = "e_domID"; (*true*) neuper@42279: "~~~~~ after fun some_spec:"; neuper@42279: val (dI, pI, mI) = some_spec ospec spec; neuper@42279: "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*) neuper@42279: val thy = assoc_thy dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*) neuper@42279: neuper@55482: "----------- identified error in fun getTactic, string_of_thmI ---------------"; neuper@55482: "----------- identified error in fun getTactic, string_of_thmI ---------------"; neuper@55482: "----------- identified error in fun getTactic, string_of_thmI ---------------"; neuper@55482: reset_states (); neuper@55482: CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], neuper@55482: ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))]; neuper@55482: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; wneuper@59248: autoCalculate 1 (Step 1); wneuper@59248: autoCalculate 1 (Step 1); wneuper@59248: autoCalculate 1 (Step 1); neuper@55482: getTactic 1 ([1],Frm); (* norm_equation *) neuper@55482: interSteps 1 ([1],Res); neuper@55482: "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1],Res)); neuper@55482: val ((pt,p), tacis) = get_calc cI; neuper@55482: (not o is_interpos) ip = false; neuper@55482: val ip' = lev_pred' pt ip; neuper@55482: "~~~~~ fun detailstep, args:"; val (pt, (pos as (p,p_):pos')) = (pt, ip); neuper@55482: (* ^^^^^^^^^ not in test/../ *) neuper@55482: val nd = get_nd pt p neuper@55482: val cn = children nd; neuper@55482: null cn = false; neuper@55482: (is_rewset o (get_obj g_tac nd)) [(*root of nd*)] = true; neuper@55482: "~~~~~ fun detailrls, args:"; val (pt, (pos as (p,p_):pos')) = (pt, pos); neuper@55482: (* ^^^^^^^^^ only once in test/../solve.sml*) neuper@55482: val t = get_obj g_form pt p neuper@55482: val tac = get_obj g_tac pt p neuper@55482: val rls = (assoc_rls o rls_of) tac neuper@55482: val ctxt = get_ctxt pt pos neuper@55482: (*rls = Rls {calc = [], erls = ...*) neuper@55482: val is = init_istate tac t neuper@55482: (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"] neuper@55482: is wrong for simpl, but working ?!? *) neuper@55482: val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt) neuper@55482: val pos' = ((lev_on o lev_dn) p, Frm) neuper@55482: val thy = assoc_thy "Isac" neuper@55482: val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, ctxt) pos' pt; neuper@55482: (*val (_,_,(pt'',_)) = *)complete_solve CompleteSubpbl [] (pt',pos'); neuper@55482: (* ^^^^^^^^^^^^^^ in test/../mathengine.sml*) neuper@55482: (* in pt'': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")}, neuper@55482: ^^^^^^^^^^^^^^^^^^^^^^^^^^^*) wneuper@59279: "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)): ctree * pos')) = neuper@55482: (CompleteSubpbl, [], (pt',pos')); neuper@55482: p = ([], Res) = false; neuper@55482: member op = [Pbl,Met] p_ = false; neuper@55482: val (_, c', ptp') = nxt_solve_ ptp; neuper@55482: (* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")}, neuper@55482: ^^^^^^^^^^^^^^^^^^^^^^^^^^^*) neuper@55482: "~~~~~ fun nxt_solve_, args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp); neuper@55482: e_metID = get_obj g_metID pt (par_pblobj pt p) = false; neuper@55482: val thy' = get_obj g_domID pt (par_pblobj pt p); neuper@55482: val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; neuper@55482: val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; neuper@55482: (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*) wneuper@59279: "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), neuper@55482: (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); neuper@55482: l = [] = false; neuper@55482: nstep_up thy ptp sc E l Skip_ a v (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...) neuper@55482: BUT WE FIND IN THE CODE ABOVE IN next_tac:*) neuper@55482: ; neuper@55482: (*----------------------------------------------------------------------------------------------*) wneuper@59117: if string_of_thmI @{thm rnorm_equation_add} = "~ ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)" neuper@55482: then () else error "string_of_thmI changed"; wneuper@59117: if string_of_thm @{thm rnorm_equation_add} = "~ ?b =!= 0 ==> (?a = ?b) = (?a + - 1 * ?b = 0)" neuper@55482: then () else error "string_of_thm changed"; neuper@55482: (*----------------------------------------------------------------------------------------------*) neuper@55482: ; neuper@55482: (*SEARCH FOR THE ERROR WENT DOWN TO THE END OF THIS TEST, AND THEN UP TO HERE AGAIN*) neuper@55482: "~~~~~ fun nxt_solv, args:"; val (tac_, is, (pt, pos as (p,p_))) = (tac_, is, ptp); neuper@55482: val pos = neuper@55482: case pos of neuper@55482: (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*) neuper@55482: | (p, Res) => (lev_on p,Res) (*somewhere in script*) neuper@55482: | _ => pos; neuper@55482: generate1 (assoc_thy "Isac") tac_ is pos pt; neuper@55482: (* tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")}, neuper@55482: ^^^^^^^^^^^^^^^^^^^^^^^^^^^*) neuper@55482: "~~~~~ fun generate1, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))), neuper@55482: (is, ctxt), (p,p_), pt) = ((assoc_thy "Isac"), tac_, is, pos, pt); neuper@55482: val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f wneuper@59253: (Rewrite thm') (f',asm) Complete; neuper@55482: (* in pt: tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")}, neuper@55482: ^^^^^^^^^^^^^^^^^^^^^^^^^^^*) neuper@55482: "~~~~~ fun cappend_atomic, args:"; val (pt, p, ist_res, f, r, f', s) = wneuper@59253: (pt, p, (is, insert_assumptions asm ctxt), f, (Rewrite thm'), (f',asm), Complete); wneuper@59253: existpt p pt andalso is_empty_tac (get_obj g_tac pt p) = false; neuper@55482: apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm)); neuper@55482: apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c; wneuper@59279: (append_atomic p ist_res f r f' s) : ctree -> ctree; neuper@55482: ; neuper@55482: (* HERE THE ERROR OCCURED IN THE FIRST APPROACH neuper@55482: getTactic 1 ([1,1],Frm); syserror in getTactic <<<<<=========================*) neuper@55482: "~~~~~ fun getTactic, args:"; val (cI, (p:pos')) = (1, ([1,1],Frm)); neuper@55482: val ((pt,_),_) = get_calc cI neuper@55482: val (form, tac, asms) = pt_extract (pt, p) neuper@55482: val SOME ta = tac; neuper@55482: "~~~~~ fun gettacticOK2xml, args:"; val ((cI:calcID), tac) = (cI, ta); wneuper@59262: val i = 2; neuper@55482: "~~~~~ fun tac2xml, args:"; val (j, (Rewrite thm')) = (i, tac); wneuper@59252: "~~~~~ fun thm'2xml, args:"; val (j, ((ID, form) : thm'')) = ((j+i), thm'); neuper@55482: ID = "rnorm_equation_add"; neuper@55482: @{thm rnorm_equation_add}; wneuper@59253: (term2str o Thm.prop_of) form = "~ ?b =!= 0 ==> (?a = ?b) = (?a + -1 * ?b = 0)" neuper@55482: (*?!? should be "\ ?b =!= 0 \ (?a = ?b) = (?a + -1 * ?b = 0)"*) neuper@55482: (*thmstr2xml (j+i) form; neuper@55482: ERROR Undeclared constant: "Test.rnorm_equation_add" ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) neuper@55482: ; neuper@55482: show_pt pt; neuper@55482: (*[ neuper@55482: (([], Frm), solve (x + 1 = 2, x)), neuper@55482: (([1], Frm), x + 1 = 2), neuper@55482: (([1,1], Frm), x + 1 = 2), neuper@55482: (([1,1], Res), x + 1 + -1 * 2 = 0), neuper@55482: (([1], Res), x + 1 + -1 * 2 = 0), neuper@55482: (([2], Res), -1 + x = 0)] neuper@55482: neuper@55482: pt; --> tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")*) neuper@55482: neuper@55486: "----------- improved fun getTactic for interSteps and numeral calculations --"; neuper@55486: "----------- improved fun getTactic for interSteps and numeral calculations --"; neuper@55486: "----------- improved fun getTactic for interSteps and numeral calculations --"; neuper@55486: reset_states (); val cI = 1; neuper@55486: CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], neuper@55486: ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))]; neuper@55486: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalcHead; wneuper@59248: autoCalculate 1 (Step 1); neuper@55486: neuper@55486: val cs = get_calc cI (* we improve from the calcstate here [*] *); neuper@55486: val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *); neuper@55486: wneuper@59123: appendFormula 1 "x + 4 + -3 = 2" (*|> Future.join*); neuper@55486: interSteps 1 ([1],Res); (* already done by appendFormula, now showed to frontend *) neuper@55486: getTactic 1 ([1,1], Res); neuper@55486: (* sym_#add_Float ((~3,0), (0,0)) __ ((4,0), (0,0)) <<<<<================== to improve neuper@55486: 1 + x = -3 + (4 + x) *) neuper@55486: neuper@55486: val ((pt''',p'''), tacis''') = get_calc cI; neuper@55486: show_pt pt''' neuper@55486: (*[ neuper@55486: (([], Frm), solve (x + 1 = 2, x)), neuper@55486: (([1], Frm), x + 1 = 2), neuper@55486: (([1,1], Frm), x + 1 = 2), neuper@55486: (([1,1], Res), 1 + x = 2), neuper@55486: (([1,2], Res), -3 + (4 + x) = 2), neuper@55486: (([1,3], Res), -3 + (x + 4) = 2), neuper@55486: (([1,4], Res), x + 4 + -3 = 2), neuper@55486: (([1], Res), x + 4 + -3 = 2)]*) neuper@55486: ; neuper@55486: "~~~~~ fun appendFormula', args:"; val (cI, ifo) = (1, "x + 4 + -3 = 2"); neuper@55486: (* val cs = get_calc cI (* we improve from the calcstate here [*] *); neuper@55486: val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);*) neuper@55486: val ("ok", cs') = step pos cs; neuper@55486: (*val ("ok", (_, c, ptp as (_,p))) = *)inform cs' (encode ifo); neuper@55486: "~~~~~ fun inform, args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) = neuper@55486: (cs', (encode ifo)); neuper@55486: val SOME f_in = parse (assoc_thy "Isac") istr wneuper@59188: val f_in = Thm.term_of f_in neuper@55486: val f_succ = get_curr_formula (pt, pos); neuper@55486: f_succ = f_in = false; neuper@55486: val NONE = cas_input f_in neuper@55486: val pos_pred = lev_back' pos neuper@55486: (* f_pred ---"step pos cs"---> f_succ in appendFormula *) neuper@55486: val f_pred = get_curr_formula (pt, pos_pred); neuper@55486: (*val msg_calcstate' = *)compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*); neuper@55486: "~~~~~ fun compare_step, args:"; val (((tacis, c, ptp as (pt, pos as (p,p_)))), ifo) = neuper@55486: (([], [], (pt, pos_pred)), f_in); neuper@55486: val fo = neuper@55486: case p_ of neuper@55486: Frm => get_obj g_form pt p neuper@55486: | Res => (fst o (get_obj g_result pt)) p neuper@55486: | _ => e_term (*on PblObj is fo <> ifo*); neuper@55486: val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p)) neuper@55486: val {rew_ord, erls, rules, ...} = rep_rls nrls; neuper@55486: (*val (found, der) = *)concat_deriv rew_ord erls rules fo ifo; (*<---------------*) neuper@55486: "~~~~~ fun concat_deriv, args:"; val (rew_ord, erls, rules, fo, ifo) = neuper@55486: (rew_ord, erls, rules, fo, ifo); neuper@55486: fun derivat ([]:(term * rule * (term * term list)) list) = e_term neuper@55486: | derivat dt = (#1 o #3 o last_elem) dt neuper@55486: fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2 neuper@55486: (*val fod = *)make_deriv (Isac"") erls rules (snd rew_ord) NONE fo; neuper@55486: (*val ifod = *)make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo; neuper@55486: