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
11 val item_to_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T ->
12 (Model_Def.m_field * TermC.as_string) option
14 val item_to_add: Proof.context -> O_Model.T -> I_Model.T_TEST ->
15 (Model_Def.m_field * TermC.as_string) option
17 val by_Add_: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
18 (*from isac_test for Minisubpbl*)
20 val for_problem: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T ->
21 string * (Pos.pos_ * Tactic.input)
23 val for_problem: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T_TEST ->
24 string * (Pos.pos_ * Tactic.input)
26 val for_method: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T ->
27 string * (Pos.pos_ * Tactic.input)
28 val select_inc_lists: I_Model.T_TEST -> I_Model.T_TEST
36 structure Specify(**): SPECIFY(**) =
40 fun select_inc_lists i_model =
42 (* filter problem with Const ("Input_Descript.solutions", _) *)
43 val filt = (fn (_, _, _, _, (I_Model.Inc_TEST (descr, _::_) , _)) => Pre_Conds.is_list_descr descr
46 (filter filt i_model) @ (filter_out filt i_model)
50 select an item in oris, notyet input in itms
51 (precondition: in itms are only I_Model.Cor, I_Model.Sup, I_Model.Inc)
54 oris: from formalization 'type fmz', structured for efficient access
55 pbt : the problem-pattern to be matched with oris in order to get itms
56 itms: already input items
58 fun item_to_add thy [] pbt itms = (*root (only) ori...fmz=[]*)
60 fun test_d d (i, _, _, _, itm_) = (d = (I_Model.descriptor itm_)) andalso i <> 0
61 fun is_elem itms (_, (d, _)) =
62 case find_first (test_d d) itms of SOME _ => true | NONE => false
64 case filter_out (is_elem itms) pbt of
65 (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, []))
68 (* m_field is in ------vvvv *)
69 | item_to_add thy oris _ itms =
71 fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
72 fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
73 fun test_id ids r = member op= ids (#1 (r : O_Model.single))
74 fun test_subset itm (_, _, _, d, ts) =
75 (I_Model.descriptor (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.o_model_values (#5 itm), ts)
76 fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
77 | false_and_not_Sup (_, _, false, _, _) = true
78 | false_and_not_Sup _ = false
79 val v = if itms = [] then 1 else Pre_Conds.max_variant itms
80 val vors = if v = 0 then oris else filter (testr_vt v) oris
83 then itms (* because of dsc without dat *)
84 else filter (testi_vt v) itms; (* itms..vat *)
85 val icl = filter false_and_not_Sup vits; (* incomplete *)
88 case filter_out (test_id (map #1 vits)) vors of
90 | miss => SOME (O_Model.get_field_term thy (hd miss))
92 case find_first (test_subset (hd icl)) vors of
93 NONE => raise ERROR "item_to_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
94 | SOME ori => SOME (I_Model.get_field_term thy ori (hd icl))
97 fun item_to_add ctxt o_model i_model =
99 val max_vnt = last_elem (*this decides, for which variant initially help is given*)
100 (Model_Def.max_variants o_model i_model)
101 val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
102 val i_to_select = i_model
103 |> filter_out (fn (_, vnts, _, _, (I_Model.Cor_TEST _, _)) => member op= vnts max_vnt | _ => false)
108 case I_Model.fill_from_o o_vnts i_to_select of
109 SOME (_, _, _, m_field, (feedb, _)) =>
110 SOME (m_field, feedb |> I_Model.feedb_args_to_string ctxt)
111 | NONE => raise ERROR "item_to_add: NONE not.impl."
116 if i_to_select = [] then NONE
118 case I_Model.fill_from_o o_vnts (hd i_to_select) of
119 SOME (_, _, _, m_field, (feedb, _)) =>
120 SOME (m_field, feedb |> I_Model.feedb_args_to_string ctxt)
121 | NONE => raise ERROR "item_to_add: NONE not.impl."
127 (** find a next step in the specify-phase **)
129 here should be mutual recursion between for_problem ctxt and for_method
131 fun for_problem ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =
133 val cpI = if pI = Problem.id_empty then pI' else pI;
134 val cmI = if mI = MethodC.id_empty then mI' else mI;
135 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
136 val {model = mpc, ...} = MethodC.from_store ctxt cmI
137 val (preok, _) = Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
139 if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then
140 ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
141 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then
142 ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
144 case find_first (fn (_, _, _, _, feedb) => I_Model.is_error feedb) pbl of
145 SOME (_, _, _, fd, itm_) =>
146 ("dummy", (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory ctxt
147 (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
150 (case item_to_add (ThyC.get_theory ctxt
151 (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
153 (case item_to_add ctxt oris (I_Model.OLD_to_TEST pbl) of
155 SOME (fd, ct') => ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct'))
156 | NONE => (*pbl-items complete*)
157 if not preok then ("dummy", (Pos.Pbl, Tactic.Refine_Problem pI'))
158 (*this is an ERROR fall through ------^^^^^^^^^^^^^^^^^^^^^ for Pre_Conds, redesign ?*)
159 else if dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
160 else if pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
161 else if mI = MethodC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Method mI'))
163 case find_first (fn (_, _, _, _, feedb) => I_Model.is_error feedb) (I_Model.TEST_to_OLD met) of
164 SOME (_, _, _, fd, itm_) =>
165 ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory ctxt dI) fd itm_))
168 (case item_to_add (ThyC.get_theory ctxt dI) oris mpc met of
170 (case item_to_add ctxt oris met of
173 ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*30.8.01: where_?!?*)
174 | NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI))))
177 fun for_method ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (_, met) =
179 val cmI = if mI = MethodC.id_empty then mI' else mI;
180 val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;
181 val (preok, _) = Pre_Conds.check ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);
183 (case find_first (fn (_, _, _, _, feedb) => I_Model.is_error feedb) met of
184 SOME (_,_,_, fd, itm_) =>
185 ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory ctxt
186 (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
189 case item_to_add (ThyC.get_theory ctxt
190 (if dI = ThyC.id_empty then dI' else dI)) oris mpc (met) of
192 case item_to_add ctxt oris (I_Model.OLD_to_TEST met) of
195 ("dummy", (Pos.Met, P_Model.mk_additem fd ct'))
197 (if dI = ThyC.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Theory dI'))
198 else if pI = Problem.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Problem pI'))
199 else if not preok then ("dummy", (Pos.Met, Tactic.Specify_Method mI))
200 else ("dummy", (Pos.Met, Tactic.Apply_Method mI))))
204 on finding a next step switching from problem to method or vice versa is possible,
205 because the user is free to switch and edit the respective models independently.
206 TODO: this free switch is NOT yet implemented; e.g.
207 preok is relevant for problem + method, i.e. in for_problem ctxt + for_method
209 fun find_next_step (pt, pos as (_, p_)) =
211 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
212 spec = refs, ...} = Calc.specify_data (pt, pos);
213 val ctxt = Ctree.get_ctxt pt pos
215 if Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin then
217 ["no_met"] => ("ok", (Pos.Pbl, Tactic.Refine_Tacitly pI'))
218 | _ => ("ok", (Pos.Pbl, Tactic.Model_Problem))
219 else if p_ = Pos.Pbl then
220 for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to_TEST met)
222 for_method ctxt oris (o_refs, refs) (pbl, met)
228 fun by_Add_ m_field ct (pt, pos as (_, p_)) =
230 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
231 val (i_model, m_patt) =
234 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
237 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
239 case I_Model.check_single ctxt m_field oris i_model m_patt ct of
240 I_Model.Add i_single => (*..union old input *)
242 val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model
243 val tac' = I_Model.make_tactic m_field (ct, i_model')
244 val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
246 ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],
249 | I_Model.Err msg => (msg, ([], [], (pt, pos)))
252 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
253 + met from fmz; assumes pos on PblObj, meth = [] *)
254 fun finish_phase (pt, pos as (p, p_)) =
256 val _ = if p_ <> Pos.Pbl
257 then raise ERROR ("###finish_phase: only impl.for Pbl, called with " ^ Pos.pos'2str pos)
259 val (oris, ospec, probl, spec, meth) = case Ctree.get_obj I pt p of
260 Ctree.PblObj {origin = (oris, ospec, _), probl, spec, meth, ...} => (oris, ospec, probl, spec, meth)
261 | _ => raise ERROR "finish_phase: unvered case get_obj"
262 val (_, pI, mI) = References.select_input ospec spec
263 val ctxt = Ctree.get_ctxt pt pos
264 val (pits, mits) = I_Model.s_make_complete ctxt oris
265 (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (pI, mI)
266 val pt = Ctree.update_pblppc pt p (I_Model.TEST_to_OLD pits)
267 val pt = Ctree.update_metppc pt p (I_Model.TEST_to_OLD mits)
268 in (pt, (p, Pos.Met)) end
271 do all specification in one single step:
272 bypass input of Problem.model and go immediately for MethodC: I_Model.complete'
274 fun do_all (pt, (p, _)) =
276 val (itms, oris, probl, o_refs, spec, ctxt) = case Ctree.get_obj I pt p of
277 Ctree.PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}
278 => (itms, oris, probl, o_spec, spec, ctxt)
279 | _ => raise ERROR "Specify.do_all: no PblObj"
280 val (_, pbl_id', met_id') = References.select_input o_refs spec
281 val (pbl_imod, met_imod) = I_Model.s_make_complete ctxt oris
282 (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_id', met_id')
283 val (pt, _) = Ctree.cupdate_problem pt p
284 (o_refs, I_Model.TEST_to_OLD pbl_imod, I_Model.TEST_to_OLD met_imod, ctxt)