3 val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input)
4 val do_all: Calc.T -> Calc.T
5 val finish_phase: Calc.T -> Calc.T
7 val item_to_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T ->
8 (Model_Def.m_field * TermC.as_string) option
9 (*TODO: vvvvvvvvvvvvvv unify code*)
10 val by_tactic_input': string -> TermC.as_string -> Calc.T -> Calc.state_post
11 val by_Add_: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
12 (*TODO: ^^^^^^^^^^^^^^ unify code*)
13 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
15 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
17 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
21 structure Specify(**): SPECIFY(**) =
26 select an item in oris, notyet input in itms
27 (precondition: in itms are only I_Model.Cor, I_Model.Sup, I_Model.Inc)
30 oris: from formalization 'type fmz', structured for efficient access
31 pbt : the problem-pattern to be matched with oris in order to get itms
32 itms: already input items
34 fun item_to_add thy [] pbt itms = (*root (only) ori...fmz=[]*)
36 fun test_d d (i, _, _, _, itm_) = (d = (I_Model.d_in itm_)) andalso i <> 0
37 fun is_elem itms (_, (d, _)) =
38 case find_first (test_d d) itms of SOME _ => true | NONE => false
40 case filter_out (is_elem itms) pbt of
41 (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, []))
44 (* m_field is in ------vvvv *)
45 | item_to_add thy oris _ itms =
47 fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
48 fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
49 fun test_id ids r = member op= ids (#1 (r : O_Model.single))
50 fun test_subset itm (_, _, _, d, ts) =
51 (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)
52 fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
53 | false_and_not_Sup (_, _, false, _, _) = true
54 | false_and_not_Sup _ = false
55 val v = if itms = [] then 1 else I_Model.max_vt itms
56 val vors = if v = 0 then oris else filter (testr_vt v) oris
59 then itms (* because of dsc without dat *)
60 else filter (testi_vt v) itms; (* itms..vat *)
61 val icl = filter false_and_not_Sup vits; (* incomplete *)
64 case filter_out (test_id (map #1 vits)) vors of
66 | miss => SOME (O_Model.getr_ct thy (hd miss))
68 case find_first (test_subset (hd icl)) vors of
69 NONE => raise ERROR "item_to_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
70 | SOME ori => SOME (I_Model.geti_ct thy ori (hd icl))
74 fun find_next_step (pt, (p, p_)) =
76 val {meth = met, origin = origin as (oris, (dI', pI', mI'), _), probl = pbl,
77 spec = (dI, pI, mI), ...} = Calc.specify_data (pt, (p, p_));
79 if Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin then
81 ["no_met"] => ("ok", (Pos.Pbl, Tactic.Refine_Tacitly pI'))
82 | _ => ("ok", (Pos.Pbl, Tactic.Model_Problem))
85 (*NEW* ) References.select (dI', pI', mI') (dI, pI, mI) ( *NEW*)
86 val cpI = if pI = Problem.id_empty then pI' else pI;
87 val cmI = if mI = Method.id_empty then mI' else mI;
88 val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;
89 val pre = Pre_Conds.check' "thy 100820" prls where_ pbl;
90 val preok = foldl and_ (true, map fst pre);
91 (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
92 val mpc = (#ppc o Method.from_store) cmI
95 (*vvvvvvv---------------------------*)
97 (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
98 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
100 case find_first (I_Model.is_error o #5) pbl of
101 SOME (_, _, _, fd, itm_) =>
102 ("dummy", (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory
103 (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
105 (case item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
106 SOME (fd, ct') => ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct'))
107 | NONE => (*pbl-items complete*)
108 if not preok then ("dummy", (Pos.Pbl, Tactic.Refine_Problem pI'))
109 else if dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
110 else if pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
111 else if mI = Method.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Method mI'))
113 case find_first (I_Model.is_error o #5) met of
114 SOME (_, _, _, fd, itm_) => ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory dI) fd itm_))
116 (case item_to_add (ThyC.get_theory dI) oris mpc met of
117 SOME (fd, ct') => ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*30.8.01: pre?!?*)
118 | NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI)))))
119 (*vvvvvvv---------------------------*)
121 (case find_first (I_Model.is_error o #5) met of
122 SOME (_,_,_, fd, itm_) => ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
124 case item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
125 SOME (fd, ct') => ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*->->*)
127 (if dI = ThyC.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Theory dI'))
128 else if pI = Problem.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Problem pI'))
129 else if not preok then ("dummy", (Pos.Met, Tactic.Specify_Method mI))
130 else ("dummy", (Pos.Met, Tactic.Apply_Method mI))))
131 | p_ => raise ERROR ("Specify.find_next_step called with " ^ Pos.pos_2str p_)
135 fun by_Add_ m_field ct (pt, pos as (_, p_)) =
137 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = Specification.get_data (pt, pos)
138 val (i_model, m_patt) =
141 (if mI = Method.id_empty then mI' else mI) |> Method.from_store |> #ppc)
144 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store |> #ppc)
146 case I_Model.check_single ctxt m_field oris i_model m_patt ct of
147 I_Model.Add i_single => (*..union old input *)
149 val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model
150 val tac' = I_Model.get_tac m_field (ct, i_model')
151 val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
153 ("ok", ([], [], (pt', pos)))
155 | I_Model.Err msg => (msg, ([], [], (pt, pos)))
158 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
159 -- for input from scratch*)
160 fun by_tactic_input' sel ct (ptp as (pt, (p, Pos.Pbl))) =
162 val (oris, dI', pI', dI, pI, pbl, ctxt) = case Ctree.get_obj I pt p of
163 Ctree.PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
164 (oris, dI', pI', dI, pI, pbl, ctxt)
165 | _ => raise ERROR "specify (Specify_Theory': uncovered case get_obj"
166 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
167 val cpI = if pI = Problem.id_empty then pI' else pI;
169 case I_Model.check_single ctxt sel oris pbl ((#ppc o Problem.from_store) cpI) ct of
170 I_Model.Add itm (*..union old input *) =>
172 val pbl' = I_Model.add_single thy itm pbl
173 val (tac, tac_) = case sel of
174 "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, pbl'))
175 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, pbl'))
176 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, pbl'))
177 | sel => raise ERROR ("by_tactic_input': uncovered case of " ^ sel)
179 case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
180 ((p, Pos.Pbl), c, _, pt') => (p, c, pt')
181 | _ => raise ERROR "by_tactic_input': uncovered case generate1"
183 ([(tac, tac_, ((p, Pos.Pbl), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Pbl)))
185 | I_Model.Err msg => (*TODO.WN03 pass error-msgs to the frontend..
186 FIXME ..and dont abuse a tactic for that purpose*)
187 ([(Tactic.Tac msg, Tactic.Tac_ (ThyC.get_theory "Isac_Knowledge", msg,msg,msg),
188 (Pos.e_pos', (Istate_Def.empty, ContextC.empty)))], [], ptp)
190 | by_tactic_input' sel ct (ptp as (pt, (p, Pos.Met))) =
192 (*NEW* ) *.specify_data ( *NEW*)
193 val (oris, dI', mI', dI, mI, met, ctxt) = case Ctree.get_obj I pt p of
194 Ctree.PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
195 (oris, dI', mI', dI, mI, met, ctxt)
196 | _ => raise ERROR "by_tactic_input' Met: uncovered case get_obj"
197 (*NEW* ) References.select ( *NEW*)
198 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
199 val cmI = if mI = Method.id_empty then mI' else mI;
201 case I_Model.check_single ctxt sel oris met ((#ppc o Method.from_store) cmI) ct of
202 I_Model.Add itm (*..union old input *) =>
204 val met' = I_Model.add_single thy itm met;
205 val (tac, tac_) = case sel of
206 "#Given" => (Tactic.Add_Given ct, Tactic.Add_Given' (ct, met'))
207 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, met'))
208 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, met'))
209 | sel => raise ERROR ("by_tactic_input' Met: uncovered case of" ^ sel)
211 case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of
212 ((p, Pos.Met), c, _, pt') => (p, c, pt')
213 | _ => raise ERROR "by_tactic_input': uncovered case generate1 (WARNING WHY ?)"
215 ([(tac, tac_, ((p, Pos.Met), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Met)))
217 | I_Model.Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
219 | by_tactic_input' _ _ (_, p) = raise ERROR ("by_tactic_input' not impl. for" ^ Pos.pos'2str p)
221 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
222 + met from fmz; assumes pos on PblObj, meth = [] *)
223 fun finish_phase (pt, pos as (p, p_)) =
225 val _ = if p_ <> Pos.Pbl
226 then raise ERROR ("###finish_phase: only impl.for Pbl, called with " ^ Pos.pos'2str pos)
228 val (oris, ospec, probl, spec) = case Ctree.get_obj I pt p of
229 Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
230 | _ => raise ERROR "finish_phase: unvered case get_obj"
231 val (_, pI, mI) = References.select ospec spec
232 val mpc = (#ppc o Method.from_store) mI
233 val ppc = (#ppc o Problem.from_store) pI
234 val (pits, mits) = I_Model.complete_method (oris, mpc, ppc, probl)
235 val pt = Ctree.update_pblppc pt p pits
236 val pt = Ctree.update_metppc pt p mits
237 in (pt, (p, Pos.Met)) end
239 (* do all specification in one single step:
240 complete calc-head for autocalc (sub-)pbl from oris (+ met from fmz);
241 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem
243 fun do_all (pt, (p, _)) =
245 val (pors, dI, pI, mI) = case Ctree.get_obj I pt p of
246 Ctree.PblObj {origin = (pors, (dI, pI, mI), _), ...}
247 => (pors, dI, pI, mI)
248 | _ => raise ERROR "do_all: uncovered case get_obj"
249 val {ppc, ...} = Method.from_store mI
250 val (_, vals) = O_Model.values' pors
251 val ctxt = ContextC.initialise dI vals
252 val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),
253 map (I_Model.complete' ppc) pors, map (I_Model.complete' ppc) pors, ctxt)