wneuper/isa: test/Tools/isac/Test_Theory.thy@a4d734f7e02b

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

     2 theory Test_Theory imports "$ISABELLE_ISAC/Build_Isac"

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

     4 begin

     5 ML_file "$ISABELLE_ISAC/BaseDefinitions/libraryC.sml"

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

     8 text \<open>

     9   declare [[show_types]]

    10   declare [[show_sorts]]

    11   find_theorems "?a <= ?a"

    13   print_theorems

    14   print_facts

    15   print_statement ""

    16   print_theory

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

    18   declare [[ML_print_depth = 999]]

    19   declare [[ML_exception_trace]]

    20 \<close>

    21 (** )

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

    23 ( **)

    24 ML \<open>

    25 \<close> ML \<open>

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

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

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

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

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

    31 "xx"

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

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

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

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

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

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

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

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

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

    43 val return_XXXXX = "XXXXX"

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

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

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

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

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

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

    50 val "XXXXX" = return_XXXXX;

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

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

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

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

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

    59 \<close> ML \<open>

    60 \<close>

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

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

    64 ML \<open>

    65 \<close> ML \<open>

    67 \<close> ML \<open>

    68 \<close>

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

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

    72 ML \<open>

    73 (*T_TESTold*)

    74 (*T_TEST*)

    75 (*T_TESTnew*)

    77 (**)

    78 open Ctree

    79 open Pos;

    80 open TermC;

    81 open Istate;

    82 open Tactic;

    83 open P_Model

    84 open Rewrite;

    85 open Step;

    86 open LItool;

    87 open LI;

    88 open Test_Code

    89 open Specify

    90 (**)

    91 open Model_Def

    92 (**)

    93 open Pre_Conds

    94 (**)

    95 open I_Model

    96 (**)

    97 \<close> ML \<open>

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

    99 fun max_variants i_model =

   100     let

   101       val all_variants =

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

   103           |> flat

   104           |> distinct op =

   105       val variants_separated = map (filter_variants' i_model) all_variants

   106       val sums_corr = map (cnt_corrects) variants_separated

   107       val sum_variant_s = arrange_args sums_corr (1, all_variants)

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

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

   111         |> map snd

   112       val option_sequence = map

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

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

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

   116             if is_some pos_in_sum_variant_s then i_model else [])

   117           (option_sequence ~~ variants_separated)

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

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

   120       PROBALBY FOR RE-USE:

   121       val option_sequence = map

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

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

   124             if is_some pos_in_sum_variant_s then i_model else [])

   125           (option_sequence ~~ variants_separated)

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

   127       \<longrightarrow> [

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

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

   130 ------   ----------------------------------------------------------------------------------------

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

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

   133       val env_model = make_env_model equal_descr_pairs

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

   135       val subst_eval_list = make_envs_preconds equal_givens

   136       val (env_subst, env_eval) = split_list subst_eval_list

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

   138     in

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

   140 (*     (maxes, max_i_models)*)

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

   142                              (env_model, (env_subst, env_eval)

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

   144     end

   145 ;

   146 (*of_max_variant*)

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

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

   149 \<close> ML \<open>

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

   151 \<close> ML \<open>

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

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

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

   155   | get_dscr' _ = NONE

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

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

   158 ;

   159 get_dscr': feedback_TEST -> descriptor option

   160 \<close> ML \<open>

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

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

   163 ;

   164 get_descr: single_TEST -> descriptor option;

   166 \<close> ML \<open>

   167 fun get_descr_vnt descr vnts i_model =

   168   let

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

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

   171   in

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

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

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

   175   end

   176 ;

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

   178 \<close> ML \<open>

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

   180 \<close> ML \<open>

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

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

   183 ;

   184 transfer_terms: O_Model.single -> I_Model.single_TEST

   185 \<close> ML \<open>

   186 (*

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

   188   called in case of item in met_imod is_empty_single_TEST

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

   190 *)

   191 fun get_descr_vnt' feedb vnts o_model =

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

   193     case get_dscr' feedb of

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

   195     | NONE => false) o_model

   196 ;

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

   198 \<close> ML \<open>

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

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

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

   202 ;

   203 msg: variants -> feedback_TEST -> string

   204 \<close> ML \<open>

   205 fun fill_method o_model pbl_imod met_patt =

   206   let

   207     val (pbl_max_vnts, _) = max_variants pbl_imod;

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

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

   210       if is_empty_single_TEST i_single

   211       then

   212         case get_descr_vnt' feedb pbl_max_vnts o_model of

   213             [] => raise ERROR (msg pbl_max_vnts feedb)

   214           | o_singles => map transfer_terms o_singles

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

   216   in

   217     from_o_model |> flat

   218   end

   219 ;

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

   221 \<close> ML \<open>

   222 \<close> ML \<open>

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

   224 \<close> ML \<open>

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

   226   let

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

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

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

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

   231       if is_empty_single_TEST i_single

   232       then

   233         case get_descr_vnt' feedb pbl_max_vnts o_model of

   234             [] => raise ERROR (msg pbl_max_vnts feedb)

   235           | o_singles => map transfer_terms o_singles

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

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

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

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

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

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

   244       if is_empty_single_TEST i_single

   245       then

   246         case get_descr_vnt' feedb [met_max_vnt] o_model of

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

   248           | o_singles => map transfer_terms o_singles

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

   250   in

   251     (pbl_from_o_model, met_from_pbl)

   252   end

   253 \<close> ML \<open>

   254 ;

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

   256   I_Model.T_TEST * I_Model.T_TEST

   257 \<close> ML \<open>

   258 \<close> ML \<open>

   259 \<close> ML \<open>

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

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

   262   let

   263     (*done in src*)

   264   in

   265     ("ok", Calc.state_empty_post)

   266   end

   267 ;

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

   269 \<close> ML \<open>

   270 \<close>

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

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

   274 ML \<open>

   275 \<close> ML \<open>

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

   277 \<close> ML \<open>

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

   279 open Ctree

   280 open Pos;

   281 open TermC;

   282 open Istate;

   283 open Tactic;

   284 open P_Model

   285 open Rewrite;

   286 open Step;

   287 open LItool;

   288 open LI;

   289 open Test_Code

   290 open Specify

   291 open Model_Def

   292 open Pre_Conds;

   293 open I_Model;

   294 ( **)

   296 val (_(*example text*),

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

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

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

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

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

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

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

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

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

   306    refs as ("Diff_App",

   307      ["univariate_calculus", "Optimisation"],

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

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

   311 val c = [];

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

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

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

   315 \<close> ML \<open>

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

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

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

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

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

   321        | _ => raise ERROR ""

   322 \<close> ML \<open>

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

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

   325 \<close> ML \<open>

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

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

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

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

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

   331 \<close> ML \<open>

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

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

   334 \<close> ML \<open>

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   351 \<close> ML \<open>

   352 val return_s_make_complete =

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

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

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

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

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

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

   359 \<close> ML \<open>

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

   361 \<close> ML \<open>

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

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

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

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

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

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

   368 \<close> ML \<open>

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

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

   371 \<close> ML \<open>

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

   373 (*+*): I_Model.T_TEST

   374 \<close> ML \<open>

   375 val return_get_descr_vnt_1 =

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

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

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

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

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

   381 \<close> ML \<open>

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

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

   384 \<close> ML \<open>

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

   386       if is_empty_single_TEST i_single

   387       then

   388         case get_descr_vnt' feedb pbl_max_vnts o_model of

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

   390             [] => raise ERROR (msg pbl_max_vnts feedb)

   391           | o_singles => map transfer_terms o_singles

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

   393 \<close> ML \<open>

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

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

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

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

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

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

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

   401 then () else error "pbl_from_o_model CHANGED"

   402 \<close> ML \<open>

   403 \<close> ML \<open>

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

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

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

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

   408              get_descr_vnt' feedb pbl_max_vnts o_model;

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

   411       if is_empty_single_TEST i_single

   412       then

   413         case get_descr_vnt' feedb pbl_max_vnts o_model of

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

   415             [] => raise ERROR (msg pbl_max_vnts feedb)

   416           | o_singles => map transfer_terms o_singles

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

   418 \<close> ML \<open>

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

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

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

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

   424 \<close> ML \<open>

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

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

   427 \<close> ML \<open>

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

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

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

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

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

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

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

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

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

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

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

   439 \<close> ML \<open>

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

   441 (*+*)val [2] = met_max_vnts

   442 \<close> ML \<open>

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

   444 \<close> ML \<open>

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

   446       if is_empty_single_TEST i_single

   447       then

   448         case get_descr_vnt' feedb [met_max_vnt] o_model of

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

   450           | o_singles => map transfer_terms o_singles

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

   452 \<close> ML \<open>

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

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

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

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

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

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

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

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

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

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

   463 \<close> ML \<open>

   464 val return_s_make_complete_step = (pbl_from_o_model, met_from_pbl)

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

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

   467 if return_s_make_complete = return_s_make_complete_step

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

   469 \<close> ML \<open>

   470 \<close>

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

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

   474 ML \<open>

   475 \<close> ML \<open>

   477 \<close> ML \<open>

   478 \<close>

   480 end

author	wneuper <Walther.Neuper@jku.at>
	Wed, 20 Sep 2023 16:51:08 +0200
changeset 60751	a4d734f7e02b
parent 60748	d9bae125ba2a
child 60752	77958bc6ed7d
permissions	-rw-r--r--