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 val by_Add_: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
10 (*from isac_test for Minisubpbl*)
11 val for_problem: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T ->
12 string * (Pos.pos_ * Tactic.input)
13 val for_method: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T ->
14 string * (Pos.pos_ * Tactic.input)
22 structure Specify(**): SPECIFY(**) =
27 select an item in oris, notyet input in itms
28 (precondition: in itms are only I_Model.Cor, I_Model.Sup, I_Model.Inc)
31 oris: from formalization 'type fmz', structured for efficient access
32 pbt : the problem-pattern to be matched with oris in order to get itms
33 itms: already input items
35 fun item_to_add thy [] pbt itms = (*root (only) ori...fmz=[]*)
37 fun test_d d (i, _, _, _, itm_) = (d = (I_Model.descriptor itm_)) andalso i <> 0
38 fun is_elem itms (_, (d, _)) =
39 case find_first (test_d d) itms of SOME _ => true | NONE => false
41 case filter_out (is_elem itms) pbt of
42 (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, []))
45 (* m_field is in ------vvvv *)
46 | item_to_add thy oris _ itms =
48 fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
49 fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
50 fun test_id ids r = member op= ids (#1 (r : O_Model.single))
51 fun test_subset itm (_, _, _, d, ts) =
52 (I_Model.descriptor (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.o_model_values (#5 itm), ts)
53 fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
54 | false_and_not_Sup (_, _, false, _, _) = true
55 | false_and_not_Sup _ = false
56 val v = if itms = [] then 1 else I_Model.max_variant itms
57 val vors = if v = 0 then oris else filter (testr_vt v) oris
60 then itms (* because of dsc without dat *)
61 else filter (testi_vt v) itms; (* itms..vat *)
62 val icl = filter false_and_not_Sup vits; (* incomplete *)
65 case filter_out (test_id (map #1 vits)) vors of
67 | miss => SOME (O_Model.get_field_term thy (hd miss))
69 case find_first (test_subset (hd icl)) vors of
70 NONE => raise ERROR "item_to_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
71 | SOME ori => SOME (I_Model.get_field_term thy ori (hd icl))
75 (** find a next step in the specify-phase **)
77 here should be mutual recursion between for_problem ctxt and for_method
79 fun for_problem ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =
81 val cpI = if pI = Problem.id_empty then pI' else pI;
82 val cmI = if mI = MethodC.id_empty then mI' else mI;
83 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
84 val {model = mpc, ...} = MethodC.from_store ctxt cmI
85 val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
87 if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then
88 ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
89 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then
90 ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
92 case find_first (I_Model.is_error o #5) pbl of
93 SOME (_, _, _, fd, itm_) =>
94 ("dummy", (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory
95 (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
97 (case item_to_add (ThyC.get_theory_PIDE ctxt
98 (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
99 SOME (fd, ct') => ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct'))
100 | NONE => (*pbl-items complete*)
101 if not preok then ("dummy", (Pos.Pbl, Tactic.Refine_Problem pI'))
102 else if dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
103 else if pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
104 else if mI = MethodC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Method mI'))
106 case find_first (I_Model.is_error o #5) met of
107 SOME (_, _, _, fd, itm_) =>
108 ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory dI) fd itm_))
110 (case item_to_add (ThyC.get_theory dI) oris mpc met of
112 ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*30.8.01: where_?!?*)
113 | NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI))))
116 fun for_method ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =
118 val cmI = if mI = MethodC.id_empty then mI' else mI;
119 val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;
120 val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
122 (case find_first (I_Model.is_error o #5) met of
123 SOME (_,_,_, fd, itm_) =>
124 ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory_PIDE ctxt
125 (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
127 case item_to_add (ThyC.get_theory_PIDE ctxt
128 (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
130 ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*->->*)
132 (if dI = ThyC.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Theory dI'))
133 else if pI = Problem.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Problem pI'))
134 else if not preok then ("dummy", (Pos.Met, Tactic.Specify_Method mI))
135 else ("dummy", (Pos.Met, Tactic.Apply_Method mI))))
139 on finding a next step switching from problem to method or vice versa is possible,
140 because the user is free to switch and edit the respective models independently.
141 TODO: this free switch is NOT yet implemented; e.g.
142 preok is relevant for problem + method, i.e. in for_problem ctxt + for_method
144 fun find_next_step (pt, pos as (_, p_)) =
146 val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
147 spec = refs, ...} = Calc.specify_data (pt, pos);
148 val ctxt = Ctree.get_ctxt pt pos
150 if Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin then
152 ["no_met"] => ("ok", (Pos.Pbl, Tactic.Refine_Tacitly pI'))
153 | _ => ("ok", (Pos.Pbl, Tactic.Model_Problem))
154 else if p_ = Pos.Pbl then
155 for_problem ctxt oris (o_refs, refs) (pbl, met)
157 for_method ctxt oris (o_refs, refs) (pbl, met)
163 fun by_Add_ m_field ct (pt, pos as (_, p_)) =
165 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
166 val (i_model, m_patt) =
169 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
172 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
174 case I_Model.check_single ctxt m_field oris i_model m_patt ct of
175 I_Model.Add i_single => (*..union old input *)
177 val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model
178 val tac' = I_Model.make_tactic m_field (ct, i_model')
179 val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
181 ("ok", ([(Tactic.input_from_T tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],
184 | I_Model.Err msg => (msg, ([], [], (pt, pos)))
187 (* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
188 + met from fmz; assumes pos on PblObj, meth = [] *)
189 fun finish_phase (pt, pos as (p, p_)) =
191 val _ = if p_ <> Pos.Pbl
192 then raise ERROR ("###finish_phase: only impl.for Pbl, called with " ^ Pos.pos'2str pos)
194 val (oris, ospec, probl, spec) = case Ctree.get_obj I pt p of
195 Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
196 | _ => raise ERROR "finish_phase: unvered case get_obj"
197 val (_, pI, mI) = References.select_input ospec spec
198 val ctxt = Ctree.get_ctxt pt pos
199 val mpc = (#model o MethodC.from_store ctxt) mI
200 val model = (#model o Problem.from_store ctxt) pI
201 val (pits, mits) = I_Model.complete_method (oris, mpc, model, probl)
202 val pt = Ctree.update_pblppc pt p pits
203 val pt = Ctree.update_metppc pt p mits
204 in (pt, (p, Pos.Met)) end
206 (* do all specification in one single step:
207 complete calc-head for autocalc (sub-)pbl from oris (+ met from fmz);
208 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem
210 fun do_all (pt, pos as (p, _)) =
212 val (pors, dI, pI, mI) = case Ctree.get_obj I pt p of
213 Ctree.PblObj {origin = (pors, (dI, pI, mI), _), ...}
214 => (pors, dI, pI, mI)
215 | _ => raise ERROR "do_all: uncovered case get_obj"
216 val ctxt = Ctree.get_ctxt pt pos
217 val {model, ...} = MethodC.from_store ctxt mI
218 val (_, vals) = O_Model.values' ctxt pors
219 val ctxt = ContextC.initialise ctxt vals
220 val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),
221 map (I_Model.complete' model) pors, map (I_Model.complete' model) pors, ctxt)