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@60712
|
10 |
(*RENA unchecked_pos*)
|
Walther@60705
|
11 |
type unchecked_TEST
|
Walther@60705
|
12 |
type checked
|
Walther@60712
|
13 |
(*RENA checked_pos*)
|
Walther@60705
|
14 |
type checked_TEST
|
Walther@60705
|
15 |
|
Walther@60705
|
16 |
type env_subst
|
Walther@60705
|
17 |
type env_eval
|
Walther@60556
|
18 |
type input
|
Walther@60705
|
19 |
|
Walther@60673
|
20 |
val to_string : Proof.context -> T -> string
|
walther@59967
|
21 |
|
Walther@60734
|
22 |
val max_variant: Model_Def.i_model -> Model_Def.variant
|
Walther@60733
|
23 |
(*T_TESTold* )
|
Walther@60705
|
24 |
val environment: Model_Def.i_model -> Env.T
|
Walther@60733
|
25 |
( *T_TEST*)
|
Walther@60733
|
26 |
val environment_TEST: Model_Pattern.T -> Model_Def.i_model_TEST -> Env.T
|
Walther@60733
|
27 |
(*T_TEST*)
|
Walther@60705
|
28 |
|
Walther@60732
|
29 |
(* WRONG ENVS * )
|
Walther@60706
|
30 |
val check: Proof.context -> Rule_Set.T -> unchecked -> Model_Def.i_model -> 'a -> checked
|
Walther@60732
|
31 |
( **)
|
Walther@60732
|
32 |
(*T_TESTold* )
|
Walther@60710
|
33 |
val check_from_store: Proof.context -> Rule_Set.T -> unchecked -> env_subst -> env_eval -> checked
|
Walther@60732
|
34 |
( *T_TEST*)
|
Walther@60732
|
35 |
(*RN check_with_envs*)
|
Walther@60732
|
36 |
val check_envs_TEST: Proof.context -> Rule_Set.T -> unchecked -> Env.T * (env_subst * env_eval)
|
Walther@60732
|
37 |
-> checked
|
Walther@60732
|
38 |
(*T_TESTnew*)
|
Walther@60732
|
39 |
(**)
|
Walther@60732
|
40 |
(*T_TESTold* )
|
Walther@60732
|
41 |
val check_TEST: Proof.context -> Rule_Set.T -> unchecked_TEST -> env_eval -> checked_TEST
|
Walther@60732
|
42 |
( *T_TEST*)
|
Walther@60732
|
43 |
val check_pos: Proof.context -> Rule_Set.T -> unchecked_TEST ->
|
Walther@60732
|
44 |
Model_Pattern.T * Model_Def.i_model_TEST -> checked_TEST
|
Walther@60732
|
45 |
(*T_TESTnew*)
|
Walther@60710
|
46 |
|
Walther@60710
|
47 |
(*this makes the OLD tests run AFTER introduction of I_Model.T_TEST..*)
|
Walther@60710
|
48 |
val check_OLD: Proof.context -> Rule_Set.T -> unchecked ->
|
Walther@60706
|
49 |
Model_Pattern.T * Model_Def.i_model_TEST -> checked
|
Walther@60706
|
50 |
|
Walther@60590
|
51 |
val eval: Proof.context -> Rule_Set.T -> bool * term -> bool * term
|
Walther@60733
|
52 |
(**)
|
Walther@60733
|
53 |
val feedback_TEST_to_string: Proof.context -> Model_Def.i_model_feedback_TEST -> string
|
Walther@60732
|
54 |
(** )
|
Walther@60705
|
55 |
val check_variant_envs: Proof.context -> Rule_Set.T -> unchecked ->
|
Walther@60705
|
56 |
env_subst -> env_eval -> checked
|
Walther@60732
|
57 |
( **)
|
Walther@60710
|
58 |
|
Walther@60715
|
59 |
(*val sep_variants_envs replaced by of_max_variant TODO
|
Walther@60732
|
60 |
for that purpose compare with sep_variants_envs_OLD TODO* )
|
Walther@60706
|
61 |
val sep_variants_envs: Model_Pattern.T -> Model_Def.i_model_TEST ->
|
Walther@60706
|
62 |
((Model_Def.i_model_TEST * env_subst * env_eval) * Model_Def.variant) list
|
Walther@60710
|
63 |
val sep_variants_envs_OLD: Model_Pattern.T -> Model_Def.i_model_TEST ->
|
Walther@60706
|
64 |
env_subst * env_eval;
|
Walther@60732
|
65 |
( **)
|
Walther@60715
|
66 |
|
Walther@60728
|
67 |
(*T_TESTold* )
|
Walther@60710
|
68 |
val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
|
Walther@60710
|
69 |
Model_Def.i_model_TEST * env_subst * env_eval
|
Walther@60728
|
70 |
( *T_TEST*)
|
Walther@60729
|
71 |
val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
|
Walther@60722
|
72 |
Model_Def.i_model_TEST * Env.T * (env_subst * env_eval)
|
Walther@60728
|
73 |
(*T_TESTnew*)
|
Walther@60706
|
74 |
|
Walther@60705
|
75 |
(*from isac_test for Minisubpbl*)
|
Walther@60729
|
76 |
val handle_lists: term -> Model_Def.descriptor * term list -> Env.T;
|
Walther@60733
|
77 |
(** )
|
Walther@60710
|
78 |
val discern_feedback_subst: Model_Def.descriptor -> Model_Def.i_model_feedback_TEST -> Env.T;
|
Walther@60710
|
79 |
val discern_type_subst: term * term -> term list -> Env.T;
|
Walther@60733
|
80 |
( **)
|
Walther@60728
|
81 |
|
Walther@60732
|
82 |
(** )
|
Walther@60705
|
83 |
val mk_env: Model_Def.i_model_feedback_TEST -> Env.T
|
Walther@60705
|
84 |
val mk_env_subst: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> env_subst
|
Walther@60710
|
85 |
val mk_env_subst_DEL: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> env_subst
|
Walther@60733
|
86 |
val mk_env_eval: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> env_eval
|
Walther@60732
|
87 |
( **)
|
Walther@60706
|
88 |
val filter_variants: (Model_Pattern.single * Model_Def.i_model_single_TEST) list ->
|
Walther@60706
|
89 |
Model_Def.variant -> (Model_Pattern.single * Model_Def.i_model_single_TEST) list
|
Walther@60706
|
90 |
val get_equal_descr: Model_Def.i_model_TEST -> Model_Pattern.single ->
|
Walther@60706
|
91 |
(Model_Pattern.single * Model_Def.i_model_single_TEST) list
|
Walther@60706
|
92 |
val unchecked_OLD_to_TEST: term list -> (term * Position.T) list
|
Walther@60705
|
93 |
|
Walther@60710
|
94 |
val filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST
|
Walther@60710
|
95 |
val arrange_args1: int list -> int * Model_Def.variant list -> (int * Model_Def.variant) list
|
Walther@60710
|
96 |
val cnt_corrects: Model_Def.i_model_TEST -> int
|
Walther@60733
|
97 |
(** )
|
Walther@60710
|
98 |
val handle_descr_ts: term -> term list -> Env.T
|
Walther@60710
|
99 |
val distinguish_atoms: term list -> Env.T
|
Walther@60733
|
100 |
( **)
|
Walther@60712
|
101 |
(*REN type_repair_env: Env.T -> Env.T*)
|
Walther@60710
|
102 |
val repair_env: Env.T -> Env.T
|
Walther@60710
|
103 |
val all_lhs_atoms: term list -> bool
|
Walther@60728
|
104 |
(*from isac_test for Minisubpbl*)
|
Walther@60728
|
105 |
val mk_env_model: term -> Model_Def.i_model_feedback_TEST -> Env.T
|
Walther@60733
|
106 |
val make_env_model: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> Env.T
|
Walther@60728
|
107 |
val make_envs_preconds: (Model_Pattern.single * Model_Def.i_model_single_TEST) list ->
|
Walther@60728
|
108 |
((term * term) * (term * term)) list
|
Walther@60728
|
109 |
val switch_type_TEST: Model_Def.descriptor -> term list -> Model_Def.descriptor;
|
Walther@60728
|
110 |
val discern_feedback: term -> Model_Def.i_model_feedback_TEST ->
|
Walther@60728
|
111 |
((term * term) * (term * term)) list
|
Walther@60728
|
112 |
val discern_typ: term -> Model_Pattern.descriptor * term list ->
|
Walther@60728
|
113 |
((term * term) * (term * term)) list
|
Walther@60710
|
114 |
|
Walther@60722
|
115 |
\<^isac_test>\<open>
|
Walther@60722
|
116 |
val switch_type: Model_Pattern.descriptor -> typ -> Model_Pattern.descriptor
|
Walther@60705
|
117 |
|
wenzelm@60223
|
118 |
\<close>
|
walther@59960
|
119 |
end
|
Walther@60722
|
120 |
|
walther@59965
|
121 |
(**)
|
walther@59960
|
122 |
structure Pre_Conds(**) : PRE_CONDITIONS(**) =
|
walther@59960
|
123 |
struct
|
walther@59965
|
124 |
(**)
|
Walther@60706
|
125 |
open Model_Def
|
walther@59960
|
126 |
|
Walther@60673
|
127 |
type T = Pre_Conds_Def.T; (*= (bool * term) list;*)
|
Walther@60605
|
128 |
type unchecked = term list
|
Walther@60705
|
129 |
type unchecked_TEST = (term * Position.T) list
|
Walther@60705
|
130 |
type checked = bool * (bool * term) list
|
Walther@60732
|
131 |
type checked_TEST = bool * ((bool * (term * Position.T)) list)
|
Walther@60705
|
132 |
|
Walther@60715
|
133 |
(*
|
Walther@60715
|
134 |
we have three kinds of Env.T in the specification-phase:
|
Walther@60715
|
135 |
(*1*) Env.T produced by I_Model.of_max_variant and required to create O_Model.T, I_Model.T from
|
Walther@60715
|
136 |
Model_Pattern.T.
|
Walther@60715
|
137 |
Env.T / (Constants, fixes) in Model_Pattern.T
|
Walther@60715
|
138 |
e.g.[(fixes, [r = 7])] |
|
Walther@60722
|
139 |
> (Constants, [<r = 7>]) in O/I_Model.T *)
|
Walther@60715
|
140 |
|
Walther@60715
|
141 |
(*2*) type env_subst = Env.T (* / 0 < fixes in Problem.{where_, ...}
|
Walther@60715
|
142 |
eg. [(fixes, r)] |
|
Walther@60715
|
143 |
> 0 < r *)
|
Walther@60715
|
144 |
(*3*) type env_eval = Env.T (* |
|
Walther@60715
|
145 |
eg. [(r, 7)] |
|
Walther@60715
|
146 |
> 0 < 7 \<longrightarrow> true
|
Walther@60715
|
147 |
|
Walther@60715
|
148 |
(*1*) is required to produce (*2*) and (*3*); thus respective code is shifted to Pre_Conds.
|
Walther@60715
|
149 |
(*2*) and (*3*) is produced from I_Model.of_max_variant by restricting to "#Given".
|
Walther@60715
|
150 |
|
Walther@60715
|
151 |
There is a typing problem, probably to be solved by a language for Specification in the future:
|
Walther@60715
|
152 |
term <fixes> in (*1*) has type "bool list"
|
Walther@60715
|
153 |
term <fixes> in (*2*) has type "real". So for the transition from (*1*) to (*2..3*)
|
Walther@60715
|
154 |
fun switch_type is required.
|
Walther@60715
|
155 |
The transition requires better modelling by a novel language for Specification.
|
Walther@60715
|
156 |
*)
|
Walther@60715
|
157 |
|
Walther@60605
|
158 |
type input = TermC.as_string list;
|
walther@59963
|
159 |
|
Walther@60675
|
160 |
fun to_str ctxt (b, t) = pair2str (bool2str b, UnparseC.term ctxt t);
|
Walther@60673
|
161 |
fun to_string ctxt pres = strs2str' (map (linefeed o (to_str ctxt)) pres);
|
walther@59960
|
162 |
|
Walther@60590
|
163 |
fun eval _ _ (false, where_) = (false, where_) (*NOT ALL Free's have been substituted*)
|
Walther@60590
|
164 |
| eval ctxt where_rls (true, where_) =
|
Walther@60590
|
165 |
if Rewrite.eval_true ctxt [where_] where_rls
|
Walther@60706
|
166 |
then (true, where_)
|
Walther@60706
|
167 |
else (false, where_);
|
walther@59960
|
168 |
|
Walther@60712
|
169 |
(** old code before I_Model.T_TEST **)
|
Walther@60712
|
170 |
|
Walther@60705
|
171 |
(* find most frequent variant v in itms *)
|
Walther@60705
|
172 |
(* ATTENTION
|
Walther@60705
|
173 |
* spurios old code
|
Walther@60705
|
174 |
* misses variants with equal number of items, etc
|
Walther@60705
|
175 |
*)
|
Walther@60705
|
176 |
fun variants itms = ((distinct op =) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms;
|
Walther@60705
|
177 |
|
Walther@60705
|
178 |
(*version without typing problem*)
|
Walther@60705
|
179 |
fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms);
|
Walther@60705
|
180 |
fun count_variants vts itms = map (cnt itms) vts;
|
Walther@60705
|
181 |
|
Walther@60734
|
182 |
fun max_list [] = raise ERROR "max_list of []"
|
Walther@60734
|
183 |
| max_list (y :: ys) =
|
Walther@60705
|
184 |
let
|
Walther@60705
|
185 |
fun mx (a, x) [] = (a, x)
|
Walther@60705
|
186 |
| mx (a, x) ((b, y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;
|
Walther@60705
|
187 |
in mx y ys end;
|
Walther@60705
|
188 |
|
Walther@60734
|
189 |
(* find the variant with most items already input, without Pre_Conds (of_max_variant) *)
|
Walther@60705
|
190 |
fun max_variant itms =
|
Walther@60705
|
191 |
let val vts = (count_variants (variants itms)) itms;
|
Walther@60734
|
192 |
in if vts = [] then 0 else (fst o max_list) vts end;
|
Walther@60705
|
193 |
|
Walther@60733
|
194 |
(** )
|
Walther@60706
|
195 |
fun mk_e (Cor (_, iv)) = [getval iv]
|
Walther@60706
|
196 |
| mk_e (Syn _) = []
|
Walther@60706
|
197 |
| mk_e (Typ _) = []
|
Walther@60706
|
198 |
| mk_e (Inc (_, iv)) = [getval iv]
|
Walther@60706
|
199 |
| mk_e (Sup _) = []
|
Walther@60706
|
200 |
| mk_e (Mis _) = []
|
Walther@60705
|
201 |
| mk_e _ = raise ERROR "mk_e: uncovered case in fun.def.";
|
Walther@60705
|
202 |
fun mk_en vt (_, vts, _, _, itm_) = if member op = vts vt then mk_e itm_ else [];
|
Walther@60733
|
203 |
( **)
|
Walther@60705
|
204 |
|
Walther@60705
|
205 |
|
Walther@60706
|
206 |
|
Walther@60712
|
207 |
(** new code for I_Model.T_TEST **)
|
Walther@60712
|
208 |
|
Walther@60733
|
209 |
(** )
|
Walther@60706
|
210 |
fun pen2str ctxt (t, ts) =
|
Walther@60706
|
211 |
pair2str (UnparseC.term ctxt t, (strs2str' o map (UnparseC.term ctxt)) ts);
|
Walther@60733
|
212 |
( **)
|
Walther@60733
|
213 |
fun feedback_TEST_to_string ctxt (Cor_TEST ((d, ts), _)) =
|
Walther@60733
|
214 |
"Cor_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
|
Walther@60733
|
215 |
| feedback_TEST_to_string _ (Syn_TEST c) =
|
Walther@60706
|
216 |
"Syn_TEST " ^ c
|
Walther@60733
|
217 |
| feedback_TEST_to_string ctxt (Inc_TEST ((d, []), _)) =
|
Walther@60714
|
218 |
"Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, [])) ^ " " ^
|
Walther@60717
|
219 |
Model_Pattern.empty_for d
|
Walther@60733
|
220 |
| feedback_TEST_to_string ctxt (Inc_TEST ((d, ts), _)) =
|
Walther@60733
|
221 |
"Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
|
Walther@60733
|
222 |
| feedback_TEST_to_string ctxt (Sup_TEST (d, ts)) =
|
Walther@60706
|
223 |
"Sup_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
|
Walther@60733
|
224 |
(** )
|
Walther@60706
|
225 |
fun feedback_TEST_to_string t = feedback_to_string_TEST (ContextC.for_ERROR ()) t;
|
Walther@60733
|
226 |
( **)
|
Walther@60705
|
227 |
|
Walther@60705
|
228 |
|
Walther@60710
|
229 |
(*** make environments for substituting model_pattern+program and for evaluating pre-conditions ***)
|
Walther@60705
|
230 |
|
Walther@60712
|
231 |
(** OLD make environment for substituting model_pattern+program and pre-conditions **)
|
Walther@60710
|
232 |
|
Walther@60733
|
233 |
(* make an Env.T for Prec_Conds.eval * )
|
Walther@60705
|
234 |
fun mk_env (Model_Def.Cor_TEST ((descr, [ts]), _)) =
|
Walther@60705
|
235 |
let
|
Walther@60706
|
236 |
(*val ts = TermC.isalist2list ts*)
|
Walther@60706
|
237 |
val ts = if TermC.is_list ts then TermC.isalist2list ts else [ts]
|
Walther@60705
|
238 |
in
|
Walther@60705
|
239 |
(*compare Model_Pattern.empty_for*)
|
Walther@60705
|
240 |
case type_of descr of
|
Walther@60705
|
241 |
(Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) (*SideConditions \<longrightarrow> (sideconds, [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2])*)
|
Walther@60712
|
242 |
=> if all_atoms_OLD ts then map (fn t => (TermC.lhs t, TermC.rhs t)) ts else []
|
Walther@60705
|
243 |
| (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) (*AdditionalValues [u, v]*)
|
Walther@60705
|
244 |
=> []
|
Walther@60705
|
245 |
| (Type ("HOL.bool", [])) (*Precision (\<epsilon> = 0.01)*)
|
Walther@60712
|
246 |
=> if all_atoms_OLD ts then map (fn t => (TermC.lhs t, TermC.rhs t)) ts else []
|
Walther@60706
|
247 |
| _ (*Maximum A*) => [(hd ts, TermC.empty (*dummy rhs*))]
|
Walther@60705
|
248 |
end
|
Walther@60705
|
249 |
| mk_env (Model_Def.Inc_TEST ((descr, [ts]), _)) =
|
Walther@60705
|
250 |
let
|
Walther@60706
|
251 |
(*val ts = TermC.isalist2list ts*)
|
Walther@60706
|
252 |
val ts = if TermC.is_list ts then TermC.isalist2list ts else [ts]
|
Walther@60705
|
253 |
in
|
Walther@60705
|
254 |
(*compare Model_Pattern.empty_for*)
|
Walther@60705
|
255 |
case type_of descr of
|
Walther@60705
|
256 |
(Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) (*SideConditions \<longrightarrow> (sideconds, [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2])*)
|
Walther@60712
|
257 |
=> if all_atoms_OLD ts then map (fn t => (TermC.lhs t, TermC.rhs t)) ts else []
|
Walther@60705
|
258 |
| (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) (*AdditionalValues [u, v]*)
|
Walther@60705
|
259 |
=> []
|
Walther@60705
|
260 |
| (Type ("HOL.bool", [])) (*Precision (\<epsilon> = 0.01)*)
|
Walther@60712
|
261 |
=> if all_atoms_OLD ts then map (fn t => (TermC.lhs t, TermC.rhs t)) ts else []
|
Walther@60706
|
262 |
| _ (*Maximum A*) => [(hd ts, TermC.empty (*dummy rhs*))]
|
Walther@60705
|
263 |
end
|
Walther@60706
|
264 |
| mk_env (Model_Def.Sup_TEST (descr, [ts])) =
|
Walther@60705
|
265 |
let
|
Walther@60706
|
266 |
(*val ts = TermC.isalist2list ts*)
|
Walther@60706
|
267 |
val ts = if TermC.is_list ts then TermC.isalist2list ts else [ts]
|
Walther@60705
|
268 |
in
|
Walther@60705
|
269 |
(*compare Model_Pattern.empty_for*)
|
Walther@60705
|
270 |
case type_of descr of
|
Walther@60705
|
271 |
(Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) (*SideConditions \<longrightarrow> (sideconds, [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2])*)
|
Walther@60712
|
272 |
=> if all_atoms_OLD ts then map (fn t => (TermC.lhs t, TermC.rhs t)) ts else []
|
Walther@60705
|
273 |
| (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) (*AdditionalValues [u, v]*)
|
Walther@60705
|
274 |
=> []
|
Walther@60705
|
275 |
| (Type ("HOL.bool", [])) (*Precision (\<epsilon> = 0.01)*)
|
Walther@60712
|
276 |
=> if all_atoms_OLD ts then map (fn t => (TermC.lhs t, TermC.rhs t)) ts else []
|
Walther@60706
|
277 |
| _ (*Maximum A*) => [(hd ts, TermC.empty (*dummy rhs*))]
|
Walther@60705
|
278 |
end
|
Walther@60706
|
279 |
| mk_env feedb =
|
Walther@60706
|
280 |
raise ERROR ("mk_env not reasonable for " ^ quote (feedback_TEST_to_string feedb))
|
Walther@60733
|
281 |
( ** )
|
Walther@60705
|
282 |
fun mk_env_subst equal_descr_pairs =
|
Walther@60705
|
283 |
map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
|
Walther@60706
|
284 |
=> (mk_env feedb) |> map fst (*dummy rhs dropped*)|> map (pair id)) equal_descr_pairs
|
Walther@60705
|
285 |
|> flat
|
Walther@60705
|
286 |
|> repair_env
|
Walther@60732
|
287 |
( **)
|
Walther@60733
|
288 |
(*fun mk_env_eval unused? DEL!* )
|
Walther@60705
|
289 |
fun mk_env_eval equal_descr_pairs =
|
Walther@60705
|
290 |
map (fn (_, (_, _, _, _, (feedb, _))) => mk_env feedb) equal_descr_pairs
|
Walther@60705
|
291 |
|> flat
|
Walther@60706
|
292 |
|> filter_out (fn (_, b) => b = TermC.empty) (*drop pairs with dummy rhs*)
|
Walther@60733
|
293 |
( **)
|
Walther@60710
|
294 |
|
Walther@60733
|
295 |
(* all_atoms: term list -> bool* )
|
Walther@60710
|
296 |
fun all_atoms ts =
|
Walther@60710
|
297 |
fold (curry and_) (map (fn t => TermC.is_atom t) ts) true
|
Walther@60733
|
298 |
( **)
|
Walther@60712
|
299 |
(* all_lhs_atoms: term list -> bool*)
|
Walther@60710
|
300 |
fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>
|
Walther@60729
|
301 |
if can TermC.lhs t andalso not (TermC.is_num (TermC.lhs t))
|
Walther@60729
|
302 |
then TermC.is_atom (TermC.lhs t)
|
Walther@60729
|
303 |
else false) ts) true
|
Walther@60729
|
304 |
(*T_TESTold* )
|
Walther@60729
|
305 |
fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>
|
Walther@60710
|
306 |
if can TermC.lhs t then TermC.is_atom (TermC.lhs t) else false) ts) true
|
Walther@60729
|
307 |
( *T_TEST*)
|
Walther@60712
|
308 |
(* distinguish_atoms: term list -> Env.T*)
|
Walther@60729
|
309 |
(*T_TESTnew*)
|
Walther@60733
|
310 |
(** )
|
Walther@60710
|
311 |
fun distinguish_atoms (*[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2], \<epsilon> = 0.01, [L]*) ts =
|
Walther@60710
|
312 |
if all_atoms ts
|
Walther@60710
|
313 |
then map (rpair TermC.empty (*dummy rhs*)) ts
|
Walther@60710
|
314 |
else if all_lhs_atoms ts
|
Walther@60710
|
315 |
then map (fn t => (TermC.lhs t, TermC.rhs t)) ts
|
Walther@60710
|
316 |
else []
|
Walther@60733
|
317 |
( ** )
|
Walther@60712
|
318 |
(* handle_descr_ts: term -> term list -> (term * term) list*)
|
Walther@60710
|
319 |
fun handle_descr_ts descr ts =
|
Walther@60710
|
320 |
(*compare Model_Pattern.empty_for*)
|
Walther@60710
|
321 |
case type_of descr of
|
Walther@60710
|
322 |
(Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) (*(SideConds [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]), [L]*)
|
Walther@60710
|
323 |
=> distinguish_atoms ts
|
Walther@60710
|
324 |
| (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) (*AdditionalValues [u, v]*)
|
Walther@60710
|
325 |
=> if TermC.is_list (hd ts)
|
Walther@60710
|
326 |
then [(descr, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.realT)]
|
Walther@60710
|
327 |
else []
|
Walther@60710
|
328 |
| (Type ("HOL.bool", [])) (*Precision (\<epsilon> = 0.01)*)
|
Walther@60710
|
329 |
=> distinguish_atoms ts
|
Walther@60710
|
330 |
| _ (*Maximum A*) => [(hd ts, TermC.empty (*dummy rhs*))]
|
Walther@60733
|
331 |
( **)
|
Walther@60710
|
332 |
|
Walther@60712
|
333 |
|
Walther@60712
|
334 |
(** NEW make environment for substituting program and pre-conditions **)
|
Walther@60710
|
335 |
|
Walther@60710
|
336 |
fun switch_type (Free (id, _)) T = Free (id, T)
|
Walther@60710
|
337 |
| switch_type t _ = raise TERM ("switch_type not for", [t])
|
Walther@60710
|
338 |
|
Walther@60733
|
339 |
(*
|
Walther@60733
|
340 |
this repair is spurious and indicates the need for considering a separate language for Model-ing.
|
Walther@60733
|
341 |
E.g. "fixes" is used with 2 different types "bool list" and "real" in the problem-definition
|
Walther@60733
|
342 |
problem pbl_opti_univ : "univariate_calculus/Optimisation" = ..
|
Walther@60733
|
343 |
Given: "Constants fixes"
|
Walther@60733
|
344 |
Where: "0 < fixes"
|
Walther@60733
|
345 |
...
|
Walther@60733
|
346 |
(1) Given: Const ("Input_Descript.Constants", "bool list \<Rightarrow> nam") $ Free ("fixes", "bool list")
|
Walther@60733
|
347 |
(2) Where: Const ("Orderings.ord_class.less", "real \<Rightarrow> real \<Rightarrow> bool") $
|
Walther@60733
|
348 |
Const ("Groups.zero_class.zero", "real") $ Free ("fixes", "real")
|
Walther@60733
|
349 |
|
Walther@60733
|
350 |
The intermediately simplistic solution is to build a pair of environments, type env_pair,
|
Walther@60733
|
351 |
|
Walther@60733
|
352 |
The simplistic design works for the instantiation of the demo-example
|
Walther@60733
|
353 |
"Constants [r = (7::real)]"
|
Walther@60733
|
354 |
but it could be extended to instantiations like
|
Walther@60733
|
355 |
"Constants [a = (1::real), b = (2::real)]"
|
Walther@60733
|
356 |
with the same Where: "0 < fixes" in the problem-definition
|
Walther@60733
|
357 |
if indexing / deletion of found elements from the association list is considered.
|
Walther@60733
|
358 |
|
Walther@60733
|
359 |
For the purpose of future pimprovements a pair of environments, type env_pair, is built;
|
Walther@60733
|
360 |
where as key of the "outer" environment Free ("fixes", "real" kept to future improvements
|
Walther@60733
|
361 |
(by indexing "fixes_1", "fixes_2" in case the are more than one element in
|
Walther@60733
|
362 |
"Input_Descript.Constants", "bool list..)
|
Walther@60733
|
363 |
*)
|
Walther@60710
|
364 |
fun repair_env env =
|
Walther@60710
|
365 |
map (fn (id_inst, val_) => (switch_type id_inst (type_of val_), val_)) env
|
Walther@60710
|
366 |
|
Walther@60710
|
367 |
(* discern_type_subst: term * term -> term list -> Env.T*)
|
Walther@60710
|
368 |
fun discern_type_subst (descr, id) ts =
|
Walther@60710
|
369 |
(*..compare Model_Pattern.empty_for*)
|
Walther@60710
|
370 |
case type_of descr of
|
Walther@60710
|
371 |
(Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) (*(SideConds [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]), [L]*)
|
Walther@60712
|
372 |
=> if TermC.is_list (hd ts)
|
Walther@60712
|
373 |
then [(id, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.boolT)]
|
Walther@60712
|
374 |
else if length ts = 1
|
Walther@60712
|
375 |
then [(id, Library.the_single ts)]
|
Walther@60710
|
376 |
else raise error "discern_type_subst list bool DESIGN ERROR"
|
Walther@60710
|
377 |
| (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) (*AdditionalValues [u, v]*)
|
Walther@60712
|
378 |
=> if TermC.is_list (hd ts)
|
Walther@60712
|
379 |
then [(id, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.realT)]
|
Walther@60712
|
380 |
else if length ts = 1
|
Walther@60712
|
381 |
then [(id, Library.the_single ts)]
|
Walther@60710
|
382 |
else raise error "discern_type_subst list bool DESIGN ERROR"
|
Walther@60712
|
383 |
| _ (*Maximum A*) => [(id, Library.the_single ts)] (*if length ts = 1 !*)
|
Walther@60710
|
384 |
|
Walther@60733
|
385 |
(** )
|
Walther@60712
|
386 |
(* discern_feedback_subst: Model_Def.i_model_feedback_TEST -> Env.T*)
|
Walther@60710
|
387 |
fun discern_feedback_subst id (Model_Def.Cor_TEST ((descr, [ts]), _)) =
|
Walther@60712
|
388 |
discern_type_subst (descr, id) [ts]
|
Walther@60710
|
389 |
| discern_feedback_subst id (Model_Def.Inc_TEST ((descr, [ts]), _)) =
|
Walther@60712
|
390 |
discern_type_subst (descr, id) [ts]
|
Walther@60712
|
391 |
| discern_feedback_subst id (Model_Def.Sup_TEST (descr, [ts])) =
|
Walther@60712
|
392 |
discern_type_subst (descr, id) [ts]
|
Walther@60710
|
393 |
| discern_feedback_subst id (Model_Def.Cor_TEST ((descr, (*[*)ts(*]*)), _)) =
|
Walther@60712
|
394 |
discern_type_subst (descr, id) ts
|
Walther@60712
|
395 |
| discern_feedback_subst _ feedb =
|
Walther@60712
|
396 |
raise ERROR ("discern_feedback_subst not reasonable for " ^ quote (feedback_TEST_to_string feedb))
|
Walther@60710
|
397 |
|
Walther@60710
|
398 |
fun mk_env_subst_DEL equal_descr_pairs =
|
Walther@60710
|
399 |
map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
|
Walther@60710
|
400 |
=> (discern_feedback_subst id feedb)) equal_descr_pairs
|
Walther@60710
|
401 |
|> flat
|
Walther@60710
|
402 |
|> repair_env
|
Walther@60733
|
403 |
( **)
|
Walther@60710
|
404 |
|
Walther@60710
|
405 |
|
Walther@60712
|
406 |
(** NEW make environment for evaluating pre-conditions **)
|
Walther@60712
|
407 |
|
Walther@60733
|
408 |
(** )
|
Walther@60712
|
409 |
(* all_atoms: term list -> bool*)
|
Walther@60710
|
410 |
fun all_atoms ts =
|
Walther@60710
|
411 |
fold (curry and_) (map (fn t => TermC.is_atom t) ts) true
|
Walther@60712
|
412 |
(* discern_atoms: term list -> (term * term) list*)
|
Walther@60710
|
413 |
fun discern_atoms (*[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2], \<epsilon> = 0.01, [L]*) ts =
|
Walther@60710
|
414 |
if all_atoms ts
|
Walther@60710
|
415 |
then map (rpair TermC.empty (*dummy rhs*)) ts
|
Walther@60710
|
416 |
else if all_lhs_atoms ts
|
Walther@60710
|
417 |
then map (fn t => (TermC.lhs t, TermC.rhs t)) ts
|
Walther@60710
|
418 |
else []
|
Walther@60710
|
419 |
|
Walther@60710
|
420 |
fun discern_type_eval descr ts =
|
Walther@60710
|
421 |
(*..compare Model_Pattern.empty_for*)
|
Walther@60710
|
422 |
case type_of descr of
|
Walther@60710
|
423 |
(Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) (*(SideConds [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]), [L]*)
|
Walther@60710
|
424 |
=> discern_atoms ts
|
Walther@60710
|
425 |
| (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) (*AdditionalValues [u, v]*)
|
Walther@60710
|
426 |
=> discern_atoms ts
|
Walther@60710
|
427 |
| _ (*Maximum A*) => discern_atoms ts
|
Walther@60710
|
428 |
|
Walther@60712
|
429 |
fun discern_feedback_eval (Model_Def.Cor_TEST ((descr, [ts]), _)) = discern_type_eval descr [ts]
|
Walther@60712
|
430 |
| discern_feedback_eval (Model_Def.Inc_TEST ((descr, [ts]), _)) = discern_type_eval descr [ts]
|
Walther@60712
|
431 |
| discern_feedback_eval (Model_Def.Sup_TEST (descr, [ts])) = discern_type_eval descr [ts]
|
Walther@60712
|
432 |
| discern_feedback_eval (Model_Def.Cor_TEST ((descr, ts), _)) = discern_type_eval descr ts
|
Walther@60712
|
433 |
| discern_feedback_eval feedb =
|
Walther@60710
|
434 |
raise ERROR ("discern_feedback_eval not defined for " ^ quote (feedback_TEST_to_string feedb))
|
Walther@60710
|
435 |
|
Walther@60710
|
436 |
fun mk_env_eval_DEL i_singles =
|
Walther@60710
|
437 |
map (fn (_, _, _, _, (feedb, _)) => discern_feedback_eval feedb) i_singles
|
Walther@60710
|
438 |
|> flat
|
Walther@60710
|
439 |
|> filter_out (fn (_, b) => b = TermC.empty) (*drop pairs with dummy rhs*)
|
Walther@60733
|
440 |
( **)
|
Walther@60710
|
441 |
|
Walther@60710
|
442 |
|
Walther@60712
|
443 |
(*** old check_variant_envs, sep_variants_envs/_OLD, of_max_variant, check/_TEST/_OLD ***)
|
Walther@60732
|
444 |
(** )
|
Walther@60705
|
445 |
fun check_variant_envs ctxt where_rls pres env_subst env_eval =
|
Walther@60705
|
446 |
let
|
Walther@60705
|
447 |
val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
|
Walther@60705
|
448 |
val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
|
Walther@60705
|
449 |
val evals = map (eval ctxt where_rls) full_subst
|
Walther@60705
|
450 |
in
|
Walther@60705
|
451 |
(foldl and_ (true, map fst evals), pres_subst)
|
Walther@60705
|
452 |
end
|
Walther@60732
|
453 |
( **)
|
Walther@60705
|
454 |
|
walther@59965
|
455 |
|
Walther@60710
|
456 |
(* check_variant_envs for PIDE *)
|
Walther@60706
|
457 |
|
Walther@60706
|
458 |
fun filter_variants pairs i =
|
Walther@60706
|
459 |
filter (fn (_, (_, variants, _, _, _)) => member op= variants i) pairs
|
Walther@60712
|
460 |
|
Walther@60706
|
461 |
(*get descriptor of those items which can contribute to Subst.T and Env.T *)
|
Walther@60712
|
462 |
(* get_dscr: feedback_TEST -> descriptor option*)
|
Walther@60710
|
463 |
fun get_dscr' (Cor_TEST ((descr, _), _)) = SOME descr
|
Walther@60710
|
464 |
| get_dscr' (Inc_TEST ((descr, _), _)) = SOME descr
|
Walther@60710
|
465 |
| get_dscr' (Sup_TEST (descr, _)) = SOME descr
|
Walther@60710
|
466 |
| get_dscr' _
|
Walther@60706
|
467 |
(*other feedback cannot contribute to I_Model.mk_env_TEST and Pre_Conds.mk_env_TEST*) = NONE
|
Walther@60712
|
468 |
(* get_descr: I_Model.single_TEST -> descriptor option*)
|
Walther@60706
|
469 |
fun get_descr (_, _, _, _, (feedb, _)) =
|
Walther@60710
|
470 |
case get_dscr' feedb of NONE => NONE | some_descr => some_descr
|
Walther@60712
|
471 |
(* get_equal_descr: I_Model.T_TEST -> Model_Pattern.single ->
|
Walther@60706
|
472 |
(Model_Pattern.single * I_Model.single_TEST) list*)
|
Walther@60706
|
473 |
fun get_equal_descr i_model (m_patt_single as (_, (descr, _))) =
|
Walther@60706
|
474 |
let
|
Walther@60706
|
475 |
val equal_variants =
|
Walther@60706
|
476 |
filter (fn i_single => case get_descr i_single of
|
Walther@60706
|
477 |
NONE => false (*--------vvvvv*)
|
Walther@60706
|
478 |
| SOME descr' => descr' = descr) (*probl_POS*) i_model
|
Walther@60706
|
479 |
in
|
Walther@60706
|
480 |
(map (pair m_patt_single) equal_variants)
|
Walther@60706
|
481 |
end
|
Walther@60733
|
482 |
(** )
|
Walther@60706
|
483 |
fun arrange_args2 [] _ _ _(*all have equal length*) = []
|
Walther@60706
|
484 |
| arrange_args2 (b :: bs) (c :: cs) (d :: ds) (cnt, all) =
|
Walther@60706
|
485 |
((b, c, d), nth cnt all) :: (arrange_args2 bs cs ds (cnt + 1, all))
|
Walther@60706
|
486 |
| arrange_args2 _ _ _ _ = raise ERROR "I_Model.arrange_args2 UnequalLengths"
|
Walther@60733
|
487 |
( ** )
|
Walther@60706
|
488 |
fun sep_variants_envs model_patt i_model =
|
Walther@60706
|
489 |
let
|
Walther@60706
|
490 |
val equal_descr_pairs =
|
Walther@60706
|
491 |
map (get_equal_descr i_model) model_patt
|
Walther@60706
|
492 |
|> flat
|
Walther@60706
|
493 |
val all_variants =
|
Walther@60706
|
494 |
map (fn (_, (_, variants, _, _, _)) => variants) equal_descr_pairs
|
Walther@60706
|
495 |
|> flat
|
Walther@60706
|
496 |
|> distinct op =
|
Walther@60706
|
497 |
val variants_separated = map (filter_variants equal_descr_pairs) all_variants
|
Walther@60712
|
498 |
val i_models = map (map snd) variants_separated
|
Walther@60706
|
499 |
val restricted_to_given = map (filter (fn ((m_field, (_, _)), (_, _, _, _, (_, _))) =>
|
Walther@60706
|
500 |
m_field = "#Given")) variants_separated
|
Walther@60706
|
501 |
val envs_subst = map mk_env_subst restricted_to_given
|
Walther@60706
|
502 |
val envs_eval = map mk_env_eval restricted_to_given
|
Walther@60706
|
503 |
in
|
Walther@60706
|
504 |
arrange_args2 i_models envs_subst envs_eval (1, all_variants)
|
Walther@60706
|
505 |
end
|
Walther@60732
|
506 |
( **)
|
Walther@60712
|
507 |
|
Walther@60706
|
508 |
(* smash all environments into one; this works only for old test before Maximum-example *)
|
Walther@60732
|
509 |
(** )
|
Walther@60706
|
510 |
fun sep_variants_envs_OLD model_patt i_model =
|
Walther@60706
|
511 |
let
|
Walther@60706
|
512 |
val equal_descr_pairs =
|
Walther@60706
|
513 |
map (get_equal_descr i_model) model_patt
|
Walther@60706
|
514 |
|> flat
|
Walther@60706
|
515 |
val all_variants =
|
Walther@60706
|
516 |
map (fn (_, (_, variants, _, _, _)) => variants) equal_descr_pairs
|
Walther@60706
|
517 |
|> flat
|
Walther@60706
|
518 |
|> distinct op =
|
Walther@60706
|
519 |
val variants_separated = map (filter_variants equal_descr_pairs) all_variants
|
Walther@60706
|
520 |
val restricted_to_given = map (filter (fn ((m_field, (_, _)), (_, _, _, _, (_, _))) =>
|
Walther@60706
|
521 |
m_field = "#Given")) variants_separated
|
Walther@60706
|
522 |
val envs_subst = map mk_env_subst restricted_to_given
|
Walther@60706
|
523 |
val envs_eval = map mk_env_eval restricted_to_given
|
Walther@60706
|
524 |
in
|
Walther@60706
|
525 |
(flat envs_subst, flat envs_eval)
|
Walther@60706
|
526 |
end
|
Walther@60732
|
527 |
( **)
|
Walther@60706
|
528 |
|
Walther@60712
|
529 |
(** of_max_variant **)
|
Walther@60721
|
530 |
|
Walther@60729
|
531 |
(*T_TESTold* )
|
Walther@60726
|
532 |
fun handle_lists id (descr, ts) =
|
Walther@60729
|
533 |
if Model_Pattern.is_list_descr descr
|
Walther@60729
|
534 |
then if length ts > 1 (*list with more than 1 element needs to collect by [.., .., ..]*)
|
Walther@60729
|
535 |
then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)
|
Walther@60729
|
536 |
else if TermC.is_atom (Library.the_single ts)
|
Walther@60729
|
537 |
then [(id, Library.the_single ts)] (* solutions L, ...*)
|
Walther@60729
|
538 |
else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)
|
Walther@60729
|
539 |
else [(id, Library.the_single ts)] (* solveFor x, Extremum (A = ...)*)
|
Walther@60729
|
540 |
( *T_TEST***)
|
Walther@60729
|
541 |
fun handle_lists id (descr, ts) =
|
Walther@60729
|
542 |
if Model_Pattern.is_list_descr descr
|
Walther@60729
|
543 |
then if length ts > 1 (*list with more than 1 element needs to collect by [.., .., ..]*)
|
Walther@60729
|
544 |
then if TermC.is_list (hd ts) (*---broken elementwise input to lists---*)
|
Walther@60729
|
545 |
then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) (map TermC.the_single ts))]
|
Walther@60729
|
546 |
else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)
|
Walther@60729
|
547 |
else if TermC.is_atom (Library.the_single ts)
|
Walther@60729
|
548 |
then [(id, Library.the_single ts)] (* solutions L, ...*)
|
Walther@60729
|
549 |
else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)
|
Walther@60729
|
550 |
else [(id, Library.the_single ts)] (* solveFor x, Extremum (A = ...)*)
|
Walther@60729
|
551 |
(*T_TESTnew*)
|
Walther@60726
|
552 |
|
Walther@60722
|
553 |
fun mk_env_model _ (Model_Def.Cor_TEST ((_, []), _)) = []
|
Walther@60722
|
554 |
| mk_env_model id (Model_Def.Cor_TEST ((descr, ts), _)) =
|
Walther@60728
|
555 |
(*T_TEST.150* )
|
Walther@60722
|
556 |
if Model_Pattern.is_list_descr descr
|
Walther@60721
|
557 |
then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)]
|
Walther@60721
|
558 |
else [(id, hd ts)]
|
Walther@60728
|
559 |
( *T_TEST*)
|
Walther@60726
|
560 |
handle_lists id (descr, ts)
|
Walther@60728
|
561 |
(*T_TEST.100*)
|
Walther@60722
|
562 |
| mk_env_model _ (Model_Def.Syn_TEST _) = [] (*TODO handle correct list elements*)
|
Walther@60722
|
563 |
| mk_env_model _ (Model_Def.Inc_TEST ((_, []), _)) = []
|
Walther@60722
|
564 |
| mk_env_model id (Model_Def.Inc_TEST ((descr, ts), _)) =
|
Walther@60728
|
565 |
(*T_TEST.150* )
|
Walther@60722
|
566 |
if Model_Pattern.is_list_descr descr
|
Walther@60721
|
567 |
then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)]
|
Walther@60721
|
568 |
else [(id, hd ts)]
|
Walther@60728
|
569 |
( *T_TEST*)
|
Walther@60726
|
570 |
handle_lists id (descr, ts)
|
Walther@60728
|
571 |
(*T_TEST.100*)
|
Walther@60722
|
572 |
| mk_env_model _ (Model_Def.Sup_TEST _) = []
|
Walther@60722
|
573 |
fun make_env_model equal_descr_pairs =
|
Walther@60721
|
574 |
map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
|
Walther@60722
|
575 |
=> (mk_env_model id feedb)) equal_descr_pairs
|
Walther@60721
|
576 |
|> flat
|
Walther@60722
|
577 |
|
Walther@60722
|
578 |
fun switch_type_TEST descr [] = descr
|
Walther@60722
|
579 |
| switch_type_TEST (Free (id_string, _)) ts =
|
Walther@60724
|
580 |
Free (id_string, ts |> hd |> TermC.lhs |> type_of)
|
Walther@60728
|
581 |
| switch_type_TEST descr _ = raise ERROR ("switch_type_TEST undefined argument " ^
|
Walther@60722
|
582 |
quote (UnparseC.term (ContextC.for_ERROR ()) descr))
|
Walther@60729
|
583 |
(*T_TESTold* )
|
Walther@60722
|
584 |
fun discern_typ _ (_, []) = []
|
Walther@60722
|
585 |
| discern_typ id (descr, ts) =
|
Walther@60728
|
586 |
(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
|
Walther@60723
|
587 |
let
|
Walther@60728
|
588 |
val ts = if Model_Pattern.is_list_descr descr andalso TermC.is_list (hd ts)
|
Walther@60723
|
589 |
then TermC.isalist2list (hd ts)
|
Walther@60723
|
590 |
else ts
|
Walther@60723
|
591 |
in
|
Walther@60728
|
592 |
(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
|
Walther@60722
|
593 |
if Model_Pattern.typ_of_element descr = HOLogic.boolT
|
Walther@60722
|
594 |
andalso ts |> map TermC.lhs |> all_atoms
|
Walther@60722
|
595 |
then
|
Walther@60722
|
596 |
if length ts > 1
|
Walther@60722
|
597 |
then raise ERROR "model items of type 'bool' in lists with 'lengt ts > 1' NOT YET IMPLEMENTED"
|
Walther@60722
|
598 |
else [((switch_type_TEST id ts, TermC.lhs (hd ts)),
|
Walther@60722
|
599 |
(TermC.lhs (hd ts), TermC.rhs (hd ts)))]
|
Walther@60722
|
600 |
else []
|
Walther@60728
|
601 |
(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
|
Walther@60723
|
602 |
end
|
Walther@60728
|
603 |
(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
|
Walther@60729
|
604 |
( *T_TEST*)
|
Walther@60729
|
605 |
fun discern_typ _ (_, []) = []
|
Walther@60729
|
606 |
| discern_typ id (descr, ts) =
|
Walther@60729
|
607 |
(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
|
Walther@60729
|
608 |
let
|
Walther@60729
|
609 |
val ts = if Model_Pattern.is_list_descr descr
|
Walther@60729
|
610 |
then if TermC.is_list (hd ts)
|
Walther@60729
|
611 |
then ts |> map TermC.isalist2list |> flat
|
Walther@60729
|
612 |
else ts
|
Walther@60729
|
613 |
else ts
|
Walther@60729
|
614 |
in
|
Walther@60729
|
615 |
(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
|
Walther@60729
|
616 |
if Model_Pattern.typ_of_element descr = HOLogic.boolT andalso all_lhs_atoms ts
|
Walther@60729
|
617 |
then
|
Walther@60729
|
618 |
if length ts > 1
|
Walther@60729
|
619 |
then (writeln "model items of type 'bool' in lists with 'lengt ts > 1' NOT YET IMPLEMENTED";
|
Walther@60729
|
620 |
[])
|
Walther@60729
|
621 |
else [((switch_type_TEST id ts, TermC.lhs (hd ts)),
|
Walther@60729
|
622 |
(TermC.lhs (hd ts), TermC.rhs (hd ts)))]
|
Walther@60729
|
623 |
else []
|
Walther@60729
|
624 |
(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
|
Walther@60729
|
625 |
end
|
Walther@60729
|
626 |
(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
|
Walther@60729
|
627 |
(*T_TESTnew*)
|
Walther@60729
|
628 |
|
Walther@60722
|
629 |
fun discern_feedback id (Model_Def.Cor_TEST ((descr, ts), _)) = discern_typ id (descr, ts)
|
Walther@60722
|
630 |
| discern_feedback _ (Model_Def.Syn_TEST _) = [] (*TODO: handle correct elements*)
|
Walther@60722
|
631 |
| discern_feedback id (Model_Def.Inc_TEST ((descr, ts), _)) = discern_typ id (descr, ts)
|
Walther@60722
|
632 |
| discern_feedback _ (Model_Def.Sup_TEST _) = []
|
Walther@60728
|
633 |
fun make_envs_preconds equal_givens =
|
Walther@60722
|
634 |
map (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) equal_givens
|
Walther@60722
|
635 |
|> flat
|
Walther@60721
|
636 |
|
Walther@60712
|
637 |
(* filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST*)
|
Walther@60710
|
638 |
fun filter_variants' i_singles n =
|
Walther@60710
|
639 |
filter (fn (_, variants, _, _, _) => member op= variants n) i_singles
|
Walther@60710
|
640 |
(*arrange_args1: int list -> int * Model_Def.variant list -> (int * Model_Def.variant) list*)
|
Walther@60710
|
641 |
fun arrange_args1 [] _ = []
|
Walther@60710
|
642 |
| arrange_args1 (sum :: ss) (cnt, all) = (sum, nth cnt all) :: (arrange_args1 ss (cnt + 1, all))
|
Walther@60710
|
643 |
(*cnt_corrects: I_Model.T_TEST -> int*)
|
Walther@60710
|
644 |
fun cnt_corrects i_model =
|
Walther@60710
|
645 |
fold (curry op +) (map (fn (_, _, _, _, (Cor_TEST _, _)) => 1 | _ => 0) i_model) 0;
|
Walther@60723
|
646 |
|
Walther@60728
|
647 |
(*T_TESTold* )
|
Walther@60710
|
648 |
fun of_max_variant model_patt i_model =
|
Walther@60728
|
649 |
( *T_TEST*)
|
Walther@60723
|
650 |
fun of_max_variant _ [] = ([], [], ([], []))
|
Walther@60723
|
651 |
| of_max_variant model_patt i_model =
|
Walther@60728
|
652 |
(*T_TESTnew*)
|
Walther@60723
|
653 |
let
|
Walther@60710
|
654 |
val all_variants =
|
Walther@60710
|
655 |
map (fn (_, variants, _, _, _) => variants) i_model
|
Walther@60710
|
656 |
|> flat
|
Walther@60710
|
657 |
|> distinct op =
|
Walther@60710
|
658 |
val variants_separated = map (filter_variants' i_model) all_variants
|
Walther@60710
|
659 |
val sums_corr = map (cnt_corrects) variants_separated
|
Walther@60710
|
660 |
val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
|
Walther@60710
|
661 |
val (_, max_variant) = hd (*..crude decision, up to improvement *)
|
Walther@60710
|
662 |
(sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
|
Walther@60710
|
663 |
val i_model_max =
|
Walther@60710
|
664 |
filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
|
Walther@60721
|
665 |
val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
|
Walther@60728
|
666 |
(*T_TESTold* )
|
Walther@60712
|
667 |
val env_subst = mk_env_subst_DEL equal_descr_pairs
|
Walther@60712
|
668 |
val env_eval = mk_env_eval_DEL i_model_max
|
Walther@60710
|
669 |
in
|
Walther@60712
|
670 |
(i_model_max, env_subst, env_eval)
|
Walther@60710
|
671 |
end
|
Walther@60728
|
672 |
( *T_TEST*)
|
Walther@60722
|
673 |
val env_model = make_env_model equal_descr_pairs
|
Walther@60722
|
674 |
val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
|
Walther@60722
|
675 |
val subst_eval_list = make_envs_preconds equal_givens
|
Walther@60722
|
676 |
val (env_subst, env_eval) = split_list subst_eval_list
|
Walther@60721
|
677 |
in
|
Walther@60722
|
678 |
(i_model_max, env_model, (env_subst, env_eval))
|
Walther@60721
|
679 |
end
|
Walther@60728
|
680 |
(*T_TESTnew*)
|
Walther@60712
|
681 |
|
Walther@60733
|
682 |
(* extract the environment from an I_Model.of_max_variant *)
|
Walther@60733
|
683 |
(*T_TESTold* )
|
Walther@60733
|
684 |
fun environment itms =
|
Walther@60733
|
685 |
let val vt = max_variant itms
|
Walther@60733
|
686 |
in (flat o (map (mk_en vt))) itms end;
|
Walther@60733
|
687 |
( *T_TEST*)
|
Walther@60733
|
688 |
fun environment_TEST model_patt i_model = of_max_variant model_patt i_model |> #2
|
Walther@60733
|
689 |
(*T_TEST*)
|
Walther@60712
|
690 |
|
Walther@60712
|
691 |
(** check pre-conditions **)
|
Walther@60710
|
692 |
|
Walther@60733
|
693 |
(* WRONG ENVS expects the precondition from Problem, ie. needs substitution * )
|
Walther@60706
|
694 |
fun check _ _ [] _ _ = (true, [])
|
Walther@60706
|
695 |
| check ctxt where_rls pres pbl (_ (*I_Model.variants UNNECESSARY: I_Model.T filtered for*)) =
|
Walther@60706
|
696 |
let
|
Walther@60706
|
697 |
val env = environment pbl;
|
Walther@60706
|
698 |
val pres' = map (TermC.subst_atomic_all env) pres;
|
Walther@60706
|
699 |
val evals = map (eval ctxt where_rls) pres';
|
Walther@60706
|
700 |
in (foldl and_ (true, map fst evals), evals) end;
|
Walther@60733
|
701 |
( **)
|
Walther@60732
|
702 |
|
Walther@60732
|
703 |
(*T_TESTold* )
|
Walther@60706
|
704 |
fun check_TEST _ _ [] _ = (true, [])
|
Walther@60706
|
705 |
| check_TEST ctxt where_rls preconds env_eval =
|
Walther@60706
|
706 |
let
|
Walther@60706
|
707 |
val full_subst =
|
Walther@60706
|
708 |
map (fn (t, pos) => (subst_atomic env_eval t, pos)) preconds
|
Walther@60706
|
709 |
val evals =
|
Walther@60706
|
710 |
map (fn (term, pos) => (Rewrite.eval_true ctxt [term] where_rls, (term, pos))) full_subst
|
Walther@60706
|
711 |
in
|
Walther@60706
|
712 |
(foldl and_ (true, map fst evals), (map fst evals) ~~ preconds)
|
Walther@60706
|
713 |
end;
|
Walther@60732
|
714 |
( *T_TEST*)
|
Walther@60732
|
715 |
fun check_pos ctxt where_rls where_POS (model_patt, i_model) =
|
Walther@60732
|
716 |
let
|
Walther@60732
|
717 |
val (_, _, (_, env_eval)) = of_max_variant model_patt
|
Walther@60732
|
718 |
(filter (fn (_, _, _, m_field ,_) => m_field = "#Given") i_model)
|
Walther@60732
|
719 |
val full_subst = if env_eval = []
|
Walther@60732
|
720 |
then map (fn (t, pos) => ((true, t), pos)) where_POS
|
Walther@60732
|
721 |
else map (fn (t, pos) => (TermC.subst_atomic_all env_eval t, pos)) where_POS;
|
Walther@60732
|
722 |
val evals = map (fn ((bool_t), pos) => (eval ctxt where_rls bool_t, pos)) full_subst;
|
Walther@60732
|
723 |
val display = map (fn ((t, pos), ((bool, _), _)) => (bool, (t, pos))) (where_POS ~~ evals)
|
Walther@60732
|
724 |
in
|
Walther@60732
|
725 |
(foldl and_ (true, map (fn ((bool, _: term), _: Position.T) => bool) evals), display)
|
Walther@60732
|
726 |
end;
|
Walther@60732
|
727 |
(*T_TESTnew*)
|
Walther@60732
|
728 |
|
Walther@60732
|
729 |
(*T_TESTold* )
|
Walther@60710
|
730 |
fun check_from_store ctxt where_rls pres env_subst env_eval =
|
Walther@60710
|
731 |
let
|
Walther@60710
|
732 |
val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
|
Walther@60710
|
733 |
val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
|
Walther@60710
|
734 |
val evals = map (eval ctxt where_rls) full_subst
|
Walther@60710
|
735 |
in
|
Walther@60710
|
736 |
(foldl and_ (true, map fst evals), pres_subst)
|
Walther@60710
|
737 |
end
|
Walther@60732
|
738 |
( *T_TEST*)
|
Walther@60732
|
739 |
(* takes the envs resulting from of_max_variant *)
|
Walther@60732
|
740 |
fun check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval)) =
|
Walther@60727
|
741 |
let
|
Walther@60732
|
742 |
val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
|
Walther@60727
|
743 |
val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
|
Walther@60727
|
744 |
val full_subst = if env_eval = [] then pres_subst_other
|
Walther@60727
|
745 |
else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
|
Walther@60727
|
746 |
val evals = map (eval ctxt where_rls) full_subst
|
Walther@60732
|
747 |
in
|
Walther@60727
|
748 |
(foldl and_ (true, map fst evals), pres_subst_other)
|
Walther@60732
|
749 |
end
|
Walther@60732
|
750 |
(*T_TESTnew*)
|
Walther@60732
|
751 |
(* vvv-replaces-^^^*)
|
Walther@60710
|
752 |
|
Walther@60726
|
753 |
(* expects the precondition from Problem, ie. needs substitution by env_model*)
|
Walther@60732
|
754 |
(* TODO: check_OLD shall call check_envs_TEST *)
|
Walther@60706
|
755 |
fun check_OLD _ _ [] _ = (true, [])
|
Walther@60729
|
756 |
| check_OLD ctxt where_rls where_ (model_patt, i_model) =
|
Walther@60706
|
757 |
let
|
Walther@60728
|
758 |
(*T_TESTold* )
|
Walther@60706
|
759 |
val (env_subst, env_eval) = sep_variants_envs_OLD model_patt i_model
|
Walther@60706
|
760 |
val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
|
Walther@60706
|
761 |
val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
|
Walther@60727
|
762 |
val evals = map (eval ctxt where_rls) full_subst
|
Walther@60727
|
763 |
in
|
Walther@60727
|
764 |
(foldl and_ (true, map fst evals), pres_subst)
|
Walther@60727
|
765 |
end;
|
Walther@60728
|
766 |
( *T_TEST*)
|
Walther@60726
|
767 |
val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
|
Walther@60729
|
768 |
val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
|
Walther@60726
|
769 |
val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
|
Walther@60726
|
770 |
val full_subst = if env_eval = [] then pres_subst_other
|
Walther@60726
|
771 |
else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
|
Walther@60706
|
772 |
val evals = map (eval ctxt where_rls) full_subst
|
Walther@60706
|
773 |
in
|
Walther@60726
|
774 |
(foldl and_ (true, map fst evals), pres_subst_other)
|
Walther@60706
|
775 |
end;
|
Walther@60728
|
776 |
(*T_TESTnew*)
|
Walther@60706
|
777 |
|
Walther@60706
|
778 |
fun unchecked_OLD_to_TEST pres = map (fn t => (t, Position.none)) pres
|
Walther@60706
|
779 |
|
walther@59965
|
780 |
(**)end(**)
|