1.1 --- a/src/Tools/isac/Specify/i-model.sml Fri Dec 01 05:51:18 2023 +0100
1.2 +++ b/src/Tools/isac/Specify/i-model.sml Fri Dec 01 06:08:22 2023 +0100
1.3 @@ -9,17 +9,17 @@
1.4 sig
1.5
1.6 type T
1.7 - type T_TEST
1.8 - val OLD_to_TEST: T -> T_TEST
1.9 - val TEST_to_OLD: T_TEST -> T
1.10 + type T_POS
1.11 + val OLD_to_POS: T -> T_POS
1.12 + val TEST_to_OLD: T_POS -> T
1.13 val empty: T
1.14 - val empty_TEST: T_TEST
1.15 + val empty_POS: T_POS
1.16
1.17 type single
1.18 - type single_TEST
1.19 + type single_POS
1.20 val empty_single: single
1.21 - val empty_single_TEST: single_TEST
1.22 - val is_empty_single_TEST: single_TEST -> bool
1.23 + val empty_single_POS: single_POS
1.24 + val is_empty_single_POS: single_POS -> bool
1.25
1.26 type variant
1.27 type variants
1.28 @@ -28,23 +28,23 @@
1.29 type values
1.30
1.31 datatype feedback = datatype Model_Def.i_model_feedback
1.32 - datatype feedback_TEST = datatype Model_Def.i_model_feedback_TEST
1.33 - val feedback_empty_TEST: Model_Def.i_model_feedback_TEST
1.34 + datatype feedback_POS = datatype Model_Def.i_model_feedback_POS
1.35 + val feedback_empty_POS: Model_Def.i_model_feedback_POS
1.36
1.37 type env
1.38 type message
1.39
1.40 val single_to_string: Proof.context -> single -> string
1.41 - val single_to_string_TEST: Proof.context -> single_TEST -> string
1.42 - val single_to_string_TEST': single_TEST -> string
1.43 + val single_to_string_POS: Proof.context -> single_POS -> string
1.44 + val single_to_string_POS': single_POS -> string
1.45 val to_string: Proof.context -> T -> string
1.46 - val to_string_TEST: Proof.context -> T_TEST -> string
1.47 + val to_string_POS: Proof.context -> T_POS -> string
1.48
1.49 - val feedback_OLD_to_TEST: feedback -> feedback_TEST
1.50 + val feedback_OLD_to_POS: feedback -> feedback_POS
1.51
1.52 datatype add_single = Add of single | Err of string
1.53 val init: Model_Pattern.T -> T
1.54 - val init_TEST: Proof.context -> O_Model.T -> Model_Pattern.T -> T_TEST
1.55 + val init_POS: Proof.context -> O_Model.T -> Model_Pattern.T -> T_POS
1.56 val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
1.57 TermC.as_string -> add_single
1.58 val add_single: theory -> single -> T -> T
1.59 @@ -53,36 +53,36 @@
1.60 (*--*)
1.61 val descriptor: feedback -> descriptor
1.62 (*--*)
1.63 - val descriptor_TEST: feedback_TEST -> descriptor
1.64 + val descriptor_POS: feedback_POS -> descriptor
1.65 val values: feedback -> values option
1.66 val o_model_values: feedback -> values
1.67 - val values_TEST': feedback_TEST -> values
1.68 - val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_TEST) list -> string
1.69 - val variables: Model_Pattern.T -> Model_Def.i_model_TEST -> term list
1.70 + val values_POS': feedback_POS -> values
1.71 + val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_POS) list -> string
1.72 + val variables: Model_Pattern.T -> Model_Def.i_model_POS -> term list
1.73 val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T
1.74 -> message * single
1.75 val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
1.76
1.77 - val fill_from_o: O_Model.T -> single_TEST -> single_TEST option
1.78 + val fill_from_o: O_Model.T -> single_POS -> single_POS option
1.79
1.80 - val add_other: variant -> T_TEST -> single_TEST -> single_TEST
1.81 - val fill_method: O_Model.T -> T_TEST * T_TEST-> Model_Pattern.T -> T_TEST
1.82 - val s_make_complete: Proof.context -> O_Model.T -> T_TEST * T_TEST -> Problem.id * MethodC.id ->
1.83 - T_TEST * T_TEST
1.84 - val s_are_complete: Proof.context -> O_Model.T -> T_TEST * T_TEST -> Problem.id * MethodC.id -> bool
1.85 + val add_other: variant -> T_POS -> single_POS -> single_POS
1.86 + val fill_method: O_Model.T -> T_POS * T_POS-> Model_Pattern.T -> T_POS
1.87 + val s_make_complete: Proof.context -> O_Model.T -> T_POS * T_POS -> Problem.id * MethodC.id ->
1.88 + T_POS * T_POS
1.89 + val s_are_complete: Proof.context -> O_Model.T -> T_POS * T_POS -> Problem.id * MethodC.id -> bool
1.90
1.91 val is_error: feedback -> bool
1.92 val to_p_model: theory -> feedback -> string
1.93
1.94 (*/----- from isac_test for Minisubpbl*)
1.95 - val msg: variants -> feedback_TEST -> string
1.96 - val transfer_terms: O_Model.single -> single_TEST
1.97 + val msg: variants -> feedback_POS -> string
1.98 + val transfer_terms: O_Model.single -> single_POS
1.99
1.100 val eq1: ''a -> 'b * (''a * 'c) -> bool
1.101 val feedback_to_string: Proof.context -> feedback -> string
1.102 - val feedback_TEST_to_string: Proof.context -> feedback_TEST -> string
1.103 + val feedback_POS_to_string: Proof.context -> feedback_POS -> string
1.104 val descr_vals_to_string: Proof.context -> descriptor * values -> string
1.105 - val feedb_args_to_string: Proof.context -> feedback_TEST -> string
1.106 + val feedb_args_to_string: Proof.context -> feedback_POS -> string
1.107
1.108 val ori_2itm: feedback -> descriptor -> Model_Def.values -> O_Model.single -> single
1.109 val seek_ppc: int -> T -> single option
1.110 @@ -110,46 +110,46 @@
1.111 type values = Model_Def.values
1.112
1.113 type T = Model_Def.i_model_single list;
1.114 -(* for developing input from PIDE, we use T_TEST with these ideas:
1.115 +(* for developing input from PIDE, we use T_POS with these ideas:
1.116 (1) the new structure is as close to old T, because we want to preserve the old tests
1.117 - (2) after development (with *_TEST) of essential parts of the Specification's semantics,
1.118 - we adapt the old tests to the new T_TEST
1.119 - (3) together with adaption of the tests we remove the *_TEST
1.120 + (2) after development (with *_POS) of essential parts of the Specification's semantics,
1.121 + we adapt the old tests to the new T_POS
1.122 + (3) together with adaption of the tests we remove the *_POS
1.123 *)
1.124 -type T_TEST = Model_Def.i_model_single_TEST list;
1.125 +type T_POS = Model_Def.i_model_single_POS list;
1.126 datatype feedback = datatype Model_Def.i_model_feedback;
1.127 -datatype feedback_TEST = datatype Model_Def.i_model_feedback_TEST;
1.128 -val feedback_empty_TEST = Model_Def.feedback_empty_TEST
1.129 +datatype feedback_POS = datatype Model_Def.i_model_feedback_POS;
1.130 +val feedback_empty_POS = Model_Def.feedback_empty_POS
1.131 type single = Model_Def.i_model_single;
1.132 -type single_TEST = Model_Def.i_model_single_TEST;
1.133 +type single_POS = Model_Def.i_model_single_POS;
1.134 val empty_single = Model_Def.i_model_empty;
1.135 -val empty_single_TEST = Model_Def.i_model_empty_TEST;
1.136 -fun is_empty_single_TEST (0, [], false, "i_model_empty", _) = true
1.137 - | is_empty_single_TEST _ = false
1.138 +val empty_single_POS = Model_Def.i_model_empty_POS;
1.139 +fun is_empty_single_POS (0, [], false, "i_model_empty", _) = true
1.140 + | is_empty_single_POS _ = false
1.141
1.142 val empty = []: T;
1.143 -val empty_TEST = []: T_TEST;
1.144 +val empty_POS = []: T_POS;
1.145
1.146 type env = Env.T
1.147
1.148
1.149 -fun feedback_OLD_to_TEST (Cor ((d, ts), _)) = (Model_Def.Cor_TEST (d, ts))
1.150 - | feedback_OLD_to_TEST (Syn c) = (Model_Def.Syn_TEST c)
1.151 - | feedback_OLD_to_TEST (Typ c) = (Model_Def.Syn_TEST c)
1.152 - | feedback_OLD_to_TEST (Inc ((d, ts), _)) = (Model_Def.Inc_TEST (d, ts))
1.153 - | feedback_OLD_to_TEST (Sup (d, ts)) = (Model_Def.Sup_TEST (d, ts))
1.154 - | feedback_OLD_to_TEST (Mis (d, pid)) = Model_Def.Syn_TEST ((UnparseC.term (ContextC.for_ERROR ()) d) ^ " " ^
1.155 +fun feedback_OLD_to_POS (Cor ((d, ts), _)) = (Model_Def.Cor_POS (d, ts))
1.156 + | feedback_OLD_to_POS (Syn c) = (Model_Def.Syn_POS c)
1.157 + | feedback_OLD_to_POS (Typ c) = (Model_Def.Syn_POS c)
1.158 + | feedback_OLD_to_POS (Inc ((d, ts), _)) = (Model_Def.Inc_POS (d, ts))
1.159 + | feedback_OLD_to_POS (Sup (d, ts)) = (Model_Def.Sup_POS (d, ts))
1.160 + | feedback_OLD_to_POS (Mis (d, pid)) = Model_Def.Syn_POS ((UnparseC.term (ContextC.for_ERROR ()) d) ^ " " ^
1.161 (UnparseC.term (ContextC.for_ERROR ()) pid))
1.162 - | feedback_OLD_to_TEST (Par s) = (Model_Def.Syn_TEST s)
1.163 -fun OLD_to_TEST i_old =
1.164 - map (fn (a, b, c, d, e) => (a, b, c, d, (feedback_OLD_to_TEST e, Position.none))) i_old
1.165 + | feedback_OLD_to_POS (Par s) = (Model_Def.Syn_POS s)
1.166 +fun OLD_to_POS i_old =
1.167 + map (fn (a, b, c, d, e) => (a, b, c, d, (feedback_OLD_to_POS e, Position.none))) i_old
1.168
1.169 -fun feedback_TEST_to_OLD (Model_Def.Cor_TEST (d, ts)) = (Cor ((d, ts), (TermC.empty, [])))
1.170 - | feedback_TEST_to_OLD (Model_Def.Syn_TEST c) = (Syn c)
1.171 - | feedback_TEST_to_OLD (Model_Def.Inc_TEST (d, ts)) = (Inc ((d, ts), (TermC.empty, [])))
1.172 - | feedback_TEST_to_OLD (Model_Def.Sup_TEST (d, ts)) = (Sup (d, ts))
1.173 +fun feedback_POS_to_OLD (Model_Def.Cor_POS (d, ts)) = (Cor ((d, ts), (TermC.empty, [])))
1.174 + | feedback_POS_to_OLD (Model_Def.Syn_POS c) = (Syn c)
1.175 + | feedback_POS_to_OLD (Model_Def.Inc_POS (d, ts)) = (Inc ((d, ts), (TermC.empty, [])))
1.176 + | feedback_POS_to_OLD (Model_Def.Sup_POS (d, ts)) = (Sup (d, ts))
1.177 fun TEST_to_OLD i_model =
1.178 - map (fn (a, b, c, d, (e, _)) => (a, b, c, d, feedback_TEST_to_OLD e)) i_model
1.179 + map (fn (a, b, c, d, (e, _)) => (a, b, c, d, feedback_POS_to_OLD e)) i_model
1.180
1.181 type message = string;
1.182
1.183 @@ -165,44 +165,44 @@
1.184 "Mis " ^ UnparseC.term ctxt d ^ " " ^ UnparseC.term ctxt pid
1.185 | feedback_to_string _ (Par s) = "Trm "^s;
1.186
1.187 -fun feedback_TEST_to_string ctxt (Cor_TEST (d, ts)) =
1.188 - "Cor_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
1.189 - | feedback_TEST_to_string _ (Syn_TEST c) =
1.190 - "Syn_TEST " ^ c
1.191 - | feedback_TEST_to_string ctxt (Inc_TEST (d, [])) =
1.192 - "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, [])) ^ " " ^
1.193 +fun feedback_POS_to_string ctxt (Cor_POS (d, ts)) =
1.194 + "Cor_POS " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
1.195 + | feedback_POS_to_string _ (Syn_POS c) =
1.196 + "Syn_POS " ^ c
1.197 + | feedback_POS_to_string ctxt (Inc_POS (d, [])) =
1.198 + "Inc_POS " ^ UnparseC.term ctxt (Input_Descript.join (d, [])) ^ " " ^
1.199 Model_Pattern.empty_for d
1.200 - | feedback_TEST_to_string ctxt (Inc_TEST (d, ts)) =
1.201 - "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
1.202 - | feedback_TEST_to_string ctxt (Sup_TEST (d, ts)) =
1.203 - "Sup_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
1.204 + | feedback_POS_to_string ctxt (Inc_POS (d, ts)) =
1.205 + "Inc_POS " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
1.206 + | feedback_POS_to_string ctxt (Sup_POS (d, ts)) =
1.207 + "Sup_POS " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
1.208
1.209 fun descr_vals_to_string ctxt (descr, values) =
1.210 UnparseC.term ctxt (descr $ Model_Def.values_to_present values)
1.211
1.212 -(*prepare for presentation to user; thus Syn_TEST does NOT raise an exn*)
1.213 -fun feedb_args_to_string ctxt (Cor_TEST (descr, values)) =
1.214 +(*prepare for presentation to user; thus Syn_POS does NOT raise an exn*)
1.215 +fun feedb_args_to_string ctxt (Cor_POS (descr, values)) =
1.216 UnparseC.term ctxt (descr $ Model_Def.values_to_present values)
1.217 - | feedb_args_to_string _ (Syn_TEST str) = str
1.218 - | feedb_args_to_string ctxt (Inc_TEST (descr, [])) =
1.219 + | feedb_args_to_string _ (Syn_POS str) = str
1.220 + | feedb_args_to_string ctxt (Inc_POS (descr, [])) =
1.221 UnparseC.term ctxt descr ^ Model_Pattern.empty_for descr
1.222 - | feedb_args_to_string ctxt (Inc_TEST (descr, values)) =
1.223 + | feedb_args_to_string ctxt (Inc_POS (descr, values)) =
1.224 UnparseC.term ctxt (descr $ Model_Def.values_to_present values)
1.225 - | feedb_args_to_string ctxt (Sup_TEST (descr, values)) =
1.226 + | feedb_args_to_string ctxt (Sup_POS (descr, values)) =
1.227 UnparseC.term ctxt (descr $ Model_Def.values_to_present values)
1.228
1.229 fun single_to_string ctxt (i, is, b, s, itm_) =
1.230 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
1.231 s ^ " ," ^ feedback_to_string ctxt itm_ ^ ")";
1.232 -fun single_to_string_TEST ctxt (i, is, b, s, (itm_, _(*Position.T*))) =
1.233 +fun single_to_string_POS ctxt (i, is, b, s, (itm_, _(*Position.T*))) =
1.234 "(" ^ string_of_int i ^ ", " ^ ints2str' is ^ ", " ^ bool2str b ^ " ," ^
1.235 - s ^ ", (" ^ feedback_TEST_to_string ctxt itm_ ^ ", Position.T))";
1.236 -fun single_to_string_TEST' (i, is, b, s, (itm_, _(*Position.T*))) =
1.237 + s ^ ", (" ^ feedback_POS_to_string ctxt itm_ ^ ", Position.T))";
1.238 +fun single_to_string_POS' (i, is, b, s, (itm_, _(*Position.T*))) =
1.239 "(" ^ string_of_int i ^ ", " ^ ints2str' is ^ ", " ^ bool2str b ^ " ," ^
1.240 - s ^ ", (" ^ feedback_TEST_to_string (ContextC.for_ERROR ()) itm_ ^ ", Position.T))";
1.241 + s ^ ", (" ^ feedback_POS_to_string (ContextC.for_ERROR ()) itm_ ^ ", Position.T))";
1.242
1.243 fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms);
1.244 -fun to_string_TEST ctxt itms = strs2str' (map (linefeed o (single_to_string_TEST ctxt)) itms);
1.245 +fun to_string_POS ctxt itms = strs2str' (map (linefeed o (single_to_string_POS ctxt)) itms);
1.246
1.247
1.248 (** make a Tactic.T **)
1.249 @@ -235,8 +235,8 @@
1.250 case find_first (fn (_, _, _, desc, _) => desc = descriptor) o_model of
1.251 NONE => raise ERROR ("I_Model.patt_to_item NONE for " ^ UnparseC.term ctxt descriptor)
1.252 | SOME (_, variants, m_field, descr, _) => (variants, false, m_field,
1.253 - (Inc_TEST (descr, []), Position.none))
1.254 -fun init_TEST ctxt o_model model_patt =
1.255 + (Inc_POS (descr, []), Position.none))
1.256 +fun init_POS ctxt o_model model_patt =
1.257 let
1.258 val pre_items = map (patt_to_item ctxt o_model) model_patt
1.259 in
1.260 @@ -254,10 +254,10 @@
1.261 | descriptor (Mis (d, _)) = d
1.262 | descriptor _ = raise ERROR "descriptor: uncovered case in fun.def.";
1.263 (*DANGEROUS: do NOT use "UnIqE_tErM" *)
1.264 -fun descriptor_TEST (Cor_TEST (d ,_)) = d
1.265 - | descriptor_TEST (Syn_TEST _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
1.266 - | descriptor_TEST (Inc_TEST (d, _)) = d
1.267 - | descriptor_TEST (Sup_TEST (d, _)) = d
1.268 +fun descriptor_POS (Cor_POS (d ,_)) = d
1.269 + | descriptor_POS (Syn_POS _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
1.270 + | descriptor_POS (Inc_POS (d, _)) = d
1.271 + | descriptor_POS (Sup_POS (d, _)) = d
1.272
1.273 fun values (Cor ((_ , ts), _)) = SOME ts
1.274 | values (Syn _) = NONE
1.275 @@ -273,18 +273,18 @@
1.276 | o_model_values (Sup (_, ts)) = ts
1.277 | o_model_values (Mis _) = []
1.278 | o_model_values _ = raise ERROR "o_model_values: uncovered case in fun.def.";
1.279 -fun values_TEST' (Cor_TEST (_, ts)) = ts
1.280 - | values_TEST' (Syn_TEST _) = raise ERROR "values_TEST' NOT for Syn_TEST"
1.281 - | values_TEST' (Inc_TEST (_, ts)) = ts
1.282 - | values_TEST' (Sup_TEST (_, ts)) = ts
1.283 +fun values_POS' (Cor_POS (_, ts)) = ts
1.284 + | values_POS' (Syn_POS _) = raise ERROR "values_POS' NOT for Syn_POS"
1.285 + | values_POS' (Inc_POS (_, ts)) = ts
1.286 + | values_POS' (Sup_POS (_, ts)) = ts
1.287
1.288 fun descr_pairs_to_string ctxt equal_descr_pairs =
1.289 -(map (fn (a, b) => pair (Model_Pattern.single_to_string ctxt a) (single_to_string_TEST ctxt b)
1.290 +(map (fn (a, b) => pair (Model_Pattern.single_to_string ctxt a) (single_to_string_POS ctxt b)
1.291 |> pair2str) equal_descr_pairs)
1.292 |> strs2str'
1.293
1.294 fun variables model_patt i_model =
1.295 - Pre_Conds.environment_TEST model_patt i_model
1.296 + Pre_Conds.environment_POS model_patt i_model
1.297 |> map snd
1.298
1.299 val unknown_descriptor = Syntax.read_term\<^context> "unknown::'a => unknow";
1.300 @@ -490,28 +490,28 @@
1.301 if Model_Def.is_list_descr descr
1.302 then
1.303 let
1.304 - val already_input = feedb |> values_TEST'
1.305 + val already_input = feedb |> values_POS'
1.306 val miss = subtract op= already_input all_values (*"[[c], [c_2], [c_3], [c_4]]"*)
1.307 val ts = already_input @ [hd miss]
1.308 in
1.309 if length all_values = length ts
1.310 - then SOME (i, vnts, bool, m_field, (Cor_TEST (descr, [Model_Def.values_to_present ts]), pos))
1.311 - else SOME (i, vnts, bool, m_field, (Inc_TEST (descr, [Model_Def.values_to_present ts]), pos))
1.312 + then SOME (i, vnts, bool, m_field, (Cor_POS (descr, [Model_Def.values_to_present ts]), pos))
1.313 + else SOME (i, vnts, bool, m_field, (Inc_POS (descr, [Model_Def.values_to_present ts]), pos))
1.314 end
1.315 - else SOME (i, vnts, bool, m_field, (Cor_TEST (descr, all_values(*only 1 term*)), pos))
1.316 + else SOME (i, vnts, bool, m_field, (Cor_POS (descr, all_values(*only 1 term*)), pos))
1.317 end
1.318
1.319 (*
1.320 - in case there is an item in i2_model(= met) with Sup_TEST,
1.321 - find_first an appropriate (variant, descriptor) item in i1_model(= pbl) and add it instead Sup_TEST,
1.322 + in case there is an item in i2_model(= met) with Sup_POS,
1.323 + find_first an appropriate (variant, descriptor) item in i1_model(= pbl) and add it instead Sup_POS,
1.324 otherwise keep the items of i2_model.
1.325 *)
1.326 -fun add_other max_vnt i1_model (i2, _, bool2, m_field2, (Sup_TEST (descr2, ts2), pos2)) =
1.327 +fun add_other max_vnt i1_model (i2, _, bool2, m_field2, (Sup_POS (descr2, ts2), pos2)) =
1.328 (case find_first (fn (_, vnts1, _, _, (feedb1, _)) => case Model_Def.get_dscr_opt feedb1 of
1.329 NONE => false
1.330 | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model of
1.331 NONE =>
1.332 - (i2, [max_vnt], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2)) (*the present in i2_model*)
1.333 + (i2, [max_vnt], bool2, m_field2, (Sup_POS (descr2, ts2), pos2)) (*the present in i2_model*)
1.334 | SOME i1_single => i1_single) (*shift the item from i1_model to i2_model*)
1.335 | add_other _ _ i2_single = i2_single (*keep all the other items in i2_model*)
1.336
1.337 @@ -534,7 +534,7 @@
1.338 "variants " ^ ints2str' vnts ^ " and descriptor " ^
1.339 (feedb |> Model_Def.get_dscr_opt |> the |> UnparseC.term (ContextC.for_ERROR ()))
1.340 fun transfer_terms (i, vnts, m_field, descr, ts) =
1.341 - (i, vnts, true, m_field, (Cor_TEST (descr, ts), Position.none))
1.342 + (i, vnts, true, m_field, (Cor_POS (descr, ts), Position.none))
1.343 fun s_make_complete ctxt o_model (pbl_imod, met_imod) (pbl_id, met_id) =
1.344 let
1.345 val {model = pbl_patt, ...} = Problem.from_store ctxt pbl_id;
1.346 @@ -543,7 +543,7 @@
1.347 val i_from_pbl = map (fn (_, (descr, _)) =>
1.348 Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt
1.349 val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
1.350 - if is_empty_single_TEST i_single
1.351 + if is_empty_single_POS i_single
1.352 then
1.353 case Pre_Conds.get_descr_vnt' feedb pbl_max_vnts o_model of
1.354 [] => raise ERROR (msg pbl_max_vnts feedb)
1.355 @@ -556,7 +556,7 @@
1.356 val max_vnt = hd met_max_vnts (*need only one for solve-phase*)
1.357
1.358 val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
1.359 - if is_empty_single_TEST i_single
1.360 + if is_empty_single_POS i_single
1.361 then
1.362 case Pre_Conds.get_descr_vnt' feedb [max_vnt] o_model of
1.363 [] => raise ERROR (msg [max_vnt] feedb)