walther@59747
|
1 |
(* Title: Specify/step-specify.sml
|
walther@59747
|
2 |
Author: Walther Neuper 2019
|
walther@59747
|
3 |
(c) due to copyright terms
|
walther@59747
|
4 |
*)
|
walther@59747
|
5 |
|
walther@59747
|
6 |
signature STEP_SPECIFY =
|
walther@59747
|
7 |
sig
|
walther@59791
|
8 |
(*val do_next: Step.specify_do_next requires LI.by_tactic, which is not yet known in Step_Specify*)
|
walther@60020
|
9 |
val by_tactic_input: Tactic.input -> Calc.T -> string * Calc.state_post
|
walther@59981
|
10 |
val by_tactic: Tactic.T -> Calc.T -> string * Calc.state_post
|
walther@59975
|
11 |
|
Walther@60652
|
12 |
val initialise: theory -> Formalise.T ->
|
walther@60114
|
13 |
term * term * References.T * O_Model.T * Proof.context
|
Walther@60652
|
14 |
val initialise': theory -> Formalise.T -> Calc.T * State_Steps.T
|
walther@59747
|
15 |
end
|
walther@59747
|
16 |
|
walther@59747
|
17 |
(**)
|
walther@59747
|
18 |
structure Step_Specify(**): STEP_SPECIFY(**) =
|
walther@59747
|
19 |
struct
|
walther@59747
|
20 |
(**)
|
walther@59763
|
21 |
open Pos
|
walther@59763
|
22 |
open Ctree
|
walther@59977
|
23 |
open Specification
|
walther@59747
|
24 |
|
walther@59806
|
25 |
fun by_tactic_input (tac as Tactic.Model_Problem) (pt, pos as (p, _)) =
|
walther@59763
|
26 |
let
|
Walther@60752
|
27 |
val (oris, ospec, probl, spec, ctxt, meth) = case get_obj I pt p of
|
Walther@60752
|
28 |
PblObj {origin = (oris, ospec, _), probl, spec, ctxt, meth, ...} => (oris, ospec, probl, spec, ctxt, meth)
|
walther@59962
|
29 |
| _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
|
Walther@60494
|
30 |
val (_, pI, mI) = References.select_input ospec spec
|
Walther@60585
|
31 |
val {cas, model, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
|
Walther@60782
|
32 |
val pbl = I_Model.init ctxt oris model (* fill in descriptions *)
|
walther@59763
|
33 |
val (pbl, met) = case cas of
|
walther@59763
|
34 |
NONE => (pbl, [])
|
Walther@60779
|
35 |
| _ => I_Model.s_make_complete ctxt oris (probl, meth) (pI, mI)
|
Walther@60774
|
36 |
val tac_ = Tactic.Model_Problem' (pI, pbl, met)
|
walther@59933
|
37 |
val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos)
|
walther@60020
|
38 |
in
|
walther@60020
|
39 |
("ok",([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)))
|
walther@60020
|
40 |
end
|
walther@60021
|
41 |
| by_tactic_input (Tactic.Add_Given ct) ptp = Specify.by_Add_ "#Given" ct ptp
|
walther@60021
|
42 |
| by_tactic_input (Tactic.Add_Find ct) ptp = Specify.by_Add_ "#Find" ct ptp
|
walther@60021
|
43 |
| by_tactic_input (Tactic.Add_Relation ct) ptp = Specify.by_Add_"#Relate" ct ptp
|
walther@60021
|
44 |
|
walther@60154
|
45 |
(* called with MethodC.id_empty *)
|
walther@59810
|
46 |
| by_tactic_input (Tactic.Refine_Tacitly pI) (ptp as (pt, pos as (p, _))) =
|
walther@59763
|
47 |
let
|
walther@59763
|
48 |
val (oris, dI, ctxt) = case get_obj I pt p of
|
walther@59763
|
49 |
(PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
|
walther@59962
|
50 |
| _ => raise ERROR "by_tactic_input Refine_Tacitly: uncovered case get_obj"
|
Walther@60742
|
51 |
val opt = Refine.by_o_model ctxt oris pI
|
walther@59763
|
52 |
in
|
walther@59763
|
53 |
case opt of
|
walther@59763
|
54 |
SOME pI' =>
|
Walther@60556
|
55 |
let
|
Walther@60585
|
56 |
val {solve_mets, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
|
walther@59763
|
57 |
(*val pt = update_pbl pt p pbl ..done by Model_Problem*)
|
Walther@60585
|
58 |
val mI = if length solve_mets = 0 then MethodC.id_empty else hd solve_mets
|
walther@59763
|
59 |
val (pos, c, _, pt) =
|
walther@59933
|
60 |
Specify_Step.add (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos)
|
walther@59763
|
61 |
in
|
walther@60020
|
62 |
("ok", ([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
|
walther@60020
|
63 |
(pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)))
|
walther@59763
|
64 |
end
|
walther@60021
|
65 |
| NONE => ("failure", ([], [], ptp))
|
walther@59763
|
66 |
end
|
walther@59806
|
67 |
| by_tactic_input (Tactic.Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
|
walther@59763
|
68 |
let
|
walther@59763
|
69 |
val (dI, dI', probl, ctxt) = case get_obj I pt p of
|
walther@59763
|
70 |
PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
|
walther@59763
|
71 |
(dI, dI', probl, ctxt)
|
walther@59962
|
72 |
| _ => raise ERROR "by_tactic_input Refine_Problem: uncovered case get_obj"
|
walther@59879
|
73 |
val thy = if dI' = ThyC.id_empty then dI else dI'
|
walther@59763
|
74 |
in
|
Walther@60779
|
75 |
case Refine.problem (ThyC.get_theory ctxt thy) pI probl of
|
walther@60021
|
76 |
NONE => ("failure", ([], [], ptp))
|
Walther@60774
|
77 |
| SOME (pI, (i_model, prec)) =>
|
walther@59763
|
78 |
let
|
Walther@60775
|
79 |
val (pos,c,_,pt) = Specify_Step.add (Tactic.Refine_Problem' (pI, (i_model, prec)) )
|
Walther@60774
|
80 |
(Istate_Def.Uistate, ctxt) (pt, pos)
|
walther@59763
|
81 |
in
|
Walther@60775
|
82 |
("ok", ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' (pI, (i_model, prec)),
|
Walther@60774
|
83 |
(pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos)))
|
walther@59763
|
84 |
end
|
walther@59763
|
85 |
end
|
walther@60020
|
86 |
| by_tactic_input (Tactic.Specify_Problem pI) (pt, pos as (p, _)) =
|
walther@59763
|
87 |
let
|
Walther@60760
|
88 |
val (oris, pI', probl, meth, ctxt) = case get_obj I pt p of
|
Walther@60760
|
89 |
PblObj {origin = (oris, _, _), spec = (_ ,pI',_), probl, meth, ctxt, ...} =>
|
Walther@60760
|
90 |
(oris, pI', probl, meth, ctxt)
|
walther@59962
|
91 |
| _ => raise ERROR ""
|
Walther@60585
|
92 |
val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
|
Walther@60760
|
93 |
val (check, (i_model, preconds)) =
|
walther@59903
|
94 |
if pI' = Problem.id_empty andalso pI = Problem.id_empty
|
Walther@60782
|
95 |
then (false, (I_Model.init ctxt oris model, []))
|
Walther@60779
|
96 |
else M_Match.by_i_models ctxt oris (probl, meth) (model, where_, where_rls)
|
walther@59810
|
97 |
val (c, pt) =
|
Walther@60774
|
98 |
case Specify_Step.add (Tactic.Specify_Problem' (pI, (check, (i_model, preconds)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
|
walther@59810
|
99 |
((_, Pbl), c, _, pt) => (c, pt)
|
walther@59962
|
100 |
| _ => raise ERROR ""
|
walther@59763
|
101 |
in
|
Walther@60774
|
102 |
("ok", ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, (check, ( i_model, preconds))),
|
walther@60020
|
103 |
(pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos)))
|
walther@59763
|
104 |
end
|
walther@60014
|
105 |
| by_tactic_input (Tactic.Specify_Method id) (pt, pos) =
|
walther@59763
|
106 |
let
|
walther@60014
|
107 |
val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos)
|
Walther@60774
|
108 |
val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, i_model))
|
walther@60014
|
109 |
(Istate_Def.Uistate, ctxt) (pt, pos)
|
walther@60011
|
110 |
in
|
Walther@60774
|
111 |
("ok", ([(Tactic.Specify_Method id, Tactic.Specify_Method' (id, o_model, i_model),
|
walther@60020
|
112 |
(pos, (Istate_Def.Uistate, ContextC.empty)))], [], (pt, pos)))
|
walther@59763
|
113 |
end
|
walther@59806
|
114 |
| by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) =
|
walther@59763
|
115 |
let
|
walther@59763
|
116 |
val ctxt = get_ctxt pt pos
|
walther@60014
|
117 |
val (pos, c, _, pt) =
|
walther@59933
|
118 |
Specify_Step.add (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) (pt, pos)
|
walther@59763
|
119 |
in (*FIXXXME: check if pbl can still be parsed*)
|
walther@60020
|
120 |
("ok", ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI,
|
walther@60020
|
121 |
(pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos)))
|
walther@59763
|
122 |
end
|
walther@59806
|
123 |
| by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Met)) =
|
walther@59763
|
124 |
let
|
walther@59763
|
125 |
val ctxt = get_ctxt pt pos
|
walther@59933
|
126 |
val (pos, c, _, pt) = Specify_Step.add (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) (pt, pos)
|
walther@59763
|
127 |
in (*FIXXXME: check if met can still be parsed*)
|
walther@60020
|
128 |
("ok", ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI,
|
walther@60020
|
129 |
(pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos)))
|
walther@59763
|
130 |
end
|
Walther@60628
|
131 |
| by_tactic_input m' (ctree, pos) =
|
Walther@60628
|
132 |
let
|
Walther@60628
|
133 |
val ctxt = Ctree.get_ctxt ctree pos
|
Walther@60628
|
134 |
in
|
Walther@60628
|
135 |
raise ERROR ("by_tactic_input: not impl. for " ^ Tactic.input_to_string ctxt m')
|
Walther@60628
|
136 |
end
|
walther@60020
|
137 |
(**)
|
walther@60020
|
138 |
|
walther@59806
|
139 |
|
walther@60015
|
140 |
fun by_tactic (Tactic.Model_Problem' (id, pbl, met)) (pt, pos) =
|
walther@59806
|
141 |
let
|
walther@60015
|
142 |
val ((p, _), _, _, pt) = Specify_Step.add (Tactic.Model_Problem'(id, pbl, met))
|
walther@60015
|
143 |
(Istate_Def.Uistate, ContextC.empty) (pt, pos)
|
walther@60015
|
144 |
(* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
|
walther@59806
|
145 |
in
|
walther@59806
|
146 |
("ok", ([], [], (pt, (p, Pbl))))
|
walther@59806
|
147 |
end
|
walther@59806
|
148 |
(* called only if no_met is specified *)
|
walther@59806
|
149 |
| by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) =
|
walther@59806
|
150 |
let
|
Walther@60585
|
151 |
val {solve_mets, thy,...} = Problem.from_store (Ctree.get_ctxt pt pos) pIre
|
Walther@60585
|
152 |
val (domID, metID) = (Context.theory_name thy,
|
Walther@60585
|
153 |
if length solve_mets = 0 then MethodC.id_empty
|
Walther@60585
|
154 |
else hd solve_mets)
|
walther@59806
|
155 |
val ((p,_), _, _, pt) =
|
walther@59933
|
156 |
Specify_Step.add (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
|
walther@59846
|
157 |
(Istate_Def.Uistate, ContextC.empty) (pt, pos)
|
walther@59806
|
158 |
(* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
|
walther@59806
|
159 |
in
|
walther@59806
|
160 |
("ok", ([], [], (pt,(p, Pbl))))
|
walther@59806
|
161 |
end
|
walther@60021
|
162 |
| by_tactic (Tactic.Refine_Problem' (rfd as (id, _))) (pt, pos) =
|
walther@59806
|
163 |
let
|
walther@59806
|
164 |
val ctxt = get_ctxt pt pos
|
walther@59806
|
165 |
val (pos, _, _, pt) =
|
walther@59933
|
166 |
Specify_Step.add (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)
|
walther@59806
|
167 |
in
|
walther@60021
|
168 |
("ok", ([(Tactic.Refine_Problem id, Tactic.Refine_Problem' rfd,
|
walther@60021
|
169 |
(pos, (Istate_Def.Uistate,ctxt)))], [], (pt, pos)))
|
walther@59806
|
170 |
end
|
Walther@60586
|
171 |
| by_tactic (Tactic.Specify_Problem' (pI, (ok, (itms, where_)))) (pt, pos as (p, _)) =
|
walther@59806
|
172 |
let
|
walther@59995
|
173 |
val (_, _, _, _, _, _, ctxt, _) = case get_obj I pt p of
|
walther@59806
|
174 |
PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>
|
walther@59806
|
175 |
(oris, dI', pI', mI', dI, mI, ctxt, met)
|
walther@59962
|
176 |
| _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
|
walther@59806
|
177 |
val (p, pt) =
|
Walther@60586
|
178 |
case Specify_Step.add (Tactic.Specify_Problem' (pI, (ok, (itms, where_)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
|
walther@59806
|
179 |
((p, Pbl), _, _, pt) => (p, pt)
|
walther@59962
|
180 |
| _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
|
walther@59806
|
181 |
in
|
walther@59806
|
182 |
("ok", ([], [], (pt, (p, Pbl))))
|
walther@59806
|
183 |
end
|
walther@60014
|
184 |
| by_tactic (Tactic.Specify_Method' (id, _, _)) (pt, pos) =
|
walther@59806
|
185 |
let
|
walther@60014
|
186 |
val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos)
|
Walther@60774
|
187 |
val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, i_model))
|
walther@60014
|
188 |
(Istate_Def.Uistate, ctxt) (pt, pos)
|
walther@60011
|
189 |
in
|
walther@59806
|
190 |
("ok", ([], [], (pt, pos)))
|
walther@60014
|
191 |
end
|
walther@60016
|
192 |
| by_tactic (Tactic.Add_Given' (ct, _)) (pt, p) = Specify.by_Add_ "#Given" ct (pt, p)
|
walther@60016
|
193 |
| by_tactic (Tactic.Add_Find' (ct, _)) (pt, p) = Specify.by_Add_ "#Find" ct (pt, p)
|
walther@60016
|
194 |
| by_tactic (Tactic.Add_Relation' (ct, _)) (pt, p) = Specify.by_Add_"#Relate" ct (pt, p)
|
walther@60020
|
195 |
(*strange old code, redes*)
|
walther@60015
|
196 |
| by_tactic (Tactic.Specify_Theory' domID) (pt, (p, p_)) =
|
walther@59806
|
197 |
let
|
walther@59806
|
198 |
val p_ = case p_ of Met => Met | _ => Pbl
|
walther@60015
|
199 |
val {spec = (dI, _, _), ctxt, ...} = Calc.specify_data (pt, (p, p_))
|
walther@59806
|
200 |
in
|
walther@60015
|
201 |
if domID = dI then
|
walther@60015
|
202 |
("ok", ([], [], (pt, (p, p_))))
|
Walther@60586
|
203 |
else (*FIXME: check model wrt. (new!) domID ..? still parsable?*)
|
walther@59806
|
204 |
let
|
walther@60015
|
205 |
val ((p, p_), _, _, pt) = Specify_Step.add (Tactic.Specify_Theory' domID)
|
walther@60015
|
206 |
(Istate_Def.Uistate, ctxt) (pt, (p, p_))
|
walther@59806
|
207 |
in
|
walther@59806
|
208 |
("ok", ([], [], (pt, (p, p_))))
|
walther@59990
|
209 |
end
|
walther@59806
|
210 |
end
|
walther@59806
|
211 |
| by_tactic _ _ = raise ERROR "Step_Specify.by_tactic uncovered pattern in fun.def"
|
walther@59806
|
212 |
|
Walther@60556
|
213 |
(* create a calc-tree with oris via a cas.refined pbl *)
|
Walther@60652
|
214 |
(* initialise <-?-> initialise' *)
|
Walther@60652
|
215 |
fun initialise thy (fmz, (_, pI, mI)) =
|
walther@60150
|
216 |
let
|
Walther@60576
|
217 |
val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise *)
|
walther@60150
|
218 |
val (pI, (pors, pctxt), mI) =
|
walther@60150
|
219 |
if mI = ["no_met"]
|
walther@60150
|
220 |
then
|
walther@60150
|
221 |
let
|
Walther@60653
|
222 |
val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
|
Walther@60742
|
223 |
val pI' = Refine.by_o_model' pctxt pors pI;
|
Walther@60651
|
224 |
in (pI', (pors (*refinement over models with diff.precond only*), pctxt),
|
Walther@60651
|
225 |
(hd o #solve_mets o Problem.from_store ctxt) pI')
|
Walther@60651
|
226 |
end
|
Walther@60651
|
227 |
else
|
Walther@60651
|
228 |
let
|
Walther@60653
|
229 |
val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
|
Walther@60651
|
230 |
in (pI, (pors, pctxt), mI) end;
|
Walther@60651
|
231 |
val {cas, model, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*)
|
Walther@60651
|
232 |
val dI = Context.theory_name (Sub_Problem.common_sub_thy (thy, thy'))
|
Walther@60651
|
233 |
val hdl = case cas of
|
Walther@60651
|
234 |
NONE => Auto_Prog.pblterm dI pI
|
Walther@60651
|
235 |
| SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t
|
Walther@60651
|
236 |
val hdlPIDE = case cas of
|
Walther@60651
|
237 |
NONE => Auto_Prog.pblterm dI pI
|
Walther@60651
|
238 |
| SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t
|
Walther@60651
|
239 |
in
|
Walther@60651
|
240 |
(hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)
|
Walther@60651
|
241 |
end;
|
Walther@60652
|
242 |
(*TODO: HOW RELATES initialise' \<longleftrightarrow> initialise *)
|
Walther@60652
|
243 |
fun initialise' thy ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*)
|
Walther@60651
|
244 |
if pI <> []
|
Walther@60651
|
245 |
then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
|
Walther@60651
|
246 |
let
|
Walther@60651
|
247 |
val {cas, solve_mets, model, thy, ...} = Problem.from_store (Proof_Context.init_global thy) pI
|
Walther@60651
|
248 |
val dI = if dI = "" then Context.theory_name thy else dI
|
Walther@60651
|
249 |
val mI = if mI = [] then hd solve_mets else mI
|
Walther@60651
|
250 |
val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
|
Walther@60651
|
251 |
val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
|
Walther@60651
|
252 |
([], (dI,pI,mI), hdl, ContextC.empty)
|
Walther@60651
|
253 |
val pt = update_spec pt [] (dI, pI, mI)
|
Walther@60782
|
254 |
val pits = I_Model.init (Proof_Context.init_global thy) [(*o_model*)] model
|
Walther@60651
|
255 |
val pt = update_pbl pt [] pits
|
Walther@60651
|
256 |
in ((pt, ([] , Pbl)), []) end
|
Walther@60651
|
257 |
else
|
Walther@60651
|
258 |
if mI <> []
|
Walther@60651
|
259 |
then (* from met-browser *)
|
Walther@60651
|
260 |
let
|
Walther@60651
|
261 |
val {model, ...} = MethodC.from_store (Proof_Context.init_global thy) mI
|
Walther@60651
|
262 |
val dI = if dI = "" then "Isac_Knowledge" else dI
|
Walther@60651
|
263 |
val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
|
Walther@60651
|
264 |
([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty)
|
Walther@60651
|
265 |
val pt = update_spec pt [] (dI, pI, mI)
|
Walther@60782
|
266 |
val mits = I_Model.init (Proof_Context.init_global thy) [(*o_model*)] model
|
Walther@60651
|
267 |
val pt = update_met pt [] mits
|
Walther@60651
|
268 |
in ((pt, ([], Met)), []) end
|
Walther@60651
|
269 |
else (* new example, pepare for interactive modeling *)
|
Walther@60651
|
270 |
let
|
Walther@60651
|
271 |
val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
|
Walther@60651
|
272 |
([], References.empty) ([], References.empty, TermC.empty, ContextC.empty)
|
Walther@60651
|
273 |
in ((pt, ([], Pbl)), []) end
|
Walther@60652
|
274 |
| initialise' thy (model, refs) =
|
Walther@60651
|
275 |
let (* both ^^^^^ ^^^^^^^^^^^^ are either empty or complete *)
|
Walther@60652
|
276 |
val (_, hdl, refs, pors, pctxt) = initialise thy (model, refs)
|
Walther@60651
|
277 |
val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt)
|
Walther@60651
|
278 |
(model, refs) (pors, refs, hdl, pctxt)
|
Walther@60651
|
279 |
in
|
Walther@60651
|
280 |
((pt, ([], Pbl)), (fst3 o snd) (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))
|
Walther@60651
|
281 |
end
|
Walther@60651
|
282 |
|
walther@59763
|
283 |
(**)end(**)
|