1.1 --- a/TODO.md Tue Jul 26 22:29:35 2022 +0200
1.2 +++ b/TODO.md Wed Jul 27 13:11:43 2022 +0200
1.3 @@ -101,8 +101,6 @@
1.4 type refs = Model_Def.form_refs;
1.5 * WN: rename in Know_Store: get_ptyps, add_pbts
1.6 get_pbls, add_pbls
1.7 -* WN: rename in References_Def: select
1.8 - select_new
1.9 * WN: as soon as parsing in Outer_Syntax.command..‹Example› works, implement in Calculation
1.10 - init_ctree, update_status, check_input
1.11
2.1 --- a/src/Tools/isac/BaseDefinitions/references-def.sml Tue Jul 26 22:29:35 2022 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/references-def.sml Wed Jul 27 13:11:43 2022 +0200
2.3 @@ -1,4 +1,4 @@
2.4 -(* Title: BaseDefinitions/refernces-def.sml
2.5 +(* Title: BaseDefinitions/references-def.sml
2.6 Author: Walther Neuper
2.7 (c) due to copyright terms
2.8
2.9 @@ -17,7 +17,7 @@
2.10 val empty: T
2.11 val to_string: string * string list * string list -> string
2.12
2.13 - val select : T -> T -> T
2.14 + val select_input : T -> T -> T
2.15 end
2.16
2.17 (**)
2.18 @@ -41,8 +41,8 @@
2.19 "(" ^ quote dom ^ ", " ^ strs2str pbl ^ ", " ^ strs2str met ^ ")";
2.20 val empty = (ThyC.id_empty, empty_probl_id, empty_meth_id);
2.21
2.22 -(* select a Specification; if still unspecified take it from PblObj.origin *)
2.23 -fun select (odI, opI, omI) (dI, pI, mI) =
2.24 +(* select_input a Specification; if still unspecified take it from PblObj.origin *)
2.25 +fun select_input (odI, opI, omI) (dI, pI, mI) =
2.26 (if dI = ThyC.id_empty then odI else dI,
2.27 if pI = empty_probl_id then opI else pI,
2.28 if mI = empty_meth_id then omI else mI);
3.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Tue Jul 26 22:29:35 2022 +0200
3.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Wed Jul 27 13:11:43 2022 +0200
3.3 @@ -136,7 +136,7 @@
3.4 val _ = if meth_id <> omet then "switch from probl check_input of meth" else "do nothing"
3.5 in
3.6 Ctree.Nd (Ctree.PblObj {
3.7 - fmz = fmz, origin = origin, spec = References.select spec (thy_id, probl_id, meth_id),
3.8 + fmz = fmz, origin = origin, spec = References.select_input spec (thy_id, probl_id, meth_id),
3.9 probl = check_input model, meth = meth, (*TODO +switch Problem_Ref | Method_Ref*)
3.10 ctxt = ctxt, loc = loc,
3.11 branch = branch, ostate = ostate, result = result}, children)
4.1 --- a/src/Tools/isac/MathEngBasic/calculation.sml Tue Jul 26 22:29:35 2022 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/calculation.sml Wed Jul 27 13:11:43 2022 +0200
4.3 @@ -52,7 +52,7 @@
4.4 let
4.5 val (p', _) = if Pos.on_specification pos then pos else (Ctree.par_pblobj pt p, p_)
4.6 in
4.7 - References.select (#2 (Ctree.get_obj Ctree.g_origin pt p')) (Ctree.get_obj Ctree.g_spec pt p')
4.8 + References.select_input (#2 (Ctree.get_obj Ctree.g_origin pt p')) (Ctree.get_obj Ctree.g_spec pt p')
4.9 end
4.10
4.11
5.1 --- a/src/Tools/isac/MathEngBasic/references.sml Tue Jul 26 22:29:35 2022 +0200
5.2 +++ b/src/Tools/isac/MathEngBasic/references.sml Wed Jul 27 13:11:43 2022 +0200
5.3 @@ -9,7 +9,7 @@
5.4 type T
5.5 val empty: T
5.6 val to_string: T -> string
5.7 - val select : T -> T -> T
5.8 + val select_input : T -> T -> T
5.9
5.10 val complete: Ctree.state -> Ctree.state
5.11 val are_complete: Ctree.state -> bool
5.12 @@ -24,7 +24,7 @@
5.13 type T = References_Def.T;
5.14 val empty = References_Def.empty;
5.15 val to_string = References_Def.to_string;
5.16 -val select = References_Def.select;
5.17 +val select_input = References_Def.select_input;
5.18
5.19 (* have (thy, pbl, met) _all_ been specified explicitly ? *)
5.20 fun are_complete (pt, pos as (p, _)) =
5.21 @@ -43,7 +43,7 @@
5.22 val (ospec, spec) = case Ctree.get_obj I pt p of
5.23 Ctree.PblObj {origin = (_, ospec, _), spec, ...} => (ospec, spec)
5.24 | _ => raise ERROR "References.complete: uncovered case get_obj"
5.25 - val pt = Ctree.update_spec pt p (select ospec spec)
5.26 + val pt = Ctree.update_spec pt p (select_input ospec spec)
5.27 in
5.28 (pt, pos)
5.29 end
6.1 --- a/src/Tools/isac/Specify/p-spec.sml Tue Jul 26 22:29:35 2022 +0200
6.2 +++ b/src/Tools/isac/Specify/p-spec.sml Wed Jul 27 13:11:43 2022 +0200
6.3 @@ -226,14 +226,14 @@
6.4 if dI <> sdI
6.5 then let val its = map (parsitm (ThyC.get_theory dI)) probl;
6.6 val (its, trms) = filter_sep is_Par its;
6.7 - val pbt = (#ppc o Problem.from_store) (#2 (References.select ospec sspec))
6.8 + val pbt = (#ppc o Problem.from_store) (#2 (References.select_input ospec sspec))
6.9 in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
6.10 else
6.11 if pI <> spI
6.12 then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
6.13 else
6.14 let val pbt = (#ppc o Problem.from_store) pI
6.15 - val dI' = #1 (References.select ospec spec)
6.16 + val dI' = #1 (References.select_input ospec spec)
6.17 val oris =
6.18 if pI = #2 ospec then oris
6.19 else O_Model.init (ThyC.get_theory "Isac_Knowledge") fmz_ pbt(* |> #1*);
6.20 @@ -245,17 +245,17 @@
6.21 in if foldl and_ (true, map #3 mits)
6.22 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
6.23 end
6.24 - else (Pos.Pbl, appl_adds (#1 (References.select ospec spec)) oris [(*!!!*)]
6.25 - ((#ppc o Problem.from_store) (#2 (References.select ospec spec)))
6.26 + else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)]
6.27 + ((#ppc o Problem.from_store) (#2 (References.select_input ospec spec)))
6.28 (imodel2fstr imodel), meth)
6.29 val pt = Ctree.update_spec pt p spec;
6.30 in if pos_ = Pos.Pbl
6.31 - then let val {prls,where_,...} = Problem.from_store (#2 (References.select ospec spec))
6.32 + then let val {prls,where_,...} = Problem.from_store (#2 (References.select_input ospec spec))
6.33 val (_, pre) = Pre_Conds.check prls where_ pits 0
6.34 in (Ctree.update_pbl pt p pits,
6.35 (SpecificationC.is_complete' pits pre spec, Pos.Pbl, hdf', pits, pre, spec): SpecificationC.T)
6.36 end
6.37 - else let val {prls,pre,...} = MethodC.from_store (#3 (References.select ospec spec))
6.38 + else let val {prls,pre,...} = MethodC.from_store (#3 (References.select_input ospec spec))
6.39 val (_, pre) = Pre_Conds.check prls pre mits 0
6.40 in (Ctree.update_met pt p mits,
6.41 (SpecificationC.is_complete' mits pre spec, Pos.Met, hdf', mits, pre, spec) : SpecificationC.T)
7.1 --- a/src/Tools/isac/Specify/specification.sml Tue Jul 26 22:29:35 2022 +0200
7.2 +++ b/src/Tools/isac/Specify/specification.sml Wed Jul 27 13:11:43 2022 +0200
7.3 @@ -116,7 +116,7 @@
7.4 val (ospec, hdf', spec, probl) = case Ctree.get_obj I pt p of
7.5 Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
7.6 | _ => raise ERROR "get Pbl: uncovered case get_obj"
7.7 - val {prls, where_, ...} = Problem.from_store (#2 (References.select ospec spec))
7.8 + val {prls, where_, ...} = Problem.from_store (#2 (References.select_input ospec spec))
7.9 val (_, pre) = Pre_Conds.check prls where_ probl 0
7.10 in
7.11 (is_complete' probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
7.12 @@ -126,7 +126,7 @@
7.13 val (ospec, hdf', spec, meth) = case Ctree.get_obj I pt p of
7.14 Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
7.15 | _ => raise ERROR "get Met: uncovered case get_obj"
7.16 - val {prls, pre, ...} = MethodC.from_store (#3 (References.select ospec spec))
7.17 + val {prls, pre, ...} = MethodC.from_store (#3 (References.select_input ospec spec))
7.18 val (_, pre) = Pre_Conds.check prls pre meth 0
7.19 in
7.20 (is_complete' meth pre spec, Pos.Met, hdf', meth, pre, spec)
8.1 --- a/src/Tools/isac/Specify/specify-step.sml Tue Jul 26 22:29:35 2022 +0200
8.2 +++ b/src/Tools/isac/Specify/specify-step.sml Wed Jul 27 13:11:43 2022 +0200
8.3 @@ -22,7 +22,7 @@
8.4 let
8.5 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
8.6 ...} = Calc.specify_data (ctree, pos);
8.7 - val (dI, _, _) = References.select o_refs refs;
8.8 + val (dI, _, _) = References.select_input o_refs refs;
8.9 val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID
8.10 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
8.11 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
9.1 --- a/src/Tools/isac/Specify/specify.sml Tue Jul 26 22:29:35 2022 +0200
9.2 +++ b/src/Tools/isac/Specify/specify.sml Wed Jul 27 13:11:43 2022 +0200
9.3 @@ -190,7 +190,7 @@
9.4 val (oris, ospec, probl, spec) = case Ctree.get_obj I pt p of
9.5 Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
9.6 | _ => raise ERROR "finish_phase: unvered case get_obj"
9.7 - val (_, pI, mI) = References.select ospec spec
9.8 + val (_, pI, mI) = References.select_input ospec spec
9.9 val mpc = (#ppc o MethodC.from_store) mI
9.10 val ppc = (#ppc o Problem.from_store) pI
9.11 val (pits, mits) = I_Model.complete_method (oris, mpc, ppc, probl)
9.12 @@ -199,7 +199,7 @@
9.13 in (pt, (p, Pos.Met)) end
9.14 fun finish_phasePIDE (o_model, o_refs) (problem_model, refs) =
9.15 let
9.16 - val (_, pI, mI) = References.select o_refs refs
9.17 + val (_, pI, mI) = References.select_input o_refs refs
9.18 val method_pattern = (#ppc o MethodC.from_store) mI
9.19 val problem_pattern = (#ppc o Problem.from_store) pI
9.20 val (problem_model, method_model) =
10.1 --- a/src/Tools/isac/Specify/step-specify.sml Tue Jul 26 22:29:35 2022 +0200
10.2 +++ b/src/Tools/isac/Specify/step-specify.sml Wed Jul 27 13:11:43 2022 +0200
10.3 @@ -29,7 +29,7 @@
10.4 val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
10.5 PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
10.6 | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
10.7 - val (_, pI, mI) = References.select ospec spec
10.8 + val (_, pI, mI) = References.select_input ospec spec
10.9 val mpc = (#ppc o MethodC.from_store) mI (* just for reuse I_Model.complete_method *)
10.10 val {cas, ppc, ...} = Problem.from_store pI
10.11 val pbl = I_Model.init ppc (* fill in descriptions *)
11.1 --- a/src/Tools/isac/TODO.thy Tue Jul 26 22:29:35 2022 +0200
11.2 +++ b/src/Tools/isac/TODO.thy Wed Jul 27 13:11:43 2022 +0200
11.3 @@ -43,7 +43,7 @@
11.4 remove defs from Test_Parse_Isac.thy
11.5 + and shift tests from Test_Parse_Isac -> test/../parseC.sml
11.6 \item xxx
11.7 - \item Specify.find_next_step: References.select
11.8 + \item Specify.find_next_step: References.select_input
11.9 cpI = ["vonBelastungZu", "Biegelinien"]: References_Def.id
11.10 ^^^^^ Problem.id
11.11 \item xxx
12.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Tue Jul 26 22:29:35 2022 +0200
12.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Wed Jul 27 13:11:43 2022 +0200
12.3 @@ -1250,8 +1250,8 @@
12.4 ...vvv
12.5 *)
12.6 (* val (dI, oris, ppc, pbt, (selct::ss))=
12.7 - (#1 (References.select ospec spec), oris, []:I_Model.T,
12.8 - ((#ppc o Problem.from_store) (#2 (References.select ospec spec))),(imodel2fstr imodel));
12.9 + (#1 (References.select_input ospec spec), oris, []:I_Model.T,
12.10 + ((#ppc o Problem.from_store) (#2 (References.select_input ospec spec))),(imodel2fstr imodel));
12.11 val iii = appl_adds dI oris ppc pbt (selct::ss);
12.12 tracing(I_Model.to_string thy iii);
12.13
13.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue Jul 26 22:29:35 2022 +0200
13.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Jul 27 13:11:43 2022 +0200
13.3 @@ -131,12 +131,12 @@
13.4 val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p;
13.5 "tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*)
13.6
13.7 -"~~~~~ fun References.select, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);
13.8 +"~~~~~ fun References.select_input, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);
13.9 dI = ThyC.id_empty; (*true*)
13.10 odI = "Build_Inverse_Z_Transform"; (*true*)
13.11 dI = ThyC.id_empty; (*true*)
13.12 -"~~~~~ after fun References.select:";
13.13 - val (dI, pI, mI) = References.select ospec spec;
13.14 +"~~~~~ after fun References.select_input:";
13.15 + val (dI, pI, mI) = References.select_input ospec spec;
13.16 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
13.17 val thy = ThyC.get_theory dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
13.18
14.1 --- a/test/Tools/isac/Specify/specify.sml Tue Jul 26 22:29:35 2022 +0200
14.2 +++ b/test/Tools/isac/Specify/specify.sml Wed Jul 27 13:11:43 2022 +0200
14.3 @@ -251,7 +251,7 @@
14.4 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (mID, (ctree, pos));
14.5 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
14.6 ...} = Calc.specify_data (ctree, pos);
14.7 - val (dI, _, _) = References.select o_refs refs;
14.8 + val (dI, _, _) = References.select_input o_refs refs;
14.9 val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID
14.10 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
14.11 val (o_model', ctxt') =
14.12 @@ -327,7 +327,7 @@
14.13 (tac', ptp);
14.14 (*NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
14.15 (*NEW*) ...} = Calc.specify_data (pt, pos);
14.16 -(*NEW*) val (dI, _, mID) = References.select o_refs refs;
14.17 +(*NEW*) val (dI, _, mID) = References.select_input o_refs refs;
14.18 (*NEW*) val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID
14.19 (*NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
14.20 (*NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
14.21 @@ -613,7 +613,7 @@
14.22 (tac', ptp);
14.23 (*.NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,
14.24 (*.NEW*) ...} =Calc.specify_data (pt, pos);
14.25 -(*.NEW*) val (dI, _, mID) = References.select o_refs refs;
14.26 +(*.NEW*) val (dI, _, mID) = References.select_input o_refs refs;
14.27 (*.NEW*) val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID
14.28 (*.NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
14.29 (*.NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt);