1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Sep 26 15:57:12 2023 +0200
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Sep 27 12:17:44 2023 +0200
1.3 @@ -501,23 +501,15 @@
1.4
1.5 fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
1.6 let
1.7 -(*OLD* )
1.8 - val (itms, oris, probl) = case get_obj I pt p of
1.9 - PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
1.10 - | _ => raise ERROR ""
1.11 - val {model = met_patt, ...} = MethodC.from_store ctxt mI;
1.12 - val (_, itms) = I_Model.fill_method oris (I_Model.OLD_to_TEST probl) met_patt
1.13 -( *---*)
1.14 val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
1.15 PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
1.16 => (itms, oris, probl, o_spec, spec)
1.17 - | _ => raise ERROR ""
1.18 + | _ => raise ERROR "LI.by_tactic: no PblObj"
1.19 val (_, pI', _) = References.select_input o_spec spec
1.20 val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
1.21 val {model = met_patt, ...} = MethodC.from_store ctxt mI;
1.22 val (_, itms) = I_Model.s_make_complete oris
1.23 (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
1.24 -(*NEW*)
1.25 val (is, env, ctxt, prog) = case LItool.init_pstate ctxt itms mI of
1.26 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
1.27 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate"
2.1 --- a/src/Tools/isac/Specify/i-model.sml Tue Sep 26 15:57:12 2023 +0200
2.2 +++ b/src/Tools/isac/Specify/i-model.sml Wed Sep 27 12:17:44 2023 +0200
2.3 @@ -62,18 +62,10 @@
2.4 (bool * Model_Def.variant * T_TEST) * Env.T * (Pre_Conds.env_subst * Pre_Conds.env_eval)
2.5
2.6 val add: single -> T -> T
2.7 -(**)
2.8 val s_make_complete: O_Model.T -> T_TEST * T_TEST -> Model_Pattern.T * Model_Pattern.T ->
2.9 T_TEST * T_TEST
2.10 -(** )
2.11 - val complete: O_Model.T -> (*Problem*)T -> (*MethodC*)T -> Model_Pattern.T -> T
2.12 - val fill_method: O_Model.T -> T_TEST -> Model_Pattern.T -> T_TEST
2.13 -( **)
2.14 - val complete': Model_Pattern.T -> O_Model.single -> single
2.15 -(*^^^--- s_make_complete SHALL REPLACE ALL THESE*)
2.16
2.17 val is_error: feedback -> bool
2.18 -
2.19 val is_complete: T -> bool
2.20 val is_complete_variant: Model_Def.variant -> T_TEST-> bool
2.21 val to_p_model: theory -> feedback -> string
2.22 @@ -475,14 +467,6 @@
2.23 end
2.24 (*T_TESTnew*)
2.25
2.26 -(*filter oris which are in pbt, too*)
2.27 -fun filter_pbt oris pbt =
2.28 - let
2.29 - val dscs = map (fst o snd) pbt
2.30 - in
2.31 - filter ((member op= dscs) o (#4)) oris
2.32 - end
2.33 -
2.34 fun is_error (Cor _) = false
2.35 | is_error (Sup _) = false
2.36 | is_error (Inc _) = false
2.37 @@ -504,54 +488,6 @@
2.38 handles superfluous items carelessly *)
2.39 fun add itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
2.40
2.41 -(*combine itms from pbl + met and complete them wrt. pbt*)
2.42 -(* FIXXXME.WN031205 complete doesnt handle incorrect itms !*)
2.43 -fun complete oris pits mits met =
2.44 - let
2.45 - val vat = Pre_Conds.max_variant pits;
2.46 - val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
2.47 - val ors = filter ((member_swap op= vat) o (#2)) oris
2.48 - val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
2.49 - in
2.50 - itms @ (map (complete' met) os)
2.51 - end
2.52 -(**)
2.53 -
2.54 -(*T_TESTold*)
2.55 -(*complete model and guard of a calc-head*)
2.56 -fun complete_method (oris, mpc, model, probl) =
2.57 - let
2.58 - val pits = filter_out ((curry op= false) o (#3)) probl
2.59 - val vat = if probl = [] then 1 else Pre_Conds.max_variant probl
2.60 - val pors = filter ((member_swap op = vat) o (#2)) oris
2.61 - val pors = filter_outs pors pits (*which are in pbl already*)
2.62 - val pors = (filter_pbt pors model) (*which are in pbt, too*)
2.63 - val pits = pits @ (map (complete' model) pors)
2.64 - val mits = complete oris pits [] mpc
2.65 - in (pits, mits) end
2.66 -(*T_TEST*)
2.67 -fun msg vnts feedb = "get_descr_vnt' returns NONE: i.e. it does not find an item of o_model with\n" ^
2.68 - "variants " ^ ints2str' vnts ^ " and descriptor " ^
2.69 - (feedb |> Pre_Conds.get_dscr' |> the |> UnparseC.term (ContextC.for_ERROR ()))
2.70 -fun transfer_terms (i, vnts, m_field, descr, ts) =
2.71 - (i, vnts, true, m_field, (Cor_TEST (descr, ts), Position.none))
2.72 -fun fill_method o_model pbl_imod met_patt =
2.73 - let
2.74 - val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
2.75 - val from_pbl = map (fn (_, (descr, _)) =>
2.76 - Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) met_patt
2.77 - val from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
2.78 - if is_empty_single_TEST i_single
2.79 - then
2.80 - case Pre_Conds.get_descr_vnt' feedb pbl_max_vnts o_model of
2.81 - [] => raise ERROR (msg pbl_max_vnts feedb)
2.82 - | o_singles => map transfer_terms o_singles
2.83 - else [i_single (*fetched before from pbl_imod*)])) from_pbl
2.84 - in
2.85 - from_o_model |> flat
2.86 - end
2.87 -(*T_TESTnew*)
2.88 -
2.89 (*TODO: also check if all elements are I_Model.Cor*)
2.90 fun is_complete ([]: T) = false
2.91 | is_complete itms = foldl and_ (true, (map #3 itms))
2.92 @@ -562,6 +498,11 @@
2.93
2.94 val of_max_variant = Pre_Conds.of_max_variant
2.95
2.96 +fun msg vnts feedb = "get_descr_vnt' returns NONE: i.e. it does not find an item of o_model with\n" ^
2.97 + "variants " ^ ints2str' vnts ^ " and descriptor " ^
2.98 + (feedb |> Pre_Conds.get_dscr' |> the |> UnparseC.term (ContextC.for_ERROR ()))
2.99 +fun transfer_terms (i, vnts, m_field, descr, ts) =
2.100 + (i, vnts, true, m_field, (Cor_TEST (descr, ts), Position.none))
2.101 fun s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt) =
2.102 let
2.103 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
3.1 --- a/src/Tools/isac/Specify/p-spec.sml Tue Sep 26 15:57:12 2023 +0200
3.2 +++ b/src/Tools/isac/Specify/p-spec.sml Wed Sep 27 12:17:44 2023 +0200
3.3 @@ -186,12 +186,6 @@
3.4 (map (itms2fstr ctxt) probl), meth) end
3.5 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
3.6 then let
3.7 -(*OLD* )
3.8 - val met = (#model o MethodC.from_store ctxt) mI
3.9 - val mits = I_Model.complete oris probl meth met
3.10 - in if foldl and_ (true, map #3 mits)
3.11 - then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
3.12 -( *---*)
3.13 val pbl_patt = (#model o Problem.from_store ctxt) pI
3.14 val met = (#model o MethodC.from_store ctxt) mI
3.15 val (_, mits) = I_Model.s_make_complete oris
3.16 @@ -199,7 +193,6 @@
3.17 in if foldl and_ (true, map #3 mits)
3.18 then (Pos.Pbl, probl, I_Model.TEST_to_OLD mits)
3.19 else (Pos.Met, probl, I_Model.TEST_to_OLD mits)
3.20 -(*NEW*)
3.21 end
3.22 else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)]
3.23 ((#model o Problem.from_store ctxt)
4.1 --- a/src/Tools/isac/Specify/specify.sml Tue Sep 26 15:57:12 2023 +0200
4.2 +++ b/src/Tools/isac/Specify/specify.sml Wed Sep 27 12:17:44 2023 +0200
4.3 @@ -208,16 +208,19 @@
4.4 do all specification in one single step:
4.5 bypass input of Problem.model and go immediately for MethodC: I_Model.complete'
4.6 *)
4.7 -fun do_all (pt, (*old* )pos as( *old*) (p, _)) =
4.8 +fun do_all (pt, (p, _)) =
4.9 let
4.10 - val (o_model, o_refs as (_, _, met_id), ctxt) = case Ctree.get_obj I pt p of
4.11 - Ctree.PblObj {origin = (o_model, o_refs, _), ctxt, ...}
4.12 - => (o_model, o_refs, ctxt)
4.13 - | _ => raise ERROR "Specify.do_all: uncovered case get_obj"
4.14 - val mod_pat = MethodC.from_store ctxt met_id |> #model
4.15 - val i_model = map (I_Model.complete' mod_pat) o_model
4.16 - (*no parse, ^^^ takes existing terms; ctxt already created by O_Model.init*)
4.17 - val (pt, _) = Ctree.cupdate_problem pt p (o_refs, i_model, i_model, ctxt)
4.18 + val (itms, oris, probl, o_refs, spec, ctxt) = case Ctree.get_obj I pt p of
4.19 + Ctree.PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}
4.20 + => (itms, oris, probl, o_spec, spec, ctxt)
4.21 + | _ => raise ERROR "LI.by_tactic: no PblObj"
4.22 + val (_, pbl_id', met_id') = References.select_input o_refs spec
4.23 + val {model = pbl_patt, ...} = Problem.from_store ctxt pbl_id';
4.24 + val {model = met_patt, ...} = MethodC.from_store ctxt met_id';
4.25 + val (pbl_imod, met_imod) = I_Model.s_make_complete oris
4.26 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
4.27 + val (pt, _) = Ctree.cupdate_problem pt p
4.28 + (o_refs, I_Model.TEST_to_OLD pbl_imod, I_Model.TEST_to_OLD met_imod, ctxt)
4.29 in
4.30 (pt, (p, Pos.Met))
4.31 end
5.1 --- a/test/Tools/isac/Knowledge/diff-app.sml Tue Sep 26 15:57:12 2023 +0200
5.2 +++ b/test/Tools/isac/Knowledge/diff-app.sml Wed Sep 27 12:17:44 2023 +0200
5.3 @@ -394,7 +394,6 @@
5.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.5 === inhibit exn 110722=============================================================*)
5.6
5.7 -(*---*)
5.8
5.9 "--------- autoCalc .. scripts for maximum-example ---------------";
5.10 "--------- autoCalc .. scripts for maximum-example ---------------";
6.1 --- a/test/Tools/isac/Specify/specify.sml Tue Sep 26 15:57:12 2023 +0200
6.2 +++ b/test/Tools/isac/Specify/specify.sml Wed Sep 27 12:17:44 2023 +0200
6.3 @@ -122,32 +122,19 @@
6.4 Specify.do_all (pt, p);
6.5 (*//------------------ step into do_all ----------------------------------------------------\\*)
6.6 "~~~~~ fun do_all , args:"; val (pt, (*old* )pos as( *old*) (p, _)) = (pt, p);
6.7 -(*new*)val (f_model, dI, pI, mI, ctxt) = case Ctree.get_obj I pt p of
6.8 -(*new*) Ctree.PblObj {origin = (f_model, (dI, pI, mI), _), ctxt, ...}
6.9 -(*new*) => (f_model, dI, pI, mI, ctxt)
6.10 -(*new*)| _ => raise ERROR "do_all: uncovered case get_obj"
6.11 -(*new*)val mod_pat = MethodC.from_store ctxt mI |> #model : Model_Pattern.T
6.12 -
6.13 -(*new*)val i_model = map
6.14 - (I_Model.complete' mod_pat) f_model (*no parse, take terms*);
6.15 -"~~~~~ fun complete' , args:"; val (mod_pat, (i, v, f, d, ts)) = (mod_pat, nth 1 f_model);
6.16 -val SOME xxx =
6.17 - \<^try>\<open> (i, v, true, f, I_Model.Cor ((d, ts),
6.18 - ((find_first ((fn descriptor => (fn (_, (d, _)) => descriptor = d)) d)) mod_pat |> the |> snd |> snd, ts)
6.19 - ))\<close>
6.20 -val "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str)" =
6.21 - I_Model.single_to_string @{context} xxx;
6.22 -
6.23 -"~~~~~ fun complete' , args:"; val (mod_pat, (i, v, f, d, ts)) = (mod_pat, nth 7 f_model);
6.24 -val SOME xxx =
6.25 - \<^try>\<open> (i, v, true, f, I_Model.Cor ((d, ts),
6.26 - ((find_first ((fn descriptor => (fn (_, (d, _)) => descriptor = d)) d)) mod_pat |> the |> snd |> snd, ts)
6.27 - ))\<close>
6.28 -val "(7 ,[1] ,true ,#undef ,Cor FunctionVariable a , pen2str)"
6.29 - = I_Model.single_to_string @{context} xxx;
6.30 + val (itms, oris, probl, o_refs, spec, ctxt) = case Ctree.get_obj I pt p of
6.31 + Ctree.PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}
6.32 + => (itms, oris, probl, o_spec, spec, ctxt)
6.33 + | _ => raise ERROR "LI.by_tactic: no PblObj"
6.34 + val (_, pbl_id', met_id') = References.select_input o_refs spec
6.35 + val {model = pbl_patt, ...} = Problem.from_store ctxt pbl_id';
6.36 + val {model = met_patt, ...} = MethodC.from_store ctxt met_id';
6.37 + val (pbl_imod, met_imod) = I_Model.s_make_complete oris
6.38 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
6.39 +;
6.40 (*-------------------- stop step into do_all -------------------------------------------------*)
6.41 (*/------------------- check result of I_Model.complete' ------------------------------------\*)
6.42 -if Model_Pattern.to_string @{context} mod_pat = "[\"" ^
6.43 +(*+*)if Model_Pattern.to_string @{context} met_patt = "[\"" ^
6.44 "(#Given, (Constants, fixes))\", \"" ^
6.45 "(#Given, (Maximum, maxx))\", \"" ^
6.46 "(#Given, (Extremum, extr))\", \"" ^
6.47 @@ -155,42 +142,25 @@
6.48 "(#Given, (FunctionVariable, funvar))\", \"" ^
6.49 "(#Given, (Input_Descript.Domain, doma))\", \"" ^
6.50 "(#Given, (ErrorBound, err))\", \"" ^
6.51 - "(#Find, (AdditionalValues, vals))\"]" then () else error "mod_pat CHANGED";
6.52 -if I_Model.to_string @{context} i_model = "[\n" ^
6.53 - "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n" ^
6.54 - "(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n" ^
6.55 - "(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n" ^
6.56 - "(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n" ^
6.57 - "(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n" ^
6.58 - "(6 ,[3] ,true ,#Relate ,Cor SideConditions [u / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>] , pen2str), \n" ^
6.59 - "(7 ,[1] ,true ,#undef ,Cor FunctionVariable a , pen2str), \n" ^
6.60 - "(8 ,[2] ,true ,#undef ,Cor FunctionVariable b , pen2str), \n" ^
6.61 - "(9 ,[3] ,true ,#undef ,Cor FunctionVariable \<alpha> , pen2str), \n" ^
6.62 - "(10 ,[1, 2] ,true ,#undef ,Cor Input_Descript.Domain {0<..<r} , pen2str), \n" ^
6.63 - "(11 ,[3] ,true ,#undef ,Cor Input_Descript.Domain {0<..<\<pi> / 2} , pen2str), \n" ^
6.64 - "(12 ,[1, 2, 3] ,true ,#undef ,Cor ErrorBound (\<epsilon> = 0) , pen2str)]"
6.65 -then () else error "i_model CHANGED";
6.66 + "(#Find, (AdditionalValues, vals))\"]"
6.67 +(*+*)then () else error "mod_pat CHANGED";
6.68 +(*+*)if I_Model.to_string_TEST @{context} met_imod = "[\n" ^
6.69 + "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
6.70 + "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
6.71 + "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
6.72 + "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
6.73 + "(7, [1], true ,#undef, (Cor_TEST FunctionVariable a , pen2str, Position.T)), \n" ^
6.74 + "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
6.75 + "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
6.76 + "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
6.77 +(*+*)then () else error "met_imod CHANGED";
6.78 (*\------------------- check result of I_Model.complete' ------------------------------------/*)
6.79 (*\\------------------ step into do_all ----------------------------------------------------//*)
6.80
6.81 (*-------------------- continuing do_all -----------------------------------------------------*)
6.82 -(*new*)
6.83 - O_Model.values' ctxt f_model;
6.84 -"~~~~~ fun values' , args:"; val (ctxt, oris) = (ctxt, f_model);
6.85 -(*//------------------ inserted hidden code ------------------------------------------------\\*)
6.86 - fun ori2fmz_vals (_, _, _, dsc, ts) =
6.87 - case \<^try>\<open>(((UnparseC.term ctxt) o Input_Descript.join') (dsc, ts), last_elem ts)\<close> of
6.88 - SOME x => x
6.89 - | NONE => raise ERROR ("O_Model.values' called with " ^ UnparseC.terms ctxt ts);
6.90 -(*\\------------------ inserted hidden code ------------------------------------------------//*)
6.91 -(split_list o (map
6.92 - ori2fmz_vals)) oris;
6.93 -"~~~~~ fun ori2fmz_vals , args:"; val (_, _, _, dsc, ts) = (nth 1 oris);
6.94 -val xxx = Input_Descript.join' (dsc, ts)
6.95 -
6.96 -(*-------------------- continuing do_all -----------------------------------------------------*)
6.97 -(*new*)val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI), i_model, i_model, ctxt);
6.98 -
6.99 + val (pt, _) = Ctree.cupdate_problem pt p
6.100 + (o_refs, I_Model.TEST_to_OLD pbl_imod, I_Model.TEST_to_OLD met_imod, ctxt)
6.101 +;
6.102
6.103
6.104 (**** specify-phase: low level functions ################################################# ****)
7.1 --- a/test/Tools/isac/Test_Isac.thy Tue Sep 26 15:57:12 2023 +0200
7.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Sep 27 12:17:44 2023 +0200
7.3 @@ -277,6 +277,939 @@
7.4 ML_file "Specify/cas-command.sml"
7.5 ML_file "Specify/p-spec.sml"
7.6 ML_file "Specify/specify.sml"
7.7 +ML \<open>
7.8 +\<close> ML \<open>
7.9 +(* Title: "Specify/specify.sml"
7.10 + Author: Walther Neuper
7.11 + (c) due to copyright terms
7.12 +*)
7.13 +
7.14 +"-----------------------------------------------------------------------------------------------";
7.15 +"table of contents -----------------------------------------------------------------------------";
7.16 +"-----------------------------------------------------------------------------------------------";
7.17 +"-----------------------------------------------------------------------------------------------";
7.18 +"----------- maximum-example: Specify.finish_phase ---------------------------------------------";
7.19 +"----------- revise Specify.do_all -------------------------------------------------------------";
7.20 +"----------- specify-phase: low level functions ------------------------------------------------";
7.21 +"-----------------------------------------------------------------------------------------------";
7.22 +"-----------------------------------------------------------------------------------------------";
7.23 +"-----------------------------------------------------------------------------------------------";
7.24 +open Pos;
7.25 +open Ctree;
7.26 +open Test_Code;
7.27 +open Tactic;
7.28 +open Specify;
7.29 +open Step;
7.30 +
7.31 +open O_Model;
7.32 +open I_Model;
7.33 +open P_Model;
7.34 +open Specify_Step;
7.35 +open Test_Code;
7.36 +
7.37 +(**** maximum-example: Specify.finish_phase ############################################# ****)
7.38 +"----------- maximum-example: Specify.finish_phase ---------------------------------------------";
7.39 +"----------- maximum-example: Specify.finish_phase ---------------------------------------------";
7.40 +(*//-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --\\* )
7.41 + val (p,_,f,nxt,_,pt) =
7.42 + Test_Code.init_calc @{context}
7.43 + [(["fixedValues [r=Arbfix]", "maximum A",
7.44 + "valuesFor [a,b]",
7.45 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
7.46 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
7.47 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
7.48 +
7.49 + "boundVariable a", "boundVariable b", "boundVariable alpha",
7.50 + "interval {x::real. 0 <= x & x <= 2*r}",
7.51 + "interval {x::real. 0 <= x & x <= 2*r}",
7.52 + "interval {x::real. 0 <= x & x <= pi}",
7.53 + "errorBound (eps=(0::real))"],
7.54 + ("Diff_App",["maximum_of", "function"],["Diff_App", "max_by_calculus"])
7.55 + )];
7.56 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.57 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.58 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.59 + (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
7.60 + val pits = get_obj g_pbl pt (fst p);
7.61 + writeln (I_Model.to_string ctxt pits);
7.62 +(*[
7.63 +(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
7.64 +(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
7.65 +(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
7.66 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
7.67 + val (pt,p) = Specify.finish_phase (pt,p);
7.68 + val pits = get_obj g_pbl pt (fst p);
7.69 + if I_Model.to_string ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(rs_, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]"
7.70 + then () else error "completetest.sml: new behav. in Specify.finish_phase 3";
7.71 + writeln (I_Model.to_string ctxt pits);
7.72 +(*[
7.73 +(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
7.74 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
7.75 +(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
7.76 +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up>
7.77 +2 = r \<up> 2] ,(relations, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]*)
7.78 + val mits = get_obj g_met pt (fst p);
7.79 + if I_Model.to_string ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(rs_, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]"
7.80 + then () else error "completetest.sml: new behav. in Specify.finish_phase 3";
7.81 + writeln (I_Model.to_string ctxt mits);
7.82 +(*[
7.83 +(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
7.84 +(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
7.85 +(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
7.86 +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up>
7.87 +2 = r \<up> 2] ,(relations, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),
7.88 +(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
7.89 +(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
7.90 +0 <= x & x <= 2 * r}])),
7.91 +(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
7.92 +( *\\-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --//*)
7.93 +
7.94 +
7.95 +(**** revise Specify.do_all ############################################################## ****);
7.96 +"----------- revise Specify.do_all -------------------------------------------------------------";
7.97 +"----------- revise Specify.do_all -------------------------------------------------------------";
7.98 +(* from Minisubplb/100-init-rootpbl.sml:
7.99 +val (_(*example text*),
7.100 + (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
7.101 + "Extremum (A = 2 * u * v - u \<up> 2)" ::
7.102 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
7.103 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
7.104 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
7.105 + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
7.106 + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
7.107 + "ErrorBound (\<epsilon> = (0::real))" :: []),
7.108 + refs as ("Diff_App",
7.109 + ["univariate_calculus", "Optimisation"],
7.110 + ["Optimisation", "by_univariate_calculus"])))
7.111 + = Store.get (Know_Store.get_expls @ {theory Know_Store}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
7.112 +*)
7.113 +val model = ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
7.114 + "Extremum (A = 2 * u * v - u \<up> 2)" ::
7.115 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
7.116 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
7.117 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
7.118 + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
7.119 + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
7.120 + "ErrorBound (\<epsilon> = (0::real))" :: [])
7.121 +val refs = ("Diff_App",
7.122 + ["univariate_calculus", "Optimisation"],
7.123 + ["Optimisation", "by_univariate_calculus"])
7.124 +
7.125 +val (p,_,f,nxt,_,pt) =
7.126 + Test_Code.init_calc @{context} [(model, refs)];
7.127 +"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])
7.128 + = (@{context}, [(model, refs)]);
7.129 +
7.130 + Specify.do_all (pt, p);
7.131 +(*//------------------ step into do_all ----------------------------------------------------\\*)
7.132 +"~~~~~ fun do_all , args:"; val (pt, (*old* )pos as( *old*) (p, _)) = (pt, p);
7.133 + val (itms, oris, probl, o_refs, spec, ctxt) = case Ctree.get_obj I pt p of
7.134 + Ctree.PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}
7.135 + => (itms, oris, probl, o_spec, spec, ctxt)
7.136 + | _ => raise ERROR "LI.by_tactic: no PblObj"
7.137 + val (_, pbl_id', met_id') = References.select_input o_refs spec
7.138 + val {model = pbl_patt, ...} = Problem.from_store ctxt pbl_id';
7.139 + val {model = met_patt, ...} = MethodC.from_store ctxt met_id';
7.140 + val (pbl_imod, met_imod) = I_Model.s_make_complete oris
7.141 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
7.142 +;
7.143 +(*-------------------- stop step into do_all -------------------------------------------------*)
7.144 +(*/------------------- check result of I_Model.complete' ------------------------------------\*)
7.145 +\<close> ML \<open>
7.146 +(*+*)if Model_Pattern.to_string @{context} met_patt = "[\"" ^
7.147 + "(#Given, (Constants, fixes))\", \"" ^
7.148 + "(#Given, (Maximum, maxx))\", \"" ^
7.149 + "(#Given, (Extremum, extr))\", \"" ^
7.150 + "(#Given, (SideConditions, sideconds))\", \"" ^
7.151 + "(#Given, (FunctionVariable, funvar))\", \"" ^
7.152 + "(#Given, (Input_Descript.Domain, doma))\", \"" ^
7.153 + "(#Given, (ErrorBound, err))\", \"" ^
7.154 + "(#Find, (AdditionalValues, vals))\"]"
7.155 +(*+*)then () else error "mod_pat CHANGED";
7.156 +\<close> ML \<open>
7.157 +(*+*)if I_Model.to_string_TEST @{context} met_imod = "[\n" ^
7.158 + "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
7.159 + "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
7.160 + "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
7.161 + "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
7.162 + "(7, [1], true ,#undef, (Cor_TEST FunctionVariable a , pen2str, Position.T)), \n" ^
7.163 + "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
7.164 + "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
7.165 + "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
7.166 +(*+*)then () else error "met_imod CHANGED";
7.167 +(*\------------------- check result of I_Model.complete' ------------------------------------/*)
7.168 +(*\\------------------ step into do_all ----------------------------------------------------//*)
7.169 +
7.170 +\<close> ML \<open>
7.171 +(*-------------------- continuing do_all -----------------------------------------------------*)
7.172 + val (pt, _) = Ctree.cupdate_problem pt p
7.173 + (o_refs, I_Model.TEST_to_OLD pbl_imod, I_Model.TEST_to_OLD met_imod, ctxt)
7.174 +;
7.175 +
7.176 +
7.177 +
7.178 +\<close> ML \<open>
7.179 +(**** specify-phase: low level functions ################################################# ****)
7.180 +"----------- specify-phase: low level functions -----------------------------------------";
7.181 +"----------- specify-phase: low level functions -----------------------------------------";
7.182 +open Pos;
7.183 +open Ctree;
7.184 +open Test_Code;
7.185 +open Tactic;
7.186 +open Specify;
7.187 +open Step;
7.188 +
7.189 +open O_Model;
7.190 +open I_Model;
7.191 +open P_Model;
7.192 +open Specify_Step;
7.193 +
7.194 +val formalise = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
7.195 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
7.196 +(*
7.197 + Now follow items for ALL SubProblems,
7.198 + since ROOT MethodC must provide values for "actuals" of ALL SubProblems.
7.199 + See Biegelinie.thy subsection \<open>Survey on Methods\<close>.
7.200 +*)
7.201 +(*
7.202 + Items for MethodC "IntegrierenUndKonstanteBestimmen2"
7.203 +*)
7.204 + "FunktionsVariable x",
7.205 + (*"Biegelinie y", ..already input for Problem above*)
7.206 + "AbleitungBiegelinie dy",
7.207 + "Biegemoment M_b",
7.208 + "Querkraft Q",
7.209 +(*
7.210 + Item for Problem "LINEAR/system", which by [''no_met''] involves refinement
7.211 +*)
7.212 + "GleichungsVariablen [c, c_2, c_3, c_4]"
7.213 +];
7.214 +(*
7.215 + Note: the above sequence of items follows the sequence of formal arguments (and of model items)
7.216 + of MethodC "IntegrierenUndKonstanteBestimmen2"
7.217 +*)
7.218 +val references = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
7.219 +val p = e_pos'; val c = [];
7.220 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(formalise, references)]; (*nxt = Model_Problem*)
7.221 +
7.222 +(*/------------------- check result of Test_Code.init_calc @{context} ----------------------------------------\*)
7.223 +(*+*)val (o_model, ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]), _) =
7.224 + get_obj g_origin pt (fst p);
7.225 +(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
7.226 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
7.227 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
7.228 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
7.229 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
7.230 + "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
7.231 + "(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^
7.232 + "(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^
7.233 + "(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^
7.234 + "(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"
7.235 +then () else error "[IntegrierenUndKonstanteBestimmen2] O_Model CHANGED";
7.236 +(*\------------------- check result of Test_Code.init_calc @{context} ----------------------------------------/*)
7.237 +
7.238 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Traegerlaenge L" = nxt
7.239 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt
7.240 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Biegelinie y" = nxt
7.241 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = nxt
7.242 +(*/---broken elementwise input to lists---\* )
7.243 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
7.244 +( *\---broken elementwise input to lists---/*)
7.245 +
7.246 +val return_me_Add_Relation_Randbedingungen = me nxt p c pt; (*\<rightarrow>Specify_Problem ["Biegelinien"]*)
7.247 +(*/------------------- step into me_Add_Relation_Randbedingungen ---------------------------\\*)
7.248 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
7.249 + val ctxt = Ctree.get_ctxt pt p
7.250 + val (pt, p) =
7.251 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
7.252 + case Step.by_tactic tac (pt, p) of
7.253 + ("ok", (_, _, ptp)) => ptp
7.254 +
7.255 +val ("ok", ([(Specify_Theory "Biegelinie", _, _)], _, _)) =
7.256 + (*case*)
7.257 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
7.258 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
7.259 + (p, ((pt, Pos.e_pos'), []));
7.260 + (*if*) Pos.on_calc_end ip (*else*);
7.261 + val (_, probl_id, _) = Calc.references (pt, p);
7.262 +val _ =
7.263 + (*case*) tacis (*of*);
7.264 + (*if*) probl_id = Problem.id_empty (*else*);
7.265 +
7.266 +\<close> ML \<open>
7.267 + switch_specify_solve p_ (pt, ip);
7.268 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
7.269 + (*if*) Pos.on_specification ([], state_pos) (*then*);
7.270 +
7.271 + specify_do_next (pt, input_pos);
7.272 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
7.273 + val (_, (p_', tac)) = Specify.find_next_step ptp
7.274 + val ist_ctxt = Ctree.get_loc pt (p, p_)
7.275 +val Specify_Theory "Biegelinie" =
7.276 + (*case*) tac (*of*);
7.277 +
7.278 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
7.279 +
7.280 +(*|------------------- contine me_Add_Relation_Randbedingungen -------------------------------*)
7.281 +(*\------------------- step into me_Add_Relation_Randbedingungen ---------------------------//*)
7.282 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = return_me_Add_Relation_Randbedingungen;
7.283 + val Specify_Theory "Biegelinie" = nxt
7.284 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["Biegelinien"] = nxt
7.285 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
7.286 +
7.287 +(*[], Met*)val return_me_Specify_Method_IntegrierenUndKonstanteBestimmen2
7.288 + = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
7.289 +(*/------------------- step into me_Specify_Method_IntegrierenUndKonstanteBestimmen2--------\*)
7.290 +
7.291 +(*/------------------- initial check for whole me ------------------------------------------\*)
7.292 +(*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt;
7.293 +
7.294 +(*+*)val {origin = (o_model, o_refs, _), probl = i_pbl, meth = i_met, spec, ...} =
7.295 + Calc.specify_data (pt, p);
7.296 +(*+*)if o_refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])
7.297 +(*+*)then () else error "initial o_refs CHANGED";
7.298 +(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
7.299 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
7.300 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
7.301 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
7.302 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
7.303 + "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
7.304 + "(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^
7.305 + "(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^
7.306 + "(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^
7.307 + "(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"
7.308 +(*+*)then () else error "initial o_model CHANGED";
7.309 +(*+*)if I_Model.to_string @{context} i_pbl = "[\n" ^
7.310 + "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
7.311 + "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
7.312 + "(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
7.313 + "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str)]"
7.314 +(*+*)then () else error "initial i_pbl CHANGED";
7.315 +(*+*)if I_Model.to_string @{context} i_met = "[]"
7.316 +(*+*)then () else error "initial i_met CHANGED";
7.317 +(*+*)val (_, ["Biegelinien"], _) = spec;
7.318 +(*\------------------- initial check for whole me ------------------------------------------/*)
7.319 +
7.320 +"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
7.321 +(*/------------------- step into Step.by_tactic \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\*)
7.322 + val (pt'''''_', p'''''_') = case
7.323 +
7.324 + Step.by_tactic tac (pt, p) of ("ok", (_, _, ptp)) => ptp;
7.325 +(*/------------------- check for entry to Step.by_tactic -----------------------------------\*)
7.326 +(*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = tac;
7.327 +(*+*)val {origin = (o_model, _, _), ...} = Calc.specify_data (pt, p);
7.328 +(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
7.329 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
7.330 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
7.331 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
7.332 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
7.333 + "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
7.334 + "(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^
7.335 + "(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^
7.336 + "(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^
7.337 + "(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"
7.338 +(*+*)then () else error "o_model AFTER Specify_Method NOTok CHANGED";
7.339 +(*\------------------- check for Step.by_tactic --------------------------------------------/*)
7.340 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
7.341 + val Applicable.Yes tac' = (*case*)
7.342 +
7.343 + Step.check tac (pt, p) (*of*);
7.344 +"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
7.345 + (*if*) Tactic.for_specify tac (*then*);
7.346 +
7.347 +Specify_Step.check tac (ctree, pos);
7.348 +"~~~~~ fun check , args:"; val ((Tactic.Specify_Method mID), (ctree, pos)) = (tac, (ctree, pos));
7.349 +
7.350 + val (o_model''''', _, i_model''''') =
7.351 + Specify_Step.complete_for mID (ctree, pos);
7.352 +"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (mID, (ctree, pos));
7.353 + val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
7.354 + ...} = Calc.specify_data (ctree, pos);
7.355 + val (dI, _, _) = References.select_input o_refs refs;
7.356 + val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
7.357 + val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
7.358 + val (o_model', ctxt') =
7.359 +
7.360 + O_Model.complete_for m_patt root_model (o_model, ctxt);
7.361 +(*/------------------- check entry to O_Model.complete_for -----------------------------------------\*)
7.362 +(*+*)Model_Pattern.to_string @{context} m_patt = "[\"" ^
7.363 + "(#Given, (Traegerlaenge, l))\", \"" ^
7.364 + "(#Given, (Streckenlast, q))\", \"" ^
7.365 + "(#Given, (FunktionsVariable, v))\", \"" ^
7.366 + "(#Given, (GleichungsVariablen, vs))\", \"" ^
7.367 + "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^
7.368 + "(#Find, (Biegelinie, b))\", \"" ^
7.369 + "(#Relate, (Randbedingungen, s))\"]";
7.370 +(*+*) O_Model.to_string @{context} root_model;
7.371 +(*\------------------- check entry to O_Model.complete_for -----------------------------------------/*)
7.372 +"~~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) = (m_patt, root_model, (o_model, ctxt));
7.373 + val missing = m_patt |> filter_out
7.374 + (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor));
7.375 + val add = (root_model
7.376 + |> filter
7.377 + (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor))
7.378 +;
7.379 + ((o_model @ add)
7.380 + |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
7.381 + |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
7.382 + |> add_enumerate (* for correct enumeration *)
7.383 + |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
7.384 + ctxt |> ContextC.add_constraints (add |> values |> TermC.vars')) (*return from O_Model.complete_for*);
7.385 +"~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.complete_for , return:"; val (o_model', ctxt') =
7.386 + ((o_model @ add)
7.387 + |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
7.388 + |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
7.389 + |> add_enumerate (* for correct enumeration *)
7.390 + |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
7.391 + ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'));
7.392 +
7.393 +(*/------------------- check of result from O_Model.complete_for -----------------------------------\*)
7.394 +(*+*) O_Model.to_string @{context} o_model'; "O_Model.complete_for: result o_model CHANGED";
7.395 +(*\------------------- check of result from O_Model.complete_for -----------------------------------/*)
7.396 +
7.397 + val thy = ThyC.get_theory @{context} dI
7.398 + val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
7.399 +
7.400 + (o_model', ctxt', i_model) (*return from Specify_Step.complete_for*);
7.401 +
7.402 +"~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.check , return:"; val (o_model, _, i_model) =
7.403 + (o_model', ctxt', i_model);
7.404 +
7.405 + Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model)) (*return from Specify_Step.check*);
7.406 +"~~~~~ fun Specify_Step.check \<longrightarrow>fun Step.check \<longrightarrow>fun Step.by_tactic , return:"; val (Applicable.Yes tac') =
7.407 + (Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model)));
7.408 + (*if*) Tactic.for_specify' tac' (*then*);
7.409 + val ("ok", ([], [], (_, _))) =
7.410 +
7.411 +Step_Specify.by_tactic tac' ptp;
7.412 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt,pos as (p, _))) =
7.413 + (tac', ptp);
7.414 +(*NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
7.415 +(*NEW*) ...} = Calc.specify_data (pt, pos);
7.416 +(*NEW*) val (dI, _, mID) = References.select_input o_refs refs;
7.417 +(*NEW*) val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
7.418 +(*NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
7.419 +(*NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
7.420 +(*NEW*) val thy = ThyC.get_theory @{context} dI
7.421 +(*NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
7.422 +(*NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))
7.423 +(*NEW*) (Istate_Def.Uistate, ctxt') (pt, pos)
7.424 +
7.425 +(*/------------------- check result of Step_Specify.by_tactic ------------------------------\*)
7.426 +(*+*)val {origin = (o_model, _, _), meth, ...} = Calc.specify_data (pt, pos);
7.427 +(*+*)O_Model.to_string @{context} o_model;
7.428 +(*+*)if I_Model.to_string @{context} meth = "[\n" ^
7.429 + "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
7.430 + "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
7.431 + "(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
7.432 + "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str), \n" ^
7.433 + "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^
7.434 + "(6 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der), \n" ^
7.435 + "(7 ,[1] ,false ,#Given ,Mis Biegemoment id_momentum), \n" ^
7.436 + "(8 ,[1] ,false ,#Given ,Mis Querkraft id_lat_force), \n" ^
7.437 + "(9 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs)]"
7.438 +(*+*)then () else error "result of Step_Specify.by_tactic o_model CHANGED";
7.439 +(*\------------------- check result of Step_Specify.by_tactic ------------------------------/*)
7.440 +(*\------------------- step into Step.by_tactic /////////////////////////////////////////////*)
7.441 +
7.442 +
7.443 +\<close> ML \<open>
7.444 +val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
7.445 + Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []) (*of*);
7.446 +(*/------------------- step into Step.do_next \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\*)
7.447 +"~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
7.448 + (p'''''_', ((pt'''''_', Pos.e_pos'), []));
7.449 + (*if*) Pos.on_calc_end ip (*else*);
7.450 + val (_, probl_id, _) = Calc.references (pt, p);
7.451 + val _ = (*case*) tacis (*of*);
7.452 + (*if*) probl_id = Problem.id_empty (*else*);
7.453 +
7.454 +val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
7.455 + switch_specify_solve p_ (pt, ip);
7.456 +"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
7.457 + (*if*) Pos.on_specification ([], state_pos) (*then*);
7.458 +
7.459 +val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], [], (pt'''''_'', p'''''_''))) =
7.460 + Step.specify_do_next (pt, input_pos);
7.461 +(*/------------------- check result of specify_do_next -------------------------------------\*)
7.462 +(*+*)val {origin = (ooo_mod, _, _), meth, ...} = Calc.specify_data (pt'''''_'', p'''''_'');
7.463 +(*+*) O_Model.to_string @{context} ooo_mod; "result of Step_Specify.by_tactic o_model CHANGED";
7.464 +(*+*)if I_Model.to_string @{context} meth = "[\n" ^
7.465 + "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
7.466 + "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
7.467 + "(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
7.468 + "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str), \n" ^
7.469 + "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x , pen2str), \n" ^
7.470 + "(6 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der), \n" ^
7.471 + "(7 ,[1] ,false ,#Given ,Mis Biegemoment id_momentum), \n" ^
7.472 + "(8 ,[1] ,false ,#Given ,Mis Querkraft id_lat_force), \n" ^
7.473 + "(9 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs)]"
7.474 +(*+*)then () else error "result of Step_Specify.by_tactic i_model CHANGED";
7.475 +(*\------------------- check result of specify_do_next -------------------------------------/*)
7.476 +"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
7.477 +
7.478 +(**)val (_, (p_', Add_Given "FunktionsVariable x")) =(**)
7.479 + Specify.find_next_step ptp;
7.480 +"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
7.481 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
7.482 + spec = refs, ...} = Calc.specify_data (pt, pos);
7.483 + val ctxt = Ctree.get_ctxt pt pos;
7.484 + (*if*) Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin (*else*);
7.485 + (*if*) p_ = Pos.Pbl (*else*);
7.486 +
7.487 +val return = for_problem ctxt oris (o_refs, refs) (pbl, met);
7.488 +"~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
7.489 + (oris, (o_refs, refs), (pbl, met));
7.490 + val cmI = if mI = MethodC.id_empty then mI' else mI;
7.491 + val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;
7.492 + val (preok, _) = Pre_Conds.check ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);
7.493 +"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return);
7.494 +(*/------------------- check within find_next_step -----------------------------------------\*)
7.495 +(*+*)Model_Pattern.to_string @{context} (MethodC.from_store ctxt mI' |> #model) = "[\"" ^
7.496 + "(#Given, (Traegerlaenge, l))\", \"" ^
7.497 + "(#Given, (Streckenlast, q))\", \"" ^
7.498 + "(#Given, (FunktionsVariable, v))\", \"" ^ (* <---------- take m_field from here !!!*)
7.499 + "(#Given, (GleichungsVariablen, vs))\", \"" ^
7.500 + "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^
7.501 + "(#Find, (Biegelinie, b))\", \"" ^
7.502 + "(#Relate, (Randbedingungen, s))\"]";
7.503 +(*\------------------- check within find_next_step -----------------------------------------/*)
7.504 +
7.505 + (*case*) item_to_add (ThyC.get_theory @{context} (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
7.506 +"~~~~~ ~ fun item_to_add , args:"; val (thy, oris, _, itms) =
7.507 + ((ThyC.get_theory @{context} (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
7.508 +(*OLD*)fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v (**)andalso (#3 ori) <> "#undef"(**)
7.509 + fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
7.510 + fun test_id ids r = member op= ids (#1 (r : O_Model.single))
7.511 + fun test_subset itm (_, _, _, d, ts) =
7.512 + (I_Model.descriptor (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.o_model_values (#5 itm), ts)
7.513 + fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
7.514 + | false_and_not_Sup (_, _, false, _, _) = true
7.515 + | false_and_not_Sup _ = false
7.516 + val v = if itms = [] then 1 else Pre_Conds.max_variant itms
7.517 + val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
7.518 + val vits =
7.519 + if v = 0
7.520 + then itms (* because of dsc without dat *)
7.521 + else filter (testi_vt v) itms; (* itms..vat *)
7.522 + val icl = filter false_and_not_Sup vits; (* incomplete *)
7.523 +
7.524 +(*/------------------- check within item_to_add --------------------------------------------\*)
7.525 +(*+*)if I_Model.to_string @{context} icl = "[\n" ^ (*.. values, not formals*)
7.526 + "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^ (*.. values, not formals*)
7.527 + "(6 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der), \n" ^ (*.. values, not formals*)
7.528 + "(7 ,[1] ,false ,#Given ,Mis Biegemoment id_momentum), \n" ^ (*.. values, not formals*)
7.529 + "(8 ,[1] ,false ,#Given ,Mis Querkraft id_lat_force), \n" ^ (*.. values, not formals*)
7.530 + "(9 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs)]"
7.531 +(*+*)then () else error "icl within item_to_add CHANGED";
7.532 +(*+*) O_Model.to_string @{context} vors; "vors within item_to_add CHANGED";
7.533 +(*+*)if I_Model.to_string @{context} itms = "[\n" ^
7.534 + "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
7.535 + "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
7.536 + "(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
7.537 + "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str), \n" ^
7.538 + "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^
7.539 + "(6 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der), \n" ^
7.540 + "(7 ,[1] ,false ,#Given ,Mis Biegemoment id_momentum), \n" ^
7.541 + "(8 ,[1] ,false ,#Given ,Mis Querkraft id_lat_force), \n" ^
7.542 + "(9 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs)]"
7.543 +(*+*)then () else error "i_model within item_to_add CHANGED";
7.544 +(*\------------------- check within item_to_add --------------------------------------------/*)
7.545 +
7.546 + (*if*) icl = [] (*else*);
7.547 + val SOME ori =(*case*) find_first (test_subset (hd icl)) vors (*of*);
7.548 +
7.549 +(*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) = ori
7.550 +(*+*)val SOME ("#Given", "FunktionsVariable x") =
7.551 +
7.552 + SOME
7.553 + (I_Model.get_field_term thy ori (hd icl)) (*return from item_to_add*);
7.554 +"~~~~~ ~~ fun get_field_term , args:"; val (thy, (_, _, _, d, ts), (_, _, _, fd, itm_)) = (thy, ori, (hd icl));
7.555 +
7.556 +val rrrrr =
7.557 + (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join)
7.558 + (d, subtract op = (o_model_values itm_) ts)) (*return from get_field_term*);
7.559 +"~~~~~ ~~ from fun get_field_term \<longrightarrow>fun item_to_add \<longrightarrow>fun find_next_step , return:"; val (SOME (fd, ct')) =
7.560 + (SOME rrrrr);
7.561 + ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*return from find_next_step*);
7.562 +
7.563 +(*+*)val Add_Given "FunktionsVariable x" = P_Model.mk_additem fd ct';
7.564 +
7.565 +"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) =
7.566 + ("dummy", (Pos.Met, P_Model.mk_additem fd ct'));
7.567 + val ist_ctxt = Ctree.get_loc pt (p, p_)
7.568 + val _ = (*case*) tac (*of*);
7.569 +
7.570 + ("dummy",
7.571 +Step_Specify.by_tactic_input tac (pt, (p, p_'))) (*return from specify_do_next*);
7.572 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
7.573 + (tac, (pt, (p, p_')));
7.574 +
7.575 + val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
7.576 + Specify.by_Add_ "#Given" ct ptp (*return from by_tactic_input*);
7.577 +"~~~~~ ~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);
7.578 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
7.579 + (*if*) p_ = Pos.Met (*then*);
7.580 + val (i_model, m_patt) = (met,
7.581 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
7.582 +
7.583 +val Add (5, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) =
7.584 + (*case*)
7.585 + I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
7.586 +"~~~~~ ~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
7.587 + (ctxt, m_field, oris, i_model, m_patt, ct);
7.588 +(*.NEW*) val SOME (t as (descriptor $ _)) = (*case*) ParseC.term_opt ctxt str (*of*);
7.589 +(*.NEW*) val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
7.590 +
7.591 +val ("", (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), [Free ("x", _)]) =
7.592 + (*case*)
7.593 + O_Model.contains ctxt m_field o_model t (*of*);
7.594 +"~~~~~ ~~~ fun contains , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
7.595 + val ots = ((distinct op =) o flat o (map #5)) ori
7.596 + val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots
7.597 + val (d, ts) = Input_Descript.split t
7.598 + val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);
7.599 + (*if*) (subtract op = oids ids) <> [] (*else*);
7.600 + (*if*) d = TermC.empty (*else*);
7.601 + (*if*) member op = (map #4 ori) d (*then*);
7.602 +
7.603 + associate_input ctxt sel (d, ts) ori;
7.604 +"~~~~~ ~~~~ fun associate_input , args:"; val (ctxt, m_field, (descript, vals), ((id, vat, m_field', descript', vals') :: oris)) =
7.605 + (ctxt, sel, (d, ts), ori);
7.606 +
7.607 +(*/------------------- check within associate_input ------------------------------------------\*)
7.608 +(*+*)val Add_Given "FunktionsVariable x" = tac;
7.609 +(*+*)m_field = "#Given";
7.610 +(*+*)val Const (\<^const_name>\<open>FunktionsVariable\<close>, _) = descript;
7.611 +(*+*)val [Free ("x", _)] = vals;
7.612 +(*+*)O_Model.to_string @{context} ori = "[\n" ^
7.613 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
7.614 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
7.615 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
7.616 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
7.617 + "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
7.618 + "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
7.619 + "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";
7.620 +(*+*)val (id, vat, m_field', descript', vals') = nth 5 ori
7.621 +(*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) =
7.622 + (id, vat, m_field', descript', vals')
7.623 +(*\------------------- check within associate_input ----------------------------------------/*)
7.624 +(*\------------------- step into me_Specify_Method_IntegrierenUndKonstanteBestimmen2--------*)
7.625 +(*[], Met*)val (p,_,f,nxt,_,pt) = return_me_Specify_Method_IntegrierenUndKonstanteBestimmen2
7.626 + val Add_Given "FunktionsVariable x" = nxt;
7.627 +
7.628 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt
7.629 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegemoment M_b" = nxt
7.630 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querkraft Q" = nxt
7.631 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]" = nxt
7.632 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
7.633 +
7.634 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
7.635 +(*/------------------- check entry to me Model_Problem -------------------------------------\*)
7.636 +(*+*)val ([1], Pbl) = p;
7.637 +(*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =
7.638 + get_obj g_origin pt (fst p);
7.639 +(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
7.640 + "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
7.641 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
7.642 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
7.643 +(*
7.644 +.. here the O_Model does NOT know, which MethodC will be chosen,
7.645 +so "belastung_zu_biegelinie q__q v_v b_b id_abl" is NOT known,
7.646 +"b_b" and "id_abl" are NOT missing.
7.647 +*)
7.648 +then () else error "[Biegelinien, ausBelastung] initial O_Model CHANGED";
7.649 +(*\------------------- check entry to me Model_Problem -------------------------------------/*)
7.650 +
7.651 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)
7.652 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
7.653 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "Funktionen funs'''":*)
7.654 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)
7.655 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Problem ["vonBelastungZu", "Biegelinien"]*)
7.656 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Method ["Biegelinien", "ausBelastung"]*)
7.657 +
7.658 +(*[1], Met*)val return_me_Specify_Method_ausBelastung = me nxt p c pt; (*\<rightarrow>Add_Given "Biegelinie y"*)
7.659 +(*//------------------ step into me_Specify_Method_ausBelastung ----------------------------\\*)
7.660 +(*+*)val Specify_Method ["Biegelinien", "ausBelastung"] = nxt;
7.661 +(*+*)(* by \<up> \<up> \<up> \<up> "b_b" and "id_abl" must be requested: PUT THEM INTO O_Model*)
7.662 +
7.663 +"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
7.664 +
7.665 + val ("ok", ([], [], (_, _))) = (*case*)
7.666 + Step.by_tactic tac (pt, p) (*of*);
7.667 +"~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
7.668 + val Applicable.Yes tac' = (*case*) check tac (pt, p) (*of*);
7.669 + (*if*) Tactic.for_specify' tac' (*then*);
7.670 +
7.671 + val ("ok", ([], [], (_, _))) =
7.672 +Step_Specify.by_tactic tac' ptp;
7.673 +(*/------------------- initial check for Step_Specify.by_tactic ----------------------------\*)
7.674 +(*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =
7.675 + get_obj g_origin pt (fst p);
7.676 +(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
7.677 + "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
7.678 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
7.679 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
7.680 +(*
7.681 +.. here the MethodC has been determined by the user,
7.682 +so "belastung_zu_biegelinie q__q v_v b_b id_abl" IS KNOWN and,
7.683 +"b_b" and "id_abl" WOULD BE missing (added by O_Model.).
7.684 +*)
7.685 +then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC";
7.686 +(*\------------------- initial check for Step_Specify.by_tactic ----------------------------/*)
7.687 +"~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt, pos as (p, _))) =
7.688 + (tac', ptp);
7.689 +(*.NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,
7.690 +(*.NEW*) ...} =Calc.specify_data (pt, pos);
7.691 +(*.NEW*) val (dI, _, mID) = References.select_input o_refs refs;
7.692 +(*.NEW*) val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
7.693 +(*.NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
7.694 +(*.NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt);
7.695 +
7.696 +(*/------------------- check for entry to O_Model.complete_for -----------------------------\*)
7.697 +(*+*)if mID = ["Biegelinien", "ausBelastung"]
7.698 +(*+*)then () else error "MethodC [Biegelinien, ausBelastung] CHANGED";
7.699 +(*+*)if Model_Pattern.to_string @{context} m_patt = "[\"" ^
7.700 + "(#Given, (Streckenlast, q__q))\", \"" ^
7.701 + "(#Given, (FunktionsVariable, v_v))\", \"" ^
7.702 + "(#Given, (Biegelinie, b_b))\", \"" ^
7.703 + "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^
7.704 + "(#Given, (Biegemoment, id_momentum))\", \"" ^
7.705 + "(#Given, (Querkraft, id_lat_force))\", \"" ^
7.706 + "(#Find, (Funktionen, fun_s))\"]"
7.707 +(*+*)then () else error "[Biegelinien, ausBelastung] Model_Pattern CHANGED";
7.708 +(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
7.709 + "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
7.710 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
7.711 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
7.712 +(*+*)then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC CHANGED";
7.713 +(*+*) O_Model.to_string @{context} root_model;
7.714 +(*+*) O_Model.to_string @{context} o_model';
7.715 + "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";
7.716 +(*\------------------- check for entry to O_Model.complete_for -----------------------------/*)
7.717 +
7.718 + O_Model.complete_for m_patt root_model (o_model, ctxt);
7.719 +"~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) =
7.720 + (m_patt, root_model, (o_model, ctxt));
7.721 + val missing = m_patt |> filter_out
7.722 + (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor))
7.723 +;
7.724 + val add = root_model
7.725 + |> filter
7.726 + (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor)
7.727 +;
7.728 + (o_model @ add
7.729 +(*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
7.730 +(*NEW*)
7.731 + |> map (fn (_, b, c, d, e) => (b, c, d, e))
7.732 + |> add_enumerate
7.733 + |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
7.734 + ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars')) (*return from O_Model.complete_for*);
7.735 +"~~~~ from fun O_Model.complete_for \<longrightarrow>Step_Specify.by_tactic , return:"; val (o_model', ctxt') =
7.736 + ((o_model @ add)
7.737 +(*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
7.738 +(*NEW*)
7.739 + |> map (fn (_, b, c, d, e) => (b, c, d, e))
7.740 + |> add_enumerate
7.741 + |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
7.742 + ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars'));
7.743 +
7.744 +(*/------------------- check within O_Model.complete_for -------------------------------------------\*)
7.745 +(*+*) O_Model.to_string @{context} o_model';
7.746 + "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";
7.747 +(*\------------------- check within O_Model.complete_for -------------------------------------------/*)
7.748 +
7.749 +(*.NEW*) val thy = ThyC.get_theory @{context} dI
7.750 +(*.NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
7.751 +(*.NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))
7.752 +(*.NEW*) (Istate_Def.Uistate, ctxt') (pt, pos)
7.753 +;
7.754 +(*+*) I_Model.to_string @{context} i_model; "[Biegelinien, ausBelastung] I_Model CHANGED 1";
7.755 +(*+*)val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt, ...} =
7.756 +(*+*) Calc.specify_data (pt, pos);
7.757 +(*+*)pos = ([1], Met);
7.758 +
7.759 + ("ok", ([], [], (pt, pos))) (*return from Step_Specify.by_tactic*);
7.760 +"~~~ from Step_Specify.by_tactic \<longrightarrow>Step.by_tactic \<longrightarrow>fun me , return:"; val ("ok", (_, _, (pt, p))) =
7.761 + ("ok", ([], [], (pt, pos)));
7.762 +(* val ("helpless", ([(xxxxx, _, _)], _, _)) = (*case*)*)
7.763 + (* SHOULD BE \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> Add_Given "Biegelinie y" | Add_Given "AbleitungBiegelinie dy"*)
7.764 +
7.765 +val ("ok", ([( Add_Given "Biegelinie y", _, _)], [], _)) =
7.766 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
7.767 +"~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
7.768 +(*.NEW*)(*if*) on_calc_end ip (*else*);
7.769 +(*.NEW*) val (_, probl_id, _) = Calc.references (pt, p);
7.770 +(*-"-*) val _ = (*case*) tacis (*of*);
7.771 +(*.NEW*) (*if*) probl_id = Problem.id_empty (*else*);
7.772 +
7.773 +(*.NEW*)val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
7.774 + switch_specify_solve p_ (pt, ip);
7.775 +"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
7.776 + (*if*) Pos.on_specification ([], state_pos) (*then*);
7.777 +
7.778 + val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
7.779 + specify_do_next (pt, input_pos);
7.780 +"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
7.781 +
7.782 + val (_, (p_', tac)) =
7.783 + Specify.find_next_step ptp;
7.784 +"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
7.785 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
7.786 + spec = refs, ...} = Calc.specify_data (pt, pos);
7.787 + val ctxt = Ctree.get_ctxt pt pos
7.788 +;
7.789 +(*+*)O_Model.to_string @{context} oris = "[\n" ^
7.790 + "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
7.791 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
7.792 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
7.793 + "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
7.794 + "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";
7.795 +(*+*)I_Model.is_complete pbl = true;
7.796 +(*+*)I_Model.to_string @{context} met = "[\n" ^
7.797 + "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
7.798 + "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
7.799 + "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
7.800 + "(4 ,[1] ,false ,#Given ,Mis Biegelinie b_b), \n" ^
7.801 + "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";
7.802 +
7.803 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
7.804 + (*if*) p_ = Pos.Pbl (*else*);
7.805 +val return = for_method ctxt oris (o_refs, refs) (pbl, met);
7.806 +"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return);
7.807 +
7.808 + val ist_ctxt = Ctree.get_loc pt (p, p_)
7.809 + val Add_Given "Biegelinie y" = (*case*) tac (*of*);
7.810 +val return = Step_Specify.by_tactic_input tac (pt, (p, p_'));
7.811 +(*+*)val Add_Given "Biegelinie y" = tac;
7.812 + val ist_ctxt = Ctree.get_loc pt (p, p_)
7.813 + val _ = (*case*) tac (*of*);
7.814 +
7.815 + val (_, ([(Add_Given "Biegelinie y", _, _)], _, (p'''''_'', ([1], Met)))) =
7.816 +Step_Specify.by_tactic_input tac (pt, (p, p_'))
7.817 +(*/------------------- check result of Step_Specify.by_tactic_input ------------------------\*)
7.818 +(*+*)val {meth, ...} = Calc.specify_data (p'''''_'', ([1], Met));
7.819 +(*+*)I_Model.to_string @{context} meth = "[\n" ^ (* result does NOT show Add_Given "Biegelinie y" *)
7.820 + "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
7.821 + "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
7.822 + "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
7.823 + "(4 ,[1] ,false ,#Given ,Mis Biegelinie b_b), \n" ^
7.824 + "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";
7.825 +(*\------------------- check result of Step_Specify.by_tactic_input ------------------------/*)
7.826 +"~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) = (tac, (pt, (p, p_')));
7.827 +
7.828 + Specify.by_Add_ "#Given" ct ptp;
7.829 +"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);
7.830 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
7.831 + (*if*) p_ = Pos.Met (*then*);
7.832 + val (i_model, m_patt) = (met,
7.833 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
7.834 +
7.835 +val Add (4, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]), (Free ("b_b", _), [Free ("y", _)]))) =
7.836 + (*case*)
7.837 + check_single ctxt m_field oris i_model m_patt ct (*of*);
7.838 +
7.839 +(*/------------------- check for entry to check_single -------------------------------------\*)
7.840 +(*+*) O_Model.to_string @{context} oris; "[Biegelinien, ausBelastung] O_Model CHANGED for entry";
7.841 +(*+*) I_Model.to_string ctxt met; "[Biegelinien, ausBelastung] I_Model CHANGED for entry";
7.842 +(*\------------------- check for entry to check_single -------------------------------------/*)
7.843 +
7.844 +"~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
7.845 + (ctxt, sel, oris, met, ((#model o MethodC.from_store ctxt) cmI), ct);
7.846 + val SOME t = (*case*) ParseC.term_opt ctxt str (*of*);
7.847 +
7.848 +(*+*)val Const (\<^const_name>\<open>Biegelinie\<close>, _) $ Free ("y", _) = t;
7.849 +
7.850 +(*("associate_input: input ('Biegelinie y') not found in oris (typed)", (0, [], "#Given", Const (\<^const_name>\<open>Biegelinie\<close>, "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]), [])*)
7.851 + (*case*)
7.852 + contains ctxt m_field o_model t (*of*);
7.853 +"~~~~~ ~~ fun contains , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
7.854 + val ots = ((distinct op =) o flat o (map #5)) ori
7.855 + val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots
7.856 + val (d, ts) = Input_Descript.split t
7.857 + val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);
7.858 + (*if*) (subtract op = oids ids) <> [] (*else*);
7.859 + (*if*) d = TermC.empty (*else*);
7.860 + (*if*) not (subset op = (map make_typeless ts, map make_typeless ots)) (*else*);
7.861 +
7.862 + (*case*) O_Model.associate_input' ctxt sel ts ori (*of*);
7.863 +"~~~~~ ~~~ fun associate_input' , args:"; val (ctxt, sel, ts, ((id, vat, sel', d, ts') :: oris)) = (ctxt, sel, ts, ori);
7.864 +
7.865 +(*+/---------------- bypass recursion of associate_input' ----------------\*)
7.866 +(*+*)O_Model.to_string @{context} oris = "[\n" ^
7.867 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
7.868 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
7.869 + "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
7.870 + "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";
7.871 +(*+*)val (id, vat, sel', d, ts') = nth 3 oris; (* 3rd iteration *)
7.872 +(*+\---------------- bypass recursion of associate_input' ----------------/*)
7.873 +
7.874 + (*if*) sel = sel' andalso (inter op = ts ts') <> [] (*else*);
7.875 +
7.876 +(*/------------------- check within associate_input' -------------------------------\*)
7.877 +(*+*)if sel = "#Given" andalso sel' = "#Given"
7.878 +(*+*)then () else error "associate_input' Model_Pattern CHANGED";
7.879 +(*BUT: m_field can change from root-Problem to sub-MethodC --------------------vvv*)
7.880 +(* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
7.881 +(*+*)if (Problem.from_store ctxt ["vonBelastungZu", "Biegelinien"] |> #model |> Model_Pattern.to_string @{context}) = "[\"" ^
7.882 + "(#Given, (Streckenlast, q_q))\", \"" ^
7.883 + "(#Given, (FunktionsVariable, v_v))\", \"" ^
7.884 + "(#Find, (Funktionen, funs'''))\"]"
7.885 +(*+*)then () else error "associate_input' Model_Pattern of Subproblem CHANGED";
7.886 +(* root-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv ------------------------------------- \<up>*)
7.887 +(*+*)if (Problem.from_store ctxt ["Biegelinien"] |> #model |> Model_Pattern.to_string @{context}) = "[\"" ^
7.888 + "(#Given, (Traegerlaenge, l_l))\", \"" ^
7.889 + "(#Given, (Streckenlast, q_q))\", \"" ^
7.890 + "(#Find, (Biegelinie, b_b))\", \"" ^ (*------------------------------------- \<up> *)
7.891 + "(#Relate, (Randbedingungen, r_b))\"]"
7.892 +(*+*)then () else error "associate_input' Model_Pattern root-problem CHANGED";
7.893 +(* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
7.894 +(*+*)if (MethodC.from_store ctxt ["Biegelinien", "ausBelastung"] |> #model |> Model_Pattern.to_string @{context}) = "[\"" ^
7.895 + "(#Given, (Streckenlast, q__q))\", \"" ^
7.896 + "(#Given, (FunktionsVariable, v_v))\", \"" ^
7.897 + "(#Given, (Biegelinie, b_b))\", \"" ^
7.898 + "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^
7.899 + "(#Given, (Biegemoment, id_momentum))\", \"" ^
7.900 + "(#Given, (Querkraft, id_lat_force))\", \"" ^
7.901 + "(#Find, (Funktionen, fun_s))\"]"
7.902 +(*+*)then () else error "associate_input' Model_Pattern CHANGED";
7.903 +(*+*)if UnparseC.term @{context} d = "Biegelinie" andalso UnparseC.terms @{context} ts = "[y]"
7.904 +(*+*) andalso UnparseC.terms @{context} ts' = "[y]"
7.905 +(*+*)then
7.906 +(*+*) (case (inter op = ts ts') of [Free ("y", _(*"real \<Rightarrow> real"*))] => ()
7.907 +(*+*) | _ => error "check within associate_input' CHANGED 1")
7.908 +(*+*)else error "check within associate_input' CHANGED 2";
7.909 +(*\------------------- check within associate_input' -------------------------------/*)
7.910 +
7.911 +(*|------------------- contine me_Specify_Method_ausBelastung --------------------------------*)
7.912 +(*\------------------- step into me_Specify_Method_ausBelastung ----------------------------//*)
7.913 +(*[1], Met*)val (p,_,f,nxt,_,pt) = return_me_Specify_Method_ausBelastung;
7.914 + val Add_Given "Biegelinie y" = nxt
7.915 +
7.916 +(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy"= nxt
7.917 +(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegemoment M_b" = nxt
7.918 +(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querkraft Q" = nxt
7.919 +(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Biegelinien", "ausBelastung"] = nxt
7.920 +
7.921 +(*[1, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("sym_neg_equal_iff_equal", _)= nxt
7.922 +(*[1, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("Belastung_Querkraft", _)= nxt
7.923 +(*[1, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["named", "integrate", "function"])= nxt
7.924 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Model_Problem= nxt
7.925 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "functionTerm (- q_0)"= nxt
7.926 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "integrateBy x"= nxt
7.927 +;
7.928 +(*/------------------- check result of Add_Given "functionTerm (- q_0)" --------------------\*)
7.929 +if p = ([1, 3], Pbl) andalso
7.930 + f = Test_Out.PpcKF (Test_Out.Problem [], {Find = [Incompl "antiDerivativeName"],
7.931 + Given = [Correct "functionTerm (- q_0)", Incompl "integrateBy"],
7.932 + Relate = [], Where = [], With = []})
7.933 +then
7.934 + (case nxt of Add_Given "integrateBy x" => () | _ => error "specify-phase: low level CHANGED 1")
7.935 +else error "specify-phase: low level CHANGED 2";
7.936 +(*\------------------- check result of Add_Given "functionTerm (- q_0)" --------------------/*)
7.937 +
7.938 +
7.939 +\<close>
7.940 ML_file "Specify/sub-problem.sml"
7.941 ML_file "Specify/step-specify.sml"
7.942
8.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue Sep 26 15:57:12 2023 +0200
8.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Sep 27 12:17:44 2023 +0200
8.3 @@ -236,6 +236,7 @@
8.4 ML_file "Minisubpbl/150a-add-given-Maximum.sml"
8.5 ML_file "Minisubpbl/150-add-given-Equation.sml"
8.6 ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml"
8.7 + ML_file "Minisubpbl/200-start-method.sml"
8.8 ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
8.9 ML_file "Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
8.10 ML_file "Minisubpbl/300-init-subpbl.sml"
9.1 --- a/test/Tools/isac/Test_Theory.thy Tue Sep 26 15:57:12 2023 +0200
9.2 +++ b/test/Tools/isac/Test_Theory.thy Wed Sep 27 12:17:44 2023 +0200
9.3 @@ -68,659 +68,9 @@
9.4 \<close>
9.5
9.6 section \<open>===================================================================================\<close>
9.7 -section \<open>===== --> src/../lucas-interpreter.sml etc ========================================\<close>
9.8 -ML \<open>
9.9 -(*T_TESTold*)
9.10 -(*T_TEST*)
9.11 -(*T_TESTnew*)
9.12 -
9.13 -(**)
9.14 -open Ctree
9.15 -open Pos;
9.16 -open TermC;
9.17 -open Istate;
9.18 -open Tactic;
9.19 -open P_Model
9.20 -open Rewrite;
9.21 -open Step;
9.22 -open LItool;
9.23 -open LI;
9.24 -open Test_Code
9.25 -open Specify
9.26 -(**)
9.27 -open Model_Def
9.28 -(**)
9.29 -open Pre_Conds
9.30 -(**)
9.31 -open I_Model
9.32 -(**)
9.33 -\<close> ML \<open>
9.34 -\<close> ML \<open> (*\<longrightarrow> pre_conditions.sml | ? model-def.sml ?*)
9.35 -(*T_TESTold* )
9.36 -fun max_variants i_model =
9.37 - let
9.38 - val all_variants =
9.39 - map (fn (_, variants, _, _, _) => variants) i_model
9.40 - |> flat
9.41 - |> distinct op =
9.42 - val variants_separated = map (filter_variants' i_model) all_variants
9.43 - val sums_corr = map (cnt_corrects) variants_separated
9.44 - val sum_variant_s = arrange_args sums_corr (1, all_variants)
9.45 -
9.46 - val max_first = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
9.47 - val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
9.48 - |> map snd
9.49 - val option_sequence = map
9.50 - (fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s
9.51 -(*das ist UNSINN'+ UNNOETIG WEGLASSEN, .., siehe (*+*)if (pbl_max_imos*)
9.52 - val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>
9.53 - if is_some pos_in_sum_variant_s then i_model else [])
9.54 - (option_sequence ~~ variants_separated)
9.55 - |> filter_out (fn place_holder => place_holder = []);
9.56 -(*/-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------\ * )
9.57 - PROBALBY FOR RE-USE:
9.58 - val option_sequence = map
9.59 - (fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s
9.60 - val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>
9.61 - if is_some pos_in_sum_variant_s then i_model else [])
9.62 - (option_sequence ~~ variants_separated)
9.63 - |> filter_out (fn place_holder => place_holder = []);
9.64 - \<longrightarrow> [
9.65 - [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])],
9.66 - [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])]]
9.67 ------- ----------------------------------------------------------------------------------------
9.68 - val equal_descr_pairs = map (get_equal_descr (hd max_i_models)) model_patt
9.69 - |> flat (*a hack for continuing ------------^^-- "turn to PIDE", works for test example*)
9.70 - val env_model = make_env_model equal_descr_pairs
9.71 - val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
9.72 - val subst_eval_list = make_envs_preconds equal_givens
9.73 - val (env_subst, env_eval) = split_list subst_eval_list
9.74 -( *\-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *)
9.75 - in
9.76 - ((maxes, max_i_models)(*, env_model, (env_subst, env_eval)*))
9.77 -(* (maxes, max_i_models)*)
9.78 -(*/-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------\ * )
9.79 - (env_model, (env_subst, env_eval)
9.80 -( *\--fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *)
9.81 - end
9.82 -;
9.83 -(*of_max_variant*)
9.84 - max_variants: (*Model_Pattern.T -> *) Model_Def.i_model_TEST ->
9.85 - (variant list * Model_Def.i_model_TEST list)(* * Env.T * (env_subst * env_eval)*)
9.86 -;
9.87 -( *T_TEST*)
9.88 -(*in case of i_model max_variants = [] we take of o_model all_variants *)
9.89 -fun max_variants o_model i_model =
9.90 - let
9.91 - val all_variants =
9.92 - map (fn (_, variants, _, _, _) => variants) i_model
9.93 - |> flat
9.94 - |> distinct op =
9.95 - val variants_separated = map (filter_variants' i_model) all_variants
9.96 - val sums_corr = map (cnt_corrects) variants_separated
9.97 - val sum_variant_s = arrange_args sums_corr (1, all_variants)
9.98 -
9.99 - val max_first = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
9.100 - val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
9.101 - |> map snd
9.102 - in
9.103 - if maxes = []
9.104 - then map (fn (_, variants, _, _, _) => variants) o_model
9.105 - |> flat
9.106 - |> distinct op =
9.107 - else maxes
9.108 - end
9.109 -;
9.110 - max_variants: Model_Def.o_model -> Model_Def.i_model_TEST -> variants
9.111 -(*T_TESTnew*)
9.112 -\<close> ML \<open>
9.113 -\<close> ML \<open> (*\<longrightarrow> pre-conditions.sml*)
9.114 -\<close> ML \<open>
9.115 -fun get_dscr' (Cor_TEST (descr, _)) = SOME descr
9.116 - | get_dscr' (Inc_TEST (descr, _)) = SOME descr
9.117 - | get_dscr' (Sup_TEST (descr, _)) = SOME descr
9.118 - | get_dscr' _ = NONE
9.119 - (*other feedback cannot contribute to I_Model.mk_env_TEST and Pre_Conds.mk_env_TEST*)
9.120 -(* get_descr: I_Model.single_TEST -> descriptor option*)
9.121 -;
9.122 -get_dscr': feedback_TEST -> descriptor option
9.123 -\<close> ML \<open>
9.124 -fun get_descr (_, _, _, _, (feedb, _)) =
9.125 - case get_dscr' feedb of NONE => NONE | some_descr => some_descr
9.126 -;
9.127 -get_descr: single_TEST -> descriptor option;
9.128 -
9.129 -\<close> ML \<open>
9.130 -fun get_descr_vnt descr vnts i_model =
9.131 - let
9.132 - val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false
9.133 - | SOME descr' => if descr = descr' then true else false) i_model
9.134 - in
9.135 - case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
9.136 - [] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
9.137 - | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
9.138 - end
9.139 -;
9.140 -get_descr_vnt: descriptor -> variants -> T_TEST -> single_TEST
9.141 -\<close> ML \<open>
9.142 -\<close> ML \<open> (*\<longrightarrow> i-model.sml*)
9.143 -\<close> ML \<open>
9.144 -fun transfer_terms (i, vnts, m_field, descr, ts) =
9.145 - (i, vnts, true, m_field, (Cor_TEST (descr, ts), Position.none))
9.146 -;
9.147 -transfer_terms: O_Model.single -> I_Model.single_TEST
9.148 -\<close> ML \<open>
9.149 -(*
9.150 - get an appropriate (description, variant) item from o_model;
9.151 - called in case of item in met_imod is_empty_single_TEST
9.152 - (i.e. was not transferred pbl_mod by \<open>fun get_descr_vnt\<close>).
9.153 -*)
9.154 -fun get_descr_vnt' feedb vnts o_model =
9.155 - filter (fn (_, vnts', _, descr', _) =>
9.156 - case get_dscr' feedb of
9.157 - SOME descr => if descr' = descr andalso inter op= vnts' vnts <> [] then true else false
9.158 - | NONE => false) o_model
9.159 -;
9.160 -get_descr_vnt': feedback_TEST -> variants -> O_Model.T -> O_Model.T
9.161 -\<close> ML \<open>
9.162 -fun msg vnts feedb = "get_descr_vnt' returns NONE: i.e. it does not find an item of o_model with\n" ^
9.163 - "variants " ^ ints2str' vnts ^ " and descriptor " ^
9.164 - (feedb |> get_dscr' |> the |> UnparseC.term (ContextC.for_ERROR ()))
9.165 -;
9.166 -msg: variants -> feedback_TEST -> string
9.167 -\<close> ML \<open>
9.168 -fun fill_method o_model pbl_imod met_patt =
9.169 - let
9.170 - val pbl_max_vnts = max_variants o_model pbl_imod;
9.171 - val from_pbl = map (fn (_, (descr, _)) => get_descr_vnt descr pbl_max_vnts pbl_imod) met_patt
9.172 - val from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
9.173 - if is_empty_single_TEST i_single
9.174 - then
9.175 - case get_descr_vnt' feedb pbl_max_vnts o_model of
9.176 - [] => raise ERROR (msg pbl_max_vnts feedb)
9.177 - | o_singles => map transfer_terms o_singles
9.178 - else [i_single (*fetched before from pbl_imod*)])) from_pbl
9.179 - in
9.180 - from_o_model |> flat
9.181 - end
9.182 -;
9.183 -fill_method: O_Model.T -> T_TEST -> Model_Pattern.T -> T_TEST
9.184 -\<close> ML \<open>
9.185 -\<close> ML \<open>
9.186 -\<close> ML \<open> (* \<longrightarrow> i-model.sml*)
9.187 -\<close> ML \<open>
9.188 -fun s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt) =
9.189 - let
9.190 - val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
9.191 - val i_from_pbl = map (fn (_, (descr, _)) =>
9.192 - Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
9.193 - val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
9.194 - if is_empty_single_TEST i_single
9.195 - then
9.196 - case get_descr_vnt' feedb pbl_max_vnts o_model of
9.197 - [] => raise ERROR (msg pbl_max_vnts feedb)
9.198 - | o_singles => map transfer_terms o_singles
9.199 - else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
9.200 -
9.201 - val i_from_met = map (fn (_, (descr, _)) =>
9.202 - Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
9.203 - val met_max_vnts = Model_Def.max_variants o_model i_from_met;
9.204 - val max_vnt = hd met_max_vnts (*need only one for solve-phase*)
9.205 -
9.206 - val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
9.207 - if is_empty_single_TEST i_single
9.208 - then
9.209 - case get_descr_vnt' feedb [max_vnt] o_model of
9.210 - [] => raise ERROR (msg [max_vnt] feedb)
9.211 - | o_singles => map transfer_terms o_singles
9.212 - else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
9.213 - in
9.214 - (filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) pbl_from_o_model,
9.215 - met_from_pbl)
9.216 - end
9.217 -\<close> ML \<open>
9.218 -;
9.219 -s_make_complete: O_Model.T -> I_Model.T_TEST * I_Model.T_TEST -> Model_Pattern.T * Model_Pattern.T ->
9.220 - I_Model.T_TEST * I_Model.T_TEST
9.221 -\<close> ML \<open>
9.222 -\<close> ML \<open>
9.223 -\<close> ML \<open>
9.224 -\<close> ML \<open> (*\<longrightarrow> lucas-interpreter.sml*)
9.225 -fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
9.226 - let
9.227 - (*done in src*)
9.228 - in
9.229 - ("ok", Calc.state_empty_post)
9.230 - end
9.231 -;
9.232 -by_tactic: Tactic.T -> Istate.T * Proof.context -> Calc.T -> string * Calc.state_post
9.233 -\<close> ML \<open>
9.234 -\<close>
9.235 -
9.236 -section \<open>===================================================================================\<close>
9.237 -section \<open>===== i-model.sml .s_complete =====================================================\<close>
9.238 +section \<open>===== ============================================================================\<close>
9.239 ML \<open>
9.240 \<close> ML \<open>
9.241 -"----------- build I_Model.s_make_complete -----------------------------------------------------";
9.242 -"----------- build I_Model.s_make_complete -----------------------------------------------------";
9.243 -"----------- build I_Model.s_make_complete -----------------------------------------------------";
9.244 -\<close> ML \<open>
9.245 -(*---vvvvv these would overwrite above definition ^^^* )
9.246 -open Ctree
9.247 -open Pos;
9.248 -open TermC;
9.249 -open Istate;
9.250 -open Tactic;
9.251 -open P_Model
9.252 -open Rewrite;
9.253 -open Step;
9.254 -open LItool;
9.255 -open LI;
9.256 -open Test_Code
9.257 -open Specify
9.258 -open Model_Def
9.259 -open Pre_Conds;
9.260 -open I_Model;
9.261 -( **)
9.262 -
9.263 -val (_(*example text*),
9.264 - (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
9.265 - "Extremum (A = 2 * u * v - u \<up> 2)" ::
9.266 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
9.267 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
9.268 - "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: (*INCORRECT 2 / v*)
9.269 -(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
9.270 - "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
9.271 - "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
9.272 - "ErrorBound (\<epsilon> = (0::real))" :: []),
9.273 - refs as ("Diff_App",
9.274 - ["univariate_calculus", "Optimisation"],
9.275 - ["Optimisation", "by_univariate_calculus"])))
9.276 - = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
9.277 -
9.278 -val c = [];
9.279 -val (p,_,f,nxt,_,pt) =
9.280 - Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
9.281 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.282 -\<close> ML \<open>
9.283 -\<close> ML \<open> (*//----------- setup test data for I_Model.s_make_complete -------------------------\\*)
9.284 -(*//------------------ setup test data for I_Model.s_make_complete -------------------------\\*)
9.285 -val (o_model, (pbl_imod, met_imod), (pI, mI)) = case get_obj I pt (fst p) of
9.286 - PblObj {meth = met_imod, origin = (o_model, (_, pI, mI), _), probl = pbl_imod, ...}
9.287 - => (o_model, (pbl_imod, met_imod), (pI, mI))
9.288 - | _ => raise ERROR ""
9.289 -\<close> ML \<open>
9.290 -val {model = pbl_patt, ...} = Problem.from_store ctxt pI;
9.291 -val {model = met_patt, ...} = MethodC.from_store ctxt mI;
9.292 -\<close> ML \<open>
9.293 -val pbl_imod = [ (*2 items for creating code ---> variants [1, 2]*)
9.294 - (1, [1, 2, 3], true, "#undef", (Cor_TEST (@{term Constants},
9.295 - [@{term "[r = (7::real)]"}]), Position.none)),
9.296 - (1, [1, 2], true, "#undef", (Cor_TEST (@{term SideConditions},
9.297 - [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]), Position.none))]
9.298 -\<close> ML \<open>
9.299 -val met_imod = [ (*1 item for creating code*)
9.300 -(8, [2], true, "#undef", (Cor_TEST (@{term FunctionVariable}, [@{term "b::real"}]), Position.none))]
9.301 -\<close> ML \<open>
9.302 -(*+*)if (o_model |> O_Model.to_string @{context}) = "[\n" ^
9.303 -(*+*) "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
9.304 -(*+*) "(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n" ^
9.305 -(*+*) "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
9.306 -(*+*) "(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
9.307 -(*+*) "(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
9.308 -(*+*) "(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
9.309 -(*+*) "(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n" ^
9.310 -(*+*) "(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n" ^
9.311 -(*+*) "(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n" ^
9.312 -(*+*) "(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
9.313 -(*+*) "(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
9.314 -(*+*) "(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
9.315 -then () else error "setup test data for I_Model.s_make_complete CHANGED";
9.316 -(*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)
9.317 -\<close> ML \<open> (*\\----------- setup test data for I_Model.s_make_complete -------------------------//*)
9.318 -\<close> ML \<open>
9.319 -val return_s_make_complete =
9.320 - s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt);
9.321 -\<close> ML \<open> (*/------------ step into s_make_complete -------------------------------------------\\*)
9.322 -(*/------------------- step into s_make_complete -------------------------------------------\\*)
9.323 -"~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt)) =
9.324 - (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt));
9.325 -\<close> ML \<open>
9.326 - val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
9.327 -\<close> ML \<open>
9.328 - val i_from_pbl = map (fn (_, (descr, _)) =>
9.329 - Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
9.330 -\<close> ML \<open> (*//----------- step into get_descr_vnt ---------------------------------------------\\*)
9.331 -(*//------------------ step into get_descr_vnt ---------------------------------------------\\*)
9.332 -"~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =
9.333 - (@{term Constants}, pbl_max_vnts, pbl_imod);
9.334 -\<close> ML \<open>
9.335 - val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false
9.336 - | SOME descr' => if descr = descr' then true else false) i_model
9.337 -\<close> ML \<open>
9.338 -(*+*)filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr
9.339 -(*+*): I_Model.T_TEST
9.340 -\<close> ML \<open>
9.341 -val return_get_descr_vnt_1 =
9.342 - case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
9.343 - [] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
9.344 - | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
9.345 -(*\\------------------ step into get_descr_vnt ---------------------------------------------//*)
9.346 -\<close> ML \<open> (*\\----------- step into get_descr_vnt ---------------------------------------------//*)
9.347 -\<close> ML \<open>
9.348 -\<close> ML \<open> (*|------------ continue s_make_complete ----------------------------------------------*)
9.349 -(*|------------------- continue s_make_complete ----------------------------------------------*)
9.350 -\<close> ML \<open>
9.351 - val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
9.352 - if is_empty_single_TEST i_single
9.353 - then
9.354 - case get_descr_vnt' feedb pbl_max_vnts o_model of
9.355 -(*-----------^^^^^^^^^^^^^^-----------------------------*)
9.356 - [] => raise ERROR (msg pbl_max_vnts feedb)
9.357 - | o_singles => map transfer_terms o_singles
9.358 - else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
9.359 -\<close> ML \<open>
9.360 -(*+*)val [2, 1] = vnts;
9.361 -(*+*)if (pbl_from_o_model |> I_Model.to_string_TEST @{context}) = "[\n" ^
9.362 - "(1, [1, 2, 3], true ,#undef, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
9.363 - "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
9.364 - "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
9.365 - "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
9.366 - "(1, [1, 2], true ,#undef, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
9.367 -then () else error "pbl_from_o_model CHANGED"
9.368 -\<close> ML \<open>
9.369 -\<close> ML \<open>
9.370 -\<close> ML \<open> (*//----------- step into map ((fn i_single -----------------------------------------\\*)
9.371 -(*//------------------ step into map ((fn i_single -----------------------------------------\\*)
9.372 -"~~~~~ fun map ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) = (nth 1 i_from_pbl);
9.373 - (*if*) is_empty_single_TEST i_single (*else*);
9.374 - get_descr_vnt' feedb pbl_max_vnts o_model;
9.375 -
9.376 - val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
9.377 - if is_empty_single_TEST i_single
9.378 - then
9.379 - case get_descr_vnt' feedb pbl_max_vnts o_model of
9.380 -(*---------- ^^^^^^^^^^^^^^ ----------------------------*)
9.381 - [] => raise ERROR (msg pbl_max_vnts feedb)
9.382 - | o_singles => map transfer_terms o_singles
9.383 - else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
9.384 -\<close> ML \<open>
9.385 -\<close> ML \<open> (*\\----------- step into map ((fn i_single -----------------------------------------//*)
9.386 -(*\\------------------ step into map ((fn i_single -----------------------------------------//*)
9.387 -
9.388 -\<close> ML \<open> (*|------------ continue s_make_complete ----------------------------------------------*)
9.389 -(*|------------------- continue s_make_complete ----------------------------------------------*)
9.390 -\<close> ML \<open>
9.391 - val i_from_met = map (fn (_, (descr, _)) =>
9.392 - Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
9.393 -\<close> ML \<open>
9.394 -(*+*)if (i_from_met |> I_Model.to_string_TEST @{context}) = "[\n" ^
9.395 - "(0, [], false ,i_model_empty, (Sup_TEST Constants [], Position.T)), \n" ^
9.396 - "(0, [], false ,i_model_empty, (Sup_TEST Maximum, Position.T)), \n" ^
9.397 - "(0, [], false ,i_model_empty, (Sup_TEST Extremum, Position.T)), \n" ^
9.398 - "(0, [], false ,i_model_empty, (Sup_TEST SideConditions [], Position.T)), \n" ^
9.399 - "(8, [2], true ,#undef, (Cor_TEST FunctionVariable b , pen2str, Position.T)), \n" ^
9.400 -(*---there is 1 item already input -^^^^^^^^^^^^^^^^^^*)
9.401 - "(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n" ^
9.402 - "(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n" ^
9.403 - "(0, [], false ,i_model_empty, (Sup_TEST AdditionalValues [], Position.T))]"
9.404 -(*+*)then () else error "s_make_complete: from_met CHANGED";
9.405 -\<close> ML \<open>
9.406 - val met_max_vnts = Model_Def.max_variants o_model i_from_met;
9.407 -(*+*)val [2] = met_max_vnts
9.408 -\<close> ML \<open>
9.409 - val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)
9.410 -\<close> ML \<open>
9.411 - val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
9.412 - if is_empty_single_TEST i_single
9.413 - then
9.414 - case get_descr_vnt' feedb [met_max_vnt] o_model of
9.415 - [] => raise ERROR (msg [met_max_vnt] feedb)
9.416 - | o_singles => map transfer_terms o_singles
9.417 - else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
9.418 -\<close> ML \<open>
9.419 -(*+*)if (met_from_pbl |> I_Model.to_string_TEST @{context}) = "[\n" ^
9.420 - "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
9.421 - "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
9.422 - "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
9.423 - "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
9.424 - "(8, [2], true ,#undef, (Cor_TEST FunctionVariable b , pen2str, Position.T)), \n" ^
9.425 - "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
9.426 - "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
9.427 - "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
9.428 -(*+*)then () else error "s_make_complete: met_from_pbl CHANGED";
9.429 -\<close> ML \<open>
9.430 -val return_s_make_complete_step = (pbl_from_o_model, met_from_pbl)
9.431 -\<close> ML \<open> (*\------------ step into s_make_complete -------------------------------------------//*)
9.432 -(*\------------------- step into s_make_complete -------------------------------------------//*)
9.433 -if return_s_make_complete = return_s_make_complete_step
9.434 -then () else error "s_make_complete: stewise construction <> value of fun"
9.435 -\<close> ML \<open>
9.436 -\<close>
9.437 -
9.438 -section \<open>===================================================================================\<close>
9.439 -section \<open>===== i-model.sml .s_make_complete [][] ===========================================\<close>
9.440 -ML \<open>
9.441 -\<close> ML \<open>
9.442 -(* most general case: user activates some <complete specification> *)
9.443 -\<close> ML \<open>
9.444 -(*---vvvvv these would overwrite above definition ^^^* )
9.445 -open Ctree
9.446 -open Pos;
9.447 -open TermC;
9.448 -open Istate;
9.449 -open Tactic;
9.450 -open P_Model
9.451 -open Rewrite;
9.452 -open Step;
9.453 -open LItool;
9.454 -open LI;
9.455 -open Test_Code
9.456 -open Specify
9.457 -open Model_Def
9.458 -open Pre_Conds;
9.459 -open I_Model;
9.460 -( **)
9.461 -
9.462 -val (_(*example text*),
9.463 - (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
9.464 - "Extremum (A = 2 * u * v - u \<up> 2)" ::
9.465 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
9.466 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
9.467 - "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: (*INCORRECT 2 / v*)
9.468 -(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
9.469 - "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
9.470 - "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
9.471 - "ErrorBound (\<epsilon> = (0::real))" :: []),
9.472 - refs as ("Diff_App",
9.473 - ["univariate_calculus", "Optimisation"],
9.474 - ["Optimisation", "by_univariate_calculus"])))
9.475 - = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
9.476 -
9.477 -val c = [];
9.478 -val (p,_,f,nxt,_,pt) =
9.479 - Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
9.480 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.481 -
9.482 -(*//------------------ setup test data for I_Model.s_make_complete -------------------------\\*)
9.483 -val (o_model, (pI, mI)) = case get_obj I pt (fst p) of
9.484 - PblObj {origin = (o_model, (_, pI, mI), _), ...}
9.485 - => (o_model, (pI, mI))
9.486 - | _ => raise ERROR ""
9.487 -
9.488 -val {model = pbl_patt, ...} = Problem.from_store ctxt pI;
9.489 -val {model = met_patt, ...} = MethodC.from_store ctxt mI;
9.490 -val pbl_imod = []
9.491 -val met_imod = []
9.492 -;
9.493 -(*+*)if (o_model |> O_Model.to_string @{context}) = "[\n" ^
9.494 -(*+*) "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
9.495 -(*+*) "(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n" ^
9.496 -(*+*) "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
9.497 -(*+*) "(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
9.498 -(*+*) "(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
9.499 -(*+*) "(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
9.500 -(*+*) "(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n" ^
9.501 -(*+*) "(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n" ^
9.502 -(*+*) "(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n" ^
9.503 -(*+*) "(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
9.504 -(*+*) "(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
9.505 -(*+*) "(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
9.506 -then () else error "setup test data for I_Model.s_make_complete CHANGED";
9.507 -(*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)
9.508 -\<close> ML \<open> (*\\----------- setup test data for I_Model.s_make_complete -------------------------//*)
9.509 -\<close> ML \<open>
9.510 -val return_s_make_complete =
9.511 - s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt);
9.512 -\<close> ML \<open> (*/------------ step into s_make_complete -------------------------------------------\\*)
9.513 -(*/------------------- step into s_make_complete -------------------------------------------\\*)
9.514 -"~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt)) =
9.515 - (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt));
9.516 -\<close> ML \<open>
9.517 - val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
9.518 -\<close> ML \<open>
9.519 - val i_from_pbl = map (fn (_, (descr, _)) =>
9.520 - Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
9.521 -\<close> ML \<open> (*//----------- step into get_descr_vnt ---------------------------------------------\\*)
9.522 -(*//------------------ step into get_descr_vnt ---------------------------------------------\\*)
9.523 -"~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =
9.524 - (@{term Constants}, pbl_max_vnts, pbl_imod);
9.525 -\<close> ML \<open>
9.526 - val equal_descr(*for (*+*)filter (fn (_, vnts',..*): I_Model.T_TEST =
9.527 - filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false
9.528 - | SOME descr' => if descr = descr' then true else false) i_model
9.529 -\<close> ML \<open>
9.530 -(*+*)filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) (equal_descr: I_Model.T_TEST)
9.531 -(*+*): I_Model.T_TEST
9.532 -\<close> ML \<open>
9.533 -val return_get_descr_vnt_1 =
9.534 - case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
9.535 - [] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
9.536 - | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
9.537 -(*\\------------------ step into get_descr_vnt ---------------------------------------------//*)
9.538 -\<close> ML \<open> (*\\----------- step into get_descr_vnt ---------------------------------------------//*)
9.539 -\<close> ML \<open>
9.540 -(*+*)if return_get_descr_vnt_1 = nth 1 i_from_pbl
9.541 -(*+*)then () else error "return_get_descr_vnt_1 <> nth 1 i_from_pbl";
9.542 -\<close> ML \<open>
9.543 -(*+*)if (i_from_pbl |> I_Model.to_string_TEST @{context}) = "[\n" ^
9.544 - "(0, [], false ,i_model_empty, (Sup_TEST Constants [], Position.T)), \n" ^
9.545 - "(0, [], false ,i_model_empty, (Sup_TEST Maximum, Position.T)), \n" ^
9.546 - "(0, [], false ,i_model_empty, (Sup_TEST AdditionalValues [], Position.T)), \n" ^
9.547 - "(0, [], false ,i_model_empty, (Sup_TEST Extremum, Position.T)), \n" ^
9.548 - "(0, [], false ,i_model_empty, (Sup_TEST SideConditions [], Position.T))]"
9.549 -(*+*)then () else error "I_Model.s_make_complete > i_from_pbl CHANGED";
9.550 -\<close> ML \<open>
9.551 -\<close> ML \<open> (*|------------ continue s_make_complete ----------------------------------------------*)
9.552 -(*|------------------- continue s_make_complete ----------------------------------------------*)
9.553 -\<close> ML \<open>
9.554 - val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
9.555 - if is_empty_single_TEST i_single
9.556 - then
9.557 - case get_descr_vnt' feedb pbl_max_vnts o_model of
9.558 -(*-----------^^^^^^^^^^^^^^-----------------------------*)
9.559 - [] => raise ERROR (msg pbl_max_vnts feedb)
9.560 - | o_singles => map transfer_terms o_singles
9.561 - else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
9.562 -\<close> ML \<open>
9.563 -(*+*)val [1, 2, 3] = vnts;
9.564 -(*+*)if (pbl_from_o_model |> I_Model.to_string_TEST @{context}) = "[\n" ^
9.565 - "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
9.566 - "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
9.567 - "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
9.568 - "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
9.569 - "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
9.570 - "(6, [3], true ,#Relate, (Cor_TEST SideConditions [u / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>] , pen2str, Position.T))]"
9.571 -then () else error "pbl_from_o_model CHANGED"
9.572 -\<close> ML \<open>
9.573 -\<close> ML \<open>
9.574 -\<close> ML \<open> (*//----------- step into map ((fn i_single -----------------------------------------\\*)
9.575 -(*//------------------ step into map ((fn i_single -----------------------------------------\\*)
9.576 -"~~~~~ fun map nth 1 ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) =
9.577 - (nth 1 i_from_pbl);
9.578 - (*if*) is_empty_single_TEST i_single (*then*);
9.579 - (*case*) get_descr_vnt' feedb pbl_max_vnts o_model;
9.580 -\<close> ML \<open>
9.581 -(*+*)val (0, [], false, "i_model_empty", (Sup_TEST (Const ("Input_Descript.Constants", _), []), _))
9.582 - = i_single
9.583 -(*+*)val true = is_empty_single_TEST i_single
9.584 -\<close> ML \<open>
9.585 -val return_get_descr_vnt'= (*case*)
9.586 - get_descr_vnt' feedb pbl_max_vnts o_model (*of*);
9.587 -\<close> ML \<open> (*\\----------- step into map ((fn i_single -----------------------------------------//*)
9.588 -(*\\------------------ step into map ((fn i_single -----------------------------------------//*)
9.589 -
9.590 -\<close> ML \<open> (*|------------ continue s_make_complete ----------------------------------------------*)
9.591 -(*|------------------- continue s_make_complete ----------------------------------------------*)
9.592 -\<close> ML \<open>
9.593 - val i_from_met = map (fn (_, (descr, _)) =>
9.594 - Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
9.595 -\<close> ML \<open>
9.596 -(*+*)val [1, 2, 3] = pbl_max_vnts (*..? ? GOON*)
9.597 -\<close> ML \<open>
9.598 -(*+*)if (i_from_met |> I_Model.to_string_TEST @{context}) = "[\n" ^
9.599 - "(0, [], false ,i_model_empty, (Sup_TEST Constants [], Position.T)), \n" ^
9.600 - "(0, [], false ,i_model_empty, (Sup_TEST Maximum, Position.T)), \n" ^
9.601 - "(0, [], false ,i_model_empty, (Sup_TEST Extremum, Position.T)), \n" ^
9.602 - "(0, [], false ,i_model_empty, (Sup_TEST SideConditions [], Position.T)), \n" ^
9.603 - "(0, [], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n" ^
9.604 - "(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n" ^
9.605 - "(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n" ^
9.606 - "(0, [], false ,i_model_empty, (Sup_TEST AdditionalValues [], Position.T))]"
9.607 -(*+*)then () else error "s_make_complete: i_from_met CHANGED";
9.608 -\<close> ML \<open>
9.609 - val met_max_vnts = Model_Def.max_variants o_model i_from_met;
9.610 -(*+*)val [1, 2, 3]: variant list = met_max_vnts
9.611 -\<close> ML \<open>
9.612 - val max_vnt = hd met_max_vnts (*need only one for solve-phase*)
9.613 -\<close> ML \<open>
9.614 - val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
9.615 - if is_empty_single_TEST i_single
9.616 - then
9.617 - case get_descr_vnt' feedb [max_vnt] o_model of
9.618 - [] => raise ERROR (msg [max_vnt] feedb)
9.619 - | o_singles => map transfer_terms o_singles
9.620 - else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
9.621 -\<close> ML \<open>
9.622 -(*+*)val 1 = max_vnt;
9.623 -(*+*)if (met_from_pbl |> I_Model.to_string_TEST @{context}) = "[\n" ^
9.624 - "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
9.625 - "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
9.626 - "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
9.627 - "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
9.628 - "(7, [1], true ,#undef, (Cor_TEST FunctionVariable a , pen2str, Position.T)), \n" ^
9.629 - "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
9.630 - "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
9.631 - "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
9.632 -(*+*)then () else error "s_make_complete: met_from_pbl CHANGED";
9.633 -\<close> ML \<open>
9.634 -\<close> ML \<open>
9.635 -val return_s_make_complete_step as (pbl_imod_step, met_imod_step)=
9.636 - (filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) pbl_from_o_model,
9.637 - met_from_pbl)
9.638 -\<close> ML \<open> (*\------------ step into s_make_complete -------------------------------------------//*)
9.639 -(*\------------------- step into s_make_complete -------------------------------------------//*)
9.640 -if return_s_make_complete = return_s_make_complete_step
9.641 -then () else error "s_make_complete: stewise construction <> value of fun"
9.642 -;
9.643 -(* final test ... ----------------------------------------------------------------------------*)
9.644 -(pbl_imod_step |> I_Model.to_string_TEST @{context},
9.645 - met_imod_step |> I_Model.to_string_TEST @{context}) =
9.646 - ("[\n" ^
9.647 - "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
9.648 - "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
9.649 - "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
9.650 - "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
9.651 - "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]",
9.652 - "[\n" ^
9.653 - "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
9.654 - "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
9.655 - "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
9.656 - "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
9.657 - "(7, [1], true ,#undef, (Cor_TEST FunctionVariable a , pen2str, Position.T)), \n" ^
9.658 - "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
9.659 - "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
9.660 - "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]")
9.661
9.662 \<close> ML \<open>
9.663 \<close>