1.1 --- a/src/Tools/isac/Specify/step-specify.sml Mon Oct 31 16:53:59 2022 +0100
1.2 +++ b/src/Tools/isac/Specify/step-specify.sml Mon Oct 31 18:28:36 2022 +0100
1.3 @@ -29,13 +29,13 @@
1.4 | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
1.5 val (_, pI, mI) = References.select_input ospec spec
1.6 val mpc = (#ppc o MethodC.from_store ctxt) mI (* just for reuse I_Model.complete_method *)
1.7 - val {cas, ppc, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
1.8 - val pbl = I_Model.init ppc (* fill in descriptions *)
1.9 + val {cas, model, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
1.10 + val pbl = I_Model.init model (* fill in descriptions *)
1.11 (*----------------if you think, this should be done by the Dialog
1.12 in the java front-end, search there for WN060225-modelProblem----*)
1.13 val (pbl, met) = case cas of
1.14 NONE => (pbl, [])
1.15 - | _ => I_Model.complete_method (oris, mpc, ppc, probl)
1.16 + | _ => I_Model.complete_method (oris, mpc, model, probl)
1.17 (*----------------------------------------------------------------*)
1.18 val tac_ = Tactic.Model_Problem' (pI, pbl, met)
1.19 val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos)
1.20 @@ -57,9 +57,9 @@
1.21 case opt of
1.22 SOME pI' =>
1.23 let
1.24 - val {met, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
1.25 + val {solve_mets, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
1.26 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1.27 - val mI = if length met = 0 then MethodC.id_empty else hd met
1.28 + val mI = if length solve_mets = 0 then MethodC.id_empty else hd solve_mets
1.29 val (pos, c, _, pt) =
1.30 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos)
1.31 in
1.32 @@ -93,11 +93,11 @@
1.33 (oris, dI, dI', pI', probl, ctxt)
1.34 | _ => raise ERROR ""
1.35 val thy = ThyC.get_theory_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI');
1.36 - val {ppc,where_,prls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
1.37 + val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
1.38 val pbl =
1.39 if pI' = Problem.id_empty andalso pI = Problem.id_empty
1.40 - then (false, (I_Model.init ppc, []))
1.41 - else M_Match.match_itms_oris thy probl (ppc,where_,prls) oris
1.42 + then (false, (I_Model.init model, []))
1.43 + else M_Match.match_itms_oris thy probl (model, where_, where_rls) oris
1.44 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1.45 val (c, pt) =
1.46 case Specify_Step.add (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of
1.47 @@ -148,8 +148,10 @@
1.48 (* called only if no_met is specified *)
1.49 | by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) =
1.50 let
1.51 - val {met, thy,...} = Problem.from_store (Ctree.get_ctxt pt pos) pIre
1.52 - val (domID, metID) = (Context.theory_name thy, if length met = 0 then MethodC.id_empty else hd met)
1.53 + val {solve_mets, thy,...} = Problem.from_store (Ctree.get_ctxt pt pos) pIre
1.54 + val (domID, metID) = (Context.theory_name thy,
1.55 + if length solve_mets = 0 then MethodC.id_empty
1.56 + else hd solve_mets)
1.57 val ((p,_), _, _, pt) =
1.58 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
1.59 (Istate_Def.Uistate, ContextC.empty) (pt, pos)
1.60 @@ -218,25 +220,25 @@
1.61 if mI = ["no_met"]
1.62 then
1.63 let
1.64 - val pors = Problem.from_store ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
1.65 + val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
1.66 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
1.67 val pI' = Refine.refine_ori' pctxt pors pI;
1.68 in (pI', (pors (*refinement over models with diff.precond only*), pctxt),
1.69 - (hd o #met o Problem.from_store ctxt) pI')
1.70 + (hd o #solve_mets o Problem.from_store ctxt) pI')
1.71 end
1.72 else
1.73 let
1.74 - val pors = Problem.from_store ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
1.75 + val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
1.76 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
1.77 in (pI, (pors, pctxt), mI) end;
1.78 - val {cas, ppc, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*)
1.79 + val {cas, model, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*)
1.80 val dI = Context.theory_name (ThyC.sub_common (thy, thy'))
1.81 val hdl = case cas of
1.82 NONE => Auto_Prog.pblterm dI pI
1.83 - | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t
1.84 + | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t
1.85 val hdlPIDE = case cas of
1.86 NONE => Auto_Prog.pblterm dI pI
1.87 - | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t
1.88 + | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t
1.89 in
1.90 (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)
1.91 end;
1.92 @@ -245,14 +247,14 @@
1.93 if pI <> []
1.94 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1.95 let
1.96 - val {cas, met, ppc, thy, ...} = Problem.from_store ctxt pI
1.97 + val {cas, solve_mets, model, thy, ...} = Problem.from_store ctxt pI
1.98 val dI = if dI = "" then Context.theory_name thy else dI
1.99 - val mI = if mI = [] then hd met else mI
1.100 + val mI = if mI = [] then hd solve_mets else mI
1.101 val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
1.102 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
1.103 ([], (dI,pI,mI), hdl, ContextC.empty)
1.104 val pt = update_spec pt [] (dI, pI, mI)
1.105 - val pits = I_Model.init ppc
1.106 + val pits = I_Model.init model
1.107 val pt = update_pbl pt [] pits
1.108 in ((pt, ([] , Pbl)), []) end
1.109 else