1.1 --- a/TODO.md Mon Oct 31 16:53:59 2022 +0100
1.2 +++ b/TODO.md Mon Oct 31 18:28:36 2022 +0100
1.3 @@ -51,7 +51,7 @@
1.4 ***** priority of WN items is top down, most urgent/simple on top
1.5
1.6 * WN?: improve Problem/MethodC..prep_input after meeting MW: parse twice?
1.7 -* WN: rename fields in Problem_def.T
1.8 +* WN: rename fields in Method_Def.T
1.9 * WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store›
1.10 * WN: KEStore_Elems.get_thes, add_thes still required for Error_Patterns, we want to eliminate thes:
1.11 (1) Error_Pattern.T are already stored by MethodC -- place them in respective thys
2.1 --- a/src/Tools/isac/BaseDefinitions/problem-def.sml Mon Oct 31 16:53:59 2022 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/problem-def.sml Mon Oct 31 18:28:36 2022 +0100
2.3 @@ -33,29 +33,25 @@
2.4 type T =
2.5 {guh : Check_Unique.id, (* unique within Isac_Knowledge, for html-presentation *)
2.6 mathauthors : string list, (* copyright *)
2.7 -(*start_refine: References_Def.id,*)
2.8 - init : References_Def.id, (* to start refinement with *)
2.9 + start_refine : References_Def.id, (* to start refinement with *)
2.10 thy : theory, (* which allows to compile that T *)
2.11 (*^^^ WN050912 NOT used during application of the problem,
2.12 because applied terms may be from 'subthy' as well as from super;
2.13 thus we take 'maxthy'; see match_ags ! *)
2.14 cas : term option, (* CAS_Cmd *)
2.15 -(*solve_mets: References_Def.id list,*)
2.16 - met : References_Def.id list, (* methods solving the T *)
2.17 -(*where_rls: Rule_Set.T,*)
2.18 - prls : Rule_Set.T, (* for evaluation of preconditions in "#Where" on "#Given" *)
2.19 + solve_mets : References_Def.id list, (* methods solving the T *)
2.20 + where_rls : Rule_Set.T, (* for evaluation of preconditions in "#Where" on "#Given" *)
2.21 where_ : term list, (* ? DEL, as soon as they are input interactively ? *)
2.22 -(*model: Model_Pattern.T*)
2.23 - ppc : Model_Pattern.T (* contains "#Given", "#Find", "#Relate"
2.24 + model : Model_Pattern.T (* contains "#Given", "#Find", "#Relate"
2.25 for constraints on identifiers see "O_Model.copy_name" *)
2.26 }
2.27 -val empty = {guh = "pbl_empty", mathauthors = [], init = id_empty, thy = @{theory "Pure"},
2.28 - cas = NONE, prls = Rule_Set.Empty, where_ = [], ppc = [], met = []} : T
2.29 -fun pbt2str ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
2.30 - prls = prls', thy = thy', where_ = w'} : T)
2.31 - = "{cas = " ^ (UnparseC.term_opt cas') ^ ", guh = \"" ^ guh' ^ "\", init = "
2.32 - ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = "
2.33 - ^ (strslist2strs met') ^ ", ppc = " ^ Model_Pattern.to_string ppc' ^ ", prls = "
2.34 +val empty = {guh = "pbl_empty", mathauthors = [], start_refine = id_empty, thy = @{theory "Pure"},
2.35 + cas = NONE, where_rls = Rule_Set.Empty, where_ = [], model = [], solve_mets = []} : T
2.36 +fun pbt2str ({cas = cas', guh = guh', start_refine = init', mathauthors = ma', solve_mets = met', model = ppc',
2.37 + where_rls = prls', thy = thy', where_ = w'} : T)
2.38 + = "{cas = " ^ (UnparseC.term_opt cas') ^ ", guh = \"" ^ guh' ^ "\", start_refine = "
2.39 + ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", solve_mets = "
2.40 + ^ (strslist2strs met') ^ ", model = " ^ Model_Pattern.to_string ppc' ^ ", where_rls = "
2.41 ^ (Rule_Set.id prls' |> quote) ^ ", thy = {" ^ Context.theory_name thy' ^ "}, where_ = "
2.42 ^ (UnparseC.terms w') ^ "}" |> linefeed;
2.43 fun s_to_string pbts = map pbt2str pbts |> list2str;
3.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Mon Oct 31 16:53:59 2022 +0100
3.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Mon Oct 31 18:28:36 2022 +0100
3.3 @@ -109,7 +109,6 @@
3.4 val atomwy: term -> unit
3.5 val atomty_thy: ThyC.id -> term -> unit
3.6 val free2var: term -> term
3.7 - val typ_a2real: term -> term
3.8 \<close>
3.9 val contains_one_of: thm * (string * typ) list -> bool
3.10 val contains_Const_typeless: term list -> term -> bool
4.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Mon Oct 31 16:53:59 2022 +0100
4.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Mon Oct 31 18:28:36 2022 +0100
4.3 @@ -102,7 +102,7 @@
4.4 Store.get (KEStore_Elems.get_expls @{theory}) example_id' example_id'
4.5 val ctxt = ContextC.initialise' thy model;
4.6
4.7 - val o_model = Problem.from_store ctxt probl_id |> #ppc |> O_Model.init thy model
4.8 + val o_model = Problem.from_store ctxt probl_id |> #model |> O_Model.init thy model
4.9 in
4.10 Ctree.Nd (Ctree.PblObj {
4.11 fmz = fmz, origin = (o_model, refs, TermC.empty (*TODO handle CAS_Cmd*)),
5.1 --- a/src/Tools/isac/Interpret/sub-problem.sml Mon Oct 31 16:53:59 2022 +0100
5.2 +++ b/src/Tools/isac/Interpret/sub-problem.sml Mon Oct 31 18:28:36 2022 +0100
5.3 @@ -18,24 +18,24 @@
5.4 if mI = ["no_met"]
5.5 then
5.6 let
5.7 - val pors = (M_Match.arguments thy ((#ppc o (Problem.from_store ctxt)) pI) ags): O_Model.T
5.8 + val pors = (M_Match.arguments thy ((#model o (Problem.from_store ctxt)) pI) ags): O_Model.T
5.9 handle ERROR "actual args do not match formal args"
5.10 => (M_Match.arguments_msg ctxt pI stac ags (*raise exn*);[]);
5.11 val pI' = Refine.refine_ori' ctxt pors pI;
5.12 in (pI', pors (* refinement over models with diff.prec only *),
5.13 - (hd o #met o Problem.from_store ctxt) pI') end
5.14 - else (pI, (M_Match.arguments thy ((#ppc o Problem.from_store ctxt) pI) ags)
5.15 + (hd o #solve_mets o Problem.from_store ctxt) pI') end
5.16 + else (pI, (M_Match.arguments thy ((#model o Problem.from_store ctxt) pI) ags)
5.17 handle ERROR "actual args do not match formal args"
5.18 => (M_Match.arguments_msg ctxt pI stac ags(*raise exn*); []), mI);
5.19 val (fmz_, vals) = O_Model.values' pors;
5.20 - val {cas, ppc, thy, ...} = Problem.from_store ctxt pI
5.21 + val {cas, model, thy, ...} = Problem.from_store ctxt pI
5.22 val dI = Context.theory_name thy (*take dI from _refined_ pbl*)
5.23 val dI = Context.theory_name (ThyC.sub_common (ThyC.get_theory dI, Ctree.rootthy pt))
5.24 val ctxt = ContextC.initialise dI vals
5.25 val hdl =
5.26 case cas of
5.27 NONE => Auto_Prog.pblterm dI pI
5.28 - | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ vals) t
5.29 + | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ vals) t
5.30 val f = Auto_Prog.subpbl (strip_thy dI) pI
5.31 in
5.32 (Tactic.Subproblem (dI, pI), Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
6.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Mon Oct 31 16:53:59 2022 +0100
6.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Mon Oct 31 18:28:36 2022 +0100
6.3 @@ -82,9 +82,9 @@
6.4 val ctxt = Proof_Context.init_global thy
6.5 val (gi, fi, re, wh) = Model_Pattern.parse_items ctxt pbl_id model_input
6.6 in
6.7 - ({guh = name, mathauthors = maa, init = start_refine, thy = thy,
6.8 + ({guh = name, mathauthors = maa, start_refine = start_refine, thy = thy,
6.9 cas = Option.map (Syntax.read_term_global thy) cas,
6.10 - prls = where_rls, where_ = wh, ppc = gi @ fi @ re, met = met_ids}, pbl_id)
6.11 + where_rls = where_rls, where_ = wh, model = gi @ fi @ re, solve_mets = met_ids}, pbl_id)
6.12 end;
6.13
6.14
6.15 @@ -159,16 +159,16 @@
6.16
6.17 (** get Problem from Store **)
6.18
6.19 -fun adapt_to_type ctxt ({guh, mathauthors, init, thy, cas, met, prls, where_, ppc} : Probl_Def.T) =
6.20 +fun adapt_to_type ctxt ({guh, mathauthors, start_refine, thy, cas, solve_mets, where_rls, where_, model} : Probl_Def.T) =
6.21 let
6.22 val cas = case cas of
6.23 SOME t => SOME (Model_Pattern.adapt_term_to_type ctxt t)
6.24 | NONE => NONE
6.25 val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
6.26 - val model = map (Model_Pattern.adapt_to_type ctxt) ppc
6.27 + val model = map (Model_Pattern.adapt_to_type ctxt) model
6.28 in
6.29 - {guh = guh, mathauthors = mathauthors, init = init, thy = thy, cas = cas, met = met,
6.30 - prls = prls, where_ = where_, ppc = model}
6.31 + {guh = guh, mathauthors = mathauthors, start_refine = start_refine, thy = thy, cas = cas, solve_mets = solve_mets,
6.32 + where_rls = where_rls, where_ = where_, model = model}
6.33 end
6.34
6.35 fun from_store ctxt id =
7.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon Oct 31 16:53:59 2022 +0100
7.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon Oct 31 18:28:36 2022 +0100
7.3 @@ -140,8 +140,9 @@
7.4 if pI' = Problem.id_empty
7.5 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
7.6 else pI'
7.7 - val {ppc, where_, prls, ...} = Problem.from_store ctxt pblID
7.8 - val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc, where_, prls) os
7.9 + val {model, where_, where_rls, ...} = Problem.from_store ctxt pblID
7.10 + val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge")
7.11 + probl (model, where_, where_rls) os
7.12 in
7.13 (model_ok, pblID, hdl, pbl, pre)
7.14 end
7.15 @@ -170,8 +171,9 @@
7.16 Ctree.PblObj {probl, origin = (os, ospec, hdl), spec, ...} => (probl, os, ospec, hdl, spec)
7.17 | Ctree.PrfObj _ => raise ERROR "context_pbl: uncovered case"
7.18 val ctxt = spec |> References.select_input ospec |> #1 |> ThyC.get_theory |> Proof_Context.init_global
7.19 - val {ppc, where_, prls, ...} = Problem.from_store ctxt pI
7.20 - val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
7.21 + val {model, where_, where_rls, ...} = Problem.from_store ctxt pI
7.22 + val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl
7.23 + (model, where_, where_rls) os
7.24 in
7.25 (model_ok, pI, hdl, pbl, pre)
7.26 end
7.27 @@ -199,8 +201,9 @@
7.28 case Refine.problem (ThyC.get_theory "Isac_Knowledge") pI probl of
7.29 NONE => (*copy from context_pbl*)
7.30 let
7.31 - val {ppc, where_, prls, ...} = Problem.from_store ctxt pI
7.32 - val (_, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
7.33 + val {model, where_, where_rls, ...} = Problem.from_store ctxt pI
7.34 + val (_, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl
7.35 + (model, where_, where_rls) os
7.36 in
7.37 (false, pI, hdl, pbl, pre)
7.38 end
8.1 --- a/src/Tools/isac/MathEngine/me-misc.sml Mon Oct 31 16:53:59 2022 +0100
8.2 +++ b/src/Tools/isac/MathEngine/me-misc.sml Mon Oct 31 18:28:36 2022 +0100
8.3 @@ -40,8 +40,8 @@
8.4 val pre = if pI = Problem.id_empty then []
8.5 else
8.6 let
8.7 - val {prls, where_, ...} = Problem.from_store ctxt pI
8.8 - val (_, pre) = Pre_Conds.check prls where_ probl 0
8.9 + val {where_rls, where_, ...} = Problem.from_store ctxt pI
8.10 + val (_, pre) = Pre_Conds.check where_rls where_ probl 0
8.11 in pre end
8.12 val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 pre))
8.13 in
9.1 --- a/src/Tools/isac/Specify/cas-command.sml Mon Oct 31 16:53:59 2022 +0100
9.2 +++ b/src/Tools/isac/Specify/cas-command.sml Mon Oct 31 18:28:36 2022 +0100
9.3 @@ -43,8 +43,8 @@
9.4 let
9.5 val thy = ThyC.get_theory dI
9.6 val ctxt = Proof_Context.init_global thy
9.7 - val {ppc, ...} = Problem.from_store ctxt pI
9.8 - val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
9.9 + val {model, ...} = Problem.from_store ctxt pI
9.10 + val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*)
9.11 val its = O_Model.add_enumerate its_
9.12 val pits = map flattup2 its
9.13 val (pI, mI) =
9.14 @@ -52,8 +52,8 @@
9.15 then (pI, mI)
9.16 else
9.17 case Refine.problem thy pI pits of
9.18 - SOME (pI,_) => (pI, (hd o #met o Problem.from_store ctxt) pI)
9.19 - | NONE => (pI, (hd o #met o Problem.from_store ctxt) pI)
9.20 + SOME (pI, _) => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)
9.21 + | NONE => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)
9.22 val {ppc, pre, prls, ...} = MethodC.from_store ctxt mI
9.23 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
9.24 val its = O_Model.add_enumerate its_
10.1 --- a/src/Tools/isac/Specify/m-match.sml Mon Oct 31 16:53:59 2022 +0100
10.2 +++ b/src/Tools/isac/Specify/m-match.sml Mon Oct 31 18:28:36 2022 +0100
10.3 @@ -48,8 +48,8 @@
10.4 datatype T =
10.5 Matches of Problem.id * P_Model.T
10.6 | NoMatch of Problem.id * P_Model.T;
10.7 -fun match2str (Matches (pI, ppc)) = "Matches (" ^ strs2str pI ^ ", " ^ P_Model.to_string ppc ^ ")"
10.8 - | match2str (NoMatch (pI, ppc)) = "NoMatch (" ^ strs2str pI ^ ", " ^ P_Model.to_string ppc ^ ")";
10.9 +fun match2str (Matches (pI, model)) = "Matches (" ^ strs2str pI ^ ", " ^ P_Model.to_string model ^ ")"
10.10 + | match2str (NoMatch (pI, model)) = "NoMatch (" ^ strs2str pI ^ ", " ^ P_Model.to_string model ^ ")";
10.11 fun matchs2str ms = (strs2str o (map match2str)) ms;
10.12
10.13
10.14 @@ -76,28 +76,28 @@
10.15 | NONE => [(f, I_Model.Mis (d, t))];
10.16 fun pair0vatsfalse (f, itm_) = (0, [], false, f, itm_);
10.17
10.18 -fun chk1_mis _(*mvat*) itms ppc = foldl and_ (true, map (chk1_m itms) ppc);
10.19 -fun chk1_mis' oris ppc = map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);
10.20 +fun chk1_mis _(*mvat*) itms model = foldl and_ (true, map (chk1_m itms) model);
10.21 +fun chk1_mis' oris model = map pair0vatsfalse ((flat o (map (chk1_m' oris))) model);
10.22
10.23 (* check a problem (ie. ori list) for matching a problemtype,
10.24 takes the I_Model.variables for concluding completeness (FIXME could be another!) *)
10.25 -fun match_oris thy prls oris (pbt,pre) =
10.26 +fun match_oris thy where_rls oris (pbt,pre) =
10.27 let
10.28 val itms = (flat o (map (chk1_ thy pbt))) oris;
10.29 val mvat = I_Model.variables itms;
10.30 val complete = chk1_mis mvat itms pbt;
10.31 - val (pb, _(*pre'*)) = Pre_Conds.check prls pre itms mvat;
10.32 + val (pb, _(*pre'*)) = Pre_Conds.check where_rls pre itms mvat;
10.33 in if complete andalso pb then true else false end;
10.34
10.35 (* check a problem (ie. ori list) for matching a problemtype,
10.36 returns items for output to math-experts *)
10.37 -fun match_oris' thy oris (ppc, pre, prls) =
10.38 +fun match_oris' thy oris (model, pre, where_rls) =
10.39 let
10.40 - val itms = (flat o (map (chk1_ thy ppc))) oris;
10.41 + val itms = (flat o (map (chk1_ thy model))) oris;
10.42 val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris;
10.43 val mvat = I_Model.variables itms;
10.44 - val miss = chk1_mis' oris ppc;
10.45 - val (pb, pre') = Pre_Conds.check prls pre itms mvat;
10.46 + val miss = chk1_mis' oris model;
10.47 + val (pb, pre') = Pre_Conds.check where_rls pre itms mvat;
10.48 in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;
10.49
10.50
10.51 @@ -112,7 +112,7 @@
10.52 (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
10.53 (3) newitms = filter (mv mem vat(news)) news
10.54 (4) pbt @ newitms *)
10.55 -fun match_itms_oris (_: theory) pbl (pbt, pre, prls) oris =
10.56 +fun match_itms_oris (_: theory) pbl (pbt, pre, where_rls) oris =
10.57 let
10.58 (*0*)val mv = I_Model.max_variant pbl;
10.59
10.60 @@ -128,7 +128,7 @@
10.61 (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
10.62 val newitms = filter mem_vat news;
10.63 (*4*)val itms' = pbl @ newitms;
10.64 - val (pb, pre') = Pre_Conds.check prls pre itms' mv;
10.65 + val (pb, pre') = Pre_Conds.check where_rls pre itms' mv;
10.66 in (length mis = 0 andalso pb, (itms', pre')) end;
10.67
10.68
10.69 @@ -139,10 +139,10 @@
10.70 | NoMatch' of P_Model.T;
10.71
10.72 (* match a formalization with a problem type, for tests *)
10.73 -fun match_pbl fmz ({thy = thy, where_ = pre, ppc, prls = er, ...}: Problem.T) =
10.74 +fun match_pbl fmz ({thy = thy, where_ = pre, model, where_rls = er, ...}: Problem.T) =
10.75 let
10.76 - val oris = O_Model.init thy fmz ppc(* |> #1*);
10.77 - val (bool, (itms, pre')) = match_oris' thy oris (ppc, pre, er);
10.78 + val oris = O_Model.init thy fmz model(* |> #1*);
10.79 + val (bool, (itms, pre')) = match_oris' thy oris (model, pre, er);
10.80 in
10.81 if bool
10.82 then Matches' (P_Model.from thy itms pre')
10.83 @@ -205,7 +205,7 @@
10.84 (* report part of the error-msg which is not available in match_args *)
10.85 fun arguments_msg ctxt pI stac ags =
10.86 let
10.87 - val pats = (#ppc o Problem.from_store ctxt) pI
10.88 + val pats = (#model o Problem.from_store ctxt) pI
10.89 val msg = (dots 70 ^ "\n"
10.90 ^ "*** problem " ^ strs2str pI ^ " has the ...\n"
10.91 ^ "*** model-pattern " ^ Model_Pattern.to_string pats ^ "\n"
11.1 --- a/src/Tools/isac/Specify/p-spec.sml Mon Oct 31 16:53:59 2022 +0100
11.2 +++ b/src/Tools/isac/Specify/p-spec.sml Mon Oct 31 18:28:36 2022 +0100
11.3 @@ -228,13 +228,13 @@
11.4 then let val its = map (parsitm (ThyC.get_theory dI)) probl;
11.5 val (its, trms) = filter_sep is_Par its;
11.6 val pbt =
11.7 - (#ppc o Problem.from_store ctxt) (#2 (References.select_input ospec sspec))
11.8 + (#model o Problem.from_store ctxt) (#2 (References.select_input ospec sspec))
11.9 in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
11.10 else
11.11 if pI <> spI
11.12 then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
11.13 else
11.14 - let val pbt = (#ppc o Problem.from_store ctxt) pI
11.15 + let val pbt = (#model o Problem.from_store ctxt) pI
11.16 val dI' = #1 (References.select_input ospec spec)
11.17 val oris =
11.18 if pI = #2 ospec then oris
11.19 @@ -248,16 +248,16 @@
11.20 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
11.21 end
11.22 else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)]
11.23 - ((#ppc o Problem.from_store ctxt)
11.24 + ((#model o Problem.from_store ctxt)
11.25 (#2 (References.select_input ospec spec)))
11.26 (imodel2fstr imodel), meth)
11.27 val pt = Ctree.update_spec pt p spec;
11.28 in if pos_ = Pos.Pbl
11.29 then
11.30 let
11.31 - val {prls, where_,...} = Problem.from_store ctxt
11.32 + val {where_rls, where_,...} = Problem.from_store ctxt
11.33 (#2 (References.select_input ospec spec))
11.34 - val (_, pre) = Pre_Conds.check prls where_ pits 0
11.35 + val (_, pre) = Pre_Conds.check where_rls where_ pits 0
11.36 in (Ctree.update_pbl pt p pits,
11.37 (SpecificationC.is_complete' pits pre spec, Pos.Pbl, hdf', pits, pre, spec))
11.38 end
12.1 --- a/src/Tools/isac/Specify/refine.sml Mon Oct 31 16:53:59 2022 +0100
12.2 +++ b/src/Tools/isac/Specify/refine.sml Mon Oct 31 18:28:36 2022 +0100
12.3 @@ -118,7 +118,7 @@
12.4
12.5 (* check a problem (ie. itm list) for matching a problemtype,
12.6 takes the I_Model.max_variant for concluding completeness (could be another!) *)
12.7 -fun match_itms thy itms (pbt, pre, prls) =
12.8 +fun match_itms thy itms (pbt, pre, where_rls) =
12.9 let
12.10 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
12.11 val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *)
12.12 @@ -126,15 +126,15 @@
12.13 val itms'' = filter (okv mvat) itms';
12.14 val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
12.15 val mis = chk_mis mvat itms'' untouched pbt;
12.16 - val (pb, pre') = Pre_Conds.check prls pre itms'' mvat
12.17 + val (pb, pre') = Pre_Conds.check where_rls pre itms'' mvat
12.18 in (length mis = 0 andalso pb, (itms'@ mis, pre')) end;
12.19
12.20 (* refine a problem; version for tactic Refine_Problem *)
12.21 fun refin'' _ (pblRD: Problem.id) itms pbls (Store.Node (pI, [py], [])) =
12.22 let
12.23 - val {thy, ppc, where_, prls, ...} = py
12.24 + val {thy, model, where_, where_rls, ...} = py
12.25 (*TODO val where_ = map TermC.adapt_to_type where_ ... adapt to current ctxt*)
12.26 - val (b, (itms', pre')) = match_itms thy itms (ppc, where_, prls);
12.27 + val (b, (itms', pre')) = match_itms thy itms (model, where_, where_rls);
12.28 in
12.29 if b
12.30 then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', pre'))]
12.31 @@ -142,8 +142,8 @@
12.32 end
12.33 | refin'' _ pblRD itms pbls (Store.Node (pI, [py], pys)) =
12.34 let
12.35 - val {thy, ppc, where_, prls, ...} = py
12.36 - val (b, (itms', pre')) = match_itms thy itms (ppc, where_, prls);
12.37 + val {thy, model, where_, where_rls, ...} = py
12.38 + val (b, (itms', pre')) = match_itms thy itms (model, where_, where_rls);
12.39 in if b
12.40 then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', pre'))
12.41 in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
12.42 @@ -171,11 +171,11 @@
12.43 *)
12.44 (** )
12.45 fun refin pblRD ori (Store.Node (pI, [py], [])) =
12.46 - if M_Match.match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
12.47 + if M_Match.match_oris (#thy py) (#where_rls py) ori (#model py, #where_ py)
12.48 then SOME (pblRD @ [pI])
12.49 else NONE
12.50 | refin pblRD ori (Store.Node (pI, [py], pys)) =
12.51 - if M_Match.match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
12.52 + if M_Match.match_oris (#thy py) (#where_rls py) ori (#model py, #where_ py)
12.53 then (case refins (pblRD @ [pI]) ori pys of
12.54 SOME pblRD' => SOME pblRD'
12.55 | NONE => SOME (pblRD @ [pI]))
12.56 @@ -192,21 +192,21 @@
12.57 (*val refin: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)
12.58 fun refin ctxt pblRD ori (Store.Node (pI, [py], [])) =
12.59 let
12.60 - val {thy, prls, ppc, where_, ...} = py: Problem.T
12.61 - val ppc = map (Model_Pattern.adapt_to_type ctxt) ppc
12.62 + val {where_rls, model, where_, ...} = py: Problem.T
12.63 + val model = map (Model_Pattern.adapt_to_type ctxt) model
12.64 val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
12.65 in
12.66 - if M_Match.match_oris (Proof_Context.theory_of ctxt) prls ori (ppc, where_)
12.67 + if M_Match.match_oris (Proof_Context.theory_of ctxt) where_rls ori (model, where_)
12.68 then SOME (pblRD @ [pI])
12.69 else NONE
12.70 end
12.71 | refin ctxt pblRD ori (Store.Node (pI, [py], pys)) =
12.72 let
12.73 - val {prls, ppc, where_, ...} = py: Problem.T
12.74 - val ppc = map (Model_Pattern.adapt_to_type ctxt) ppc
12.75 + val {where_rls, model, where_, ...} = py: Problem.T
12.76 + val model = map (Model_Pattern.adapt_to_type ctxt) model
12.77 val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
12.78 in
12.79 - if M_Match.match_oris (Proof_Context.theory_of ctxt) prls ori (ppc, where_)
12.80 + if M_Match.match_oris (Proof_Context.theory_of ctxt) where_rls ori (model, where_)
12.81 then (case refins ctxt (pblRD @ [pI]) ori pys of
12.82 SOME pblRD' => SOME pblRD'
12.83 | NONE => SOME (pblRD @ [pI]))
12.84 @@ -225,10 +225,10 @@
12.85 fun refin' pblRD fmz pbls (Store.Node (pI, [py: Probl_Def.T], [])) =
12.86 let
12.87 val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])
12.88 - val {thy, ppc, where_, prls, ...} = py
12.89 - val oris = O_Model.init thy fmz ppc(* |> #1*);
12.90 + val {thy, model, where_, where_rls, ...} = py
12.91 + val oris = O_Model.init thy fmz model(* |> #1*);
12.92 (* WN020803: itms!: oris might _not_ be complete here *)
12.93 - val (b, (itms, pre')) = M_Match.match_oris' thy oris (ppc, where_, prls)
12.94 + val (b, (itms, pre')) = M_Match.match_oris' thy oris (model, where_, where_rls)
12.95 in
12.96 if b
12.97 then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')]
12.98 @@ -237,10 +237,10 @@
12.99 | refin' pblRD fmz pbls (Store.Node (pI, [py], pys)) =
12.100 let
12.101 val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
12.102 - val {thy, ppc, where_, prls, ...} = py
12.103 - val oris = O_Model.init thy fmz ppc(* |> #1*);
12.104 + val {thy, model, where_, where_rls, ...} = py
12.105 + val oris = O_Model.init thy fmz model(* |> #1*);
12.106 (* WN020803: itms!: oris might _not_ be complete here *)
12.107 - val(b, (itms, pre')) = M_Match.match_oris' thy oris (ppc,where_,prls);
12.108 + val(b, (itms, pre')) = M_Match.match_oris' thy oris (model,where_,where_rls);
12.109 in
12.110 if b
12.111 then
12.112 @@ -264,12 +264,12 @@
12.113 fun refin' ctxt pblRD fmz pbls (Store.Node (pI, [py: Probl_Def.T], [])) =
12.114 let
12.115 val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])
12.116 - val {thy, ppc, where_, prls, ...} = py
12.117 - val ppc = map (Model_Pattern.adapt_to_type ctxt) ppc
12.118 + val {thy, model, where_, where_rls, ...} = py
12.119 + val model = map (Model_Pattern.adapt_to_type ctxt) model
12.120 val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
12.121 - val oris = O_Model.init thy fmz ppc; (*WN020803: oris might NOT be complete here*)
12.122 + val oris = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)
12.123 val (b, (itms, pre')) =
12.124 - M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (ppc, where_, prls)
12.125 + M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls)
12.126 in
12.127 if b
12.128 then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')]
12.129 @@ -278,12 +278,12 @@
12.130 | refin' ctxt pblRD fmz pbls (Store.Node (pI, [py], pys)) =
12.131 let
12.132 val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
12.133 - val {thy, ppc, where_, prls, ...} = py
12.134 - val ppc = map (Model_Pattern.adapt_to_type ctxt) ppc
12.135 + val {thy, model, where_, where_rls, ...} = py
12.136 + val model = map (Model_Pattern.adapt_to_type ctxt) model
12.137 val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
12.138 - val oris = O_Model.init thy fmz ppc; (*WN020803: oris might NOT be complete here*)
12.139 + val oris = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)
12.140 val (b, (itms, pre')) =
12.141 - M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (ppc, where_, prls)
12.142 + M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls)
12.143 in
12.144 if b
12.145 then
13.1 --- a/src/Tools/isac/Specify/specification.sml Mon Oct 31 16:53:59 2022 +0100
13.2 +++ b/src/Tools/isac/Specify/specification.sml Mon Oct 31 18:28:36 2022 +0100
13.3 @@ -117,9 +117,9 @@
13.4 val (ospec, hdf', spec, probl, ctxt) = case Ctree.get_obj I pt p of
13.5 Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl, ctxt, ...} => (ospec, hdf', spec, probl, ctxt)
13.6 | _ => raise ERROR "get Pbl: uncovered case get_obj"
13.7 - val {prls, where_, ...} =
13.8 + val {where_rls, where_, ...} =
13.9 Problem.from_store (Ctree.get_ctxt pt pos) (#2 (References.select_input ospec spec))
13.10 - val (_, pre) = Pre_Conds.check prls where_ probl 0
13.11 + val (_, pre) = Pre_Conds.check where_rls where_ probl 0
13.12 in
13.13 (is_complete' probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
13.14 end
14.1 --- a/src/Tools/isac/Specify/specify-step.sml Mon Oct 31 16:53:59 2022 +0100
14.2 +++ b/src/Tools/isac/Specify/specify-step.sml Mon Oct 31 18:28:36 2022 +0100
14.3 @@ -50,8 +50,8 @@
14.4 val pI' = case Ctree.get_obj I pt p of
14.5 Ctree.PblObj {origin = (_, (_, pI', _),_), ...} => pI'
14.6 | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
14.7 - val {ppc, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
14.8 - val pbl = I_Model.init ppc
14.9 + val {model, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
14.10 + val pbl = I_Model.init model
14.11 in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
14.12 | check (Tactic.Refine_Problem pI) (pt, (p, _)) =
14.13 let
14.14 @@ -93,10 +93,10 @@
14.15 => (oris, dI, pI, dI', pI', itms, ctxt)
14.16 | _ => raise ERROR "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj"
14.17 val thy = ThyC.get_theory_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI');
14.18 - val {ppc, where_, prls, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pID;
14.19 + val {model, where_, where_rls, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pID;
14.20 val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty
14.21 - then (false, (I_Model.init ppc, []))
14.22 - else M_Match.match_itms_oris thy itms (ppc, where_, prls) oris;
14.23 + then (false, (I_Model.init model, []))
14.24 + else M_Match.match_itms_oris thy itms (model, where_, where_rls) oris;
14.25 in
14.26 Applicable.Yes (Tactic.Specify_Problem' (pID, pbl))
14.27 end
15.1 --- a/src/Tools/isac/Specify/specify.sml Mon Oct 31 16:53:59 2022 +0100
15.2 +++ b/src/Tools/isac/Specify/specify.sml Mon Oct 31 18:28:36 2022 +0100
15.3 @@ -80,9 +80,9 @@
15.4 let
15.5 val cpI = if pI = Problem.id_empty then pI' else pI;
15.6 val cmI = if mI = MethodC.id_empty then mI' else mI;
15.7 - val {ppc = pbt, prls, where_, ...} = Problem.from_store ctxt cpI;
15.8 + val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
15.9 val {ppc = mpc, ...} = MethodC.from_store ctxt cmI
15.10 - val (preok, _) = Pre_Conds.check prls where_ pbl 0;
15.11 + val (preok, _) = Pre_Conds.check where_rls where_ pbl 0;
15.12 in
15.13 if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then
15.14 ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
15.15 @@ -169,7 +169,7 @@
15.16 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #ppc)
15.17 else
15.18 (pbl,
15.19 - (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #ppc)
15.20 + (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
15.21 in
15.22 case I_Model.check_single ctxt m_field oris i_model m_patt ct of
15.23 I_Model.Add i_single => (*..union old input *)
15.24 @@ -197,7 +197,7 @@
15.25 val (_, pI, mI) = References.select_input ospec spec
15.26 val ctxt = Ctree.get_ctxt pt pos
15.27 val mpc = (#ppc o MethodC.from_store ctxt) mI
15.28 - val ppc = (#ppc o Problem.from_store ctxt) pI
15.29 + val ppc = (#model o Problem.from_store ctxt) pI
15.30 val (pits, mits) = I_Model.complete_method (oris, mpc, ppc, probl)
15.31 val pt = Ctree.update_pblppc pt p pits
15.32 val pt = Ctree.update_metppc pt p mits
16.1 --- a/src/Tools/isac/Specify/step-specify.sml Mon Oct 31 16:53:59 2022 +0100
16.2 +++ b/src/Tools/isac/Specify/step-specify.sml Mon Oct 31 18:28:36 2022 +0100
16.3 @@ -29,13 +29,13 @@
16.4 | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
16.5 val (_, pI, mI) = References.select_input ospec spec
16.6 val mpc = (#ppc o MethodC.from_store ctxt) mI (* just for reuse I_Model.complete_method *)
16.7 - val {cas, ppc, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
16.8 - val pbl = I_Model.init ppc (* fill in descriptions *)
16.9 + val {cas, model, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
16.10 + val pbl = I_Model.init model (* fill in descriptions *)
16.11 (*----------------if you think, this should be done by the Dialog
16.12 in the java front-end, search there for WN060225-modelProblem----*)
16.13 val (pbl, met) = case cas of
16.14 NONE => (pbl, [])
16.15 - | _ => I_Model.complete_method (oris, mpc, ppc, probl)
16.16 + | _ => I_Model.complete_method (oris, mpc, model, probl)
16.17 (*----------------------------------------------------------------*)
16.18 val tac_ = Tactic.Model_Problem' (pI, pbl, met)
16.19 val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos)
16.20 @@ -57,9 +57,9 @@
16.21 case opt of
16.22 SOME pI' =>
16.23 let
16.24 - val {met, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
16.25 + val {solve_mets, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
16.26 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
16.27 - val mI = if length met = 0 then MethodC.id_empty else hd met
16.28 + val mI = if length solve_mets = 0 then MethodC.id_empty else hd solve_mets
16.29 val (pos, c, _, pt) =
16.30 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos)
16.31 in
16.32 @@ -93,11 +93,11 @@
16.33 (oris, dI, dI', pI', probl, ctxt)
16.34 | _ => raise ERROR ""
16.35 val thy = ThyC.get_theory_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI');
16.36 - val {ppc,where_,prls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
16.37 + val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
16.38 val pbl =
16.39 if pI' = Problem.id_empty andalso pI = Problem.id_empty
16.40 - then (false, (I_Model.init ppc, []))
16.41 - else M_Match.match_itms_oris thy probl (ppc,where_,prls) oris
16.42 + then (false, (I_Model.init model, []))
16.43 + else M_Match.match_itms_oris thy probl (model, where_, where_rls) oris
16.44 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
16.45 val (c, pt) =
16.46 case Specify_Step.add (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of
16.47 @@ -148,8 +148,10 @@
16.48 (* called only if no_met is specified *)
16.49 | by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) =
16.50 let
16.51 - val {met, thy,...} = Problem.from_store (Ctree.get_ctxt pt pos) pIre
16.52 - val (domID, metID) = (Context.theory_name thy, if length met = 0 then MethodC.id_empty else hd met)
16.53 + val {solve_mets, thy,...} = Problem.from_store (Ctree.get_ctxt pt pos) pIre
16.54 + val (domID, metID) = (Context.theory_name thy,
16.55 + if length solve_mets = 0 then MethodC.id_empty
16.56 + else hd solve_mets)
16.57 val ((p,_), _, _, pt) =
16.58 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
16.59 (Istate_Def.Uistate, ContextC.empty) (pt, pos)
16.60 @@ -218,25 +220,25 @@
16.61 if mI = ["no_met"]
16.62 then
16.63 let
16.64 - val pors = Problem.from_store ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
16.65 + val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
16.66 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
16.67 val pI' = Refine.refine_ori' pctxt pors pI;
16.68 in (pI', (pors (*refinement over models with diff.precond only*), pctxt),
16.69 - (hd o #met o Problem.from_store ctxt) pI')
16.70 + (hd o #solve_mets o Problem.from_store ctxt) pI')
16.71 end
16.72 else
16.73 let
16.74 - val pors = Problem.from_store ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
16.75 + val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
16.76 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
16.77 in (pI, (pors, pctxt), mI) end;
16.78 - val {cas, ppc, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*)
16.79 + val {cas, model, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*)
16.80 val dI = Context.theory_name (ThyC.sub_common (thy, thy'))
16.81 val hdl = case cas of
16.82 NONE => Auto_Prog.pblterm dI pI
16.83 - | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t
16.84 + | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t
16.85 val hdlPIDE = case cas of
16.86 NONE => Auto_Prog.pblterm dI pI
16.87 - | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t
16.88 + | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t
16.89 in
16.90 (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)
16.91 end;
16.92 @@ -245,14 +247,14 @@
16.93 if pI <> []
16.94 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
16.95 let
16.96 - val {cas, met, ppc, thy, ...} = Problem.from_store ctxt pI
16.97 + val {cas, solve_mets, model, thy, ...} = Problem.from_store ctxt pI
16.98 val dI = if dI = "" then Context.theory_name thy else dI
16.99 - val mI = if mI = [] then hd met else mI
16.100 + val mI = if mI = [] then hd solve_mets else mI
16.101 val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
16.102 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
16.103 ([], (dI,pI,mI), hdl, ContextC.empty)
16.104 val pt = update_spec pt [] (dI, pI, mI)
16.105 - val pits = I_Model.init ppc
16.106 + val pits = I_Model.init model
16.107 val pt = update_pbl pt [] pits
16.108 in ((pt, ([] , Pbl)), []) end
16.109 else
17.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Mon Oct 31 16:53:59 2022 +0100
17.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Mon Oct 31 18:28:36 2022 +0100
17.3 @@ -38,7 +38,7 @@
17.4 then raise error "else not covered by test"
17.5 else
17.6 let
17.7 - val pors = Problem.from_store ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
17.8 + val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
17.9 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
17.10 in (pI, (pors, pctxt), mI) end;
17.11
18.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Mon Oct 31 16:53:59 2022 +0100
18.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Mon Oct 31 18:28:36 2022 +0100
18.3 @@ -76,9 +76,9 @@
18.4 val cdI = if dI = ThyC.id_empty then dI' else dI;
18.5 val cpI = if pI = Problem.id_empty then pI' else pI;
18.6 val cmI = if mI = MethodC.id_empty then mI' else mI;
18.7 - val {ppc = pbt, prls, where_, ...} = Problem.from_store ctxt cpI;
18.8 + val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
18.9 val {ppc = mpc, ...} = MethodC.from_store ctxt cmI
18.10 - val (preok, _) = Pre_Conds.check prls where_ pbl 0;
18.11 + val (preok, _) = Pre_Conds.check where_rls where_ pbl 0;
18.12 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
18.13 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
18.14 (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
18.15 @@ -198,7 +198,7 @@
18.16 PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
18.17 (oris, dI, dI', pI', probl, ctxt)
18.18 val thy = ThyC.get_theory_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI');
18.19 - val {ppc,where_,prls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
18.20 + val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
18.21 (*-------------------- stop step into me Specify_Theory --------------------------------------*)
18.22 (*\\------------------ step into me Specify_Theory -----------------------------------------//*)
18.23