prep. remove Specify/mstools.sml
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 -> Chead.calcstate'
10 val by_tactic: Tactic.T -> Calc.T -> string * Chead.calcstate'
11 (* ---- keep, probably required later in devel. ----------------------------------------------- *)
12 val nxt_specify_init_calc: Formalise.T -> Calc.T * State_Steps.T
13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
14 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
19 structure Step_Specify(**): STEP_SPECIFY(**) =
26 (* was fun Math_Engine.nxt_specify_ *)
27 fun by_tactic_input (tac as Tactic.Model_Problem) (pt, pos as (p, _)) =
29 val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
30 PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
31 | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
32 val (dI, pI, mI) = some_spec ospec spec
33 val thy = ThyC.get_theory dI
34 val mpc = (#ppc o Specify.get_met) mI (* just for reuse complete_mod_ *)
35 val {cas, ppc, ...} = Specify.get_pbt pI
36 val pbl = I_Model.init ppc (* fill in descriptions *)
37 (*----------------if you think, this should be done by the Dialog
38 in the java front-end, search there for WN060225-modelProblem----*)
39 val (pbl, met) = case cas of
41 | _ => complete_mod_ (oris, mpc, ppc, probl)
42 (*----------------------------------------------------------------*)
43 val tac_ = Tactic.Model_Problem' (pI, pbl, met)
44 val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos)
45 in ([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)) end
46 | by_tactic_input (Tactic.Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
47 | by_tactic_input (Tactic.Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
48 | by_tactic_input (Tactic.Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
49 (*. called only if no_met is specified .*)
50 | by_tactic_input (Tactic.Refine_Tacitly pI) (ptp as (pt, pos as (p, _))) =
52 val (oris, dI, ctxt) = case get_obj I pt p of
53 (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
54 | _ => raise ERROR "by_tactic_input Refine_Tacitly: uncovered case get_obj"
55 val opt = Specify.refine_ori oris pI
60 val {met, ...} = Specify.get_pbt pI'
61 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
62 val mI = if length met = 0 then Method.id_empty else hd met
63 val thy = ThyC.get_theory dI
65 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos)
67 ([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
68 (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos))
70 | NONE => ([], [], ptp)
72 | by_tactic_input (Tactic.Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
74 val (dI, dI', probl, ctxt) = case get_obj I pt p of
75 PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
76 (dI, dI', probl, ctxt)
77 | _ => raise ERROR "by_tactic_input Refine_Problem: uncovered case get_obj"
78 val thy = if dI' = ThyC.id_empty then dI else dI'
80 case Refine.problem (ThyC.get_theory thy) pI probl of
84 val (pos,c,_,pt) = Specify_Step.add (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)
86 ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos))
89 | by_tactic_input (Tactic.Specify_Problem pI) (pt, pos as (p,_)) =
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, ...} =>
93 (oris, dI, dI', pI', probl, ctxt)
95 val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
96 val {ppc,where_,prls,...} = Specify.get_pbt pI
98 if pI' = Problem.id_empty andalso pI = Problem.id_empty
99 then (false, (I_Model.init ppc, []))
100 else Specify.match_itms_oris thy probl (ppc,where_,prls) oris
101 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
103 case Specify_Step.add (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of
104 ((_, Pbl), c, _, pt) => (c, pt)
105 | _ => raise ERROR ""
107 ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl), (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos))
109 (* transfers oris (not required in pbl) to met-model for script-env
110 FIXME.WN.8.03: application of several mIDs to SAME model? *)
111 | by_tactic_input (Tactic.Specify_Method mID) (pt, pos as (p,_)) =
113 val (oris, pbl, dI, met, ctxt) = case get_obj I pt p of
114 PblObj {origin = (oris, _, _), probl = pbl, spec = (dI, _, _), meth=met, ctxt, ...}
115 => (oris, pbl, dI, met, ctxt)
116 | _ => raise ERROR "by_tactic_input Specify_Method: uncovered case get_obj"
117 val {ppc,pre,prls,...} = Specify.get_met mID
118 val thy = ThyC.get_theory dI
119 val oris = O_Model.add thy ppc oris
120 val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
121 val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris
122 val itms = Specify.hack_until_review_Specify_2 mID itms
123 val (pos, c, _, pt) =
124 Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)
126 ([(Tactic.Specify_Method mID, Tactic.Specify_Method' (mID, oris, itms), (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos))
128 | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) =
130 val ctxt = get_ctxt pt pos
131 val (pos, c, _, pt) =
132 Specify_Step.add (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) (pt, pos)
133 in (*FIXXXME: check if pbl can still be parsed*)
134 ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate_Def.Uistate, ctxt)))], c,
137 | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Met)) =
139 val ctxt = get_ctxt pt pos
140 val (pos, c, _, pt) = Specify_Step.add (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) (pt, pos)
141 in (*FIXXXME: check if met can still be parsed*)
142 ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos))
144 | by_tactic_input m' _ = raise ERROR ("by_tactic_input: not impl. for " ^ Tactic.input_to_string m')
145 (* was fun Math_Engine.nxt_specify_ *)
148 (* was fun Chead.specify *)
149 fun by_tactic (Tactic.Model_Problem' (_, pbl, met)) (pt, pos as (p, _)) =
151 val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of
152 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} =>
153 (oris, dI',pI',mI', dI, ctxt)
154 | _ => raise ERROR "Step_Solve.by_tactic (Model_Problem': uncovered case get_obj"
155 val thy' = if dI = ThyC.id_empty then dI' else dI
156 val thy = ThyC.get_theory thy'
157 val {ppc, prls, where_, ...} = Specify.get_pbt pI'
158 val pre = Pre_Conds.check' thy prls where_ pbl
159 val pb = foldl and_ (true, map fst pre)
160 val ((p, _), _, _, pt) =
161 Specify_Step.add (Tactic.Model_Problem'([],pbl,met)) (Istate_Def.Uistate, ctxt) (pt, pos)
162 val (_, _) = Chead.nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
163 (ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI');
165 ("ok", ([], [], (pt, (p, Pbl))))
167 (* called only if no_met is specified *)
168 | by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) =
170 (* val (dI', ctxt) = case get_obj I pt p of
171 PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)
172 | _ => raise ERROR "Step_Solve.by_tactic (Refine_Tacitly': uncovered case get_obj"*)
173 val {met, thy,...} = Specify.get_pbt pIre
174 val (domID, metID) = (Context.theory_name thy, if length met = 0 then Method.id_empty else hd met)
175 val ((p,_), _, _, pt) =
176 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
177 (Istate_Def.Uistate, ContextC.empty) (pt, pos)
178 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
179 (* val (pbl, pre, _) = ([], [], false)*)
181 ("ok", ([], [], (pt,(p, Pbl))))
183 | by_tactic (Tactic.Refine_Problem' rfd) (pt, pos) =
185 val ctxt = get_ctxt pt pos
186 val (pos, _, _, pt) =
187 Specify_Step.add (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)
189 ("ok", ([], [], (pt,pos)))
191 (*WN110515 initialise ctxt again from itms and add preconds*)
192 | by_tactic (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (pt, pos as (p, _)) =
194 val (_, _, _, _, dI, _, ctxt, _) = case get_obj I pt p of
195 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>
196 (oris, dI', pI', mI', dI, mI, ctxt, met)
197 | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
198 val thy = ThyC.get_theory dI
200 case Specify_Step.add (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
201 ((p, Pbl), _, _, pt) => (p, pt)
202 | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
204 ("ok", ([], [], (pt, (p, Pbl))))
206 (*WN110515 initialise ctxt again from itms and add preconds*)
207 | by_tactic (Tactic.Specify_Method' (mID, _, _)) (pt,pos as (p, _)) =
209 val (oris, _, _, mI', dI, _, pbl, met, ctxt) = case get_obj I pt p of
210 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
211 (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
212 | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
213 val {ppc, pre, prls,...} = Specify.get_met mID
214 val thy = ThyC.get_theory dI
215 val oris = O_Model.add thy ppc oris
216 val met = if met = [] then pbl else met
217 val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc, pre, prls) oris
218 val itms = Specify.hack_until_review_Specify_1 mI' itms
219 val (pos, _, _, pt) =
220 Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)
222 ("ok", ([], [], (pt, pos)))
224 | by_tactic (Tactic.Add_Given' (ct, _)) (pt, p) = Chead.specify_additem "#Given" ct (pt, p)
225 | by_tactic (Tactic.Add_Find' (ct, _)) (pt, p) = Chead.specify_additem "#Find" ct (pt, p)
226 | by_tactic (Tactic.Add_Relation' (ct, _)) (pt, p) = Chead.specify_additem"#Relate" ct (pt, p)
227 | by_tactic (Tactic.Specify_Theory' domID) (pt, (p,p_)) =
229 val p_ = case p_ of Met => Met | _ => Pbl
230 val thy = ThyC.get_theory domID
231 val (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt) = case get_obj I pt p of
232 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, mI), probl = pbl, meth = met, ctxt, ...} =>
233 (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt)
234 | _ => raise ERROR "Step_Solve.by_tactic (Specify_Theory': uncovered case get_obj"
235 val _ = case p_ of Met => met | _ => pbl
236 val cpI = if pI = Problem.id_empty then pI' else pI
237 val {prls = per, ppc, where_ = pwh, ...} = Specify.get_pbt cpI
238 val cmI = if mI = Method.id_empty then mI' else mI
239 val {prls = mer, ppc = mpc, pre= mwh, ...} = Specify.get_met cmI
241 Met => (Pre_Conds.check' thy mer mwh met)
242 | _ => (Pre_Conds.check' thy per pwh pbl)
243 val pb = foldl and_ (true, map fst pre)
247 let val (p_, _) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
249 ("ok", ([], [], (pt, (p, p_))))
251 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
253 val ((p, p_), _, _, pt) = Specify_Step.add (Tactic.Specify_Theory' domID) (Istate_Def.Uistate, ctxt) (pt, (p,p_))
254 val (p_, _) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
256 ("ok", ([], [], (pt, (p, p_))))
259 | by_tactic _ _ = raise ERROR "Step_Specify.by_tactic uncovered pattern in fun.def"
260 (* was fun Chead.specify *)
262 (* create a calc-tree with oris via an cas.refined pbl *)
263 fun nxt_specify_init_calc ([], (dI, pI, mI)) =
265 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
267 val {cas, met, ppc, thy, ...} = Specify.get_pbt pI
268 val dI = if dI = "" then Context.theory_name thy else dI
269 val mI = if mI = [] then hd met else mI
270 val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
271 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
272 ([], (dI,pI,mI), hdl, ContextC.empty)
273 val pt = update_spec pt [] (dI, pI, mI)
274 val pits = I_Model.init ppc
275 val pt = update_pbl pt [] pits
276 in ((pt, ([] , Pbl)), []) end
279 then (* from met-browser *)
281 val {ppc, ...} = Specify.get_met mI
282 val dI = if dI = "" then "Isac_Knowledge" else dI
283 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
284 ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty)
285 val pt = update_spec pt [] (dI, pI, mI)
286 val mits = I_Model.init ppc
287 val pt = update_met pt [] mits
288 in ((pt, ([], Met)), []) end
289 else (* new example, pepare for interactive modeling *)
291 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
292 ([], Spec.empty) ([], Spec.empty, TermC.empty, ContextC.empty)
293 in ((pt, ([], Pbl)), []) end
294 | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
295 let (* both """"""""""""""""""""""""" either empty or complete *)
296 val thy = ThyC.get_theory dI
297 val (pI, (pors, pctxt), mI) =
301 val (pors(*, pctxt*)) = Specify.get_pbt pI |> #ppc |> O_Model.init fmz thy;
302 val pctxt = ContextC.initialise' thy fmz;
303 val pI' = Specify.refine_ori' pors pI;
304 in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
305 (hd o #met o Specify.get_pbt) pI')
309 val pors = Specify.get_pbt pI |> #ppc |> O_Model.init fmz thy;
310 val pctxt = ContextC.initialise' thy fmz;
311 in (pI, (pors, pctxt), mI) end;
312 val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)
313 val dI = Context.theory_name (ThyC.sub_common (thy, thy'))
314 val hdl = case cas of
315 NONE => Auto_Prog.pblterm dI pI
316 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
317 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt)
318 (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl, pctxt)
320 ((pt, ([], Pbl)), fst3 (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))