1 (* Title: Specify/step-specify.sml
2 Author: Walther Neuper 2019
3 (c) due to copyright terms
6 signature STEP_SPECIFY =
8 (*val do_next: Step.specify_do_next requires LI.by_tactic, which is not yet known in Step_Specify*)
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
12 val initialisePIDE: Formalise.T ->
13 term * term * References.T * O_Model.T * Proof.context
14 val nxt_specify_init_calc: Formalise.T -> Calc.T * State_Steps.T
15 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
17 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
22 structure Step_Specify(**): STEP_SPECIFY(**) =
29 fun by_tactic_input (tac as Tactic.Model_Problem) (pt, pos as (p, _)) =
31 val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
32 PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
33 | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
34 val (_, pI, mI) = References.select ospec spec
35 val mpc = (#ppc o Method.from_store) mI (* just for reuse I_Model.complete_method *)
36 val {cas, ppc, ...} = Problem.from_store pI
37 val pbl = I_Model.init ppc (* fill in descriptions *)
38 (*----------------if you think, this should be done by the Dialog
39 in the java front-end, search there for WN060225-modelProblem----*)
40 val (pbl, met) = case cas of
42 | _ => I_Model.complete_method (oris, mpc, ppc, probl)
43 (*----------------------------------------------------------------*)
44 val tac_ = Tactic.Model_Problem' (pI, pbl, met)
45 val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos)
47 ("ok",([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)))
49 | by_tactic_input (Tactic.Add_Given ct) ptp = Specify.by_Add_ "#Given" ct ptp
50 | by_tactic_input (Tactic.Add_Find ct) ptp = Specify.by_Add_ "#Find" ct ptp
51 | by_tactic_input (Tactic.Add_Relation ct) ptp = Specify.by_Add_"#Relate" ct ptp
53 (* called with Method.id_empty *)
54 | by_tactic_input (Tactic.Refine_Tacitly pI) (ptp as (pt, pos as (p, _))) =
56 val (oris, dI, ctxt) = case get_obj I pt p of
57 (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
58 | _ => raise ERROR "by_tactic_input Refine_Tacitly: uncovered case get_obj"
59 val opt = Refine.refine_ori oris pI
64 val {met, ...} = Problem.from_store pI'
65 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
66 val mI = if length met = 0 then Method.id_empty else hd met
68 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos)
70 ("ok", ([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
71 (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)))
73 | NONE => ("failure", ([], [], ptp))
75 | by_tactic_input (Tactic.Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
77 val (dI, dI', probl, ctxt) = case get_obj I pt p of
78 PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
79 (dI, dI', probl, ctxt)
80 | _ => raise ERROR "by_tactic_input Refine_Problem: uncovered case get_obj"
81 val thy = if dI' = ThyC.id_empty then dI else dI'
83 case Refine.problem (ThyC.get_theory thy) pI probl of
84 NONE => ("failure", ([], [], ptp))
87 val (pos,c,_,pt) = Specify_Step.add (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)
89 ("ok", ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd,
90 (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)))
93 | by_tactic_input (Tactic.Specify_Problem pI) (pt, pos as (p, _)) =
95 val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
96 PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
97 (oris, dI, dI', pI', probl, ctxt)
99 val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
100 val {ppc,where_,prls,...} = Problem.from_store pI
102 if pI' = Problem.id_empty andalso pI = Problem.id_empty
103 then (false, (I_Model.init ppc, []))
104 else M_Match.match_itms_oris thy probl (ppc,where_,prls) oris
105 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
107 case Specify_Step.add (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of
108 ((_, Pbl), c, _, pt) => (c, pt)
109 | _ => raise ERROR ""
111 ("ok", ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl),
112 (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos)))
114 | by_tactic_input (Tactic.Specify_Method id) (pt, pos) =
116 val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos)
117 val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, i_model))
118 (Istate_Def.Uistate, ctxt) (pt, pos)
120 ("ok", ([(Tactic.Specify_Method id, Tactic.Specify_Method' (id, o_model, i_model),
121 (pos, (Istate_Def.Uistate, ContextC.empty)))], [], (pt, pos)))
123 | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) =
125 val ctxt = get_ctxt pt pos
126 val (pos, c, _, pt) =
127 Specify_Step.add (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) (pt, pos)
128 in (*FIXXXME: check if pbl can still be parsed*)
129 ("ok", ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI,
130 (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos)))
132 | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Met)) =
134 val ctxt = get_ctxt pt pos
135 val (pos, c, _, pt) = Specify_Step.add (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) (pt, pos)
136 in (*FIXXXME: check if met can still be parsed*)
137 ("ok", ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI,
138 (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos)))
140 | by_tactic_input m' _ = raise ERROR ("by_tactic_input: not impl. for " ^ Tactic.input_to_string m')
144 fun by_tactic (Tactic.Model_Problem' (id, pbl, met)) (pt, pos) =
146 val ((p, _), _, _, pt) = Specify_Step.add (Tactic.Model_Problem'(id, pbl, met))
147 (Istate_Def.Uistate, ContextC.empty) (pt, pos)
148 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
150 ("ok", ([], [], (pt, (p, Pbl))))
152 (* called only if no_met is specified *)
153 | by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) =
155 val {met, thy,...} = Problem.from_store pIre
156 val (domID, metID) = (Context.theory_name thy, if length met = 0 then Method.id_empty else hd met)
157 val ((p,_), _, _, pt) =
158 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
159 (Istate_Def.Uistate, ContextC.empty) (pt, pos)
160 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
162 ("ok", ([], [], (pt,(p, Pbl))))
164 | by_tactic (Tactic.Refine_Problem' (rfd as (id, _))) (pt, pos) =
166 val ctxt = get_ctxt pt pos
167 val (pos, _, _, pt) =
168 Specify_Step.add (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)
170 ("ok", ([(Tactic.Refine_Problem id, Tactic.Refine_Problem' rfd,
171 (pos, (Istate_Def.Uistate,ctxt)))], [], (pt, pos)))
173 | by_tactic (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (pt, pos as (p, _)) =
175 val (_, _, _, _, _, _, ctxt, _) = case get_obj I pt p of
176 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>
177 (oris, dI', pI', mI', dI, mI, ctxt, met)
178 | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
180 case Specify_Step.add (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
181 ((p, Pbl), _, _, pt) => (p, pt)
182 | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
184 ("ok", ([], [], (pt, (p, Pbl))))
186 | by_tactic (Tactic.Specify_Method' (id, _, _)) (pt, pos) =
188 val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos)
189 val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, i_model))
190 (Istate_Def.Uistate, ctxt) (pt, pos)
192 ("ok", ([], [], (pt, pos)))
194 | by_tactic (Tactic.Add_Given' (ct, _)) (pt, p) = Specify.by_Add_ "#Given" ct (pt, p)
195 | by_tactic (Tactic.Add_Find' (ct, _)) (pt, p) = Specify.by_Add_ "#Find" ct (pt, p)
196 | by_tactic (Tactic.Add_Relation' (ct, _)) (pt, p) = Specify.by_Add_"#Relate" ct (pt, p)
197 (*strange old code, redes*)
198 | by_tactic (Tactic.Specify_Theory' domID) (pt, (p, p_)) =
200 val p_ = case p_ of Met => Met | _ => Pbl
201 val {spec = (dI, _, _), ctxt, ...} = Calc.specify_data (pt, (p, p_))
204 ("ok", ([], [], (pt, (p, p_))))
205 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
207 val ((p, p_), _, _, pt) = Specify_Step.add (Tactic.Specify_Theory' domID)
208 (Istate_Def.Uistate, ctxt) (pt, (p, p_))
210 ("ok", ([], [], (pt, (p, p_))))
213 | by_tactic _ _ = raise ERROR "Step_Specify.by_tactic uncovered pattern in fun.def"
215 (* create a calc-tree with oris via an cas.refined pbl *)
216 (* initialisePI <- nxt_specify_init_calc *)
217 fun initialisePIDE (fmz, (dI, pI, mI)) =
219 val thy = ThyC.get_theory dI
220 val (pI, (pors, pctxt), mI) =
224 val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy; (*..TermC.parseNEW'*)
225 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
226 val pI' = Refine.refine_ori' pors pI;
227 in (pI', (pors (*refinement over models with diff.precond only*), pctxt),
228 (hd o #met o Problem.from_store) pI')
232 val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy; (*..TermC.parseNEW'*)
233 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
234 in (pI, (pors, pctxt), mI) end;
235 val {cas, ppc, thy = thy', ...} = Problem.from_store pI (*take dI from _refined_ pbl*)
236 val dI = Context.theory_name (ThyC.sub_common (thy, thy'))
237 val hdl = case cas of
238 NONE => Auto_Prog.pblterm dI pI
239 | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t
240 val hdlPIDE = case cas of
241 NONE => Auto_Prog.pbltermPIDE dI pI
242 | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t
244 (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)
246 (* nxt_specify_init_calc \<rightarrow> initialise *)
247 fun nxt_specify_init_calc ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*)
249 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
251 val {cas, met, ppc, thy, ...} = Problem.from_store pI
252 val dI = if dI = "" then Context.theory_name thy else dI
253 val mI = if mI = [] then hd met else mI
254 val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
255 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
256 ([], (dI,pI,mI), hdl, ContextC.empty)
257 val pt = update_spec pt [] (dI, pI, mI)
258 val pits = I_Model.init ppc
259 val pt = update_pbl pt [] pits
260 in ((pt, ([] , Pbl)), []) end
263 then (* from met-browser *)
265 val {ppc, ...} = Method.from_store mI
266 val dI = if dI = "" then "Isac_Knowledge" else dI
267 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
268 ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty)
269 val pt = update_spec pt [] (dI, pI, mI)
270 val mits = I_Model.init ppc
271 val pt = update_met pt [] mits
272 in ((pt, ([], Met)), []) end
273 else (* new example, pepare for interactive modeling *)
275 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
276 ([], References.empty) ([], References.empty, TermC.empty, ContextC.empty)
277 in ((pt, ([], Pbl)), []) end
278 | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
279 let (* both ^^^ ^^^^^^^^^^^^ are either empty or complete *)
280 val (_, hdl, (dI, pI, mI), pors, pctxt) = initialisePIDE (fmz, (dI, pI, mI))
281 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt)
282 (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl, pctxt)
284 ((pt, ([], Pbl)), (fst3 o snd) (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))