1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Oct 02 12:02:59 2023 +0200
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Oct 02 15:39:22 2023 +0200
1.3 @@ -256,7 +256,7 @@
1.4
1.5 | scan_up pcc ist (Const (\<^const_name>\<open>Tactical.If\<close>(*1*), _) $ _ $ _ $ _) = go_scan_up pcc ist
1.6
1.7 - | scan_up (pcc as (_, (_, ctxt))) _ t = raise ERROR ("scan_up not impl for " ^
1.8 + | scan_up (_, (_, ctxt)) _ t = raise ERROR ("scan_up not impl for " ^
1.9 UnparseC.term ctxt t)
1.10
1.11 (* scan program until an applicable tactic is found *)
1.12 @@ -267,7 +267,7 @@
1.13 | scan_to_tactic _ _ = raise ERROR "scan_to_tactic: uncovered pattern";
1.14
1.15 (* find the next applicable Prog_Tac in a prog *)
1.16 -fun find_next_step (Rule.Prog prog) (ptp as (pt, pos as (p, _))) (Pstate ist) ctxt =
1.17 +fun find_next_step (Rule.Prog prog) (ptp as (pt, pos)) (Pstate ist) ctxt =
1.18 (case scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) of
1.19 Accept_Tac (tac, ist, ctxt) =>
1.20 Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac)
1.21 @@ -471,8 +471,9 @@
1.22 | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*1*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist
1.23 | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*2*), _) $ _ $ _) = go_scan_up1 pcct ist
1.24 | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*3*), _) $ _ ) = go_scan_up1 pcct (ist |> path_up)
1.25 -
1.26 +(*/----- ML warning: Pattern 17 is redundant. *)
1.27 | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.If\<close>,_) $ _ $ _ $ _) = go_scan_up1 pcct ist
1.28 +(*\----- ML warning: Pattern 17 is redundant. *)
1.29
1.30 | scan_up1 (_, (_, ctxt, _)) _ t =
1.31 raise ERROR ("scan_up1 not impl for t= " ^ UnparseC.term ctxt t)
1.32 @@ -506,10 +507,8 @@
1.33 => (itms, oris, probl, o_spec, spec)
1.34 | _ => raise ERROR "LI.by_tactic: no PblObj"
1.35 val (_, pI', _) = References.select_input o_spec spec
1.36 - val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
1.37 - val {model = met_patt, ...} = MethodC.from_store ctxt mI;
1.38 - val (_, itms) = I_Model.s_make_complete oris
1.39 - (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
1.40 + val (_, itms) = I_Model.s_make_complete ctxt oris
1.41 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pI', mI)
1.42 val (is, env, ctxt, prog) = case LItool.init_pstate ctxt itms mI of
1.43 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
1.44 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate"
2.1 --- a/src/Tools/isac/Specify/i-model.sml Mon Oct 02 12:02:59 2023 +0200
2.2 +++ b/src/Tools/isac/Specify/i-model.sml Mon Oct 02 15:39:22 2023 +0200
2.3 @@ -62,14 +62,12 @@
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 - val s_make_complete: O_Model.T -> T_TEST * T_TEST -> Model_Pattern.T * Model_Pattern.T ->
2.8 + val s_make_complete: Proof.context -> O_Model.T -> T_TEST * T_TEST -> Problem.id * MethodC.id ->
2.9 T_TEST * T_TEST
2.10 - val s_are_complete: Proof.context -> O_Model.T -> T_TEST * T_TEST -> Problem.id * MethodC.id
2.11 - -> bool
2.12 + val s_are_complete: Proof.context -> O_Model.T -> T_TEST * T_TEST -> Problem.id * MethodC.id -> bool
2.13
2.14 val is_error: feedback -> bool
2.15 val to_p_model: theory -> feedback -> string
2.16 -
2.17 (*/----- from isac_test for Minisubpbl*)
2.18 val msg: variants -> feedback_TEST -> string
2.19 val transfer_terms: O_Model.single -> single_TEST
2.20 @@ -456,8 +454,10 @@
2.21 (feedb |> Pre_Conds.get_dscr' |> the |> UnparseC.term (ContextC.for_ERROR ()))
2.22 fun transfer_terms (i, vnts, m_field, descr, ts) =
2.23 (i, vnts, true, m_field, (Cor_TEST (descr, ts), Position.none))
2.24 -fun s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt) =
2.25 +fun s_make_complete ctxt o_model (pbl_imod, met_imod) (pbl_id, met_id) =
2.26 let
2.27 + val {model = pbl_patt, ...} = Problem.from_store ctxt pbl_id;
2.28 + val {model = met_patt, ...} = MethodC.from_store ctxt met_id;
2.29 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
2.30 val i_from_pbl = map (fn (_, (descr, _)) =>
2.31 Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt
3.1 --- a/src/Tools/isac/Specify/p-model.sml Mon Oct 02 12:02:59 2023 +0200
3.2 +++ b/src/Tools/isac/Specify/p-model.sml Mon Oct 02 15:39:22 2023 +0200
3.3 @@ -106,7 +106,7 @@
3.4 | boolterm2item ctxt(false, term) = False (UnparseC.term ctxt term);
3.5
3.6 fun from thy itms where_ =
3.7 - let
3.8 + let
3.9 fun coll model [] = model
3.10 | coll model ((_, _, _, field, itm_) :: itms) =
3.11 coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
4.1 --- a/src/Tools/isac/Specify/p-spec.sml Mon Oct 02 12:02:59 2023 +0200
4.2 +++ b/src/Tools/isac/Specify/p-spec.sml Mon Oct 02 15:39:22 2023 +0200
4.3 @@ -176,8 +176,8 @@
4.4 else
4.5 if pI <> spI
4.6 then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
4.7 - else
4.8 - let val pbt = (#model o Problem.from_store ctxt) pI
4.9 + else let
4.10 + val pbt = (#model o Problem.from_store ctxt) pI
4.11 val dI' = #1 (References.select_input ospec spec)
4.12 val oris =
4.13 if pI = #2 ospec then oris
4.14 @@ -186,14 +186,12 @@
4.15 (map (itms2fstr ctxt) probl), meth) end
4.16 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
4.17 then let
4.18 - val pbl_patt = (#model o Problem.from_store ctxt) pI
4.19 - val met = (#model o MethodC.from_store ctxt) mI
4.20 - val (_, mits) = I_Model.s_make_complete oris
4.21 - (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (met, pbl_patt)
4.22 - in if foldl and_ (true, map #3 mits)
4.23 - then (Pos.Pbl, probl, I_Model.TEST_to_OLD mits)
4.24 - else (Pos.Met, probl, I_Model.TEST_to_OLD mits)
4.25 - end
4.26 + val (_, mits) = I_Model.s_make_complete ctxt oris
4.27 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (pI, mI)
4.28 + in if foldl and_ (true, map #3 mits)
4.29 + then (Pos.Pbl, probl, I_Model.TEST_to_OLD mits)
4.30 + else (Pos.Met, probl, I_Model.TEST_to_OLD mits)
4.31 + end
4.32 else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)]
4.33 ((#model o Problem.from_store ctxt)
4.34 (#2 (References.select_input ospec spec)))
5.1 --- a/src/Tools/isac/Specify/specify.sml Mon Oct 02 12:02:59 2023 +0200
5.2 +++ b/src/Tools/isac/Specify/specify.sml Mon Oct 02 15:39:22 2023 +0200
5.3 @@ -197,9 +197,8 @@
5.4 | _ => raise ERROR "finish_phase: unvered case get_obj"
5.5 val (_, pI, mI) = References.select_input ospec spec
5.6 val ctxt = Ctree.get_ctxt pt pos
5.7 - val mpc = (#model o MethodC.from_store ctxt) mI
5.8 - val model = (#model o Problem.from_store ctxt) pI
5.9 - val (pits, mits) = I_Model.s_make_complete oris (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (model, mpc)
5.10 + val (pits, mits) = I_Model.s_make_complete ctxt oris
5.11 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (pI, mI)
5.12 val pt = Ctree.update_pblppc pt p (I_Model.TEST_to_OLD pits)
5.13 val pt = Ctree.update_metppc pt p (I_Model.TEST_to_OLD mits)
5.14 in (pt, (p, Pos.Met)) end
5.15 @@ -213,12 +212,10 @@
5.16 val (itms, oris, probl, o_refs, spec, ctxt) = case Ctree.get_obj I pt p of
5.17 Ctree.PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}
5.18 => (itms, oris, probl, o_spec, spec, ctxt)
5.19 - | _ => raise ERROR "LI.by_tactic: no PblObj"
5.20 + | _ => raise ERROR "Specify.do_all: no PblObj"
5.21 val (_, pbl_id', met_id') = References.select_input o_refs spec
5.22 - val {model = pbl_patt, ...} = Problem.from_store ctxt pbl_id';
5.23 - val {model = met_patt, ...} = MethodC.from_store ctxt met_id';
5.24 - val (pbl_imod, met_imod) = I_Model.s_make_complete oris
5.25 - (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
5.26 + val (pbl_imod, met_imod) = I_Model.s_make_complete ctxt oris
5.27 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_id', met_id')
5.28 val (pt, _) = Ctree.cupdate_problem pt p
5.29 (o_refs, I_Model.TEST_to_OLD pbl_imod, I_Model.TEST_to_OLD met_imod, ctxt)
5.30 in
6.1 --- a/src/Tools/isac/Specify/step-specify.sml Mon Oct 02 12:02:59 2023 +0200
6.2 +++ b/src/Tools/isac/Specify/step-specify.sml Mon Oct 02 15:39:22 2023 +0200
6.3 @@ -28,12 +28,11 @@
6.4 PblObj {origin = (oris, ospec, _), probl, spec, ctxt, meth, ...} => (oris, ospec, probl, spec, ctxt, meth)
6.5 | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
6.6 val (_, pI, mI) = References.select_input ospec spec
6.7 - val mpc = (#model o MethodC.from_store ctxt) mI (* just for reuse I_Model.complete_method *)
6.8 val {cas, model, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
6.9 val pbl = I_Model.init_TEST oris model (* fill in descriptions *)
6.10 val (pbl, met) = case cas of
6.11 NONE => (pbl, [])
6.12 - | _ => I_Model.s_make_complete oris (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (model, mpc)
6.13 + | _ => I_Model.s_make_complete ctxt oris (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (pI, mI)
6.14 val tac_ = Tactic.Model_Problem' (pI, I_Model.TEST_to_OLD pbl, I_Model.TEST_to_OLD met)
6.15 val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos)
6.16 in
7.1 --- a/test/Tools/isac/Interpret/li-tool.sml Mon Oct 02 12:02:59 2023 +0200
7.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Mon Oct 02 15:39:22 2023 +0200
7.3 @@ -336,10 +336,8 @@
7.4 => (itms, oris, probl, o_spec, spec)
7.5 | _ => raise ERROR ""
7.6 val (_, pI', _) = References.select_input o_spec spec
7.7 - val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
7.8 - val {model = met_patt, ...} = MethodC.from_store ctxt mI;
7.9 - val (_, itms) = I_Model.s_make_complete oris
7.10 - (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
7.11 + val (_, itms) = I_Model.s_make_complete ctxt oris
7.12 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pI', mI)
7.13 ;
7.14 (*+*)if (itms |> I_Model.to_string_TEST @{context}) = "[\n" ^
7.15 "(1, [1], true ,#Given, (Cor_TEST Traegerlaenge L , pen2str, Position.T)), \n" ^
8.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Oct 02 12:02:59 2023 +0200
8.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Oct 02 15:39:22 2023 +0200
8.3 @@ -71,10 +71,8 @@
8.4 => (itms, oris, probl, o_spec, spec)
8.5 | _ => raise ERROR ""
8.6 val (_, pI', _) = References.select_input o_spec spec
8.7 - val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
8.8 - val {model = met_patt, ...} = MethodC.from_store ctxt mI;
8.9 - val (_, itms) = I_Model.s_make_complete oris
8.10 - (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
8.11 + val (_, itms) = I_Model.s_make_complete ctxt oris
8.12 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pI', mI)
8.13
8.14 val (is, env, ctxt, prog) = case
8.15 LItool.init_pstate ctxt itms mI of
8.16 @@ -171,10 +169,8 @@
8.17 => (itms, oris, probl, o_spec, spec)
8.18 | _ => raise ERROR ""
8.19 val (_, pI', _) = References.select_input o_spec spec
8.20 - val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
8.21 - val {model = met_patt, ...} = MethodC.from_store ctxt mI;
8.22 - val (_, itms) = I_Model.s_make_complete oris
8.23 - (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
8.24 + val (_, itms) = I_Model.s_make_complete ctxt oris
8.25 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pI', mI)
8.26
8.27 val (is, env, ctxt, sc) = case
8.28 LItool.init_pstate ctxt itms mI of
9.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Mon Oct 02 12:02:59 2023 +0200
9.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Mon Oct 02 15:39:22 2023 +0200
9.3 @@ -153,10 +153,8 @@
9.4 => (itms, oris, probl, o_spec, spec)
9.5 | _ => raise ERROR ""
9.6 val (_, pI', _) = References.select_input o_spec spec
9.7 - val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
9.8 - val {model = met_patt, ...} = MethodC.from_store ctxt mI;
9.9 - val (_, itms) = I_Model.s_make_complete oris
9.10 - (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
9.11 + val (_, itms) = I_Model.s_make_complete ctxt oris
9.12 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pI', mI)
9.13
9.14 val (is, env, ctxt, prog) = case
9.15 LItool.init_pstate ctxt itms mI of
10.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Mon Oct 02 12:02:59 2023 +0200
10.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Mon Oct 02 15:39:22 2023 +0200
10.3 @@ -68,10 +68,8 @@
10.4 => (itms, oris, probl, o_spec, spec)
10.5 | _ => raise ERROR ""
10.6 val (_, pI', _) = References.select_input o_spec spec
10.7 - val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
10.8 - val {model = met_patt, ...} = MethodC.from_store ctxt mI;
10.9 - val (_, itms) = I_Model.s_make_complete oris
10.10 - (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
10.11 + val (_, itms) = I_Model.s_make_complete ctxt oris
10.12 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pI', mI)
10.13
10.14 val (is, env, ctxt, prog) = case
10.15 LItool.init_pstate ctxt itms mI of
11.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Mon Oct 02 12:02:59 2023 +0200
11.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Mon Oct 02 15:39:22 2023 +0200
11.3 @@ -45,10 +45,8 @@
11.4 => (itms, oris, probl, o_spec, spec)
11.5 | _ => raise ERROR ""
11.6 val (_, pI', _) = References.select_input o_spec spec
11.7 - val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
11.8 - val {model = met_patt, ...} = MethodC.from_store ctxt mI;
11.9 - val (_, itms) = I_Model.s_make_complete oris
11.10 - (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
11.11 + val (_, itms) = I_Model.s_make_complete ctxt oris
11.12 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pI', mI)
11.13
11.14 val thy' = get_obj g_domID pt p;
11.15 val thy = Know_Store.get_via_last_thy thy';
12.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Mon Oct 02 12:02:59 2023 +0200
12.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Mon Oct 02 15:39:22 2023 +0200
12.3 @@ -199,10 +199,8 @@
12.4 (*+*)then () else error "assumptions 8";
12.5
12.6 val (_, pI', _) = References.select_input o_spec spec
12.7 - val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
12.8 - val {model = met_patt, ...} = MethodC.from_store ctxt mI;
12.9 - val (_, itms) = I_Model.s_make_complete oris
12.10 - (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
12.11 + val (_, itms) = I_Model.s_make_complete ctxt oris
12.12 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pI', mI)
12.13 val prog_rls = LItool.get_simplifier (pt, pos)
12.14
12.15 val (is, env, ctxt, prog) = case
13.1 --- a/test/Tools/isac/Specify/i-model.sml Mon Oct 02 12:02:59 2023 +0200
13.2 +++ b/test/Tools/isac/Specify/i-model.sml Mon Oct 02 15:39:22 2023 +0200
13.3 @@ -321,9 +321,6 @@
13.4 => (o_model, (pbl_imod, met_imod), (pI, mI))
13.5 | _ => raise ERROR ""
13.6
13.7 -val {model = pbl_patt, ...} = Problem.from_store ctxt pI;
13.8 -val {model = met_patt, ...} = MethodC.from_store ctxt mI;
13.9 -
13.10 val pbl_imod = [ (*2 items for creating code ---> variants [1, 2]*)
13.11 (1, [1, 2, 3], true, "#undef", (Cor_TEST (@{term Constants},
13.12 [@{term "[r = (7::real)]"}]), Position.none)),
13.13 @@ -350,10 +347,12 @@
13.14 (*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)
13.15
13.16 val return_s_make_complete =
13.17 - s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt);
13.18 + s_make_complete ctxt o_model (pbl_imod, met_imod) (pI, mI);
13.19 (*/------------------- step into s_make_complete -------------------------------------------\\*)
13.20 -"~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt)) =
13.21 - (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt));
13.22 +"~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pI, mI)) =
13.23 + (o_model, (pbl_imod, met_imod), (pI, mI));
13.24 + val {model = pbl_patt, ...} = Problem.from_store ctxt pI;
13.25 + val {model = met_patt, ...} = MethodC.from_store ctxt mI;
13.26 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
13.27 val i_from_pbl = map (fn (_, (descr, _)) =>
13.28 Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
13.29 @@ -389,7 +388,7 @@
13.30 "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
13.31 "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
13.32 "(1, [1, 2], true ,#undef, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
13.33 -then () else error "pbl_from_o_model CHANGED"
13.34 +then () else error "pbl_from_o_model CHANGED 1"
13.35
13.36 (*//------------------ step into map ((fn i_single -----------------------------------------\\*)
13.37 "~~~~~ fun map ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) = (nth 1 i_from_pbl);
13.38 @@ -481,8 +480,6 @@
13.39 => (o_model, (pI, mI))
13.40 | _ => raise ERROR ""
13.41
13.42 -val {model = pbl_patt, ...} = Problem.from_store ctxt pI;
13.43 -val {model = met_patt, ...} = MethodC.from_store ctxt mI;
13.44 val pbl_imod = []
13.45 val met_imod = []
13.46 ;
13.47 @@ -503,7 +500,7 @@
13.48 (*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)
13.49
13.50 val return_s_make_complete =
13.51 - s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt);
13.52 + s_make_complete ctxt o_model (pbl_imod, met_imod) (pI, mI);
13.53 (*/------------------- step into s_make_complete -------------------------------------------\\*)
13.54 "~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt)) =
13.55 (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt));
13.56 @@ -555,7 +552,7 @@
13.57 "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
13.58 "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
13.59 "(6, [3], true ,#Relate, (Cor_TEST SideConditions [u / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>] , pen2str, Position.T))]"
13.60 -then () else error "pbl_from_o_model CHANGED"
13.61 +then () else error "pbl_from_o_model CHANGED 2"
13.62
13.63 (*//------------------ step into map ((fn i_single -----------------------------------------\\*)
13.64 "~~~~~ fun map nth 1 ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) =
14.1 --- a/test/Tools/isac/Specify/specify.sml Mon Oct 02 12:02:59 2023 +0200
14.2 +++ b/test/Tools/isac/Specify/specify.sml Mon Oct 02 15:39:22 2023 +0200
14.3 @@ -127,14 +127,12 @@
14.4 => (itms, oris, probl, o_spec, spec, ctxt)
14.5 | _ => raise ERROR "LI.by_tactic: no PblObj"
14.6 val (_, pbl_id', met_id') = References.select_input o_refs spec
14.7 - val {model = pbl_patt, ...} = Problem.from_store ctxt pbl_id';
14.8 - val {model = met_patt, ...} = MethodC.from_store ctxt met_id';
14.9 - val (pbl_imod, met_imod) = I_Model.s_make_complete oris
14.10 - (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
14.11 + val (pbl_imod, met_imod) = I_Model.s_make_complete ctxt oris
14.12 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_id', met_id')
14.13 ;
14.14 (*-------------------- stop step into do_all -------------------------------------------------*)
14.15 (*/------------------- check result of I_Model.complete' ------------------------------------\*)
14.16 -(*+*)if Model_Pattern.to_string @{context} met_patt = "[\"" ^
14.17 +(*+*)if Model_Pattern.to_string @{context} (#model (MethodC.from_store ctxt met_id')) = "[\"" ^
14.18 "(#Given, (Constants, fixes))\", \"" ^
14.19 "(#Given, (Maximum, maxx))\", \"" ^
14.20 "(#Given, (Extremum, extr))\", \"" ^
15.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Oct 02 12:02:59 2023 +0200
15.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Oct 02 15:39:22 2023 +0200
15.3 @@ -266,10 +266,189 @@
15.4 ML_file "Specify/formalise.sml"
15.5 ML_file "Specify/o-model.sml"
15.6 ML_file "Specify/i-model.sml" (* (BROKEN!) test on elementwise input to lists*)
15.7 +ML \<open>
15.8 +\<close> ML \<open>
15.9 +"----------- build I_Model.s_make_complete -----------------------------------------------------";
15.10 +"----------- build I_Model.s_make_complete -----------------------------------------------------";
15.11 +"----------- build I_Model.s_make_complete -----------------------------------------------------";
15.12 +val (_(*example text*),
15.13 + (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
15.14 + "Extremum (A = 2 * u * v - u \<up> 2)" ::
15.15 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
15.16 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
15.17 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: (*INCORRECT 2 / v*)
15.18 +(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
15.19 + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
15.20 + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
15.21 + "ErrorBound (\<epsilon> = (0::real))" :: []),
15.22 + refs as ("Diff_App",
15.23 + ["univariate_calculus", "Optimisation"],
15.24 + ["Optimisation", "by_univariate_calculus"])))
15.25 + = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
15.26 +
15.27 +val c = [];
15.28 +val (p,_,f,nxt,_,pt) =
15.29 + Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
15.30 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.31 +
15.32 +(*//------------------ setup test data for I_Model.s_make_complete -------------------------\\*)
15.33 +val (o_model, (pbl_imod, met_imod), (pI, mI)) = case get_obj I pt (fst p) of
15.34 + PblObj {meth = met_imod, origin = (o_model, (_, pI, mI), _), probl = pbl_imod, ...}
15.35 + => (o_model, (pbl_imod, met_imod), (pI, mI))
15.36 + | _ => raise ERROR ""
15.37 +
15.38 +val pbl_imod = [ (*2 items for creating code ---> variants [1, 2]*)
15.39 + (1, [1, 2, 3], true, "#undef", (Cor_TEST (@{term Constants},
15.40 + [@{term "[r = (7::real)]"}]), Position.none)),
15.41 + (1, [1, 2], true, "#undef", (Cor_TEST (@{term SideConditions},
15.42 + [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]), Position.none))]
15.43 +
15.44 +val met_imod = [ (*1 item for creating code*)
15.45 +(8, [2], true, "#undef", (Cor_TEST (@{term FunctionVariable}, [@{term "b::real"}]), Position.none))]
15.46 +;
15.47 +(*+*)if (o_model |> O_Model.to_string @{context}) = "[\n" ^
15.48 +(*+*) "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
15.49 +(*+*) "(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n" ^
15.50 +(*+*) "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
15.51 +(*+*) "(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
15.52 +(*+*) "(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
15.53 +(*+*) "(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
15.54 +(*+*) "(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n" ^
15.55 +(*+*) "(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n" ^
15.56 +(*+*) "(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n" ^
15.57 +(*+*) "(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
15.58 +(*+*) "(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
15.59 +(*+*) "(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
15.60 +then () else error "setup test data for I_Model.s_make_complete CHANGED";
15.61 +(*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)
15.62 +
15.63 +val return_s_make_complete =
15.64 + s_make_complete ctxt o_model (pbl_imod, met_imod) (pI, mI);
15.65 +(*/------------------- step into s_make_complete -------------------------------------------\\*)
15.66 +"~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pI, mI)) =
15.67 + (o_model, (pbl_imod, met_imod), (pI, mI));
15.68 + val {model = pbl_patt, ...} = Problem.from_store ctxt pbl_id;
15.69 + val {model = met_patt, ...} = MethodC.from_store ctxt met_id;
15.70 + val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
15.71 + val i_from_pbl = map (fn (_, (descr, _)) =>
15.72 + Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
15.73 +\<close> ML \<open>
15.74 +val [] = i_from_pbl
15.75 +\<close> ML \<open>
15.76 +
15.77 +(*//------------------ step into get_descr_vnt ---------------------------------------------\\*)
15.78 +"~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =
15.79 + (@{term Constants}, pbl_max_vnts, pbl_imod);
15.80 + val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false
15.81 + | SOME descr' => if descr = descr' then true else false) i_model
15.82 +;
15.83 +(*+*)filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr: I_Model.T_TEST
15.84 +;
15.85 +val return_get_descr_vnt_1 =
15.86 + case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
15.87 + [] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
15.88 + | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
15.89 +(*\\------------------ step into get_descr_vnt ---------------------------------------------//*)
15.90 +\<close> ML \<open>
15.91 +\<close> ML \<open>
15.92 +
15.93 +(*|------------------- continue s_make_complete ----------------------------------------------*)
15.94 + val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
15.95 + if is_empty_single_TEST i_single
15.96 + then
15.97 + case get_descr_vnt' feedb pbl_max_vnts o_model of
15.98 +(*-----------^^^^^^^^^^^^^^-----------------------------*)
15.99 + [] => raise ERROR (msg pbl_max_vnts feedb)
15.100 + | o_singles => map transfer_terms o_singles
15.101 + else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
15.102 +
15.103 +\<close> ML \<open>
15.104 +(*+*)val [2, 1] = vnts;
15.105 +\<close> ML \<open>
15.106 +val "[]" = (pbl_from_o_model |> I_Model.to_string_TEST @{context})
15.107 +\<close> ML \<open>
15.108 +(*+*)if (pbl_from_o_model |> I_Model.to_string_TEST @{context}) = "[\n" ^
15.109 + "(1, [1, 2, 3], true ,#undef, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
15.110 + "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
15.111 + "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
15.112 + "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
15.113 + "(1, [1, 2], true ,#undef, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
15.114 +then () else error "pbl_from_o_model CHANGED 1"
15.115 +
15.116 +\<close> ML \<open>
15.117 +(*//------------------ step into map ((fn i_single -----------------------------------------\\*)
15.118 +"~~~~~ fun map ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) = (nth 1 i_from_pbl);
15.119 + (*if*) is_empty_single_TEST i_single (*else*);
15.120 + get_descr_vnt' feedb pbl_max_vnts o_model;
15.121 +
15.122 + val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
15.123 + if is_empty_single_TEST i_single
15.124 + then
15.125 + case get_descr_vnt' feedb pbl_max_vnts o_model of
15.126 +(*---------- ^^^^^^^^^^^^^^ ----------------------------*)
15.127 + [] => raise ERROR (msg pbl_max_vnts feedb)
15.128 + | o_singles => map transfer_terms o_singles
15.129 + else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
15.130 +(*\\------------------ step into map ((fn i_single -----------------------------------------//*)
15.131 +
15.132 +(*|------------------- continue s_make_complete ----------------------------------------------*)
15.133 + val i_from_met = map (fn (_, (descr, _)) =>
15.134 + Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
15.135 +;
15.136 +(*+*)if (i_from_met |> I_Model.to_string_TEST @{context}) = "[\n" ^
15.137 + "(0, [], false ,i_model_empty, (Sup_TEST Constants [], Position.T)), \n" ^
15.138 + "(0, [], false ,i_model_empty, (Sup_TEST Maximum, Position.T)), \n" ^
15.139 + "(0, [], false ,i_model_empty, (Sup_TEST Extremum, Position.T)), \n" ^
15.140 + "(0, [], false ,i_model_empty, (Sup_TEST SideConditions [], Position.T)), \n" ^
15.141 + "(8, [2], true ,#undef, (Cor_TEST FunctionVariable b , pen2str, Position.T)), \n" ^
15.142 +(*---there is 1 item already input -^^^^^^^^^^^^^^^^^^*)
15.143 + "(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n" ^
15.144 + "(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n" ^
15.145 + "(0, [], false ,i_model_empty, (Sup_TEST AdditionalValues [], Position.T))]"
15.146 +(*+*)then () else error "s_make_complete: from_met CHANGED";
15.147 +;
15.148 + val met_max_vnts = Model_Def.max_variants o_model i_from_met;
15.149 +(*+*)val [2] = met_max_vnts
15.150 +
15.151 + val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)
15.152 + val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
15.153 + if is_empty_single_TEST i_single
15.154 + then
15.155 + case get_descr_vnt' feedb [met_max_vnt] o_model of
15.156 + [] => raise ERROR (msg [met_max_vnt] feedb)
15.157 + | o_singles => map transfer_terms o_singles
15.158 + else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
15.159 +;
15.160 +(*+*)if (met_from_pbl |> I_Model.to_string_TEST @{context}) = "[\n" ^
15.161 + "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
15.162 + "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
15.163 + "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
15.164 + "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
15.165 + "(8, [2], true ,#undef, (Cor_TEST FunctionVariable b , pen2str, Position.T)), \n" ^
15.166 + "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
15.167 + "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
15.168 + "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
15.169 +(*+*)then () else error "s_make_complete: met_from_pbl CHANGED";
15.170 +;
15.171 +val return_s_make_complete_step = (pbl_from_o_model, met_from_pbl)
15.172 +(*\------------------- step into s_make_complete -------------------------------------------//*)
15.173 +;
15.174 +if return_s_make_complete = return_s_make_complete_step
15.175 +then () else error "s_make_complete: stewise construction <> value of fun"
15.176 +
15.177 +
15.178 +
15.179 +\<close> ML \<open>
15.180 +\<close>
15.181 ML_file "Specify/pre-conditions.sml"
15.182 ML_file "Specify/p-model.sml"
15.183 ML_file "Specify/m-match.sml"
15.184 ML_file "Specify/refine.sml" (* requires setup from refine.thy *)
15.185 +ML \<open>
15.186 +\<close> ML \<open>
15.187 +
15.188 +\<close> ML \<open>
15.189 +\<close>
15.190 ML_file "Specify/test-out.sml"
15.191 ML_file "Specify/specify-step.sml"
15.192 ML_file "Specify/specification.sml"