(* Title:  "Specify/i-model.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- investigate fun add_single in I_Model ---------------------------------------------";

"----------- build I_Model.init_TEST -----------------------------------------------------------";

"----------- exercise preparing I_Model.is_complete --------------------------------------------";

"----------- build I_Model.is_complete_OLD -----------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

open I_Model;

open Test_Code;

open Tactic;

open Pos;

"----------- investigate fun add_single in I_Model -------------------------------------------";

"----------- investigate fun add_single in I_Model -------------------------------------------";

"----------- investigate fun add_single in I_Model -------------------------------------------";

val f_model = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

	"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",

	"FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

  "AbleitungBiegelinie dy"];

val f_spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);

(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(f_model, f_spec)]; (*\<rightarrow>Model_Problem*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "Traegerlaenge L"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "Streckenlast q_0"*)

(*[], Pbl*)val return_me_Add_Given =

           me nxt p [] pt; (*\<rightarrow>Add_Find "Biegelinie y"*)

(*/------------------- step into me Add_Given ----------------------------------------------\\*)

"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);

val ("ok", (_, _, ptp)) = (*case*)

      Step.by_tactic tac (pt, p) (*of*);

"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));

  val Applicable.Yes tac' = (*case*)

      Step.check tac (pt, p) (*of*);

	    (*if*) Tactic.for_specify' tac' (*then*);

Step_Specify.by_tactic tac' ptp;

"~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);

val ("ok", ([(Add_Given "Streckenlast q_0", _, _)], [], _)) = (*case*)

   Specify.by_Add_ "#Given" ct (pt, p);

"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) =

  ("#Given", ct, (pt, p));

    val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)

    val (i_model, m_patt) =

       if p_ = Pos.Met then

         (met,

           (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)

       else

         (pbl,

           (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)

;

(*+*)if O_Model.to_string @{context} oris = "[\n" ^

  "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

  "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

  "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^

  "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^

  "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"

(*+*)then () else error "INITIAL O_Model CHANGED";

(*+*)if I_Model.to_string ctxt pbl = "[\n" ^

  "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^

  "(2 ,[1] ,false ,#Given ,Inc Streckenlast ,(Streckenlast, [])), \n" ^

  "(3 ,[1] ,false ,#Find ,Inc Biegelinie ,(Biegelinie, [])), \n" ^

  "(4 ,[1] ,false ,#Relate ,Inc Randbedingungen [] ,(Randbedingungen, []))]"

(*+*)then () else error "INITIAL I_Model CHANGED";

val return_check_single = (*case*)

   I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);

(*//------------------ step into check_single ----------------------------------------------\\*)

"~~~~~ fun check_single , args <>[]:"; val (ctxt, m_field, o_model, i_model, m_patt, str)

  = (ctxt, m_field, oris, i_model, m_patt, ct);

      val (t as (descriptor $ _)) = Syntax.read_term ctxt str

        handle ERROR msg => error (msg (*^ Position.here pp*))

val SOME m_field' =

        (*case*) Model_Pattern.get_field descriptor m_patt (*of*);

          (*if*) m_field <> m_field' (*else*);

(**)val ("", ori', all) =(**)

          (*case*) O_Model.contains ctxt m_field o_model t (*of*);

(*+*)O_Model.single_to_string @{context} ori';

(*+*)val [Free ("q_0", _)] = all;

(**)val ("", itm) =(**)

 (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);

(*+*)val (2, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), (Free ("q_q", _), [Free ("q_0", _)]))) = itm

(*\\------------------ step into check_single ----------------------------------------------//*)

val return_check_single = Add itm;

"~~~~~ from fun check_single \<longrightarrow>fun by_Add_ , return:"; val (I_Model.Add i_single) = (return_check_single);

	          val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model

            val tac' = I_Model.make_tactic m_field (ct, i_model')

;

(*+*)if I_Model.to_string ctxt i_model' = "[\n" ^

  "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^

  "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^

  "(3 ,[1] ,false ,#Find ,Inc Biegelinie ,(Biegelinie, [])), \n" ^

  "(4 ,[1] ,false ,#Relate ,Inc Randbedingungen [] ,(Randbedingungen, []))]"

(*+*)then () else error "FINAL I_Model CHANGED";

	          val  (_, _, _, pt') =  Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)

val return_by_Add_ = ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],

              [], (pt', pos)));

(*-------------------- stop into me Add_Given ------------------------------------------------*)

(*\------------------- step into me Add_Given ----------------------------------------------//*)

                                val (p,_,f,nxt,_,pt) = return_me_Add_Given

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]"*)

(* final test ... BEFORE BREAKING ELEMENTWISE INPUT TO LISTS* )

if p = ([], Pbl) then

  case nxt of Add_Relation "Randbedingungen [y 0 = 0]" => () | _

    => error "investigate fun add_single CHANGED 1"

else error "investigate fun add_single CHANGED 2"

( * final test ... AFTER BREAKING ELEMENTWISE INPUT TO LISTS*)

if p = ([], Pbl) then

  case nxt of Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" => () | _

    => error "investigate fun add_single CHANGED 1"

else error "investigate fun add_single CHANGED 2"

"----------- build I_Model.init_TEST -----------------------------------------------------------";

"----------- build I_Model.init_TEST -----------------------------------------------------------";

"----------- build I_Model.init_TEST -----------------------------------------------------------";

(*/---------------------------------------- mimic input from PIDE -----------------------------\*)

(* Test_Example "Diff_App-No.123a" (*complete Model, empty References*) *)

val in_refs as (thy_id, probl_id, meth_id) = ("__", "__/__", "__/__")

val thy = @{theory}

val model_input = (*type Position.T is hidden, thus redefinition*)

 [("#Given", [("Constants [r = 7]", Position.none)]),

  ("#Where", [("0 < r", Position.none)]),

  ("#Find",

   [("Maximum A", Position.none), ("AdditionalValues [u, v]", Position.none)]),

  ("#Relate",

   [("Extremum (A = 2 * u * v - u \<up> 2)", Position.none),

    ("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", Position.none)])]

: (Model_Pattern.m_field * (string * Position.T) list) list

val example_id = "Diff_App-No.123a";

(*----------------------------------------- init state -----------------------------------------*)

set_data CTbasic_TEST.EmptyPtree @{theory Calculation};

(*\---------------------------------------- mimic input from PIDE -----------------------------/*)

val CTbasic_TEST.EmptyPtree =

              (*case*) the_data @{theory Calculation} (*of*);

(* Calculation..*)

"~~~~~ fun init_ctree , args:"; val (thy, example_id) = (thy, example_id);

      val example_id' = References_Def.explode_id example_id

      val (_, (formalise as (model, refs as (thy_id, probl_id, meth_id)))) =

        Store.get (Know_Store.get_expls @{theory}) example_id' example_id' 

      val {model = model_patt, ...} = Problem.from_store (Proof_Context.init_global thy) probl_id

      val (o_model, ctxt) = O_Model.init thy model model_patt

;

(*+*)o_model: O_Model.T; (* |> O_Model.to_string @{context}*)

(*+*)val ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]) =

(*+*)  refs       

      val empty_i_model =

   I_Model.init_TEST o_model model_patt;

"~~~~~ fun init_TEST , args:"; val (ctxt, model_patt) = (ctxt, model_patt);

;

(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [] [__=__, __=__], Position.T))]"

 = I_Model.to_string_TEST @{context} empty_i_model;

"----------- exercise preparing I_Model.is_complete --------------------------------------------";

"----------- exercise preparing I_Model.is_complete --------------------------------------------";

"----------- exercise preparing I_Model.is_complete --------------------------------------------";

fun check str = if str = "true" then true else false

fun complete str = if str = "true" then true else false

val i_model_envs_v = [("i_model_envs-1", 11), ("i_model_envs-2", 12), ("i_model_envs-3", 13)]

val result_all_variants =

  map (fn (a, variant) => if check a andalso complete a then SOME [variant] else NONE) i_model_envs_v;

(*----^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

;

val [NONE, NONE, NONE] = result_all_variants: int list option list

(*+*)val true = forall is_none result_all_variants

val variants_complete =

  if forall is_none result_all_variants

  then NONE

  else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)

;

val NONE = variants_complete: int list option

(*more significant result ..*)

val result_all_variants = [SOME [11], NONE, SOME [13]]: int list option list

(*

in case the result is null, no I_Model is_complete,

in case the result contains more than 1 variant, this might determine the decision for MethodC.

*)

val variants_complete =

  if forall is_none result_all_variants

  then NONE

  else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)

;

val SOME [11, 13] = variants_complete: int list option;

(*/----- reactivate with CS "remove sep_variants_envs"-----\* )

"----------- build I_Model.is_complete_OLD -----------------------------------------------------";

"----------- build I_Model.is_complete_OLD -----------------------------------------------------";

"----------- build I_Model.is_complete_OLD -----------------------------------------------------";

(*see Outer_Syntax:    val (model, where_) = Model_Pattern.parse_pos_empty ctxt model_input*)

open I_Model

open Pre_Conds;

(*//------------------ test data setup -----------------------------------------------------\\*)

(*

*****************************************************************************************

***** WE FIRST MAINTAIN THE ERROR, THAT ITEMS WITH TYPE list ARE STORED AS isalist, *****

***** NOT AS term list (NECESSARY TO DETECT INCOMPLETE INPUT OF lists)              *****

*****************************************************************************************

  The ERROR occurred somewhere since introducing structure or since transition to PIDE.

*****************************************************************************************

  We complete the two single_TEST "1" and "5" below and replace them in  empty_input;

  we add "6" as variant of "5" to the empty input.

  later we shall replace empty_input by partial input "AdditionalValues [v]" (u missing).

  The test intermediatly pairs (feedback_TEST, Position.T) in I_Model.T_TEST 

  and leaves the rest as is.

I_Model.is_complete_OLD: because PIDE gets instantiated Pre_Conds by Template.show,

  I_Model.is_complete_TEST NO instantiation (done in Template.show):

  it serves to maintain the OLD test/*

*)

val thy = @{theory Calculation}

            val state =

              case the_data thy of

                  CTbasic_TEST.EmptyPtree => Preliminary.init_ctree thy example_id

                | _(*state (*FOR TEST*)*) => (**)the_data thy(**)

                  (*let*)

                    val {origin = (o_model, o_ref, _), spec = spec_ref, probl, meth, ctxt, ...} =

                      CTbasic_TEST.get_obj I state [(*Pos will become variable*)] |> CTbasic_TEST.rep_specify_data

;

probl: Model_Def.i_model_TEST 

(*[(1, [1, 2, 3], false, "#Given", (Inp_TEST (Const ("Input_Descript.Constants", "bool list \<Rightarrow> nam"), "[__=__, __=__]"), {})),

   (2, [1, 2, 3], false, "#Find", (Inp_TEST (Const ("Input_Descript.Maximum", "real \<Rightarrow> toreal"), "__"), {})),

   (3, [1, 2, 3], false, "#Find", (Inp_TEST (Const ("Input_Descript.AdditionalValues", "real list \<Rightarrow> toreall"), "[__, __]"), {})),

   (4, [1, 2, 3], false, "#Relate", (Inp_TEST (Const ("Input_Descript.Extremum", "bool \<Rightarrow> toreal"), "(__=__)"), {})),

   (5, [1, 2], false, "#Relate", (Inp_TEST (Const ("Input_Descript.SideConditions", "bool list \<Rightarrow> una"), "[__=__, __=__]"), {}))]*)

;

val probl_POS = (*from above, #1 and #5,6 replaced by complete items for building code.test*)

  (1, [1,2,3], true, "#Given",

    (Cor_TEST ((@{term "Constants"}, [@{term "[r = (7::real)]"(*should be "r = (7::real)"*)}]),

      (@{term "fixes::bool list"}, [@{term "[r = (7::real)]"}])), Position.none )) ::

  nth 2 probl :: nth 3 probl :: nth 4 probl ::

  (5, [1,2], true, "#Relate",

    (Cor_TEST ((@{term "SideConditions"}, [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]),

      (@{term "sideconds::bool list"}, [TermC.empty])), Position.none )) ::

  (6, [3], true, "#Relate",

    (Cor_TEST ((@{term "SideConditions"}, [@{term "[2 * u = r * sin \<alpha>, 2 * v = r * cos \<alpha>]"}]),

      (@{term "sideconds::bool list"}, [TermC.empty])), Position.none ))

  :: [];

val {model = model_patt, where_rls, where_ = where_OLD, ...} = (*from_store without Position.T-vv*)

  Problem.from_store ctxt (References.explode_id "univariate_calculus/Optimisation")

;

val [Const ("Orderings.ord_class.less", _(*"real \<Rightarrow> real \<Rightarrow> bool"*)) $

  Const ("Groups.zero_class.zero", _(*"real"*)) $ Free ("fixes", _(*"real"*))] = where_OLD

(*design-ERROR: "fixes" is used twice, as variable ------^^^^^^^^^^^^^^^^^^^^^^^^^^^ in pre-condition

  AND as "id" in Subst.T [("fixes", [0 < x])] *);

(model_patt |> Model_Pattern.to_string ctxt) =

 "[\"(#Given, (Constants, fixes))\", " ^

  "\"(#Find, (Maximum, maxx))\", " ^

  "\"(#Find, (AdditionalValues, vals))\", " ^

  "\"(#Relate, (Extremum, extr))\", " ^

  "\"(#Relate, (SideConditions, sideconds))\"]";

val "[0 < fixes]" = (where_OLD |> UnparseC.terms @{context})

(*\\------------------ test data setup -----------------------------------------------------//*)

(*/------------------- test on OLD algorithm (with I_Model.T_TEST) --------------------------\*)

;

   I_Model.is_complete_OLD ctxt model_patt where_rls where_OLD probl_POS;

(*//------------------ step into is_complete_OLD -------------------------------------------\\*)

"~~~~~ fun is_complete_OLD , args:"; val (ctxt, model_patt, where_rls, pres, i_model) =

  (ctxt, model_patt, where_rls, where_OLD,

    (** )filter (fn (_, _, _, m_field, _) => m_field = "#Given")( **) probl_POS);

    (*for Pre_Conds.eval we only need ------------------^^^^^^^^, -UNCOMMENT EITHER HER OR THERE-*)

(*+*)val [Const ("Orderings.ord_class.less", _(*"real \<Rightarrow> real \<Rightarrow> bool"*)) $

  Const ("Groups.zero_class.zero", _(*"real"*)) $ Free ("fixes", xxx(*"real"*))] = pres;

(*+*) if I_Model.to_string_TEST @{context} i_model = "[\n" ^

  "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] ,(fixes, [[r = 7]]), Position.T)), \n" ^

  "(2, [1, 2, 3], false ,#Find, (Inp_TEST Maximum __, Position.T)), \n" ^

  "(3, [1, 2, 3], false ,#Find, (Inp_TEST AdditionalValues [__, __], Position.T)), \n" ^

  "(4, [1, 2, 3], false ,#Relate, (Inp_TEST Extremum (__=__), Position.T)), \n" ^

  "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [??.empty]), Position.T)), \n" ^

  "(6, [3], true ,#Relate, (Cor_TEST SideConditions\n [(2::'a) * u = r * sin \<alpha>, (2::'a) * v = r * cos \<alpha>] ,(sideconds, [??.empty]), Position.T))]"

  then () else raise error "I_Model.to_string_TEST i_model CHANGED";

    val no_model_items = length model_patt

(*+*)val 5 = no_model_items;

           sep_variants_envs model_patt i_model;

(*///----------------- step into sep_variants_envs ----------------------------------------\\\*)

(*+*)sep_variants_envs: Model_Pattern.T -> I_Model.T_TEST ->

    ((I_Model.T_TEST * Pre_Conds.env_subst * Pre_Conds.env_eval) * variant) list;

"~~~~~ fun sep_variants_envs , args:"; val (model_patt, i_model) = (model_patt, i_model);

    val equal_descr_pairs =

      map (get_equal_descr i_model) model_patt

      |> flat

(*+*)val

   [(("#Given", (Const ("Input_Descript.Constants", _), Free ("fixes", _))),

     (1, [1, 2, 3], true, "#Given", _)),

(*"#Given"^^^^ would be appropriate for pre-conditions, but kept to build code:...*)

    (("#Relate", (Const ("Input_Descript.SideConditions", _), Free ("sideconds", _))),

     (5, [1, 2], true, "#Relate", _)),

    (("#Relate", (Const ("Input_Descript.SideConditions", _), Free ("sideconds", _))),

     (6, [3], true, "#Relate", _) )] = equal_descr_pairs

    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

  [

   [(("#Given", (Const ("Input_Descript.Constants", _), Free ("fixes", _(*"bool list"*)))),

     (1, [1(*#*), 2, 3], true, "#Given", (Cor_TEST ((Const ("Input_Descript.Constants", _),

       [_ $ (Const ("HOL.eq", _) $ Free ("r", _) $ _) $ _]), _(*eliminate*)), _))),

    (("#Relate", (Const ("Input_Descript.SideConditions", _), Free ("sideconds", _))),

     (5, [1(*#*), 2], true, "#Relate", (Cor_TEST ((Const ("Input_Descript.SideConditions", _),

         [_ $ (_ $ (_ $ (_ $ (_ $ Free ("u", _) $ _) $ _) $ _) $ _) $ _]), _(*eliminate*)), _)))],

   [(("#Given", (Const ("Input_Descript.Constants", _), Free ("fixes", _(*"bool list"*)))),

     (1, [1, 2(*#*), 3], true, "#Given", (Cor_TEST ((Const ("Input_Descript.Constants", _),

         [_ $ (_ $ Free ("r", _) $ _) $ _]), _(*eliminate*)), _))),

    (("#Relate", (Const ("Input_Descript.SideConditions", _), Free ("sideconds", _))),

     (5, [1, 2(*#*)], true, "#Relate", (Cor_TEST ((Const ("Input_Descript.SideConditions", _),

         [_ $ (_ $ (_ $ (_ $ (_ $ Free ("u", _) $ _) $ _) $ _) $ _) $ _]), _(*eliminate*)), _)))],

   [(("#Given", (Const ("Input_Descript.Constants", _), Free ("fixes", _(*"bool list"*)))),

     (1, [1, 2, 3(*#*)], true, "#Given", (Cor_TEST ((Const ("Input_Descript.Constants", _),

       [_ $ (Const ("HOL.eq", _) $ Free ("r", _) $ _) $ _]), _(*eliminate*)), _))),

    (("#Relate", (Const ("Input_Descript.SideConditions", _), Free ("sideconds", _))),

     (6, [3(*#*)], true, "#Relate", (Cor_TEST ((Const ("Input_Descript.SideConditions", _),

       [_ $ (_ $ _ $ (_ $ _ $ (Const ("Transcendental.sin", _) $ Free ("\<alpha>", _)))) $ _]), _), _)))]]

(*+*) = variants_separated (*#*):

   (Model_Pattern.single * single_TEST) list list

    val i_models = map (map snd) variants_separated; (*drop Model_Pattern.T from pair*)

(*+*)i_models: I_Model.T_TEST list;

    val envs_subst = map mk_env_subst variants_separated;

(*+*)envs_subst: Pre_Conds.env_subst list;

    val envs_eval =  map mk_env_eval variants_separated;

(*+*)envs_eval: Pre_Conds.env_subst list;

val return_sep_variants_envs = arrange_args2 i_models envs_subst envs_eval (1, all_variants);

(*+*)return_sep_variants_envs:

   ((I_Model.T_TEST * Pre_Conds.env_subst * Pre_Conds.env_eval) * variant) list;

(*\\\----------------- step into sep_variants_envs ----------------------------------------///*)

(*||------------------ continuing is_complete_OLD --------------------------------------------*)

(*+*)val [[(Free ("fixes", _), Free ("r", _))], (*.. vor 3 variants*)

     [(Free ("fixes", _), Free ("r", _))], 

     [(Free ("fixes", _), Free ("r", _))]] = envs_subst;

(*taken from local environment -----------------------vvvvvvvvvv, ----vvvvvvvvv*)

           check_variant_envs ctxt where_rls pres (hd envs_subst) (hd envs_eval);

(*+*)val (true,

       [(true, Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $

         Free ("r", _))])

        = check_variant_envs ctxt where_rls pres (hd envs_subst) (hd envs_eval);;

(*///----------------- step into check_variant_envs --------------------------------------\\\*)

(*these come in variants..*)

val variant_envs as ((_, env_subst, env_eval), _) = hd return_sep_variants_envs;

(*args of is_complete_OLD -------------------vvvv--vvvvvvvvv--vvvv*)

"~~~~~ fun check_variant_envs , args:"; val (ctxt, where_rls, pres, env_subst, env_eval) =

  (ctxt, where_rls, pres, hd envs_subst, hd envs_eval);

(*+*)val [Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $

      Free ("fixes", _)] = pres

(*+*)val [(Free ("fixes", _),  Free ("r", _))] = env_subst 

(*+*)val [(Free ("r", _), Const ("Num.numeral_class.numeral", _) $ _ )] = env_eval (*env2*)

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

(*+*)val [(true, Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $

      Free ("r", _))] = pres_subst

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

(*+*)val [(true, Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $

       (Const ("Num.numeral_class.numeral", _) $ _ ))] = full_subst

    val evals = map (eval ctxt where_rls) full_subst

(*+*)val [(true,

     Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $

       (Const ("Num.numeral_class.numeral", _) $ _ ))] = evals

(*-------------- fixpoint of foldl -----vvvv*)

val return_check_variant = (foldl and_ (true, map fst evals), pres_subst)

(*+*)val (true, [(true, Const ("Orderings.ord_class.less", _) $

        Const ("Groups.zero_class.zero", _) $ Free ("r", _))]) = return_check_variant

(*\\\----------------- step into check_variant_envs --------------------------------------///*)

(*||------------------ continuing is_complete_OLD --------------------------------------------*)

(*+*)val false = is_complete_variant no_model_items i_model

    val variants_envs = sep_variants_envs model_patt i_model;

(*+*)variants_envs: ((I_Model.T_TEST * Pre_Conds.env_subst * Pre_Conds.env_eval) * variant) list;

    val result_all_variants = map

      (fn ((i_model, env_subst, env_eval), variant) =>

        if fst (check_variant_envs ctxt where_rls pres env_subst env_eval)

          andalso is_complete_variant no_model_items i_model

        then SOME [variant] else NONE) variants_envs;

(*+*)result_all_variants: variant list option list;

(*+*)val [NONE, NONE, NONE] = result_all_variants

    val variants_complete =

      if forall is_none result_all_variants

      then NONE

      else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat);

(*+*)variants_complete: variant list option;

val return_is_complete_OLD = variants_complete;

(*\\------------------ step into into is_complete_OLD --------------------------------------//*)

(*\------------------- test on OLD algorithm (with I_Model.T_TEST) --------------------------/*)

( *\----- reactivate with CS "remove sep_variants_envs"-----/*)