1.1 --- a/TODO.md Wed Jul 27 13:11:43 2022 +0200
1.2 +++ b/TODO.md Wed Jul 27 13:59:58 2022 +0200
1.3 @@ -99,7 +99,7 @@
1.4
1.5 * WN: rename in Formalise: type spec = Model_Def.form_spec;
1.6 type refs = Model_Def.form_refs;
1.7 -* WN: rename in Know_Store: get_ptyps, add_pbts
1.8 +* WN: rename in Know_Store: get_ptyps, add_pbls
1.9 get_pbls, add_pbls
1.10 * WN: as soon as parsing in Outer_Syntax.command..‹Example› works, implement in Calculation
1.11 - init_ctree, update_status, check_input
2.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Jul 27 13:11:43 2022 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Jul 27 13:59:58 2022 +0200
2.3 @@ -72,8 +72,8 @@
2.4 val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory
2.5 val get_cas: theory -> CAS_Def.T list
2.6 val add_cas: CAS_Def.T list -> theory -> theory
2.7 - val get_ptyps: theory -> Probl_Def.store
2.8 - val add_pbts: (Probl_Def.T * References_Def.id) list -> theory -> theory
2.9 + val get_pbls: theory -> Probl_Def.store
2.10 + val add_pbls: (Probl_Def.T * References_Def.id) list -> theory -> theory
2.11 val get_mets: theory -> Meth_Def.store
2.12 val add_mets: (Meth_Def.T * References_Def.id) list -> theory -> theory
2.13 val get_thes: theory -> (Thy_Write.thydata Store.node) list
2.14 @@ -120,8 +120,8 @@
2.15 val extend = I;
2.16 val merge = Store.merge;
2.17 );
2.18 - fun get_ptyps thy = Data.get thy;
2.19 - fun add_pbts pbts thy = let
2.20 + fun get_pbls thy = Data.get thy;
2.21 + fun add_pbls pbts thy = let
2.22 fun add_pbt (pbt as {guh,...}, pblID) =
2.23 (* the pblID has the leaf-element as first; better readability achieved *)
2.24 (if (!Check_Unique.on) then Probl_Def.check_unique guh (Data.get thy) else ();
2.25 @@ -252,7 +252,7 @@
2.26
2.27 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
2.28
2.29 -fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps;
2.30 +fun get_pbls () = get_ref_thy () |> KEStore_Elems.get_pbls;
2.31 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
2.32 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
2.33 \<close>
3.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Jul 27 13:11:43 2022 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Jul 27 13:59:58 2022 +0200
3.3 @@ -80,7 +80,7 @@
3.4 " <ID> problem hierarchy </ID>\n" ^
3.5 " <NO> 1 </NO>\n" ^
3.6 " <CONTENTREF> pbl_ROOT </CONTENTREF>\n" ^
3.7 - (hierarchy_pbl (get_ptyps ())) ^
3.8 + (hierarchy_pbl (get_pbls ())) ^
3.9 "</NODE>");
3.10 fun met_hierarchy2file path =
3.11 (*str2file*) (path ^ "met_hierarchy.xml" : filepath,
4.1 --- a/src/Tools/isac/BridgeLibisabelle/present-tool.sml Wed Jul 27 13:11:43 2022 +0200
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/present-tool.sml Wed Jul 27 13:59:58 2022 +0200
4.3 @@ -37,7 +37,7 @@
4.4 | nodes ids gu (n :: ns) = case node ids gu n of
4.5 SOME id => SOME id
4.6 | NONE => nodes ids gu ns
4.7 - in case nodes [] guh (get_ptyps ()) of
4.8 + in case nodes [] guh (get_pbls ()) of
4.9 SOME id => rev id
4.10 | NONE => raise ERROR ("Ptool.guh2kestoreID: \"" ^ guh ^ "\" " ^ "not found in ptyps")
4.11 end
5.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Wed Jul 27 13:11:43 2022 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Wed Jul 27 13:59:58 2022 +0200
5.3 @@ -35,7 +35,7 @@
5.4 These items are contained in the ML_structure\<open>Context\<close> in current Isabelle,
5.5 thus all ML_structure\<open>KEStore_Elems\<close> can be replaced by more native Isabelle mechanisms --
5.6 with two exceptions
5.7 - \<^item> \<^ML>\<open>KEStore_Elems.add_pbts\<close> and \<^ML>\<open>KEStore_Elems.get_ptyps\<close>,
5.8 + \<^item> \<^ML>\<open>KEStore_Elems.add_pbls\<close> and \<^ML>\<open>KEStore_Elems.get_pbls\<close>,
5.9 handling a tree of \<^ML_type>\<open>Problem.T\<close>
5.10 \<^item> \<^ML>\<open>KEStore_Elems.add_mets\<close> and \<^ML>\<open>KEStore_Elems.get_mets\<close>,
5.11 handling a tree of \<^ML_type>\<open>MethodC.T\<close>
6.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Wed Jul 27 13:11:43 2022 +0200
6.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Wed Jul 27 13:59:58 2022 +0200
6.3 @@ -270,7 +270,7 @@
6.4 * in case there are no errors, do prep_input_PIDE (to be simplified)
6.5 *)
6.6 val arg = prep_input_PIDE thy name maa id_empty (pblID, model_input, input, cas, metIDs);
6.7 - in KEStore_Elems.add_pbts [arg] thy end)))
6.8 + in KEStore_Elems.add_pbls [arg] thy end)))
6.9
6.10 in end;
6.11
6.12 @@ -278,6 +278,6 @@
6.13
6.14 (** get Problem from Store **)
6.15
6.16 -fun from_store id = Store.get (get_ptyps ()) id (rev id);
6.17 +fun from_store id = Store.get (get_pbls ()) id (rev id);
6.18
6.19 (**)end(**)
7.1 --- a/src/Tools/isac/Specify/refine.sml Wed Jul 27 13:11:43 2022 +0200
7.2 +++ b/src/Tools/isac/Specify/refine.sml Wed Jul 27 13:59:58 2022 +0200
7.3 @@ -128,7 +128,7 @@
7.4 end;
7.5
7.6 fun problem thy pblID itms =
7.7 - case refined_ ((Store.apply (get_ptyps ())) (refin'' thy ((rev o tl) pblID) itms [])
7.8 + case refined_ ((Store.apply (get_pbls ())) (refin'' thy ((rev o tl) pblID) itms [])
7.9 pblID (rev pblID)) of
7.10 NONE => NONE
7.11 | SOME (Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd
7.12 @@ -193,7 +193,7 @@
7.13 \<close>
7.14
7.15 (* apply a fun to a ptyps node *)
7.16 -fun app_ptyp x = Store.apply (get_ptyps ()) x;
7.17 +fun app_ptyp x = Store.apply (get_pbls ()) x;
7.18
7.19 (* for tactic Refine_Tacitly
7.20 oris are already created wrt. some pbt; pbt contains thy for parsing *)
8.1 --- a/src/Tools/isac/Test_Code/test-tool.sml Wed Jul 27 13:11:43 2022 +0200
8.2 +++ b/src/Tools/isac/Test_Code/test-tool.sml Wed Jul 27 13:59:58 2022 +0200
8.3 @@ -28,16 +28,16 @@
8.4 fun format_pblID strl = enclose " [" "]" (commas_quote strl);
8.5 fun format_pblIDl strll = enclose "[\n" "\n]\n" (space_implode ",\n" (map format_pblID strll));
8.6
8.7 -fun show_ptyps () = (writeln o format_pblIDl o (Store.scan [])) (get_ptyps ()); (* for tests *)
8.8 -fun show_mets () = (writeln o format_pblIDl o (Store.scan [])) (get_mets ()); (* for tests *)
8.9 +fun show_ptyps () = (writeln o format_pblIDl o (Store.scan [])) (get_pbls ()); (* for tests *)
8.10 +fun show_mets () = (writeln o format_pblIDl o (Store.scan [])) (get_pbls ()); (* for tests *)
8.11
8.12 fun show_pblguhs () =
8.13 (tracing o strs2str o (map linefeed))
8.14 - (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id) (get_ptyps ()))
8.15 + (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id) (get_pbls ()))
8.16 fun sort_pblguhs () =
8.17 (tracing o strs2str o (map linefeed))
8.18 (((sort string_ord) o (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id)))
8.19 - (get_ptyps ()))
8.20 + (get_pbls ()))
8.21
8.22 fun show_metguhs () =
8.23 (tracing o strs2str o (map linefeed))
9.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Jul 27 13:11:43 2022 +0200
9.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Jul 27 13:59:58 2022 +0200
9.3 @@ -886,7 +886,7 @@
9.4 with \em SignalProcessing \normalfont and go on by creating the node
9.5 \em Z\_Transform\normalfont.\<close>
9.6
9.7 -setup \<open>KEStore_Elems.add_pbts
9.8 +setup \<open>KEStore_Elems.add_pbls
9.9 [Problem.prep_input @{theory} "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
9.10 Problem.prep_input @{theory} "pbl_SP_Ztrans" [] Problem.id_empty
9.11 (["Z_Transform", "SignalProcessing"], [], Rule_Set.empty, NONE, [])]\<close>
9.12 @@ -895,7 +895,7 @@
9.13 and output parameters. We already prepared their definition in
9.14 Section~\ref{sec:deffdes}.\<close>
9.15
9.16 -setup \<open>KEStore_Elems.add_pbts
9.17 +setup \<open>KEStore_Elems.add_pbls
9.18 [Problem.prep_input @{theory} "pbl_SP_Ztrans_inv" [] Problem.id_empty
9.19 (["Inverse", "Z_Transform", "SignalProcessing"],
9.20 [("#Given" ,["filterExpression X_eq"]),
10.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Wed Jul 27 13:11:43 2022 +0200
10.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Wed Jul 27 13:59:58 2022 +0200
10.3 @@ -55,7 +55,7 @@
10.4 (*WN: \<up> --- bitte nimm vorerst immer (theory "Isac_Knowledge"), damit wird richtig gematcht,
10.5 siehe unten. Wir werden w"ahrend der Arbeit auf diesen Fehler drauskommen*)
10.6
10.7 -KEStore_Elems.add_pbts
10.8 +KEStore_Elems.add_pbls
10.9 [Problem.prep_input (*Test.thy*) (theory "Isac_Knowledge")
10.10 (["rootX", "univariate", "equation", "test"],
10.11 [("#Given" ,["equality e_e", "solveFor v_v"]),
10.12 @@ -67,7 +67,7 @@
10.13
10.14 M_Match.match_pbl ["equality (sqrt(x)=1)", "solveFor x", "solutions L"] (Problem.from_store ["rootX", "univariate", "equation", "test"]);
10.15
10.16 -KEStore_Elems.add_pbts
10.17 +KEStore_Elems.add_pbls
10.18 [Problem.prep_input (theory "Isac_Knowledge")
10.19 (["approximate", "univariate", "equation", "test"],
10.20 [("#Given", ["equality e_e", "solveFor v_v", "errorBound err_"]),
11.1 --- a/test/Tools/isac/ProgLang/calculate.thy Wed Jul 27 13:11:43 2022 +0200
11.2 +++ b/test/Tools/isac/ProgLang/calculate.thy Wed Jul 27 13:59:58 2022 +0200
11.3 @@ -7,7 +7,7 @@
11.4 begin
11.5
11.6 text \<open>
11.7 - *setup* KEStore_Elems.add_pbts / add_mets is impossible in *.sml files.
11.8 + *setup* KEStore_Elems.add_pbls / add_mets is impossible in *.sml files.
11.9 The respective test/../evaluate.sml is called in Test_Isac.thy.
11.10 \<close>
11.11
11.12 @@ -17,7 +17,7 @@
11.13 "-calculate.thy: provides 'setup' -----------------------";
11.14 \<close>
11.15
11.16 -setup \<open>KEStore_Elems.add_pbts
11.17 +setup \<open>KEStore_Elems.add_pbls
11.18 [Problem.prep_input @{theory "Test"} "pbl_ttest" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, []),
11.19 Problem.prep_input @{theory "Test"} "pbl_ttest_calc" [] Problem.id_empty
11.20 (["calculate", "test"],
12.1 --- a/test/Tools/isac/Specify/refine.thy Wed Jul 27 13:11:43 2022 +0200
12.2 +++ b/test/Tools/isac/Specify/refine.thy Wed Jul 27 13:59:58 2022 +0200
12.3 @@ -8,12 +8,12 @@
12.4 begin
12.5
12.6 text \<open>
12.7 - *setup* KEStore_Elems.add_pbts is impossible in *.sml files.
12.8 + *setup* KEStore_Elems.add_pbls is impossible in *.sml files.
12.9 The respective test/../refine.sml is called in Test_Isac.thy.
12.10 \<close>
12.11
12.12 section \<open>data for test "-ptyps.thy: store test-pbtyps by 'setup' ---"\<close>
12.13 -setup \<open>KEStore_Elems.add_pbts
12.14 +setup \<open>KEStore_Elems.add_pbls
12.15 [(Problem.prep_input @{theory} "pbl_test_refine" [] Problem.id_empty
12.16 (["refine", "test"], [], Rule_Set.empty, NONE, [])),
12.17 (Problem.prep_input @{theory Diff_App} "pbl_pbla" [] Problem.id_empty