test/Tools/isac/Specify/i-model.sml
author wneuper <Walther.Neuper@jku.at>
Tue, 05 Dec 2023 18:15:45 +0100
changeset 60772 ac0317936138
parent 60771 1b072aab8f4e
child 60773 439e23525491
permissions -rw-r--r--
prepare 1: towards I_Model.T_POS in Specify/ (and no I_Model.T)
walther@59957
     1
(* Title:  "Specify/i-model.sml"
walther@59957
     2
   Author: Walther Neuper
walther@59957
     3
   (c) due to copyright terms
walther@59957
     4
*)
walther@59957
     5
walther@59957
     6
"-----------------------------------------------------------------------------------------------";
walther@59957
     7
"table of contents -----------------------------------------------------------------------------";
walther@59957
     8
"-----------------------------------------------------------------------------------------------";
Walther@60763
     9
"----------- survey on handling of input terms -------------------------------------------------";
walther@59957
    10
"----------- investigate fun add_single in I_Model ---------------------------------------------";
Walther@60771
    11
"----------- build I_Model.init_POS -----------------------------------------------------------";
Walther@60705
    12
"----------- exercise preparing I_Model.is_complete --------------------------------------------";
Walther@60705
    13
"----------- build I_Model.is_complete_OLD -----------------------------------------------------";
Walther@60751
    14
"----------- build I_Model.s_make_complete -----------------------------------------------------";
Walther@60753
    15
"----------- check I_Model.s_make_complete for ([], [])-----------------------------------------";
Walther@60766
    16
"----------- fun item_to_add: Maximum-exammple -------------------------------------------------";
Walther@60766
    17
"----------- fun item_to_add: Biegelinie-example -----------------------------------------------";
walther@59957
    18
"-----------------------------------------------------------------------------------------------";
walther@59957
    19
"-----------------------------------------------------------------------------------------------";
walther@59957
    20
"-----------------------------------------------------------------------------------------------";
walther@59957
    21
walther@59957
    22
open I_Model;
Walther@60705
    23
open Test_Code;
Walther@60705
    24
open Tactic;
Walther@60753
    25
open Pos; 
Walther@60763
    26
open Ctree; 
Walther@60763
    27
open Pre_Conds; 
Walther@60763
    28
open Specify; 
Walther@60763
    29
val ctxt = Proof_Context.init_global @{theory Biegelinie};
Walther@60763
    30
Walther@60763
    31
"----------- survey on handling of input terms -------------------------------------------------";
Walther@60763
    32
"----------- survey on handling of input terms -------------------------------------------------";
Walther@60763
    33
"----------- survey on handling of input terms -------------------------------------------------";
Walther@60763
    34
(*//------------------ survey on handling of input terms in specify-phase ------------------\\*)
Walther@60763
    35
(*        * ---------- handling of lists -----------------------------------------------------*)
Walther@60763
    36
(*         ** ---------- current situation ---------------------------------------------------*)
Walther@60763
    37
(** )(*---- from tests -------------------------------------------vvvvvvv *);
Walther@60763
    38
val o_single as (3, [1, 2, 3], "#Find", descr, [t1, t2]) = (nth 3 o_model)
Walther@60763
    39
val "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"])"
Walther@60763
    40
  = O_Model.single_to_string ctxt o_single
Walther@60763
    41
val "[u]" = UnparseC.term ctxt t1
Walther@60763
    42
val "[v]" = UnparseC.term ctxt t2
Walther@60763
    43
( **)
Walther@60763
    44
val t as (descr $ vals_term) = @{term "AdditionalValues [u, v]"}
Walther@60766
    45
val true = (*if*)Model_Def.is_list_descr descr(*else*);
Walther@60763
    46
Walther@60763
    47
val values = vals_term |> TermC.isalist2list |> map TermC.single_to_list
Walther@60771
    48
val feedb = Cor_POS (descr, values)
Walther@60763
    49
Walther@60771
    50
val "Cor_POS AdditionalValues [u, v] , pen2str" = feedb |> feedback_POS_to_string ctxt
Walther@60763
    51
Walther@60763
    52
(*get values out of feedback:*)
Walther@60763
    53
val [Free ("u", _), Free ("v", _)] = (values |> map TermC.isalist2list  |> flat): term list
Walther@60763
    54
Walther@60763
    55
(*         ** ---------- wanted situation ----------------------------------------------------*)
Walther@60763
    56
val t as (descr $ vals_term) = @{term "AdditionalValues [u, v]"}
Walther@60766
    57
val true = (*if*)Model_Def.is_list_descr descr(*else*);
Walther@60763
    58
Walther@60763
    59
val values = [vals_term]
Walther@60771
    60
val feedb = Cor_POS (descr, values)
Walther@60763
    61
Walther@60771
    62
val "Cor_POS AdditionalValues [u, v] , pen2str" = feedb |> feedback_POS_to_string ctxt (*OK*)
Walther@60763
    63
Walther@60763
    64
(*get values out of feedback:*)
Walther@60763
    65
val "[u, v]" = values |> map (UnparseC.term ctxt) |> hd
Walther@60763
    66
Walther@60763
    67
(*        * ---------- handling of NON-lists -------------------------------------------------*)
Walther@60763
    68
(*         ** ---------- current situation ---------------------------------------------------*)
Walther@60763
    69
(** )(*---- from tests -------------------------------------------vvvvvvv *);
Walther@60763
    70
val o_single as (2, [1, 2, 3], "#Find", Const ("Input_Descript.Maximum", _), [Free ("A", _)])
Walther@60763
    71
  = (nth 2 o_model) 
Walther@60763
    72
( **)
Walther@60763
    73
val t as (descr $ vals_term) = @{term "Maximum A"}
Walther@60766
    74
val false = (*if*)Model_Def.is_list_descr descr(*then*);
Walther@60763
    75
Walther@60763
    76
val values = [vals_term]
Walther@60771
    77
val feedb = Cor_POS (descr, values)
Walther@60763
    78
Walther@60771
    79
val "Cor_POS Maximum A , pen2str" = feedb |> feedback_POS_to_string ctxt (*OK*)
Walther@60763
    80
Walther@60763
    81
(*get values out of feedback:*)
Walther@60763
    82
val "A" = values |> map (UnparseC.term ctxt) |> hd
Walther@60763
    83
Walther@60763
    84
(*         ** ---------- wanted situation ----------------------------------------------------*)
Walther@60763
    85
val t as (descr $ vals_term) = @{term "Maximum A"}
Walther@60766
    86
val false = (*if*)Model_Def.is_list_descr descr(*then*);
Walther@60763
    87
Walther@60763
    88
val values = [vals_term]
Walther@60771
    89
val feedb = Cor_POS (descr, values)
Walther@60763
    90
Walther@60771
    91
val "Cor_POS Maximum A , pen2str" = feedb |> feedback_POS_to_string ctxt (*OK*)
Walther@60763
    92
Walther@60763
    93
(*get values out of feedback:*)
Walther@60763
    94
val "A" = values |> map (UnparseC.term ctxt) |> hd;
Walther@60763
    95
(*\\------------------ survey on handling of input terms in specify-phase ------------------//*)
Walther@60763
    96
Walther@60729
    97
walther@59957
    98
"----------- investigate fun add_single in I_Model -------------------------------------------";
walther@59957
    99
"----------- investigate fun add_single in I_Model -------------------------------------------";
walther@59957
   100
"----------- investigate fun add_single in I_Model -------------------------------------------";
walther@59997
   101
val f_model = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
walther@59957
   102
	"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
walther@59957
   103
	"FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
walther@59957
   104
  "AbleitungBiegelinie dy"];
walther@59957
   105
val f_spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
Walther@60571
   106
(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(f_model, f_spec)]; (*\<rightarrow>Model_Problem*)
walther@59957
   107
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "Traegerlaenge L"*)
walther@59957
   108
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "Streckenlast q_0"*)
walther@59957
   109
Walther@60676
   110
(*[], Pbl*)val return_me_Add_Given =
Walther@60676
   111
           me nxt p [] pt; (*\<rightarrow>Add_Find "Biegelinie y"*)
Walther@60676
   112
(*/------------------- step into me Add_Given ----------------------------------------------\\*)
walther@59957
   113
"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
walther@59957
   114
Walther@60676
   115
val ("ok", (_, _, ptp)) = (*case*)
walther@59957
   116
      Step.by_tactic tac (pt, p) (*of*);
walther@59957
   117
"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
Walther@60676
   118
walther@59957
   119
  val Applicable.Yes tac' = (*case*)
walther@59957
   120
      Step.check tac (pt, p) (*of*);
walther@59957
   121
	    (*if*) Tactic.for_specify' tac' (*then*);
walther@59957
   122
walther@59957
   123
Step_Specify.by_tactic tac' ptp;
walther@59957
   124
"~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);
walther@59957
   125
Walther@60676
   126
val ("ok", ([(Add_Given "Streckenlast q_0", _, _)], [], _)) = (*case*)
walther@60016
   127
   Specify.by_Add_ "#Given" ct (pt, p);
Walther@60676
   128
"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) =
walther@59957
   129
  ("#Given", ct, (pt, p));
Walther@60676
   130
    val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
Walther@60676
   131
    val (i_model, m_patt) =
Walther@60676
   132
       if p_ = Pos.Met then
Walther@60676
   133
         (met,
Walther@60676
   134
           (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
Walther@60676
   135
       else
Walther@60676
   136
         (pbl,
Walther@60676
   137
           (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
Walther@60676
   138
;
Walther@60655
   139
(*+*)if O_Model.to_string @{context} oris = "[\n" ^
walther@59997
   140
  "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
walther@59997
   141
  "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
walther@59997
   142
  "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
walther@59997
   143
  "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
walther@59997
   144
  "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
walther@59997
   145
  "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
walther@59997
   146
  "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
walther@59957
   147
(*+*)then () else error "INITIAL O_Model CHANGED";
walther@59957
   148
(*+*)if I_Model.to_string ctxt pbl = "[\n" ^
Walther@60739
   149
  "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
Walther@60739
   150
  "(2 ,[1] ,false ,#Given ,Inc Streckenlast , pen2str), \n" ^
Walther@60739
   151
  "(3 ,[1] ,false ,#Find ,Inc Biegelinie , pen2str), \n" ^
Walther@60739
   152
  "(4 ,[1] ,false ,#Relate ,Inc Randbedingungen [] , pen2str)]"
walther@59957
   153
(*+*)then () else error "INITIAL I_Model CHANGED";
walther@59957
   154
Walther@60676
   155
val return_check_single = (*case*)
Walther@60676
   156
   I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
Walther@60676
   157
(*//------------------ step into check_single ----------------------------------------------\\*)
Walther@60676
   158
"~~~~~ fun check_single , args <>[]:"; val (ctxt, m_field, o_model, i_model, m_patt, str)
Walther@60676
   159
  = (ctxt, m_field, oris, i_model, m_patt, ct);
Walther@60676
   160
      val (t as (descriptor $ _)) = Syntax.read_term ctxt str
Walther@60676
   161
        handle ERROR msg => error (msg (*^ Position.here pp*))
Walther@60676
   162
val SOME m_field' =
Walther@60676
   163
        (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
Walther@60676
   164
          (*if*) m_field <> m_field' (*else*);
Walther@60676
   165
walther@59957
   166
(**)val ("", ori', all) =(**)
Walther@60469
   167
          (*case*) O_Model.contains ctxt m_field o_model t (*of*);
walther@59957
   168
Walther@60655
   169
(*+*)O_Model.single_to_string @{context} ori';
walther@59957
   170
(*+*)val [Free ("q_0", _)] = all;
walther@59957
   171
walther@59957
   172
(**)val ("", itm) =(**)
Walther@60772
   173
 (*case*) is_notyet_input ctxt (OLD_to_POS i_model) all ori' m_patt (*of*);
walther@59957
   174
Walther@60772
   175
(*+*)val (2, [1], true, "#Given", (Cor_POS (Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), _)) = itm
Walther@60676
   176
(*\\------------------ step into check_single ----------------------------------------------//*)
Walther@60676
   177
val return_check_single = Add itm;
walther@59957
   178
Walther@60676
   179
"~~~~~ from fun check_single \<longrightarrow>fun by_Add_ , return:"; val (I_Model.Add i_single) = (return_check_single);
Walther@60772
   180
	          val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt)
Walther@60772
   181
	            (I_Model.TEST_to_OLD_single i_single) i_model
Walther@60676
   182
            val tac' = I_Model.make_tactic m_field (ct, i_model')
Walther@60676
   183
;
Walther@60676
   184
(*+*)if I_Model.to_string ctxt i_model' = "[\n" ^
Walther@60739
   185
  "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
Walther@60739
   186
  "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
Walther@60739
   187
  "(3 ,[1] ,false ,#Find ,Inc Biegelinie , pen2str), \n" ^
Walther@60739
   188
  "(4 ,[1] ,false ,#Relate ,Inc Randbedingungen [] , pen2str)]"
walther@59957
   189
(*+*)then () else error "FINAL I_Model CHANGED";
walther@59957
   190
Walther@60676
   191
	          val  (_, _, _, pt') =  Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
walther@59957
   192
Walther@60676
   193
val return_by_Add_ = ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],
Walther@60676
   194
              [], (pt', pos)));
Walther@60676
   195
(*-------------------- stop into me Add_Given ------------------------------------------------*)
Walther@60676
   196
(*\------------------- step into me Add_Given ----------------------------------------------//*)
Walther@60763
   197
                                val (p,_,f,nxt,_,pt) = return_me_Add_Given;
walther@59957
   198
Walther@60763
   199
(*ErRoR Clash of types "_ \<Rightarrow> _" and "_ list", Randbedingungen :: bool list \<Rightarrow> una, y :: real \<Rightarrow> real* )
Walther@60676
   200
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]"*)
walther@59957
   201
Walther@60729
   202
(* final test ... BEFORE BREAKING ELEMENTWISE INPUT TO LISTS* )
walther@59957
   203
if p = ([], Pbl) then
Walther@60729
   204
  case nxt of Add_Relation "Randbedingungen [y 0 = 0]" => () | _
Walther@60729
   205
    => error "investigate fun add_single CHANGED 1"
Walther@60729
   206
else error "investigate fun add_single CHANGED 2"
Walther@60729
   207
( * final test ... AFTER BREAKING ELEMENTWISE INPUT TO LISTS*)
Walther@60729
   208
if p = ([], Pbl) then
Walther@60729
   209
  case nxt of Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" => () | _
Walther@60729
   210
    => error "investigate fun add_single CHANGED 1"
walther@59957
   211
else error "investigate fun add_single CHANGED 2"
Walther@60763
   212
( *ErRoR Clash of types "_ \<Rightarrow> _" and "_ list", Randbedingungen :: bool list \<Rightarrow> una, y :: real \<Rightarrow> real*)
Walther@60763
   213
Walther@60690
   214
Walther@60771
   215
"----------- build I_Model.init_POS -----------------------------------------------------------";
Walther@60771
   216
"----------- build I_Model.init_POS -----------------------------------------------------------";
Walther@60771
   217
"----------- build I_Model.init_POS -----------------------------------------------------------";
Walther@60690
   218
(*/---------------------------------------- mimic input from PIDE -----------------------------\*)
Walther@60690
   219
Walther@60690
   220
(* Test_Example "Diff_App-No.123a" (*complete Model, empty References*) *)
Walther@60690
   221
val in_refs as (thy_id, probl_id, meth_id) = ("__", "__/__", "__/__")
Walther@60690
   222
val thy = @{theory}
Walther@60690
   223
val model_input = (*type Position.T is hidden, thus redefinition*)
Walther@60690
   224
 [("#Given", [("Constants [r = 7]", Position.none)]),
Walther@60690
   225
  ("#Where", [("0 < r", Position.none)]),
Walther@60690
   226
  ("#Find",
Walther@60690
   227
   [("Maximum A", Position.none), ("AdditionalValues [u, v]", Position.none)]),
Walther@60690
   228
  ("#Relate",
Walther@60690
   229
   [("Extremum (A = 2 * u * v - u \<up> 2)", Position.none),
Walther@60690
   230
    ("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", Position.none)])]
Walther@60690
   231
: (Model_Pattern.m_field * (string * Position.T) list) list
Walther@60690
   232
val example_id = "Diff_App-No.123a";
Walther@60690
   233
(*----------------------------------------- init state -----------------------------------------*)
Walther@60771
   234
set_data CTbasic_POS.EmptyPtree @{theory Calculation};
Walther@60690
   235
(*\---------------------------------------- mimic input from PIDE -----------------------------/*)
Walther@60690
   236
Walther@60771
   237
val CTbasic_POS.EmptyPtree =
Walther@60694
   238
              (*case*) the_data @{theory Calculation} (*of*);
Walther@60690
   239
Walther@60690
   240
(* Calculation..*)
Walther@60704
   241
"~~~~~ fun init_ctree , args:"; val (thy, example_id) = (thy, example_id);
Walther@60690
   242
      val example_id' = References_Def.explode_id example_id
Walther@60690
   243
      val (_, (formalise as (model, refs as (thy_id, probl_id, meth_id)))) =
Walther@60690
   244
        Store.get (Know_Store.get_expls @{theory}) example_id' example_id' 
Walther@60690
   245
      val {model = model_patt, ...} = Problem.from_store (Proof_Context.init_global thy) probl_id
Walther@60690
   246
      val (o_model, ctxt) = O_Model.init thy model model_patt
Walther@60690
   247
;
Walther@60690
   248
(*+*)o_model: O_Model.T; (* |> O_Model.to_string @{context}*)
Walther@60690
   249
(*+*)val ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]) =
Walther@60695
   250
(*+*)  refs       
Walther@60690
   251
Walther@60694
   252
      val empty_i_model =
Walther@60771
   253
   I_Model.init_POS ctxt o_model model_patt;
Walther@60771
   254
"~~~~~ fun init_POS , args:"; val (ctxt, model_patt) = (ctxt, model_patt);
Walther@60694
   255
;
Walther@60771
   256
(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_POS Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]"
Walther@60771
   257
 = I_Model.to_string_POS @{context} empty_i_model;
Walther@60705
   258
Walther@60705
   259
Walther@60705
   260
"----------- exercise preparing I_Model.is_complete --------------------------------------------";
Walther@60705
   261
"----------- exercise preparing I_Model.is_complete --------------------------------------------";
Walther@60705
   262
"----------- exercise preparing I_Model.is_complete --------------------------------------------";
Walther@60705
   263
fun check str = if str = "true" then true else false
Walther@60705
   264
fun complete str = if str = "true" then true else false
Walther@60705
   265
Walther@60705
   266
val i_model_envs_v = [("i_model_envs-1", 11), ("i_model_envs-2", 12), ("i_model_envs-3", 13)]
Walther@60705
   267
Walther@60705
   268
val result_all_variants =
Walther@60705
   269
  map (fn (a, variant) => if check a andalso complete a then SOME [variant] else NONE) i_model_envs_v;
Walther@60705
   270
(*----^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
Walther@60705
   271
;
Walther@60705
   272
val [NONE, NONE, NONE] = result_all_variants: int list option list
Walther@60705
   273
Walther@60705
   274
(*+*)val true = forall is_none result_all_variants
Walther@60705
   275
Walther@60705
   276
val variants_complete =
Walther@60705
   277
  if forall is_none result_all_variants
Walther@60705
   278
  then NONE
Walther@60705
   279
  else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)
Walther@60705
   280
;
Walther@60705
   281
val NONE = variants_complete: int list option
Walther@60705
   282
Walther@60705
   283
Walther@60705
   284
(*more significant result ..*)
Walther@60705
   285
val result_all_variants = [SOME [11], NONE, SOME [13]]: int list option list
Walther@60705
   286
(*
Walther@60705
   287
in case the result is null, no I_Model is_complete,
Walther@60705
   288
in case the result contains more than 1 variant, this might determine the decision for MethodC.
Walther@60705
   289
*)
Walther@60705
   290
val variants_complete =
Walther@60705
   291
  if forall is_none result_all_variants
Walther@60705
   292
  then NONE
Walther@60705
   293
  else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)
Walther@60705
   294
;
Walther@60705
   295
val SOME [11, 13] = variants_complete: int list option;
Walther@60705
   296
Walther@60714
   297
(*/----- reactivate with CS "remove sep_variants_envs"-----\* )
Walther@60705
   298
"----------- build I_Model.is_complete_OLD -----------------------------------------------------";
Walther@60705
   299
"----------- build I_Model.is_complete_OLD -----------------------------------------------------";
Walther@60705
   300
"----------- build I_Model.is_complete_OLD -----------------------------------------------------";
Walther@60705
   301
(*see Outer_Syntax:    val (model, where_) = Model_Pattern.parse_pos_empty ctxt model_input*)
Walther@60705
   302
open I_Model
Walther@60705
   303
open Pre_Conds;
Walther@60705
   304
(*//------------------ test data setup -----------------------------------------------------\\*)
Walther@60705
   305
(*
Walther@60705
   306
*****************************************************************************************
Walther@60705
   307
***** WE FIRST MAINTAIN THE ERROR, THAT ITEMS WITH TYPE list ARE STORED AS isalist, *****
Walther@60705
   308
***** NOT AS term list (NECESSARY TO DETECT INCOMPLETE INPUT OF lists)              *****
Walther@60705
   309
*****************************************************************************************
Walther@60705
   310
  The ERROR occurred somewhere since introducing structure or since transition to PIDE.
Walther@60705
   311
*****************************************************************************************
Walther@60771
   312
  We complete the two single_POS "1" and "5" below and replace them in  empty_input;
Walther@60705
   313
  we add "6" as variant of "5" to the empty input.
Walther@60705
   314
  later we shall replace empty_input by partial input "AdditionalValues [v]" (u missing).
Walther@60771
   315
  The test intermediatly pairs (feedback_POS, Position.T) in I_Model.T_POS 
Walther@60705
   316
  and leaves the rest as is.
Walther@60705
   317
Walther@60705
   318
I_Model.is_complete_OLD: because PIDE gets instantiated Pre_Conds by Template.show,
Walther@60771
   319
  I_Model.is_complete_POS NO instantiation (done in Template.show):
Walther@60705
   320
  it serves to maintain the OLD test/*
Walther@60705
   321
*)
Walther@60705
   322
val thy = @{theory Calculation}
Walther@60705
   323
Walther@60705
   324
            val state =
Walther@60705
   325
              case the_data thy of
Walther@60771
   326
                  CTbasic_POS.EmptyPtree => Preliminary.init_ctree thy example_id
Walther@60705
   327
                | _(*state (*FOR TEST*)*) => (**)the_data thy(**)
Walther@60705
   328
                  (*let*)
Walther@60705
   329
                    val {origin = (o_model, o_ref, _), spec = spec_ref, probl, meth, ctxt, ...} =
Walther@60771
   330
                      CTbasic_POS.get_obj I state [(*Pos will become variable*)] |> CTbasic_POS.rep_specify_data
Walther@60705
   331
;
Walther@60771
   332
probl: Model_Def.i_model_POS 
Walther@60771
   333
(*[(1, [1, 2, 3], false, "#Given", (Inp_POS (Const ("Input_Descript.Constants", "bool list \<Rightarrow> nam"), "[__=__, __=__]"), {})),
Walther@60771
   334
   (2, [1, 2, 3], false, "#Find", (Inp_POS (Const ("Input_Descript.Maximum", "real \<Rightarrow> toreal"), "__"), {})),
Walther@60771
   335
   (3, [1, 2, 3], false, "#Find", (Inp_POS (Const ("Input_Descript.AdditionalValues", "real list \<Rightarrow> toreall"), "[__, __]"), {})),
Walther@60771
   336
   (4, [1, 2, 3], false, "#Relate", (Inp_POS (Const ("Input_Descript.Extremum", "bool \<Rightarrow> toreal"), "(__=__)"), {})),
Walther@60771
   337
   (5, [1, 2], false, "#Relate", (Inp_POS (Const ("Input_Descript.SideConditions", "bool list \<Rightarrow> una"), "[__=__, __=__]"), {}))]*)
Walther@60705
   338
;
Walther@60705
   339
val probl_POS = (*from above, #1 and #5,6 replaced by complete items for building code.test*)
Walther@60705
   340
  (1, [1,2,3], true, "#Given",
Walther@60771
   341
    (Cor_POS ((@{term "Constants"}, [@{term "[r = (7::real)]"(*should be "r = (7::real)"*)}]),
Walther@60705
   342
      (@{term "fixes::bool list"}, [@{term "[r = (7::real)]"}])), Position.none )) ::
Walther@60705
   343
  nth 2 probl :: nth 3 probl :: nth 4 probl ::
Walther@60705
   344
  (5, [1,2], true, "#Relate",
Walther@60771
   345
    (Cor_POS ((@{term "SideConditions"}, [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]),
Walther@60705
   346
      (@{term "sideconds::bool list"}, [TermC.empty])), Position.none )) ::
Walther@60705
   347
  (6, [3], true, "#Relate",
Walther@60771
   348
    (Cor_POS ((@{term "SideConditions"}, [@{term "[2 * u = r * sin \<alpha>, 2 * v = r * cos \<alpha>]"}]),
Walther@60705
   349
      (@{term "sideconds::bool list"}, [TermC.empty])), Position.none ))
Walther@60705
   350
  :: [];
Walther@60705
   351
Walther@60705
   352
val {model = model_patt, where_rls, where_ = where_OLD, ...} = (*from_store without Position.T-vv*)
Walther@60705
   353
  Problem.from_store ctxt (References.explode_id "univariate_calculus/Optimisation")
Walther@60705
   354
;
Walther@60705
   355
val [Const ("Orderings.ord_class.less", _(*"real \<Rightarrow> real \<Rightarrow> bool"*)) $
Walther@60705
   356
  Const ("Groups.zero_class.zero", _(*"real"*)) $ Free ("fixes", _(*"real"*))] = where_OLD
Walther@60705
   357
(*design-ERROR: "fixes" is used twice, as variable ------^^^^^^^^^^^^^^^^^^^^^^^^^^^ in pre-condition
Walther@60705
   358
  AND as "id" in Subst.T [("fixes", [0 < x])] *);
Walther@60705
   359
(model_patt |> Model_Pattern.to_string ctxt) =
Walther@60705
   360
 "[\"(#Given, (Constants, fixes))\", " ^
Walther@60705
   361
  "\"(#Find, (Maximum, maxx))\", " ^
Walther@60705
   362
  "\"(#Find, (AdditionalValues, vals))\", " ^
Walther@60705
   363
  "\"(#Relate, (Extremum, extr))\", " ^
Walther@60705
   364
  "\"(#Relate, (SideConditions, sideconds))\"]";
Walther@60705
   365
val "[0 < fixes]" = (where_OLD |> UnparseC.terms @{context})
Walther@60705
   366
(*\\------------------ test data setup -----------------------------------------------------//*)
Walther@60705
   367
Walther@60771
   368
(*/------------------- test on OLD algorithm (with I_Model.T_POS) --------------------------\*)
Walther@60771
   369
(*\------------------- test on OLD algorithm (with I_Model.T_POS) --------------------------/*)
Walther@60714
   370
( *\----- reactivate with CS "remove sep_variants_envs"-----/*)
Walther@60751
   371
Walther@60751
   372
Walther@60751
   373
"----------- build I_Model.s_make_complete -----------------------------------------------------";
Walther@60751
   374
"----------- build I_Model.s_make_complete -----------------------------------------------------";
Walther@60751
   375
"----------- build I_Model.s_make_complete -----------------------------------------------------";
Walther@60751
   376
val (_(*example text*),
Walther@60751
   377
  (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: 
Walther@60751
   378
     "Extremum (A = 2 * u * v - u \<up> 2)" :: 
Walther@60751
   379
     "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: 
Walther@60751
   380
     "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: 
Walther@60751
   381
     "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: (*INCORRECT 2 / v*)
Walther@60751
   382
(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
Walther@60751
   383
     "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" :: 
Walther@60751
   384
     "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
Walther@60751
   385
     "ErrorBound (\<epsilon> = (0::real))" :: []), 
Walther@60751
   386
   refs as ("Diff_App", 
Walther@60751
   387
     ["univariate_calculus", "Optimisation"],
Walther@60751
   388
     ["Optimisation", "by_univariate_calculus"])))
Walther@60751
   389
  = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
Walther@60751
   390
Walther@60751
   391
val c = [];
Walther@60751
   392
val (p,_,f,nxt,_,pt) = 
Walther@60751
   393
 Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
Walther@60751
   394
val (p,_,f,nxt,_,pt) = me nxt p c pt;
Walther@60751
   395
Walther@60751
   396
(*//------------------ setup test data for I_Model.s_make_complete -------------------------\\*)
Walther@60751
   397
val (o_model, (pbl_imod, met_imod), (pI, mI)) = case get_obj I pt (fst p) of
Walther@60751
   398
   PblObj {meth = met_imod, origin = (o_model, (_, pI, mI), _), probl = pbl_imod, ...}
Walther@60751
   399
      => (o_model, (pbl_imod, met_imod), (pI, mI))
Walther@60751
   400
       | _ => raise ERROR ""
Walther@60751
   401
Walther@60751
   402
val pbl_imod = [ (*2 items for creating code ---> variants [1, 2]*)
Walther@60771
   403
  (1, [1, 2, 3], true, "#undef", (Cor_POS (@{term Constants},
Walther@60751
   404
    [@{term "[r = (7::real)]"}]), Position.none)),
Walther@60771
   405
  (1, [1, 2], true, "#undef", (Cor_POS (@{term SideConditions},
Walther@60751
   406
    [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]), Position.none))]
Walther@60751
   407
Walther@60751
   408
val met_imod = [ (*1 item for creating code*)
Walther@60771
   409
(8, [2], true, "#undef", (Cor_POS (@{term FunctionVariable}, [@{term "b::real"}]), Position.none))]
Walther@60751
   410
;
Walther@60751
   411
(*+*)if (o_model |> O_Model.to_string @{context}) = "[\n" ^
Walther@60751
   412
(*+*)  "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
Walther@60751
   413
(*+*)  "(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n" ^
Walther@60751
   414
(*+*)  "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
Walther@60751
   415
(*+*)  "(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
Walther@60751
   416
(*+*)  "(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
Walther@60751
   417
(*+*)  "(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
Walther@60751
   418
(*+*)  "(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n" ^
Walther@60751
   419
(*+*)  "(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n" ^
Walther@60751
   420
(*+*)  "(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n" ^
Walther@60751
   421
(*+*)  "(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
Walther@60751
   422
(*+*)  "(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
Walther@60751
   423
(*+*)  "(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
Walther@60751
   424
then () else error "setup test data for I_Model.s_make_complete CHANGED";
Walther@60751
   425
(*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)
Walther@60751
   426
Walther@60751
   427
val return_s_make_complete =
Walther@60757
   428
           s_make_complete ctxt o_model (pbl_imod, met_imod) (pI, mI);
Walther@60751
   429
(*/------------------- step into s_make_complete -------------------------------------------\\*)
Walther@60757
   430
"~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pI, mI)) =
Walther@60757
   431
  (o_model, (pbl_imod, met_imod), (pI, mI));
Walther@60757
   432
    val {model = pbl_patt, ...} = Problem.from_store ctxt pI;
Walther@60757
   433
    val {model = met_patt, ...} = MethodC.from_store ctxt mI;
Walther@60752
   434
    val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
Walther@60751
   435
    val i_from_pbl = map (fn (_, (descr, _)) =>
Walther@60751
   436
      Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
Walther@60751
   437
Walther@60751
   438
(*//------------------ step into get_descr_vnt ---------------------------------------------\\*)
Walther@60751
   439
"~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =
Walther@60751
   440
  (@{term Constants}, pbl_max_vnts, pbl_imod);
Walther@60767
   441
    val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr_opt feedb of NONE => false
Walther@60751
   442
      | SOME descr' => if descr = descr' then true else false) i_model 
Walther@60751
   443
;
Walther@60771
   444
(*+*)filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr: I_Model.T_POS
Walther@60751
   445
;
Walther@60751
   446
val return_get_descr_vnt_1 =
Walther@60751
   447
    case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
Walther@60771
   448
      [] => (0, [], false, "i_model_empty", (Sup_POS (descr, []), Position.none))
Walther@60751
   449
    | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
Walther@60751
   450
(*\\------------------ step into get_descr_vnt ---------------------------------------------//*)
Walther@60751
   451
Walther@60751
   452
(*|------------------- continue s_make_complete ----------------------------------------------*)
Walther@60751
   453
    val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
Walther@60771
   454
      if is_empty_single_POS i_single
Walther@60751
   455
      then
Walther@60751
   456
        case get_descr_vnt' feedb pbl_max_vnts o_model of
Walther@60751
   457
(*-----------^^^^^^^^^^^^^^-----------------------------*)
Walther@60751
   458
            [] => raise ERROR (msg pbl_max_vnts feedb)
Walther@60751
   459
          | o_singles => map transfer_terms o_singles
Walther@60751
   460
      else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
Walther@60751
   461
Walther@60751
   462
(*+*)val [2, 1] = vnts;
Walther@60771
   463
(*+*)if (pbl_from_o_model |> I_Model.to_string_POS @{context}) = "[\n" ^
Walther@60771
   464
  "(1, [1, 2, 3], true ,#undef, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n" ^
Walther@60771
   465
  "(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n" ^
Walther@60771
   466
  "(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
Walther@60771
   467
  "(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
Walther@60771
   468
  "(1, [1, 2], true ,#undef, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
Walther@60757
   469
then () else error "pbl_from_o_model CHANGED 1"
Walther@60751
   470
Walther@60751
   471
(*//------------------ step into map ((fn i_single -----------------------------------------\\*)
Walther@60751
   472
"~~~~~ fun map ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) = (nth 1 i_from_pbl);
Walther@60771
   473
      (*if*) is_empty_single_POS i_single (*else*);
Walther@60751
   474
             get_descr_vnt' feedb pbl_max_vnts o_model;
Walther@60751
   475
Walther@60751
   476
    val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
Walther@60771
   477
      if is_empty_single_POS i_single
Walther@60751
   478
      then
Walther@60751
   479
        case get_descr_vnt' feedb pbl_max_vnts o_model of
Walther@60751
   480
(*---------- ^^^^^^^^^^^^^^ ----------------------------*)
Walther@60751
   481
            [] => raise ERROR (msg pbl_max_vnts feedb)
Walther@60751
   482
          | o_singles => map transfer_terms o_singles
Walther@60751
   483
      else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
Walther@60751
   484
(*\\------------------ step into map ((fn i_single -----------------------------------------//*)
Walther@60751
   485
Walther@60751
   486
(*|------------------- continue s_make_complete ----------------------------------------------*)
Walther@60751
   487
    val i_from_met = map (fn (_, (descr, _)) =>
Walther@60753
   488
      Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
Walther@60751
   489
;
Walther@60771
   490
(*+*)if (i_from_met |> I_Model.to_string_POS @{context}) = "[\n" ^
Walther@60771
   491
  "(0, [], false ,i_model_empty, (Sup_POS Constants [], Position.T)), \n" ^
Walther@60771
   492
  "(0, [], false ,i_model_empty, (Sup_POS Maximum, Position.T)), \n" ^
Walther@60771
   493
  "(0, [], false ,i_model_empty, (Sup_POS Extremum, Position.T)), \n" ^
Walther@60771
   494
  "(0, [], false ,i_model_empty, (Sup_POS SideConditions [], Position.T)), \n" ^
Walther@60771
   495
  "(8, [2], true ,#undef, (Cor_POS FunctionVariable b , pen2str, Position.T)), \n" ^
Walther@60751
   496
(*---there is 1 item already input -^^^^^^^^^^^^^^^^^^*)
Walther@60771
   497
  "(0, [], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n" ^
Walther@60771
   498
  "(0, [], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n" ^
Walther@60771
   499
  "(0, [], false ,i_model_empty, (Sup_POS AdditionalValues [], Position.T))]"
Walther@60751
   500
(*+*)then () else error "s_make_complete: from_met CHANGED";
Walther@60751
   501
;
Walther@60752
   502
    val met_max_vnts = Model_Def.max_variants o_model i_from_met;
Walther@60751
   503
(*+*)val [2] = met_max_vnts
Walther@60751
   504
Walther@60751
   505
    val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)
Walther@60751
   506
    val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
Walther@60771
   507
      if is_empty_single_POS i_single
Walther@60751
   508
      then
Walther@60751
   509
        case get_descr_vnt' feedb [met_max_vnt] o_model of
Walther@60751
   510
            [] => raise ERROR (msg [met_max_vnt] feedb)
Walther@60751
   511
          | o_singles => map transfer_terms o_singles
Walther@60751
   512
      else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
Walther@60751
   513
;
Walther@60771
   514
(*+*)if (met_from_pbl |> I_Model.to_string_POS @{context}) = "[\n" ^
Walther@60771
   515
  "(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n" ^
Walther@60771
   516
  "(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n" ^
Walther@60771
   517
  "(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
Walther@60771
   518
  "(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
Walther@60771
   519
  "(8, [2], true ,#undef, (Cor_POS FunctionVariable b , pen2str, Position.T)), \n" ^
Walther@60771
   520
  "(10, [1, 2], true ,#undef, (Cor_POS Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
Walther@60771
   521
  "(12, [1, 2, 3], true ,#undef, (Cor_POS ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
Walther@60771
   522
  "(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
Walther@60751
   523
(*+*)then () else error "s_make_complete: met_from_pbl CHANGED";
Walther@60751
   524
;
Walther@60751
   525
val return_s_make_complete_step = (pbl_from_o_model, met_from_pbl)
Walther@60751
   526
(*\------------------- step into s_make_complete -------------------------------------------//*)
Walther@60751
   527
;
Walther@60751
   528
if return_s_make_complete = return_s_make_complete_step
Walther@60751
   529
then () else error "s_make_complete: stewise construction <> value of fun"
Walther@60753
   530
Walther@60753
   531
Walther@60753
   532
"----------- check I_Model.s_make_complete for ([], [])-----------------------------------------";
Walther@60753
   533
"----------- check I_Model.s_make_complete for ([], [])-----------------------------------------";
Walther@60753
   534
"----------- check I_Model.s_make_complete for ([], [])-----------------------------------------";
Walther@60753
   535
val (_(*example text*),
Walther@60753
   536
  (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: 
Walther@60753
   537
     "Extremum (A = 2 * u * v - u \<up> 2)" :: 
Walther@60753
   538
     "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: 
Walther@60753
   539
     "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" :: 
Walther@60753
   540
     "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: (*INCORRECT 2 / v*)
Walther@60753
   541
(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
Walther@60753
   542
     "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" :: 
Walther@60753
   543
     "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
Walther@60753
   544
     "ErrorBound (\<epsilon> = (0::real))" :: []), 
Walther@60753
   545
   refs as ("Diff_App", 
Walther@60753
   546
     ["univariate_calculus", "Optimisation"],
Walther@60753
   547
     ["Optimisation", "by_univariate_calculus"])))
Walther@60753
   548
  = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
Walther@60753
   549
Walther@60753
   550
val c = [];
Walther@60753
   551
val (p,_,f,nxt,_,pt) = 
Walther@60753
   552
 Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
Walther@60753
   553
val (p,_,f,nxt,_,pt) = me nxt p c pt;
Walther@60753
   554
Walther@60753
   555
(*//------------------ setup test data for I_Model.s_make_complete -------------------------\\*)
Walther@60753
   556
val (o_model, (pI, mI)) = case get_obj I pt (fst p) of
Walther@60753
   557
   PblObj {origin = (o_model, (_, pI, mI), _), ...}
Walther@60753
   558
      => (o_model, (pI, mI))
Walther@60753
   559
       | _ => raise ERROR ""
Walther@60753
   560
Walther@60753
   561
val pbl_imod = []
Walther@60753
   562
val met_imod = []
Walther@60753
   563
;
Walther@60753
   564
(*+*)if (o_model |> O_Model.to_string @{context}) = "[\n" ^
Walther@60753
   565
(*+*)  "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
Walther@60753
   566
(*+*)  "(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n" ^
Walther@60753
   567
(*+*)  "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
Walther@60753
   568
(*+*)  "(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
Walther@60753
   569
(*+*)  "(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
Walther@60753
   570
(*+*)  "(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
Walther@60753
   571
(*+*)  "(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n" ^
Walther@60753
   572
(*+*)  "(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n" ^
Walther@60753
   573
(*+*)  "(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n" ^
Walther@60753
   574
(*+*)  "(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
Walther@60753
   575
(*+*)  "(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
Walther@60753
   576
(*+*)  "(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
Walther@60753
   577
then () else error "setup test data for I_Model.s_make_complete CHANGED";
Walther@60753
   578
(*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)
Walther@60753
   579
Walther@60753
   580
val return_s_make_complete =
Walther@60757
   581
           s_make_complete ctxt o_model (pbl_imod, met_imod) (pI, mI);
Walther@60753
   582
(*/------------------- step into s_make_complete -------------------------------------------\\*)
Walther@60753
   583
"~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt)) =
Walther@60753
   584
  (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt));
Walther@60753
   585
    val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
Walther@60753
   586
Walther@60753
   587
    val i_from_pbl = map (fn (_, (descr, _)) =>
Walther@60753
   588
      Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
Walther@60753
   589
(*//------------------ step into get_descr_vnt ---------------------------------------------\\*)
Walther@60753
   590
"~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =
Walther@60753
   591
  (@{term Constants}, pbl_max_vnts, pbl_imod);
Walther@60771
   592
    val equal_descr(*for (*+*)filter (fn (_, vnts',..*): I_Model.T_POS =
Walther@60767
   593
                      filter (fn (_, _, _, _, (feedb, _)) => case get_dscr_opt feedb of NONE => false
Walther@60753
   594
      | SOME descr' => if descr = descr' then true else false) i_model 
Walther@60753
   595
;
Walther@60771
   596
(*+*)filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) (equal_descr: I_Model.T_POS)
Walther@60771
   597
(*+*): I_Model.T_POS
Walther@60753
   598
;
Walther@60753
   599
val return_get_descr_vnt_1 =
Walther@60753
   600
    case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
Walther@60771
   601
      [] => (0, [], false, "i_model_empty", (Sup_POS (descr, []), Position.none))
Walther@60753
   602
    | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
Walther@60753
   603
(*\\------------------ step into get_descr_vnt ---------------------------------------------//*)
Walther@60753
   604
;
Walther@60753
   605
(*+*)if return_get_descr_vnt_1 = nth 1 i_from_pbl
Walther@60753
   606
(*+*)then () else error "return_get_descr_vnt_1 <> nth 1 i_from_pbl";
Walther@60771
   607
(*+*)if (i_from_pbl |> I_Model.to_string_POS @{context}) = "[\n" ^
Walther@60771
   608
  "(0, [], false ,i_model_empty, (Sup_POS Constants [], Position.T)), \n" ^
Walther@60771
   609
  "(0, [], false ,i_model_empty, (Sup_POS Maximum, Position.T)), \n" ^
Walther@60771
   610
  "(0, [], false ,i_model_empty, (Sup_POS AdditionalValues [], Position.T)), \n" ^
Walther@60771
   611
  "(0, [], false ,i_model_empty, (Sup_POS Extremum, Position.T)), \n" ^
Walther@60771
   612
  "(0, [], false ,i_model_empty, (Sup_POS SideConditions [], Position.T))]"
Walther@60753
   613
(*+*)then () else error "I_Model.s_make_complete > i_from_pbl CHANGED";
Walther@60753
   614
Walther@60753
   615
(*|------------------- continue s_make_complete ----------------------------------------------*)
Walther@60753
   616
    val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
Walther@60771
   617
      if is_empty_single_POS i_single
Walther@60753
   618
      then
Walther@60753
   619
        case get_descr_vnt' feedb pbl_max_vnts o_model of
Walther@60753
   620
(*-----------^^^^^^^^^^^^^^-----------------------------*)
Walther@60753
   621
            [] => raise ERROR (msg pbl_max_vnts feedb)
Walther@60753
   622
          | o_singles => map transfer_terms o_singles
Walther@60753
   623
      else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
Walther@60753
   624
Walther@60753
   625
(*+*)val [1, 2, 3] = vnts;
Walther@60771
   626
(*+*)if (pbl_from_o_model |> I_Model.to_string_POS @{context}) = "[\n" ^
Walther@60771
   627
  "(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n" ^
Walther@60771
   628
  "(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n" ^
Walther@60771
   629
  "(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
Walther@60771
   630
  "(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
Walther@60771
   631
  "(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
Walther@60771
   632
  "(6, [3], true ,#Relate, (Cor_POS SideConditions [u / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>] , pen2str, Position.T))]"
Walther@60757
   633
then () else error "pbl_from_o_model CHANGED 2"
Walther@60753
   634
Walther@60753
   635
(*//------------------ step into map ((fn i_single -----------------------------------------\\*)
Walther@60753
   636
"~~~~~ fun map nth 1 ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) =
Walther@60753
   637
  (nth 1 i_from_pbl);
Walther@60771
   638
      (*if*) is_empty_single_POS i_single (*then*);
Walther@60753
   639
  (*case*) get_descr_vnt' feedb pbl_max_vnts o_model;
Walther@60753
   640
Walther@60771
   641
(*+*)val (0, [], false, "i_model_empty", (Sup_POS (Const ("Input_Descript.Constants", _), []), _))
Walther@60753
   642
  = i_single
Walther@60771
   643
(*+*)val true = is_empty_single_POS i_single
Walther@60753
   644
Walther@60753
   645
val return_get_descr_vnt'= (*case*)
Walther@60753
   646
           get_descr_vnt' feedb pbl_max_vnts o_model (*of*);
Walther@60753
   647
(*\\------------------ step into map ((fn i_single -----------------------------------------//*)
Walther@60753
   648
Walther@60753
   649
(*|------------------- continue s_make_complete ----------------------------------------------*)
Walther@60753
   650
    val i_from_met = map (fn (_, (descr, _)) =>
Walther@60753
   651
      Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
Walther@60753
   652
Walther@60753
   653
(*+*)val [1, 2, 3] = pbl_max_vnts (*..? ? GOON*);
Walther@60771
   654
(*+*)if (i_from_met |> I_Model.to_string_POS @{context}) = "[\n" ^
Walther@60771
   655
  "(0, [], false ,i_model_empty, (Sup_POS Constants [], Position.T)), \n" ^
Walther@60771
   656
  "(0, [], false ,i_model_empty, (Sup_POS Maximum, Position.T)), \n" ^
Walther@60771
   657
  "(0, [], false ,i_model_empty, (Sup_POS Extremum, Position.T)), \n" ^
Walther@60771
   658
  "(0, [], false ,i_model_empty, (Sup_POS SideConditions [], Position.T)), \n" ^
Walther@60771
   659
  "(0, [], false ,i_model_empty, (Sup_POS FunctionVariable, Position.T)), \n" ^
Walther@60771
   660
  "(0, [], false ,i_model_empty, (Sup_POS Input_Descript.Domain, Position.T)), \n" ^
Walther@60771
   661
  "(0, [], false ,i_model_empty, (Sup_POS ErrorBound, Position.T)), \n" ^
Walther@60771
   662
  "(0, [], false ,i_model_empty, (Sup_POS AdditionalValues [], Position.T))]"
Walther@60753
   663
(*+*)then () else error "s_make_complete: i_from_met CHANGED";
Walther@60753
   664
Walther@60753
   665
    val met_max_vnts = Model_Def.max_variants o_model i_from_met;
Walther@60753
   666
(*+*)val [1, 2, 3]: variant list = met_max_vnts
Walther@60753
   667
Walther@60753
   668
    val max_vnt = hd met_max_vnts (*need only one for solve-phase*)
Walther@60753
   669
    val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
Walther@60771
   670
      if is_empty_single_POS i_single
Walther@60753
   671
      then
Walther@60753
   672
        case get_descr_vnt' feedb [max_vnt] o_model of
Walther@60753
   673
            [] => raise ERROR (msg [max_vnt] feedb)
Walther@60753
   674
          | o_singles => map transfer_terms o_singles
Walther@60753
   675
      else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
Walther@60753
   676
Walther@60753
   677
(*+*)val 1 = max_vnt;
Walther@60771
   678
(*+*)if (met_from_pbl |> I_Model.to_string_POS @{context}) = "[\n" ^
Walther@60771
   679
  "(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n" ^
Walther@60771
   680
  "(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n" ^
Walther@60771
   681
  "(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
Walther@60771
   682
  "(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
Walther@60771
   683
  "(7, [1], true ,#undef, (Cor_POS FunctionVariable a , pen2str, Position.T)), \n" ^
Walther@60771
   684
  "(10, [1, 2], true ,#undef, (Cor_POS Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
Walther@60771
   685
  "(12, [1, 2, 3], true ,#undef, (Cor_POS ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
Walther@60771
   686
  "(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
Walther@60753
   687
(*+*)then () else error "s_make_complete: met_from_pbl CHANGED";
Walther@60753
   688
Walther@60753
   689
val return_s_make_complete_step as (pbl_imod_step, met_imod_step)=
Walther@60753
   690
    (filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) pbl_from_o_model,
Walther@60753
   691
      met_from_pbl);
Walther@60753
   692
(*\------------------- step into s_make_complete -------------------------------------------//*)
Walther@60753
   693
if return_s_make_complete = return_s_make_complete_step
Walther@60753
   694
then () else error "s_make_complete: stewise construction <> value of fun"
Walther@60753
   695
;
Walther@60753
   696
(* final test ... ----------------------------------------------------------------------------*)
Walther@60771
   697
val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
Walther@60771
   698
 = pbl_imod_step |> I_Model.to_string_POS @{context}
Walther@60771
   699
val "[\n(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_POS Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_POS Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(7, [1], true ,#undef, (Cor_POS FunctionVariable a , pen2str, Position.T)), \n(10, [1, 2], true ,#undef, (Cor_POS Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n(12, [1, 2, 3], true ,#undef, (Cor_POS ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_POS AdditionalValues [u, v] , pen2str, Position.T))]"
Walther@60771
   700
 = met_imod_step |> I_Model.to_string_POS @{context};
Walther@60763
   701
Walther@60766
   702
Walther@60766
   703
Walther@60766
   704
(*** fun item_to_add: Maximum-example ====================================================== ***);
Walther@60766
   705
"----------- fun item_to_add: Maximum-example --------------------------------------------------";
Walther@60766
   706
"----------- fun item_to_add: Maximum-example --------------------------------------------------";
Walther@60763
   707
(*//------------------ setup test data for item_to_add Maximum-exammple --------------------\\*)
Walther@60763
   708
(*
Walther@60763
   709
(*+*)val "[\n
Walther@60763
   710
  (1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n
Walther@60763
   711
  (2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n
Walther@60763
   712
  (3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n
Walther@60763
   713
  (4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n
Walther@60763
   714
  (5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n
Walther@60763
   715
  (7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n
Walther@60763
   716
  (10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n
Walther@60763
   717
  (12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
Walther@60763
   718
 = o_model |> O_Model.to_string ctxt
Walther@60763
   719
Walther@60763
   720
val true = o_model_test = o_model
Walther@60763
   721
*)
Walther@60763
   722
val ctxt = @{context}
Walther@60763
   723
Walther@60763
   724
val o_model_test = [
Walther@60763
   725
  (1, [1, 2, 3], "#Given",  @{term Constants},        [@{term "[r = (7::real)]"}]),
Walther@60763
   726
  (2, [1, 2, 3], "#Find",   @{term Maximum},          [@{term "A::real"}            ]),
Walther@60763
   727
  (3, [1, 2, 3], "#Find",   @{term AdditionalValues}, [@{term "[u::real]"}, @{term "[v::real]"}]),
Walther@60763
   728
  (4, [1, 2, 3], "#Relate", @{term Extremum},         [@{term "A = 2 * u * v - u \<up> 2"}]),
Walther@60763
   729
  (5, [1, 2],    "#Relate", @{term SideConditions},   [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]),
Walther@60763
   730
  (7, [1],       "#undef",  @{term FunctionVariable}, [@{term "a::real"}]),
Walther@60763
   731
  (10,[1, 2],    "#undef",  @{term Domain},           [@{term "{0<..<(r::real)}"}]),
Walther@60763
   732
  (12,[1, 2, 3], "#undef",  @{term ErrorBound},       [@{term "\<epsilon> = (0::real)"}]),
Walther@60763
   733
  (0, [1],       "#Find",   @{term solutions},        [@{term "L::real list"}])
Walther@60763
   734
];
Walther@60763
   735
(*\\------------------ setup test data for item_to_add Maximum-exammple --------------------//*)
Walther@60763
   736
Walther@60766
   737
(** fun item_to_add: Constants [r = (7::real)] ============================================== **);
Walther@60771
   738
val i_single : I_Model.single_POS =
Walther@60771
   739
((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term Constants}, []) , Position.none)))
Walther@60763
   740
val SOME ("#Given", "Constants [r = 7]") = item_to_add ctxt o_model_test [i_single];
Walther@60763
   741
Walther@60766
   742
(** fun item_to_add: Maximum A ============================================================== **);
Walther@60771
   743
val i_single : I_Model.single_POS =
Walther@60771
   744
((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term Maximum}, []) , Position.none)))
Walther@60763
   745
val SOME ("#Find", "Maximum A") = item_to_add ctxt o_model_test [i_single];
Walther@60763
   746
Walther@60766
   747
(** fun item_to_add: AdditionalValues [u] =================================================== **);
Walther@60771
   748
val i_single : I_Model.single_POS =
Walther@60771
   749
((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term AdditionalValues}, []) , Position.none)))
Walther@60763
   750
val SOME ("#Find", "AdditionalValues [u]") = item_to_add ctxt o_model_test [i_single];
Walther@60763
   751
Walther@60766
   752
(** fun item_to_add: AdditionalValues [u, v] ================================================ **);
Walther@60771
   753
val i_single : I_Model.single_POS =
Walther@60771
   754
((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term AdditionalValues}, [@{term "[u::real]"}]) , Position.none)))
Walther@60763
   755
(**)val SOME ("#Find", "AdditionalValues [u, v]") = item_to_add ctxt o_model_test [i_single];
Walther@60763
   756
Walther@60766
   757
(** fun item_to_add: AdditionalValues [v, u] ================================================ **);
Walther@60763
   758
(*/------------------- fun item_to_add: AdditionalValues [v, u] ----------------------------\\*)
Walther@60771
   759
val i_single : I_Model.single_POS =
Walther@60763
   760
(*present [v, u] (reverse order), because second element has been input first ------vvvvvvvvvv*)
Walther@60771
   761
((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term AdditionalValues}, [@{term "[v::real]"}]) , Position.none)))
Walther@60763
   762
Walther@60763
   763
(**)val return_item_to_add as SOME ("#Find", "AdditionalValues [v, u]") = (**)
Walther@60763
   764
(** )val calling_code as SOME ("#Find", "AdditionalValues [v, u]") =( **)
Walther@60763
   765
           item_to_add ctxt o_model_test [i_single];
Walther@60763
   766
(*//------------------ step into item_to_add -----------------------------------------------\\*)
Walther@60763
   767
"~~~~~ fun item_to_add , args:"; val (ctxt, o_model, i_model) = (ctxt, o_model_test, [i_single]);
Walther@60766
   768
    val max_vnt as 1 = last_elem (*this decides, for which variant initially help is given*)
Walther@60763
   769
      (Model_Def.max_variants o_model i_model)
Walther@60763
   770
    val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
Walther@60763
   771
    val i_to_select = i_model
Walther@60771
   772
      |> filter_out (fn (_, vnts, _, _, (I_Model.Cor_POS _, _)) => member op= vnts max_vnt | _ => false)
Walther@60763
   773
      |> select_inc_lists
Walther@60766
   774
    (*in*)
Walther@60771
   775
(*+*)val "[\n(3, [1, 2, 3], false ,from o_model, (Inc_POS AdditionalValues [v] , pen2str, Position.T))]"
Walther@60771
   776
 = i_to_select |> I_Model.to_string_POS ctxt
Walther@60771
   777
(*+*)val [(_, _, _, _, (Inc_POS (_, [Const ("List.list.Cons", _) $ Free ("v", _) $ _]), _))]
Walther@60766
   778
 = i_to_select
Walther@60763
   779
Walther@60763
   780
val false =
Walther@60763
   781
    (*if*) i_to_select = []
Walther@60763
   782
Walther@60766
   783
(** )val return_item_to_add =( **)
Walther@60766
   784
(**)val return_fill_from_o as
Walther@60771
   785
      SOME (_, _, _, _, (Cor_POS (Const ("Input_Descript.AdditionalValues", _), xxx), _)) =(**)
Walther@60763
   786
(*I_Model.*)fill_from_o o_vnts (hd i_to_select) (*of*);
Walther@60763
   787
(*///----------------- step into fill_from_o -----------------------------------------------\\*)
Walther@60763
   788
"~~~~~ fun fill_from_o , args:"; val (o_model, (i, vnts, bool, _, (feedb, pos))) =
Walther@60763
   789
  (o_vnts, (hd i_to_select));
Walther@60763
   790
    val (m_field, all_value) =
Walther@60767
   791
      case find_first (fn (_, _, _, descr', _) => Model_Def.descriptor_exists descr' feedb) o_model of
Walther@60763
   792
        SOME (_, _, m_field, _, ts) =>  (m_field, ts)
Walther@60763
   793
      | NONE => raise ERROR "I_Model.fill_from_o does NOT find a descriptor in O_Model"
Walther@60767
   794
    val descr = Model_Def.get_descr feedb (*i_single has been filtered appropriately*)
Walther@60763
   795
(*+*)val "[[u], [v]]" = all_value |> UnparseC.terms ctxt
Walther@60766
   796
    (*in*)
Walther@60766
   797
val true =
Walther@60766
   798
    (*if*) Model_Def.is_list_descr descr
Walther@60771
   799
        val already_input as [Const ("List.list.Cons", _) $ Free ("v", _) $ _] = feedb |> values_POS'
Walther@60763
   800
Walther@60766
   801
        val miss = subtract op= already_input all_value
Walther@60766
   802
(*+*)val "[[u]]" = miss |> UnparseC.terms ctxt
Walther@60766
   803
Walther@60766
   804
        val ts = already_input @ [hd miss]
Walther@60766
   805
val "[[v], [u]]" = ts |> UnparseC.terms ctxt
Walther@60766
   806
    (*in*)
Walther@60763
   807
val true =
Walther@60766
   808
        (*if*) length all_value = length ts
Walther@60771
   809
val return_fill_from_o_STEP = SOME (i, vnts, bool, m_field, (Cor_POS (descr, [values_to_present ts]), pos))
Walther@60763
   810
(*\\\----------------- step into fill_from_o -----------------------------------------------//*)
Walther@60763
   811
        val SOME (_, _, _, m_field, (feedb, _)) = return_fill_from_o
Walther@60771
   812
(*+*)val Cor_POS (Const ("Input_Descript.AdditionalValues", _), xxx) = feedb;
Walther@60766
   813
(*+*)val xxx = xxx |> UnparseC.terms ctxt;
Walther@60763
   814
Walther@60763
   815
(*||------------------ contiue.. item_to_add -------------------------------------------------*)
Walther@60763
   816
(** )val return_item_to_add = ( **)
Walther@60763
   817
  SOME (m_field, feedb |> 
Walther@60766
   818
   (*I_Model.*)feedb_args_to_string ctxt);
Walther@60763
   819
(*///----------------- step into feedb_args_to_string --------------------------------------\\*)
Walther@60771
   820
"~~~~~ fun feedb_args_to_string , args:"; val (ctxt, Cor_POS (descr, values)) = (ctxt, feedb);
Walther@60763
   821
(** )val return_feedb_args_to_string =( **)
Walther@60766
   822
val return_feedb_args_to_string_STEP =
Walther@60769
   823
    UnparseC.term ctxt (descr $ values_to_present values);
Walther@60763
   824
(*\\\----------------- step into feedb_args_to_string --------------------------------------//*)
Walther@60763
   825
(*\\------------------ step into item_to_add -----------------------------------------------//*)
Walther@60763
   826
val calling_code as SOME ("#Find", "AdditionalValues [v, u]") = return_item_to_add;
Walther@60763
   827
(*\------------------- fun item_to_add: AdditionalValues [v, u] ----------------------------//*)
Walther@60763
   828
Walther@60766
   829
Walther@60766
   830
(** fun item_to_add: Constants Extremum (A = 2 * u * v - u \<up> 2) ============================= **);
Walther@60771
   831
val i_single : I_Model.single_POS =
Walther@60771
   832
((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term Extremum}, []) , Position.none)))
Walther@60763
   833
val SOME ("#Relate", "Extremum (A = 2 * u * v - u \<up> 2)")
Walther@60763
   834
  = item_to_add ctxt o_model_test [i_single];
Walther@60763
   835
Walther@60766
   836
(** fun item_to_add: Constants SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ============ **);
Walther@60771
   837
val i_single : I_Model.single_POS =
Walther@60771
   838
((3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term SideConditions}, []) , Position.none)))
Walther@60763
   839
val SOME ("#Relate", "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]")
Walther@60763
   840
  = item_to_add ctxt o_model_test [i_single];
Walther@60763
   841
Walther@60766
   842
(** fun item_to_add: Solutions L ============================================================ **);
Walther@60771
   843
val i_single : I_Model.single_POS =
Walther@60771
   844
(3, [1, 2, 3], false, "from o_model", (Inc_POS (@{term solutions}, []) , Position.none))
Walther@60763
   845
val SOME ("#Find", "solutions L") = item_to_add ctxt o_model_test [i_single];
Walther@60766
   846
Walther@60766
   847
Walther@60766
   848
(*** fun item_to_add Biegelinie-exammple =================================================== ***);
Walther@60766
   849
"----------- fun item_to_add: Biegelinie-exammple ----------------------------------------------";
Walther@60766
   850
"----------- fun item_to_add: Biegelinie-exammple ----------------------------------------------";
Walther@60766
   851
Walther@60766
   852
(** fun item_to_add: solveForVars [c] ======================================================= **);
Walther@60766
   853
val (descr $ t) = @{term "solveForVars [c, c_2, c_3, c_4]"}
Walther@60766
   854
val [Const ("List.list.Cons", _) $ Free ("c",   _) $ Const ("List.list.Nil", _),
Walther@60766
   855
     Const ("List.list.Cons", _) $ Free ("c_2", _) $ Const ("List.list.Nil", _),
Walther@60766
   856
     Const ("List.list.Cons", _) $ Free ("c_3", _) $ Const ("List.list.Nil", _),
Walther@60766
   857
     Const ("List.list.Cons", _) $ Free ("c_4", _) $ Const ("List.list.Nil", _)]
Walther@60766
   858
  = make_values (descr, t)
Walther@60766
   859
Walther@60766
   860
val o_model_test : O_Model.T = [(0, [1], "#Given", descr, make_values (descr, t))]
Walther@60771
   861
val i_model_test : I_Model.T_POS = [
Walther@60771
   862
  (0, [1], false, "get-from-o_model", (Inc_POS (descr, []) , Position.none))]
Walther@60766
   863
val SOME ("#Given", "solveForVars [c]") = item_to_add ctxt o_model_test i_model_test;
Walther@60766
   864
Walther@60766
   865
(** fun item_to_add: solveForVars [c, c_2] ================================================== **);
Walther@60771
   866
val i_model_test : I_Model.T_POS = [
Walther@60771
   867
  (0, [1], false, "get-from-o_model", (Inc_POS (descr,
Walther@60766
   868
    [nth 1 (make_values (descr, t))]) , Position.none))]
Walther@60766
   869
val SOME ("#Given", "solveForVars [c, c_2]") = item_to_add ctxt o_model_test i_model_test;
Walther@60766
   870
Walther@60766
   871
(** fun item_to_add: solveForVars [c, c_2, c_3] ============================================= **);
Walther@60771
   872
val i_model_test : I_Model.T_POS = [
Walther@60771
   873
  (0, [1], false, "get-from-o_model", (Inc_POS (descr,
Walther@60766
   874
    (nth 1 (make_values (descr, t))) :: (nth 2 (make_values (descr, t))) :: []) , Position.none))]
Walther@60766
   875
val SOME ("#Given", "solveForVars [c, c_2, c_3]") = item_to_add ctxt o_model_test i_model_test;