1.1 --- a/src/Tools/isac/BaseDefinitions/references-def.sml Fri May 27 12:07:55 2022 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/references-def.sml Fri May 27 15:12:54 2022 +0200
1.3 @@ -1,4 +1,4 @@
1.4 -(* Title: BaseDefinitions/specification.sml
1.5 +(* Title: BaseDefinitions/refernces-def.sml
1.6 Author: Walther Neuper
1.7 (c) due to copyright terms
1.8
2.1 --- a/src/Tools/isac/BaseDefinitions/theoryC.sml Fri May 27 12:07:55 2022 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml Fri May 27 15:12:54 2022 +0200
2.3 @@ -30,6 +30,7 @@
2.4 (**)
2.5
2.6 type id = string;
2.7 +val id_empty = "empty_thy_id";
2.8 fun cut_id dn = hd (space_explode "." dn);
2.9
2.10 val last_isabelle_thy = @{theory Complex_Main}
2.11 @@ -45,13 +46,12 @@
2.12 then Thy_Info.get_theory ("Interpret." ^ thyID)
2.13 else Thy_Info.get_theory ("Isac." ^ thyID);
2.14 fun get_theory thy =
2.15 - if thy = "empty_thy_id"
2.16 + if thy = id_empty
2.17 then (get_thy "Base_Tools") (*lower bound of Knowledge*)
2.18 else (get_thy thy) handle ERROR _ => raise ERROR ("ME_Isa: thy \"" ^ thy ^ "\" not in system");
2.19
2.20 fun id_to_ctxt thy' = Proof_Context.init_global (get_theory thy');
2.21
2.22 -val id_empty = "empty_thy_id";
2.23 fun Isac _ = Proof_Context.theory_of (id_to_ctxt "Isac_Knowledge");
2.24
2.25 fun parent_of thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1;
3.1 --- a/src/Tools/isac/Build_Isac.thy Fri May 27 12:07:55 2022 +0200
3.2 +++ b/src/Tools/isac/Build_Isac.thy Fri May 27 15:12:54 2022 +0200
3.3 @@ -174,6 +174,11 @@
3.4 (*declare [[ML_print_depth = 999]]*)
3.5 ML \<open>
3.6 \<close> ML \<open>
3.7 +ThyC.id_empty
3.8 +\<close> ML \<open>
3.9 +Problem.id_empty
3.10 +\<close> ML \<open>
3.11 +MethodC.id_empty
3.12 \<close> ML \<open>
3.13 \<close>
3.14 ML \<open>Eval.adhoc_thm; (*from "ProgLang/evaluate.sml" *)\<close>
4.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Fri May 27 12:07:55 2022 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Fri May 27 15:12:54 2022 +0200
4.3 @@ -46,6 +46,7 @@
4.4
4.5 ML \<open>
4.6 \<close> ML \<open>
4.7 +References.empty
4.8 \<close> ML \<open>
4.9 -\<close>
4.10 +(ThyC.id_empty, Problem.id_empty, MethodC.id_empty)\<close>
4.11 end
5.1 --- a/src/Tools/isac/MathEngBasic/references.sml Fri May 27 12:07:55 2022 +0200
5.2 +++ b/src/Tools/isac/MathEngBasic/references.sml Fri May 27 15:12:54 2022 +0200
5.3 @@ -1,4 +1,4 @@
5.4 -(* Title: BaseDefinitions/specification.sml
5.5 +(* Title: BaseDefinitions/references.sml
5.6 Author: Walther Neuper
5.7 (c) due to copyright terms
5.8
6.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Fri May 27 12:07:55 2022 +0200
6.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Fri May 27 15:12:54 2022 +0200
6.3 @@ -580,7 +580,7 @@
6.4 (*setContext 1 pos (Ptool.kestoreID2guh Ptool.Met_ ["Test", "solve_linear"]);*)
6.5 refFormula 1 (get_pos 1 1);
6.6 val ((pt,_),_) = get_calc 1;
6.7 - if get_obj g_spec pt [] = ("empty_thy_id",
6.8 + if get_obj g_spec pt [] = (ThyC.id_empty,
6.9 ["LINEAR", "univariate", "equation", "test"],
6.10 ["Test", "solve_linear"]) then ()
6.11 else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
6.12 @@ -1007,14 +1007,14 @@
6.13 P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
6.14 P_Spec.Relate ["relations [A=a*b, \
6.15 \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
6.16 - ("DiffApp", ["empty_probl_id"], ["empty_meth_id"]));
6.17 + ("DiffApp", Problem.id_empty, MethodC.id_empty));
6.18 modifyCalcHead 1 (([],Pbl), "not used here",
6.19 [P_Spec.Given ["fixedValues [r=Arbfix]"],
6.20 P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
6.21 P_Spec.Relate ["relations [A=a*b, \
6.22 \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
6.23 ("DiffApp", ["maximum_of", "function"],
6.24 - ["empty_meth_id"]));
6.25 + MethodC.id_empty));
6.26 modifyCalcHead 1 (([],Pbl), "not used here",
6.27 [P_Spec.Given ["fixedValues [r=Arbfix]"],
6.28 P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
6.29 @@ -1530,7 +1530,7 @@
6.30 "--------- UC errpat add-fraction, fillpat by input --------------";
6.31 "--------- UC errpat add-fraction, fillpat by input --------------";
6.32 (*cp from BridgeLog Java <=> SML*)
6.33 -CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
6.34 +CalcTree [([], References.empty)];
6.35 Iterator 1;
6.36 moveActiveRoot 1;
6.37 moveActiveFormula 1 ([],Pbl);
7.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Fri May 27 12:07:55 2022 +0200
7.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Fri May 27 15:12:54 2022 +0200
7.3 @@ -470,7 +470,7 @@
7.4 "--------- CAS-command on ([],Pbl) -------------------------------";
7.5 "--------- CAS-command on ([],Pbl) -------------------------------";
7.6 val (p,_,f,nxt,_,pt) =
7.7 - CalcTreeTEST [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
7.8 + CalcTreeTEST [([], References.empty)];
7.9 val ifo = "solve(x+1=2,x)";
7.10 val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt,p) "solve(x+1=2,x)";
7.11 (*
7.12 @@ -492,7 +492,7 @@
7.13 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
7.14 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
7.15 reset_states ();
7.16 -CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
7.17 +CalcTree [([], References.empty)];
7.18 Iterator 1;
7.19 moveActiveRoot 1;
7.20 replaceFormula 1 "solve(x+1=2,x)";
7.21 @@ -644,7 +644,7 @@
7.22 TermC.atomty t;
7.23 "-----------------------------------------------------------------";
7.24 (*1>*)reset_states ();
7.25 -(*2>*)CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
7.26 +(*2>*)CalcTree [([], References.empty)];
7.27 (*3>*)Iterator 1;moveActiveRoot 1;
7.28 "----- here the Headline has been finished";
7.29 (*4>*)moveActiveFormula 1 ([],Pbl);
7.30 @@ -744,7 +744,7 @@
7.31 "--------- implicit_take, start with <NEW> (CAS input) ---------------";
7.32 "--------- implicit_take, start with <NEW> (CAS input) ---------------";
7.33 reset_states ();
7.34 -CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
7.35 +CalcTree [([], References.empty)];
7.36 (*[[from sml: > @@@@@begin@@@@@
7.37 [[from sml: 1
7.38 [[from sml: <CALCTREE>
8.1 --- a/test/Tools/isac/Knowledge/equation.sml Fri May 27 12:07:55 2022 +0200
8.2 +++ b/test/Tools/isac/Knowledge/equation.sml Fri May 27 15:12:54 2022 +0200
8.3 @@ -18,7 +18,7 @@
8.4 "----------- CAS input -------------------------------------------";
8.5 "----------- CAS input -------------------------------------------";
8.6 reset_states ();
8.7 -CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
8.8 +CalcTree [([], References.empty)];
8.9 Iterator 1;
8.10 moveActiveRoot 1;
8.11 replaceFormula 1 "solve (x+1=2, x)";
9.1 --- a/test/Tools/isac/Knowledge/inssort.sml Fri May 27 12:07:55 2022 +0200
9.2 +++ b/test/Tools/isac/Knowledge/inssort.sml Fri May 27 15:12:54 2022 +0200
9.3 @@ -119,7 +119,7 @@
9.4 "----------- insertion sort: CAS-command -------------------------------------";
9.5 "----------- insertion sort: CAS-command -------------------------------------";
9.6 "----------- insertion sort: CAS-command -------------------------------------";
9.7 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
9.8 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [([], References.empty)];
9.9 (*+*)if ((fst p) |> get_obj g_origin pt |> LibraryC.fst3) = []
9.10 (*+*)then () else error "check correct of get_ctxt at start of (sub-)problem";
9.11 val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt, p) "Sort {||1, 3, 2||}";
10.1 --- a/test/Tools/isac/Knowledge/simplify.sml Fri May 27 12:07:55 2022 +0200
10.2 +++ b/test/Tools/isac/Knowledge/simplify.sml Fri May 27 15:12:54 2022 +0200
10.3 @@ -19,7 +19,7 @@
10.4 "----------- CAS-command Simplify -----------------------";
10.5 "----------- CAS-command Simplify -----------------------";
10.6 reset_states ();
10.7 -CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
10.8 +CalcTree [([], References.empty)];
10.9 Iterator 1;
10.10 moveActiveRoot 1;
10.11 replaceFormula 1 "Simplify (2*a + 3*a)";
11.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Fri May 27 12:07:55 2022 +0200
11.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Fri May 27 15:12:54 2022 +0200
11.3 @@ -134,7 +134,7 @@
11.4 "~~~~~ fun References.select, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);
11.5 dI = ThyC.id_empty; (*true*)
11.6 odI = "Build_Inverse_Z_Transform"; (*true*)
11.7 -dI = "empty_thy_id"; (*true*)
11.8 +dI = ThyC.id_empty; (*true*)
11.9 "~~~~~ after fun References.select:";
11.10 val (dI, pI, mI) = References.select ospec spec;
11.11 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
12.1 --- a/test/Tools/isac/MathEngine/step.sml Fri May 27 12:07:55 2022 +0200
12.2 +++ b/test/Tools/isac/MathEngine/step.sml Fri May 27 15:12:54 2022 +0200
12.3 @@ -428,12 +428,12 @@
12.4 EmptyPtree;
12.5 val nxt = tac2tac_ pt p nxt;
12.6 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
12.7 -(*val nxt = Specify_Theory "empty_thy_id" : tac*)
12.8 +(*val nxt = Specify_Theory ThyC.id_empty : tac*)
12.9
12.10 val nxt = Specify_Theory "DiffApp";
12.11 val nxt = tac2tac_ pt p nxt;
12.12 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
12.13 -(*val nxt = Specify_Problem ["empty_probl_id"] : tac*)
12.14 +(*val nxt = Specify_Problem Problem.id_empty : tac*)
12.15
12.16 val nxt = Specify_Problem ["maximum_of", "function"];
12.17 val nxt = tac2tac_ pt p nxt;
12.18 @@ -469,7 +469,7 @@
12.19 val nxt = Add_Relation "relations [(A=a+b)]";
12.20 val nxt = tac2tac_ pt p nxt;
12.21 val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
12.22 -(*val nxt = Specify_Method ("empty_thy_id", "empty_meth_id") : tac*)
12.23 +(*val nxt = Specify_Method (ThyC.id_empty, MethodC.id_empty) : tac*)
12.24
12.25 val nxt = Specify_Method ["DiffApp", "max_by_calculus"];
12.26 val nxt = tac2tac_ pt p nxt;
13.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Fri May 27 12:07:55 2022 +0200
13.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Fri May 27 15:12:54 2022 +0200
13.3 @@ -268,15 +268,15 @@
13.4 val pt = update_met pt [] [];
13.5 (*
13.6 > get_obj g_spec pt [];
13.7 -val it = ("empty_thy_id",["empty_probl_id"],("empty_thy_id", "empty_meth_id")) : spec
13.8 +val it = (ThyC.id_empty,Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : spec
13.9 > val pt = update_domID pt [] "RatArith";
13.10 > get_obj g_spec pt [];
13.11 -val it = ("RatArith",["empty_probl_id"],("empty_thy_id", "empty_meth_id")) : spec
13.12 +val it = ("RatArith",Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : spec
13.13 > val pt = update_pblID pt [] ["RatArith",
13.14 "equations", "univariate", "square-root"];
13.15 > get_obj g_spec pt [];
13.16 ("RatArith",["RatArith", "equations", "univariate", "square-root"],
13.17 - ("empty_thy_id", "empty_meth_id")) : spec
13.18 + (ThyC.id_empty, MethodC.id_empty)) : spec
13.19 > val pt = update_metID pt [] ("RatArith", "sqrt-equ-test");
13.20 > get_obj g_spec pt [];
13.21 ("RatArith",["RatArith", "equations", "univariate", "square-root"],
13.22 @@ -402,7 +402,7 @@
13.23 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.24 (* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl");
13.25 > get_obj g_spec pt (fst p);
13.26 -val it = ("empty_thy_id",["empty_probl_id"],("empty_thy_id", "empty_meth_id")) : spec*)
13.27 +val it = (ThyC.id_empty,Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : spec*)
13.28 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
13.29 (*val nxt = ("Specify_Problem", Specify_Problem *)
13.30 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
14.1 --- a/test/Tools/isac/Specify/step-specify.sml Fri May 27 12:07:55 2022 +0200
14.2 +++ b/test/Tools/isac/Specify/step-specify.sml Fri May 27 15:12:54 2022 +0200
14.3 @@ -28,7 +28,7 @@
14.4 pt;(*isa==REP*)
14.5 val (_, ("Integrate", ["integrate", "function"], ["diff", "integration"]), _)
14.6 = get_obj g_origin pt (fst p);
14.7 -get_obj g_spec pt (fst p) = ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]); (*isa==REP*)
14.8 +get_obj g_spec pt (fst p) = References.empty; (*isa==REP*)
14.9
14.10 (*this steps into according to "----- step 2 ---" below*)
14.11 "~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, (Steps 1));
14.12 @@ -70,7 +70,7 @@
14.13 Nd (PblObj
14.14 :
14.15 result = (Const ("empty", "??.'a"), []), spec =
14.16 - ("Integrate", ["integrate", "function"], ["empty_meth_id"])},
14.17 + ("Integrate", ["integrate", "function"], MethodC.id_empty)},
14.18 []):
14.19 ctree*)
14.20