1 (* Title: Specify/specify.sml
6 val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input)
7 val do_all: Calc.T -> Calc.T
8 val finish_phase: Calc.T -> Calc.T
10 val item_to_add: Proof.context -> O_Model.T -> I_Model.T ->
11 (Model_Def.m_field * TermC.as_string) option
12 val by_Add_: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
14 (*from isac_test for Minisubpbl*)
15 val for_problem: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T ->
16 string * (Pos.pos_ * Tactic.input)
17 val for_method: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T ->
18 string * (Pos.pos_ * Tactic.input)
19 val select_inc_lists: I_Model.T -> I_Model.T
27 structure Specify(**): SPECIFY(**) =
31 fun select_inc_lists i_model =
33 (* filter problem like with Const ("Input_Descript.solutions", _) *)
34 val filt = (fn (_, _, _, _, (I_Model.Inc (descr, _::_) , _)) => Model_Def.is_list_descr descr
37 (filter filt i_model) @ (filter_out filt i_model)
40 fun item_to_add ctxt o_model i_model =
42 val max_vnt = last_elem (*this decides, for which variant initially help is given*)
43 (Model_Def.max_variants o_model i_model)
44 val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
45 val i_to_select = i_model
46 |> filter_out (fn (_, vnts, _, _, (I_Model.Cor _, _)) => member op= vnts max_vnt | _ => false)
49 if i_to_select = [] then NONE
51 case I_Model.fill_from_o o_vnts (hd i_to_select) of
52 SOME (_, _, _, m_field, (feedb, _)) =>
53 SOME (m_field, feedb |> I_Model.feedb_args_to_string ctxt)
54 | NONE => raise ERROR "item_to_add: NONE not.impl."
58 (** find a next step in the specify-phase **)
60 here should be mutual recursion between for_problem ctxt and for_method
62 fun for_problem ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =
64 val cpI = if pI = Problem.id_empty then pI' else pI;
65 val cmI = if mI = MethodC.id_empty then mI' else mI;
66 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
67 val {model = mpc, ...} = MethodC.from_store ctxt cmI
68 val (preok, _) = Pre_Conds.check ctxt where_rls where_ (pbt, pbl);
70 if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then
71 ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
72 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then
73 ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
75 case find_first (fn (_, _, _, _, (feedb, _)) => I_Model.is_error feedb) pbl of
76 SOME (_, _, _, fd, (itm_, _)) =>
77 ("dummy", (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory ctxt
78 (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
80 (case item_to_add ctxt oris pbl of
81 SOME (fd, ct') => ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct'))
82 | NONE => (*pbl-items complete*)
83 if not preok then ("dummy", (Pos.Pbl, Tactic.Refine_Problem pI'))
84 (*this is an ERROR fall through ------^^^^^^^^^^^^^^^^^^^^^ for Pre_Conds, redesign ?*)
85 else if dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
86 else if pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
87 else if mI = MethodC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Method mI'))
89 case find_first (fn (_, _, _, _, (feedb, _)) => I_Model.is_error feedb) met of
90 SOME (_, _, _, fd, (itm_, _)) =>
91 ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory ctxt dI) fd itm_))
93 (case item_to_add ctxt oris met of
95 ("dummy", (Pos.Met, P_Model.mk_additem fd ct'))
96 | NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI))))
99 fun for_method ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (_, met) =
101 val cmI = if mI = MethodC.id_empty then mI' else mI;
102 val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;
103 val (preok, _) = Pre_Conds.check ctxt where_rls where_ (mpc, met);
105 (case find_first (fn (_, _, _, _, (feedb, _)) => I_Model.is_error feedb) met of
106 SOME (_,_,_, fd, (itm_, _)) =>
107 ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory ctxt
108 (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
110 case item_to_add ctxt oris met of
112 ("dummy", (Pos.Met, P_Model.mk_additem fd ct'))
114 (if dI = ThyC.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Theory dI'))
115 else if pI = Problem.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Problem pI'))
116 else if not preok then ("dummy", (Pos.Met, Tactic.Specify_Method mI))
117 else ("dummy", (Pos.Met, Tactic.Apply_Method mI))))
121 on finding a next step switching from problem to method or vice versa is possible,
122 because the user is free to switch and edit the respective models independently.
123 TODO: this free switch is NOT yet implemented; e.g.
124 preok is relevant for problem + method, i.e. in for_problem ctxt + for_method
126 fun find_next_step (pt, pos as (_, p_)) =
128 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
129 spec = refs, ...} = Calc.specify_data (pt, pos);
130 val ctxt = Ctree.get_ctxt pt pos
132 if Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin then
134 ["no_met"] => ("ok", (Pos.Pbl, Tactic.Refine_Tacitly pI'))
135 | _ => ("ok", (Pos.Pbl, Tactic.Model_Problem))
136 else if p_ = Pos.Pbl then
137 for_problem ctxt oris (o_refs, refs) (pbl, met)
139 for_method ctxt oris (o_refs, refs) (pbl, met)
145 fun by_Add_ m_field ct (pt, pos as (_, p_)) =
147 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
148 val (i_model, m_patt) =
151 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
154 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
156 case I_Model.check_single ctxt m_field oris i_model m_patt ct of
157 I_Model.Add i_single => (*..union old input *)
159 val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model
160 val tac' = I_Model.make_tactic m_field (ct, i_model')
161 val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
163 ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],
166 | I_Model.Err msg => (msg, ([], [], (pt, pos)))
169 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
170 + met from fmz; assumes pos on PblObj, meth = [] *)
171 fun finish_phase (pt, pos as (p, p_)) =
173 val _ = if p_ <> Pos.Pbl
174 then raise ERROR ("###finish_phase: only impl.for Pbl, called with " ^ Pos.pos'2str pos)
176 val (oris, ospec, probl, spec, meth) = case Ctree.get_obj I pt p of
177 Ctree.PblObj {origin = (oris, ospec, _), probl, spec, meth, ...} => (oris, ospec, probl, spec, meth)
178 | _ => raise ERROR "finish_phase: unvered case get_obj"
179 val (_, pI, mI) = References.select_input ospec spec
180 val ctxt = Ctree.get_ctxt pt pos
181 val (pits, mits) = I_Model.s_make_complete ctxt oris (probl, meth) (pI, mI)
182 val pt = Ctree.update_pblppc pt p pits
183 val pt = Ctree.update_metppc pt p mits
184 in (pt, (p, Pos.Met)) end
187 do all specification in one single step:
188 bypass input of Problem.model and go immediately for MethodC: I_Model.complete'
190 fun do_all (pt, (p, _)) =
192 val (itms, oris, probl, o_refs, spec, ctxt) = case Ctree.get_obj I pt p of
193 Ctree.PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}
194 => (itms, oris, probl, o_spec, spec, ctxt)
195 | _ => raise ERROR "Specify.do_all: no PblObj"
196 val (_, pbl_id', met_id') = References.select_input o_refs spec
197 val (pbl_imod, met_imod) = I_Model.s_make_complete ctxt oris (probl, itms) (pbl_id', met_id')
198 val (pt, _) = Ctree.cupdate_problem pt p (o_refs, pbl_imod, met_imod, ctxt)