9 val by_tactic_input: Tactic.input -> Calc.T -> string * Calc.state_post |
9 val by_tactic_input: Tactic.input -> Calc.T -> string * Calc.state_post |
10 val by_tactic: Tactic.T -> Calc.T -> string * Calc.state_post |
10 val by_tactic: Tactic.T -> Calc.T -> string * Calc.state_post |
11 |
11 |
12 val initialise: Proof.context -> Formalise.T -> |
12 val initialise: Proof.context -> Formalise.T -> |
13 term * term * References.T * O_Model.T * Proof.context |
13 term * term * References.T * O_Model.T * Proof.context |
|
14 val initialise_PIDE: theory -> Formalise.T -> |
|
15 term * term * References.T * O_Model.T * Proof.context |
14 val nxt_specify_init_calc: Proof.context -> Formalise.T -> Calc.T * State_Steps.T |
16 val nxt_specify_init_calc: Proof.context -> Formalise.T -> Calc.T * State_Steps.T |
|
17 val nxt_specify_init_calc_PIDE: theory -> Formalise.T -> Calc.T * State_Steps.T |
15 end |
18 end |
16 |
19 |
17 (**) |
20 (**) |
18 structure Step_Specify(**): STEP_SPECIFY(**) = |
21 structure Step_Specify(**): STEP_SPECIFY(**) = |
19 struct |
22 struct |
233 else |
236 else |
234 let |
237 let |
235 val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*) |
238 val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*) |
236 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*) |
239 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*) |
237 in (pI, (pors, pctxt), mI) end; |
240 in (pI, (pors, pctxt), mI) end; |
|
241 val {cas, model, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*) |
|
242 val dI = Context.theory_name (Sub_Problem.common_sub_thy (thy, thy')) |
|
243 val hdl = case cas of |
|
244 NONE => Auto_Prog.pblterm dI pI |
|
245 | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t |
|
246 val hdlPIDE = case cas of |
|
247 NONE => Auto_Prog.pblterm dI pI |
|
248 | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t |
|
249 in |
|
250 (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt) |
|
251 end; |
|
252 (* initialise <-?-> nxt_specify_init_calc *) |
|
253 fun initialise_PIDE thy (fmz, (_, pI, mI)) = |
|
254 let |
|
255 (*old* )val thy = ThyC.get_theory_PIDE ctxt dI( *old*) |
|
256 val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise *) |
|
257 val (pI, (pors, pctxt), mI) = |
|
258 if mI = ["no_met"] |
|
259 then |
|
260 let |
|
261 (*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*) |
|
262 (*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*) |
|
263 ( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz; |
|
264 val pI' = Refine.refine_ori' pctxt pors pI; |
|
265 in (pI', (pors (*refinement over models with diff.precond only*), pctxt), |
|
266 (hd o #solve_mets o Problem.from_store ctxt) pI') |
|
267 end |
|
268 else |
|
269 let |
|
270 (*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*) |
|
271 (*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*) |
|
272 (*old*) in (pI, (pors, pctxt), mI) end; |
|
273 ( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz; |
|
274 in (pI, (pors, pctxt), mI) end; |
238 val {cas, model, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*) |
275 val {cas, model, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*) |
239 val dI = Context.theory_name (Sub_Problem.common_sub_thy (thy, thy')) |
276 val dI = Context.theory_name (Sub_Problem.common_sub_thy (thy, thy')) |
240 val hdl = case cas of |
277 val hdl = case cas of |
241 NONE => Auto_Prog.pblterm dI pI |
278 NONE => Auto_Prog.pblterm dI pI |
242 | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t |
279 | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t |
284 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt) |
321 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt) |
285 (model, (dI, pI, mI)) (pors, (dI, pI, mI), hdl, pctxt) |
322 (model, (dI, pI, mI)) (pors, (dI, pI, mI), hdl, pctxt) |
286 in |
323 in |
287 ((pt, ([], Pbl)), (fst3 o snd) (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl)))) |
324 ((pt, ([], Pbl)), (fst3 o snd) (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl)))) |
288 end |
325 end |
289 |
326 fun nxt_specify_init_calc_PIDE thy ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*) |
|
327 if pI <> [] |
|
328 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *) |
|
329 let |
|
330 val {cas, solve_mets, model, thy, ...} = Problem.from_store (Proof_Context.init_global thy) pI |
|
331 val dI = if dI = "" then Context.theory_name thy else dI |
|
332 val mI = if mI = [] then hd solve_mets else mI |
|
333 val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t |
|
334 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI)) |
|
335 ([], (dI,pI,mI), hdl, ContextC.empty) |
|
336 val pt = update_spec pt [] (dI, pI, mI) |
|
337 val pits = I_Model.init model |
|
338 val pt = update_pbl pt [] pits |
|
339 in ((pt, ([] , Pbl)), []) end |
|
340 else |
|
341 if mI <> [] |
|
342 then (* from met-browser *) |
|
343 let |
|
344 val {model, ...} = MethodC.from_store (Proof_Context.init_global thy) mI |
|
345 val dI = if dI = "" then "Isac_Knowledge" else dI |
|
346 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) |
|
347 ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty) |
|
348 val pt = update_spec pt [] (dI, pI, mI) |
|
349 val mits = I_Model.init model |
|
350 val pt = update_met pt [] mits |
|
351 in ((pt, ([], Met)), []) end |
|
352 else (* new example, pepare for interactive modeling *) |
|
353 let |
|
354 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) |
|
355 ([], References.empty) ([], References.empty, TermC.empty, ContextC.empty) |
|
356 in ((pt, ([], Pbl)), []) end |
|
357 | nxt_specify_init_calc_PIDE thy (model, refs) = |
|
358 let (* both ^^^^^ ^^^^^^^^^^^^ are either empty or complete *) |
|
359 val (_, hdl, refs, pors, pctxt) = initialise_PIDE thy (model, refs) |
|
360 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt) |
|
361 (model, refs) (pors, refs, hdl, pctxt) |
|
362 in |
|
363 ((pt, ([], Pbl)), (fst3 o snd) (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl)))) |
|
364 end |
|
365 |
290 (**)end(**) |
366 (**)end(**) |