Walther@60424: (* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2) wneuper@59553: Author: Walther Neuper 101001 wneuper@59553: (c) copyright due to license terms. wneuper@59553: wneuper@59553: Isac's tests are organised parallel to sources: wenzelm@60192: $ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC wneuper@59553: plus wenzelm@60217: $ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS wenzelm@60217: $ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality walther@59935: walther@59935: Note, that only the first error in a file is shown here. wneuper@59553: *) wneuper@59553: walther@59623: section \Notes on running tests\ walther@59623: subsection \Switch between running tests and updating code\ wneuper@59553: text \ walther@59623: Isac encapsulates code as much as possible in structures without open. walther@59623: This policy conflicts with those tests, which go into functions to details walther@59623: not declared in the signatures. walther@59623: \ walther@59623: subsection \Decide between running Test_Isac_Short.thy and Test_Isac.thy\ walther@59623: text \ walther@59623: Some tests raise exception Size raised (line 171 of "./basis/LibrarySupport.sml") walther@59623: if run in x86_64_32 mode of Poly/ML 5.8 (which is set as default). walther@59626: This exception can be avoided by ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences. walther@59626: A model is in the repository at ~~/etc/preferences. walther@59623: These preferences have drawbacks, however: walther@59623: * they claim more memory such that Isabelle instances canNOT run in parallel. walther@59623: * they do NOT reach Build_Isac.thy hanging in Build_Thydata.thy, see there. wneuper@59553: walther@59623: So default for Build_Isac.thy and for general testing is Test_Isac_Short.thy is x86_64_32 mode. walther@59623: From time to time full testing in Test_Isac.thy is recommended. For that purpose walther@59626: * set ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences. wneuper@59553: walther@59964: \\******************* don't forget to re-set defaults BEFORE updating code *******************// walther@59623: walther@59626: Note that Isabelle/jEdit re-generates the preferences file on shutdown, thus always use walther@59626: ***************** $ gedit ~/.isabelle/isabisac/etc/preferences & wneuper@59553: \ wneuper@59553: wneuper@59553: section \Run the tests\ wneuper@59553: text \ wneuper@59553: * say "OK" to the popup asking for theories to be loaded wneuper@59553: * watch the window for errors in the "imports" below wneuper@59553: \ wneuper@59553: walther@59623: theory Test_Isac_Short walther@59603: imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*) walther@59997: (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one walther@59997: and find out, which ML_file or *.thy causes an error (might be ONLY one). walther@59997: Also backup files (#* ) recognised by jEdit cause this trouble *) wneuper@59553: (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) Walther@60519: (* "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(*but ok in editor*)*) walther@60387: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics" Walther@60519: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo" wneuper@59553: (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform" wneuper@59553: ADDTESTS/------------------------------------------- see end of tests *) walther@60317: (*/~~~ these work directly from Pure, but create problems here .. wenzelm@60217: "$ISABELLE_ISAC_TEST/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *) wenzelm@60217: "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *) wenzelm@60217: "$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers_Cookbook.thy" (* Malformed theory import ?!? *) wenzelm@60217: "$ISABELLE_ISAC_TEST/Pure/Isar/Theory_Commands" (* Duplicate outer syntax command "ISAC" *) wenzelm@60217: "$ISABELLE_ISAC_TEST/Pure/Isar/Downto_Synchronized" (* re-defines / breaks structures !!! *) walther@60317: \~~~ .. these work independently, but create problems here *) wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers" wenzelm@60217: (**)"$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer/Try_Sledgehammer" wneuper@59553: (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*) wenzelm@60217: "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *) wenzelm@60217: "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *) wenzelm@60217: "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*) walther@60317: (** ) wneuper@59553: (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) wenzelm@60192: (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) Test_Isac_Short*) wenzelm@60192: (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) Test_Isac_Short*) wneuper@59556: (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*) walther@60317: ( **) Walther@60491: "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example" wneuper@59553: wneuper@59553: begin wneuper@59553: wenzelm@60240: declare [[ML_print_depth = 20]] wenzelm@60240: walther@59628: ML \open ML_System\ wneuper@59553: ML \ wneuper@59553: open Kernel; walther@59814: open Math_Engine; walther@59814: open Test_Code; CalcTreeTEST; walther@59848: open LItool; arguments_from_model; walther@59817: open Sub_Problem; walther@59823: open Fetch_Tacs; walther@59814: open Step walther@59659: open Env; walther@59814: open LI; scan_dn; walther@59617: open Istate; walther@59909: open Error_Pattern; walther@59909: open Error_Pattern_Def; walther@59977: open Specification; wneuper@59553: open Ctree; append_problem; walther@59696: open Pos; walther@59618: open Program; wneuper@59601: open Prog_Tac; walther@59603: open Tactical; walther@59603: open Prog_Expr; walther@59618: open Auto_Prog; rule2stac; wneuper@59600: open Input_Descript; walther@59971: open Specify; walther@59976: open Specify; walther@59763: open Step_Specify; walther@59749: open Step_Solve; walther@59763: open Step; wneuper@59553: open Solve; (* NONE *) wneuper@59577: open ContextC; transfer_asms_from_to; walther@59814: open Tactic; (* NONE *) walther@60126: open I_Model; walther@60126: open O_Model; walther@60126: open P_Model; (* NONE *) walther@59872: open Rewrite; walther@59878: open Eval; get_pair; wneuper@59553: open TermC; atomt; walther@59858: open Rule; walther@59878: open Rule_Set; Sequence; walther@59919: open Eval_Def walther@59854: open ThyC walther@59865: open ThmC_Def walther@59858: open ThmC walther@59857: open Rewrite_Ord walther@59861: open UnparseC wenzelm@60223: \ wneuper@59553: wneuper@59553: ML \ walther@59659: "~~~~~ fun xxx , args:"; val () = (); walther@59659: "~~~~~ and xxx , args:"; val () = (); walther@59814: "~~~~~ from fun xxx \fun yyy \fun zzz , return:"; val () = (); walther@60262: (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*); walther@59659: "xx" walther@60329: ^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**) walther@60329: \ ML \ (*//---------------- adhoc inserted ------------------------------------------------\\*) walther@59723: \ ML \ walther@60329: \ ML \ (*\\---------------- adhoc inserted ------------------------------------------------//*) walther@59723: \ walther@59723: ML \ walther@59723: \ ML \ wneuper@59553: \ ML \ walther@59851: \ ML \ walther@59851: \ ML \ wneuper@59553: \ wneuper@59553: wneuper@59553: ML \ wneuper@59553: KEStore_Elems.set_ref_thy @{theory}; wneuper@59553: (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*); wneuper@59553: \ wneuper@59553: wneuper@59553: section \trials with Isabelle's functions\ wneuper@59553: ML \"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\ Walther@60424: ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML" wenzelm@60217: ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML" wenzelm@60217: ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML" wenzelm@60217: ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML" wneuper@59553: ML \"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\ wneuper@59553: wneuper@59553: section \test ML Code of isac\ wneuper@59600: subsection \basic code first\ wneuper@59553: ML \"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\ walther@60413: ML_file "BaseDefinitions/base-definitions.sml" walther@59866: ML_file "BaseDefinitions/libraryC.sml" walther@59866: ML_file "BaseDefinitions/rule-def.sml" walther@59919: ML_file "BaseDefinitions/eval-def.sml" walther@59866: ML_file "BaseDefinitions/rewrite-order.sml" walther@59866: ML_file "BaseDefinitions/theoryC.sml" walther@59866: ML_file "BaseDefinitions/rule.sml" walther@59866: ML_file "BaseDefinitions/thmC-def.sml" walther@59866: ML_file "BaseDefinitions/error-fill-def.sml" walther@59866: ML_file "BaseDefinitions/rule-set.sml" walther@59892: ML_file "BaseDefinitions/check-unique.sml" walther@59932: (*called by Know_Store..*) walther@59866: ML_file "BaseDefinitions/calcelems.sml" walther@59866: ML_file "BaseDefinitions/termC.sml" walther@59912: ML_file "BaseDefinitions/substitution.sml" Walther@60424: ML_file "BaseDefinitions/contextC.sml" (*!!!!! sometimes evaluates if separated into ML blocks*) walther@59866: ML_file "BaseDefinitions/environment.sml" Walther@60424: (**)ML_file "BaseDefinitions/kestore.sml"(*setup in ADDTEST/accumulate-val/lucas_interpreter.sml*) wneuper@59553: (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- wneuper@59553: ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) walther@59932: walther@60317: ML_file "ProgLang/calculate.sml" walther@59964: ML_file "ProgLang/evaluate.sml" (* requires setup from calculate.thy *) walther@59633: ML_file "ProgLang/listC.sml" walther@59633: ML_file "ProgLang/prog_expr.sml" walther@59633: ML_file "ProgLang/program.sml" walther@59633: ML_file "ProgLang/prog_tac.sml" walther@59763: ML_file "ProgLang/tactical.sml" walther@60326: ML_file "ProgLang/auto_prog.sml" wneuper@59553: (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- wneuper@59553: ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) wneuper@59600: wneuper@59600: subsection \basic functionality on simple example first\ wneuper@59553: ML_file "Minisubpbl/000-comments.sml" wneuper@59553: ML_file "Minisubpbl/100-init-rootpbl.sml" wneuper@59553: ML_file "Minisubpbl/150-add-given.sml" walther@59781: ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml" wneuper@59553: ML_file "Minisubpbl/200-start-method.sml" wneuper@59553: ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml" walther@59722: ML_file "Minisubpbl/300-init-subpbl-NEXT_STEP.sml" wneuper@59553: ML_file "Minisubpbl/300-init-subpbl.sml" wneuper@59553: ML_file "Minisubpbl/400-start-meth-subpbl.sml" wneuper@59553: ML_file "Minisubpbl/450-Rewrite_Set_Inst.sml" walther@59722: ML_file "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml" wneuper@59553: ML_file "Minisubpbl/490-nxt-Check_Postcond.sml" wneuper@59553: ML_file "Minisubpbl/500-met-sub-to-root.sml" wneuper@59553: ML_file "Minisubpbl/530-error-Check_Elementwise.sml" walther@59781: ML_file "Minisubpbl/600-postcond-NEXT_STEP.sml" wneuper@59553: ML_file "Minisubpbl/600-postcond.sml" wneuper@59553: ML_file "Minisubpbl/700-interSteps.sml" walther@59820: ML_file "Minisubpbl/710-interSteps-short.sml" walther@59836: ML_file "Minisubpbl/790-complete-NEXT_STEP.sml" walther@59686: ML_file "Minisubpbl/790-complete.sml" walther@60340: ML_file "Minisubpbl/800-append-on-Frm.sml" wneuper@59600: wneuper@59600: subsection \further functionality alongside batch build sequence\ walther@59865: ML_file "MathEngBasic/thmC.sml" walther@60389: ML_file "MathEngBasic/rewrite.sml" walther@59728: ML_file "MathEngBasic/tactic.sml" Walther@60519: ML_file "MathEngBasic/ctree.sml" (*if red, get the file into a text buffer -- this might clear*) walther@59774: ML_file "MathEngBasic/calculation.sml" walther@59763: walther@59996: ML_file "Specify/formalise.sml" walther@59952: ML_file "Specify/o-model.sml" walther@59957: ML_file "Specify/i-model.sml" walther@59996: ML_file "Specify/pre-conditions.sml" walther@59996: ML_file "Specify/p-model.sml" walther@59985: ML_file "Specify/m-match.sml" walther@59967: ML_file "Specify/refine.sml" (* requires setup from refine.thy *) walther@59996: ML_file "Specify/test-out.sml" walther@59996: ML_file "Specify/specify-step.sml" walther@59996: ML_file "Specify/specification.sml" walther@59996: ML_file "Specify/cas-command.sml" walther@59996: ML_file "Specify/p-spec.sml" walther@59996: ML_file "Specify/specify.sml" walther@59800: ML_file "Specify/step-specify.sml" walther@59813: walther@59860: ML_file "Interpret/istate.sml" walther@59817: ML_file "Interpret/sub-problem.sml" walther@60389: ML_file "Interpret/error-pattern.sml" walther@59790: ML_file "Interpret/li-tool.sml" walther@60340: ML_file "Interpret/lucas-interpreter.sml" Walther@60530: ML \ Walther@60530: \ ML \ Walther@60530: \ ML \ Walther@60530: (* Title: "Interpret/lucas-interpreter.sml" Walther@60530: Author: Walther Neuper Walther@60530: (c) due to copyright terms Walther@60530: *) Walther@60530: Walther@60530: "-----------------------------------------------------------------------------------------------"; Walther@60530: "table of contents -----------------------------------------------------------------------------"; Walther@60530: "-----------------------------------------------------------------------------------------------"; Walther@60530: "----------- Take as 1st stac in program -------------------------------------------------------"; Walther@60530: "----------- re-build: fun locate_input_tactic -------------------------------------------------"; Walther@60530: "----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------"; Walther@60530: "----------- re-build: fun find_next_step, mini ------------------------------------------------"; Walther@60530: "----------- re-build: fun locate_input_term ---------------------------------------------------"; Walther@60530: "-----------------------------------------------------------------------------------------------"; Walther@60530: "-----------------------------------------------------------------------------------------------"; Walther@60530: "-----------------------------------------------------------------------------------------------"; Walther@60530: Walther@60530: "----------- Take as 1st stac in program -------------------------------------------------------"; Walther@60530: "----------- Take as 1st stac in program -------------------------------------------------------"; Walther@60530: "----------- Take as 1st stac in program -------------------------------------------------------"; Walther@60530: "compare --- Apply_Method with initial Take by Step.do_next --- in test/../step-solve ----------"; Walther@60530: val p = e_pos'; val c = []; Walther@60530: val (p,_,f,nxt,_,pt) = Walther@60530: CalcTreeTEST Walther@60530: [(["functionTerm (x \ 2 + 1)", "integrateBy x", "antiDerivative FF"], Walther@60530: ("Integrate", ["integrate", "function"], ["diff", "integration"]))]; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*) Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p c pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p c pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p c pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p c pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p c pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p c pt; Walther@60530: case nxt of (Apply_Method ["diff", "integration"]) => () Walther@60530: | _ => error "integrate.sml -- me method [diff,integration] -- spec"; Walther@60530: "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")"; Walther@60530: Walther@60530: "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt); Walther@60530: "~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p)); Walther@60530: val Applicable.Yes m = Step.check tac (pt, p); Walther@60530: (*if*) Tactic.for_specify' m; (*false*) Walther@60530: "~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp); Walther@60530: Walther@60530: "~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_)))) Walther@60530: = (m, (pt, pos)); Walther@60530: val {srls, ...} = MethodC.from_store mI; Walther@60530: val itms = case get_obj I pt p of Walther@60530: PblObj {meth=itms, ...} => itms Walther@60530: | _ => error "solve Apply_Method: uncovered case get_obj" Walther@60530: val thy' = get_obj g_domID pt p; Walther@60530: val thy = ThyC.get_theory thy'; Walther@60530: val srls = LItool.get_simplifier (pt, pos) Walther@60530: val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of Walther@60530: (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc) Walther@60530: | _ => error "solve Apply_Method: uncovered case init_pstate"; Walther@60530: (*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x \ 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)"; Walther@60530: val ini = LItool.implicit_take sc env; Walther@60530: val p = lev_dn p; Walther@60530: Walther@60530: val NONE = (*case*) ini (*of*); Walther@60530: val Next_Step (is', ctxt', m') = Walther@60530: LI.find_next_step sc (pt, (p, Res)) is ctxt; Walther@60530: (*+*)pstate2str (the_pstate is') = "([\"\n(f_f, x \ 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], empty, NONE, \nIntegral x \ 2 + 1 D x, ORundef, false, false)"; Walther@60530: val Safe_Step (_, _, Take' _) = (*case*) Walther@60530: locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*); Walther@60530: "~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac) Walther@60530: = (sc, (pt, (p, Res)), is', ctxt', m'); Walther@60530: Walther@60530: (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*); Walther@60530: "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...}))) Walther@60530: = ((prog, (cstate, ctxt, tac)), istate); Walther@60530: (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*); Walther@60530: Walther@60530: val Accept_Tac1 (_, _, Take' _) = Walther@60530: scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog); Walther@60530: "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\Let\, _) $ e $ (Abs (id, T, b)))) Walther@60530: = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog)); Walther@60530: Walther@60530: (*+*) if UnparseC.term e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed"; Walther@60530: Walther@60530: (*case*) Walther@60530: scan_dn1 xxx (ist |> path_down [L, R]) e (*of*); Walther@60530: (*======= end of scanning tacticals, a leaf =======*) Walther@60530: "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t) Walther@60530: = (xxx, (ist |> path_down [L, R]), e); Walther@60530: val (Program.Tac stac, a') = check_leaf "locate" ctxt eval (get_subst ist) t; Walther@60530: Walther@60530: Walther@60530: Walther@60530: "----------- re-build: fun locate_input_tactic -------------------------------------------------"; Walther@60530: "----------- re-build: fun locate_input_tactic -------------------------------------------------"; Walther@60530: "----------- re-build: fun locate_input_tactic -------------------------------------------------"; Walther@60530: val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"]; Walther@60530: val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"], Walther@60530: ["Test", "squ-equ-test-subpbl1"]); Walther@60530: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p [] pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p [] pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p [] pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p [] pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p [] pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p [] pt; Walther@60530: (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*); Walther@60530: (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*) Walther@60530: Walther@60530: (*//------------------ begin step into ------------------------------------------------------\\*) Walther@60530: (*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*) Walther@60530: Walther@60530: "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt); Walther@60530: Walther@60530: (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*) Walther@60530: Step.by_tactic tac (pt,p) (*of*); Walther@60530: "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p)); Walther@60530: val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*); Walther@60530: (*if*) Tactic.for_specify' m; (*false*) Walther@60530: Walther@60530: (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **) Walther@60530: Step_Solve.by_tactic m ptp; Walther@60530: "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp); Walther@60530: (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_)); Walther@60530: (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*) Walther@60530: val thy' = get_obj g_domID pt (par_pblobj pt p); Walther@60530: val (is, sc) = LItool.resume_prog thy' (p,p_) pt; Walther@60530: Walther@60530: locate_input_tactic sc (pt, po) (fst is) (snd is) m; Walther@60530: "~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac) Walther@60530: = (sc, (pt, po), (fst is), (snd is), m); Walther@60530: val srls = get_simplifier cstate; Walther@60530: Walther@60530: (** )val Accept_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **) Walther@60530: (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*); Walther@60530: "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...}))) Walther@60530: = ((prog, (cstate, ctxt, tac)), istate); Walther@60530: (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*); Walther@60530: Walther@60530: (** )val xxxxx_xx = ( **) Walther@60530: scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog); Walther@60530: "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\Let\, _) $ e $ (Abs (id, T, b)))) Walther@60530: = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog)); Walther@60530: Walther@60530: (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*); Walther@60530: "~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const (\<^const_name>\Chain\(*1*), _) $ e1 $ e2 $ a)) Walther@60530: = (xxx, (ist |> path_down [L, R]), e); Walther@60530: Walther@60530: (*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*); Walther@60530: "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\Try\(*2*), _) $ e)) Walther@60530: = (xxx, (ist |> path_down_form ([L, L, R], a)), e1); Walther@60530: Walther@60530: (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*); Walther@60530: (*======= end of scanning tacticals, a leaf =======*) Walther@60530: "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) Walther@60530: = (xxx, (ist |> path_down [R]), e); Walther@60530: val (Program.Tac stac, a') = Walther@60530: (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*); Walther@60530: val LItool.Associated (m, v', ctxt) = Walther@60530: (*case*) associate pt ctxt (m, stac) (*of*); Walther@60530: Walther@60530: Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*); Walther@60530: "~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx) Walther@60530: = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m)); Walther@60530: Walther@60530: "~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac') Walther@60530: = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m)); Walther@60530: (*if*) LibraryC.assoc (*then*); Walther@60530: Walther@60530: Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*); Walther@60530: "~~~~~ from locate_input_tactic to fun Step_Solve.by_tactic return:"; val Safe_Step (istate, ctxt, tac) Walther@60530: = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**); Walther@60530: Walther@60530: (*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *) Walther@60530: val (p'', _, _,pt') = Walther@60530: Step.add tac (istate, ctxt) (pt, (lev_on p, Pbl)); Walther@60530: (*in*) Walther@60530: Walther@60530: ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))], Walther@60530: [(*ctree NOT cut*)], (pt', p''))) (*return value*); Walther@60530: "~~~~~ from Step_Solve.by_tactic \ Step.by_tactic return:"; val ((msg, cs' : Calc.state_post)) Walther@60530: = ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )], Walther@60530: [(*ctree NOT cut*)], (pt', p''))); Walther@60530: Walther@60530: "~~~~~ from Step.by_tactic to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs'); Walther@60530: val (_, ts) = Walther@60530: (case Step.do_next p ((pt, Pos.e_pos'), []) of Walther@60530: ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts) Walther@60530: | ("helpless", _) => ("helpless: cannot propose tac", []) Walther@60530: | ("no-fmz-spec", _) => error "no-fmz-spec" Walther@60530: | ("end-of-calculation", (ts, _, _)) => ("", ts) Walther@60530: | _ => error "me: uncovered case") Walther@60530: handle ERROR msg => raise ERROR msg Walther@60530: val tac = Walther@60530: case ts of Walther@60530: tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end Walther@60530: | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac; Walther@60530: Walther@60530: (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt); Walther@60530: "~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt) Walther@60530: = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt); Walther@60530: Walther@60530: (*//--------------------- check results from modified me ----------------------------------\\*) Walther@60530: if p = ([2], Res) andalso Walther@60530: pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n" Walther@60530: then Walther@60530: (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => () Walther@60530: | _ => error "") Walther@60530: else error "check results from modified me CHANGED"; Walther@60530: (*\\--------------------- check results from modified me ----------------------------------//*) Walther@60530: Walther@60530: "~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**); Walther@60530: (*\\------------------ end step into --------------------------------------------------------//*) Walther@60530: Walther@60530: (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*) Walther@60530: (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*) Walther@60530: (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*) Walther@60530: (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*) Walther@60530: (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*) Walther@60530: (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*) Walther@60530: (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*) Walther@60530: (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*) Walther@60530: (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*) Walther@60530: (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*) Walther@60530: (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*) Walther@60530: (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*) Walther@60530: (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*) Walther@60530: (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*) Walther@60530: (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*) Walther@60530: Walther@60530: (*/--------------------- final test ----------------------------------\\*) Walther@60530: if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt = Walther@60530: ". ----- pblobj -----\n" ^ Walther@60530: "1. x + 1 = 2\n" ^ Walther@60530: "2. x + 1 + - 1 * 2 = 0\n" ^ Walther@60530: "3. ----- pblobj -----\n" ^ Walther@60530: "3.1. - 1 + x = 0\n" ^ Walther@60530: "3.2. x = 0 + - 1 * - 1\n" ^ Walther@60530: "4. [x = 1]\n" Walther@60530: then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1" Walther@60530: else error "re-build: fun locate_input_tactic changed 2"; Walther@60530: Walther@60530: Walther@60530: "----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------"; Walther@60530: "----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------"; Walther@60530: "----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------"; Walther@60530: (*cp from -- try fun applyTactics ------- *) Walther@60530: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", Walther@60530: "normalform N"], Walther@60530: ("PolyMinus",["plus_minus", "polynom", "vereinfachen"], Walther@60530: ["simplification", "for_polynomials", "with_minus"]))]; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; Walther@60530: (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*) Walther@60530: Walther@60530: (*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f Walther@60530: Walther@60530: (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*) Walther@60530: Walther@60530: (*+*)if map Tactic.input_to_string (specific_from_prog pt p) = Walther@60530: ["Rewrite (\"subtrahiere_x_plus_minus\", \"\?l is_num; ?m is_num\\n\ ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")", Walther@60530: "Rewrite (\"subtrahiere_x_minus_plus\", \"\?l is_num; ?m is_num\\n\ ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", Walther@60530: (*this is new since ThmC.numerals_to_Free.-----\\*) Walther@60530: "Calculate PLUS"] Walther@60530: then () else error "specific_from_prog ([1], Res) 1 CHANGED"; Walther@60530: (*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p); Walther@60530: Walther@60530: (*+*)if map Tactic.input_to_string (specific_from_prog pt p) = [ Walther@60530: "Rewrite (\"tausche_minus\", \"\?b ist_monom; ?a kleiner ?b\\n\ ?b - ?a = - ?a + ?b\")", Walther@60530: "Rewrite (\"subtrahiere_x_plus_minus\", \"\?l is_num; ?m is_num\\n\ ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")", Walther@60530: "Rewrite (\"subtrahiere_x_minus_plus\", \"\?l is_num; ?m is_num\\n\ ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", Walther@60530: (*this is new since ThmC.numerals_to_Free.-----\\*) Walther@60530: "Calculate PLUS", Walther@60530: (*this is new since ThmC.numerals_to_Free.-----//*) Walther@60530: "Calculate MINUS"] Walther@60530: then () else error "specific_from_prog ([1], Res) 2 CHANGED"; Walther@60530: (* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p); Walther@60530: Walther@60530: (*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*) Walther@60530: (**)val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*) Walther@60530: Step.by_tactic (hd (specific_from_prog pt p)) (pt, p); Walther@60530: "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (specific_from_prog pt p), (pt, p)); Walther@60530: val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*); Walther@60530: (*if*) Tactic.for_specify' m; (*false*) Walther@60530: Walther@60530: (**) val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*) Walther@60530: Step_Solve.by_tactic m (pt, p); Walther@60530: "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p)); Walther@60530: (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); Walther@60530: val thy' = get_obj g_domID pt (par_pblobj pt p); Walther@60530: val (is, sc) = LItool.resume_prog thy' (p,p_) pt; Walther@60530: Walther@60530: (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*); Walther@60530: "~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac) Walther@60530: = (sc, (pt, po), (fst is), (snd is), m); Walther@60530: val srls = LItool.get_simplifier cstate (*TODO: shift into Istate.T*); Walther@60530: Walther@60530: (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*); Walther@60530: "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...}))) Walther@60530: = ((prog, (cstate, ctxt, tac)), istate); Walther@60530: (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*); Walther@60530: Walther@60530: go_scan_up1 (prog, cctt) ist; Walther@60530: "~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...})) Walther@60530: = ((prog, cctt), ist); Walther@60530: (*if*) 1 < length path (*then*); Walther@60530: Walther@60530: scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog); Walther@60530: "~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\Try\(*2*), _) $ _)) Walther@60530: = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog)); Walther@60530: Walther@60530: go_scan_up1 pcct ist; Walther@60530: "~~~~~ and go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...})) Walther@60530: = (pcct, ist); Walther@60530: (*if*) 1 < length path (*then*); Walther@60530: Walther@60530: scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog); Walther@60530: "~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist, Walther@60530: (Const (\<^const_name>\Chain\(*3*), _) $ _ )) Walther@60530: = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog)); Walther@60530: val e2 = check_Seq_up ist prog Walther@60530: ; Walther@60530: (*case*) scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 (*of*); Walther@60530: "~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const (\<^const_name>\Chain\(*2*), _) $ e1 $ e2)) Walther@60530: = (cct, (ist |> path_up_down [R] |> set_or ORundef), e2); Walther@60530: Walther@60530: (*case*) scan_dn1 cct (ist |> path_down [L, R]) e1 (*of*); Walther@60530: "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\Try\(*2*), _) $ e)) Walther@60530: = (cct, (ist |> path_down [L, R]), e1); Walther@60530: Walther@60530: \ ML \ Walther@60530: (*case*) scan_dn1 cct (ist |> path_down [R]) e (*of*); Walther@60530: (*======= end of scanning tacticals, a leaf =======*) Walther@60530: "~~~~~ fun scan_dn1 , args:"; val ((cct as (_, ctxt, _)), (ist as {eval, ...}), t) Walther@60530: = (cct, (ist |> path_down [R]), e); Walther@60530: (*if*) Tactical.contained_in t (*else*); Walther@60530: val (Program.Tac prog_tac, form_arg) = (*case*) Walther@60530: LItool.check_leaf "locate" ctxt eval (get_subst ist) t (*of*); Walther@60530: Walther@60530: check_tac1 cct ist (prog_tac, form_arg); Walther@60530: "~~~~~ fun check_tac1 , args:"; val (((pt, p), ctxt, tac), (ist as {act_arg, or, ...}), (prog_tac, form_arg)) = Walther@60530: (cct, ist, (prog_tac, form_arg)); Walther@60530: val LItool.Not_Associated = (*case*) Walther@60530: LItool.associate pt ctxt (tac, prog_tac) (*of*); Walther@60530: val _(*ORundef*) = (*case*) or (*of*); Walther@60530: Walther@60530: (*+*)Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p); Walther@60530: Walther@60530: val Applicable.Yes m' = Walther@60530: (*case*) Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) (*of*); Walther@60530: Walther@60530: Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac) Walther@60530: (*return from check_tac1*); Walther@60530: "~~~~~ from fun check_tac1 \fun scan_dn1 \fun scan_dn1 \fun locate_input_tactic , return:"; val (Reject_Tac1 _) = Walther@60530: (Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)); Walther@60530: Walther@60530: val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f; Walther@60530: val ([3], Res) = p; Walther@60530: Walther@60530: Walther@60530: \ ML \ Walther@60530: "----------- re-build: fun find_next_step, mini ------------------------------------------------"; Walther@60530: "----------- re-build: fun find_next_step, mini ------------------------------------------------"; Walther@60530: "----------- re-build: fun find_next_step, mini ------------------------------------------------"; Walther@60530: val fmz = ["Term (a + a ::real)", "normalform n_n"]; Walther@60530: val (dI',pI',mI') = ("Poly",["polynomial", "simplification"],["simplification", "for_polynomials"]); Walther@60530: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; Walther@60530: (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*) Walther@60530: (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory "Poly"*) Walther@60530: (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["polynomial", "simplification"]*) Walther@60530: (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["simplification", "for_polynomials"]*) Walther@60530: (*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["simplification", "for_polynomials"]*) Walther@60530: (*[1], Res*)val (_, ([(tac'''''_', _, _)], _, (pt'''''_', p'''''_'))) = Walther@60530: Walther@60530: Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_Poly"*) Walther@60530: (*//------------------ go into 1 ------------------------------------------------------------\\*) Walther@60530: "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) Walther@60530: = (p, ((pt, e_pos'), [])); Walther@60530: val pIopt = Ctree.get_pblID (pt, ip); Walther@60530: (*if*) ip = ([], Res) (*else*); Walther@60530: val _ = (*case*) tacis (*of*); Walther@60530: val SOME _ = (*case*) pIopt (*of*); Walther@60530: (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*); Walther@60530: Walther@60530: val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) = Walther@60530: Step_Solve.do_next (pt, ip); Walther@60530: "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); Walther@60530: (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); Walther@60530: val thy' = get_obj g_domID pt (par_pblobj pt p); Walther@60530: val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; Walther@60530: Walther@60530: val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) = Walther@60530: LI.find_next_step sc (pt, pos) ist ctxt (*of*); Walther@60530: "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt) Walther@60530: = (sc, (pt, pos), ist, ctxt); Walther@60530: Walther@60530: val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) = Walther@60530: (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*); Walther@60530: "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) Walther@60530: = ((prog, (ptp, ctxt)), (Pstate ist)); Walther@60530: (*if*) path = [] (*then*); Walther@60530: Walther@60530: val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) = Walther@60530: scan_dn cc (trans_scan_dn ist) (Program.body_of prog); Walther@60530: "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t) Walther@60530: = (cc, (trans_scan_dn ist), (Program.body_of prog)); Walther@60530: (*if*) Tactical.contained_in t (*else*); Walther@60530: val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*); Walther@60530: Walther@60530: val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) = Walther@60530: check_tac cc ist (prog_tac, form_arg) (*return from xxx*); Walther@60530: "~~~~~ from fun scan_dn\fun scan_to_tactic\fun find_next_step, return:"; val (Accept_Tac (tac, ist, ctxt)) Walther@60530: = (check_tac cc ist (prog_tac, form_arg)); Walther@60530: Walther@60530: Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac) (*return from find_next_step*); Walther@60530: "~~~~~ from fun find_next_step\and do_next\fun zzz, return:"; val (Next_Step (ist, ctxt, tac)) Walther@60530: = (Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac)); Walther@60530: Walther@60530: LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp (*return from and do_next*); Walther@60530: "~~~~~ from and do_next\fun do_next\toplevel, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) Walther@60530: = (LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp); Walther@60530: (*\\------------------ end of go into 1 -----------------------------------------------------//*) Walther@60530: Walther@60530: (*[], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) = Walther@60530: Walther@60530: Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []);(* Check_Postcond ["polynomial", "simplification"]*) Walther@60530: (*//------------------ go into 2 ------------------------------------------------------------\\*) Walther@60530: "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) Walther@60530: = (p''''', ((pt''''', e_pos'), [])); Walther@60530: val pIopt = Ctree.get_pblID (pt, ip); Walther@60530: (*if*) ip = ([], Res) (*else*); Walther@60530: val _ = (*case*) tacis (*of*); Walther@60530: val SOME _ = (*case*) pIopt (*of*); Walther@60530: (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*); Walther@60530: Walther@60530: val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) = Walther@60530: Step_Solve.do_next (pt, ip); Walther@60530: "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); Walther@60530: (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); Walther@60530: val thy' = get_obj g_domID pt (par_pblobj pt p); Walther@60530: val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; Walther@60530: Walther@60530: (** )val End_Program (ist, tac) = Walther@60530: ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*); Walther@60530: "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt) Walther@60530: = (sc, (pt, pos), ist, ctxt); Walther@60530: Walther@60530: (* val Term_Val (Const (\<^const_name>\times\, _) $ Free ("2", _) $ Free ("a", _))*) Walther@60530: (** )val Term_Val prog_result = Walther@60530: ( *case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*); Walther@60530: "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) Walther@60530: = ((prog, (ptp, ctxt)), (Pstate ist)); Walther@60530: (*if*) path = [] (*else*); Walther@60530: Walther@60530: go_scan_up (prog, cc) (trans_scan_up ist |> set_found); Walther@60530: "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) Walther@60530: = ((prog, cc), (trans_scan_up ist(*|> set_found !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *))); Walther@60530: (*if*) path = [R] (*then*); Walther@60530: (*if*) found_accept = true (*then*); Walther@60530: Walther@60530: Term_Val act_arg (*return from go_scan_up*); Walther@60530: "~~~~~ from fun go_scan_up\fun scan_to_tactic, return:"; val (Term_Val prog_result) = (Term_Val act_arg); Walther@60530: Walther@60530: Term_Val prog_result (*return from scan_to_tactic*); Walther@60530: "~~~~~ from fun scan_to_tactic\fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result); Walther@60530: val (true, p', _) = (*case*) parent_node pt p (*of*); Walther@60530: val (_, pblID, _) = get_obj g_spec pt p'; Walther@60530: Walther@60530: End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result)) Walther@60530: (*return from find_next_step*); Walther@60530: "~~~~~ from fun find_next_step\and do_next\fun zzz, return:"; val (End_Program (ist, tac)) Walther@60530: = (End_Program (Pstate ist, Tactic.Check_Postcond' (pblID,prog_result))); Walther@60530: val _ = (*case*) tac (*of*); Walther@60530: Walther@60530: val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) Walther@60530: = LI.by_tactic tac (ist, ctxt) ptp (*return from and do_next*); Walther@60530: "~~~~~ from and do_next\top level, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) Walther@60530: = (LI.by_tactic tac (ist, ctxt) ptp); Walther@60530: (*\\------------------ end of go into 2 -----------------------------------------------------//*) Walther@60530: Walther@60530: (*[], Und*)val (msg, ([], _, (pt, p))) = Step.do_next p''''' ((pt''''', Pos.e_pos'), []);(**) Walther@60530: Walther@60530: Test_Tool.show_pt_tac pt; (*[ Walther@60530: ([], Frm), Simplify (a + a) Walther@60530: . . . . . . . . . . Apply_Method ["simplification", "for_polynomials"], Walther@60530: ([1], Frm), a + a Walther@60530: . . . . . . . . . . Rewrite_Set "norm_Poly", Walther@60530: ([1], Res), 2 * a Walther@60530: . . . . . . . . . . Check_Postcond ["polynomial", "simplification"], Walther@60530: ([], Res), 2 * a]*) Walther@60530: Walther@60530: (*/--- final test ---------------------------------------------------------------------------\\*) Walther@60530: val (res, asm) = (get_obj g_result pt (fst p)); Walther@60530: if UnparseC.term res = "2 * a" andalso map UnparseC.term asm = [] Walther@60530: andalso p = ([], Und) andalso msg = "end-of-calculation" Walther@60530: andalso pr_ctree pr_short pt = ". ----- pblobj -----\n1. a + a\n" Walther@60530: then Walther@60530: case tac''''' of Check_Postcond ["polynomial", "simplification"] => () Walther@60530: | _ => error "re-build: fun find_next_step, mini 1" Walther@60530: else error "re-build: fun find_next_step, mini 2" Walther@60530: Walther@60530: Walther@60530: "----------- re-build: fun locate_input_term ---------------------------------------------------"; Walther@60530: "----------- re-build: fun locate_input_term ---------------------------------------------------"; Walther@60530: "----------- re-build: fun locate_input_term ---------------------------------------------------"; Walther@60530: (*cp from inform.sml Walther@60530: ----------- appendFormula: on Res + late deriv ------------------------------------------------*) Walther@60530: val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"]; Walther@60530: val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"], Walther@60530: ["Test", "squ-equ-test-subpbl1"]); Walther@60530: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p [] pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p [] pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p [] pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p [] pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p [] pt; Walther@60530: val (p,_,f,nxt,_,pt) = me nxt p [] pt; Walther@60530: (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["Test", "squ-equ-test-subpbl1"]*); Walther@60530: Walther@60530: (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "norm_equation"*) Walther@60530: (*+*)if f2str f = "x + 1 = 2" then () else error "locate_input_term at ([1], Frm) CHANGED"; Walther@60530: Walther@60530: (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "Test_simplify"*) Walther@60530: (*+*)if f2str f = "x + 1 + - 1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED"; Walther@60530: Walther@60530: Test_Tool.show_pt_tac pt; (*[ Walther@60530: ([], Frm), solve (x + 1 = 2, x) Walther@60530: . . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"], Walther@60530: ([1], Frm), x + 1 = 2 Walther@60530: . . . . . . . . . . Rewrite_Set "norm_equation", Walther@60530: ([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond..ERROR*) Walther@60530: Walther@60530: \ ML \ Walther@60530: (*//---------- appendFormula 1 "x = 1" \ Step_Solve.inform \ LI.locate_input_term ----------\\*) Walther@60530: "~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: TermC.as_string) = ((**) "x = 1"); Walther@60530: val cs = (*get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)]) Walther@60530: val pos = (*get_pos cI 1*) p Walther@60530: Walther@60530: (*+*)val ptp''''' = (pt, p); Walther@60530: (*+*)if snd ptp''''' = ([1], Res) then () else error "old_cs changed"; Walther@60530: (*+*)Test_Tool.show_pt_tac pt; (*[ Walther@60530: (*+*)([], Frm), solve (x + 1 = 2, x) Walther@60530: (*+*). . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"], Walther@60530: (*+*)([1], Frm), x + 1 = 2 Walther@60530: (*+*). . . . . . . . . . Rewrite_Set "norm_equation", Walther@60530: (*+*)([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond*) Walther@60530: Walther@60530: val ("ok", cs' as (_, _, ptp')) = Walther@60530: (*case*) Step.do_next pos cs (*of*); Walther@60530: Walther@60530: \ ML \ Walther@60530: val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) = (*case*) Walther@60530: Step_Solve.by_term ptp' (encode ifo) (*of*); Walther@60530: \ ML \ Walther@60530: "~~~~~ fun by_term , args:"; val ((pt, pos as (p, _)), istr) Walther@60530: = (ptp', (encode ifo)); Walther@60530: \ ML \ Walther@60530: val SOME f_in = Walther@60530: (*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*); Walther@60530: val pos_pred = lev_back(*'*) pos Walther@60530: val f_pred = Ctree.get_curr_formula (pt, pos_pred); Walther@60530: val f_succ = Ctree.get_curr_formula (pt, pos); Walther@60530: (*if*) f_succ = f_in (*else*); Walther@60530: val NONE = Walther@60530: (*case*) CAS_Cmd.input f_in (*of*); Walther@60530: Walther@60530: \ ML \ Walther@60530: (*NEW*) LI.locate_input_term (pt, pos) f_in (*of*); Walther@60530: \ ML \ Walther@60530: "~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in); Walther@60530: val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*) Walther@60530: Walther@60530: \ ML \ Walther@60530: val ("ok", (_, _, cstate as (pt', pos'))) = Walther@60530: (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*); Walther@60530: \ ML \ Walther@60530: "~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = Walther@60530: (([], [], (pt, pos_pred)), tm); Walther@60530: val fo = Calc.current_formula ptp Walther@60530: val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) Walther@60530: val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls Walther@60530: \ ML \ Walther@60530: (*+*)Proof_Context.theory_of (Ctree.get_ctxt pt pos) (*Isac.Test OK!*) Walther@60530: \ ML \ Walther@60530: val (found, der) = Derive.steps (Ctree.get_ctxt pt pos) rew_ord erls rules fo ifo; (*<---------------*) Walther@60530: \ ML \ Walther@60530: (*if*) found (*else*); Walther@60530: (*if*) pos = ([], Pos.Res) (*else*); Walther@60530: \ ML \ Walther@60530: val msg_cs' as (_, (tacis, c', ptp)) = LI.do_next ptp; (*<---------------------*) Walther@60530: \ ML \ Walther@60530: (*case*) tacis (*of \ [(Rewrite_Set "Test_simplify",...*) :State_Steps.T; Walther@60530: \ ML \ Walther@60530: Walther@60530: (*+*) val ((input, tac, (pos, (ist, ctxt))) :: _) = tacis; Walther@60530: (*+*) input (*= Tactic.Rewrite_Set "Test_simplify"*); Walther@60530: (*+*) tac; Walther@60530: (*+*) pos = ([2], Res); Walther@60530: (*+*) ist; Walther@60530: (*+*) Proof_Context.theory_of ctxt (*.., Isac.Test*); Walther@60530: Walther@60530: \ ML \ Walther@60530: (*in*) compare_step (tacis, c @ c' (*@ c'' =c'BECAUSE OF | _ => msg_cs'*), ptp) ifo (*end*) Walther@60530: \ ML \ Walther@60530: "~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = Walther@60530: (([], [], (pt, pos_pred)), tm); Walther@60530: val fo = Calc.current_formula ptp Walther@60530: val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) Walther@60530: val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls Walther@60530: \ ML \ Walther@60530: val (found, der) = Derive.steps (Ctree.get_ctxt pt pos) rew_ord erls rules fo ifo; (*<---------------*) Walther@60530: \ ML \ Walther@60530: (*if*) found (*else*); Walther@60530: (*if*) pos = ([], Pos.Res) (*else*); Walther@60530: \ ML \ Walther@60530: val msg_cs' as (_, (tacis, c', ptp)) = LI.do_next ptp; (*<---------------------*) Walther@60530: \ ML \ Walther@60530: Walther@60530: (*+*) val ((input, tac, (pos, (ist, ctxt))) :: _) = tacis; Walther@60530: (*+*) input (*= Tactic.Rewrite_Set "Test_simplify"*); Walther@60530: \ ML \ Walther@60530: (*+*) tac; Walther@60530: (*+*) pos = ([2], Res); Walther@60530: (*+*) ist; Walther@60530: (*+*) Proof_Context.theory_of ctxt (*.., Isac.Test*); Walther@60530: Walther@60530: \ ML \ Walther@60530: \ ML \ Walther@60530: \ ML \ Walther@60530: Tactic.Apply_Method': MethodC.id * term option * Istate.T * Proof.context -> Tactic.T Walther@60530: \ ML \ Walther@60530: \ ML \ Walther@60530: \ ML \ Walther@60530: \ ML \ Walther@60530: \ ML \ Walther@60530: \ ML \ Walther@60530: \ ML \ Walther@60530: Walther@60530: \ ML \ (*----- original..*) Walther@60530: (*NEW*) Found_Step cstate (*return from locate_input_term*); Walther@60530: (*LI.Found_Step ( *)cstate(*, _(*istate*), _(*ctxt*))( *return from locate_input_term*); Walther@60530: "~~~~~ from fun locate_input_term\fun Step_Solve.by_term, return:"; val ("ok", (_(*use in DG !!!*), c, ptp as (_, p))) Walther@60530: = (("ok" , ([], [], cstate (* already contains istate, ctxt *)))); Walther@60530: Walther@60530: ("ok", ((*_ use in DG !!!,*) c, ptp(* as (_*), p))(*)*)(*return from Step_Solve.by_term*); Walther@60530: "~~~~~ from fun Step_Solve.by_term\(fun appendFormula)!toplevel, return:"; val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) Walther@60530: = ("ok", ([], [], ptp)); Walther@60530: Walther@60530: \ ML \ Walther@60530: (*fun me requires nxt...*) Walther@60530: Step.do_next p''''' (ptp''''', []); Walther@60530: val ("ok", ([(nxt'''''_' as Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _, Walther@60530: (pt'''''_', p'''''_'))) = Step.do_next p''''' (ptp''''', []) Walther@60530: (*\\---------- appendFormula 1 "x = 1" \ Step_Solve.inform \ LI.locate_input_term ----------//*) Walther@60530: Walther@60530: (*//----- REPLACED BY appendFormula 1 "x = 1" \ Step_Solve.inform \ LI.locate_input_term -----\\* ) Walther@60530: (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*) Walther@60530: (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*) Walther@60530: (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*) Walther@60530: (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*) Walther@60530: (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*) Walther@60530: (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*) Walther@60530: (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*) Walther@60530: (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*) Walther@60530: (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*) Walther@60530: (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*) Walther@60530: (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*) Walther@60530: (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*) Walther@60530: ( *\\----- REPLACED BY appendFormula 1 "x = 1" \ Step_Solve.inform \ LI.locate_input_term -----//*) Walther@60530: Walther@60530: (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_' p'''''_' [] pt'''''_'; (*nxt = Check_elementwise "Assumptions"*) Walther@60530: (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*) Walther@60530: (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*) Walther@60530: Walther@60530: \ ML \ Walther@60530: (*/--- final test ---------------------------------------------------------------------------\\*) Walther@60530: if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt = Walther@60530: ". ----- pblobj -----\n" ^ Walther@60530: "1. x + 1 = 2\n" ^ Walther@60530: "2. x + 1 + - 1 * 2 = 0\n" ^ Walther@60530: "3. ----- pblobj -----\n" ^ Walther@60530: "3.1. - 1 + x = 0\n" ^ Walther@60530: "3.2. x = 0 + - 1 * - 1\n" ^ Walther@60530: "3.2.1. x = 0 + - 1 * - 1\n" ^ Walther@60530: "3.2.2. x = 0 + 1\n" (*ATTENTION: see complete Calc below*) Walther@60530: then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_term CHANGED 1" Walther@60530: else error "re-build: fun locate_input_term CHANGED 2"; Walther@60530: Walther@60530: Test_Tool.show_pt_tac pt; (*[ Walther@60530: ([], Frm), solve (x + 1 = 2, x) Walther@60530: . . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"], Walther@60530: ([1], Frm), x + 1 = 2 Walther@60530: . . . . . . . . . . Rewrite_Set "norm_equation", Walther@60530: ([1], Res), x + 1 + - 1 * 2 = 0 Walther@60530: . . . . . . . . . . Rewrite_Set "Test_simplify", Walther@60530: ([2], Res), - 1 + x = 0 Walther@60530: . . . . . . . . . . Subproblem (Test, ["LINEAR", "univariate", "equation", "test"]), Walther@60530: ([3], Pbl), solve (- 1 + x = 0, x) Walther@60530: . . . . . . . . . . Apply_Method ["Test", "solve_linear"], Walther@60530: ([3,1], Frm), - 1 + x = 0 Walther@60530: . . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"), Walther@60530: ([3,1], Res), x = 0 + - 1 * - 1 Walther@60530: . . . . . . . . . . Derive Test_simplify, Walther@60530: ([3,2,1], Frm), x = 0 + - 1 * - 1 Walther@60530: . . . . . . . . . . Rewrite ("#: - 1 * - 1 = 1", "- 1 * - 1 = 1"), Walther@60530: ([3,2,1], Res), x = 0 + 1 Walther@60530: . . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"), Walther@60530: ([3,2,2], Res), x = 1 Walther@60530: . . . . . . . . . . Tactic.input_to_string not impl. for ?!, Walther@60530: ([3,2], Res), x = 1 Walther@60530: . . . . . . . . . . Check_Postcond ["LINEAR", "univariate", "equation", "test"], Walther@60530: ([3], Res), [x = 1] Walther@60530: . . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"], Walther@60530: ([], Res), [x = 1]]*) Walther@60530: \ ML \ Walther@60530: \ ML \ Walther@60530: \ walther@59751: ML_file "Interpret/step-solve.sml" walther@59751: walther@60326: ML_file "MathEngine/me-misc.sml" walther@59823: ML_file "MathEngine/fetch-tactics.sml" walther@60326: ML_file "MathEngine/solve.sml" walther@59763: ML_file "MathEngine/step.sml" walther@60340: ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*) walther@60326: ML_file "MathEngine/messages.sml" wneuper@59600: ML_file "MathEngine/states.sml" wneuper@59600: walther@59917: ML_file "BridgeLibisabelle/thy-present.sml" wneuper@59600: ML_file "BridgeLibisabelle/mathml.sml" (*part.*) walther@60277: ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml" wneuper@59600: ML_file "BridgeLibisabelle/thy-hierarchy.sml" Walther@60424: ML_file "BridgeLibisabelle/interface-xml.sml" (*TODO after 2009-2*) walther@60389: ML_file "BridgeLibisabelle/interface.sml" walther@60044: ML_file "BridgeJEdit/parseC.sml" walther@60146: ML_file "BridgeJEdit/preliminary.sml" Walther@60465: ML_file "BridgeJEdit/vscode-example.sml" walther@60044: wneuper@59553: ML_file "Knowledge/delete.sml" wneuper@59553: ML_file "Knowledge/descript.sml" wneuper@59553: ML_file "Knowledge/simplify.sml" Walther@60530: ML \ Walther@60530: \ ML \ Walther@60530: \ ML \ Walther@60530: \ ML \ Walther@60530: \ ML \ Walther@60530: \ walther@60340: ML_file "Knowledge/poly-1.sml" walther@60329: (*ML_file "Knowledge/poly-2.sml" Test_Isac_Short*) wneuper@59553: ML_file "Knowledge/gcd_poly_ml.sml" walther@60329: ML_file "Knowledge/rational-1.sml" walther@60329: (*ML_file "Knowledge/rational-2.sml" Test_Isac_Short*) Walther@60519: ML_file "Knowledge/equation.sml" walther@60384: ML_file "Knowledge/root.sml" wneuper@59553: ML_file "Knowledge/lineq.sml" wneuper@59553: (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *) walther@59628: (*ML_file "Knowledge/rateq.sml" some complicated equations not recovered----Test_Isac_Short*) walther@60389: ML_file "Knowledge/rootrat.sml" wneuper@59553: ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *) walther@59628: (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*) walther@60393: ML_file "Knowledge/polyeq-1.sml" walther@60393: (*ML_file "Knowledge/polyeq-2.sml" Test_Isac_Short*) wneuper@59553: (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *) wneuper@59553: ML_file "Knowledge/calculus.sml" wneuper@59553: ML_file "Knowledge/trig.sml" wneuper@59553: (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*) walther@60350: ML_file "Knowledge/diff.sml" walther@60350: ML_file "Knowledge/integrate.sml" walther@60347: ML_file "Knowledge/eqsystem-1.sml" walther@60395: ML_file "Knowledge/eqsystem-2.sml" walther@59996: ML_file "Knowledge/test.sml" wneuper@59553: ML_file "Knowledge/polyminus.sml" wneuper@59553: ML_file "Knowledge/vect.sml" Walther@60458: ML_file "Knowledge/diff-app.sml" (* postponed to dev. specification | TP-prog. *) walther@60396: ML_file "Knowledge/biegelinie-1.sml" walther@59628: (*ML_file "Knowledge/biegelinie-2.sml" Test_Isac_Short*) walther@59628: (*ML_file "Knowledge/biegelinie-3.sml" Test_Isac_Short*) walther@60398: ML_file "Knowledge/biegelinie-4.sml" walther@60326: ML_file "Knowledge/algein.sml" wneuper@59553: ML_file "Knowledge/diophanteq.sml" walther@59628: (*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*) wneuper@59553: ML_file "Knowledge/inssort.sml" wneuper@59553: ML_file "Knowledge/isac.sml" wneuper@59553: ML_file "Knowledge/build_thydata.sml" wneuper@59600: walther@59814: ML_file "Test_Code/test-code.sml" walther@59814: walther@59617: section \further tests additional to src/.. files\ walther@60399: ML_file "BridgeLibisabelle/use-cases.sml" wneuper@59600: wneuper@59553: ML \"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\ wneuper@59553: ML \"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\ wneuper@59553: ML \"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\ walther@60262: ML \ walther@60262: \ ML \ wneuper@59561: \ ML \ walther@59804: \ ML \ walther@59804: \ ML \ wneuper@59561: \ wneuper@59553: wneuper@59553: section \history of tests\ wneuper@59553: text \ wneuper@59553: Systematic regression tests have been introduced to isac development in 2003. wneuper@59553: Sanity of the regression tests suffers from updates following Isabelle development, wneuper@59553: which mostly exceeded the resources available in isac's development. wneuper@59553: wneuper@59553: The survey below shall support to efficiently use the tests for isac wneuper@59553: on different Isabelle versions. Conclusion in most cases will be: wneuper@59553: wneuper@59553: !!! Use most recent tests or go back to the old notebook wneuper@59553: with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! wneuper@59553: \ wneuper@59553: wneuper@59553: wneuper@59553: subsection \isac on Isabelle2017\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: * Add further signatures, separate structures and cleanup respective files. wneuper@59553: * Show feasibility of moving Isac programs to partial_function, i.e. to the function package. wneuper@59553: * Clean theory dependencies. wneuper@59553: * Start preparing shift from isac-java to Isabelle/jEdit. wneuper@59553: \ wneuper@59553: subsubsection \State of tests: unchanged\ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: last changeset with Test_Isac 925fef0f4c81 wneuper@59553: first changeset with Test_Isac bbb414976dfe wneuper@59553: \ wneuper@59553: wneuper@59553: subsection \isac on Isabelle2015\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: * Add signatures from top of thy-hierarchy down to Interpret (not ProgLang). wneuper@59553: This complicates Test_Isac, see "Prepare running tests" above. wneuper@59553: * Remove TTY interface. wneuper@59553: * Re-activate insertion sort. wneuper@59553: \ wneuper@59553: subsubsection \State of tests: unchanged\ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: last changeset with Test_Isac 2f1b2854927a wneuper@59553: first changeset with Test_Isac ??? wneuper@59553: \ wneuper@59553: wneuper@59553: subsection \isac on Isabelle2014\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: migration from "isabelle tty" --> libisabelle wneuper@59553: \ wneuper@59553: Walther@60424: subsection \isac on Isabelle2013-2\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: reactivated context_thy wneuper@59553: \ wneuper@59553: subsubsection \State of tests\ wneuper@59553: text \ wneuper@59553: TODO wneuper@59553: \ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: TODO wneuper@59553: : Walther@60424: : isac on Isablle2013-2 wneuper@59553: : wneuper@59553: Changeset: 55318 (03826ceb24da) merged wneuper@59553: User: Walther Neuper Walther@60424: Date: 2013-12-12 14:27:37 +0100 (7 minutes) wneuper@59553: \ wneuper@59553: Walther@60424: subsection \isac on Isabelle2013-1\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ Walther@60424: Isabelle2013-1 was replaced within a few weeks due to problems with the document model; wneuper@59553: no significant development steps for ISAC. wneuper@59553: \ wneuper@59553: subsubsection \State of tests\ wneuper@59553: text \ wneuper@59553: See points in subsection "isac on Isabelle2011", "State of tests". wneuper@59553: \ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy wneuper@59553: User: Walther Neuper Walther@60424: Date: 2013-12-03 18:13:31 +0100 (8 days) wneuper@59553: : Walther@60424: : isac on Isablle2013-1 wneuper@59553: : Walther@60424: Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect wneuper@59553: User: Walther Neuper Walther@60424: Date: 2013-11-21 18:12:17 +0100 (2 weeks) wneuper@59553: wneuper@59553: \ wneuper@59553: wneuper@59553: subsection \isac on Isabelle2013\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: # Oct.13: replaced "axioms" by "axiomatization" wneuper@59553: # Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref wneuper@59553: # Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into wneuper@59553: simplification of multivariate rationals (without improving the rulesets involved). wneuper@59553: \ wneuper@59553: subsubsection \Run tests\ wneuper@59553: text \ Walther@60424: Is standard now; this subsection will be discontinued under Isabelle2013-1 wneuper@59553: \ wneuper@59553: subsubsection \State of tests\ wneuper@59553: text \ wneuper@59553: See points in subsection "isac on Isabelle2011", "State of tests". wneuper@59553: # re-activated listC.sml wneuper@59553: \ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref" wneuper@59553: User: Mathias Lehnfeld wneuper@59553: Date: Tue Nov 19 22:23:30 2013 +0000 wneuper@59553: : wneuper@59553: : isac on Isablle2013 wneuper@59553: : wneuper@59553: Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013 wneuper@59553: User: Walther Neuper Walther@60424: Date: 2013-07-15 08:28:50 +0200 (4 weeks) wneuper@59553: \ wneuper@59553: wneuper@59553: subsection \isac on Isabelle2012\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: isac on Isabelle2012 is considered just a transitional stage wneuper@59553: within the update from Isabelle2011 to Isabelle2013; thus no further development of isac; wneuper@59553: For considerations on the transition see wenzelm@60192: $ISABELLE_ISAC/Knowledge/Build_Thydata/thy, section "updating isac..". wneuper@59553: \ wneuper@59553: subsubsection \Run tests\ wneuper@59553: text \ wneuper@59553: $ cd /usr/local/isabisac12/ wneuper@59553: $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy wneuper@59553: $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy wneuper@59553: \ wneuper@59553: subsubsection \State of tests\ wneuper@59553: text \ wneuper@59553: At least the tests from isac on Isabelle2011 run again. wneuper@59553: However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling wneuper@59553: in parallel with evaluation. wneuper@59553: wneuper@59553: Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant) Walther@60424: yields 69 hits, some of which were already present before Isabelle2002-->2009-2 wneuper@59553: (i.e. on the old notebook from 2002). wneuper@59553: wneuper@59553: Now many tests with (*...=== inhibit exn ...*) give a reason or at least the origin: wneuper@59553: # === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy wneuper@59553: # === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002 Walther@60424: # === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002 wneuper@59553: Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml. wneuper@59553: wneuper@59553: Some tests have been re-activated (e.g. error patterns, fill patterns). wneuper@59553: \ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012 wneuper@59553: User: Walther Neuper Walther@60424: Date: 2013-07-11 16:58:31 +0200 (4 weeks) wneuper@59553: : wneuper@59553: : isac on Isablle2012 wneuper@59553: : wneuper@59553: Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012 wneuper@59553: User: Walther Neuper Walther@60424: Date: 2012-09-24 18:35:13 +0200 (8 months) wneuper@59553: ------------------------------------------------------------------------------ wneuper@59553: Changeset: 48756 (7443906996a8) merged wneuper@59553: User: Walther Neuper Walther@60424: Date: 2012-09-24 18:15:49 +0200 (8 months) wneuper@59553: \ wneuper@59553: wneuper@59553: subsection \isac on Isabelle2011\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: isac's mathematics engine has been extended by two developments: wneuper@59553: (1) Isabelle's contexts were introduced by Mathias Lehnfeld wneuper@59553: (2) Z_Transform was introduced by Jan Rocnik, which revealed wneuper@59553: further errors introduced by (1). wneuper@59553: (3) "error patterns" were introduced by Gabriella Daroczy wneuper@59553: Regressions tests have been added for all of these. wneuper@59553: \ wneuper@59553: subsubsection \Run tests\ wneuper@59553: text \ wneuper@59553: $ cd /usr/local/isabisac11/ wneuper@59553: $ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy wneuper@59553: $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy wneuper@59553: \ wneuper@59553: subsubsection \State of tests\ wneuper@59553: text \ wneuper@59553: Systematic efforts outcommented less significant tests by (*...=== inhibit exn ...*) wneuper@59553: and sometimes give reasons for failing tests. wneuper@59553: (*...=== inhibit exn AK...*) was done by Alexander Kargl; this is reliable wneuper@59553: work, some of which couldn't be revised (and renamed) by WN and thus survived some time. wneuper@59553: wneuper@59553: The most signification tests (in particular Frontend/interface.sml) run, wneuper@59553: however, many "error in kernel" are not caught by an exception. wneuper@59553: ------------------------------------------------------------------------------ wneuper@59553: After the changeset below Test_Isac worked with check_unsynchronized_ref (): wneuper@59553: ------------------------------------------------------------------------------ wneuper@59553: Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref wneuper@59553: User: Walther Neuper wneuper@59553: Date: 2012-08-06 10:38:11 +0200 (11 months) wneuper@59553: wneuper@59553: wneuper@59553: The list below records TODOs while producing an ISAC kernel for wneuper@59553: gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING Walther@60424: (so to be resumed with Isabelle2013-1): wneuper@59553: ############## WNxxxxxx.TODO can be found in sources ############## wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN111013.TODO: lots of cleanup/removal in test/../Test.thy wneuper@59553: -------------------------------------------------------------------------------- walther@59845: WN111013.TODO: remove concept around "fun implicit_take", lots of troubles with wneuper@59553: this special case (see) --- why not nxt = Model_Problem here ? --- wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/ wneuper@59553: ... FIRST redesign wneuper@59553: # simplify_* , *_simp_* wneuper@59553: # norm_* wneuper@59553: # calc_* , calculate_* ... require iteration over all rls ... wneuper@59553: ... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE ! wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!! wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120314 changeset a393bb9f5e9f drops root equations. wneuper@59553: see test/Tools/isac/Knowledge/rootrateq.sml wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120317.TODO changeset 977788dfed26 dropped rateq: wneuper@59553: # test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002 Walther@60424: # test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...: wneuper@59553: investigation Check_elementwise stopped due to too much effort finding out, wneuper@59553: why Check_elementwise worked in 2002 in spite of the error. wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120317.TODO found by test --- interSteps for Schalk 299a --- that wneuper@59553: NO test with 'interSteps' is checked properly (with exn on changed behaviour) wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has wneuper@59553: a newly outcommented test where rewrite_set_ make_polynomial --> NONE wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120320.TODO check-improve rlsthmsNOTisac: wneuper@59553: DONE make test --- old compute rlsthmsNOTisac by eq_thmI' Walther@60424: DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy wneuper@59553: FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab wneuper@59553: # mark twice thms (in isac + (later) in Isabelle) in Isac.thy wneuper@59553: -------------------------------------------------------------------------------- Walther@60424: WN120320.TODO rlsthmsNOTisac: replace twice thms ^ wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test wneuper@59553: --- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac. wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120321.TODO rearrange theories: wneuper@59553: Knowledge wneuper@59553: : walther@59603: Prog_Expr.thy walther@60125: ///Input_Descript.thy --> ProgLang walther@59603: Delete.thy <--- first_Knowledge_thy (*mv to Prog_Expr.thy*) wneuper@59553: ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy wneuper@59553: Interpret.thy are generated (simplifies xml structure for theories) wneuper@59585: Program.thy wneuper@59553: Tools.thy wneuper@59553: ListC.thy <--- first_Proglang_thy wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify wneuper@59553: EXN "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)" wneuper@59553: broken during work on thy-hierarchy wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see wneuper@59553: test --- the_hier (get_thes ()) (collect_thydata ())--- wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_ wneuper@59553: !!add mutual crossreferences to ?fun headline??? where the same has to be done: wneuper@59553: !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!! wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120411 scanning html representation of newly generated knowledge: wneuper@59553: * thy: wneuper@59553: ** Theorems: only "Proof of the theorem" (correct!) wneuper@59553: and "(c) isac-team (math-autor)" wneuper@59553: ** Rulesets: only "Identifier:///" wneuper@59553: and "(c) isac-team (math-autor)" wneuper@59553: ** IsacKnowledge: link to dependency graph (which needs to be created first) wneuper@59553: ** IsacScripts --> ProgramLanguage wneuper@59553: *** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen wneuper@59553: wneuper@59553: * pbl: OK !?! wneuper@59553: * met: OK !?! wneuper@59553: * exp: wneuper@59553: ** Z-Transform is missing !!! wneuper@59553: ** type-constraints !!! wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: WN120417: merging xmldata revealed: wneuper@59553: ..............NEWLY generated:........................................ wneuper@59553: wneuper@59553: thy_isab_Fun-thm-o_apply wneuper@59553: wneuper@59553: Isabelle wneuper@59553: Fun wneuper@59553: Theorems wneuper@59553: o_apply wneuper@59553: wneuper@59553: wneuper@59553: (?f o ?g) ?x = ?f (?g ?x) wneuper@59553: wneuper@59553: wneuper@59553: Proof of the theorem wneuper@59553: http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: Isabelle team, TU Munich wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: ..............OLD FORMAT:............................................. wneuper@59553: wneuper@59553: thy_isab_Fun-thm-o_apply wneuper@59553: wneuper@59553: Isabelle wneuper@59553: Fun wneuper@59553: Theorems wneuper@59553: o_apply wneuper@59553: wneuper@59553: wneuper@59553: o_apply wneuper@59553: wneuper@59553: (?f o ?g) ?x = ?f (?g ?x) wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: Proof of the theorem wneuper@59553: http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: Isabelle team, TU Munich wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: wneuper@59553: -------------------------------------------------------------------------------- wneuper@59553: \ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: isac development was done between these changesets: wneuper@59553: ------------------------------------------------------------------------------ wneuper@59553: Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files wneuper@59553: User: Walther Neuper Walther@60424: Date: 2012-09-24 16:39:30 +0200 (8 months) wneuper@59553: : wneuper@59553: : isac on Isablle2011 wneuper@59553: : wneuper@59553: Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011 wneuper@59553: Branch: decompose-isar wneuper@59553: User: Walther Neuper Walther@60424: Date: 2011-02-25 13:04:56 +0100 (2011-02-25) wneuper@59553: ------------------------------------------------------------------------------ wneuper@59553: \ wneuper@59553: Walther@60424: subsection \isac on Isabelle2009-2\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg. wneuper@59553: The update was painful (bridging 7 years of Isabelle development) and cut short wneuper@59553: due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and wneuper@59553: going on to Isabelle2011 although most of the tests did not run. wneuper@59553: \ wneuper@59553: subsubsection \Run tests\ wneuper@59553: text \ wneuper@59553: WN131021 this is broken by installation of Isabelle2011/12/13, wneuper@59553: because all these write their binaries to ~/.isabelle/heaps/.. wneuper@59553: Walther@60424: $ cd /usr/local/isabisac09-2/ wneuper@59553: $ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy wneuper@59553: $ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy wneuper@59553: NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!! wneuper@59553: \ wneuper@59553: subsubsection \State of tests\ wneuper@59553: text \ Walther@60424: Most tests are broken by the update from Isabelle2002 to Isabelle2009-2. wneuper@59553: \ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: isac development was done between these changesets: wneuper@59553: ------------------------------------------------------------------------------ wneuper@59553: Changeset: 38115 (940a5feea094) Little improvements of isac-plugin wneuper@59553: Branch: decompose-isar wneuper@59553: User: Marco Steger wneuper@59553: Date: 2011-02-06 18:30:28 +0100 (2011-02-06) wneuper@59553: : Walther@60424: : isac on Isablle2009-2 wneuper@59553: : Walther@60424: Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2 Walther@60424: Branch: isac-from-Isabelle2009-2 wneuper@59553: User: Walther Neuper Walther@60424: Date: 2010-07-21 09:59:35 +0200 (2010-07-21) wneuper@59553: ------------------------------------------------------------------------------ wneuper@59553: \ wneuper@59553: wneuper@59553: subsection \isac on Isabelle2002\ wneuper@59553: subsubsection \Summary of development\ wneuper@59553: text \ wneuper@59553: From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern") wneuper@59553: of isac's mathematics engine has been implemented. wneuper@59553: \ wneuper@59553: subsubsection \Run tests\ wneuper@59553: subsubsection \State of tests\ wneuper@59553: text \ wneuper@59553: All tests work on an old notebook (the right PolyML coudn't be upgraded to more wneuper@59553: recent Linux versions) wneuper@59553: \ wneuper@59553: subsubsection \Changesets of begin and end\ wneuper@59553: text \ wneuper@59553: Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS; wneuper@59553: see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial. wneuper@59553: \ wneuper@59553: wneuper@59553: end wneuper@59553: (*========== inhibit exn 130719 Isabelle2013 =================================== wneuper@59553: ============ inhibit exn 130719 Isabelle2013 =================================*) wneuper@59553: wneuper@59553: (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. wneuper@59553: -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) wneuper@59553: