1.1 --- a/TODO.md Thu Sep 29 18:02:10 2022 +0200
1.2 +++ b/TODO.md Fri Oct 07 20:46:48 2022 +0200
1.3 @@ -65,7 +65,7 @@
1.4 * WN: follow up 5: cleanup
1.5 follow up 6: ctxt_user at init Example mimiced by CalcTreeTest @{context}
1.6 Thus eliminate use of Thy_Info.get_theory
1.7 - follow up 7: ANSWER ?How represent items, which have not yet been input? IN VSCode_Example.thy WITH "__"
1.8 + follow up 7: ANSWER: represent items, which have not yet been input IN VSCode_Example.thy WITH "__"
1.9
1.10 * WN: improve naming in refine.sml, m-match.sml
1.11 * WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store›
2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Sep 29 18:02:10 2022 +0200
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Fri Oct 07 20:46:48 2022 +0200
2.3 @@ -498,8 +498,8 @@
2.4
2.5 fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
2.6 let
2.7 - val (itms, oris, probl, ctxt) = case get_obj I pt p of
2.8 - PblObj {meth = itms, origin = (oris, _, _), probl, ctxt, ...} => (itms, oris, probl, ctxt)
2.9 + val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
2.10 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
2.11 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
2.12 val {ppc, ...} = MethodC.from_store_PIDE ctxt mI;
2.13 val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
2.14 @@ -551,8 +551,8 @@
2.15 val {scr, ...} = MethodC.from_store_PIDE ctxt (get_obj g_metID pt parent_pos);
2.16 val prog_res =
2.17 case find_next_step scr (pt, pos) sub_ist sub_ctxt of
2.18 - (*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
2.19 - |(*OLD*) End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res
2.20 + Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
2.21 + | End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res
2.22 | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)
2.23 in
2.24 if parent_pos = [] then
3.1 --- a/src/Tools/isac/MathEngBasic/method.sml Thu Sep 29 18:02:10 2022 +0200
3.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Fri Oct 07 20:46:48 2022 +0200
3.3 @@ -168,7 +168,7 @@
3.4
3.5 fun from_store_PIDE ctxt id =
3.6 let
3.7 - val pbl = Store.get (get_mets ()) id (rev id)
3.8 + val pbl = Store.get (get_mets ()) id id
3.9 in adapt_to_type ctxt pbl end
3.10 handle ERROR _ =>
3.11 raise error ("*** ERROR MethodC.from_store thy " ^ strs2str id ^ " not found");
4.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Thu Sep 29 18:02:10 2022 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Fri Oct 07 20:46:48 2022 +0200
4.3 @@ -439,7 +439,6 @@
4.4 | res (Or_to_List' (_, t)) = (t, [])
4.5 | res m = raise ERROR ("result: not impl.for " ^ string_of m)
4.6
4.7 -(*fun result m = (fst o res) m; TODO*)
4.8 fun result tac = (fst o res) tac;
4.9 fun creates_assms tac = (snd o res) tac;
4.10
5.1 --- a/src/Tools/isac/Specify/specify.sml Thu Sep 29 18:02:10 2022 +0200
5.2 +++ b/src/Tools/isac/Specify/specify.sml Fri Oct 07 20:46:48 2022 +0200
5.3 @@ -73,7 +73,7 @@
5.4
5.5 (** find a next step in the specify-phase **)
5.6 (*
5.7 - here should be mutual recursion between for_problem and for_method
5.8 + here should be mutual recursion between for_problem_PIDE ctxt and for_method
5.9 *)
5.10 fun for_problem_PIDE ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =
5.11 let
5.12 @@ -137,7 +137,7 @@
5.13 on finding a next step switching from problem to method or vice versa is possible,
5.14 because the user is free to switch and edit the respective models independently.
5.15 TODO: this free switch is NOT yet implemented; e.g.
5.16 - preok is relevant for problem + method, i.e. in for_problem + for_method
5.17 + preok is relevant for problem + method, i.e. in for_problem_PIDE ctxt + for_method
5.18 *)
5.19 fun find_next_step (pt, pos as (_, p_)) =
5.20 let
6.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy Thu Sep 29 18:02:10 2022 +0200
6.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy Fri Oct 07 20:46:48 2022 +0200
6.3 @@ -3,7 +3,7 @@
6.4 (c) due to copyright terms
6.5
6.6 this theory is evaluated BEFORE Test_Isac.thy opens structures.
6.7 - So, if you encounter errors here, first fix them in $ISABELLE_ISAC_TEST/Tools/isac/Minimsubpbl/* *)
6.8 + So, if you encounter errors here, first fix them in $ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/* *)
6.9
6.10 theory All_Ctxt imports Isac.Build_Isac
6.11 begin
6.12 @@ -98,6 +98,9 @@
6.13
6.14 ML \<open>
6.15 \<close> ML \<open>
6.16 +UnparseC.terms_to_strings (Ctree.get_assumptions pt p);
6.17 +(*"precond_rootmet (x::real)" -- fix in Model_Pattern? *)
6.18 +\<close> ML \<open>
6.19 \<close>
6.20
6.21 ML \<open>
7.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Sep 29 18:02:10 2022 +0200
7.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri Oct 07 20:46:48 2022 +0200
7.3 @@ -517,7 +517,7 @@
7.4 the original \emph{srls}.\\
7.5
7.6 \begin{verbatim}
7.7 - val {srls,...} = MethodC.from_store ["SignalProcessing",
7.8 + val {srls,...} = MethodC.from_store_PIDE ctxt ["SignalProcessing",
7.9 "Z_Transform",
7.10 "Inverse"];
7.11 \end{verbatim}
7.12 @@ -978,7 +978,7 @@
7.13 the hierarchy.\<close>
7.14
7.15 ML \<open>
7.16 - MethodC.from_store ["SignalProcessing", "Z_Transform", "Inverse"];
7.17 + MethodC.from_store_PIDE ctxt ["SignalProcessing", "Z_Transform", "Inverse"];
7.18 \<close>
7.19
7.20 section \<open>Program in TP-based language \label{prog-steps}\<close>
7.21 @@ -1235,7 +1235,7 @@
7.22 ) = O_Model.init thy fmz ((#ppc o Problem.from_store) pI);
7.23
7.24 val Prog sc
7.25 - = (#scr o MethodC.from_store) ["SignalProcessing",
7.26 + = (#scr o MethodC.from_store_PIDE ctxt) ["SignalProcessing",
7.27 "Z_Transform",
7.28 "Inverse"];
7.29 atomty sc;
7.30 @@ -1311,7 +1311,7 @@
7.31 arguments in the arguments\ldots
7.32 \begin{verbatim}
7.33 val Prog s =
7.34 - (#scr o MethodC.from_store) ["SignalProcessing",
7.35 + (#scr o MethodC.from_store_PIDE ctxt) ["SignalProcessing",
7.36 "Z_Transform",
7.37 "Inverse"];
7.38 writeln (UnparseC.term s);
7.39 @@ -1595,7 +1595,7 @@
7.40 parse-tree of the program with {\sisac}'s specific debug tools:
7.41 \begin{verbatim}
7.42 val {scr = Prog t,...} =
7.43 - MethodC.from_store ["simplification",
7.44 + MethodC.from_store_PIDE ctxt ["simplification",
7.45 "of_rationals",
7.46 "to_partial_fraction"];
7.47 atomty_thy @{theory "Inverse_Z_Transform"} t ;
8.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Thu Sep 29 18:02:10 2022 +0200
8.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Fri Oct 07 20:46:48 2022 +0200
8.3 @@ -1002,7 +1002,7 @@
8.4 the original \emph{srls}.\\
8.5
8.6 \begin{verbatim}
8.7 - val {srls,...} = MethodC.from_store ["SignalProcessing",
8.8 + val {srls,...} = MethodC.from_store_PIDE ctxt ["SignalProcessing",
8.9 "Z_Transform",
8.10 "Inverse"];
8.11 \end{verbatim}
8.12 @@ -2391,7 +2391,7 @@
8.13 arguments in the arguments\ldots
8.14 \begin{verbatim}
8.15 val Prog s =
8.16 - (#scr o MethodC.from_store) ["SignalProcessing",
8.17 + (#scr o MethodC.from_store_PIDE ctxt) ["SignalProcessing",
8.18 "Z_Transform",
8.19 "Inverse"];
8.20 writeln (UnparseC.term s);
8.21 @@ -2698,7 +2698,7 @@
8.22 parse-tree of the program with {\sisac}'s specific debug tools:
8.23 \begin{verbatim}
8.24 val {scr = Prog t,...} =
8.25 - MethodC.from_store ["simplification",
8.26 + MethodC.from_store_PIDE ctxt ["simplification",
8.27 "of_rationals",
8.28 "to_partial_fraction"];
8.29 atomty_thy @ { theory } t ;
9.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Thu Sep 29 18:02:10 2022 +0200
9.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Fri Oct 07 20:46:48 2022 +0200
9.3 @@ -43,7 +43,7 @@
9.4 \<close>
9.5 ML \<open>
9.6 Test_Tool.show_mets ();
9.7 -MethodC.from_store ["simplification", "for_polynomials", "with_minus"];
9.8 +MethodC.from_store_PIDE @{context} ["simplification", "for_polynomials", "with_minus"];
9.9 \<close>
9.10 text \<open>For a readable format of the method look up the definition in
9.11 $ISABELLE_ISAC/Knowledge/PolyMinus.thy or
10.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Thu Sep 29 18:02:10 2022 +0200
10.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Fri Oct 07 20:46:48 2022 +0200
10.3 @@ -16,7 +16,7 @@
10.4 "----------- fun transfer_asms_from_to ---------------------------------------------------------";
10.5 "----------- fun avoid_contradict --------------------------------------------------------------";
10.6 "----------- fun subpbl_to_caller --------------------------------------------------------------";
10.7 -"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";
10.8 +"----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
10.9 "-----------------------------------------------------------------------------------------------";
10.10 "-----------------------------------------------------------------------------------------------";
10.11 "-----------------------------------------------------------------------------------------------";
10.12 @@ -137,9 +137,9 @@
10.13 then () else error "fun subpbl_to_caller changed 2";
10.14
10.15
10.16 -"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";
10.17 -"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";
10.18 -"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";
10.19 +"----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
10.20 +"----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
10.21 +"----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
10.22 (*ER-7*) (*Schalk I s.87 Bsp 55b*)
10.23 val fmz = ["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
10.24 "solveFor x", "solutions L"];
10.25 @@ -232,7 +232,7 @@
10.26 "~~~~~ fun by_tactic , args:"; val ((Tactic.Check_Postcond' (pI, res)), (sub_ist, sub_ctxt), (pt, pos as (p, _)))
10.27 = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp);
10.28 val parent_pos = par_pblobj pt p
10.29 - val {scr, ...} = MethodC.from_store (get_obj g_metID pt parent_pos);
10.30 + val {scr, ...} = MethodC.from_store_PIDE ctxt (get_obj g_metID pt parent_pos);
10.31 val prog_res =
10.32 case LI.find_next_step scr (pt, pos) sub_ist sub_ctxt of
10.33 (*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
11.1 --- a/test/Tools/isac/BaseDefinitions/substitution.sml Thu Sep 29 18:02:10 2022 +0200
11.2 +++ b/test/Tools/isac/BaseDefinitions/substitution.sml Fri Oct 07 20:46:48 2022 +0200
11.3 @@ -100,7 +100,7 @@
11.4 "-------- build fun for_bdv --------------------------------------------------";
11.5 Subst.program_to_input: Subst.program -> string list;
11.6
11.7 -val {scr = Prog prog, ...} = MethodC.from_store ["diff", "differentiate_on_R"];
11.8 +val {scr = Prog prog, ...} = MethodC.from_store_PIDE ctxt ["diff", "differentiate_on_R"];
11.9 val env = [(TermC.str2term "v_v", TermC.str2term "x")] : Subst.T;
11.10
11.11 "~~~~~ fun for_bdv, args:"; val (prog, env) = (prog, env);
12.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Thu Sep 29 18:02:10 2022 +0200
12.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Fri Oct 07 20:46:48 2022 +0200
12.3 @@ -27,7 +27,7 @@
12.4 "--------------------------------------------------------";
12.5 "exported from struct -----------------------------------";
12.6 "--------------------------------------------------------";
12.7 -"--------- empty rootpbl --------------------------------";
12.8 +(*"--------- empty rootpbl --------------------------------";*)
12.9 "--------- solve_linear as rootpbl FE -------------------";
12.10 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
12.11 "--------- miniscript with mini-subpbl ------------------";
12.12 @@ -78,6 +78,7 @@
12.13 States.reset (); (*resets all state information in Kernel *)
12.14 (*----------------------------------------------------------------*)
12.15
12.16 +(*---------------------------------------------------- postpone to Outer_Syntax..Example -----
12.17 "--------- empty rootpbl --------------------------------";
12.18 "--------- empty rootpbl --------------------------------";
12.19 "--------- empty rootpbl --------------------------------";
12.20 @@ -87,6 +88,7 @@
12.21 refFormula 1 (States.get_pos 1 1);
12.22 (*WN.040222: stoert das sehr, dass ThyC.id_empty etc. statt leer kommt ???*)
12.23 DEconstrCalcTree 1;
12.24 +------------------------------------------------------ postpone to Outer_Syntax..Example -----*)
12.25
12.26 "--------- solve_linear as rootpbl FE -------------------";
12.27 "--------- solve_linear as rootpbl FE -------------------";
12.28 @@ -191,7 +193,7 @@
12.29 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
12.30 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
12.31 val thy' = get_obj g_domID pt (par_pblobj pt p);
12.32 - val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
12.33 + val (is, sc) = LItool.resume_prog_PIDE (p,p_) pt;
12.34 val Safe_Step (istate, _, tac) =
12.35 (*case*) LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
12.36
13.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Thu Sep 29 18:02:10 2022 +0200
13.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Fri Oct 07 20:46:48 2022 +0200
13.3 @@ -47,9 +47,9 @@
13.4 "--------- appendFormula: on Res + equ_nrls ----------------------";
13.5 "--------- appendFormula: on Res + equ_nrls ----------------------";
13.6 "--------- appendFormula: on Res + equ_nrls ----------------------";
13.7 - val Prog sc = (#scr o MethodC.from_store) ["Test", "squ-equ-test-subpbl1"];
13.8 + val Prog sc = (#scr o MethodC.from_store_PIDE ctxt) ["Test", "squ-equ-test-subpbl1"];
13.9 (writeln o UnparseC.term) sc;
13.10 - val Prog sc = (#scr o MethodC.from_store) ["Test", "solve_linear"];
13.11 + val Prog sc = (#scr o MethodC.from_store_PIDE ctxt) ["Test", "solve_linear"];
13.12 (writeln o UnparseC.term) sc;
13.13
13.14 States.reset ();
13.15 @@ -986,7 +986,7 @@
13.16 val (res, inf) =
13.17 (TermC.str2term "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))",
13.18 TermC.str2term "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
13.19 -val {errpats, nrls = rls, scr = Prog prog, ...} = MethodC.from_store ["diff", "differentiate_on_R"]
13.20 +val {errpats, nrls = rls, scr = Prog prog, ...} = MethodC.from_store_PIDE ctxt ["diff", "differentiate_on_R"]
13.21
13.22 val env = [(TermC.str2term "v_v", TermC.str2term "x")];
13.23 val errpats =
13.24 @@ -1033,16 +1033,16 @@
13.25 (*if*) f_pred = f_in; (*else*)
13.26 val NONE = (*case*) CAS_Cmd.input f_in (*of*);
13.27 (*old* )val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
13.28 - (*old*)val {scr = prog, ...} = MethodC.from_store metID
13.29 + (*old*)val {scr = prog, ...} = MethodC.from_store_PIDE ctxt metID
13.30 (*old*)val istate = get_istate_LI pt pos
13.31 (*old*)val ctxt = get_ctxt pt pos
13.32 ( *old*)
13.33 val LI.Not_Derivable =
13.34 (*case*) LI.locate_input_term (pt, pos) f_in (*of*);
13.35 val pp = Ctree.par_pblobj pt p
13.36 - val (errpats, nrls, prog) = case MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
13.37 + val (errpats, nrls, prog) = case MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
13.38 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
13.39 - | _ => error "inform: uncovered case of MethodC.from_store"
13.40 + | _ => error "inform: uncovered case of MethodC.from_store_PIDE ctxt"
13.41 ;
13.42 (*+*)if Error_Pattern.s_to_string errpats = "[(\"chain-rule-diff-both\",\n[\"d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)\", \"d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)\", \"d_d ?bdv (LogExp.ln ?u) = 1 / ?u\", \"d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u\"],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\", \"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1) * d_d ?bdv ?u\", \"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\", \"d_d ?bdv (exp ?u) = exp ?u * d_d ?x ?u\"]]"
13.43 (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3";
13.44 @@ -1085,9 +1085,9 @@
13.45 "~~~~~ fun find_fill_patterns , args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
13.46 val f_curr = Ctree.get_curr_formula (pt, pos);
13.47 val pp = Ctree.par_pblobj pt p
13.48 - val (errpats, prog) = case MethodC.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
13.49 + val (errpats, prog) = case MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
13.50 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
13.51 - | _ => error "find_fill_patterns: uncovered case of MethodC.from_store"
13.52 + | _ => error "find_fill_patterns: uncovered case of MethodC.from_store_PIDE ctxt"
13.53 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
13.54 val subst = Subst.for_bdv prog env
13.55 val errpatthms = errpats
14.1 --- a/test/Tools/isac/Interpret/li-tool.sml Thu Sep 29 18:02:10 2022 +0200
14.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Fri Oct 07 20:46:48 2022 +0200
14.3 @@ -41,7 +41,7 @@
14.4 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = (m, ptp);
14.5 "~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,ctxt), pos as (p,_))
14.6 = (m, pos);
14.7 -val {srls, ...} = MethodC.from_store mI;
14.8 +val {srls, ...} = MethodC.from_store_PIDE ctxt mI;
14.9 val PblObj {meth=itms, ...} = get_obj I pt p;
14.10 val thy' = get_obj g_domID pt p;
14.11 val thy = ThyC.get_theory thy';
14.12 @@ -138,7 +138,7 @@
14.13 if metID = MethodC.id_empty
14.14 then (thd3 o snd3) (get_obj g_origin pt pp)
14.15 else metID
14.16 - val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = MethodC.from_store metID'
14.17 + val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = MethodC.from_store_PIDE ctxt metID'
14.18 val Pstate ist = get_istate_LI pt (p,p_)
14.19 val ctxt = get_ctxt pt (p, p_)
14.20 val alltacs = (*we expect at least 1 stac in a script*)
15.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Sep 29 18:02:10 2022 +0200
15.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Fri Oct 07 20:46:48 2022 +0200
15.3 @@ -43,7 +43,7 @@
15.4
15.5 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
15.6 = (m, (pt, pos));
15.7 - val {srls, ...} = MethodC.from_store mI;
15.8 + val {srls, ...} = MethodC.from_store_PIDE ctxt mI;
15.9 val itms = case get_obj I pt p of
15.10 PblObj {meth=itms, ...} => itms
15.11 | _ => error "solve Apply_Method: uncovered case get_obj"
15.12 @@ -120,7 +120,7 @@
15.13 (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
15.14 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
15.15 val thy' = get_obj g_domID pt (par_pblobj pt p);
15.16 - val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
15.17 + val (is, sc) = LItool.resume_prog_PIDE (p,p_) pt;
15.18
15.19 locate_input_tactic sc (pt, po) (fst is) (snd is) m;
15.20 "~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
15.21 @@ -285,7 +285,7 @@
15.22 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
15.23 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
15.24 val thy' = get_obj g_domID pt (par_pblobj pt p);
15.25 - val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
15.26 + val (is, sc) = LItool.resume_prog_PIDE (p,p_) pt;
15.27
15.28 (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
15.29 "~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
15.30 @@ -382,7 +382,7 @@
15.31 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
15.32 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
15.33 val thy' = get_obj g_domID pt (par_pblobj pt p);
15.34 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
15.35 + val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
15.36
15.37 val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) =
15.38 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
15.39 @@ -433,7 +433,7 @@
15.40 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
15.41 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
15.42 val thy' = get_obj g_domID pt (par_pblobj pt p);
15.43 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
15.44 + val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
15.45
15.46 (** )val End_Program (ist, tac) =
15.47 ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
15.48 @@ -441,8 +441,8 @@
15.49 = (sc, (pt, pos), ist, ctxt);
15.50
15.51 (* val Term_Val (Const (\<^const_name>\<open>times\<close>, _) $ Free ("2", _) $ Free ("a", _))*)
15.52 - (** )val Term_Val prog_result =
15.53 - ( *case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
15.54 + (**)val Term_Val prog_result =
15.55 + (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
15.56 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
15.57 = ((prog, (ptp, ctxt)), (Pstate ist));
15.58 (*if*) path = [] (*else*);
15.59 @@ -458,7 +458,7 @@
15.60
15.61 Term_Val prog_result (*return from scan_to_tactic*);
15.62 "~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result);
15.63 - val (true, p', _) = (*case*) parent_node pt pos (*of*);
15.64 + val (true, p' as [], Rule_Set.Empty, _) = (*case*) parent_node_PIDE pt pos (*of*);
15.65 val (_, pblID, _) = get_obj g_spec pt p';
15.66
15.67 End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))
16.1 --- a/test/Tools/isac/Knowledge/biegelinie-2.sml Thu Sep 29 18:02:10 2022 +0200
16.2 +++ b/test/Tools/isac/Knowledge/biegelinie-2.sml Fri Oct 07 20:46:48 2022 +0200
16.3 @@ -132,7 +132,7 @@
16.4 val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
16.5 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
16.6 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
16.7 - val {ppc, ...} = MethodC.from_store mI;
16.8 + val {ppc, ...} = MethodC.from_store_PIDE ctxt mI;
16.9 val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
16.10 val srls = LItool.get_simplifier (pt, pos);
16.11
16.12 @@ -172,7 +172,7 @@
16.13 NONE => raise ERROR "arguments_from_model ..."(*error_msg_2 d itms*)
16.14 | SOME (_, _, _, _, itm_) => I_Model.penvval_in itm_
16.15
16.16 - val pats = (#ppc o MethodC.from_store) mI;
16.17 + val pats = (#ppc o MethodC.from_store_PIDE ctxt) mI;
16.18 (*[("#Given", (Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), Free ("q__q", "real"))),
16.19 ("#Given", (Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), Free ("v_v", "real"))),
16.20 ("#Given", (Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), Free ("id_fun", "real \<Rightarrow> real"))),
17.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Thu Sep 29 18:02:10 2022 +0200
17.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Fri Oct 07 20:46:48 2022 +0200
17.3 @@ -20,7 +20,7 @@
17.4 "----------- retrieve errpats ------------------------------------";
17.5 "----------- retrieve errpats ------------------------------------";
17.6 "----------- retrieve errpats ------------------------------------";
17.7 -val {errpats, nrls, scr = Prog prog, ...} = MethodC.from_store ["diff", "differentiate_on_R"];
17.8 +val {errpats, nrls, scr = Prog prog, ...} = MethodC.from_store_PIDE ctxt ["diff", "differentiate_on_R"];
17.9 case errpats of [("chain-rule-diff-both", _, _)] => ()
17.10 | _ => error "errpats chain-rule-diff-both changed"
17.11
18.1 --- a/test/Tools/isac/Knowledge/diff.sml Thu Sep 29 18:02:10 2022 +0200
18.2 +++ b/test/Tools/isac/Knowledge/diff.sml Fri Oct 07 20:46:48 2022 +0200
18.3 @@ -42,7 +42,7 @@
18.4 val chkorg = map (TermC.parseNEW' ctxt) org;
18.5
18.6 Problem.from_store_PIDE @{context} ["derivative_of", "function"];
18.7 -MethodC.from_store ["diff", "differentiate_on_R"];
18.8 +MethodC.from_store_PIDE ctxt ["diff", "differentiate_on_R"];
18.9
18.10 "----------- for correction of diff_const ---------------";
18.11 "----------- for correction of diff_const ---------------";
19.1 --- a/test/Tools/isac/Knowledge/eqsystem-1a.sml Thu Sep 29 18:02:10 2022 +0200
19.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1a.sml Fri Oct 07 20:46:48 2022 +0200
19.3 @@ -84,7 +84,7 @@
19.4 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
19.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
19.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
19.7 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
19.8 + val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
19.9
19.10 val Next_Step (Pstate {act_arg = t, ...}, _, _) = (*case*)
19.11 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
20.1 --- a/test/Tools/isac/Knowledge/integrate.sml Thu Sep 29 18:02:10 2022 +0200
20.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Fri Oct 07 20:46:48 2022 +0200
20.3 @@ -353,7 +353,7 @@
20.4 val {ppc,...} = Problem.from_store_PIDE @{context} ["named", "integrate", "function"];
20.5 val ("#Find", (Const (\<^const_name>\<open>antiDerivativeName\<close>, _),
20.6 F1_ as Free ("F_F", F1_type))) = last_elem ppc;
20.7 -val {scr = Prog sc,... } = MethodC.from_store ["diff", "integration", "named"];
20.8 +val {scr = Prog sc,... } = MethodC.from_store_PIDE ctxt ["diff", "integration", "named"];
20.9 val [_,_, F2_] = formal_args sc;
20.10 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
20.11
21.1 --- a/test/Tools/isac/Knowledge/integrate.thy Thu Sep 29 18:02:10 2022 +0200
21.2 +++ b/test/Tools/isac/Knowledge/integrate.thy Fri Oct 07 20:46:48 2022 +0200
21.3 @@ -15,7 +15,7 @@
21.4 (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'') #>
21.5 (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'')) (f_f::real))"
21.6 setup \<open>KEStore_Elems.add_mets @{context}
21.7 - [MethodC.prep_input @{theory "Isac_Knowledge"} "met_testint" [] MethodC.id_empty
21.8 + [MethodC.prep_input_PIDE @{theory "Isac_Knowledge"} "met_testint" [] MethodC.id_empty
21.9 (["diff", "integration", "test"],
21.10 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find", ["antiDerivative F_F"])],
21.11 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
22.1 --- a/test/Tools/isac/Knowledge/inverse_z_transform.sml Thu Sep 29 18:02:10 2022 +0200
22.2 +++ b/test/Tools/isac/Knowledge/inverse_z_transform.sml Fri Oct 07 20:46:48 2022 +0200
22.3 @@ -16,7 +16,7 @@
22.4 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
22.5 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
22.6 Problem.from_store ["Inverse", "Z_Transform", "SignalProcessing"];
22.7 -MethodC.from_store ["SignalProcessing", "Z_Transform", "Inverse"];
22.8 +MethodC.from_store_PIDE ctxt ["SignalProcessing", "Z_Transform", "Inverse"];
22.9
22.10 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
22.11 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
23.1 --- a/test/Tools/isac/Knowledge/rateq.sml Thu Sep 29 18:02:10 2022 +0200
23.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Fri Oct 07 20:46:48 2022 +0200
23.3 @@ -105,7 +105,7 @@
23.4 member op = [Pbl,Met] p_; (*= false*)
23.5 "~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
23.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
23.7 -val (is, sc) = resume_prog thy' (p,p_) pt; (*is: which ctxt?*)
23.8 +val (is, sc) = resume_prog_PIDE (p,p_) pt; (*is: which ctxt?*)
23.9 "~~~~~ fun find_next_step, args:"; val () = ();
23.10 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
23.11 "~~~~~ fun go_scan_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
23.12 @@ -141,7 +141,7 @@
23.13 val thy' = (get_obj g_domID pt pp):theory';
23.14 val thy = ThyC.get_theory thy'
23.15 val metID = (get_obj g_metID pt pp)
23.16 - val {crls,...} = MethodC.from_store metID
23.17 + val {crls,...} = MethodC.from_store_PIDE ctxt metID
23.18 val (f,asm) = case p_ of Frm => (get_obj g_form pt p , [])
23.19 | Res => get_obj g_result pt p;
23.20 UnparseC.term f = "[x = 1 / 5]"; (*the current formula*)
23.21 @@ -226,102 +226,6 @@
23.22 if p = ([], Res) andalso f2str f = "[x = - 2, x = 10]" then ()
23.23 else error "rateq.sml: new behaviour: [x = - 2, x = 10]";
23.24
23.25 -"----------- remove x = 0 from [x = 0, x = 6 / 5] ----------------------------------------------";
23.26 -"----------- remove x = 0 from [x = 0, x = 6 / 5] ----------------------------------------------";
23.27 -"----------- remove x = 0 from [x = 0, x = 6 / 5] ----------------------------------------------";
23.28 -(*ER-7*) (*Schalk I s.87 Bsp 55b*)
23.29 -val fmz = ["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
23.30 - "solveFor x", "solutions L"];
23.31 -val spec =
23.32 - ((** )"RatEq"( **)"PolyEq"(*rls "make_ratpoly_in" missing in theory "RatEq" (and ancestors)*),
23.33 - ["univariate", "equation"],["no_met"]);
23.34 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)]; (* 0. specify-phase *)
23.35 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.36 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.37 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.38 -
23.39 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.40 -(*+*)case nxt of Apply_Method ["RatEq", "solve_rat_equation"] => ()
23.41 -(*+*)| _ => error "55b root specification broken";
23.42 -
23.43 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 0. solve-phase*)
23.44 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.45 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "(3 + - 1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)";
23.46 -
23.47 -(*+*)if eq_set op = (Ctree.get_assumptions pt p |> map UnparseC.term,
23.48 -(*+*) ["x \<noteq> 0", "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0", "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x"])
23.49 -(*+*)then () else error "assumptions before 1. Subproblem CHANGED";
23.50 -(*+*)if p = ([3], Res) andalso f2str f = "(3 + - 1 * x + x \<up> 2) * x = 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)"
23.51 -(*+*)then
23.52 -(*+*) ((case nxt of Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]) => ()
23.53 -(*+*) | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))
23.54 -(*+*)else error "1. Subproblem -- call changed";
23.55 -
23.56 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 1. specify-phase *)
23.57 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.58 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.59 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.60 -
23.61 -(*[4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.62 -case nxt of Apply_Method ["PolyEq", "normalise_poly"] => ()
23.63 -| _ => error "55b normalise_poly specification broken 1";
23.64 -
23.65 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 1. solve-phase *)
23.66 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.67 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "-6 * x + 5 * x \<up> 2 = 0";
23.68 -
23.69 -if p = ([4, 3], Res) andalso f2str f = "- 6 * x + 5 * x \<up> 2 = 0"
23.70 -then
23.71 - ((case nxt of Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]) => ()
23.72 - | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string nxt)))
23.73 -else error "xxx";
23.74 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 2. specify-phase *)
23.75 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.76 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.77 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.78 -
23.79 -(*[4, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>*)
23.80 -case nxt of Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"] => ()
23.81 -| _ => error "55b normalise_poly specification broken 2";
23.82 -
23.83 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*f = "-6 * x + 5 * x \<up> 2 = 0"*) (* 2. solve-phase *)
23.84 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23.85 -
23.86 -(*[4, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Or_to_List*)
23.87 -(*[4, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "[x = 0, x = 6 / 5]";
23.88 -(*[4, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>2. Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]*)
23.89 -
23.90 -(* *)if eq_set op = ((Ctree.get_assumptions pt p |> map UnparseC.term), [
23.91 -(*0.pre*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
23.92 -(*1.pre*) "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) \<or>\n"
23.93 -(*1.pre*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
23.94 -(*2.pre*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
23.95 -(*2.pre*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
23.96 -(*0.asm*) "x \<noteq> 0",
23.97 -(*0.asm*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
23.98 -(* *)])
23.99 -(* *)then () else error "assumptions at end 2. Subproblem CHANGED";
23.100 -
23.101 -(*[4, 4], Res*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt;(*\<rightarrow>1. Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
23.102 -
23.103 -(*/--------- step into 2. Check_Postcond SEE .. ----------------------------------------------\*)
23.104 -"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";
23.105 -(*\--------- step into 2. Check_Postcond -----------------------------------------------------/*)
23.106 -
23.107 -(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>IDLE LEGACY: Check_elementwise "Assumptions"*)
23.108 -(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>End_Proof'*)
23.109 -
23.110 -(*/-------- final test -----------------------------------------------------------------------\*)
23.111 -if f2str f = "[x = 6 / 5]" andalso eq_set op = (map UnparseC.term (Ctree.get_assumptions pt p),
23.112 - ["x = 6 / 5",
23.113 - "lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
23.114 - "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
23.115 - "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) \<or>\n\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
23.116 - "x \<noteq> 0",
23.117 - "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
23.118 - "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x"]
23.119 -) then () else error "test CHANGED";
23.120 -
23.121
23.122 "----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";
23.123 "----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";
24.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Thu Sep 29 18:02:10 2022 +0200
24.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Fri Oct 07 20:46:48 2022 +0200
24.3 @@ -548,7 +548,7 @@
24.4 val (dI',pI',mI') =
24.5 ("Test",["sqroot-test", "univariate", "equation", "test"],
24.6 ["Test", "square_equation2"]);
24.7 -val Prog sc = (#scr o MethodC.from_store) ["Test", "square_equation2"];
24.8 +val Prog sc = (#scr o MethodC.from_store_PIDE ctxt) ["Test", "square_equation2"];
24.9 (writeln o UnparseC.term) sc;
24.10
24.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
24.12 @@ -614,7 +614,7 @@
24.13
24.14
24.15
24.16 -val Prog s = (#scr o MethodC.from_store) ["Test", "square_equation"];
24.17 +val Prog s = (#scr o MethodC.from_store_PIDE ctxt) ["Test", "square_equation"];
24.18 atomt s;
24.19
24.20
24.21 @@ -685,7 +685,7 @@
24.22 val (dI',pI',mI') =
24.23 ("Test",["squareroot", "univariate", "equation", "test"],
24.24 ["Test", "square_equation"]);
24.25 - val Prog sc = (#scr o MethodC.from_store) ["Test", "square_equation"];
24.26 + val Prog sc = (#scr o MethodC.from_store_PIDE ctxt) ["Test", "square_equation"];
24.27 (writeln o UnparseC.term) sc;
24.28
24.29 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
25.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Thu Sep 29 18:02:10 2022 +0200
25.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Fri Oct 07 20:46:48 2022 +0200
25.3 @@ -341,7 +341,7 @@
25.4 val thy' = get_obj g_domID pt (par_pblobj pt p);
25.5
25.6 val (_, (ist, ctxt), sc) =
25.7 - LItool.resume_prog thy' (p,p_) pt;
25.8 + LItool.resume_prog_PIDE (p,p_) pt;
25.9 "~~~~~ fun resume_prog , args:"; val (thy, (p, p_), pt) = (thy', (p,p_), pt);
25.10 (*if*) Pos.on_specification (p, p_) (*else*);
25.11 val (pbl, p', rls') = parent_node pt pos
26.1 --- a/test/Tools/isac/Knowledge/simplify.sml Thu Sep 29 18:02:10 2022 +0200
26.2 +++ b/test/Tools/isac/Knowledge/simplify.sml Fri Oct 07 20:46:48 2022 +0200
26.3 @@ -106,11 +106,11 @@
26.4
26.5 (** ) val (_, (Met, Specify_Method ["simplification", "of_rationals"])) = ( *isa*)
26.6 (**) val (_, (Met, Apply_Method ["simplification", "of_rationals"])) = (*isa2*)
26.7 - for_method oris (o_refs, refs) (pbl, met);
26.8 + for_method_PIDE ctxt oris (o_refs, refs) (pbl, met);
26.9 "~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
26.10 (oris, (o_refs, refs), (pbl, met));
26.11 val cmI = if mI = MethodC.id_empty then mI' else mI;
26.12 - val {ppc = mpc, prls, pre, ...} = MethodC.from_store cmI; (*..MethodC ?*)
26.13 + val {ppc = mpc, prls, pre, ...} = MethodC.from_store_PIDE ctxt cmI; (*..MethodC ?*)
26.14
26.15 (** ) val (preok as false, _) = Pre_Conds.check prls pre pbl 0; ( *isa*)
26.16 (**) val (preok as true, _) = Pre_Conds.check prls pre pbl 0; (*isa2*)
27.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Thu Sep 29 18:02:10 2022 +0200
27.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Fri Oct 07 20:46:48 2022 +0200
27.3 @@ -169,7 +169,7 @@
27.4 "----------- fun upds_envv ---------------------------------------------------------------------";
27.5 (* eval test-maximum.sml until Specify_Method ...
27.6 val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt [];
27.7 - val met = (#ppc o MethodC.from_store) mI;
27.8 + val met = (#ppc o MethodC.from_store_PIDE ctxt) mI;
27.9
27.10 val envv = [];
27.11 val eargs = flat eargs;
28.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu Sep 29 18:02:10 2022 +0200
28.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Fri Oct 07 20:46:48 2022 +0200
28.3 @@ -86,7 +86,7 @@
28.4 "~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
28.5 MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*false*)
28.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
28.7 -val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
28.8 +val ((ist, ctxt), sc) = resume_prog_PIDE (p,p_) pt;
28.9
28.10 val Next_Step (istate, ctxt, tac) = LI.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)
28.11 case tac of Or_to_List' _ => ()
28.12 @@ -114,7 +114,7 @@
28.13
28.14 "~~~~~ fun CalcTreeTEST , args:"; val [(fmz, sp):Formalise.T] = [(fmz, (dI,pI,mI))];
28.15 (*val ((pt, p), tacis) =*)
28.16 -Step_Specify.nxt_specify_init_calc (fmz, sp);
28.17 +Step_Specify.nxt_specify_init_calc ctxt (fmz, sp);
28.18 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
28.19 (*val (_, hdl, (dI, pI, mI), pors, pctxt) =*)
28.20 initialise_PIDE (fmz, (dI, pI, mI));
28.21 @@ -198,7 +198,7 @@
28.22 "~~~~~ fun do_next , args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);
28.23 MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;
28.24 val thy' = get_obj g_domID pt (par_pblobj pt p);
28.25 - val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
28.26 + val ((ist, ctxt), sc) = resume_prog_PIDE (p,p_) pt;
28.27 val Next_Step (is, ctxt, tac_) = LI.find_next_step sc (pt,pos) ist ctxt;
28.28 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
28.29
28.30 @@ -322,7 +322,7 @@
28.31 Frm => get_obj g_form pt p
28.32 | Res => (fst o (get_obj g_result pt)) p
28.33 | _ => TermC.empty (*on PblObj is fo <> ifo*);
28.34 - val {nrls, ...} = MethodC.from_store (get_obj g_metID pt (par_pblobj pt p))
28.35 + val {nrls, ...} = MethodC.from_store_PIDE ctxt (get_obj g_metID pt (par_pblobj pt p))
28.36 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls;
28.37 (*val (found, der) = *)Derive.steps ctxt rew_ord erls rules fo ifo; (*<---------------*)
28.38 "~~~~~ fun concat_deriv, args:"; val (rew_ord, erls, rules, fo, ifo) =
29.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Thu Sep 29 18:02:10 2022 +0200
29.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Fri Oct 07 20:46:48 2022 +0200
29.3 @@ -12,7 +12,7 @@
29.4 ["Test", "squ-equ-test-subpbl1"]);
29.5 "~~~~~ fun CalcTreeTEST , args:"; val [(fmz, sp): Formalise.T] = [(fmz, (dI',pI',mI'))];
29.6
29.7 -Step_Specify.nxt_specify_init_calc (fmz, sp);
29.8 +Step_Specify.nxt_specify_init_calc ctxt (fmz, sp);
29.9 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
29.10 val (_, hdl, (dI, pI, mI), pors, pctxt) = initialise_PIDE (fmz, (dI, pI, mI))
29.11 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt)
29.12 @@ -25,7 +25,7 @@
29.13 (*///----------------------------------------- save for final check ------------------------\\\*)
29.14 val [(fmz''''', spec''''')] = [(fmz, (dI',pI',mI'))];
29.15 "~~~~~ fun CalcTreeTEST, args:"; val ([(fmz, sp)]) = ([(fmz, (dI',pI',mI'))]);
29.16 - val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc (fmz, sp)
29.17 + val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc ctxt (fmz, sp)
29.18 (*ADD check*)
29.19 val PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} = get_obj I pt (fst p);
29.20 (* ERROR Specify.item_to_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt
30.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Thu Sep 29 18:02:10 2022 +0200
30.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Fri Oct 07 20:46:48 2022 +0200
30.3 @@ -43,7 +43,7 @@
30.4 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
30.5 (*if*) p_ = Pos.Pbl (*then*);
30.6 "~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) =
30.7 - for_problem oris (o_refs, refs) (pbl, met);
30.8 + Specify.for_problem_PIDE ctxt oris (o_refs, refs) (pbl, met);
30.9 (*\--------- step into Specify_Theory --------------------------------------------------------/*)
30.10
30.11 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p''''' ((pt''''', e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)
31.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Sep 29 18:02:10 2022 +0200
31.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Fri Oct 07 20:46:48 2022 +0200
31.3 @@ -66,7 +66,7 @@
31.4 val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
31.5 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
31.6 | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj"
31.7 - val {ppc, ...} = MethodC.from_store mI;
31.8 + val {ppc, ...} = MethodC.from_store_PIDE ctxt mI;
31.9 val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
31.10 val srls = LItool.get_simplifier (pt, pos)
31.11 val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
32.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Sep 29 18:02:10 2022 +0200
32.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Fri Oct 07 20:46:48 2022 +0200
32.3 @@ -38,7 +38,7 @@
32.4 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
32.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (* = else*);
32.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
32.7 - val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
32.8 + val (is, sc) = LItool.resume_prog_PIDE (p,p_) pt;
32.9
32.10 val Safe_Step (_, _, Rewrite_Set' (_, _, Rule_Set.Repeat {id = "norm_equation", ...}, _, _)) = (*case*)
32.11 locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
32.12 @@ -94,7 +94,7 @@
32.13 MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;
32.14 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p)(*else*);
32.15 val thy' = get_obj g_domID pt (par_pblobj pt p);
32.16 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
32.17 + val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
32.18
32.19 val Next_Step (_, _, _) =
32.20 (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
32.21 @@ -146,7 +146,7 @@
32.22 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
32.23 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
32.24 val thy' = get_obj g_domID pt (par_pblobj pt p);
32.25 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
32.26 + val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
32.27
32.28 val Next_Step (_, _, _) =
32.29 (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
33.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Thu Sep 29 18:02:10 2022 +0200
33.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Fri Oct 07 20:46:48 2022 +0200
33.3 @@ -36,7 +36,7 @@
33.4 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt ptp;
33.5 "~~~~~ fun begin_end_prog , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (ist, ctxt), (pt, pos as (p, _)))
33.6 = ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, ptp);
33.7 - val {ppc, ...} = MethodC.from_store mI;
33.8 + val {ppc, ...} = MethodC.from_store_PIDE ctxt mI;
33.9 val (itms, oris, probl) = case get_obj I pt p of
33.10 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
33.11 | _ => error "begin_end_prog Apply_Method': uncovered case get_obj"
34.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Sep 29 18:02:10 2022 +0200
34.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Fri Oct 07 20:46:48 2022 +0200
34.3 @@ -39,7 +39,7 @@
34.4 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, p));
34.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*false*);
34.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
34.7 - val (is, sc) = resume_prog thy' (p,p_) pt;
34.8 + val (is, sc) = resume_prog_PIDE (p,p_) pt;
34.9
34.10 val Safe_Step (Pstate ist''''', ctxt''''', tac'_''''') =
34.11 locate_input_tactic sc (pt, po) (fst is) (snd is) m;
35.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Sep 29 18:02:10 2022 +0200
35.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Fri Oct 07 20:46:48 2022 +0200
35.3 @@ -28,56 +28,89 @@
35.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
35.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
35.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
35.7 -val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
35.8 -(*//--1 begin step into relevant call --------- \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> ^-------\\
35.9 - 1 relevant for all Apply_Method *)
35.10 -(*+*)if get_ctxt pt p |> ContextC.is_empty then error "ctxt no initialised by specify, PblObj{ctxt,...}" else ();
35.11 -(*+*)if get_ctxt pt p |> ContextC.is_empty then error "ctxt NOT initialised by Subproblem'}" else ();
35.12 -(*+*)val SOME t = parseNEW (get_ctxt pt p) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
35.13 +val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; (*nxt''' = Apply_Method ["Test", "solve_linear"]*)
35.14 +(*/------------------- step into ---------------- nxt''' = Apply_Method ["Test", "solve_linear"]-\*)
35.15 +(*+*)val ([3], Pbl) = p;
35.16 +(*+*)if get_ctxt pt p |> ContextC.is_empty then error "ctxt not initialised by specify, PblObj{ctxt,...}" else ();
35.17 +(*+*)if get_ctxt pt''' p''' |> ContextC.is_empty then error "ctxt NOT initialised by Subproblem'}" else ();
35.18
35.19 + me nxt''' p''' [] pt''';
35.20 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
35.21 -
35.22 - val ("ok", (_, _, (pt'''', p''''))) = (*case*)
35.23 + val ("ok", (_, _, (_, _))) = (*case*)
35.24 Step.by_tactic tac (pt, p) (*of*);
35.25 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
35.26 - val Applicable.Yes m = (*case*) Step.check tac (pt, p) (*of*);
35.27 - (*if*) Tactic.for_specify' m; (*false*)
35.28 + val Applicable.Yes tac' = (*case*) Step.check tac (pt, p) (*of*);
35.29 + (*if*) Tactic.for_specify' tac'; (*else*)
35.30
35.31 -Step_Solve.by_tactic m ptp;
35.32 -"~~~~~ fun by_tactic , args:"; val (m as Tactic.Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p, _))))
35.33 - = (m, (pt, p));
35.34 - val itms = case get_obj I pt p of
35.35 - PblObj {meth=itms, ...} => itms
35.36 - | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case get_obj"
35.37 - val thy' = get_obj g_domID pt p;
35.38 - val thy = ThyC.get_theory thy';
35.39 - val srls = LItool.get_simplifier (pt, pos)
35.40 - val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
35.41 - (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
35.42 - | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case init_pstate"
35.43 +Step_Solve.by_tactic tac' ptp;
35.44 +"~~~~~ fun by_tactic , args:"; val (tac as Tactic.Apply_Method' _, ptp as (pt, p))
35.45 + = (tac', ptp);
35.46
35.47 -(*+*)val (pt, p) = case Step.by_tactic tac (pt, pos) of
35.48 - ("ok", (_, _, ptp)) => ptp | _ => error "script.sml Step.by_tactic";
35.49 -(*+*)val SOME t = parseNEW (get_ctxt pt p) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
35.50 +(*+*)val PblObj {ctxt, ...} = get_obj I pt [3];
35.51 +(*+isa==isa2*)ContextC.get_assumptions ctxt = [];
35.52 +(*+isa==isa2*)(Ctree.get_assumptions pt p |> map UnparseC.term) = [];
35.53
35.54 -"~~~~~ from Step_Solve.by_tactic to..to me return"; val (pt, p) = (pt'''', p'''');
35.55 + LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;
35.56 +"~~~~~ fun by_tactic , args:"; val (Tactic.Apply_Method' (mI, _, _, _), (_, ctxt), (pt, (pos as (p, _))))
35.57 + = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), (pt, p));
35.58
35.59 - val ("ok", ([(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), _, (_, (Pstate _, _)))], _, _)) = (*case*)
35.60 - Step.do_next p ((pt, e_pos'), []) (*of*);
35.61 -"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p'''', ((pt'''', e_pos'), []))
35.62 -val pIopt = get_pblID (pt,ip);
35.63 -tacis; (*= []*)
35.64 -member op = [Pbl,Met] p_ (*= false*);
35.65 +(*+isa==isa2*)if (ContextC.get_assumptions ctxt |> map UnparseC.term) = ["precond_rootmet x"]
35.66 +(*+*)then () else error "assumptions 7 from Apply_Method'";
35.67
35.68 -"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
35.69 -val thy' = get_obj g_domID pt (par_pblobj pt p);
35.70 -val (is, sc) = resume_prog thy' (p,p_) pt;
35.71 +(*+*)val [3] = p;
35.72 + val (itms, oris, probl(*, ctxt*)) = case get_obj I pt p of
35.73 + PblObj {meth = itms, origin = (oris, _, _), probl(*, ctxt*), ...} => (itms, oris, probl(*, ctxt*))
35.74 + | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj";
35.75
35.76 -"~~~~~ fun find_next_step , args:"; val ((thy, _), (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, _))
35.77 - = ((thy',srls), (pt,pos), sc, is);
35.78 +(*+isa==isa2*)if (ContextC.get_assumptions ctxt |> map UnparseC.term) = ["precond_rootmet x"]
35.79 +(*+*)then () else error "assumptions 8";
35.80
35.81 -(*+*)val SOME t = parseNEW (get_ctxt pt pos) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
35.82 -(*\\--1 end step into relevant call ----------------------------------------------------------//*)
35.83 + val {ppc, ...} = MethodC.from_store_PIDE ctxt mI;
35.84 + val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
35.85 + val srls = LItool.get_simplifier (pt, pos)
35.86 + val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
35.87 + (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
35.88 + | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate";
35.89 +
35.90 +(*+*)(ContextC.get_assumptions ctxt |> map UnparseC.term)
35.91 +(*+isa==isa2*) = ["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"];
35.92 +
35.93 + val ini = LItool.implicit_take prog env;
35.94 + val pos = start_new_level pos
35.95 +val SOME t =
35.96 + (*case*) ini (*of*);
35.97 + val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
35.98 + val (pos, c, _, pt) = Solve_Step.add show_add (is, ctxt) (pt, pos);
35.99 +
35.100 +(*+*)if (ContextC.get_assumptions ctxt |> map UnparseC.term)
35.101 +(*+isa==isa2*) = ["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"]
35.102 +(*+*)then () else error "assumptions 9";
35.103 +
35.104 +val return = ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos)));
35.105 +"~~~~~ from LI.by_tactic to..to me return"; val ("ok", (_, _, ptp)) = return;
35.106 + val (pt, p) = ptp;
35.107 +
35.108 + (*case*)
35.109 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
35.110 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
35.111 + = (p, ((pt, Pos.e_pos'), []));
35.112 + (*if*) Pos.on_calc_end ip (*else*);
35.113 + val (_, probl_id, _) = Calc.references (pt, p);
35.114 +val _ =
35.115 + (*case*) tacis (*of*);
35.116 + (*if*) probl_id = Problem.id_empty (*else*);
35.117 +
35.118 + switch_specify_solve p_ (pt, ip);
35.119 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos))
35.120 + = (p_, (pt, ip));
35.121 + val result =
35.122 + if Pos.on_specification ([], state_pos)
35.123 + then specify_do_next (pt, input_pos)
35.124 + else LI.do_next (pt, input_pos);
35.125 +
35.126 +"~~~~~ from fun switch_specify_solve \<longrightarrow>fun Step.do_next \<longrightarrow>fun me , return:"; val (_, ts)
35.127 + = (LI.do_next (pt, input_pos));
35.128 +(*\------------------- step into ---------------- nxt''' = Apply_Method ["Test", "solve_linear"]-/*)
35.129
35.130 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
35.131
35.132 @@ -85,4 +118,20 @@
35.133 Tactic.input_to_string nxt = "Rewrite_Set_Inst ([(''bdv'', x)], \"isolate_bdv\")"
35.134 then () else error "Minisubpbl/400-start-meth-subpbl changed";
35.135
35.136 -Proof_Context.theory_of (Ctree.get_ctxt pt p); (*"Test"*)
35.137 +(*+*)val p_frm = ([3], Frm);
35.138 +(*+*)if (Ctree.get_assumptions pt p_frm |> map UnparseC.term) = ["precond_rootmet x"]
35.139 +(*+*)then () else error "p_frm BEFORE Apply_Method at Subproblem CHANGED";
35.140 +
35.141 +(*+*)val ([3], Met) = p''';
35.142 +(*+*)if (Ctree.get_assumptions pt''' p''')
35.143 +(*+*) = [(*------ inserted by Apply_Method ------------------*)]
35.144 +(*+*)then () else error "assumptions<>[] before Apply_Method of Subproblem";
35.145 +
35.146 +(*+*)val ([3, 1], Frm) = p;
35.147 +(*+*)if (Ctree.get_assumptions pt p |> map UnparseC.term)
35.148 +(*+*) = ["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"]
35.149 +(*+*)then () else error "FALSE: 2 assumptions recorded Apply_Method of Subproblem";
35.150 +
35.151 +(*+*)val p_res = ([3], Res);
35.152 +(*+*)if (Ctree.get_assumptions pt p_res |> map UnparseC.term) = ["precond_rootmet x"]
35.153 +(*+*)then () else error "p_res AFTER Apply_Method at Subproblem CHANGED";
36.1 --- a/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Thu Sep 29 18:02:10 2022 +0200
36.2 +++ b/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Fri Oct 07 20:46:48 2022 +0200
36.3 @@ -54,7 +54,7 @@
36.4 "~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = ((pt, ip));
36.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
36.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
36.7 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
36.8 + val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
36.9
36.10 LI.find_next_step sc (pt, pos) ist ctxt;
36.11 "~~~~~ fun find_next_step , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
37.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Thu Sep 29 18:02:10 2022 +0200
37.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Fri Oct 07 20:46:48 2022 +0200
37.3 @@ -46,7 +46,7 @@
37.4 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
37.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*false*)
37.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
37.7 -val ((ist, ctxt), sc) = resume_prog thy' (p,p_) pt;
37.8 +val ((ist, ctxt), sc) = resume_prog_PIDE (p,p_) pt;
37.9
37.10 val End_Program (ist, tac) =
37.11 (*case*) LI.find_next_step sc (pt,pos) ist ctxt (*of*);
37.12 @@ -56,7 +56,7 @@
37.13 "~~~~~ fun by_tactic , args:"; val ((Check_Postcond' (pI, _)), (sub_ist, sub_ctxt), (pt, pos as (p,_))) =
37.14 (tac, (ist, ctxt), ptp);
37.15 val parent_pos = par_pblobj pt p
37.16 - val {scr, ...} = MethodC.from_store (get_obj g_metID pt parent_pos);
37.17 + val {scr, ...} = MethodC.from_store_PIDE ctxt (get_obj g_metID pt parent_pos);
37.18 val prog_res =
37.19 case LI.find_next_step scr (pt, pos) sub_ist sub_ctxt of
37.20 (*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
37.21 @@ -82,7 +82,7 @@
37.22 (tac, (ist', ctxt'), (pt, (parent_pos, Res)));
37.23 val (pt,c) = append_result pt p l (scval, asm) Complete;
37.24
37.25 -val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["LINEAR", "uval (is, sc) = resume_prog thy' (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *);
37.26 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["LINEAR", "uval (is, sc) = resume_prog_PIDE (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *);
37.27 case nxt of ( Check_Postcond ["LINEAR", "univariate", "equation", "test"]) => ()
37.28 | _ => error "450-nxt-Check_Postcond broken";
37.29
38.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Sep 29 18:02:10 2022 +0200
38.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Fri Oct 07 20:46:48 2022 +0200
38.3 @@ -55,7 +55,7 @@
38.4 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
38.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
38.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
38.7 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
38.8 + val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
38.9
38.10 val Next_Step (_, _, Check_elementwise' _) =
38.11 (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
39.1 --- a/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml Thu Sep 29 18:02:10 2022 +0200
39.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml Fri Oct 07 20:46:48 2022 +0200
39.3 @@ -100,7 +100,7 @@
39.4 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
39.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
39.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
39.7 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
39.8 + val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
39.9
39.10 (*+*)Istate.string_of ist
39.11 = "Pstate ([\"\n(e_e, - 1 + x = 0)\",\"\n(v_v, x)\",\"\n(L_L, [x = 1])\"], [R,R,D,R,D], empty, NONE, \n[x = 1],"
40.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Thu Sep 29 18:02:10 2022 +0200
40.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Fri Oct 07 20:46:48 2022 +0200
40.3 @@ -51,7 +51,7 @@
40.4 "~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = (pt, input_pos);
40.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
40.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
40.7 - val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
40.8 + val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
40.9
40.10 val Next_Step (ist, ctxt, tac) = (*case*) (**..Ctree NOT updated yet**)
40.11 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
40.12 @@ -111,7 +111,7 @@
40.13 (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
40.14 "~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = (([], [], (pt, pos_pred)), tm);
40.15 val fo = Calc.current_formula ptp
40.16 - val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
40.17 + val {nrls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
40.18 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
40.19 val (found, der) = Derive.steps ctxt rew_ord erls rules fo ifo; (*<---------------*)
40.20 (*if*) found (*then*);
40.21 @@ -129,7 +129,7 @@
40.22 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
40.23 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
40.24 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
40.25 - val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
40.26 + val {nrls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
40.27 val (pt, c, pos as (p, _)) =
40.28
40.29 Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res));
41.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Thu Sep 29 18:02:10 2022 +0200
41.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Fri Oct 07 20:46:48 2022 +0200
41.3 @@ -542,7 +542,7 @@
41.4 (*solve*)
41.5 val pp = par_pblobj pt p;
41.6 val metID = get_obj g_metID pt pp;
41.7 - val sc = (#scr o MethodC.from_store) metID;
41.8 + val sc = (#scr o MethodC.from_store_PIDE ctxt) metID;
41.9 val is = get_istate_LI pt (p,p_);
41.10 val thy' = get_obj g_domID pt pp;
41.11 val thy = ThyC.get_theory thy';
42.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Thu Sep 29 18:02:10 2022 +0200
42.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Fri Oct 07 20:46:48 2022 +0200
42.3 @@ -279,7 +279,7 @@
42.4 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
42.5 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
42.6 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
42.7 -val {scr, ...} = MethodC.from_store ["Test", "sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
42.8 +val {scr, ...} = MethodC.from_store_PIDE ctxt ["Test", "sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
42.9 case stacpbls sc of
42.10 [Const (\<^const_name>\<open>Rewrite\<close>, _) $ square_equation_left,
42.11 Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ Test_simplify,
43.1 --- a/test/Tools/isac/ProgLang/calculate.thy Thu Sep 29 18:02:10 2022 +0200
43.2 +++ b/test/Tools/isac/ProgLang/calculate.thy Fri Oct 07 20:46:48 2022 +0200
43.3 @@ -34,7 +34,7 @@
43.4 (Try (Repeat (Calculate ''DIVIDE''))) #>
43.5 (Try (Repeat (Calculate ''POWER''))))) t_t"
43.6 setup \<open>KEStore_Elems.add_mets @{context}
43.7 - [MethodC.prep_input (@{theory "Test"}) "met_testcal" [] MethodC.id_empty
43.8 + [MethodC.prep_input_PIDE (@{theory "Test"}) "met_testcal" [] MethodC.id_empty
43.9 (["Test", "test_calculate"],
43.10 [("#Given" , ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])],
43.11 {rew_ord'="sqrt_right",rls'=tval_rls,srls = Rule_Set.empty, prls = Rule_Set.empty,
44.1 --- a/test/Tools/isac/ProgLang/prog_tac.sml Thu Sep 29 18:02:10 2022 +0200
44.2 +++ b/test/Tools/isac/ProgLang/prog_tac.sml Fri Oct 07 20:46:48 2022 +0200
44.3 @@ -18,7 +18,7 @@
44.4 "-------- fun eval_leaf -------------------------------------------------------------------";
44.5 "-------- fun eval_leaf -------------------------------------------------------------------";
44.6 "-------- fun eval_leaf -------------------------------------------------------------------";
44.7 -val {scr = Prog sc, ...} = MethodC.from_store ["Test", "sqrt-equ-test"];
44.8 +val {scr = Prog sc, ...} = MethodC.from_store_PIDE ctxt ["Test", "sqrt-equ-test"];
44.9 case eval_leaf [] NONE TermC.empty sc of
44.10 (Expr (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
44.11 (Const (\<^const_name>\<open>Test.solve_root_equ\<close>, _) $ Free ("e_e", _) $ Free ("v_v", _)) $
45.1 --- a/test/Tools/isac/ProgLang/tactical.sml Thu Sep 29 18:02:10 2022 +0200
45.2 +++ b/test/Tools/isac/ProgLang/tactical.sml Fri Oct 07 20:46:48 2022 +0200
45.3 @@ -17,7 +17,7 @@
45.4 "-------- fun Tactical.is ----------------------------------------------------------------------";
45.5 "-------- fun Tactical.is ----------------------------------------------------------------------";
45.6 "-------- fun Tactical.is ----------------------------------------------------------------------";
45.7 -val {scr = Prog t, ...} = MethodC.from_store ["simplification", "for_polynomials"];
45.8 +val {scr = Prog t, ...} = MethodC.from_store_PIDE ctxt ["simplification", "for_polynomials"];
45.9
45.10 if Tactical.is (Program.body_of t)
45.11 then error "Tactical.is body_of [simplification,for_polynomials]" else ();
45.12 @@ -25,11 +25,11 @@
45.13 "-------- fun contained_in ---------------------------------------------------------------------";
45.14 "-------- fun contained_in ---------------------------------------------------------------------";
45.15 "-------- fun contained_in ---------------------------------------------------------------------";
45.16 -val {scr = Prog t, ...} = MethodC.from_store ["simplification", "for_polynomials"];
45.17 +val {scr = Prog t, ...} = MethodC.from_store_PIDE ctxt ["simplification", "for_polynomials"];
45.18 if contained_in t then error "NOT Tactical.contained_in [simplification,for_polynomials]" else ();
45.19
45.20 -val {scr = Prog t, ...} = MethodC.from_store ["Test", "squ-equ-test-subpbl1"];
45.21 +val {scr = Prog t, ...} = MethodC.from_store_PIDE ctxt ["Test", "squ-equ-test-subpbl1"];
45.22 if contained_in t then () else error "Tactical.contained_in [Test,squ-equ-test-subpbl1]";
45.23
45.24 -val {scr = Prog t, ...} = MethodC.from_store ["simplification", "of_rationals"];
45.25 +val {scr = Prog t, ...} = MethodC.from_store_PIDE ctxt ["simplification", "of_rationals"];
45.26 if contained_in t then () else error "Tactical.contained_in [simplification,of_rationals]";
46.1 --- a/test/Tools/isac/Specify/o-model.sml Thu Sep 29 18:02:10 2022 +0200
46.2 +++ b/test/Tools/isac/Specify/o-model.sml Fri Oct 07 20:46:48 2022 +0200
46.3 @@ -32,7 +32,7 @@
46.4 "~~~~~ fun CalcTreeTEST , args:"; val [(fmz, sp)] = [(f_model, f_spec)];
46.5
46.6 (* val ((pt, p), tacis) =*)
46.7 -Step_Specify.nxt_specify_init_calc (fmz, sp);
46.8 +Step_Specify.nxt_specify_init_calc ctxt (fmz, sp);
46.9 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
46.10 (*val (_, hdl, (dI, pI, mI), pors, pctxt) = *)
46.11 initialise_PIDE (fmz, (dI, pI, mI));
47.1 --- a/test/Tools/isac/Specify/refine.sml Thu Sep 29 18:02:10 2022 +0200
47.2 +++ b/test/Tools/isac/Specify/refine.sml Fri Oct 07 20:46:48 2022 +0200
47.3 @@ -406,7 +406,7 @@
47.4 (*if*) p_ = Pos.Pbl (*then*);
47.5
47.6 val ("dummy", (Pbl, Refine_Problem ["sqroot-test", "univariate", "equation", "test"])) =
47.7 - for_problem oris (o_refs, refs) (pbl, met);
47.8 + for_problem_PIDE ctxt oris (o_refs, refs) (pbl, met);
47.9 "~~~~~ fun for_problem , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
47.10 (oris, (o_refs, refs), (pbl, met));
47.11 val cdI = if dI = ThyC.id_empty then dI' else dI;
47.12 @@ -414,7 +414,7 @@
47.13 val cpI = if pI = Problem.id_empty then pI' else pI;
47.14 val cmI = if mI = MethodC.id_empty then mI' else mI;
47.15 val {ppc = pbt, prls, where_, ...} = Problem.from_store_PIDE ctxt cpI;
47.16 - val {ppc = mpc, ...} = MethodC.from_store cmI
47.17 + val {ppc = mpc, ...} = MethodC.from_store_PIDE ctxt cmI
47.18 val (preok, (*+*)xxxxx(*+*) ) = Pre_Conds.check prls where_ pbl 0;
47.19 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
47.20 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
48.1 --- a/test/Tools/isac/Specify/specify.sml Thu Sep 29 18:02:10 2022 +0200
48.2 +++ b/test/Tools/isac/Specify/specify.sml Fri Oct 07 20:46:48 2022 +0200
48.3 @@ -126,7 +126,7 @@
48.4 val method_i_model= get_obj g_met pt (fst p); (* is still empty *)
48.5 if method_i_model = []then () else error "is still empty CHANGED";
48.6 val method_i_model = I_Model.complete o_model problem_i_model
48.7 - [] ((#ppc o MethodC.from_store) ["Diff_App", "max_by_calculus"]);
48.8 + [] ((#ppc o MethodC.from_store_PIDE ctxt) ["Diff_App", "max_by_calculus"]);
48.9 if I_Model.to_string ctxt method_i_model = "[\n" ^
48.10 "(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])), \n" ^
48.11 "(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A ,(m_m, [A])), \n" ^
48.12 @@ -252,7 +252,7 @@
48.13 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
48.14 ...} = Calc.specify_data (ctree, pos);
48.15 val (dI, _, _) = References.select_input o_refs refs;
48.16 - val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID
48.17 + val {ppc = m_patt, pre, prls, ...} = MethodC.from_store_PIDE ctxt mID
48.18 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
48.19 val (o_model', ctxt') =
48.20
48.21 @@ -328,7 +328,7 @@
48.22 (*NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
48.23 (*NEW*) ...} = Calc.specify_data (pt, pos);
48.24 (*NEW*) val (dI, _, mID) = References.select_input o_refs refs;
48.25 -(*NEW*) val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID
48.26 +(*NEW*) val {ppc = m_patt, pre, prls, ...} = MethodC.from_store_PIDE ctxt mID
48.27 (*NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
48.28 (*NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
48.29 (*NEW*) val thy = ThyC.get_theory dI
48.30 @@ -408,15 +408,15 @@
48.31 val ctxt = Ctree.get_ctxt pt pos;
48.32 (*if*) Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin (*else*);
48.33 (*if*) p_ = Pos.Pbl (*else*);
48.34 -val return = for_method oris (o_refs, refs) (pbl, met);
48.35 +val return = for_problem_PIDE ctxt oris (o_refs, refs) (pbl, met);
48.36 "~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
48.37 (oris, (o_refs, refs), (pbl, met));
48.38 val cmI = if mI = MethodC.id_empty then mI' else mI;
48.39 - val {ppc = mpc, prls, pre, ...} = MethodC.from_store cmI; (*..MethodC ?*)
48.40 + val {ppc = mpc, prls, pre, ...} = MethodC.from_store_PIDE ctxt cmI; (*..MethodC ?*)
48.41 val (preok, _) = Pre_Conds.check prls pre pbl 0;
48.42 "~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return);
48.43 (*/------------------- check within find_next_step -----------------------------------------\*)
48.44 -(*+*)Model_Pattern.to_string (MethodC.from_store mI' |> #ppc) = "[\"" ^
48.45 +(*+*)Model_Pattern.to_string (MethodC.from_store_PIDE ctxt mI' |> #ppc) = "[\"" ^
48.46 "(#Given, (Traegerlaenge, l))\", \"" ^
48.47 "(#Given, (Streckenlast, q))\", \"" ^
48.48 "(#Given, (FunktionsVariable, v))\", \"" ^ (* <---------- take m_field from here !!!*)
48.49 @@ -506,7 +506,7 @@
48.50 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
48.51 (*if*) p_ = Pos.Met (*then*);
48.52 val (i_model, m_patt) = (met,
48.53 - (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store |> #ppc)
48.54 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store_PIDE ctxt |> #ppc)
48.55
48.56 val Add (5, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) =
48.57 (*case*)
48.58 @@ -614,7 +614,7 @@
48.59 (*.NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,
48.60 (*.NEW*) ...} =Calc.specify_data (pt, pos);
48.61 (*.NEW*) val (dI, _, mID) = References.select_input o_refs refs;
48.62 -(*.NEW*) val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID
48.63 +(*.NEW*) val {ppc = m_patt, pre, prls, ...} = MethodC.from_store_PIDE ctxt mID
48.64 (*.NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
48.65 (*.NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt);
48.66
48.67 @@ -751,7 +751,7 @@
48.68
48.69 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
48.70 (*if*) p_ = Pos.Pbl (*else*);
48.71 -val return = for_method oris (o_refs, refs) (pbl, met);
48.72 +val return = for_method_PIDE ctxt oris (o_refs, refs) (pbl, met);
48.73 "~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return);
48.74
48.75 val ist_ctxt = Ctree.get_loc pt (p, p_)
48.76 @@ -779,7 +779,7 @@
48.77 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
48.78 (*if*) p_ = Pos.Met (*then*);
48.79 val (i_model, m_patt) = (met,
48.80 - (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store |> #ppc)
48.81 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store_PIDE ctxt |> #ppc)
48.82
48.83 val Add (4, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]), (Free ("id_fun", _), [Free ("y", _)]))) =
48.84 (*case*)
48.85 @@ -803,7 +803,7 @@
48.86 (*\------------------- check for entry to check_single -------------------------------------/*)
48.87
48.88 "~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
48.89 - (ctxt, sel, oris, met, ((#ppc o MethodC.from_store) cmI), ct);
48.90 + (ctxt, sel, oris, met, ((#ppc o MethodC.from_store_PIDE ctxt) cmI), ct);
48.91 val SOME t = (*case*) TermC.parseNEW ctxt str (*of*);
48.92
48.93 (*+*)val Const (\<^const_name>\<open>Biegelinie\<close>, _) $ Free ("y", _) = t;
48.94 @@ -852,7 +852,7 @@
48.95 "(#Relate, (Randbedingungen, r_b))\"]"
48.96 (*+*)then () else error "associate_input' Model_Pattern root-problem CHANGED";
48.97 (* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
48.98 -(*+*)if (MethodC.from_store ["Biegelinien", "ausBelastung"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
48.99 +(*+*)if (MethodC.from_store_PIDE ctxt ["Biegelinien", "ausBelastung"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
48.100 "(#Given, (Streckenlast, q__q))\", \"" ^
48.101 "(#Given, (FunktionsVariable, v_v))\", \"" ^
48.102 "(#Given, (Biegelinie, id_fun))\", \"" ^ (*--------------------------------- \<up> *)
49.1 --- a/test/Tools/isac/Test_Isac.thy Thu Sep 29 18:02:10 2022 +0200
49.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Oct 07 20:46:48 2022 +0200
49.3 @@ -183,7 +183,7 @@
49.4 ML_file "BaseDefinitions/calcelems.sml"
49.5 ML_file "BaseDefinitions/termC.sml"
49.6 ML_file "BaseDefinitions/substitution.sml"
49.7 - ML_file "BaseDefinitions/contextC.sml" (*!!!!! sometimes evaluates if separated into ML blocks*)
49.8 + ML_file "BaseDefinitions/contextC.sml"(*sometimes needs separation into ML blocks for evaluation*)
49.9 ML_file "BaseDefinitions/environment.sml"
49.10 (** )ML_file "BaseDefinitions/kestore.sml"( *setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
49.11 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
49.12 @@ -227,7 +227,7 @@
49.13 ML_file "MathEngBasic/thmC.sml"
49.14 ML_file "MathEngBasic/rewrite.sml"
49.15 ML_file "MathEngBasic/tactic.sml"
49.16 - ML_file "MathEngBasic/ctree.sml" (*if red, get the file into a text buffer -- this might clear*)
49.17 + ML_file "MathEngBasic/ctree.sml"
49.18 ML_file "MathEngBasic/calculation.sml"
49.19
49.20 ML_file "Specify/formalise.sml"
49.21 @@ -256,7 +256,7 @@
49.22 ML_file "MathEngine/fetch-tactics.sml"
49.23 ML_file "MathEngine/solve.sml"
49.24 ML_file "MathEngine/step.sml"
49.25 - ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*)
49.26 + ML_file "MathEngine/mathengine-stateless.sml"
49.27 ML_file "MathEngine/messages.sml"
49.28 ML_file "MathEngine/states.sml"
49.29
49.30 @@ -316,6 +316,12 @@
49.31
49.32 section \<open>further tests additional to src/.. files\<close>
49.33 ML_file "BridgeLibisabelle/use-cases.sml"
49.34 +ML \<open>
49.35 +\<close> ML \<open>
49.36 +\<close> ML \<open>
49.37 +\<close> ML \<open>
49.38 +\<close> ML \<open>
49.39 +\<close>
49.40
49.41 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
49.42 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
50.1 --- a/test/Tools/isac/Test_Isac_Short.thy Thu Sep 29 18:02:10 2022 +0200
50.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Fri Oct 07 20:46:48 2022 +0200
50.3 @@ -184,7 +184,7 @@
50.4 ML_file "BaseDefinitions/calcelems.sml"
50.5 ML_file "BaseDefinitions/termC.sml"
50.6 ML_file "BaseDefinitions/substitution.sml"
50.7 - ML_file "BaseDefinitions/contextC.sml" (*!!!!! sometimes evaluates if separated into ML blocks*)
50.8 + ML_file "BaseDefinitions/contextC.sml"(*sometimes needs separation into ML blocks for evaluation*)
50.9 ML_file "BaseDefinitions/environment.sml"
50.10 (**)ML_file "BaseDefinitions/kestore.sml"(*setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
50.11 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
51.1 --- a/test/Tools/isac/Test_Some.thy Thu Sep 29 18:02:10 2022 +0200
51.2 +++ b/test/Tools/isac/Test_Some.thy Fri Oct 07 20:46:48 2022 +0200
51.3 @@ -111,584 +111,6 @@
51.4 section \<open>===================================================================================\<close>
51.5 ML \<open>
51.6 \<close> ML \<open>
51.7 -(* Title: Knowledge/eqsystem-1.sml
51.8 - author: Walther Neuper 050826,
51.9 - (c) due to copyright terms
51.10 -*)
51.11 -
51.12 -"-----------------------------------------------------------------";
51.13 -"table of contents -----------------------------------------------";
51.14 -"-----------------------------------------------------------------";
51.15 -"----------- occur_exactly_in ------------------------------------";
51.16 -"----------- problems --------------------------------------------";
51.17 -"----------- rewrite-order ord_simplify_System -------------------";
51.18 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
51.19 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
51.20 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
51.21 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
51.22 -"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
51.23 -"----------- refine [linear,system]-------------------------------";
51.24 -"----------- refine [2x2,linear,system] search error--------------";
51.25 -(*^^^--- eqsystem-1.sml #####################################################################*)
51.26 -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
51.27 -(*^^^--- eqsystem-1a.sml #####################################################################
51.28 - vvv--- eqsystem-2.sml #####################################################################*)
51.29 -"----------- me [linear,system] ..normalise..top_down_sub..-------";
51.30 -"----------- all systems from Biegelinie -------------------------";
51.31 -"----------- 4x4 systems from Biegelinie -------------------------";
51.32 -"-----------------------------------------------------------------";
51.33 -"-----------------------------------------------------------------";
51.34 -"-----------------------------------------------------------------";
51.35 -
51.36 -val thy = @{theory "EqSystem"};
51.37 -val ctxt = Proof_Context.init_global thy;
51.38 -
51.39 -"----------- occur_exactly_in ------------------------------------";
51.40 -"----------- occur_exactly_in ------------------------------------";
51.41 -"----------- occur_exactly_in ------------------------------------";
51.42 -val all = [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"];
51.43 -val t = TermC.str2term"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
51.44 -
51.45 -if occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2"] all t
51.46 -then () else error "eqsystem.sml occur_exactly_in 1";
51.47 -
51.48 -if not (occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"] all t)
51.49 -then () else error "eqsystem.sml occur_exactly_in 2";
51.50 -
51.51 -if not (occur_exactly_in [TermC.str2term"c_2"] all t)
51.52 -then () else error "eqsystem.sml occur_exactly_in 3";
51.53 -
51.54 -val t = TermC.str2term"[c,c_2] from [c,c_2,c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
51.55 -eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
51.56 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
51.57 -if str = "[c, c_2] from [c, c_2,\n" ^
51.58 - " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"
51.59 -then () else error "eval_occur_exactly_in [c, c_2]";
51.60 -
51.61 -val t = TermC.str2term ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
51.62 - "- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");
51.63 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
51.64 -if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
51.65 -" c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
51.66 -then () else error "eval_occur_exactly_in [c, c_2, c_3]";
51.67 -
51.68 -val t = TermC.str2term"[c_2] from [c,c_2,c_3] occur_exactly_in \
51.69 - \- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
51.70 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
51.71 -if str = "[c_2] from [c, c_2,\n" ^
51.72 - " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
51.73 -then () else error "eval_occur_exactly_in [c, c_2, c_3]";
51.74 -
51.75 -val t = TermC.str2term"[] from [c,c_2,c_3] occur_exactly_in 0";
51.76 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
51.77 -if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
51.78 -else error "eval_occur_exactly_in [c, c_2, c_3]";
51.79 -
51.80 -val t =
51.81 - TermC.str2term
51.82 - "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) /2";
51.83 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
51.84 -if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
51.85 - \- 1 * (q_0 * L \<up> 2) / 2 = True" then ()
51.86 -else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
51.87 -
51.88 -"----------- problems --------------------------------------------";
51.89 -"----------- problems --------------------------------------------";
51.90 -"----------- problems --------------------------------------------";
51.91 -val t = TermC.str2term "Length [x+y=1,y=2] = 2";
51.92 -TermC.atomty t;
51.93 -val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty
51.94 - [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
51.95 - (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
51.96 - Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
51.97 - Eval (\<^const_name>\<open>HOL.eq\<close>,eval_equal "#equal_")
51.98 - ];
51.99 -val SOME (t',_) = rewrite_set_ ctxt false testrls t;
51.100 -if UnparseC.term t' = "True" then ()
51.101 -else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
51.102 -
51.103 -val SOME t = TermC.parseNEW ctxt "solution LL";
51.104 -TermC.atomty t;
51.105 -val SOME t = TermC.parseNEW ctxt "solution LL";
51.106 -TermC.atomty t;
51.107 -
51.108 -val t = TermC.str2term
51.109 -"(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
51.110 -TermC.atomty t;
51.111 -val t = TermC.str2term ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
51.112 - "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
51.113 -(*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
51.114 - assume flawed test setup hidden by "handle _ => ..."
51.115 - ERROR rewrite__set_ called with 'Erls' for '1 < 1'
51.116 -val SOME (t,_) =
51.117 - rewrite_set_ ctxt true
51.118 - (Rule_Set.append_rules "prls_" Rule_Set.empty
51.119 - [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
51.120 - Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
51.121 - Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}),
51.122 - Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}),
51.123 - Eval ("EqSystem.occur_exactly_in", eval_occur_exactly_in "#eval_occur_exactly_in_")
51.124 - ]) t;
51.125 -if t = @{term True} then ()
51.126 -else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
51.127 - broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite ---//*)
51.128 -
51.129 -
51.130 -"----------- rewrite-order ord_simplify_System -------------------";
51.131 -"----------- rewrite-order ord_simplify_System -------------------";
51.132 -"----------- rewrite-order ord_simplify_System -------------------";
51.133 -"M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
51.134 -"--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
51.135 -if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)",
51.136 - TermC.str2term"c * x") then ()
51.137 -else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
51.138 -
51.139 -if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)",
51.140 - TermC.str2term"c_2") then ()
51.141 -else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
51.142 -
51.143 -if ord_simplify_System false thy [] (TermC.str2term"c * x",
51.144 - TermC.str2term"c_2") then ()
51.145 -else error "integrate.sml, (c * x) < (c_2) not#3";
51.146 -
51.147 -"--- mult.commute ---";
51.148 -if ord_simplify_System false thy [] (TermC.str2term"x * c",
51.149 - TermC.str2term"c * x") then ()
51.150 -else error "integrate.sml, (x * c) < (c * x) not#4";
51.151 -
51.152 -if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c",
51.153 - TermC.str2term"- 1 * q_0 * c * (x \<up> 2 / 2)")
51.154 -then () else error "integrate.sml, (. * .) < (. * .) not#5";
51.155 -
51.156 -if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c",
51.157 - TermC.str2term"c * - 1 * q_0 * (x \<up> 2 / 2)")
51.158 -then () else error "integrate.sml, (. * .) < (. * .) not#6";
51.159 -
51.160 -
51.161 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
51.162 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
51.163 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
51.164 -val t = TermC.str2term"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\
51.165 - \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
51.166 -val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
51.167 - (TermC.str2term"bdv_2",TermC.str2term"c_2")];
51.168 -val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
51.169 -if UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
51.170 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
51.171 -
51.172 -val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
51.173 -if UnparseC.term t = "[L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2), c_2 = 0]"
51.174 -then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
51.175 -
51.176 -val SOME (t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
51.177 -if UnparseC.term t = "[L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0]"
51.178 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
51.179 -
51.180 -"--- 3--- see EqSystem.thy (*..if replaced by 'and' ...*)";
51.181 -val SOME (t,_) = rewrite_set_ ctxt true order_system t;
51.182 -if UnparseC.term t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"
51.183 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
51.184 -
51.185 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
51.186 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
51.187 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
51.188 -val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
51.189 -val ctxt = Proof_Context.init_global thy;
51.190 -val t =
51.191 - TermC.str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
51.192 - \ - 1 * q_0 / 24 * 0 \<up> 4),\
51.193 - \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
51.194 - \ - 1 * q_0 / 24 * L \<up> 4)]";
51.195 -val SOME (t, _) = rewrite_set_ ctxt true norm_Rational t;
51.196 -if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
51.197 - "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
51.198 - "[0 = c_2, 0 = (24 * c_2 + 24 * L * c + L \<up> 4 * q_0) / 24]"
51.199 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
51.200 -
51.201 -val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
51.202 -if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
51.203 - "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
51.204 - "[0 = c_2, 0 = q_0 * L \<up> 4 / 24 + (L * c + c_2)]"
51.205 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
51.206 -
51.207 -val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
51.208 -if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
51.209 - "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"*)
51.210 - "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / 24)]"
51.211 -then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
51.212 -
51.213 -val SOME(t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
51.214 -if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
51.215 - "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
51.216 - "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"
51.217 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
51.218 -
51.219 -val xxx = rewrite_set_ ctxt true order_system t;
51.220 -if is_none xxx
51.221 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
51.222 -
51.223 -
51.224 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
51.225 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
51.226 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
51.227 -val e1__ = TermC.str2term "c_2 = 77";
51.228 -val e2__ = TermC.str2term "L * c + c_2 = q_0 * L \<up> 2 / 2";
51.229 -val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
51.230 - (TermC.str2term"bdv_2",TermC.str2term"c_2")];
51.231 -val SOME (e2__,_) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty [e1__] e2__;
51.232 -if UnparseC.term e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
51.233 -else error "eqsystem.sml top_down_substitution,2x2] subst";
51.234 -
51.235 -val SOME (e2__,_) =
51.236 - rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized e2__;
51.237 -if UnparseC.term e2__ = "77 + L * c = q_0 * L \<up> 2 / 2" then ()
51.238 -else error "eqsystem.sml top_down_substitution,2x2] simpl_par";
51.239 -
51.240 -val SOME (e2__,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs e2__;
51.241 -if UnparseC.term e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()
51.242 -else error "eqsystem.sml top_down_substitution,2x2] isolate";
51.243 -
51.244 -val t = TermC.str2term "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
51.245 -val SOME (t,_) = rewrite_set_ ctxt true order_system t;
51.246 -if UnparseC.term t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()
51.247 -else error "eqsystem.sml top_down_substitution,2x2] order_system";
51.248 -
51.249 -if not (ord_simplify_System
51.250 - false thy []
51.251 - (TermC.str2term"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]",
51.252 - TermC.str2term"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]"))
51.253 -then () else error "eqsystem.sml, order_result rew_ord";
51.254 -
51.255 -
51.256 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
51.257 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
51.258 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
51.259 -(*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)
51.260 -val t = TermC.str2term (
51.261 - "[(0::real) = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4, " ^
51.262 - "(0::real) = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4, " ^
51.263 - "c + c_2 + c_3 + c_4 = 0, " ^
51.264 - "c_2 + c_3 + c_4 = 0]");
51.265 -val bdvs = [(TermC.str2term"bdv_1::real",TermC.str2term"c::real"),
51.266 - (TermC.str2term"bdv_2::real",TermC.str2term"c_2::real"),
51.267 - (TermC.str2term"bdv_3::real",TermC.str2term"c_3::real"),
51.268 - (TermC.str2term"bdv_4::real",TermC.str2term"c_4::real")];
51.269 -val SOME (t, _) =
51.270 - rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
51.271 -if UnparseC.term t = "[0 = c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4),\n c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
51.272 -then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
51.273 -
51.274 -val SOME (t, _) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
51.275 -if UnparseC.term t = "[c_4 = 0, \
51.276 - \L * c_3 + c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2),\n \
51.277 - \c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
51.278 -then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
51.279 -
51.280 -val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
51.281 -if UnparseC.term t = "[c_4 = 0,\
51.282 - \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
51.283 - \ c + (c_2 + (c_3 + c_4)) = 0,\n\
51.284 - \ c_2 + (c_3 + c_4) = 0]"
51.285 -then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
51.286 -
51.287 -val SOME (t, _) = rewrite_set_ ctxt true order_system t;
51.288 -if UnparseC.term t = "[c_4 = 0,\
51.289 - \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
51.290 - \ c_2 + (c_3 + c_4) = 0,\n\
51.291 - \ c + (c_2 + (c_3 + c_4)) = 0]"
51.292 -then () else error "eqsystem.sml rewrite in 4x4 order_system";
51.293 -
51.294 -\<close> ML \<open>
51.295 -"----------- refine [linear,system]-------------------------------";
51.296 -"----------- refine [linear,system]-------------------------------";
51.297 -"----------- refine [linear,system]-------------------------------";
51.298 -val fmz =
51.299 - ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
51.300 - "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]",
51.301 - "solveForVars [c, c_2]", "solution LL"];
51.302 -
51.303 -(*WN120313 in "solution L" above "Refine.refine_PIDE @{context} fmz ["LINEAR", "system"]" caused an error...*)
51.304 -"~~~~~ fun Refine.refine , args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);
51.305 -"~~~~~ fun refin' , args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
51.306 - ((rev o tl) pblID, fmz, [(*match list*)],
51.307 - ((Store.Node ("LINEAR", [Problem.from_store_PIDE ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));
51.308 - val {thy, ppc, where_, prls, ...} = py ;
51.309 -"~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, ppc);
51.310 - val ctxt = Proof_Context.init_global thy;
51.311 -"~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
51.312 - fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
51.313 - (_, _::_) => (Free (v,T)::get_vars vs)
51.314 - | (_, [] ) => get_vars vs) (*filter out nums as long as
51.315 - we have Free ("123",_)*)
51.316 - | get_vars [] = [];
51.317 - t = "equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,"^
51.318 - "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]";
51.319 - val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
51.320 -val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
51.321 -val ctxt = Variable.declare_constraints (nth 2 ts) ctxt;
51.322 -val ctxt = Variable.declare_constraints (nth 3 ts) ctxt;
51.323 -val ctxt = Variable.declare_constraints (nth 4 ts) ctxt;
51.324 - val t = nth 2 fmz; t = "solveForVars [c, c_2]";
51.325 - val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
51.326 -val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
51.327 - val t = nth 3 fmz; t = "solution LL";
51.328 - (*(Syntax.read_term ctxt t);
51.329 -Type unification failed: Clash of types "real" and "_ list"
51.330 -Type error in application: incompatible operand type
51.331 -
51.332 -Operator: solution :: bool list \<Rightarrow> toreall
51.333 -Operand: L :: real ========== L was already present in equalities ========== *)
51.334 -
51.335 -"===== case 1 =====";
51.336 -val matches = Refine.refine_PIDE @{context} fmz ["LINEAR", "system"];
51.337 -case matches of
51.338 - [M_Match.Matches (["LINEAR", "system"], _), (*Matches*)
51.339 - M_Match.Matches (["2x2", "LINEAR", "system"], _), (*NoMatch ! GOON !*)
51.340 - M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _), (**)
51.341 - M_Match.Matches (["normalise", "2x2", "LINEAR", "system"], (**)
51.342 - {Find = [Correct "solution LL"], With = [], (**)
51.343 - Given = [Correct "equalities\n [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
51.344 - Correct "solveForVars [c, c_2]"],
51.345 - Where = [],
51.346 - Relate = []})] => ()
51.347 -| _ => error "eqsystem.sml Refine.refine ['normalise','2x2'...]";
51.348 -
51.349 -"===== case 2 =====";
51.350 -val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
51.351 - "solveForVars [c, c_2]", "solution LL"];
51.352 -val matches = Refine.refine_PIDE @{context} fmz ["LINEAR", "system"];
51.353 -case matches of [_,_,
51.354 - M_Match.Matches
51.355 - (["triangular", "2x2", "LINEAR", "system"],
51.356 - {Find = [Correct "solution LL"],
51.357 - With = [],
51.358 - Given =
51.359 - [Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
51.360 - Correct "solveForVars [c, c_2]"],
51.361 - Where = [Correct
51.362 - "tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
51.363 - Correct
51.364 - "[c, c_2] from [c, c_2] occur_exactly_in NTH 2\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"],
51.365 - Relate = []})] => ()
51.366 -| _ => error "eqsystem.sml Refine.refine ['triangular','2x2'...]";
51.367 -
51.368 -(*WN051014-----------------------------------------------------------------------------------\\
51.369 - the above 'val matches = Refine.refine_PIDE @{context} fmz ["LINEAR", "system"]'
51.370 - didn't work anymore; we investigated in these steps:*)
51.371 -val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
51.372 - "solveForVars [c, c_2]", "solution LL"];
51.373 -val matches = Refine.refine_PIDE @{context} fmz ["triangular", "2x2", "LINEAR", "system"];
51.374 -(*... resulted in
51.375 - False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
51.376 - [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
51.377 -val t = TermC.str2term ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^
51.378 - "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]");
51.379 -
51.380 -val SOME (t', _) = rewrite_set_ ctxt false prls_triangular t;
51.381 -(*found:...
51.382 -## try thm: NTH_CONS
51.383 -### eval asms: 1 < 2 + - 1
51.384 -==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L \<up> 2 / 2] =
51.385 - nth_ (2 + - 1 + - 1) []
51.386 -#### rls: erls_prls_triangular on: 1 < 2 + - 1
51.387 -##### try calc: op <'
51.388 -### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + - 1"]
51.389 -
51.390 -... i.e Eval ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") was missing in erls_prls_triangular*)
51.391 -(*--------------------------------------------------------------------------------------------//*)
51.392 -
51.393 -
51.394 -"===== case 3: relaxed preconditions for triangular system =====";
51.395 -val fmz = ["equalities [L * q_0 = c, \
51.396 - \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
51.397 - \ 0 = c_4, \
51.398 - \ 0 = c_3]",
51.399 - "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
51.400 -(*============ inhibit exn WN120314 TODO: investigate type error (same) in these 2 cases:
51.401 -probably exn thrown by fun declare_constraints
51.402 -/-------------------------------------------------------\
51.403 -Type unification failed
51.404 -Type error in application: incompatible operand type
51.405 -
51.406 -Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
51.407 -Operand: [c_4] :: 'b list
51.408 -\-------------------------------------------------------/
51.409 -val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
51.410 -case TermC.matches of
51.411 - [M_Match.Matches (["LINEAR", "system"], _),
51.412 - M_Match.NoMatch (["2x2", "LINEAR", "system"], _),
51.413 - M_Match.NoMatch (["3x3", "LINEAR", "system"], _),
51.414 - M_Match.Matches (["4x4", "LINEAR", "system"], _),
51.415 - M_Match.NoMatch (["triangular", "4x4", "LINEAR", "system"], _),
51.416 - M_Match.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => ()
51.417 - | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
51.418 -(*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
51.419 -
51.420 -"===== case 4 =====";
51.421 -val fmz = ["equalities [L * q_0 = c, \
51.422 - \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
51.423 - \ 0 = c_3, \
51.424 - \ 0 = c_4]",
51.425 - "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
51.426 -val TermC.matches = Refine.refine fmz ["triangular", "4x4", "LINEAR", "system"];
51.427 -case TermC.matches of
51.428 - [M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => ()
51.429 - | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
51.430 -val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
51.431 -============ inhibit exn WN120314 ==============================================*)
51.432 -
51.433 -\<close> ML \<open>
51.434 -"----------- Refine.refine [2x2,linear,system] search error--------------";
51.435 -"----------- Refine.refine [2x2,linear,system] search error--------------";
51.436 -"----------- Refine.refine [2x2,linear,system] search error--------------";
51.437 -(*didn't go into ["2x2", "LINEAR", "system"];
51.438 - we investigated in these steps:*)
51.439 -val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
51.440 - \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
51.441 - "solveForVars [c, c_2]", "solution LL"];
51.442 -val matches = Refine.refine_PIDE @{context} fmz ["2x2", "LINEAR", "system"];
51.443 -(*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)
51.444 -(*brought: 'False "length_ es_ = 2"'*)
51.445 -
51.446 -(*-----fun refin' (pblRD:Problem.id_reverse) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
51.447 -(* val ((pblRD:Problem.id_reverse), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
51.448 - (rev ["LINEAR", "system"], fmz, [(*match list*)],
51.449 - ((Store.Node ("2x2",[Problem.from_store ["2x2", "LINEAR", "system"]],[])):pbt Store.store));
51.450 - *)
51.451 -> show_types:=true; UnparseC.term (hd where_); show_types:=false;
51.452 -val it = "length_ (es_::real list) = (2::real)" : string
51.453 -
51.454 -=========================================================================\
51.455 --------fun Problem.prep_input
51.456 -(* val (thy, (pblID, dsc_dats: (string * (string list)) list,
51.457 - ev:rls, ca: string option, metIDs:metID list)) =
51.458 - (EqSystem.thy, (["system"],
51.459 - [("#Given" ,["equalities es_", "solveForVars v_s"]),
51.460 - ("#Find" ,["solution ss___"](*___ is copy-named*))
51.461 - ],
51.462 - Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
51.463 - SOME "solveSystem es_ v_s",
51.464 - []));
51.465 - *)
51.466 -> val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
51.467 -val equalities_es_ = "equalities es_" : string
51.468 -> val (dd, ii) = (split_did o Thm.term_of o the o (TermC.parse thy)) equalities_es_;
51.469 -> show_types:=true; UnparseC.term ii; show_types:=false;
51.470 -val it = "es_::bool list" : string
51.471 -~~~~~~~~~~~~~~~ \<up> \<up> \<up> OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
51.472 -
51.473 -> val {where_,...} = Problem.from_store ["2x2", "LINEAR", "system"];
51.474 -> show_types:=true; UnparseC.term (hd where_); show_types:=false;
51.475 -
51.476 -=========================================================================/
51.477 -
51.478 ------fun refin' ff:
51.479 -> (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
51.480 -[
51.481 -(1 ,[1] ,true ,#Given ,Cor equalities
51.482 - [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
51.483 - 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2] ,(es_, [[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
51.484 - 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]])),
51.485 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
51.486 -(3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
51.487 -
51.488 -> (writeln o pres2str) pre';
51.489 -[
51.490 -(false, length_ es_ = 2),
51.491 -(true, length_ [c, c_2] = 2)]
51.492 -
51.493 ------ fun match_oris':
51.494 -> (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
51.495 -> (writeln o pres2str) pre';
51.496 -..as in refin'
51.497 -
51.498 ------ fun check in Pre_Conds.
51.499 -> (writeln o env2str) env;
51.500 -["
51.501 -(es_, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
51.502 - 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])", "
51.503 -(v_s, [c, c_2])", "
51.504 -(ss___, L)"]
51.505 -
51.506 -> val es_ = (fst o hd) env;
51.507 -val es_ = Free ("es_", "bool List.list") : Term.term
51.508 -
51.509 -> val pre1 = hd pres;
51.510 -TermC.atomty pre1;
51.511 -***
51.512 -*** Const (op =, [real, real] => bool)
51.513 -*** . Const (ListG.length_, real list => real)
51.514 -*** . . Free (es_, real list)
51.515 -~~~~~~~~~~~~~~~~~~~ \<up> \<up> \<up> should be bool list~~~~~~~~~~~~~~~~~~~
51.516 -*** . Free (2, real)
51.517 -***
51.518 -
51.519 -THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM
51.520 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
51.521 -*)
51.522 -
51.523 -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
51.524 -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
51.525 -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
51.526 -val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
51.527 - \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
51.528 - "solveForVars [c, c_2]", "solution LL"];
51.529 -val (dI',pI',mI') =
51.530 - ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
51.531 - ["EqSystem", "normalise", "2x2"]);
51.532 -val p = e_pos'; val c = [];
51.533 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
51.534 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
51.535 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
51.536 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
51.537 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
51.538 -case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()
51.539 - | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
51.540 -
51.541 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
51.542 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
51.543 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f(*["(bdv_1, c)", "(bdv_2, hd (tl [c, c_2] ... corrected srls; ran only AFTER use"RCODE-root.sml", store_met was NOT SUFFICIENT*);
51.544 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
51.545 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
51.546 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
51.547 -case nxt of
51.548 - (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
51.549 - | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";
51.550 -
51.551 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
51.552 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
51.553 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
51.554 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
51.555 -case nxt of
51.556 - (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
51.557 - | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
51.558 -
51.559 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
51.560 -val PblObj {probl,...} = get_obj I pt [5];
51.561 - (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl;
51.562 -(*[
51.563 -(1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
51.564 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
51.565 -(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
51.566 -*)
51.567 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
51.568 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
51.569 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
51.570 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
51.571 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
51.572 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
51.573 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
51.574 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
51.575 -case nxt of
51.576 - (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
51.577 - | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
51.578 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
51.579 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
51.580 -if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
51.581 -else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
51.582 -case nxt of
51.583 - (End_Proof') => ()
51.584 - | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
51.585 \<close> ML \<open>
51.586 \<close> ML \<open>
51.587 \<close>