27 val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of |
27 val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of |
28 PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt) |
28 PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt) |
29 | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj" |
29 | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj" |
30 val (_, pI, mI) = References.select_input ospec spec |
30 val (_, pI, mI) = References.select_input ospec spec |
31 val mpc = (#ppc o MethodC.from_store ctxt) mI (* just for reuse I_Model.complete_method *) |
31 val mpc = (#ppc o MethodC.from_store ctxt) mI (* just for reuse I_Model.complete_method *) |
32 val {cas, ppc, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI |
32 val {cas, model, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI |
33 val pbl = I_Model.init ppc (* fill in descriptions *) |
33 val pbl = I_Model.init model (* fill in descriptions *) |
34 (*----------------if you think, this should be done by the Dialog |
34 (*----------------if you think, this should be done by the Dialog |
35 in the java front-end, search there for WN060225-modelProblem----*) |
35 in the java front-end, search there for WN060225-modelProblem----*) |
36 val (pbl, met) = case cas of |
36 val (pbl, met) = case cas of |
37 NONE => (pbl, []) |
37 NONE => (pbl, []) |
38 | _ => I_Model.complete_method (oris, mpc, ppc, probl) |
38 | _ => I_Model.complete_method (oris, mpc, model, probl) |
39 (*----------------------------------------------------------------*) |
39 (*----------------------------------------------------------------*) |
40 val tac_ = Tactic.Model_Problem' (pI, pbl, met) |
40 val tac_ = Tactic.Model_Problem' (pI, pbl, met) |
41 val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos) |
41 val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos) |
42 in |
42 in |
43 ("ok",([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos))) |
43 ("ok",([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos))) |
55 val opt = Refine.refine_ori ctxt oris pI |
55 val opt = Refine.refine_ori ctxt oris pI |
56 in |
56 in |
57 case opt of |
57 case opt of |
58 SOME pI' => |
58 SOME pI' => |
59 let |
59 let |
60 val {met, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI' |
60 val {solve_mets, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI' |
61 (*val pt = update_pbl pt p pbl ..done by Model_Problem*) |
61 (*val pt = update_pbl pt p pbl ..done by Model_Problem*) |
62 val mI = if length met = 0 then MethodC.id_empty else hd met |
62 val mI = if length solve_mets = 0 then MethodC.id_empty else hd solve_mets |
63 val (pos, c, _, pt) = |
63 val (pos, c, _, pt) = |
64 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos) |
64 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos) |
65 in |
65 in |
66 ("ok", ([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]), |
66 ("ok", ([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]), |
67 (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos))) |
67 (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos))) |
91 val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of |
91 val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of |
92 PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} => |
92 PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} => |
93 (oris, dI, dI', pI', probl, ctxt) |
93 (oris, dI, dI', pI', probl, ctxt) |
94 | _ => raise ERROR "" |
94 | _ => raise ERROR "" |
95 val thy = ThyC.get_theory_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI'); |
95 val thy = ThyC.get_theory_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI'); |
96 val {ppc,where_,prls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI |
96 val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI |
97 val pbl = |
97 val pbl = |
98 if pI' = Problem.id_empty andalso pI = Problem.id_empty |
98 if pI' = Problem.id_empty andalso pI = Problem.id_empty |
99 then (false, (I_Model.init ppc, [])) |
99 then (false, (I_Model.init model, [])) |
100 else M_Match.match_itms_oris thy probl (ppc,where_,prls) oris |
100 else M_Match.match_itms_oris thy probl (model, where_, where_rls) oris |
101 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*) |
101 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*) |
102 val (c, pt) = |
102 val (c, pt) = |
103 case Specify_Step.add (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of |
103 case Specify_Step.add (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of |
104 ((_, Pbl), c, _, pt) => (c, pt) |
104 ((_, Pbl), c, _, pt) => (c, pt) |
105 | _ => raise ERROR "" |
105 | _ => raise ERROR "" |
146 ("ok", ([], [], (pt, (p, Pbl)))) |
146 ("ok", ([], [], (pt, (p, Pbl)))) |
147 end |
147 end |
148 (* called only if no_met is specified *) |
148 (* called only if no_met is specified *) |
149 | by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) = |
149 | by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) = |
150 let |
150 let |
151 val {met, thy,...} = Problem.from_store (Ctree.get_ctxt pt pos) pIre |
151 val {solve_mets, thy,...} = Problem.from_store (Ctree.get_ctxt pt pos) pIre |
152 val (domID, metID) = (Context.theory_name thy, if length met = 0 then MethodC.id_empty else hd met) |
152 val (domID, metID) = (Context.theory_name thy, |
|
153 if length solve_mets = 0 then MethodC.id_empty |
|
154 else hd solve_mets) |
153 val ((p,_), _, _, pt) = |
155 val ((p,_), _, _, pt) = |
154 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) |
156 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) |
155 (Istate_Def.Uistate, ContextC.empty) (pt, pos) |
157 (Istate_Def.Uistate, ContextC.empty) (pt, pos) |
156 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *) |
158 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *) |
157 in |
159 in |
216 val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise *) |
218 val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise *) |
217 val (pI, (pors, pctxt), mI) = |
219 val (pI, (pors, pctxt), mI) = |
218 if mI = ["no_met"] |
220 if mI = ["no_met"] |
219 then |
221 then |
220 let |
222 let |
221 val pors = Problem.from_store ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*) |
223 val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*) |
222 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*) |
224 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*) |
223 val pI' = Refine.refine_ori' pctxt pors pI; |
225 val pI' = Refine.refine_ori' pctxt pors pI; |
224 in (pI', (pors (*refinement over models with diff.precond only*), pctxt), |
226 in (pI', (pors (*refinement over models with diff.precond only*), pctxt), |
225 (hd o #met o Problem.from_store ctxt) pI') |
227 (hd o #solve_mets o Problem.from_store ctxt) pI') |
226 end |
228 end |
227 else |
229 else |
228 let |
230 let |
229 val pors = Problem.from_store ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*) |
231 val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*) |
230 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*) |
232 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*) |
231 in (pI, (pors, pctxt), mI) end; |
233 in (pI, (pors, pctxt), mI) end; |
232 val {cas, ppc, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*) |
234 val {cas, model, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*) |
233 val dI = Context.theory_name (ThyC.sub_common (thy, thy')) |
235 val dI = Context.theory_name (ThyC.sub_common (thy, thy')) |
234 val hdl = case cas of |
236 val hdl = case cas of |
235 NONE => Auto_Prog.pblterm dI pI |
237 NONE => Auto_Prog.pblterm dI pI |
236 | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t |
238 | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t |
237 val hdlPIDE = case cas of |
239 val hdlPIDE = case cas of |
238 NONE => Auto_Prog.pblterm dI pI |
240 NONE => Auto_Prog.pblterm dI pI |
239 | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t |
241 | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t |
240 in |
242 in |
241 (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt) |
243 (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt) |
242 end; |
244 end; |
243 (*TODO: HOW RELATES nxt_specify_init_calc \<longleftrightarrow> initialise *) |
245 (*TODO: HOW RELATES nxt_specify_init_calc \<longleftrightarrow> initialise *) |
244 fun nxt_specify_init_calc ctxt ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*) |
246 fun nxt_specify_init_calc ctxt ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*) |
245 if pI <> [] |
247 if pI <> [] |
246 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *) |
248 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *) |
247 let |
249 let |
248 val {cas, met, ppc, thy, ...} = Problem.from_store ctxt pI |
250 val {cas, solve_mets, model, thy, ...} = Problem.from_store ctxt pI |
249 val dI = if dI = "" then Context.theory_name thy else dI |
251 val dI = if dI = "" then Context.theory_name thy else dI |
250 val mI = if mI = [] then hd met else mI |
252 val mI = if mI = [] then hd solve_mets else mI |
251 val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t |
253 val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t |
252 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI)) |
254 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI)) |
253 ([], (dI,pI,mI), hdl, ContextC.empty) |
255 ([], (dI,pI,mI), hdl, ContextC.empty) |
254 val pt = update_spec pt [] (dI, pI, mI) |
256 val pt = update_spec pt [] (dI, pI, mI) |
255 val pits = I_Model.init ppc |
257 val pits = I_Model.init model |
256 val pt = update_pbl pt [] pits |
258 val pt = update_pbl pt [] pits |
257 in ((pt, ([] , Pbl)), []) end |
259 in ((pt, ([] , Pbl)), []) end |
258 else |
260 else |
259 if mI <> [] |
261 if mI <> [] |
260 then (* from met-browser *) |
262 then (* from met-browser *) |