Walther@60605
|
1 |
(* Title: Specify/pre-conds.sml
|
walther@59960
|
2 |
Author: Walther Neuper 110226
|
Walther@60705
|
3 |
(c) due to copyrigh,t terms
|
walther@59960
|
4 |
*)
|
walther@59960
|
5 |
|
walther@59960
|
6 |
signature PRE_CONDITIONS =
|
walther@59960
|
7 |
sig
|
walther@59963
|
8 |
type T
|
Walther@60605
|
9 |
type unchecked
|
Walther@60741
|
10 |
type unchecked_pos
|
Walther@60705
|
11 |
type checked
|
Walther@60741
|
12 |
type checked_pos
|
Walther@60705
|
13 |
|
Walther@60705
|
14 |
type env_subst
|
Walther@60705
|
15 |
type env_eval
|
Walther@60556
|
16 |
type input
|
Walther@60705
|
17 |
|
Walther@60673
|
18 |
val to_string : Proof.context -> T -> string
|
Walther@60740
|
19 |
val eval: Proof.context -> Rule_Set.T -> bool * term -> bool * term
|
walther@59967
|
20 |
|
Walther@60734
|
21 |
val max_variant: Model_Def.i_model -> Model_Def.variant
|
Walther@60733
|
22 |
val environment_TEST: Model_Pattern.T -> Model_Def.i_model_TEST -> Env.T
|
Walther@60705
|
23 |
|
Walther@60747
|
24 |
val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
|
Walther@60746
|
25 |
(bool * Model_Def.variant * Model_Def.i_model_TEST) * Env.T * (env_subst * env_eval)
|
Walther@60747
|
26 |
val make_envs_preconds: (Model_Pattern.single * Model_Def.i_model_single_TEST) list ->
|
Walther@60747
|
27 |
((term * term) * (term * term)) list
|
Walther@60740
|
28 |
|
Walther@60741
|
29 |
val check_pos: Proof.context -> Rule_Set.T -> unchecked_pos ->
|
Walther@60741
|
30 |
Model_Pattern.T * Model_Def.i_model_TEST -> checked_pos
|
Walther@60741
|
31 |
val check_envs: Proof.context -> Rule_Set.T -> unchecked -> Env.T * (env_subst * env_eval)
|
Walther@60732
|
32 |
-> checked
|
Walther@60741
|
33 |
val check: Proof.context -> Rule_Set.T -> unchecked ->
|
Walther@60706
|
34 |
Model_Pattern.T * Model_Def.i_model_TEST -> checked
|
Walther@60706
|
35 |
|
Walther@60705
|
36 |
(*from isac_test for Minisubpbl*)
|
Walther@60706
|
37 |
val get_equal_descr: Model_Def.i_model_TEST -> Model_Pattern.single ->
|
Walther@60706
|
38 |
(Model_Pattern.single * Model_Def.i_model_single_TEST) list
|
Walther@60706
|
39 |
val unchecked_OLD_to_TEST: term list -> (term * Position.T) list
|
Walther@60705
|
40 |
|
Walther@60710
|
41 |
val all_lhs_atoms: term list -> bool
|
Walther@60740
|
42 |
val handle_lists: term -> Model_Def.descriptor * term list -> Env.T;
|
Walther@60740
|
43 |
val filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST
|
Walther@60741
|
44 |
val switch_type: Model_Def.descriptor -> term list -> Model_Def.descriptor;
|
Walther@60728
|
45 |
val discern_feedback: term -> Model_Def.i_model_feedback_TEST ->
|
Walther@60728
|
46 |
((term * term) * (term * term)) list
|
Walther@60728
|
47 |
val discern_typ: term -> Model_Pattern.descriptor * term list ->
|
Walther@60728
|
48 |
((term * term) * (term * term)) list
|
Walther@60710
|
49 |
|
Walther@60740
|
50 |
val mk_env_model: term -> Model_Def.i_model_feedback_TEST -> Env.T
|
Walther@60740
|
51 |
val make_env_model: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> Env.T
|
Walther@60740
|
52 |
|
Walther@60747
|
53 |
val get_descr: Model_Def.i_model_single_TEST -> Model_Def.descriptor option;
|
Walther@60747
|
54 |
val get_dscr': Model_Def.i_model_feedback_TEST -> Model_Def.descriptor option
|
Walther@60747
|
55 |
val get_descr_vnt: Model_Def.descriptor -> Model_Def.variants -> Model_Def.i_model_TEST ->
|
Walther@60747
|
56 |
Model_Def.i_model_single_TEST
|
Walther@60747
|
57 |
val get_descr_vnt': Model_Def.i_model_feedback_TEST -> Model_Def.variants -> O_Model.T ->
|
Walther@60749
|
58 |
O_Model.T
|
Walther@60747
|
59 |
|
Walther@60747
|
60 |
\<^isac_test>\<open>
|
Walther@60740
|
61 |
(**)
|
wenzelm@60223
|
62 |
\<close>
|
walther@59960
|
63 |
end
|
Walther@60722
|
64 |
|
walther@59965
|
65 |
(**)
|
walther@59960
|
66 |
structure Pre_Conds(**) : PRE_CONDITIONS(**) =
|
walther@59960
|
67 |
struct
|
walther@59965
|
68 |
(**)
|
Walther@60706
|
69 |
open Model_Def
|
walther@59960
|
70 |
|
Walther@60673
|
71 |
type T = Pre_Conds_Def.T; (*= (bool * term) list;*)
|
Walther@60605
|
72 |
type unchecked = term list
|
Walther@60741
|
73 |
type unchecked_pos = (term * Position.T) list
|
Walther@60705
|
74 |
type checked = bool * (bool * term) list
|
Walther@60741
|
75 |
type checked_pos = bool * ((bool * (term * Position.T)) list)
|
Walther@60705
|
76 |
|
Walther@60715
|
77 |
(*
|
Walther@60715
|
78 |
we have three kinds of Env.T in the specification-phase:
|
Walther@60715
|
79 |
(*1*) Env.T produced by I_Model.of_max_variant and required to create O_Model.T, I_Model.T from
|
Walther@60715
|
80 |
Model_Pattern.T.
|
Walther@60715
|
81 |
Env.T / (Constants, fixes) in Model_Pattern.T
|
Walther@60715
|
82 |
e.g.[(fixes, [r = 7])] |
|
Walther@60722
|
83 |
> (Constants, [<r = 7>]) in O/I_Model.T *)
|
Walther@60715
|
84 |
|
Walther@60715
|
85 |
(*2*) type env_subst = Env.T (* / 0 < fixes in Problem.{where_, ...}
|
Walther@60715
|
86 |
eg. [(fixes, r)] |
|
Walther@60715
|
87 |
> 0 < r *)
|
Walther@60715
|
88 |
(*3*) type env_eval = Env.T (* |
|
Walther@60715
|
89 |
eg. [(r, 7)] |
|
Walther@60715
|
90 |
> 0 < 7 \<longrightarrow> true
|
Walther@60715
|
91 |
|
Walther@60715
|
92 |
(*1*) is required to produce (*2*) and (*3*); thus respective code is shifted to Pre_Conds.
|
Walther@60715
|
93 |
(*2*) and (*3*) is produced from I_Model.of_max_variant by restricting to "#Given".
|
Walther@60715
|
94 |
|
Walther@60715
|
95 |
There is a typing problem, probably to be solved by a language for Specification in the future:
|
Walther@60715
|
96 |
term <fixes> in (*1*) has type "bool list"
|
Walther@60715
|
97 |
term <fixes> in (*2*) has type "real". So for the transition from (*1*) to (*2..3*)
|
Walther@60715
|
98 |
fun switch_type is required.
|
Walther@60715
|
99 |
The transition requires better modelling by a novel language for Specification.
|
Walther@60715
|
100 |
*)
|
Walther@60715
|
101 |
|
Walther@60605
|
102 |
type input = TermC.as_string list;
|
walther@59963
|
103 |
|
Walther@60740
|
104 |
(** tools **)
|
Walther@60740
|
105 |
|
Walther@60675
|
106 |
fun to_str ctxt (b, t) = pair2str (bool2str b, UnparseC.term ctxt t);
|
Walther@60673
|
107 |
fun to_string ctxt pres = strs2str' (map (linefeed o (to_str ctxt)) pres);
|
walther@59960
|
108 |
|
Walther@60590
|
109 |
fun eval _ _ (false, where_) = (false, where_) (*NOT ALL Free's have been substituted*)
|
Walther@60590
|
110 |
| eval ctxt where_rls (true, where_) =
|
Walther@60590
|
111 |
if Rewrite.eval_true ctxt [where_] where_rls
|
Walther@60706
|
112 |
then (true, where_)
|
Walther@60706
|
113 |
else (false, where_);
|
walther@59960
|
114 |
|
Walther@60712
|
115 |
|
Walther@60740
|
116 |
(** find the maximal variant within an I_Model.T **)
|
Walther@60705
|
117 |
|
Walther@60740
|
118 |
(* old code before I_Model.T_TEST *)
|
Walther@60740
|
119 |
(*ATTENTION: misses variants with equal number of items, etc*)
|
Walther@60705
|
120 |
fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms);
|
Walther@60705
|
121 |
fun count_variants vts itms = map (cnt itms) vts;
|
Walther@60705
|
122 |
|
Walther@60734
|
123 |
fun max_list [] = raise ERROR "max_list of []"
|
Walther@60734
|
124 |
| max_list (y :: ys) =
|
Walther@60705
|
125 |
let
|
Walther@60747
|
126 |
fun mx (a, x) [] = (a, x)
|
Walther@60705
|
127 |
| mx (a, x) ((b, y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
|
Walther@60705
|
128 |
in mx y ys end;
|
Walther@60705
|
129 |
|
Walther@60740
|
130 |
(*find most frequent variant v in itms*)
|
Walther@60740
|
131 |
fun variants itms = ((distinct op =) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms;
|
Walther@60740
|
132 |
(*find the variant with most items already input, without Pre_Conds (of_max_variant)*)
|
Walther@60747
|
133 |
(*T_TESTold \<rightarrow> fun max_variants*)
|
Walther@60705
|
134 |
fun max_variant itms =
|
Walther@60705
|
135 |
let val vts = (count_variants (variants itms)) itms;
|
Walther@60734
|
136 |
in if vts = [] then 0 else (fst o max_list) vts end;
|
Walther@60705
|
137 |
|
Walther@60705
|
138 |
|
Walther@60740
|
139 |
(* new code with I_Model.T_TEST proper handling variants *)
|
Walther@60705
|
140 |
|
Walther@60740
|
141 |
(*get descriptor of those items which can contribute to Subst.T and Env.T*)
|
Walther@60712
|
142 |
(* get_dscr: feedback_TEST -> descriptor option*)
|
Walther@60750
|
143 |
fun get_dscr' (Cor_TEST (descr, _)) = SOME descr
|
Walther@60750
|
144 |
| get_dscr' (Inc_TEST (descr, _)) = SOME descr
|
Walther@60710
|
145 |
| get_dscr' (Sup_TEST (descr, _)) = SOME descr
|
Walther@60747
|
146 |
| get_dscr' _ = NONE
|
Walther@60747
|
147 |
(*other feedback cannot contribute to I_Model.mk_env_TEST and Pre_Conds.mk_env_TEST*)
|
Walther@60712
|
148 |
(* get_descr: I_Model.single_TEST -> descriptor option*)
|
Walther@60706
|
149 |
fun get_descr (_, _, _, _, (feedb, _)) =
|
Walther@60710
|
150 |
case get_dscr' feedb of NONE => NONE | some_descr => some_descr
|
Walther@60747
|
151 |
(* get_equal_descr: I_Model.T_TEST -> Model_Pattern.single -> (Model_Pattern.single * I_Model.single_TEST) list*)
|
Walther@60706
|
152 |
fun get_equal_descr i_model (m_patt_single as (_, (descr, _))) =
|
Walther@60706
|
153 |
let
|
Walther@60706
|
154 |
val equal_variants =
|
Walther@60706
|
155 |
filter (fn i_single => case get_descr i_single of
|
Walther@60706
|
156 |
NONE => false (*--------vvvvv*)
|
Walther@60706
|
157 |
| SOME descr' => descr' = descr) (*probl_POS*) i_model
|
Walther@60706
|
158 |
in
|
Walther@60706
|
159 |
(map (pair m_patt_single) equal_variants)
|
Walther@60706
|
160 |
end
|
Walther@60712
|
161 |
|
Walther@60747
|
162 |
(*get an appropriate (description, variant) item from pbl_imod, otherwise return empty item*)
|
Walther@60747
|
163 |
fun get_descr_vnt descr vnts i_model =
|
Walther@60747
|
164 |
let
|
Walther@60747
|
165 |
val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false
|
Walther@60747
|
166 |
| SOME descr' => if descr = descr' then true else false) i_model
|
Walther@60747
|
167 |
in
|
Walther@60749
|
168 |
case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
|
Walther@60749
|
169 |
[] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
|
Walther@60749
|
170 |
| items => Library.the_single items (*only applied to model_patt, which has each descr once*)
|
Walther@60747
|
171 |
end
|
Walther@60747
|
172 |
(*
|
Walther@60747
|
173 |
get an appropriate (description, variant) item from o_model;
|
Walther@60747
|
174 |
called in case of item in met_imod is_empty_single_TEST
|
Walther@60747
|
175 |
(i.e. was not transferred pbl_mod by \<open>fun get_descr_vnt\<close>).
|
Walther@60747
|
176 |
*)
|
Walther@60747
|
177 |
fun get_descr_vnt' feedb vnts o_model =
|
Walther@60749
|
178 |
filter (fn (_, vnts', _, descr', _) =>
|
Walther@60747
|
179 |
case get_dscr' feedb of
|
Walther@60747
|
180 |
SOME descr => if descr' = descr andalso inter op= vnts' vnts <> [] then true else false
|
Walther@60747
|
181 |
| NONE => false) o_model
|
Walther@60747
|
182 |
|
Walther@60740
|
183 |
(* all_lhs_atoms: term list -> bool*)
|
Walther@60740
|
184 |
fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>
|
Walther@60740
|
185 |
if can TermC.lhs t andalso not (TermC.is_num (TermC.lhs t))
|
Walther@60740
|
186 |
then TermC.is_atom (TermC.lhs t)
|
Walther@60740
|
187 |
else false) ts) true
|
Walther@60706
|
188 |
|
Walther@60729
|
189 |
fun handle_lists id (descr, ts) =
|
Walther@60729
|
190 |
if Model_Pattern.is_list_descr descr
|
Walther@60729
|
191 |
then if length ts > 1 (*list with more than 1 element needs to collect by [.., .., ..]*)
|
Walther@60729
|
192 |
then if TermC.is_list (hd ts) (*---broken elementwise input to lists---*)
|
Walther@60729
|
193 |
then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) (map TermC.the_single ts))]
|
Walther@60729
|
194 |
else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)
|
Walther@60729
|
195 |
else if TermC.is_atom (Library.the_single ts)
|
Walther@60729
|
196 |
then [(id, Library.the_single ts)] (* solutions L, ...*)
|
Walther@60729
|
197 |
else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)
|
Walther@60729
|
198 |
else [(id, Library.the_single ts)] (* solveFor x, Extremum (A = ...)*)
|
Walther@60726
|
199 |
|
Walther@60750
|
200 |
fun mk_env_model _ (Model_Def.Cor_TEST (_, [])) = []
|
Walther@60750
|
201 |
| mk_env_model id (Model_Def.Cor_TEST (descr, ts)) =
|
Walther@60726
|
202 |
handle_lists id (descr, ts)
|
Walther@60722
|
203 |
| mk_env_model _ (Model_Def.Syn_TEST _) = [] (*TODO handle correct list elements*)
|
Walther@60750
|
204 |
| mk_env_model _ (Model_Def.Inc_TEST (_, [])) = []
|
Walther@60750
|
205 |
| mk_env_model id (Model_Def.Inc_TEST (descr, ts)) =
|
Walther@60726
|
206 |
handle_lists id (descr, ts)
|
Walther@60722
|
207 |
| mk_env_model _ (Model_Def.Sup_TEST _) = []
|
Walther@60722
|
208 |
fun make_env_model equal_descr_pairs =
|
Walther@60721
|
209 |
map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
|
Walther@60722
|
210 |
=> (mk_env_model id feedb)) equal_descr_pairs
|
Walther@60721
|
211 |
|> flat
|
Walther@60722
|
212 |
|
Walther@60741
|
213 |
fun switch_type descr [] = descr
|
Walther@60741
|
214 |
| switch_type (Free (id_string, _)) ts =
|
Walther@60724
|
215 |
Free (id_string, ts |> hd |> TermC.lhs |> type_of)
|
Walther@60741
|
216 |
| switch_type descr _ = raise ERROR ("switch_type undefined argument " ^
|
Walther@60722
|
217 |
quote (UnparseC.term (ContextC.for_ERROR ()) descr))
|
Walther@60740
|
218 |
|
Walther@60729
|
219 |
fun discern_typ _ (_, []) = []
|
Walther@60729
|
220 |
| discern_typ id (descr, ts) =
|
Walther@60729
|
221 |
(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
|
Walther@60729
|
222 |
let
|
Walther@60729
|
223 |
val ts = if Model_Pattern.is_list_descr descr
|
Walther@60729
|
224 |
then if TermC.is_list (hd ts)
|
Walther@60729
|
225 |
then ts |> map TermC.isalist2list |> flat
|
Walther@60729
|
226 |
else ts
|
Walther@60729
|
227 |
else ts
|
Walther@60729
|
228 |
in
|
Walther@60729
|
229 |
(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
|
Walther@60729
|
230 |
if Model_Pattern.typ_of_element descr = HOLogic.boolT andalso all_lhs_atoms ts
|
Walther@60729
|
231 |
then
|
Walther@60729
|
232 |
if length ts > 1
|
Walther@60729
|
233 |
then (writeln "model items of type 'bool' in lists with 'lengt ts > 1' NOT YET IMPLEMENTED";
|
Walther@60729
|
234 |
[])
|
Walther@60741
|
235 |
else [((switch_type id ts, TermC.lhs (hd ts)),
|
Walther@60729
|
236 |
(TermC.lhs (hd ts), TermC.rhs (hd ts)))]
|
Walther@60729
|
237 |
else []
|
Walther@60729
|
238 |
(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
|
Walther@60729
|
239 |
end
|
Walther@60729
|
240 |
(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
|
Walther@60729
|
241 |
(*T_TESTnew*)
|
Walther@60729
|
242 |
|
Walther@60750
|
243 |
fun discern_feedback id (Model_Def.Cor_TEST (descr, ts)) = discern_typ id (descr, ts)
|
Walther@60722
|
244 |
| discern_feedback _ (Model_Def.Syn_TEST _) = [] (*TODO: handle correct elements*)
|
Walther@60750
|
245 |
| discern_feedback id (Model_Def.Inc_TEST (descr, ts)) = discern_typ id (descr, ts)
|
Walther@60722
|
246 |
| discern_feedback _ (Model_Def.Sup_TEST _) = []
|
Walther@60728
|
247 |
fun make_envs_preconds equal_givens =
|
Walther@60722
|
248 |
map (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) equal_givens
|
Walther@60722
|
249 |
|> flat
|
Walther@60721
|
250 |
|
Walther@60747
|
251 |
(*T_TESTold*)
|
Walther@60746
|
252 |
fun of_max_variant _ [] = ((false, 0, []), [], ([], []))
|
Walther@60723
|
253 |
| of_max_variant model_patt i_model =
|
Walther@60723
|
254 |
let
|
Walther@60710
|
255 |
val all_variants =
|
Walther@60710
|
256 |
map (fn (_, variants, _, _, _) => variants) i_model
|
Walther@60710
|
257 |
|> flat
|
Walther@60710
|
258 |
|> distinct op =
|
Walther@60710
|
259 |
val variants_separated = map (filter_variants' i_model) all_variants
|
Walther@60710
|
260 |
val sums_corr = map (cnt_corrects) variants_separated
|
Walther@60741
|
261 |
val sum_variant_s = arrange_args sums_corr (1, all_variants)
|
Walther@60710
|
262 |
val (_, max_variant) = hd (*..crude decision, up to improvement *)
|
Walther@60710
|
263 |
(sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
|
Walther@60710
|
264 |
val i_model_max =
|
Walther@60710
|
265 |
filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
|
Walther@60721
|
266 |
val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
|
Walther@60722
|
267 |
val env_model = make_env_model equal_descr_pairs
|
Walther@60722
|
268 |
val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
|
Walther@60722
|
269 |
val subst_eval_list = make_envs_preconds equal_givens
|
Walther@60722
|
270 |
val (env_subst, env_eval) = split_list subst_eval_list
|
Walther@60721
|
271 |
in
|
Walther@60746
|
272 |
((length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model_max)
|
Walther@60746
|
273 |
= length model_patt, max_variant, i_model_max),
|
Walther@60746
|
274 |
env_model, (env_subst, env_eval))
|
Walther@60721
|
275 |
end
|
Walther@60748
|
276 |
(*T_TEST* \<longrightarrow> Model_Def)
|
Walther@60747
|
277 |
fun max_variants model_patt i_model =
|
Walther@60747
|
278 |
let
|
Walther@60747
|
279 |
val all_variants =
|
Walther@60747
|
280 |
map (fn (_, variants, _, _, _) => variants) i_model
|
Walther@60747
|
281 |
|> flat
|
Walther@60747
|
282 |
|> distinct op =
|
Walther@60747
|
283 |
val variants_separated = map (filter_variants' i_model) all_variants
|
Walther@60747
|
284 |
val sums_corr = map (cnt_corrects) variants_separated
|
Walther@60747
|
285 |
val sum_variant_s = arrange_args sums_corr (1, all_variants)
|
Walther@60747
|
286 |
|
Walther@60747
|
287 |
val max_first = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
|
Walther@60747
|
288 |
val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
|
Walther@60747
|
289 |
|> map snd
|
Walther@60747
|
290 |
val option_sequence = map
|
Walther@60747
|
291 |
(fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s
|
Walther@60748
|
292 |
(*THAT IS NONSENSE, SEE Test_Theory (*+*)if (pbl_max_imos*)
|
Walther@60747
|
293 |
val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>
|
Walther@60747
|
294 |
if is_some pos_in_sum_variant_s then i_model else [])
|
Walther@60747
|
295 |
(option_sequence ~~ variants_separated)
|
Walther@60747
|
296 |
|> filter_out (fn place_holder => place_holder = []);
|
Walther@60747
|
297 |
(*/-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------\ * )
|
Walther@60747
|
298 |
PROBALBY FOR RE-USE:
|
Walther@60747
|
299 |
val option_sequence = map
|
Walther@60747
|
300 |
(fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s
|
Walther@60747
|
301 |
val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>
|
Walther@60747
|
302 |
if is_some pos_in_sum_variant_s then i_model else [])
|
Walther@60747
|
303 |
(option_sequence ~~ variants_separated)
|
Walther@60747
|
304 |
|> filter_out (fn place_holder => place_holder = []);
|
Walther@60747
|
305 |
\<longrightarrow> [
|
Walther@60747
|
306 |
[(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])],
|
Walther@60747
|
307 |
[(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])]]
|
Walther@60747
|
308 |
------ ----------------------------------------------------------------------------------------
|
Walther@60747
|
309 |
val equal_descr_pairs = map (get_equal_descr (hd max_i_models)) model_patt
|
Walther@60747
|
310 |
|> flat (*a hack for continuing ------------^^-- "turn to PIDE", works for test example*)
|
Walther@60747
|
311 |
val env_model = make_env_model equal_descr_pairs
|
Walther@60747
|
312 |
val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
|
Walther@60747
|
313 |
val subst_eval_list = make_envs_preconds equal_givens
|
Walther@60747
|
314 |
val (env_subst, env_eval) = split_list subst_eval_list
|
Walther@60747
|
315 |
( *\-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *)
|
Walther@60747
|
316 |
in
|
Walther@60747
|
317 |
((maxes, max_i_models)(*, env_model, (env_subst, env_eval)*))
|
Walther@60747
|
318 |
(* (maxes, max_i_models)*)
|
Walther@60747
|
319 |
(*/-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------\ * )
|
Walther@60747
|
320 |
(env_model, (env_subst, env_eval)
|
Walther@60747
|
321 |
( *\--fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *)
|
Walther@60747
|
322 |
end
|
Walther@60748
|
323 |
( *T_TESTnew*)
|
Walther@60747
|
324 |
|
Walther@60712
|
325 |
|
Walther@60740
|
326 |
(*extract the environment from an I_Model.of_max_variant*)
|
Walther@60733
|
327 |
fun environment_TEST model_patt i_model = of_max_variant model_patt i_model |> #2
|
Walther@60740
|
328 |
|
Walther@60712
|
329 |
(** check pre-conditions **)
|
Walther@60710
|
330 |
|
Walther@60732
|
331 |
fun check_pos ctxt where_rls where_POS (model_patt, i_model) =
|
Walther@60732
|
332 |
let
|
Walther@60732
|
333 |
val (_, _, (_, env_eval)) = of_max_variant model_patt
|
Walther@60732
|
334 |
(filter (fn (_, _, _, m_field ,_) => m_field = "#Given") i_model)
|
Walther@60732
|
335 |
val full_subst = if env_eval = []
|
Walther@60732
|
336 |
then map (fn (t, pos) => ((true, t), pos)) where_POS
|
Walther@60732
|
337 |
else map (fn (t, pos) => (TermC.subst_atomic_all env_eval t, pos)) where_POS;
|
Walther@60732
|
338 |
val evals = map (fn ((bool_t), pos) => (eval ctxt where_rls bool_t, pos)) full_subst;
|
Walther@60732
|
339 |
val display = map (fn ((t, pos), ((bool, _), _)) => (bool, (t, pos))) (where_POS ~~ evals)
|
Walther@60732
|
340 |
in
|
Walther@60732
|
341 |
(foldl and_ (true, map (fn ((bool, _: term), _: Position.T) => bool) evals), display)
|
Walther@60732
|
342 |
end;
|
Walther@60732
|
343 |
|
Walther@60740
|
344 |
(*takes the envs resulting from of_max_variant*)
|
Walther@60741
|
345 |
fun check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval)) =
|
Walther@60727
|
346 |
let
|
Walther@60732
|
347 |
val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
|
Walther@60727
|
348 |
val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
|
Walther@60727
|
349 |
val full_subst = if env_eval = [] then pres_subst_other
|
Walther@60727
|
350 |
else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
|
Walther@60727
|
351 |
val evals = map (eval ctxt where_rls) full_subst
|
Walther@60732
|
352 |
in
|
Walther@60727
|
353 |
(foldl and_ (true, map fst evals), pres_subst_other)
|
Walther@60732
|
354 |
end
|
Walther@60710
|
355 |
|
Walther@60740
|
356 |
(*expects the precondition from Problem, ie. needs substitution by env_model*)
|
Walther@60741
|
357 |
(*TODO: check shall call check_envs*)
|
Walther@60741
|
358 |
fun check _ _ [] _ = (true, [])
|
Walther@60741
|
359 |
| check ctxt where_rls where_ (model_patt, i_model) =
|
Walther@60706
|
360 |
let
|
Walther@60726
|
361 |
val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
|
Walther@60729
|
362 |
val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
|
Walther@60726
|
363 |
val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
|
Walther@60726
|
364 |
val full_subst = if env_eval = [] then pres_subst_other
|
Walther@60726
|
365 |
else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
|
Walther@60706
|
366 |
val evals = map (eval ctxt where_rls) full_subst
|
Walther@60706
|
367 |
in
|
Walther@60726
|
368 |
(foldl and_ (true, map fst evals), pres_subst_other)
|
Walther@60706
|
369 |
end;
|
Walther@60706
|
370 |
|
Walther@60706
|
371 |
fun unchecked_OLD_to_TEST pres = map (fn t => (t, Position.none)) pres
|
Walther@60706
|
372 |
|
walther@59965
|
373 |
(**)end(**)
|