(* Title:  Specify/pre-conds.sml

    Author: Walther Neuper 110226

    (c) due to copyrigh,t terms

 *)

 signature PRE_CONDITIONS =

 sig

   type T

   type unchecked

 (*RENA unchecked_pos*)

   type unchecked_TEST

   type checked

 (*RENA checked_pos*)

   type checked_TEST

   type env_subst

   type env_eval

   type input

   val to_string : Proof.context -> T -> string

   val max_variant: Model_Def.i_model -> int

   val environment: Model_Def.i_model -> Env.T

   val check: Proof.context -> Rule_Set.T -> unchecked -> Model_Def.i_model -> 'a -> checked

   (*check_TEST is intermediately introduced for step-wise adapting test/* to I_Model.T_TEST

     in parallel to check, and will finally be replaced by check_from_store:*)

   val check_from_store: Proof.context -> Rule_Set.T -> unchecked -> env_subst -> env_eval -> checked

 (*REN check_input: Proof.context -> Rule_Set.T -> unchecked_input -> env_eval -> checked_input*)

   val check_TEST : Proof.context -> Rule_Set.T -> unchecked_TEST  -> env_eval -> checked_TEST

   (*this makes the OLD tests run AFTER introduction of I_Model.T_TEST..*)

   val check_OLD: Proof.context -> Rule_Set.T -> unchecked ->

     Model_Pattern.T * Model_Def.i_model_TEST -> checked

   val eval: Proof.context -> Rule_Set.T -> bool * term -> bool * term

   val feedback_TEST_to_string: Model_Def.i_model_feedback_TEST -> string

   val check_variant_envs: Proof.context -> Rule_Set.T -> unchecked ->

     env_subst -> env_eval -> checked

 (*val sep_variants_envs replaced by of_max_variant       TODO

     for that purpose compare with sep_variants_envs_OLD  TODO*)

   val sep_variants_envs: Model_Pattern.T -> Model_Def.i_model_TEST ->

     ((Model_Def.i_model_TEST * env_subst * env_eval) * Model_Def.variant) list

   val sep_variants_envs_OLD: Model_Pattern.T -> Model_Def.i_model_TEST ->

     env_subst * env_eval;

 (*T_TESTold*)

   val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->

     Model_Def.i_model_TEST * env_subst * env_eval

 (*T_TEST* )

   val of_max_variant:Model_Pattern.T -> Model_Def.i_model_TEST ->

        Model_Def.i_model_TEST * Env.T * (env_subst * env_eval)

 ( *T_TESTnew*)

 (*from isac_test for Minisubpbl*)

   val discern_feedback_subst: Model_Def.descriptor -> Model_Def.i_model_feedback_TEST -> Env.T;

   val discern_type_subst: term * term -> term list -> Env.T;

   val discern_type_eval: Model_Def.descriptor -> term list -> env_eval

   val discern_atoms: term list -> Env.T;

   val mk_env: Model_Def.i_model_feedback_TEST -> Env.T

   val mk_env_subst: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> env_subst

   val mk_env_subst_DEL: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> env_subst

   val mk_env_eval: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> env_eval

   val mk_env_eval_DEL: Model_Def.i_model_single_TEST list -> env_eval

   val arrange_args2: 'a list -> 'b list -> 'c list -> int * 'd list -> (('a * 'b * 'c) * 'd) list

   val filter_variants: (Model_Pattern.single * Model_Def.i_model_single_TEST) list ->

     Model_Def.variant -> (Model_Pattern.single * Model_Def.i_model_single_TEST) list

   val get_equal_descr: Model_Def.i_model_TEST -> Model_Pattern.single ->

     (Model_Pattern.single * Model_Def.i_model_single_TEST) list

   val unchecked_OLD_to_TEST: term list -> (term * Position.T) list

   val filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST

   val arrange_args1: int list -> int * Model_Def.variant list -> (int * Model_Def.variant) list

   val cnt_corrects: Model_Def.i_model_TEST -> int

   val handle_descr_ts: term -> term list -> Env.T

   val distinguish_atoms: term list -> Env.T

 (*REN type_repair_env: Env.T -> Env.T*)

   val repair_env: Env.T -> Env.T

   val all_atoms: term list -> bool

   val all_lhs_atoms: term list -> bool

 \<^isac_test>\<open>  

   val mk_env_model: term -> Model_Def.i_model_feedback_TEST -> Env.T

   val switch_type: Model_Pattern.descriptor -> typ -> Model_Pattern.descriptor

   val discern_typ: term -> Model_Pattern.descriptor * term list ->

     ((term * term) * (term * term)) list

   val discern_feedback: term -> Model_Def.i_model_feedback_TEST ->

     ((term * term) * (term * term)) list

   val make_envs_preconds: (Model_Pattern.single * Model_Def.i_model_single_TEST) list ->

     ((term * term) * (term * term)) list

 \<close>

 end

 (**)

 structure Pre_Conds(**) : PRE_CONDITIONS(**) =

 struct

 (**)

 open Model_Def

 type T = Pre_Conds_Def.T;  (*= (bool * term) list;*)

 type unchecked = term list

 type unchecked_TEST = (term * Position.T) list

 type checked = bool * (bool * term) list

 type checked_TEST = bool * (bool * (term * Position.T)) list

 (* 

   we have three kinds of Env.T in the specification-phase:

 (*1*) Env.T produced by I_Model.of_max_variant and required to create O_Model.T, I_Model.T from

     Model_Pattern.T.

                        Env.T                  / (Constants, fixes)  in Model_Pattern.T

                        e.g.[(fixes, [r = 7])] |

                                               > (Constants, [<r = 7>]) in O/I_Model.T       *)

 (*2*) type env_subst = Env.T (*               / 0 < fixes           in Problem.{where_, ...}

                        eg. [(fixes, r)]       |

                                               > 0 < r *)

 (*3*) type env_eval =  Env.T (*               |

                        eg. [(r, 7)]           |

                                               > 0 < 7 \<longrightarrow> true

   (*1*) is required to produce (*2*) and (*3*); thus respective code is shifted to Pre_Conds.

   (*2*) and (*3*) is produced from I_Model.of_max_variant by restricting to "#Given".

   There is a typing problem, probably to be solved by a language for Specification in the future:

   term <fixes> in (*1*) has type "bool list"

   term <fixes> in (*2*) has type "real". So for the transition from (*1*) to (*2..3*)

     fun switch_type is required.

   The transition requires better modelling by a novel language for Specification.

 *)

 type input = TermC.as_string list;

 fun to_str ctxt (b, t) = pair2str (bool2str b, UnparseC.term ctxt t);

 fun to_string ctxt pres = strs2str' (map (linefeed o (to_str ctxt)) pres);

 fun eval _ _ (false, where_) = (false, where_) (*NOT ALL Free's have been substituted*)

   | eval ctxt where_rls (true, where_) =

     if Rewrite.eval_true ctxt [where_] where_rls

     then (true, where_)

     else (false, where_);

 (** old code before I_Model.T_TEST **)

 (* find most frequent variant v in itms *)

 (* ATTENTION

  * spurios old code

  * misses variants with equal number of items, etc

 *)

 fun variants itms = ((distinct op =) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms;

 (*version without typing problem*)

 fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms);

 fun count_variants vts itms = map (cnt itms) vts;

 fun max2 [] = raise ERROR "max2 of []"

   | max2 (y :: ys) =

     let

       fun mx (a, x) [] = (a, x)

   	    | mx (a, x) ((b, y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;

     in mx y ys end;

 (* get the constant value from a penv *)

 fun getval (id, values) = 

   case values of

 	  [] => raise ERROR ("penv_value: no values in '" ^ UnparseC.term (ContextC.for_ERROR ()) id)

   | [v] => (id, v)

   | (v1 :: v2 :: _) => (case v1 of 

 	      Const (\<^const_name>\<open>Program.Arbfix\<close>, _) => (id, v2)

 	    | _ => (id, v1));

 (* find the variant with most items already input *)

 fun max_variant itms = 

     let val vts = (count_variants (variants itms)) itms;

     in if vts = [] then 0 else (fst o max2) vts end;

 fun mk_e (Cor (_, iv)) = [getval iv]

   | mk_e (Syn _) = []

   | mk_e (Typ _) = [] 

   | mk_e (Inc (_, iv)) = [getval iv]

   | mk_e (Sup _) = []

   | mk_e (Mis _) = []

   | mk_e  _ = raise ERROR "mk_e: uncovered case in fun.def.";

 fun mk_en vt (_, vts, _, _, itm_) = if member op = vts vt then mk_e itm_ else [];

 (* extract the environment from an item list; takes the variant with most items *)

 fun environment itms = 

   let val vt = max_variant itms

   in (flat o (map (mk_en vt))) itms end;

 (** new code for I_Model.T_TEST **)

 fun pen2str ctxt (t, ts) =

   pair2str (UnparseC.term ctxt t, (strs2str' o map (UnparseC.term  ctxt)) ts);

 fun feedback_to_string_TEST ctxt (Cor_TEST ((d, ts), penv)) = 

     "Cor_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv

   | feedback_to_string_TEST _ (Syn_TEST c) =

     "Syn_TEST " ^ c

   | feedback_to_string_TEST ctxt (Inc_TEST ((d, []), _)) = 

     "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, [])) ^ " " ^ 

       Model_Pattern.empty_for d

   | feedback_to_string_TEST ctxt (Inc_TEST ((d, ts), penv)) =

     "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv

   | feedback_to_string_TEST ctxt (Sup_TEST (d, ts)) = 

     "Sup_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))

 fun feedback_TEST_to_string t = feedback_to_string_TEST (ContextC.for_ERROR ()) t;

 (*** make environments for substituting model_pattern+program and for evaluating pre-conditions ***)

 (** OLD make environment for substituting model_pattern+program and pre-conditions **)

 (*val all_atoms_OLD: term list -> bool*)

 fun all_atoms_OLD ts =

   fold (curry and_) (map (fn t => TermC.is_atom (TermC.lhs t)) ts) true

 fun switch_type (Free (id, _)) T = Free (id, T)

   | switch_type t _ = raise TERM ("switch_type not for", [t])

 (*

   this repair is spurious and indicates the need for considering a separate language for Model-ing.

   E.g. "fixes" is used with 2 different types "bool list" and "real" in the problem-definition

     problem pbl_opti_univ : "univariate_calculus/Optimisation" = ..

       Given: "Constants fixes"

       Where: "0 < fixes"

       ...

      (1) Given: Const ("Input_Descript.Constants", "bool list \<Rightarrow> nam") $ Free ("fixes", "bool list")

      (2) Where: Const ("Orderings.ord_class.less", "real \<Rightarrow> real \<Rightarrow> bool") $

            Const ("Groups.zero_class.zero", "real") $ Free ("fixes", "real")

   The intermediately simplistic solution is to build a pair of environments, type env_pair,

   The simplistic design works for the instantiation of the demo-example

     "Constants [r = (7::real)]"

   but it could be extended to instantiations like

       "Constants [a = (1::real), b = (2::real)]"

     with the same Where: "0 < fixes" in the problem-definition

     if indexing / deletion of found elements from the association list is considered.

   For the purpose of future pimprovements a pair of environments, type env_pair, is built;

   where as key of the "outer" environment Free ("fixes", "real" kept to future improvements

   (by indexing "fixes_1", "fixes_2" in case the are more than one element in 

   "Input_Descript.Constants", "bool list..)

 *)

 fun repair_env env = 

   map (fn (id_inst, val_) => (switch_type id_inst (type_of val_), val_)) env

 (* make an Env.T for Prec_Conds.eval *)

 fun mk_env (Model_Def.Cor_TEST ((descr, [ts]), _)) =

     let

     (*val ts = TermC.isalist2list ts*)

       val ts = if TermC.is_list ts then TermC.isalist2list ts else [ts]

     in

       (*compare Model_Pattern.empty_for*)

       case type_of descr of

         (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) (*SideConditions \<longrightarrow> (sideconds, [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2])*)

           => if all_atoms_OLD ts then map (fn t => (TermC.lhs t, TermC.rhs t)) ts else []

       | (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) (*AdditionalValues [u, v]*)

           => []

       | (Type ("HOL.bool", [])) (*Precision (\<epsilon> = 0.01)*)

           => if all_atoms_OLD ts then map (fn t => (TermC.lhs t, TermC.rhs t)) ts else []

       | _ (*Maximum A*) => [(hd ts, TermC.empty (*dummy rhs*))]

     end

   | mk_env (Model_Def.Inc_TEST ((descr, [ts]), _)) =

     let

     (*val ts = TermC.isalist2list ts*)

       val ts = if TermC.is_list ts then TermC.isalist2list ts else [ts]

     in

       (*compare Model_Pattern.empty_for*)

       case type_of descr of

         (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) (*SideConditions \<longrightarrow> (sideconds, [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2])*)

           => if all_atoms_OLD ts then map (fn t => (TermC.lhs t, TermC.rhs t)) ts else []

       | (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) (*AdditionalValues [u, v]*)

           => []

       | (Type ("HOL.bool", [])) (*Precision (\<epsilon> = 0.01)*)

           => if all_atoms_OLD ts then map (fn t => (TermC.lhs t, TermC.rhs t)) ts else []

       | _ (*Maximum A*) => [(hd ts, TermC.empty (*dummy rhs*))]

    end

   | mk_env (Model_Def.Sup_TEST (descr, [ts])) =      

     let

     (*val ts = TermC.isalist2list ts*)

       val ts = if TermC.is_list ts then TermC.isalist2list ts else [ts]

     in

       (*compare Model_Pattern.empty_for*)

       case type_of descr of

         (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) (*SideConditions \<longrightarrow> (sideconds, [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2])*)

           => if all_atoms_OLD ts then map (fn t => (TermC.lhs t, TermC.rhs t)) ts else []

       | (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) (*AdditionalValues [u, v]*)

           => []

       | (Type ("HOL.bool", [])) (*Precision (\<epsilon> = 0.01)*)

           => if all_atoms_OLD ts then map (fn t => (TermC.lhs t, TermC.rhs t)) ts else []

       | _ (*Maximum A*) => [(hd ts, TermC.empty (*dummy rhs*))]

     end

   | mk_env feedb =

     raise ERROR ("mk_env not reasonable for " ^  quote (feedback_TEST_to_string feedb))

 fun mk_env_subst equal_descr_pairs =

   map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))

         => (mk_env feedb) |> map fst (*dummy rhs dropped*)|> map (pair id)) equal_descr_pairs

   |> flat

   |> repair_env

 (*fun mk_env_eval unused? DEL!*)

 fun mk_env_eval equal_descr_pairs =

   map (fn (_, (_, _, _, _, (feedb, _))) => mk_env feedb) equal_descr_pairs

   |> flat

   |> filter_out (fn (_, b) => b = TermC.empty) (*drop pairs with dummy rhs*)

 (*  all_atoms: term list -> bool*)

 fun all_atoms ts =

   fold (curry and_) (map (fn t => TermC.is_atom t) ts) true

 (*  all_lhs_atoms: term list -> bool*)

 fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>

   if can TermC.lhs t then TermC.is_atom (TermC.lhs t) else false) ts) true

 (*  distinguish_atoms: term list -> Env.T*)

 fun distinguish_atoms (*[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2], \<epsilon> = 0.01, [L]*) ts =

   if all_atoms ts

   then map (rpair TermC.empty (*dummy rhs*)) ts

   else if all_lhs_atoms ts

     then map (fn t => (TermC.lhs t, TermC.rhs t)) ts

     else []

 (*  handle_descr_ts: term -> term list -> (term * term) list*)

 fun handle_descr_ts descr ts =

   (*compare Model_Pattern.empty_for*)

   case type_of descr of

     (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) (*(SideConds [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]), [L]*)

       => distinguish_atoms ts

   | (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) (*AdditionalValues [u, v]*)

       => if TermC.is_list (hd ts)

          then [(descr, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.realT)]

          else []

   | (Type ("HOL.bool", [])) (*Precision (\<epsilon> = 0.01)*)

       => distinguish_atoms ts

   | _ (*Maximum A*) => [(hd ts, TermC.empty (*dummy rhs*))]

 (** NEW make environment for substituting program and pre-conditions **)

 fun switch_type (Free (id, _)) T = Free (id, T)

   | switch_type t _ = raise TERM ("switch_type not for", [t])

 fun repair_env env =

   map (fn (id_inst, val_) => (switch_type id_inst (type_of val_), val_)) env

 (*  discern_type_subst: term * term -> term list -> Env.T*)

 fun discern_type_subst (descr, id) ts =

   (*..compare Model_Pattern.empty_for*)

   case type_of descr of 

     (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) (*(SideConds [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]), [L]*)

       => if TermC.is_list (hd ts)

          then [(id, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.boolT)]

          else if length ts = 1 

            then [(id, Library.the_single ts)]

            else raise error "discern_type_subst list bool DESIGN ERROR"

   | (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) (*AdditionalValues [u, v]*)

       => if TermC.is_list (hd ts)

          then [(id, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.realT)]

          else if length ts = 1 

            then [(id, Library.the_single ts)]

            else raise error "discern_type_subst list bool DESIGN ERROR"

   | _ (*Maximum A*) => [(id, Library.the_single ts)] (*if length ts = 1 !*)

 (*  discern_feedback_subst: Model_Def.i_model_feedback_TEST -> Env.T*)

 fun discern_feedback_subst id (Model_Def.Cor_TEST ((descr, [ts]), _)) =

     discern_type_subst (descr, id) [ts]

   | discern_feedback_subst id (Model_Def.Inc_TEST ((descr, [ts]), _)) =

     discern_type_subst (descr, id) [ts]

   | discern_feedback_subst id (Model_Def.Sup_TEST (descr, [ts])) =

     discern_type_subst (descr, id) [ts]

   | discern_feedback_subst id (Model_Def.Cor_TEST ((descr, (*[*)ts(*]*)), _)) =

     discern_type_subst (descr, id) ts

   | discern_feedback_subst _ feedb =

     raise ERROR ("discern_feedback_subst not reasonable for " ^ quote (feedback_TEST_to_string feedb))

 fun mk_env_subst_DEL equal_descr_pairs =

   map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))

         => (discern_feedback_subst id feedb)) equal_descr_pairs

   |> flat

   |> repair_env

 (** NEW make environment for evaluating pre-conditions **)

 (*  all_atoms: term list -> bool*)

 fun all_atoms ts =

   fold (curry and_) (map (fn t => TermC.is_atom t) ts) true

 (*  all_lhs_atoms: term list -> bool*)

 fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>

   if can TermC.lhs t then TermC.is_atom (TermC.lhs t) else false) ts) true

 (*  discern_atoms: term list -> (term * term) list*)

 fun discern_atoms (*[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2], \<epsilon> = 0.01, [L]*) ts =

   if all_atoms ts

   then map (rpair TermC.empty (*dummy rhs*)) ts

   else if all_lhs_atoms ts

     then map (fn t => (TermC.lhs t, TermC.rhs t)) ts

     else []

 fun discern_type_eval descr ts =

   (*..compare Model_Pattern.empty_for*)

   case type_of descr of 

     (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) (*(SideConds [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]), [L]*)

       => discern_atoms ts

   | (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) (*AdditionalValues [u, v]*)

       => discern_atoms ts

   | _ (*Maximum A*) => discern_atoms ts

 fun discern_feedback_eval (Model_Def.Cor_TEST ((descr, [ts]), _)) = discern_type_eval descr [ts]

   | discern_feedback_eval (Model_Def.Inc_TEST ((descr, [ts]), _)) = discern_type_eval descr [ts]

   | discern_feedback_eval (Model_Def.Sup_TEST (descr, [ts])) = discern_type_eval descr [ts]

   | discern_feedback_eval (Model_Def.Cor_TEST ((descr, ts), _)) = discern_type_eval descr ts

   | discern_feedback_eval feedb =

     raise ERROR ("discern_feedback_eval not defined for " ^  quote (feedback_TEST_to_string feedb))

 fun mk_env_eval_DEL i_singles =

   map (fn (_, _, _, _, (feedb, _)) => discern_feedback_eval feedb) i_singles

   |> flat

   |> filter_out (fn (_, b) => b = TermC.empty) (*drop pairs with dummy rhs*)

 (*** old check_variant_envs, sep_variants_envs/_OLD, of_max_variant, check/_TEST/_OLD ***)

 fun check_variant_envs ctxt where_rls pres env_subst env_eval =

   let

     val pres_subst = map (TermC.subst_atomic_all env_subst) pres;

     val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst

     val evals = map (eval ctxt where_rls) full_subst

   in

     (foldl and_ (true, map fst evals), pres_subst)

   end

 (* check_variant_envs for PIDE *)

 fun filter_variants pairs i = 

   filter (fn (_, (_, variants, _, _, _)) => member op= variants i) pairs

 (*get descriptor of those items which can contribute to Subst.T and Env.T *)

 (*  get_dscr: feedback_TEST -> descriptor option*)

 fun get_dscr' (Cor_TEST ((descr, _), _)) = SOME descr

   | get_dscr' (Inc_TEST ((descr, _), _)) = SOME descr

   | get_dscr' (Sup_TEST (descr, _)) = SOME descr

   | get_dscr' _

     (*other feedback cannot contribute to I_Model.mk_env_TEST and Pre_Conds.mk_env_TEST*) = NONE

 (*  get_descr: I_Model.single_TEST -> descriptor option*)

 fun get_descr (_, _, _, _, (feedb, _)) =

   case get_dscr' feedb of NONE => NONE | some_descr => some_descr

 (*  get_equal_descr: I_Model.T_TEST -> Model_Pattern.single ->

     (Model_Pattern.single * I_Model.single_TEST) list*)

 fun get_equal_descr i_model (m_patt_single as (_, (descr, _))) =

   let

     val equal_variants = 

       filter (fn i_single => case get_descr i_single of

           NONE => false (*--------vvvvv*)

         | SOME descr' => descr' = descr) (*probl_POS*) i_model

     in

       (map (pair m_patt_single) equal_variants)

     end

 fun arrange_args2 [] _ _ _(*all have equal length*) = []

   | arrange_args2 (b :: bs) (c :: cs) (d :: ds) (cnt, all) =

     ((b, c, d), nth cnt all) :: (arrange_args2 bs cs ds (cnt + 1, all)) 

   | arrange_args2 _ _ _ _ = raise ERROR "I_Model.arrange_args2 UnequalLengths"

 fun sep_variants_envs model_patt i_model =

   let

     val equal_descr_pairs =

       map (get_equal_descr i_model) model_patt

       |> flat

     val all_variants =

         map (fn (_, (_, variants, _, _, _)) => variants) equal_descr_pairs

         |> flat

         |> distinct op =

     val variants_separated = map (filter_variants equal_descr_pairs) all_variants

     val i_models = map (map snd) variants_separated

     val restricted_to_given = map (filter (fn ((m_field, (_, _)), (_, _, _, _, (_, _))) =>

       m_field = "#Given")) variants_separated

     val envs_subst = map mk_env_subst restricted_to_given

     val envs_eval =  map mk_env_eval restricted_to_given

   in

     arrange_args2 i_models envs_subst envs_eval (1, all_variants)

   end

 (* smash all environments into one; this works only for old test before Maximum-example *)

 fun sep_variants_envs_OLD model_patt i_model =

   let

     val equal_descr_pairs =

       map (get_equal_descr i_model) model_patt

       |> flat

     val all_variants =

         map (fn (_, (_, variants, _, _, _)) => variants) equal_descr_pairs

         |> flat

         |> distinct op =

     val variants_separated = map (filter_variants equal_descr_pairs) all_variants

     val restricted_to_given = map (filter (fn ((m_field, (_, _)), (_, _, _, _, (_, _))) =>

       m_field = "#Given")) variants_separated

     val envs_subst = map mk_env_subst restricted_to_given

     val envs_eval =  map mk_env_eval restricted_to_given

   in

     (flat envs_subst, flat envs_eval)

   end

 (** of_max_variant **)

 (*T_TESTold*)

 (*T_TEST*)

 fun mk_env_model _ (Model_Def.Cor_TEST ((_, []), _)) = []

   | mk_env_model id (Model_Def.Cor_TEST ((descr, ts), _)) = 

     if Model_Pattern.is_list_descr descr 

     then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)]

     else [(id, hd ts)]

   | mk_env_model _ (Model_Def.Syn_TEST _) = [] (*TODO handle correct list elements*)

   | mk_env_model _ (Model_Def.Inc_TEST ((_, []), _)) = []

   | mk_env_model id (Model_Def.Inc_TEST ((descr, ts), _)) = 

     if Model_Pattern.is_list_descr descr 

     then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)]

     else [(id, hd ts)]

   | mk_env_model _ (Model_Def.Sup_TEST _) = []

 fun make_env_model equal_descr_pairs =

   map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))

         => (mk_env_model id feedb)) equal_descr_pairs

   |> flat

 fun switch_type_TEST descr [] = descr

   | switch_type_TEST (Free (id_string, _)) ts =

     Free (id_string, ts |> hd |> TermC.lhs |> type_of)

   | switch_type_TEST descr _ = raise ERROR ("switch_type undefined argument " ^

       quote (UnparseC.term (ContextC.for_ERROR ()) descr))

 fun discern_typ _ (_, []) = []

   | discern_typ id (descr, ts) =

 (*TODO.md "review (descriptor, ts)" REMOVE---------------\*)

     let

       val ts = if Model_Pattern.is_list_descr descr

         then TermC.isalist2list (hd ts)

         else ts

     in

 (*TODO.md "review (descriptor, ts)" REMOVE---------------/*)

   if Model_Pattern.typ_of_element descr = HOLogic.boolT

     andalso ts |> map TermC.lhs |> all_atoms

   then

     if length ts > 1

     then raise ERROR "model items of type 'bool' in lists with 'lengt ts > 1' NOT YET IMPLEMENTED"

     else [((switch_type_TEST id ts, TermC.lhs (hd ts)), 

            (TermC.lhs (hd ts), TermC.rhs (hd ts)))]

   else []

 (*TODO.md "review (descriptor, ts)" REMOVE---------------\*)

     end

 (*TODO.md "review (descriptor, ts)" REMOVE---------------/*)

 fun discern_feedback id (Model_Def.Cor_TEST ((descr, ts), _)) = discern_typ id (descr, ts)

   | discern_feedback _ (Model_Def.Syn_TEST _) = [] (*TODO: handle correct elements*)

   | discern_feedback id (Model_Def.Inc_TEST ((descr, ts), _)) = discern_typ id (descr, ts)

   | discern_feedback _ (Model_Def.Sup_TEST _) = []

 fun make_envs_preconds equal_givens = 

   map (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) equal_givens

   |> flat

 (*T_TESTnew*)

 (*  filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST*)

 fun filter_variants' i_singles n = 

   filter (fn (_, variants, _, _, _) => member op= variants n) i_singles

 (*arrange_args1: int list -> int * Model_Def.variant list -> (int * Model_Def.variant) list*)

 fun arrange_args1 [] _ = []

   | arrange_args1 (sum :: ss) (cnt, all) = (sum, nth cnt all) :: (arrange_args1 ss (cnt + 1, all)) 

 (*cnt_corrects: I_Model.T_TEST -> int*)

 fun cnt_corrects i_model = 

   fold (curry op +) (map (fn (_, _, _, _, (Cor_TEST _, _)) => 1 | _ => 0) i_model) 0;

 (*T_TESTold*)

 fun of_max_variant model_patt i_model =

 (*T_TEST* )

 fun of_max_variant _ [] = ([], [], ([], []))

   | of_max_variant model_patt i_model =

 ( *T_TESTnew*)

  let

     val all_variants =

         map (fn (_, variants, _, _, _) => variants) i_model

         |> flat

         |> distinct op =

     val variants_separated = map (filter_variants' i_model) all_variants

     val sums_corr = map (cnt_corrects) variants_separated

     val sum_variant_s = arrange_args1 sums_corr (1, all_variants)

     val (_, max_variant) = hd (*..crude decision, up to improvement *)

       (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)

     val i_model_max =

       filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model

     val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat

 (*T_TESTold*)

     val env_subst = mk_env_subst_DEL equal_descr_pairs

     val env_eval = mk_env_eval_DEL i_model_max

   in

     (i_model_max, env_subst, env_eval)

   end

 (*T_TEST* )

     val env_model = make_env_model equal_descr_pairs

     val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs

     val subst_eval_list = make_envs_preconds equal_givens

     val (env_subst, env_eval) = split_list subst_eval_list

   in

     (i_model_max, env_model, (env_subst, env_eval))

   end

 ( *T_TESTnew*)

 (** check pre-conditions **)

 (* expects the precondition from Problem, ie. needs substitution *)

 fun check _ _ [] _ _ = (true, [])

   | check ctxt where_rls pres pbl (_ (*I_Model.variants UNNECESSARY: I_Model.T filtered for*)) =

     let

       val env = environment pbl;

       val pres' = map (TermC.subst_atomic_all env) pres;

       val evals = map (eval ctxt where_rls) pres';

     in (foldl and_ (true, map fst evals), evals) end;

 (* expects the precondition from PIDE, ie. already substituted *)

 fun check_TEST _ _ [] _ = (true, [])

   | check_TEST ctxt where_rls preconds env_eval =

     let

       val full_subst =

         map (fn (t, pos) => (subst_atomic env_eval t, pos)) preconds

       val evals =

         map (fn (term, pos) => (Rewrite.eval_true ctxt [term] where_rls, (term, pos))) full_subst

     in

       (foldl and_ (true, map fst evals), (map fst evals) ~~ preconds)

     end;

 fun check_from_store ctxt where_rls pres env_subst env_eval =

   let

     val pres_subst = map (TermC.subst_atomic_all env_subst) pres;

     val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst

     val evals = map (eval ctxt where_rls) full_subst

   in

     (foldl and_ (true, map fst evals), pres_subst)

   end

 (* expects the precondition from Problem, ie. needs substitution *)

 fun check_OLD _ _ [] _  = (true, [])

   | check_OLD ctxt where_rls pres (model_patt, i_model) =

     let

 (*T_TESTold*)

       val (env_subst, env_eval) = sep_variants_envs_OLD model_patt i_model

 (*T_TEST* )

       val (_, _, (env_subst, env_eval)) = of_max_variant model_patt i_model

 ( *T_TESTnew*)

       val pres_subst = map (TermC.subst_atomic_all env_subst) pres;

       val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst

       val evals = map (eval ctxt where_rls) full_subst

     in

       (foldl and_ (true, map fst evals), pres_subst)

     end;

 fun unchecked_OLD_to_TEST pres = map (fn t => (t, Position.none)) pres

 (**)end(**)