Walther@60760
|
1 |
(* Title: Specify/specify.sml
|
Walther@60760
|
2 |
Author: Walther Neuper
|
Walther@60760
|
3 |
*)
|
walther@59984
|
4 |
signature SPECIFY =
|
walther@59763
|
5 |
sig
|
walther@59775
|
6 |
val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input)
|
walther@59990
|
7 |
val do_all: Calc.T -> Calc.T
|
walther@59990
|
8 |
val finish_phase: Calc.T -> Calc.T
|
walther@59990
|
9 |
|
Walther@60782
|
10 |
val item_to_add: Proof.context -> O_Model.T -> I_Model.T ->
|
Walther@60763
|
11 |
(Model_Def.m_field * TermC.as_string) option
|
walther@60016
|
12 |
val by_Add_: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
|
Walther@60768
|
13 |
|
Walther@60578
|
14 |
(*from isac_test for Minisubpbl*)
|
Walther@60782
|
15 |
val for_problem: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T ->
|
Walther@60763
|
16 |
string * (Pos.pos_ * Tactic.input)
|
Walther@60782
|
17 |
val for_method: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T ->
|
walther@60019
|
18 |
string * (Pos.pos_ * Tactic.input)
|
Walther@60782
|
19 |
val select_inc_lists: I_Model.T -> I_Model.T
|
Walther@60578
|
20 |
|
Walther@60578
|
21 |
\<^isac_test>\<open>
|
Walther@60578
|
22 |
(**)
|
wenzelm@60223
|
23 |
\<close>
|
walther@59763
|
24 |
end
|
walther@59763
|
25 |
|
walther@59763
|
26 |
(**)
|
walther@59984
|
27 |
structure Specify(**): SPECIFY(**) =
|
walther@59763
|
28 |
struct
|
walther@59763
|
29 |
(**)
|
walther@59763
|
30 |
|
Walther@60763
|
31 |
fun select_inc_lists i_model =
|
Walther@60763
|
32 |
let
|
Walther@60770
|
33 |
(* filter problem like with Const ("Input_Descript.solutions", _) *)
|
Walther@60782
|
34 |
val filt = (fn (_, _, _, _, (I_Model.Inc (descr, _::_) , _)) => Model_Def.is_list_descr descr
|
Walther@60763
|
35 |
| _ => false)
|
Walther@60763
|
36 |
in
|
Walther@60763
|
37 |
(filter filt i_model) @ (filter_out filt i_model)
|
Walther@60763
|
38 |
end
|
Walther@60766
|
39 |
|
Walther@60763
|
40 |
fun item_to_add ctxt o_model i_model =
|
Walther@60763
|
41 |
let
|
Walther@60763
|
42 |
val max_vnt = last_elem (*this decides, for which variant initially help is given*)
|
Walther@60763
|
43 |
(Model_Def.max_variants o_model i_model)
|
Walther@60763
|
44 |
val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
|
Walther@60763
|
45 |
val i_to_select = i_model
|
Walther@60782
|
46 |
|> filter_out (fn (_, vnts, _, _, (I_Model.Cor _, _)) => member op= vnts max_vnt | _ => false)
|
Walther@60763
|
47 |
|> select_inc_lists
|
Walther@60763
|
48 |
in
|
Walther@60763
|
49 |
if i_to_select = [] then NONE
|
Walther@60763
|
50 |
else
|
Walther@60763
|
51 |
case I_Model.fill_from_o o_vnts (hd i_to_select) of
|
Walther@60763
|
52 |
SOME (_, _, _, m_field, (feedb, _)) =>
|
Walther@60763
|
53 |
SOME (m_field, feedb |> I_Model.feedb_args_to_string ctxt)
|
Walther@60763
|
54 |
| NONE => raise ERROR "item_to_add: NONE not.impl."
|
Walther@60763
|
55 |
end
|
walther@60002
|
56 |
|
walther@60019
|
57 |
|
walther@60019
|
58 |
(** find a next step in the specify-phase **)
|
walther@60021
|
59 |
(*
|
Walther@60575
|
60 |
here should be mutual recursion between for_problem ctxt and for_method
|
walther@60021
|
61 |
*)
|
Walther@60575
|
62 |
fun for_problem ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =
|
walther@59763
|
63 |
let
|
walther@60019
|
64 |
val cpI = if pI = Problem.id_empty then pI' else pI;
|
walther@60154
|
65 |
val cmI = if mI = MethodC.id_empty then mI' else mI;
|
Walther@60585
|
66 |
val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
|
Walther@60586
|
67 |
val {model = mpc, ...} = MethodC.from_store ctxt cmI
|
Walther@60776
|
68 |
val (preok, _) = Pre_Conds.check ctxt where_rls where_ (pbt, pbl);
|
walther@60019
|
69 |
in
|
walther@60021
|
70 |
if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then
|
walther@60019
|
71 |
("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
|
walther@60019
|
72 |
else if pI' = Problem.id_empty andalso pI = Problem.id_empty then
|
walther@60019
|
73 |
("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
|
walther@60019
|
74 |
else
|
Walther@60776
|
75 |
case find_first (fn (_, _, _, _, (feedb, _)) => I_Model.is_error feedb) pbl of
|
Walther@60776
|
76 |
SOME (_, _, _, fd, (itm_, _)) =>
|
Walther@60676
|
77 |
("dummy", (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory ctxt
|
walther@60019
|
78 |
(if dI = ThyC.id_empty then dI' else dI)) fd itm_))
|
walther@60019
|
79 |
| NONE =>
|
Walther@60776
|
80 |
(case item_to_add ctxt oris pbl of
|
walther@60019
|
81 |
SOME (fd, ct') => ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct'))
|
walther@60019
|
82 |
| NONE => (*pbl-items complete*)
|
walther@60019
|
83 |
if not preok then ("dummy", (Pos.Pbl, Tactic.Refine_Problem pI'))
|
Walther@60726
|
84 |
(*this is an ERROR fall through ------^^^^^^^^^^^^^^^^^^^^^ for Pre_Conds, redesign ?*)
|
walther@60019
|
85 |
else if dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
|
walther@60019
|
86 |
else if pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
|
walther@60154
|
87 |
else if mI = MethodC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Method mI'))
|
walther@60019
|
88 |
else
|
Walther@60776
|
89 |
case find_first (fn (_, _, _, _, (feedb, _)) => I_Model.is_error feedb) met of
|
Walther@60776
|
90 |
SOME (_, _, _, fd, (itm_, _)) =>
|
Walther@60676
|
91 |
("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory ctxt dI) fd itm_))
|
walther@60019
|
92 |
| NONE =>
|
Walther@60763
|
93 |
(case item_to_add ctxt oris met of
|
walther@60019
|
94 |
SOME (fd, ct') =>
|
Walther@60776
|
95 |
("dummy", (Pos.Met, P_Model.mk_additem fd ct'))
|
walther@60021
|
96 |
| NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI))))
|
walther@60019
|
97 |
end
|
walther@60019
|
98 |
|
Walther@60706
|
99 |
fun for_method ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (_, met) =
|
walther@60019
|
100 |
let
|
walther@60154
|
101 |
val cmI = if mI = MethodC.id_empty then mI' else mI;
|
Walther@60586
|
102 |
val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;
|
Walther@60776
|
103 |
val (preok, _) = Pre_Conds.check ctxt where_rls where_ (mpc, met);
|
walther@60019
|
104 |
in
|
Walther@60776
|
105 |
(case find_first (fn (_, _, _, _, (feedb, _)) => I_Model.is_error feedb) met of
|
Walther@60776
|
106 |
SOME (_,_,_, fd, (itm_, _)) =>
|
Walther@60676
|
107 |
("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory ctxt
|
Walther@60578
|
108 |
(if dI = ThyC.id_empty then dI' else dI)) fd itm_))
|
walther@60019
|
109 |
| NONE =>
|
Walther@60776
|
110 |
case item_to_add ctxt oris met of
|
walther@60019
|
111 |
SOME (fd, ct') =>
|
Walther@60763
|
112 |
("dummy", (Pos.Met, P_Model.mk_additem fd ct'))
|
walther@60019
|
113 |
| NONE =>
|
walther@60019
|
114 |
(if dI = ThyC.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Theory dI'))
|
walther@60019
|
115 |
else if pI = Problem.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Problem pI'))
|
walther@60019
|
116 |
else if not preok then ("dummy", (Pos.Met, Tactic.Specify_Method mI))
|
walther@60019
|
117 |
else ("dummy", (Pos.Met, Tactic.Apply_Method mI))))
|
walther@60019
|
118 |
end
|
walther@60019
|
119 |
|
walther@60019
|
120 |
(*
|
walther@60019
|
121 |
on finding a next step switching from problem to method or vice versa is possible,
|
walther@60019
|
122 |
because the user is free to switch and edit the respective models independently.
|
walther@60019
|
123 |
TODO: this free switch is NOT yet implemented; e.g.
|
Walther@60575
|
124 |
preok is relevant for problem + method, i.e. in for_problem ctxt + for_method
|
walther@60019
|
125 |
*)
|
walther@60019
|
126 |
fun find_next_step (pt, pos as (_, p_)) =
|
walther@60019
|
127 |
let
|
walther@60019
|
128 |
val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
|
walther@60019
|
129 |
spec = refs, ...} = Calc.specify_data (pt, pos);
|
Walther@60556
|
130 |
val ctxt = Ctree.get_ctxt pt pos
|
Walther@60766
|
131 |
in
|
Walther@60766
|
132 |
if Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin then
|
Walther@60766
|
133 |
case mI' of
|
Walther@60766
|
134 |
["no_met"] => ("ok", (Pos.Pbl, Tactic.Refine_Tacitly pI'))
|
Walther@60766
|
135 |
| _ => ("ok", (Pos.Pbl, Tactic.Model_Problem))
|
Walther@60766
|
136 |
else if p_ = Pos.Pbl then
|
Walther@60779
|
137 |
for_problem ctxt oris (o_refs, refs) (pbl, met)
|
Walther@60766
|
138 |
else
|
Walther@60779
|
139 |
for_method ctxt oris (o_refs, refs) (pbl, met)
|
Walther@60766
|
140 |
end
|
walther@60019
|
141 |
|
walther@60019
|
142 |
|
walther@60021
|
143 |
(** tools **)
|
walther@59763
|
144 |
|
Walther@60556
|
145 |
fun by_Add_ m_field ct (pt, pos as (_, p_)) =
|
walther@60016
|
146 |
let
|
walther@60097
|
147 |
val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
|
walther@60016
|
148 |
val (i_model, m_patt) =
|
walther@60016
|
149 |
if p_ = Pos.Met then
|
walther@60016
|
150 |
(met,
|
Walther@60586
|
151 |
(if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
|
walther@60016
|
152 |
else
|
walther@60016
|
153 |
(pbl,
|
Walther@60585
|
154 |
(if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
|
walther@60016
|
155 |
in
|
Walther@60778
|
156 |
case I_Model.check_single ctxt m_field oris i_model m_patt ct of
|
walther@60016
|
157 |
I_Model.Add i_single => (*..union old input *)
|
walther@60016
|
158 |
let
|
Walther@60773
|
159 |
val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model
|
Walther@60774
|
160 |
val tac' = I_Model.make_tactic m_field (ct, i_model')
|
walther@60016
|
161 |
val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
|
walther@60016
|
162 |
in
|
Walther@60611
|
163 |
("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],
|
walther@60021
|
164 |
[], (pt', pos)))
|
walther@60016
|
165 |
end
|
walther@60016
|
166 |
| I_Model.Err msg => (msg, ([], [], (pt, pos)))
|
walther@60016
|
167 |
end
|
walther@59990
|
168 |
|
walther@59990
|
169 |
(* complete _NON_empty calc-head for autocalc (sub-)pbl from oris
|
walther@59990
|
170 |
+ met from fmz; assumes pos on PblObj, meth = [] *)
|
walther@59990
|
171 |
fun finish_phase (pt, pos as (p, p_)) =
|
walther@59990
|
172 |
let
|
walther@59990
|
173 |
val _ = if p_ <> Pos.Pbl
|
walther@59990
|
174 |
then raise ERROR ("###finish_phase: only impl.for Pbl, called with " ^ Pos.pos'2str pos)
|
walther@59990
|
175 |
else ()
|
Walther@60752
|
176 |
val (oris, ospec, probl, spec, meth) = case Ctree.get_obj I pt p of
|
Walther@60752
|
177 |
Ctree.PblObj {origin = (oris, ospec, _), probl, spec, meth, ...} => (oris, ospec, probl, spec, meth)
|
walther@59990
|
178 |
| _ => raise ERROR "finish_phase: unvered case get_obj"
|
Walther@60494
|
179 |
val (_, pI, mI) = References.select_input ospec spec
|
Walther@60556
|
180 |
val ctxt = Ctree.get_ctxt pt pos
|
Walther@60779
|
181 |
val (pits, mits) = I_Model.s_make_complete ctxt oris (probl, meth) (pI, mI)
|
Walther@60779
|
182 |
val pt = Ctree.update_pblppc pt p pits
|
Walther@60779
|
183 |
val pt = Ctree.update_metppc pt p mits
|
walther@59990
|
184 |
in (pt, (p, Pos.Met)) end
|
Walther@60556
|
185 |
|
Walther@60654
|
186 |
(*
|
Walther@60654
|
187 |
do all specification in one single step:
|
Walther@60746
|
188 |
bypass input of Problem.model and go immediately for MethodC: I_Model.complete'
|
walther@59990
|
189 |
*)
|
Walther@60755
|
190 |
fun do_all (pt, (p, _)) =
|
walther@59990
|
191 |
let
|
Walther@60755
|
192 |
val (itms, oris, probl, o_refs, spec, ctxt) = case Ctree.get_obj I pt p of
|
Walther@60755
|
193 |
Ctree.PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}
|
Walther@60755
|
194 |
=> (itms, oris, probl, o_spec, spec, ctxt)
|
Walther@60757
|
195 |
| _ => raise ERROR "Specify.do_all: no PblObj"
|
Walther@60755
|
196 |
val (_, pbl_id', met_id') = References.select_input o_refs spec
|
Walther@60779
|
197 |
val (pbl_imod, met_imod) = I_Model.s_make_complete ctxt oris (probl, itms) (pbl_id', met_id')
|
Walther@60779
|
198 |
val (pt, _) = Ctree.cupdate_problem pt p (o_refs, pbl_imod, met_imod, ctxt)
|
walther@59990
|
199 |
in
|
walther@59990
|
200 |
(pt, (p, Pos.Met))
|
walther@59990
|
201 |
end
|
walther@59990
|
202 |
|
walther@59946
|
203 |
(**)end(**)
|