(* use this theory for tests before Build_Isac.thy has succeeded *)

theory Test_Theory imports "$ISABELLE_ISAC/Build_Isac"

  "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine"        (* setup for refine.sml   *)

begin                                                                            

ML_file "$ISABELLE_ISAC/BaseDefinitions/libraryC.sml"

section \<open>code for copy & paste ===============================================================\<close>

text \<open>

  declare [[show_types]] 

  declare [[show_sorts]]

  find_theorems "?a <= ?a"

  print_theorems

  print_facts

  print_statement ""

  print_theory

  ML_command \<open>Pretty.writeln prt\<close>

  declare [[ML_print_depth = 999]]

  declare [[ML_exception_trace]]

\<close>

(** )

  (@{print} {a = "dict_cond_ord ([], [])"}; EQUAL)

( **)

ML \<open>

\<close> ML \<open>

"~~~~~ fun xxx , args:"; val () = ();

"~~~~~ and xxx , args:"; val () = ();

"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();

"~~~~~ continue fun xxx"; val () = ();

(*if*) (*then*); (*else*); (*andalso*)  (*case*) (*of*);  (*return value*); (*in*) (*end*);

"xx"

^ "xxx"   (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)

\<close> ML \<open> (*//----------- build fun XXXXX -----------------------------------------------------\\*)

(*//------------------ build fun XXXXX -----------------------------------------------------\\*)

(*\\------------------ build fun XXXXX -----------------------------------------------------//*)

\<close> ML \<open> (*\\----------- build fun XXXXX -----------------------------------------------------//*)

\<close> ML \<open> (*//----------- setup test data for XXXXX -------------------------------------------\\*)

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

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

\<close> ML \<open> (*\\----------- setup test data for XXXXX -------------------------------------------//*)

val return_XXXXX = "XXXXX"

\<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)

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

\<close> ML \<open> (*||----------- contine XXXXX ---------------------------------------------------------*)

(*||------------------ contine XXXXX ---------------------------------------------------------*)

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

\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)

val "XXXXX" = return_XXXXX;

(* final test ... ----------------------------------------------------------------------------*)

\<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)

(*//------------------ inserted hidden code ------------------------------------------------\\*)

(*\\------------------ inserted hidden code ------------------------------------------------//*)

\<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)

\<close> ML \<open>

\<close>

section \<open>===================================================================================\<close>

section \<open>=====  ============================================================================\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

section \<open>===================================================================================\<close>

section \<open>===== --> src/../lucas-interpreter.sml etc ========================================\<close>

ML \<open>

(*T_TESTold*)

(*T_TEST*)

(*T_TESTnew*)

(**)

open Ctree

open Pos;

open TermC;

open Istate;

open Tactic;

open P_Model

open Rewrite;

open Step;

open LItool;

open LI;

open Test_Code

open Specify

(**)

open Model_Def

(**)

open Pre_Conds

(**)

open I_Model

(**)

\<close> ML \<open>

\<close> ML \<open> (*\<longrightarrow> pre_conditions.sml | ? model-def.sml ?*)

fun max_variants i_model =

    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_args sums_corr (1, all_variants)

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

      val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first

        |> map snd

      val option_sequence = map 

        (fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s

(*das ist UNSINN'+ UNNOETIG WEGLASSEN,  .., siehe (*+*)if (pbl_max_imos*)

      val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>

            if is_some pos_in_sum_variant_s then i_model else [])

          (option_sequence ~~ variants_separated)

        |> filter_out (fn place_holder => place_holder = []);

(*/-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------\ * )

      PROBALBY FOR RE-USE:

      val option_sequence = map 

        (fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s

      val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>

            if is_some pos_in_sum_variant_s then i_model else [])

          (option_sequence ~~ variants_separated)

        |> filter_out (fn place_holder => place_holder = []);

      \<longrightarrow> [

           [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])], 

           [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])]]

------   ----------------------------------------------------------------------------------------

      val equal_descr_pairs = map (get_equal_descr (hd max_i_models)) model_patt

        |> flat (*a hack for continuing ------------^^--  "turn to PIDE", works for test example*)

      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

( *\-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *)

    in

      ((maxes, max_i_models)(*, env_model, (env_subst, env_eval)*))

(*     (maxes, max_i_models)*)

(*/-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------\ * )

                             (env_model, (env_subst, env_eval)

( *\--fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *)

    end 

;

(*of_max_variant*)

  max_variants: (*Model_Pattern.T -> *) Model_Def.i_model_TEST ->

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

\<close> ML \<open>

\<close> ML \<open> (*\<longrightarrow> pre-conditions.sml*)

\<close> ML \<open>

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

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

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

  | get_dscr' _ = NONE

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

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

;

get_dscr': feedback_TEST -> descriptor option

\<close> ML \<open>

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

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

;

get_descr: single_TEST -> descriptor option;

\<close> ML \<open>

fun get_descr_vnt descr vnts i_model =

  let

    val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false

      | SOME descr' => if descr = descr' then true else false) i_model 

  in

    case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of

      [] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))

    | items => Library.the_single items (*only applied to model_patt, which has each descr once*)

  end

;

get_descr_vnt: descriptor -> variants -> T_TEST -> single_TEST

\<close> ML \<open>

\<close> ML \<open> (*\<longrightarrow> i-model.sml*)

\<close> ML \<open>

fun transfer_terms (i, vnts, m_field, descr, ts) =

  (i, vnts, true, m_field, (Cor_TEST (descr, ts), Position.none))

;

transfer_terms: O_Model.single -> I_Model.single_TEST

\<close> ML \<open>

(*             

  get an appropriate (description, variant) item from o_model;

  called in case of item in met_imod is_empty_single_TEST

  (i.e. was not transferred pbl_mod by \<open>fun get_descr_vnt\<close>).

*)

fun get_descr_vnt' feedb vnts o_model =

  filter (fn (_, vnts', _, descr', _) =>

    case get_dscr' feedb of

      SOME descr => if descr' = descr andalso inter op= vnts' vnts <> [] then true else false

    | NONE => false) o_model

;

get_descr_vnt': feedback_TEST -> variants -> O_Model.T -> O_Model.T

\<close> ML \<open>

fun msg vnts feedb = "get_descr_vnt' returns NONE: i.e. it does not find an item of o_model with\n" ^

  "variants " ^ ints2str' vnts ^ " and descriptor " ^

  (feedb |> get_dscr' |> the |> UnparseC.term (ContextC.for_ERROR ()))

;

msg: variants -> feedback_TEST -> string

\<close> ML \<open>

fun fill_method o_model pbl_imod met_patt =

  let

    val (pbl_max_vnts, _) = max_variants pbl_imod;

    val from_pbl = map (fn (_, (descr, _)) => get_descr_vnt descr pbl_max_vnts pbl_imod) met_patt

    val from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>

      if is_empty_single_TEST i_single

      then

        case get_descr_vnt' feedb pbl_max_vnts o_model of

            [] => raise ERROR (msg pbl_max_vnts feedb)

          | o_singles => map transfer_terms o_singles

      else [i_single (*fetched before from pbl_imod*)])) from_pbl

  in

    from_o_model |> flat

  end

;

fill_method: O_Model.T -> T_TEST -> Model_Pattern.T -> T_TEST

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open> (* \<longrightarrow> i-model.sml*)

\<close> ML \<open>

fun s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt) =

  let

    val (pbl_max_vnts, _) = Model_Def.max_variants pbl_imod;

    val i_from_pbl = map (fn (_, (descr, _)) =>

      (*Pre_Conds.*)get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt

    val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>

      if is_empty_single_TEST i_single

      then

        case get_descr_vnt' feedb pbl_max_vnts o_model of

            [] => raise ERROR (msg pbl_max_vnts feedb)

          | o_singles => map transfer_terms o_singles

      else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat

    val i_from_met = map (fn (_, (descr, _)) =>

      (*Pre_Conds.*)get_descr_vnt descr pbl_max_vnts met_imod) met_patt

    val (met_max_vnts, _) = Model_Def.max_variants i_from_met;

    val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)

    val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>

      if is_empty_single_TEST i_single

      then

        case get_descr_vnt' feedb [met_max_vnt] o_model of

            [] => raise ERROR (msg [met_max_vnt] feedb)

          | o_singles => map transfer_terms o_singles

      else [i_single (*fetched before from met_imod*)])) i_from_met |> flat

  in

    (pbl_from_o_model, met_from_pbl)

  end

\<close> ML \<open>

;

s_make_complete: O_Model.T -> I_Model.T_TEST * I_Model.T_TEST -> Model_Pattern.T * Model_Pattern.T ->

  I_Model.T_TEST * I_Model.T_TEST

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open> (*\<longrightarrow> lucas-interpreter.sml*)

fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =

  let

    (*done in src*)

  in

    ("ok", Calc.state_empty_post)

  end

;

by_tactic: Tactic.T -> Istate.T * Proof.context -> Calc.T -> string * Calc.state_post

\<close> ML \<open>

\<close>

section \<open>===================================================================================\<close>

section \<open>===== i-model.sml .s_complete =====================================================\<close>

ML \<open>

\<close> ML \<open>

(* most general case: user activates some <complete specification> *)

\<close> ML \<open>

(*---vvvvv these would overwrite above definition ^^^* )

open Ctree

open Pos;

open TermC;

open Istate;

open Tactic;

open P_Model

open Rewrite;

open Step;

open LItool;

open LI;

open Test_Code

open Specify

open Model_Def

open Pre_Conds;

open I_Model;

( **)

val (_(*example text*),

  (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: 

     "Extremum (A = 2 * u * v - u \<up> 2)" :: 

     "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: 

     "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: 

     "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: (*INCORRECT 2 / v*)

(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)

     "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" :: 

     "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::

     "ErrorBound (\<epsilon> = (0::real))" :: []), 

   refs as ("Diff_App", 

     ["univariate_calculus", "Optimisation"],

     ["Optimisation", "by_univariate_calculus"])))

  = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];

val c = [];

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

 Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

\<close> ML \<open>

\<close> ML \<open> (*//----------- setup test data for I_Model.s_make_complete -------------------------\\*)

(*//------------------ setup test data for I_Model.s_make_complete -------------------------\\*)

val (o_model, (pbl_imod, met_imod), (pI, mI)) = case get_obj I pt (fst p) of

   PblObj {meth = met_imod, origin = (o_model, (_, pI, mI), _), probl = pbl_imod, ...}

      => (o_model, (pbl_imod, met_imod), (pI, mI))

       | _ => raise ERROR ""

\<close> ML \<open>

val {model = pbl_patt, ...} = Problem.from_store ctxt pI;

val {model = met_patt, ...} = MethodC.from_store ctxt mI;

\<close> ML \<open>

val pbl_imod = [ (*2 items for creating code ---> variants [1, 2]*)

  (1, [1, 2, 3], true, "#undef", (Cor_TEST (@{term Constants},

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

  (1, [1, 2], true, "#undef", (Cor_TEST (@{term SideConditions},

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

\<close> ML \<open>

val met_imod = [ (*1 item for creating code*)

(8, [2], true, "#undef", (Cor_TEST (@{term FunctionVariable}, [@{term "b::real"}]), Position.none))]

\<close> ML \<open>

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

(*+*)  "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^

(*+*)  "(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n" ^

(*+*)  "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^

(*+*)  "(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^

(*+*)  "(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^

(*+*)  "(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^

(*+*)  "(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n" ^

(*+*)  "(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n" ^

(*+*)  "(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n" ^

(*+*)  "(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^

(*+*)  "(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^

(*+*)  "(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"

then () else error "setup test data for I_Model.s_make_complete CHANGED";

(*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)

\<close> ML \<open> (*\\----------- setup test data for I_Model.s_make_complete -------------------------//*)

\<close> ML \<open>

val return_s_make_complete = 

           s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt);

\<close> ML \<open> (*/------------ step into s_make_complete -------------------------------------------\\*)

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

(*.....~~~ fill_method....*)

"~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt)) =

  (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt));

\<close> ML \<open>

    val (pbl_max_vnts, _) = Model_Def.max_variants pbl_imod;

\<close> ML \<open>

    val i_from_pbl = map (fn (_, (descr, _)) =>

      (*Pre_Conds.*)get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;

\<close> ML \<open> (*//----------- step into get_descr_vnt ---------------------------------------------\\*)

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

"~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =

  (@{term Constants}, pbl_max_vnts, pbl_imod);

\<close> ML \<open>

    val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false

      | SOME descr' => if descr = descr' then true else false) i_model 

\<close> ML \<open>

(*+*)filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr 

(*+*): I_Model.T_TEST

\<close> ML \<open>

val return_get_descr_vnt_1 =

    case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of

      [] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))

    | items => Library.the_single items (*only applied to model_patt, which has each descr once*)

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

\<close> ML \<open> (*\\----------- step into get_descr_vnt ---------------------------------------------//*)

\<close> ML \<open>

\<close> ML \<open> (*|------------ continue s_make_complete ----------------------------------------------*)

(*|------------------- continue s_make_complete ----------------------------------------------*)

\<close> ML \<open>

    val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>

      if is_empty_single_TEST i_single

      then

        case get_descr_vnt' feedb pbl_max_vnts o_model of

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

            [] => raise ERROR (msg pbl_max_vnts feedb)

          | o_singles => map transfer_terms o_singles

      else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat

\<close> ML \<open>

(*+*)val [2, 1] = vnts;

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

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

  "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^

  "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^

  "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^

  "(1, [1, 2], true ,#undef, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"

then () else error "pbl_from_o_model CHANGED"

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open> (*//----------- step into map ((fn i_single -----------------------------------------\\*)

(*//------------------ step into map ((fn i_single -----------------------------------------\\*)

"~~~~~ fun map ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) = (nth 1 i_from_pbl);

      (*if*) is_empty_single_TEST i_single (*else*);

             get_descr_vnt' feedb pbl_max_vnts o_model;

    val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>

      if is_empty_single_TEST i_single

      then

        case get_descr_vnt' feedb pbl_max_vnts o_model of

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

            [] => raise ERROR (msg pbl_max_vnts feedb)

          | o_singles => map transfer_terms o_singles

      else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat

\<close> ML \<open>

\<close> ML \<open> (*\\----------- step into map ((fn i_single -----------------------------------------//*)

(*\\------------------ step into map ((fn i_single -----------------------------------------//*)

\<close> ML \<open> (*|------------ continue s_make_complete ----------------------------------------------*)

(*|------------------- continue s_make_complete ----------------------------------------------*)

\<close> ML \<open>

    val i_from_met = map (fn (_, (descr, _)) =>

      (*Pre_Conds.*)get_descr_vnt descr pbl_max_vnts met_imod) met_patt

\<close> ML \<open>

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

  "(0, [], false ,i_model_empty, (Sup_TEST Constants [], Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_TEST Maximum, Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_TEST Extremum, Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_TEST SideConditions [], Position.T)), \n" ^

  "(8, [2], true ,#undef, (Cor_TEST FunctionVariable b , pen2str, Position.T)), \n" ^

(*---there is 1 item already input -^^^^^^^^^^^^^^^^^^*)

  "(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n" ^

  "(0, [], false ,i_model_empty, (Sup_TEST AdditionalValues [], Position.T))]"

(*+*)then () else error "s_make_complete: from_met CHANGED";

\<close> ML \<open>

    val (met_max_vnts, _) = Model_Def.max_variants i_from_met;

(*+*)val [2] = met_max_vnts

\<close> ML \<open>

    val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)

\<close> ML \<open>

    val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>

      if is_empty_single_TEST i_single

      then

        case get_descr_vnt' feedb [met_max_vnt] o_model of

            [] => raise ERROR (msg [met_max_vnt] feedb)

          | o_singles => map transfer_terms o_singles

      else [i_single (*fetched before from met_imod*)])) i_from_met |> flat

\<close> ML \<open>

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

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

  "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^

  "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^

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

  "(8, [2], true ,#undef, (Cor_TEST FunctionVariable b , pen2str, Position.T)), \n" ^

  "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^

  "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^

  "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"

(*+*)then () else error "s_make_complete: met_from_pbl CHANGED";

\<close> ML \<open>

val return_s_make_complete_step = (pbl_from_o_model, met_from_pbl)

\<close> ML \<open> (*\------------ step into s_make_complete -------------------------------------------//*)

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

if return_s_make_complete = return_s_make_complete_step

then () else error "s_make_complete: stewise construction <> value of fun"

\<close> ML \<open>

\<close>

section \<open>===================================================================================\<close>

section \<open>=====   ===========================================================================\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

end