Walther@60610
|
1 |
signature SUB_PROBLEM =
|
Walther@60610
|
2 |
sig
|
Walther@60610
|
3 |
val tac_from_prog: Ctree.state -> term -> Tactic.input * Tactic.T
|
Walther@60610
|
4 |
val common_sub_thy: theory * theory -> theory
|
Walther@60610
|
5 |
end
|
Walther@60610
|
6 |
|
Walther@60610
|
7 |
(**)
|
Walther@60610
|
8 |
structure Sub_Problem(**): SUB_PROBLEM(**) =
|
Walther@60610
|
9 |
struct
|
Walther@60610
|
10 |
(**)
|
Walther@60610
|
11 |
|
Walther@60610
|
12 |
fun common_sub_thy (thy1, thy2) =
|
Walther@60610
|
13 |
if Context.subthy (thy1, thy2) then thy2
|
Walther@60610
|
14 |
else if Context.subthy (thy2, thy1) then thy1
|
Walther@60610
|
15 |
else Know_Store.get_ref_last_thy ()
|
Walther@60610
|
16 |
|
Walther@60742
|
17 |
fun tac_from_prog (pt, _) (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ spec' $ ags') =
|
Walther@60610
|
18 |
let
|
Walther@60610
|
19 |
val (dI, pI, mI) = Prog_Tac.dest_spec spec'
|
Walther@60610
|
20 |
val thy = common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt);
|
Walther@60610
|
21 |
val init_ctxt = Proof_Context.init_global thy
|
Walther@60610
|
22 |
val ags = TermC.isalist2list ags';
|
Walther@60610
|
23 |
val (pI, pors, mI) =
|
Walther@60610
|
24 |
if mI = ["no_met"]
|
Walther@60610
|
25 |
then
|
Walther@60610
|
26 |
let
|
Walther@60610
|
27 |
val pors = (M_Match.arguments thy ((#model o (Problem.from_store init_ctxt)) pI) ags): O_Model.T
|
Walther@60610
|
28 |
handle ERROR "actual args do not match formal args"
|
Walther@60610
|
29 |
=> (M_Match.arguments_msg init_ctxt pI stac ags (*raise exn*);[]);
|
Walther@60742
|
30 |
val pI' = Refine.by_o_model' init_ctxt pors pI;
|
Walther@60640
|
31 |
in (pI', pors (* refinement over models with diff.precond only *),
|
Walther@60610
|
32 |
(hd o #solve_mets o Problem.from_store init_ctxt) pI') end
|
Walther@60610
|
33 |
else (pI, (M_Match.arguments thy ((#model o Problem.from_store init_ctxt) pI) ags)
|
Walther@60610
|
34 |
handle ERROR "actual args do not match formal args"
|
Walther@60610
|
35 |
=> (M_Match.arguments_msg init_ctxt pI stac ags(*raise exn*); []), mI);
|
Walther@60610
|
36 |
val (fmz_, vals) = O_Model.values' init_ctxt pors;
|
Walther@60610
|
37 |
val {cas, model, thy, ...} = Problem.from_store init_ctxt pI
|
Walther@60610
|
38 |
val dI = Context.theory_name thy (*take dI from _refined_ pbl*)
|
Walther@60610
|
39 |
val dI = Context.theory_name
|
Walther@60610
|
40 |
(common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt))
|
Walther@60654
|
41 |
val ctxt = ContextC.init_for_prog init_ctxt vals
|
Walther@60610
|
42 |
val hdl =
|
Walther@60610
|
43 |
case cas of
|
Walther@60610
|
44 |
NONE => Auto_Prog.pblterm dI pI
|
Walther@60610
|
45 |
| SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ vals) t
|
Walther@60682
|
46 |
val f = Auto_Prog.subpbl (ThmC.cut_longid dI) pI
|
Walther@60610
|
47 |
in
|
Walther@60610
|
48 |
(Tactic.Subproblem (dI, pI), Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
|
Walther@60610
|
49 |
end
|
Walther@60673
|
50 |
| tac_from_prog _ t =
|
Walther@60678
|
51 |
raise ERROR ("Sub_Problem.tac_from_prog not impl. for " ^ UnparseC.term (ContextC.for_ERROR ()) t)
|
Walther@60610
|
52 |
|
Walther@60610
|
53 |
(**)end(**)
|