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 initialise: theory -> Formalise.T ->
13 term * term * References.T * O_Model.T * Proof.context
14 val initialise': theory -> Formalise.T -> Calc.T * State_Steps.T
18 structure Step_Specify(**): STEP_SPECIFY(**) =
25 fun by_tactic_input (tac as Tactic.Model_Problem) (pt, pos as (p, _)) =
27 val (oris, ospec, probl, spec, ctxt, meth) = case get_obj I pt p of
28 PblObj {origin = (oris, ospec, _), probl, spec, ctxt, meth, ...} => (oris, ospec, probl, spec, ctxt, meth)
29 | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
30 val (_, pI, mI) = References.select_input ospec spec
31 val {cas, model, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
32 val pbl = I_Model.init ctxt oris model (* fill in descriptions *)
33 val (pbl, met) = case cas of
35 | _ => I_Model.s_make_complete ctxt oris (probl, meth) (pI, mI)
36 val tac_ = Tactic.Model_Problem' (pI, pbl, met)
37 val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos)
39 ("ok",([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)))
41 | by_tactic_input (Tactic.Add_Given ct) ptp = Specify.by_Add_ "#Given" ct ptp
42 | by_tactic_input (Tactic.Add_Find ct) ptp = Specify.by_Add_ "#Find" ct ptp
43 | by_tactic_input (Tactic.Add_Relation ct) ptp = Specify.by_Add_"#Relate" ct ptp
45 (* called with MethodC.id_empty *)
46 | by_tactic_input (Tactic.Refine_Tacitly pI) (ptp as (pt, pos as (p, _))) =
48 val (oris, dI, ctxt) = case get_obj I pt p of
49 (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
50 | _ => raise ERROR "by_tactic_input Refine_Tacitly: uncovered case get_obj"
51 val opt = Refine.by_o_model ctxt oris pI
56 val {solve_mets, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
57 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
58 val mI = if length solve_mets = 0 then MethodC.id_empty else hd solve_mets
60 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos)
62 ("ok", ([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
63 (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)))
65 | NONE => ("failure", ([], [], ptp))
67 | by_tactic_input (Tactic.Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
69 val (dI, dI', probl, ctxt) = case get_obj I pt p of
70 PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
71 (dI, dI', probl, ctxt)
72 | _ => raise ERROR "by_tactic_input Refine_Problem: uncovered case get_obj"
73 val thy = if dI' = ThyC.id_empty then dI else dI'
75 case Refine.problem (ThyC.get_theory ctxt thy) pI probl of
76 NONE => ("failure", ([], [], ptp))
77 | SOME (pI, (i_model, prec)) =>
79 val (pos,c,_,pt) = Specify_Step.add (Tactic.Refine_Problem' (pI, (i_model, prec)) )
80 (Istate_Def.Uistate, ctxt) (pt, pos)
82 ("ok", ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' (pI, (i_model, prec)),
83 (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos)))
86 | by_tactic_input (Tactic.Specify_Problem pI) (pt, pos as (p, _)) =
88 val (oris, pI', probl, meth, ctxt) = case get_obj I pt p of
89 PblObj {origin = (oris, _, _), spec = (_ ,pI',_), probl, meth, ctxt, ...} =>
90 (oris, pI', probl, meth, ctxt)
92 val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
93 val (check, (i_model, preconds)) =
94 if pI' = Problem.id_empty andalso pI = Problem.id_empty
95 then (false, (I_Model.init ctxt oris model, []))
96 else M_Match.by_i_models ctxt oris (probl, meth) (model, where_, where_rls)
98 case Specify_Step.add (Tactic.Specify_Problem' (pI, (check, (i_model, preconds)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
99 ((_, Pbl), c, _, pt) => (c, pt)
100 | _ => raise ERROR ""
102 ("ok", ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, (check, ( i_model, preconds))),
103 (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos)))
105 | by_tactic_input (Tactic.Specify_Method id) (pt, pos) =
107 val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos)
108 val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, i_model))
109 (Istate_Def.Uistate, ctxt) (pt, pos)
111 ("ok", ([(Tactic.Specify_Method id, Tactic.Specify_Method' (id, o_model, i_model),
112 (pos, (Istate_Def.Uistate, ContextC.empty)))], [], (pt, pos)))
114 | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) =
116 val ctxt = get_ctxt pt pos
117 val (pos, c, _, pt) =
118 Specify_Step.add (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) (pt, pos)
119 in (*FIXXXME: check if pbl can still be parsed*)
120 ("ok", ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI,
121 (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos)))
123 | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Met)) =
125 val ctxt = get_ctxt pt pos
126 val (pos, c, _, pt) = Specify_Step.add (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) (pt, pos)
127 in (*FIXXXME: check if met can still be parsed*)
128 ("ok", ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI,
129 (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos)))
131 | by_tactic_input m' (ctree, pos) =
133 val ctxt = Ctree.get_ctxt ctree pos
135 raise ERROR ("by_tactic_input: not impl. for " ^ Tactic.input_to_string ctxt m')
140 fun by_tactic (Tactic.Model_Problem' (id, pbl, met)) (pt, pos) =
142 val ((p, _), _, _, pt) = Specify_Step.add (Tactic.Model_Problem'(id, pbl, met))
143 (Istate_Def.Uistate, ContextC.empty) (pt, pos)
144 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
146 ("ok", ([], [], (pt, (p, Pbl))))
148 (* called only if no_met is specified *)
149 | by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) =
151 val {solve_mets, thy,...} = Problem.from_store (Ctree.get_ctxt pt pos) pIre
152 val (domID, metID) = (Context.theory_name thy,
153 if length solve_mets = 0 then MethodC.id_empty
155 val ((p,_), _, _, pt) =
156 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
157 (Istate_Def.Uistate, ContextC.empty) (pt, pos)
158 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
160 ("ok", ([], [], (pt,(p, Pbl))))
162 | by_tactic (Tactic.Refine_Problem' (rfd as (id, _))) (pt, pos) =
164 val ctxt = get_ctxt pt pos
165 val (pos, _, _, pt) =
166 Specify_Step.add (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)
168 ("ok", ([(Tactic.Refine_Problem id, Tactic.Refine_Problem' rfd,
169 (pos, (Istate_Def.Uistate,ctxt)))], [], (pt, pos)))
171 | by_tactic (Tactic.Specify_Problem' (pI, (ok, (itms, where_)))) (pt, pos as (p, _)) =
173 val (_, _, _, _, _, _, ctxt, _) = case get_obj I pt p of
174 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>
175 (oris, dI', pI', mI', dI, mI, ctxt, met)
176 | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
178 case Specify_Step.add (Tactic.Specify_Problem' (pI, (ok, (itms, where_)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
179 ((p, Pbl), _, _, pt) => (p, pt)
180 | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
182 ("ok", ([], [], (pt, (p, Pbl))))
184 | by_tactic (Tactic.Specify_Method' (id, _, _)) (pt, pos) =
186 val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos)
187 val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, i_model))
188 (Istate_Def.Uistate, ctxt) (pt, pos)
190 ("ok", ([], [], (pt, pos)))
192 | by_tactic (Tactic.Add_Given' (ct, _)) (pt, p) = Specify.by_Add_ "#Given" ct (pt, p)
193 | by_tactic (Tactic.Add_Find' (ct, _)) (pt, p) = Specify.by_Add_ "#Find" ct (pt, p)
194 | by_tactic (Tactic.Add_Relation' (ct, _)) (pt, p) = Specify.by_Add_"#Relate" ct (pt, p)
195 (*strange old code, redes*)
196 | by_tactic (Tactic.Specify_Theory' domID) (pt, (p, p_)) =
198 val p_ = case p_ of Met => Met | _ => Pbl
199 val {spec = (dI, _, _), ctxt, ...} = Calc.specify_data (pt, (p, p_))
202 ("ok", ([], [], (pt, (p, p_))))
203 else (*FIXME: check model wrt. (new!) domID ..? still parsable?*)
205 val ((p, p_), _, _, pt) = Specify_Step.add (Tactic.Specify_Theory' domID)
206 (Istate_Def.Uistate, ctxt) (pt, (p, p_))
208 ("ok", ([], [], (pt, (p, p_))))
211 | by_tactic _ _ = raise ERROR "Step_Specify.by_tactic uncovered pattern in fun.def"
213 (* create a calc-tree with oris via a cas.refined pbl *)
214 (* initialise <-?-> initialise' *)
215 fun initialise thy (fmz, (_, pI, mI)) =
217 val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise *)
218 val (pI, (pors, pctxt), mI) =
222 val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
223 val pI' = Refine.by_o_model' pctxt pors pI;
224 in (pI', (pors (*refinement over models with diff.precond only*), pctxt),
225 (hd o #solve_mets o Problem.from_store ctxt) pI')
229 val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
230 in (pI, (pors, pctxt), mI) end;
231 val {cas, model, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*)
232 val dI = Context.theory_name (Sub_Problem.common_sub_thy (thy, thy'))
233 val hdl = case cas of
234 NONE => Auto_Prog.pblterm dI pI
235 | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t
236 val hdlPIDE = case cas of
237 NONE => Auto_Prog.pblterm dI pI
238 | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t
240 (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)
242 (*TODO: HOW RELATES initialise' \<longleftrightarrow> initialise *)
243 fun initialise' thy ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*)
245 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
247 val {cas, solve_mets, model, thy, ...} = Problem.from_store (Proof_Context.init_global thy) pI
248 val dI = if dI = "" then Context.theory_name thy else dI
249 val mI = if mI = [] then hd solve_mets else mI
250 val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
251 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
252 ([], (dI,pI,mI), hdl, ContextC.empty)
253 val pt = update_spec pt [] (dI, pI, mI)
254 val pits = I_Model.init (Proof_Context.init_global thy) [(*o_model*)] model
255 val pt = update_pbl pt [] pits
256 in ((pt, ([] , Pbl)), []) end
259 then (* from met-browser *)
261 val {model, ...} = MethodC.from_store (Proof_Context.init_global thy) mI
262 val dI = if dI = "" then "Isac_Knowledge" else dI
263 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
264 ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty)
265 val pt = update_spec pt [] (dI, pI, mI)
266 val mits = I_Model.init (Proof_Context.init_global thy) [(*o_model*)] model
267 val pt = update_met pt [] mits
268 in ((pt, ([], Met)), []) end
269 else (* new example, pepare for interactive modeling *)
271 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
272 ([], References.empty) ([], References.empty, TermC.empty, ContextC.empty)
273 in ((pt, ([], Pbl)), []) end
274 | initialise' thy (model, refs) =
275 let (* both ^^^^^ ^^^^^^^^^^^^ are either empty or complete *)
276 val (_, hdl, refs, pors, pctxt) = initialise thy (model, refs)
277 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt)
278 (model, refs) (pors, refs, hdl, pctxt)
280 ((pt, ([], Pbl)), (fst3 o snd) (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))