1 signature SPECIFY = |
1 signature SPECIFY = |
2 sig |
2 sig |
3 val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input) |
3 val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input) |
4 val do_all: Calc.T -> Calc.T |
4 val do_all: Calc.T -> Calc.T |
5 val finish_phase: Calc.T -> Calc.T |
5 val finish_phase: Calc.T -> Calc.T |
6 val finish_phase_PIDEnote: Proof.context -> O_Model.T * References.T -> I_Model.T * References.T -> |
|
7 I_Model.T * I_Model.T |
|
8 |
6 |
9 val item_to_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> |
7 val item_to_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> |
10 (Model_Def.m_field * TermC.as_string) option |
8 (Model_Def.m_field * TermC.as_string) option |
11 val by_Add_: string -> TermC.as_string -> Calc.T -> string * Calc.state_post |
9 val by_Add_: string -> TermC.as_string -> Calc.T -> string * Calc.state_post |
12 \<^isac_test>\<open> |
10 \<^isac_test>\<open> |
78 fun for_problem_PIDE ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) = |
76 fun for_problem_PIDE ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) = |
79 let |
77 let |
80 val cdI = if dI = ThyC.id_empty then dI' else dI; |
78 val cdI = if dI = ThyC.id_empty then dI' else dI; |
81 val cpI = if pI = Problem.id_empty then pI' else pI; |
79 val cpI = if pI = Problem.id_empty then pI' else pI; |
82 val cmI = if mI = MethodC.id_empty then mI' else mI; |
80 val cmI = if mI = MethodC.id_empty then mI' else mI; |
83 val {ppc = pbt, prls, where_, ...} = Problem.from_store_PIDE ctxt cpI; |
81 val {ppc = pbt, prls, where_, ...} = Problem.from_store ctxt cpI; |
84 val {ppc = mpc, ...} = MethodC.from_store_PIDE ctxt cmI |
82 val {ppc = mpc, ...} = MethodC.from_store ctxt cmI |
85 val (preok, _) = Pre_Conds.check prls where_ pbl 0; |
83 val (preok, _) = Pre_Conds.check prls where_ pbl 0; |
86 in |
84 in |
87 if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then |
85 if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then |
88 ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI')) |
86 ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI')) |
89 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then |
87 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then |
113 end |
111 end |
114 |
112 |
115 fun for_method_PIDE ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) = |
113 fun for_method_PIDE ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) = |
116 let |
114 let |
117 val cmI = if mI = MethodC.id_empty then mI' else mI; |
115 val cmI = if mI = MethodC.id_empty then mI' else mI; |
118 val {ppc = mpc, prls, pre, ...} = MethodC.from_store_PIDE ctxt cmI; (*..MethodC ?*) |
116 val {ppc = mpc, prls, pre, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*) |
119 val (preok, _) = Pre_Conds.check prls pre pbl 0; |
117 val (preok, _) = Pre_Conds.check prls pre pbl 0; |
120 in |
118 in |
121 (case find_first (I_Model.is_error o #5) met of |
119 (case find_first (I_Model.is_error o #5) met of |
122 SOME (_,_,_, fd, itm_) => |
120 SOME (_,_,_, fd, itm_) => |
123 ("dummy", (Pos.Met, |
121 ("dummy", (Pos.Met, |
162 let |
160 let |
163 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos) |
161 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos) |
164 val (i_model, m_patt) = |
162 val (i_model, m_patt) = |
165 if p_ = Pos.Met then |
163 if p_ = Pos.Met then |
166 (met, |
164 (met, |
167 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store_PIDE ctxt |> #ppc) |
165 (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #ppc) |
168 else |
166 else |
169 (pbl, |
167 (pbl, |
170 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store_PIDE ctxt |> #ppc) |
168 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #ppc) |
171 in |
169 in |
172 case I_Model.check_single ctxt m_field oris i_model m_patt ct of |
170 case I_Model.check_single ctxt m_field oris i_model m_patt ct of |
173 I_Model.Add i_single => (*..union old input *) |
171 I_Model.Add i_single => (*..union old input *) |
174 let |
172 let |
175 val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model |
173 val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model |
192 val (oris, ospec, probl, spec) = case Ctree.get_obj I pt p of |
190 val (oris, ospec, probl, spec) = case Ctree.get_obj I pt p of |
193 Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec) |
191 Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec) |
194 | _ => raise ERROR "finish_phase: unvered case get_obj" |
192 | _ => raise ERROR "finish_phase: unvered case get_obj" |
195 val (_, pI, mI) = References.select_input ospec spec |
193 val (_, pI, mI) = References.select_input ospec spec |
196 val ctxt = Ctree.get_ctxt pt pos |
194 val ctxt = Ctree.get_ctxt pt pos |
197 val mpc = (#ppc o MethodC.from_store_PIDE ctxt) mI |
195 val mpc = (#ppc o MethodC.from_store ctxt) mI |
198 val ppc = (#ppc o Problem.from_store_PIDE ctxt) pI |
196 val ppc = (#ppc o Problem.from_store ctxt) pI |
199 val (pits, mits) = I_Model.complete_method (oris, mpc, ppc, probl) |
197 val (pits, mits) = I_Model.complete_method (oris, mpc, ppc, probl) |
200 val pt = Ctree.update_pblppc pt p pits |
198 val pt = Ctree.update_pblppc pt p pits |
201 val pt = Ctree.update_metppc pt p mits |
199 val pt = Ctree.update_metppc pt p mits |
202 in (pt, (p, Pos.Met)) end |
200 in (pt, (p, Pos.Met)) end |
203 |
|
204 (*an unclarified remainder of the transition from sessions to PIDE with ctxt*) |
|
205 fun finish_phase_PIDEnote ctxt (o_model, o_refs) (problem_model, refs) = |
|
206 let |
|
207 val (_, pI, mI) = References.select_input o_refs refs |
|
208 val method_pattern = (#ppc o MethodC.from_store_PIDE ctxt) mI |
|
209 val problem_pattern = (#ppc o Problem.from_store_PIDE ctxt) pI |
|
210 val (problem_model, method_model) = |
|
211 I_Model.complete_method (o_model, method_pattern, problem_pattern, problem_model) |
|
212 in (problem_model, method_model) end |
|
213 |
201 |
214 (* do all specification in one single step: |
202 (* do all specification in one single step: |
215 complete calc-head for autocalc (sub-)pbl from oris (+ met from fmz); |
203 complete calc-head for autocalc (sub-)pbl from oris (+ met from fmz); |
216 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem |
204 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem |
217 *) |
205 *) |
220 val (pors, dI, pI, mI) = case Ctree.get_obj I pt p of |
208 val (pors, dI, pI, mI) = case Ctree.get_obj I pt p of |
221 Ctree.PblObj {origin = (pors, (dI, pI, mI), _), ...} |
209 Ctree.PblObj {origin = (pors, (dI, pI, mI), _), ...} |
222 => (pors, dI, pI, mI) |
210 => (pors, dI, pI, mI) |
223 | _ => raise ERROR "do_all: uncovered case get_obj" |
211 | _ => raise ERROR "do_all: uncovered case get_obj" |
224 val ctxt = Ctree.get_ctxt pt pos |
212 val ctxt = Ctree.get_ctxt pt pos |
225 val {ppc, ...} = MethodC.from_store_PIDE ctxt mI |
213 val {ppc, ...} = MethodC.from_store ctxt mI |
226 val (_, vals) = O_Model.values' pors |
214 val (_, vals) = O_Model.values' pors |
227 val ctxt = ContextC.initialise dI vals |
215 val ctxt = ContextC.initialise dI vals |
228 val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI), |
216 val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI), |
229 map (I_Model.complete' ppc) pors, map (I_Model.complete' ppc) pors, ctxt) |
217 map (I_Model.complete' ppc) pors, map (I_Model.complete' ppc) pors, ctxt) |
230 in |
218 in |