3 val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input)
4 val find_next_step': Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T ->
5 Model_Pattern.T * Model_Pattern.T -> References.T -> Pos.pos_ * Tactic.input
6 val do_all: Calc.T -> Calc.T
7 val finish_phase: Calc.T -> Calc.T
9 val item_to_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T ->
10 (Model_Def.m_field * TermC.as_string) option
11 val item_to_add': theory -> O_Model.T -> Model_Pattern.T -> I_Model.T ->
12 (Model_Def.m_field * TermC.as_string) option
13 (*TODO: vvvvvvvvvvvvvv unify code*)
14 val by_tactic_input': string -> TermC.as_string -> Calc.T -> Calc.state_post
15 val by_tactic': string -> TermC.as_string -> Calc.T -> string * Calc.state_post
16 (*TODO: ^^^^^^^^^^^^^^ unify code*)
17 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
19 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
21 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
25 structure Specify(**): SPECIFY(**) =
30 select an item in oris, notyet input in itms
31 (precondition: in itms are only I_Model.Cor, I_Model.Sup, I_Model.Inc)
34 oris: from formalization 'type fmz', structured for efficient access
35 pbt : the problem-pattern to be matched with oris in order to get itms
36 itms: already input items
38 fun item_to_add' thy [] pbt itms = (*root (only) ori...fmz=[]*)
40 (*<>*)fun test_d d (i, _, _, _, itm_) = (d = (I_Model.d_in itm_)) andalso i <> 0
41 fun is_elem itms (_, (d, _)) =
42 case find_first (test_d d) itms of SOME _ => true | NONE => false
44 case filter_out (is_elem itms) pbt of
45 (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, []))
48 | item_to_add' thy oris _ itms =
50 fun testr_vt v ori = Library.member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
51 fun testi_vt v itm = Library.member op= (#2 (itm : I_Model.single)) v
52 fun test_id ids r = Library.member op= ids (#1 (r : O_Model.single))
53 fun test_subset itm (_, _, _, d, ts) =
54 (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)
55 fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
56 | false_and_not_Sup (_, _, false, _, _) = true
57 | false_and_not_Sup _ = false
58 val v = if itms = [] then 1 else I_Model.max_vt itms
59 val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
62 then itms (* because of dsc without dat *)
63 else filter (testi_vt v) itms; (* itms..vat *)
64 val icl = filter false_and_not_Sup vits; (* incomplete *)
67 case filter_out (test_id (map #1 vits)) vors of
69 | miss => SOME (O_Model.getr_ct thy (hd miss))
71 case find_first (test_subset (hd icl)) vors of
72 NONE => raise ERROR "item_to_add': types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
73 | SOME ori => SOME (I_Model.geti_ct thy ori (hd icl))
76 (* preliminary doubling of code, ONLY difference SHALL BE in fun testr_vt *)
77 (* m_field is in --vvv *)
78 fun item_to_add thy [] pbt itms = (*root (only) ori...fmz=[]*)
80 fun test_d d (i, _, _, _, itm_) = (d = (I_Model.d_in itm_)) andalso i <> 0
81 fun is_elem itms (_, (d, _)) =
82 case find_first (test_d d) itms of SOME _ => true | NONE => false
84 case filter_out (is_elem itms) pbt of
85 (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, []))
88 (* m_field is in ------vvvv *)
89 | item_to_add thy oris _ itms =
91 (*NEW*)fun testr_vt v ori = Library.member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
92 fun testi_vt v itm = Library.member op= (#2 (itm : I_Model.single)) v
93 fun test_id ids r = Library.member op= ids (#1 (r : O_Model.single))
94 fun test_subset itm (_, _, _, d, ts) =
95 (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)
96 fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
97 | false_and_not_Sup (_, _, false, _, _) = true
98 | false_and_not_Sup _ = false
99 val v = if itms = [] then 1 else I_Model.max_vt itms
100 val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
103 then itms (* because of dsc without dat *)
104 else filter (testi_vt v) itms; (* itms..vat *)
105 val icl = filter false_and_not_Sup vits; (* incomplete *)
108 case filter_out (test_id (map #1 vits)) vors of
110 | miss => SOME (O_Model.getr_ct thy (hd miss))
112 case find_first (test_subset (hd icl)) vors of
113 NONE => raise ERROR "item_to_add': types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
114 | SOME ori => SOME (I_Model.geti_ct thy ori (hd icl))
118 fun find_next_step (pt, (p, p_)) =
120 (*OLD* )val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) =
121 (*OLD*) case Ctree.get_obj I pt p of
122 (*OLD*) pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
123 (*OLD*) probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
124 (*OLD*) | Ctree.PrfObj _ => raise ERROR "nxt_specify_: not on PrfObj"
126 (*OLD*) if Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin then
128 (*NEW*)val pblobj as {meth = met, origin = origin as (oris, (dI', pI', mI'), _), probl = pbl,
129 (*NEW*) spec = (dI, pI, mI), ctxt, ...} = Calc.specify_data (pt, (p, p_));
131 (*NEW*) if Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin then
134 ["no_met"] => ("ok", (Pos.Pbl, Tactic.Refine_Tacitly pI'))
135 | _ => ("ok", (Pos.Pbl, Tactic.Model_Problem))
138 (*NEW* ) References.select (dI', pI', mI') (dI, pI, mI) ( *NEW*)
139 val cpI = if pI = Problem.id_empty then pI' else pI;
140 val cmI = if mI = Method.id_empty then mI' else mI;
141 val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;
142 val pre = Pre_Conds.check' "thy 100820" prls where_ pbl;
143 val preok = foldl and_ (true, map fst pre);
144 (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
145 val mpc = (#ppc o Method.from_store) cmI
148 (*vvvvvvv---------------------------*)
150 (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
151 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
153 case find_first (I_Model.is_error o #5) pbl of
154 SOME (_, _, _, fd, itm_) =>
155 ("dummy", (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory
156 (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
158 (case item_to_add' (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
159 SOME (fd, ct') => ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct'))
160 | NONE => (*pbl-items complete*)
161 if not preok then ("dummy", (Pos.Pbl, Tactic.Refine_Problem pI'))
162 else if dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
163 else if pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
164 else if mI = Method.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Method mI'))
166 case find_first (I_Model.is_error o #5) met of
167 SOME (_, _, _, fd, itm_) => ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory dI) fd itm_))
169 (case item_to_add (ThyC.get_theory dI) oris mpc met of
170 SOME (fd, ct') => ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*30.8.01: pre?!?*)
171 | NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI)))))
172 (*vvvvvvv---------------------------*)
174 (case find_first (I_Model.is_error o #5) met of
175 SOME (_,_,_, fd, itm_) => ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
177 case item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
178 SOME (fd, ct') => ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*->->*)
180 (if dI = ThyC.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Theory dI'))
181 else if pI = Problem.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Problem pI'))
182 else if not preok then ("dummy", (Pos.Met, Tactic.Specify_Method mI))
183 else ("dummy", (Pos.Met, Tactic.Apply_Method mI))))
184 | p_ => raise ERROR ("Specify.find_next_step called with " ^ Pos.pos_2str p_)
189 TODO: unify code with Specify.find_next_step ! ! ! USED ONLY to determine Pos.Pbl .. Pos.Met
191 determine the next step of specification;
192 not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))
193 eg. in rootpbl 'no_met':
195 preok predicates are _all_ ok (and problem matches completely)
196 oris immediately from formalization
197 (dI',pI',mI') specification coming from author/parent-problem
198 (pbl, item lists specified by user
199 met) -"-, tacitly completed by copy_probl
200 (dI,pI,mI) specification explicitly done by the user
201 (pbt, mpc) problem type, guard of method
203 (*--------------vvvvvvv *)
204 fun find_next_step' Pos.Pbl preok oris (dI', pI', mI') (pbl, met) (pbt, mpc) (dI, pI, mI) =
205 (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')
206 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')
208 case find_first (I_Model.is_error o #5) pbl of
209 SOME (_, _, _, fd, itm_) =>
210 (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
212 (case item_to_add' (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
213 SOME (fd, ct') => (Pos.Pbl, P_Model.mk_additem fd ct')
214 | NONE => (*pbl-items complete*)
215 if not preok then (Pos.Pbl, Tactic.Refine_Problem pI')
216 else if dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')
217 else if pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')
218 else if mI = Method.id_empty then (Pos.Pbl, Tactic.Specify_Method mI')
220 case find_first (I_Model.is_error o #5) met of
221 SOME (_, _, _, fd, itm_) => (Pos.Met, P_Model.mk_delete (ThyC.get_theory dI) fd itm_)
223 (case item_to_add (ThyC.get_theory dI) oris mpc met of
224 SOME (fd, ct') => (Pos.Met, P_Model.mk_additem fd ct') (*30.8.01: pre?!?*)
225 | NONE => (Pos.Met, Tactic.Apply_Method mI))))
226 (*--------------vvvvvvv *)
227 | find_next_step' Pos.Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
228 (case find_first (I_Model.is_error o #5) met of
229 SOME (_,_,_,fd,itm_) => (Pos.Met, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
231 case item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
232 SOME (fd,ct') => (Pos.Met, P_Model.mk_additem fd ct')
234 (if dI = ThyC.id_empty then (Pos.Met, Tactic.Specify_Theory dI')
235 else if pI = Problem.id_empty then (Pos.Met, Tactic.Specify_Problem pI')
236 else if not preok then (Pos.Met, Tactic.Specify_Method mI)
237 else (Pos.Met, Tactic.Apply_Method mI)))
238 | find_next_step' p _ _ _ _ _ _ = raise ERROR ("find_next_step': uncovered case with " ^ Pos.pos_2str p)
240 fun by_tactic' sel ct (pt, pos as (p, Pos.Met)) =
242 val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos)
243 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
244 val cpI = if pI = Problem.id_empty then pI' else pI
245 val cmI = if mI = Method.id_empty then mI' else mI
246 val {ppc, pre, prls, ...} = Method.from_store cmI
248 case I_Model.check_single ctxt sel oris met ppc ct of
249 I_Model.Add itm => (*..union old input *)
251 val met' = I_Model.add_single thy itm met
252 val tac' = I_Model.get_tac sel (ct, met')
254 case Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of
255 ((p, Pos.Met), _, _, pt') => (p, pt')
256 | _ => raise ERROR "by_tactic': uncovered case of generate1"
257 val pre' = Pre_Conds.check' thy prls pre met'
258 val pb = foldl and_ (true, map fst pre')
259 val (p_, _) = find_next_step' Pos.Met pb oris (dI',pI',mI') (pbl,met')
260 ((#ppc o Problem.from_store) cpI,ppc) (dI,pI,mI);
262 ("ok", ([], [], (pt', (p, p_))))
266 val pre' = Pre_Conds.check' thy prls pre met
267 val pb = foldl and_ (true, map fst pre')
268 val (p_, _) = find_next_step' Pos.Met pb oris (dI',pI',mI') (pbl,met)
269 ((#ppc o Problem.from_store) cpI,(#ppc o Method.from_store) cmI) (dI,pI,mI);
271 (msg, ([], [], (pt, (p, p_))))
274 | by_tactic' sel ct (pt, pos as (p, _(*Frm, Pbl*))) =
276 val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos)
277 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
278 val cpI = if pI = Problem.id_empty then pI' else pI
279 val cmI = if mI = Method.id_empty then mI' else mI
280 val {ppc, where_, prls, ...} = Problem.from_store cpI
282 case I_Model.check_single ctxt sel oris pbl ppc ct of
283 I_Model.Add itm => (*..union old input *)
285 val pbl' = I_Model.add_single thy itm pbl
286 val tac' = I_Model.get_tac sel (ct, pbl')
288 case Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
289 ((p, Pos.Pbl), _, _, pt') => (p, pt')
290 | _ => raise ERROR "by_tactic': uncovered case of Specify_Step.add"
291 (* only for getting final p_ ..*)
292 val pre = Pre_Conds.check' thy prls where_ pbl';
293 val pb = foldl and_ (true, map fst pre);
294 val (p_, _) = find_next_step' Pos.Pbl pb oris (dI',pI',mI')
295 (pbl',met) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI);
297 ("ok", ([], [], (pt', (p, p_))))
301 val pre = Pre_Conds.check' thy prls where_ pbl
302 val pb = foldl and_ (true, map fst pre)
303 val (p_, _(*Tactic.input*)) = find_next_step' Pos.Pbl pb oris (dI', pI', mI')
304 (pbl, met) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI)
306 (msg, ([], [], (pt, (p, p_))))
310 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
311 -- for input from scratch*)
312 fun by_tactic_input' sel ct (ptp as (pt, (p, Pos.Pbl))) =
314 val (oris, dI', pI', dI, pI, pbl, ctxt) = case Ctree.get_obj I pt p of
315 Ctree.PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
316 (oris, dI', pI', dI, pI, pbl, ctxt)
317 | _ => raise ERROR "specify (Specify_Theory': uncovered case get_obj"
318 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
319 val cpI = if pI = Problem.id_empty then pI' else pI;
321 case I_Model.check_single ctxt sel oris pbl ((#ppc o Problem.from_store) cpI) ct of
322 I_Model.Add itm (*..union old input *) =>
324 val pbl' = I_Model.add_single thy itm pbl
325 val (tac, tac_) = case sel of
326 "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, pbl'))
327 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, pbl'))
328 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, pbl'))
329 | sel => raise ERROR ("by_tactic_input': uncovered case of " ^ sel)
331 case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
332 ((p, Pos.Pbl), c, _, pt') => (p, c, pt')
333 | _ => raise ERROR "by_tactic_input': uncovered case generate1"
335 ([(tac, tac_, ((p, Pos.Pbl), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Pbl)))
337 | I_Model.Err msg => (*TODO.WN03 pass error-msgs to the frontend..
338 FIXME ..and dont abuse a tactic for that purpose*)
339 ([(Tactic.Tac msg, Tactic.Tac_ (ThyC.get_theory "Isac_Knowledge", msg,msg,msg),
340 (Pos.e_pos', (Istate_Def.empty, ContextC.empty)))], [], ptp)
342 | by_tactic_input' sel ct (ptp as (pt, (p, Pos.Met))) =
344 (*NEW* )val sel = "#undef"; (* m_field may change from root- to sub-Model_Pattern *)
346 (*NEW* ) *.specify_data ( *NEW*)
347 val (oris, dI', mI', dI, mI, met, ctxt) = case Ctree.get_obj I pt p of
348 Ctree.PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
349 (oris, dI', mI', dI, mI, met, ctxt)
350 | _ => raise ERROR "by_tactic_input' Met: uncovered case get_obj"
351 (*NEW* ) References.select ( *NEW*)
352 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
353 val cmI = if mI = Method.id_empty then mI' else mI;
355 case I_Model.check_single ctxt sel oris met ((#ppc o Method.from_store) cmI) ct of
356 I_Model.Add itm (*..union old input *) =>
358 val met' = I_Model.add_single thy itm met;
359 val (tac, tac_) = case sel of
360 "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, met'))
361 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, met'))
362 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, met'))
363 | sel => raise ERROR ("by_tactic_input' Met: uncovered case of" ^ sel)
365 case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of
366 ((p, Pos.Met), c, _, pt') => (p, c, pt')
367 | _ => raise ERROR "by_tactic_input': uncovered case generate1 (WARNING WHY ?)"
369 ([(tac, tac_, ((p, Pos.Met), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Met)))
371 | I_Model.Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
373 | by_tactic_input' _ _ (_, p) = raise ERROR ("by_tactic_input' not impl. for" ^ Pos.pos'2str p)
375 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
376 + met from fmz; assumes pos on PblObj, meth = [] *)
377 fun finish_phase (pt, pos as (p, p_)) =
379 val _ = if p_ <> Pos.Pbl
380 then raise ERROR ("###finish_phase: only impl.for Pbl, called with " ^ Pos.pos'2str pos)
382 val (oris, ospec, probl, spec) = case Ctree.get_obj I pt p of
383 Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
384 | _ => raise ERROR "finish_phase: unvered case get_obj"
385 val (_, pI, mI) = References.select ospec spec
386 val mpc = (#ppc o Method.from_store) mI
387 val ppc = (#ppc o Problem.from_store) pI
388 val (pits, mits) = I_Model.complete_method (oris, mpc, ppc, probl)
389 val pt = Ctree.update_pblppc pt p pits
390 val pt = Ctree.update_metppc pt p mits
391 in (pt, (p, Pos.Met)) end
393 (* do all specification in one single step:
394 complete calc-head for autocalc (sub-)pbl from oris (+ met from fmz);
395 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem
397 fun do_all (pt, (p, _)) =
399 val (pors, dI, pI, mI) = case Ctree.get_obj I pt p of
400 Ctree.PblObj {origin = (pors, (dI, pI, mI), _), ...}
401 => (pors, dI, pI, mI)
402 | _ => raise ERROR "do_all: uncovered case get_obj"
403 val {ppc, ...} = Method.from_store mI
404 val (_, vals) = O_Model.values' pors
405 val ctxt = ContextC.initialise dI vals
406 val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),
407 map (I_Model.complete' ppc) pors, map (I_Model.complete' ppc) pors, ctxt)