1.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Oct 02 12:02:59 2023 +0200
1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Oct 02 15:39:22 2023 +0200
1.3 @@ -266,10 +266,189 @@
1.4 ML_file "Specify/formalise.sml"
1.5 ML_file "Specify/o-model.sml"
1.6 ML_file "Specify/i-model.sml" (* (BROKEN!) test on elementwise input to lists*)
1.7 +ML \<open>
1.8 +\<close> ML \<open>
1.9 +"----------- build I_Model.s_make_complete -----------------------------------------------------";
1.10 +"----------- build I_Model.s_make_complete -----------------------------------------------------";
1.11 +"----------- build I_Model.s_make_complete -----------------------------------------------------";
1.12 +val (_(*example text*),
1.13 + (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
1.14 + "Extremum (A = 2 * u * v - u \<up> 2)" ::
1.15 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
1.16 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
1.17 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: (*INCORRECT 2 / v*)
1.18 +(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
1.19 + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
1.20 + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
1.21 + "ErrorBound (\<epsilon> = (0::real))" :: []),
1.22 + refs as ("Diff_App",
1.23 + ["univariate_calculus", "Optimisation"],
1.24 + ["Optimisation", "by_univariate_calculus"])))
1.25 + = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
1.26 +
1.27 +val c = [];
1.28 +val (p,_,f,nxt,_,pt) =
1.29 + Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
1.30 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.31 +
1.32 +(*//------------------ setup test data for I_Model.s_make_complete -------------------------\\*)
1.33 +val (o_model, (pbl_imod, met_imod), (pI, mI)) = case get_obj I pt (fst p) of
1.34 + PblObj {meth = met_imod, origin = (o_model, (_, pI, mI), _), probl = pbl_imod, ...}
1.35 + => (o_model, (pbl_imod, met_imod), (pI, mI))
1.36 + | _ => raise ERROR ""
1.37 +
1.38 +val pbl_imod = [ (*2 items for creating code ---> variants [1, 2]*)
1.39 + (1, [1, 2, 3], true, "#undef", (Cor_TEST (@{term Constants},
1.40 + [@{term "[r = (7::real)]"}]), Position.none)),
1.41 + (1, [1, 2], true, "#undef", (Cor_TEST (@{term SideConditions},
1.42 + [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]), Position.none))]
1.43 +
1.44 +val met_imod = [ (*1 item for creating code*)
1.45 +(8, [2], true, "#undef", (Cor_TEST (@{term FunctionVariable}, [@{term "b::real"}]), Position.none))]
1.46 +;
1.47 +(*+*)if (o_model |> O_Model.to_string @{context}) = "[\n" ^
1.48 +(*+*) "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
1.49 +(*+*) "(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n" ^
1.50 +(*+*) "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
1.51 +(*+*) "(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
1.52 +(*+*) "(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
1.53 +(*+*) "(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
1.54 +(*+*) "(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n" ^
1.55 +(*+*) "(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n" ^
1.56 +(*+*) "(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n" ^
1.57 +(*+*) "(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
1.58 +(*+*) "(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
1.59 +(*+*) "(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
1.60 +then () else error "setup test data for I_Model.s_make_complete CHANGED";
1.61 +(*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)
1.62 +
1.63 +val return_s_make_complete =
1.64 + s_make_complete ctxt o_model (pbl_imod, met_imod) (pI, mI);
1.65 +(*/------------------- step into s_make_complete -------------------------------------------\\*)
1.66 +"~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pI, mI)) =
1.67 + (o_model, (pbl_imod, met_imod), (pI, mI));
1.68 + val {model = pbl_patt, ...} = Problem.from_store ctxt pbl_id;
1.69 + val {model = met_patt, ...} = MethodC.from_store ctxt met_id;
1.70 + val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
1.71 + val i_from_pbl = map (fn (_, (descr, _)) =>
1.72 + Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
1.73 +\<close> ML \<open>
1.74 +val [] = i_from_pbl
1.75 +\<close> ML \<open>
1.76 +
1.77 +(*//------------------ step into get_descr_vnt ---------------------------------------------\\*)
1.78 +"~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =
1.79 + (@{term Constants}, pbl_max_vnts, pbl_imod);
1.80 + val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false
1.81 + | SOME descr' => if descr = descr' then true else false) i_model
1.82 +;
1.83 +(*+*)filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr: I_Model.T_TEST
1.84 +;
1.85 +val return_get_descr_vnt_1 =
1.86 + case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
1.87 + [] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
1.88 + | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
1.89 +(*\\------------------ step into get_descr_vnt ---------------------------------------------//*)
1.90 +\<close> ML \<open>
1.91 +\<close> ML \<open>
1.92 +
1.93 +(*|------------------- continue s_make_complete ----------------------------------------------*)
1.94 + val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
1.95 + if is_empty_single_TEST i_single
1.96 + then
1.97 + case get_descr_vnt' feedb pbl_max_vnts o_model of
1.98 +(*-----------^^^^^^^^^^^^^^-----------------------------*)
1.99 + [] => raise ERROR (msg pbl_max_vnts feedb)
1.100 + | o_singles => map transfer_terms o_singles
1.101 + else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
1.102 +
1.103 +\<close> ML \<open>
1.104 +(*+*)val [2, 1] = vnts;
1.105 +\<close> ML \<open>
1.106 +val "[]" = (pbl_from_o_model |> I_Model.to_string_TEST @{context})
1.107 +\<close> ML \<open>
1.108 +(*+*)if (pbl_from_o_model |> I_Model.to_string_TEST @{context}) = "[\n" ^
1.109 + "(1, [1, 2, 3], true ,#undef, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
1.110 + "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
1.111 + "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
1.112 + "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
1.113 + "(1, [1, 2], true ,#undef, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
1.114 +then () else error "pbl_from_o_model CHANGED 1"
1.115 +
1.116 +\<close> ML \<open>
1.117 +(*//------------------ step into map ((fn i_single -----------------------------------------\\*)
1.118 +"~~~~~ fun map ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) = (nth 1 i_from_pbl);
1.119 + (*if*) is_empty_single_TEST i_single (*else*);
1.120 + get_descr_vnt' feedb pbl_max_vnts o_model;
1.121 +
1.122 + val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
1.123 + if is_empty_single_TEST i_single
1.124 + then
1.125 + case get_descr_vnt' feedb pbl_max_vnts o_model of
1.126 +(*---------- ^^^^^^^^^^^^^^ ----------------------------*)
1.127 + [] => raise ERROR (msg pbl_max_vnts feedb)
1.128 + | o_singles => map transfer_terms o_singles
1.129 + else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
1.130 +(*\\------------------ step into map ((fn i_single -----------------------------------------//*)
1.131 +
1.132 +(*|------------------- continue s_make_complete ----------------------------------------------*)
1.133 + val i_from_met = map (fn (_, (descr, _)) =>
1.134 + Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
1.135 +;
1.136 +(*+*)if (i_from_met |> I_Model.to_string_TEST @{context}) = "[\n" ^
1.137 + "(0, [], false ,i_model_empty, (Sup_TEST Constants [], Position.T)), \n" ^
1.138 + "(0, [], false ,i_model_empty, (Sup_TEST Maximum, Position.T)), \n" ^
1.139 + "(0, [], false ,i_model_empty, (Sup_TEST Extremum, Position.T)), \n" ^
1.140 + "(0, [], false ,i_model_empty, (Sup_TEST SideConditions [], Position.T)), \n" ^
1.141 + "(8, [2], true ,#undef, (Cor_TEST FunctionVariable b , pen2str, Position.T)), \n" ^
1.142 +(*---there is 1 item already input -^^^^^^^^^^^^^^^^^^*)
1.143 + "(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n" ^
1.144 + "(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n" ^
1.145 + "(0, [], false ,i_model_empty, (Sup_TEST AdditionalValues [], Position.T))]"
1.146 +(*+*)then () else error "s_make_complete: from_met CHANGED";
1.147 +;
1.148 + val met_max_vnts = Model_Def.max_variants o_model i_from_met;
1.149 +(*+*)val [2] = met_max_vnts
1.150 +
1.151 + val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)
1.152 + val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
1.153 + if is_empty_single_TEST i_single
1.154 + then
1.155 + case get_descr_vnt' feedb [met_max_vnt] o_model of
1.156 + [] => raise ERROR (msg [met_max_vnt] feedb)
1.157 + | o_singles => map transfer_terms o_singles
1.158 + else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
1.159 +;
1.160 +(*+*)if (met_from_pbl |> I_Model.to_string_TEST @{context}) = "[\n" ^
1.161 + "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
1.162 + "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
1.163 + "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
1.164 + "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
1.165 + "(8, [2], true ,#undef, (Cor_TEST FunctionVariable b , pen2str, Position.T)), \n" ^
1.166 + "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
1.167 + "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
1.168 + "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
1.169 +(*+*)then () else error "s_make_complete: met_from_pbl CHANGED";
1.170 +;
1.171 +val return_s_make_complete_step = (pbl_from_o_model, met_from_pbl)
1.172 +(*\------------------- step into s_make_complete -------------------------------------------//*)
1.173 +;
1.174 +if return_s_make_complete = return_s_make_complete_step
1.175 +then () else error "s_make_complete: stewise construction <> value of fun"
1.176 +
1.177 +
1.178 +
1.179 +\<close> ML \<open>
1.180 +\<close>
1.181 ML_file "Specify/pre-conditions.sml"
1.182 ML_file "Specify/p-model.sml"
1.183 ML_file "Specify/m-match.sml"
1.184 ML_file "Specify/refine.sml" (* requires setup from refine.thy *)
1.185 +ML \<open>
1.186 +\<close> ML \<open>
1.187 +
1.188 +\<close> ML \<open>
1.189 +\<close>
1.190 ML_file "Specify/test-out.sml"
1.191 ML_file "Specify/specify-step.sml"
1.192 ML_file "Specify/specification.sml"