1 (* Title: Specify/pre-conds.sml
2 Author: Walther Neuper 110226
3 (c) due to copyrigh,t terms
6 signature PRE_CONDITIONS =
18 val to_string : Proof.context -> T -> string
19 val eval: Proof.context -> Rule_Set.T -> bool * term -> bool * term
21 val max_variant: Model_Def.i_model -> Model_Def.variant
22 val environment_TEST: Model_Pattern.T -> Model_Def.i_model_TEST -> Env.T
24 (*TODO: replace in pre-conditions.m, see fun max_variants + make_envs_preconds,
25 see i-model.sml (** complete I_Model.T **) *)
26 val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
27 (bool * Model_Def.variant * Model_Def.i_model_TEST) * Env.T * (env_subst * env_eval)
28 val make_envs_preconds: (Model_Pattern.single * Model_Def.i_model_single_TEST) list ->
29 ((term * term) * (term * term)) list
31 val check_pos: Proof.context -> Rule_Set.T -> unchecked_pos ->
32 Model_Pattern.T * Model_Def.i_model_TEST -> checked_pos
33 val check_envs: Proof.context -> Rule_Set.T -> unchecked -> Env.T * (env_subst * env_eval)
35 val check: Proof.context -> Rule_Set.T -> unchecked ->
36 Model_Pattern.T * Model_Def.i_model_TEST -> checked
38 (*from isac_test for Minisubpbl*)
39 val get_equal_descr: Model_Def.i_model_TEST -> Model_Pattern.single ->
40 (Model_Pattern.single * Model_Def.i_model_single_TEST) list
41 val unchecked_OLD_to_TEST: term list -> (term * Position.T) list
43 val all_lhs_atoms: term list -> bool
44 val handle_lists: term -> Model_Def.descriptor * term list -> Env.T;
45 val filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST
46 val switch_type: Model_Def.descriptor -> term list -> Model_Def.descriptor;
47 val discern_feedback: term -> Model_Def.i_model_feedback_TEST ->
48 ((term * term) * (term * term)) list
49 val discern_typ: term -> Model_Pattern.descriptor * term list ->
50 ((term * term) * (term * term)) list
52 val mk_env_model: term -> Model_Def.i_model_feedback_TEST -> Env.T
53 val make_env_model: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> Env.T
55 val get_descr: Model_Def.i_model_single_TEST -> Model_Def.descriptor option;
56 val get_dscr': Model_Def.i_model_feedback_TEST -> Model_Def.descriptor option
57 val get_descr_vnt: Model_Def.descriptor -> Model_Def.variants -> Model_Def.i_model_TEST ->
58 Model_Def.i_model_single_TEST
59 val get_descr_vnt': Model_Def.i_model_feedback_TEST -> Model_Def.variants -> O_Model.T ->
68 structure Pre_Conds(**) : PRE_CONDITIONS(**) =
73 type T = Pre_Conds_Def.T; (*= (bool * term) list;*)
74 type unchecked = term list
75 type unchecked_pos = (term * Position.T) list
76 type checked = bool * (bool * term) list
77 type checked_pos = bool * ((bool * (term * Position.T)) list)
80 we have three kinds of Env.T in the specification-phase:
81 (*1*) Env.T produced by I_Model.of_max_variant and required to create O_Model.T, I_Model.T from
83 Env.T / (Constants, fixes) in Model_Pattern.T
84 e.g.[(fixes, [r = 7])] |
85 > (Constants, [<r = 7>]) in O/I_Model.T *)
87 (*2*) type env_subst = Env.T (* / 0 < fixes in Problem.{where_, ...}
90 (*3*) type env_eval = Env.T (* |
92 > 0 < 7 \<longrightarrow> true
94 (*1*) is required to produce (*2*) and (*3*); thus respective code is shifted to Pre_Conds.
95 (*2*) and (*3*) is produced from I_Model.of_max_variant by restricting to "#Given".
97 There is a typing problem, probably to be solved by a language for Specification in the future:
98 term <fixes> in (*1*) has type "bool list"
99 term <fixes> in (*2*) has type "real". So for the transition from (*1*) to (*2..3*)
100 fun switch_type is required.
101 The transition requires better modelling by a novel language for Specification.
104 type input = TermC.as_string list;
108 fun to_str ctxt (b, t) = pair2str (bool2str b, UnparseC.term ctxt t);
109 fun to_string ctxt pres = strs2str' (map (linefeed o (to_str ctxt)) pres);
111 fun eval _ _ (false, where_) = (false, where_) (*NOT ALL Free's have been substituted*)
112 | eval ctxt where_rls (true, where_) =
113 if Rewrite.eval_true ctxt [where_] where_rls
115 else (false, where_);
118 (** find the maximal variant within an I_Model.T **)
120 (* old code before I_Model.T_TEST *)
121 (*ATTENTION: misses variants with equal number of items, etc*)
122 fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms);
123 fun count_variants vts itms = map (cnt itms) vts;
125 fun max_list [] = raise ERROR "max_list of []"
126 | max_list (y :: ys) =
128 fun mx (a, x) [] = (a, x)
129 | mx (a, x) ((b, y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
132 (*find most frequent variant v in itms*)
133 fun variants itms = ((distinct op =) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms;
134 (*find the variant with most items already input, without Pre_Conds (of_max_variant)*)
135 (*T_TESTold \<rightarrow> fun max_variants*)
136 fun max_variant itms =
137 let val vts = (count_variants (variants itms)) itms;
138 in if vts = [] then 0 else (fst o max_list) vts end;
141 (* new code with I_Model.T_TEST proper handling variants *)
143 (*get descriptor of those items which can contribute to Subst.T and Env.T*)
144 (* get_dscr: feedback_TEST -> descriptor option*)
145 fun get_dscr' (Cor_TEST (descr, _)) = SOME descr
146 | get_dscr' (Inc_TEST (descr, _)) = SOME descr
147 | get_dscr' (Sup_TEST (descr, _)) = SOME descr
149 (*other feedback cannot contribute to I_Model.mk_env_TEST and Pre_Conds.mk_env_TEST*)
150 (* get_descr: I_Model.single_TEST -> descriptor option*)
151 fun get_descr (_, _, _, _, (feedb, _)) =
152 case get_dscr' feedb of NONE => NONE | some_descr => some_descr
153 (* get_equal_descr: I_Model.T_TEST -> Model_Pattern.single -> (Model_Pattern.single * I_Model.single_TEST) list*)
154 fun get_equal_descr i_model (m_patt_single as (_, (descr, _))) =
157 filter (fn i_single => case get_descr i_single of
158 NONE => false (*--------vvvvv*)
159 | SOME descr' => descr' = descr) (*probl_POS*) i_model
161 (map (pair m_patt_single) equal_variants)
164 (*get an appropriate (description, variant) item from pbl_imod, otherwise return empty item*)
165 fun get_descr_vnt descr vnts i_model =
167 val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false
168 | SOME descr' => if descr = descr' then true else false) i_model
170 case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
171 [] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
172 | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
175 get an appropriate (description, variant) item from o_model;
176 called in case of item in met_imod is_empty_single_TEST
177 (i.e. was not transferred pbl_mod by \<open>fun get_descr_vnt\<close>).
179 fun get_descr_vnt' feedb vnts o_model =
180 filter (fn (_, vnts', _, descr', _) =>
181 case get_dscr' feedb of
182 SOME descr => if descr' = descr andalso inter op= vnts' vnts <> [] then true else false
183 | NONE => false) o_model
185 (* all_lhs_atoms: term list -> bool*)
186 fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>
187 if can TermC.lhs t andalso not (TermC.is_num (TermC.lhs t))
188 then TermC.is_atom (TermC.lhs t)
191 fun handle_lists id (descr, ts) =
192 if Model_Pattern.is_list_descr descr
193 then if length ts > 1 (*list with more than 1 element needs to collect by [.., .., ..]*)
194 then if TermC.is_list (hd ts) (*---broken elementwise input to lists---*)
195 then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) (map TermC.the_single ts))]
196 else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)
197 else if TermC.is_atom (Library.the_single ts)
198 then [(id, Library.the_single ts)] (* solutions L, ...*)
199 else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)
200 else [(id, Library.the_single ts)] (* solveFor x, Extremum (A = ...)*)
202 fun mk_env_model _ (Model_Def.Cor_TEST (_, [])) = []
203 | mk_env_model id (Model_Def.Cor_TEST (descr, ts)) =
204 handle_lists id (descr, ts)
205 | mk_env_model _ (Model_Def.Syn_TEST _) = [] (*TODO handle correct list elements*)
206 | mk_env_model _ (Model_Def.Inc_TEST (_, [])) = []
207 | mk_env_model id (Model_Def.Inc_TEST (descr, ts)) =
208 handle_lists id (descr, ts)
209 | mk_env_model _ (Model_Def.Sup_TEST _) = []
210 fun make_env_model equal_descr_pairs =
211 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
212 => (mk_env_model id feedb)) equal_descr_pairs
215 fun switch_type descr [] = descr
216 | switch_type (Free (id_string, _)) ts =
217 Free (id_string, ts |> hd |> TermC.lhs |> type_of)
218 | switch_type descr _ = raise ERROR ("switch_type undefined argument " ^
219 quote (UnparseC.term (ContextC.for_ERROR ()) descr))
221 fun discern_typ _ (_, []) = []
222 | discern_typ id (descr, ts) =
223 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
225 val ts = if Model_Pattern.is_list_descr descr
226 then if TermC.is_list (hd ts)
227 then ts |> map TermC.isalist2list |> flat
231 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
232 if Model_Pattern.typ_of_element descr = HOLogic.boolT andalso all_lhs_atoms ts
235 then (writeln "model items of type 'bool' in lists with 'lengt ts > 1' NOT YET IMPLEMENTED";
237 else [((switch_type id ts, TermC.lhs (hd ts)),
238 (TermC.lhs (hd ts), TermC.rhs (hd ts)))]
240 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
242 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
245 fun discern_feedback id (Model_Def.Cor_TEST (descr, ts)) = discern_typ id (descr, ts)
246 | discern_feedback _ (Model_Def.Syn_TEST _) = [] (*TODO: handle correct elements*)
247 | discern_feedback id (Model_Def.Inc_TEST (descr, ts)) = discern_typ id (descr, ts)
248 | discern_feedback _ (Model_Def.Sup_TEST _) = []
249 fun make_envs_preconds equal_givens =
250 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) equal_givens
254 fun of_max_variant _ [] = ((false, 0, []), [], ([], []))
255 | of_max_variant model_patt i_model =
258 map (fn (_, variants, _, _, _) => variants) i_model
261 val variants_separated = map (filter_variants' i_model) all_variants
262 val sums_corr = map (cnt_corrects) variants_separated
263 val sum_variant_s = arrange_args sums_corr (1, all_variants)
264 val (_, max_variant) = hd (*..crude decision, up to improvement *)
265 (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
267 filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
268 val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
269 val env_model = make_env_model equal_descr_pairs
270 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
271 val subst_eval_list = make_envs_preconds equal_givens
272 val (env_subst, env_eval) = split_list subst_eval_list
274 ((length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model_max)
275 = length model_patt, max_variant, i_model_max),
276 env_model, (env_subst, env_eval))
278 (*T_TEST* \<longrightarrow> Model_Def)
279 fun max_variants model_patt i_model =
282 map (fn (_, variants, _, _, _) => variants) i_model
285 val variants_separated = map (filter_variants' i_model) all_variants
286 val sums_corr = map (cnt_corrects) variants_separated
287 val sum_variant_s = arrange_args sums_corr (1, all_variants)
289 val max_first = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
290 val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
292 val option_sequence = map
293 (fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s
294 (*THAT IS NONSENSE, SEE Test_Theory (*+*)if (pbl_max_imos*)
295 val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>
296 if is_some pos_in_sum_variant_s then i_model else [])
297 (option_sequence ~~ variants_separated)
298 |> filter_out (fn place_holder => place_holder = []);
299 (*/-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------\ * )
301 val option_sequence = map
302 (fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s
303 val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>
304 if is_some pos_in_sum_variant_s then i_model else [])
305 (option_sequence ~~ variants_separated)
306 |> filter_out (fn place_holder => place_holder = []);
308 [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])],
309 [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])]]
310 ------ ----------------------------------------------------------------------------------------
311 val equal_descr_pairs = map (get_equal_descr (hd max_i_models)) model_patt
312 |> flat (*a hack for continuing ------------^^-- "turn to PIDE", works for test example*)
313 val env_model = make_env_model equal_descr_pairs
314 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
315 val subst_eval_list = make_envs_preconds equal_givens
316 val (env_subst, env_eval) = split_list subst_eval_list
317 ( *\-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *)
319 ((maxes, max_i_models)(*, env_model, (env_subst, env_eval)*))
320 (* (maxes, max_i_models)*)
321 (*/-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------\ * )
322 (env_model, (env_subst, env_eval)
323 ( *\--fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *)
328 (*extract the environment from an I_Model.of_max_variant*)
329 fun environment_TEST model_patt i_model = of_max_variant model_patt i_model |> #2
331 (** check pre-conditions **)
332 fun check_pos ctxt where_rls where_POS (model_patt, i_model) =
334 val (_, _, (_, env_eval)) = of_max_variant model_patt
335 (filter (fn (_, _, _, m_field ,_) => m_field = "#Given") i_model)
336 val full_subst = if env_eval = []
337 then map (fn (t, pos) => ((true, t), pos)) where_POS
338 else map (fn (t, pos) => (TermC.subst_atomic_all env_eval t, pos)) where_POS;
339 val evals = map (fn ((bool_t), pos) => (eval ctxt where_rls bool_t, pos)) full_subst;
340 val display = map (fn ((t, pos), ((bool, _), _)) => (bool, (t, pos))) (where_POS ~~ evals)
342 (foldl and_ (true, map (fn ((bool, _: term), _: Position.T) => bool) evals), display)
345 (*takes the envs resulting from of_max_variant*)
346 fun check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval)) =
348 val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
349 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
350 val full_subst = if env_eval = [] then pres_subst_other
351 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
352 val evals = map (eval ctxt where_rls) full_subst
354 (foldl and_ (true, map fst evals), pres_subst_other)
357 (*expects the precondition from Problem, ie. needs substitution by env_model*)
358 (*TODO: check shall call check_envs*)
359 fun check _ _ [] _ = (true, [])
360 | check ctxt where_rls where_ (model_patt, i_model) =
362 val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
363 val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
364 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
365 val full_subst = if env_eval = [] then pres_subst_other
366 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
367 val evals = map (eval ctxt where_rls) full_subst
369 (foldl and_ (true, map fst evals), pres_subst_other)
372 fun unchecked_OLD_to_TEST pres = map (fn t => (t, Position.none)) pres