# HG changeset patch # User wneuper # Date 1653657174 -7200 # Node ID 203438ff792fe233d1814efae9c57f93fc567d59 # Parent aa835b157a2a5ba46000d9d8e134ca9067fc4438 replace literals with constants diff -r aa835b157a2a -r 203438ff792f src/Tools/isac/BaseDefinitions/references-def.sml --- a/src/Tools/isac/BaseDefinitions/references-def.sml Fri May 27 12:07:55 2022 +0200 +++ b/src/Tools/isac/BaseDefinitions/references-def.sml Fri May 27 15:12:54 2022 +0200 @@ -1,4 +1,4 @@ -(* Title: BaseDefinitions/specification.sml +(* Title: BaseDefinitions/refernces-def.sml Author: Walther Neuper (c) due to copyright terms diff -r aa835b157a2a -r 203438ff792f src/Tools/isac/BaseDefinitions/theoryC.sml --- a/src/Tools/isac/BaseDefinitions/theoryC.sml Fri May 27 12:07:55 2022 +0200 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml Fri May 27 15:12:54 2022 +0200 @@ -30,6 +30,7 @@ (**) type id = string; +val id_empty = "empty_thy_id"; fun cut_id dn = hd (space_explode "." dn); val last_isabelle_thy = @{theory Complex_Main} @@ -45,13 +46,12 @@ then Thy_Info.get_theory ("Interpret." ^ thyID) else Thy_Info.get_theory ("Isac." ^ thyID); fun get_theory thy = - if thy = "empty_thy_id" + if thy = id_empty then (get_thy "Base_Tools") (*lower bound of Knowledge*) else (get_thy thy) handle ERROR _ => raise ERROR ("ME_Isa: thy \"" ^ thy ^ "\" not in system"); fun id_to_ctxt thy' = Proof_Context.init_global (get_theory thy'); -val id_empty = "empty_thy_id"; fun Isac _ = Proof_Context.theory_of (id_to_ctxt "Isac_Knowledge"); fun parent_of thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1; diff -r aa835b157a2a -r 203438ff792f src/Tools/isac/Build_Isac.thy --- a/src/Tools/isac/Build_Isac.thy Fri May 27 12:07:55 2022 +0200 +++ b/src/Tools/isac/Build_Isac.thy Fri May 27 15:12:54 2022 +0200 @@ -174,6 +174,11 @@ (*declare [[ML_print_depth = 999]]*) ML \ \ ML \ +ThyC.id_empty +\ ML \ +Problem.id_empty +\ ML \ +MethodC.id_empty \ ML \ \ ML \Eval.adhoc_thm; (*from "ProgLang/evaluate.sml" *)\ diff -r aa835b157a2a -r 203438ff792f src/Tools/isac/MathEngBasic/MathEngBasic.thy --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Fri May 27 12:07:55 2022 +0200 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Fri May 27 15:12:54 2022 +0200 @@ -46,6 +46,7 @@ ML \ \ ML \ +References.empty \ ML \ -\ +(ThyC.id_empty, Problem.id_empty, MethodC.id_empty)\ end diff -r aa835b157a2a -r 203438ff792f src/Tools/isac/MathEngBasic/references.sml --- a/src/Tools/isac/MathEngBasic/references.sml Fri May 27 12:07:55 2022 +0200 +++ b/src/Tools/isac/MathEngBasic/references.sml Fri May 27 15:12:54 2022 +0200 @@ -1,4 +1,4 @@ -(* Title: BaseDefinitions/specification.sml +(* Title: BaseDefinitions/references.sml Author: Walther Neuper (c) due to copyright terms diff -r aa835b157a2a -r 203438ff792f test/Tools/isac/BridgeLibisabelle/use-cases.sml --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Fri May 27 12:07:55 2022 +0200 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Fri May 27 15:12:54 2022 +0200 @@ -580,7 +580,7 @@ (*setContext 1 pos (Ptool.kestoreID2guh Ptool.Met_ ["Test", "solve_linear"]);*) refFormula 1 (get_pos 1 1); val ((pt,_),_) = get_calc 1; - if get_obj g_spec pt [] = ("empty_thy_id", + if get_obj g_spec pt [] = (ThyC.id_empty, ["LINEAR", "univariate", "equation", "test"], ["Test", "solve_linear"]) then () else error "FE-interface.sml: diff.behav. in setProblem, setMethod"; @@ -1007,14 +1007,14 @@ P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)], P_Spec.Relate ["relations [A=a*b, \ \(a/2) \ 2 + (b/2) \ 2 = r \ 2]"]], Pbl, - ("DiffApp", ["empty_probl_id"], ["empty_meth_id"])); + ("DiffApp", Problem.id_empty, MethodC.id_empty)); modifyCalcHead 1 (([],Pbl), "not used here", [P_Spec.Given ["fixedValues [r=Arbfix]"], P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)], P_Spec.Relate ["relations [A=a*b, \ \(a/2) \ 2 + (b/2) \ 2 = r \ 2]"]], Pbl, ("DiffApp", ["maximum_of", "function"], - ["empty_meth_id"])); + MethodC.id_empty)); modifyCalcHead 1 (([],Pbl), "not used here", [P_Spec.Given ["fixedValues [r=Arbfix]"], P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)], @@ -1530,7 +1530,7 @@ "--------- UC errpat add-fraction, fillpat by input --------------"; "--------- UC errpat add-fraction, fillpat by input --------------"; (*cp from BridgeLog Java <=> SML*) -CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))]; +CalcTree [([], References.empty)]; Iterator 1; moveActiveRoot 1; moveActiveFormula 1 ([],Pbl); diff -r aa835b157a2a -r 203438ff792f test/Tools/isac/Interpret/error-pattern.sml --- a/test/Tools/isac/Interpret/error-pattern.sml Fri May 27 12:07:55 2022 +0200 +++ b/test/Tools/isac/Interpret/error-pattern.sml Fri May 27 15:12:54 2022 +0200 @@ -470,7 +470,7 @@ "--------- CAS-command on ([],Pbl) -------------------------------"; "--------- CAS-command on ([],Pbl) -------------------------------"; val (p,_,f,nxt,_,pt) = - CalcTreeTEST [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))]; + CalcTreeTEST [([], References.empty)]; val ifo = "solve(x+1=2,x)"; val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt,p) "solve(x+1=2,x)"; (* @@ -492,7 +492,7 @@ "--------- CAS-command on ([],Pbl) FE-interface ------------------"; "--------- CAS-command on ([],Pbl) FE-interface ------------------"; reset_states (); -CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))]; +CalcTree [([], References.empty)]; Iterator 1; moveActiveRoot 1; replaceFormula 1 "solve(x+1=2,x)"; @@ -644,7 +644,7 @@ TermC.atomty t; "-----------------------------------------------------------------"; (*1>*)reset_states (); -(*2>*)CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))]; +(*2>*)CalcTree [([], References.empty)]; (*3>*)Iterator 1;moveActiveRoot 1; "----- here the Headline has been finished"; (*4>*)moveActiveFormula 1 ([],Pbl); @@ -744,7 +744,7 @@ "--------- implicit_take, start with (CAS input) ---------------"; "--------- implicit_take, start with (CAS input) ---------------"; reset_states (); -CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))]; +CalcTree [([], References.empty)]; (*[[from sml: > @@@@@begin@@@@@ [[from sml: 1 [[from sml: diff -r aa835b157a2a -r 203438ff792f test/Tools/isac/Knowledge/equation.sml --- a/test/Tools/isac/Knowledge/equation.sml Fri May 27 12:07:55 2022 +0200 +++ b/test/Tools/isac/Knowledge/equation.sml Fri May 27 15:12:54 2022 +0200 @@ -18,7 +18,7 @@ "----------- CAS input -------------------------------------------"; "----------- CAS input -------------------------------------------"; reset_states (); -CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))]; +CalcTree [([], References.empty)]; Iterator 1; moveActiveRoot 1; replaceFormula 1 "solve (x+1=2, x)"; diff -r aa835b157a2a -r 203438ff792f test/Tools/isac/Knowledge/inssort.sml --- a/test/Tools/isac/Knowledge/inssort.sml Fri May 27 12:07:55 2022 +0200 +++ b/test/Tools/isac/Knowledge/inssort.sml Fri May 27 15:12:54 2022 +0200 @@ -119,7 +119,7 @@ "----------- insertion sort: CAS-command -------------------------------------"; "----------- insertion sort: CAS-command -------------------------------------"; "----------- insertion sort: CAS-command -------------------------------------"; -val (p,_,f,nxt,_,pt) = CalcTreeTEST [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))]; +val (p,_,f,nxt,_,pt) = CalcTreeTEST [([], References.empty)]; (*+*)if ((fst p) |> get_obj g_origin pt |> LibraryC.fst3) = [] (*+*)then () else error "check correct of get_ctxt at start of (sub-)problem"; val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt, p) "Sort {||1, 3, 2||}"; diff -r aa835b157a2a -r 203438ff792f test/Tools/isac/Knowledge/simplify.sml --- a/test/Tools/isac/Knowledge/simplify.sml Fri May 27 12:07:55 2022 +0200 +++ b/test/Tools/isac/Knowledge/simplify.sml Fri May 27 15:12:54 2022 +0200 @@ -19,7 +19,7 @@ "----------- CAS-command Simplify -----------------------"; "----------- CAS-command Simplify -----------------------"; reset_states (); -CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))]; +CalcTree [([], References.empty)]; Iterator 1; moveActiveRoot 1; replaceFormula 1 "Simplify (2*a + 3*a)"; diff -r aa835b157a2a -r 203438ff792f test/Tools/isac/MathEngine/mathengine-stateless.sml --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Fri May 27 12:07:55 2022 +0200 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Fri May 27 15:12:54 2022 +0200 @@ -134,7 +134,7 @@ "~~~~~ fun References.select, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec); dI = ThyC.id_empty; (*true*) odI = "Build_Inverse_Z_Transform"; (*true*) -dI = "empty_thy_id"; (*true*) +dI = ThyC.id_empty; (*true*) "~~~~~ after fun References.select:"; val (dI, pI, mI) = References.select ospec spec; "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*) diff -r aa835b157a2a -r 203438ff792f test/Tools/isac/MathEngine/step.sml --- a/test/Tools/isac/MathEngine/step.sml Fri May 27 12:07:55 2022 +0200 +++ b/test/Tools/isac/MathEngine/step.sml Fri May 27 15:12:54 2022 +0200 @@ -428,12 +428,12 @@ EmptyPtree; val nxt = tac2tac_ pt p nxt; val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; -(*val nxt = Specify_Theory "empty_thy_id" : tac*) +(*val nxt = Specify_Theory ThyC.id_empty : tac*) val nxt = Specify_Theory "DiffApp"; val nxt = tac2tac_ pt p nxt; val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; -(*val nxt = Specify_Problem ["empty_probl_id"] : tac*) +(*val nxt = Specify_Problem Problem.id_empty : tac*) val nxt = Specify_Problem ["maximum_of", "function"]; val nxt = tac2tac_ pt p nxt; @@ -469,7 +469,7 @@ val nxt = Add_Relation "relations [(A=a+b)]"; val nxt = tac2tac_ pt p nxt; val(p,_, Test_Out.PpcKF ppc, nxt,_,pt) = specify nxt p [] pt; -(*val nxt = Specify_Method ("empty_thy_id", "empty_meth_id") : tac*) +(*val nxt = Specify_Method (ThyC.id_empty, MethodC.id_empty) : tac*) val nxt = Specify_Method ["DiffApp", "max_by_calculus"]; val nxt = tac2tac_ pt p nxt; diff -r aa835b157a2a -r 203438ff792f test/Tools/isac/OLDTESTS/root-equ.sml --- a/test/Tools/isac/OLDTESTS/root-equ.sml Fri May 27 12:07:55 2022 +0200 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Fri May 27 15:12:54 2022 +0200 @@ -268,15 +268,15 @@ val pt = update_met pt [] []; (* > get_obj g_spec pt []; -val it = ("empty_thy_id",["empty_probl_id"],("empty_thy_id", "empty_meth_id")) : spec +val it = (ThyC.id_empty,Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : spec > val pt = update_domID pt [] "RatArith"; > get_obj g_spec pt []; -val it = ("RatArith",["empty_probl_id"],("empty_thy_id", "empty_meth_id")) : spec +val it = ("RatArith",Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : spec > val pt = update_pblID pt [] ["RatArith", "equations", "univariate", "square-root"]; > get_obj g_spec pt []; ("RatArith",["RatArith", "equations", "univariate", "square-root"], - ("empty_thy_id", "empty_meth_id")) : spec + (ThyC.id_empty, MethodC.id_empty)) : spec > val pt = update_metID pt [] ("RatArith", "sqrt-equ-test"); > get_obj g_spec pt []; ("RatArith",["RatArith", "equations", "univariate", "square-root"], @@ -402,7 +402,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl"); > get_obj g_spec pt (fst p); -val it = ("empty_thy_id",["empty_probl_id"],("empty_thy_id", "empty_meth_id")) : spec*) +val it = (ThyC.id_empty,Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : spec*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*val nxt = ("Specify_Problem", Specify_Problem *) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; diff -r aa835b157a2a -r 203438ff792f test/Tools/isac/Specify/step-specify.sml --- a/test/Tools/isac/Specify/step-specify.sml Fri May 27 12:07:55 2022 +0200 +++ b/test/Tools/isac/Specify/step-specify.sml Fri May 27 15:12:54 2022 +0200 @@ -28,7 +28,7 @@ pt;(*isa==REP*) val (_, ("Integrate", ["integrate", "function"], ["diff", "integration"]), _) = get_obj g_origin pt (fst p); -get_obj g_spec pt (fst p) = ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]); (*isa==REP*) +get_obj g_spec pt (fst p) = References.empty; (*isa==REP*) (*this steps into according to "----- step 2 ---" below*) "~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, (Steps 1)); @@ -70,7 +70,7 @@ Nd (PblObj : result = (Const ("empty", "??.'a"), []), spec = - ("Integrate", ["integrate", "function"], ["empty_meth_id"])}, + ("Integrate", ["integrate", "function"], MethodC.id_empty)}, []): ctree*)