1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Sep 25 08:39:43 2023 +0200
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Sep 26 15:57:12 2023 +0200
1.3 @@ -501,15 +501,23 @@
1.4
1.5 fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
1.6 let
1.7 -(*new*)val (itms, oris, probl) = case get_obj I pt p of
1.8 -(*new*) PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
1.9 - | _ => raise ERROR ""
1.10 -(*old* )val {model, ...} = MethodC.from_store ctxt mI;
1.11 - val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
1.12 ---------------------^^^^^^^^^^----------------------------------------------------
1.13 -( *old*)
1.14 -(*new*)val {model = met_patt, ...} = MethodC.from_store ctxt mI;
1.15 -(*new*)val itms = I_Model.fill_method oris (I_Model.OLD_to_TEST probl) met_patt(*new*)
1.16 +(*OLD* )
1.17 + val (itms, oris, probl) = case get_obj I pt p of
1.18 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
1.19 + | _ => raise ERROR ""
1.20 + val {model = met_patt, ...} = MethodC.from_store ctxt mI;
1.21 + val (_, itms) = I_Model.fill_method oris (I_Model.OLD_to_TEST probl) met_patt
1.22 +( *---*)
1.23 + val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
1.24 + PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
1.25 + => (itms, oris, probl, o_spec, spec)
1.26 + | _ => raise ERROR ""
1.27 + val (_, pI', _) = References.select_input o_spec spec
1.28 + val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
1.29 + val {model = met_patt, ...} = MethodC.from_store ctxt mI;
1.30 + val (_, itms) = I_Model.s_make_complete oris
1.31 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
1.32 +(*NEW*)
1.33 val (is, env, ctxt, prog) = case LItool.init_pstate ctxt itms mI of
1.34 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
1.35 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate"
2.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Mon Sep 25 08:39:43 2023 +0200
2.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Sep 26 15:57:12 2023 +0200
2.3 @@ -10,7 +10,7 @@
2.4 (c) by Richard Lang, 2003
2.5 *)
2.6
2.7 -theory PolyEq imports LinEq RootRatEq begin
2.8 +theory PolyEq imports LinEq RootRatEq begin
2.9
2.10 (*-------------------- rules -------------------------------------------------*)
2.11 (* type real enforced by op " \<up> " *)
3.1 --- a/src/Tools/isac/MathEngBasic/references.sml Mon Sep 25 08:39:43 2023 +0200
3.2 +++ b/src/Tools/isac/MathEngBasic/references.sml Tue Sep 26 15:57:12 2023 +0200
3.3 @@ -9,7 +9,6 @@
3.4 type T
3.5 val empty: T
3.6 val to_string: T -> string
3.7 - val select_input: T -> T -> T
3.8
3.9 type input
3.10 val for_parse: ThyC.id -> ThyC.id -> ThyC.id -> ThyC.id
3.11 @@ -26,12 +25,14 @@
3.12 val explode_id: input_id -> References_Def.id
3.13 val implode_id: References_Def.id -> input_id
3.14
3.15 - val select_from_input: input -> T -> T -> T
3.16 -
3.17 val explode: input -> T
3.18 val implode: T -> input
3.19 val for_template: input -> T -> input
3.20
3.21 +(*REN select_formalise*)
3.22 + val select_input: T -> T -> T
3.23 + val select_from_input: input -> T -> T -> T
3.24 +
3.25 val complete: Ctree.state -> Ctree.state
3.26 val are_complete: Ctree.state -> bool
3.27 end
4.1 --- a/src/Tools/isac/Specify/i-model.sml Mon Sep 25 08:39:43 2023 +0200
4.2 +++ b/src/Tools/isac/Specify/i-model.sml Tue Sep 26 15:57:12 2023 +0200
4.3 @@ -62,12 +62,15 @@
4.4 (bool * Model_Def.variant * T_TEST) * Env.T * (Pre_Conds.env_subst * Pre_Conds.env_eval)
4.5
4.6 val add: single -> T -> T
4.7 +(**)
4.8 val s_make_complete: O_Model.T -> T_TEST * T_TEST -> Model_Pattern.T * Model_Pattern.T ->
4.9 T_TEST * T_TEST
4.10 -(*^^^--- s_make_complete SHALL REPLACE ALL THESE ---vvv*)
4.11 +(** )
4.12 val complete: O_Model.T -> (*Problem*)T -> (*MethodC*)T -> Model_Pattern.T -> T
4.13 + val fill_method: O_Model.T -> T_TEST -> Model_Pattern.T -> T_TEST
4.14 +( **)
4.15 val complete': Model_Pattern.T -> O_Model.single -> single
4.16 - val fill_method: O_Model.T -> T_TEST -> Model_Pattern.T -> T_TEST
4.17 +(*^^^--- s_make_complete SHALL REPLACE ALL THESE*)
4.18
4.19 val is_error: feedback -> bool
4.20
5.1 --- a/src/Tools/isac/Specify/p-spec.sml Mon Sep 25 08:39:43 2023 +0200
5.2 +++ b/src/Tools/isac/Specify/p-spec.sml Tue Sep 26 15:57:12 2023 +0200
5.3 @@ -185,10 +185,21 @@
5.4 in (Pos.Pbl, appl_adds dI' oris probl pbt
5.5 (map (itms2fstr ctxt) probl), meth) end
5.6 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
5.7 - then let val met = (#model o MethodC.from_store ctxt) mI
5.8 + then let
5.9 +(*OLD* )
5.10 + val met = (#model o MethodC.from_store ctxt) mI
5.11 val mits = I_Model.complete oris probl meth met
5.12 in if foldl and_ (true, map #3 mits)
5.13 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
5.14 +( *---*)
5.15 + val pbl_patt = (#model o Problem.from_store ctxt) pI
5.16 + val met = (#model o MethodC.from_store ctxt) mI
5.17 + val (_, mits) = I_Model.s_make_complete oris
5.18 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (met, pbl_patt)
5.19 + in if foldl and_ (true, map #3 mits)
5.20 + then (Pos.Pbl, probl, I_Model.TEST_to_OLD mits)
5.21 + else (Pos.Met, probl, I_Model.TEST_to_OLD mits)
5.22 +(*NEW*)
5.23 end
5.24 else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)]
5.25 ((#model o Problem.from_store ctxt)
6.1 --- a/test/Tools/isac/Interpret/li-tool.sml Mon Sep 25 08:39:43 2023 +0200
6.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Tue Sep 26 15:57:12 2023 +0200
6.3 @@ -331,28 +331,32 @@
6.4 ist_ctxt (pt, (p, p_'));
6.5 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
6.6 ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
6.7 - val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
6.8 - PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
6.9 - | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
6.10 - val {model, ...} = MethodC.from_store ctxt mI;
6.11 - val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
6.12 + val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
6.13 + PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
6.14 + => (itms, oris, probl, o_spec, spec)
6.15 + | _ => raise ERROR ""
6.16 + val (_, pI', _) = References.select_input o_spec spec
6.17 + val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
6.18 + val {model = met_patt, ...} = MethodC.from_store ctxt mI;
6.19 + val (_, itms) = I_Model.s_make_complete oris
6.20 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
6.21 ;
6.22 -(*+*)if (itms |> I_Model.to_string @{context}) = "[\n" ^
6.23 - "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
6.24 - "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
6.25 - "(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
6.26 - "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str), \n" ^
6.27 - "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x , pen2str), \n" ^
6.28 - "(6 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie y' , pen2str), \n" ^
6.29 - "(7 ,[1] ,true ,#Given ,Cor Biegemoment M_b , pen2str), \n" ^
6.30 - "(8 ,[1] ,true ,#Given ,Cor Querkraft Q , pen2str), \n" ^
6.31 - "(9 ,[1] ,true ,#Given ,Cor GleichungsVariablen [c, c_2, c_3, c_4] , pen2str)]"
6.32 +(*+*)if (itms |> I_Model.to_string_TEST @{context}) = "[\n" ^
6.33 + "(1, [1], true ,#Given, (Cor_TEST Traegerlaenge L , pen2str, Position.T)), \n" ^
6.34 + "(2, [1], true ,#Given, (Cor_TEST Streckenlast q_0 , pen2str, Position.T)), \n" ^
6.35 + "(4, [1], true ,#Relate, (Cor_TEST Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str, Position.T)), \n" ^
6.36 + "(5, [1], true ,#Given, (Cor_TEST FunktionsVariable x , pen2str, Position.T)), \n" ^
6.37 + "(6, [1], true ,#Given, (Cor_TEST AbleitungBiegelinie y' , pen2str, Position.T)), \n" ^
6.38 + "(7, [1], true ,#Given, (Cor_TEST Biegemoment M_b , pen2str, Position.T)), \n" ^
6.39 + "(8, [1], true ,#Given, (Cor_TEST Querkraft Q , pen2str, Position.T)), \n" ^
6.40 + "(9, [1], true ,#Given, (Cor_TEST GleichungsVariablen [c, c_2, c_3, c_4] , pen2str, Position.T)), \n" ^
6.41 + "(3, [1], true ,#Find, (Cor_TEST Biegelinie y , pen2str, Position.T))]"
6.42 (*+*)then () else error "init_pstate: initial i_model changed";
6.43
6.44 (*case*)
6.45 - LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI (*of*);
6.46 + LItool.init_pstate ctxt itms mI (*of*);
6.47 (*//------------------ step into init_pstate -----------------------------------------------\\*)
6.48 -"~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) = (ctxt, (I_Model.OLD_to_TEST itms), mI);
6.49 +"~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) = (ctxt, itms, mI);
6.50 val (model_patt, program, prog, prog_rls, where_, where_rls) =
6.51 case MethodC.from_store ctxt met_id of
6.52 {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...}=>
7.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Sep 25 08:39:43 2023 +0200
7.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Sep 26 15:57:12 2023 +0200
7.3 @@ -66,16 +66,18 @@
7.4 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _)))
7.5 = ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)),
7.6 ist_ctxt, (pt, (p, p_')));
7.7 - val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
7.8 - PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
7.9 - | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
7.10 - val {model, ...} = MethodC.from_store ctxt mI;
7.11 - val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
7.12 - val prog_rls = LItool.get_simplifier (pt, pos)
7.13 - val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
7.14 + val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
7.15 + PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
7.16 + => (itms, oris, probl, o_spec, spec)
7.17 + | _ => raise ERROR ""
7.18 + val (_, pI', _) = References.select_input o_spec spec
7.19 + val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
7.20 + val {model = met_patt, ...} = MethodC.from_store ctxt mI;
7.21 + val (_, itms) = I_Model.s_make_complete oris
7.22 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
7.23
7.24 val (is, env, ctxt, prog) = case
7.25 - LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of
7.26 + LItool.init_pstate ctxt itms mI of
7.27 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
7.28 val ini = LItool.implicit_take ctxt prog env;
7.29 val pos = start_new_level pos
7.30 @@ -164,16 +166,18 @@
7.31
7.32 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
7.33 = (m, (pt, pos));
7.34 - val {prog_rls, ...} = MethodC.from_store ctxt mI;
7.35 - val itms = case get_obj I pt p of
7.36 - PblObj {meth=itms, ...} => itms
7.37 - | _ => error "solve Apply_Method: uncovered case get_obj"
7.38 - val thy' = get_obj g_domID pt p;
7.39 - val thy = ThyC.get_theory @{context} thy';
7.40 - val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
7.41 + val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
7.42 + PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
7.43 + => (itms, oris, probl, o_spec, spec)
7.44 + | _ => raise ERROR ""
7.45 + val (_, pI', _) = References.select_input o_spec spec
7.46 + val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
7.47 + val {model = met_patt, ...} = MethodC.from_store ctxt mI;
7.48 + val (_, itms) = I_Model.s_make_complete oris
7.49 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
7.50
7.51 val (is, env, ctxt, sc) = case
7.52 - LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of
7.53 + LItool.init_pstate ctxt itms mI of
7.54 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
7.55 | _ => error "solve Apply_Method: uncovered case init_pstate";
7.56 (*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)";
8.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Mon Sep 25 08:39:43 2023 +0200
8.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Tue Sep 26 15:57:12 2023 +0200
8.3 @@ -865,58 +865,3 @@
8.4 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt;
8.5 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;
8.6
8.7 -(* ------------------- step into UNTIL A PROGRAM IS REQUIRED (not yet impl. ---------------- )*)
8.8 -(*/------------------- step into me_Add_Given_ErrorBound------------------------------------\\*)
8.9 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
8.10 - val ctxt = Ctree.get_ctxt pt p
8.11 - val (pt, p) =
8.12 - (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
8.13 - case Step.by_tactic tac (pt, p) of
8.14 - ("ok", (_, _, ptp)) => ptp;
8.15 -(*ERROR due to missing program in creating the environment from formal args* )
8.16 - (*case*)
8.17 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
8.18 -( *ERROR*)
8.19 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis) ) =
8.20 - (p, ((pt, Pos.e_pos'), []));
8.21 - (*if*) Pos.on_calc_end ip (*else*);
8.22 - val (_, probl_id, _) = Calc.references (pt, p);
8.23 -val _ =
8.24 - (*case*) tacis (*of*);
8.25 - (*if*) probl_id = Problem.id_empty (*else*);
8.26 -
8.27 -(*ERROR due to missing program in creating the environment from formal args* )
8.28 - switch_specify_solve p_ (pt, ip);
8.29 -( *ERROR*)
8.30 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
8.31 - (*if*) Pos.on_specification ([], state_pos) (*then*);
8.32 -
8.33 -(*ERROR due to missing program in creating the environment from formal args* )
8.34 - specify_do_next (pt, input_pos)
8.35 -( *ERROR*)
8.36 -"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
8.37 - val (_, (p_', tac as Apply_Method ["Optimisation", "by_univariate_calculus"])) =
8.38 - (*-------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ not yet impl.*)
8.39 - Specify.find_next_step ptp
8.40 - val ist_ctxt = Ctree.get_loc pt (p, p_)
8.41 -
8.42 -val Tactic.Apply_Method (mI as ["Optimisation", "by_univariate_calculus"]) =
8.43 - (*case*) tac (*of*);
8.44 -(*ERROR due to missing program in creating the environment from formal args* )
8.45 - LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
8.46 - ist_ctxt (pt, (p, p_'))
8.47 -( *ERROR*)
8.48 -"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
8.49 - ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
8.50 - val (itms, oris, probl) = case get_obj I pt p of
8.51 - PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
8.52 - val {model, ...} = MethodC.from_store ctxt mI;
8.53 - (*if*) itms <> [] (*then*);
8.54 - val itms = I_Model.complete oris probl [] model
8.55 -
8.56 -(*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,true ,#Given ,Cor FunctionVariable a , pen2str), \n(10 ,[1, 2] ,true ,#Given ,Cor Input_Descript.Domain {0<..<r} , pen2str), \n(12 ,[1, 2, 3] ,true ,#Given ,Cor ErrorBound (\<epsilon> = 0) , pen2str)]"
8.57 - = itms |> I_Model.to_string @{context}
8.58 -(*+*)val 8 = length itms
8.59 -(*+*)val 8 = length model
8.60 -(*\------------------- step into me_Add_Given_ErrorBound------------------------------------//*)
8.61 -
9.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Mon Sep 25 08:39:43 2023 +0200
9.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Tue Sep 26 15:57:12 2023 +0200
9.3 @@ -148,14 +148,18 @@
9.4 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
9.5 ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)),
9.6 ist_ctxt, (pt, (p, p_')));
9.7 - val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
9.8 - PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
9.9 - | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
9.10 - val {model, ...} = MethodC.from_store ctxt mI;
9.11 - val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
9.12 + val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
9.13 + PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
9.14 + => (itms, oris, probl, o_spec, spec)
9.15 + | _ => raise ERROR ""
9.16 + val (_, pI', _) = References.select_input o_spec spec
9.17 + val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
9.18 + val {model = met_patt, ...} = MethodC.from_store ctxt mI;
9.19 + val (_, itms) = I_Model.s_make_complete oris
9.20 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
9.21
9.22 val (is, env, ctxt, prog) = case
9.23 - LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of
9.24 + LItool.init_pstate ctxt itms mI of
9.25 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
9.26 val return_init_pstate = (is, env, ctxt, prog)
9.27 (*#------------------- un-hide local of init_pstate -----------------------------------------\*)
9.28 @@ -222,7 +226,7 @@
9.29 (*//------------------ step into init_pstate NEW -------------------------------------------\\*)
9.30 val (_, ctxt, i_model, met_id) = (prog_rls, ctxt, itms, mI);
9.31 "~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) =
9.32 - (ctxt, I_Model.OLD_to_TEST i_model, met_id);
9.33 + (ctxt, i_model, met_id);
9.34 val (model_patt, program, prog, prog_rls, where_, where_rls) =
9.35 case MethodC.from_store ctxt met_id of
9.36 {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...} =>
10.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Mon Sep 25 08:39:43 2023 +0200
10.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Tue Sep 26 15:57:12 2023 +0200
10.3 @@ -63,14 +63,18 @@
10.4 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt (pt, (p, p_'));
10.5 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
10.6 ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
10.7 - val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
10.8 - PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
10.9 - | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj"
10.10 - val {model, ...} = MethodC.from_store ctxt mI;
10.11 - val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
10.12 + val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
10.13 + PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
10.14 + => (itms, oris, probl, o_spec, spec)
10.15 + | _ => raise ERROR ""
10.16 + val (_, pI', _) = References.select_input o_spec spec
10.17 + val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
10.18 + val {model = met_patt, ...} = MethodC.from_store ctxt mI;
10.19 + val (_, itms) = I_Model.s_make_complete oris
10.20 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
10.21
10.22 val (is, env, ctxt, prog) = case
10.23 - LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of
10.24 + LItool.init_pstate ctxt itms mI of
10.25 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
10.26 | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate"
10.27 val ini = LItool.implicit_take ctxt prog env;
11.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Mon Sep 25 08:39:43 2023 +0200
11.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Tue Sep 26 15:57:12 2023 +0200
11.3 @@ -40,18 +40,23 @@
11.4 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt ptp;
11.5 "~~~~~ fun begin_end_prog , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (ist, ctxt), (pt, pos as (p, _)))
11.6 = ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, ptp);
11.7 - val {model, ...} = MethodC.from_store ctxt mI;
11.8 - val (itms, oris, probl) = case get_obj I pt p of
11.9 - PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
11.10 - | _ => error "begin_end_prog Apply_Method': uncovered case get_obj"
11.11 - val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
11.12 + val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
11.13 + PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
11.14 + => (itms, oris, probl, o_spec, spec)
11.15 + | _ => raise ERROR ""
11.16 + val (_, pI', _) = References.select_input o_spec spec
11.17 + val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
11.18 + val {model = met_patt, ...} = MethodC.from_store ctxt mI;
11.19 + val (_, itms) = I_Model.s_make_complete oris
11.20 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
11.21 +
11.22 val thy' = get_obj g_domID pt p;
11.23 val thy = Know_Store.get_via_last_thy thy';
11.24
11.25 (*THIS HERE---vvvvvvvvvvvvvvvvvvvvvvvvvvvvvv---MUST BE FROM A PREVIOUS TEST: EXPECT ["Test", "squ-equ-test-subpbl1"]*)
11.26 (*if*) mI = ["Biegelinien", "ausBelastung"] (*else*);
11.27 val (is, env, ctxt, prog) = case
11.28 - LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of
11.29 + LItool.init_pstate ctxt itms mI of
11.30 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
11.31 | _ => error "begin_end_prog Apply_Method': uncovered case init_pstate"
11.32
12.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Mon Sep 25 08:39:43 2023 +0200
12.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Tue Sep 26 15:57:12 2023 +0200
12.3 @@ -189,20 +189,24 @@
12.4 (*+*)then () else error "assumptions 7 from Apply_Method'";
12.5
12.6 (*+*)val [3] = p;
12.7 - val (itms, oris, probl(*, ctxt*)) = case get_obj I pt p of
12.8 - PblObj {meth = itms, origin = (oris, _, _), probl(*, ctxt*), ...} => (itms, oris, probl(*, ctxt*))
12.9 + val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
12.10 + PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
12.11 + => (itms, oris, probl, o_spec, spec)
12.12 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj";
12.13
12.14 (*+isa==isa2*)if (ContextC.get_assumptions ctxt |> map (UnparseC.term ctxt))
12.15 (*+*) = ["precond_rootmet x"]
12.16 (*+*)then () else error "assumptions 8";
12.17
12.18 - val {model, ...} = MethodC.from_store ctxt mI;
12.19 - val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
12.20 + val (_, pI', _) = References.select_input o_spec spec
12.21 + val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
12.22 + val {model = met_patt, ...} = MethodC.from_store ctxt mI;
12.23 + val (_, itms) = I_Model.s_make_complete oris
12.24 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
12.25 val prog_rls = LItool.get_simplifier (pt, pos)
12.26
12.27 val (is, env, ctxt, prog) = case
12.28 - LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of
12.29 + LItool.init_pstate ctxt itms mI of
12.30 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
12.31 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate";
12.32
13.1 --- a/test/Tools/isac/Specify/specify.sml Mon Sep 25 08:39:43 2023 +0200
13.2 +++ b/test/Tools/isac/Specify/specify.sml Tue Sep 26 15:57:12 2023 +0200
13.3 @@ -8,7 +8,6 @@
13.4 "-----------------------------------------------------------------------------------------------";
13.5 "-----------------------------------------------------------------------------------------------";
13.6 "----------- maximum-example: Specify.finish_phase ---------------------------------------------";
13.7 -"----------- maximum-example: I_Model.complete -------------------------------------------------";
13.8 "----------- revise Specify.do_all -------------------------------------------------------------";
13.9 "----------- specify-phase: low level functions ------------------------------------------------";
13.10 "-----------------------------------------------------------------------------------------------";
13.11 @@ -84,96 +83,6 @@
13.12 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
13.13 ( *\\-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --//*)
13.14
13.15 -(**** maximum-example: I_Model.complete ################################################## ****)
13.16 -"----------- maximum-example: I_Model.complete -------------------------------------------------";
13.17 -"----------- maximum-example: I_Model.complete -------------------------------------------------";
13.18 - val c = [];
13.19 - val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context}
13.20 - [(["fixedValues [r=Arbfix]", "maximum A",
13.21 - "valuesFor [a,b]",
13.22 - "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
13.23 - "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
13.24 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
13.25 - "boundVariable a", "boundVariable b", "boundVariable alpha",
13.26 - "interval {x::real. 0 <= x & x <= 2*r}",
13.27 - "interval {x::real. 0 <= x & x <= 2*r}",
13.28 - "interval {x::real. 0 <= x & x <= pi}",
13.29 - "errorBound (eps=(0::real))"],
13.30 - ("Diff_App", ["maximum_of", "function"], ["Diff_App", "max_by_calculus"]))];
13.31 -(*** stepwise Specification: Problem model================================================= ***)
13.32 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "fixedValues [r = Arbfix]" = nxt
13.33 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "maximum A" = nxt
13.34 -(*/---broken elementwise input to lists---\* )
13.35 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "valuesFor [a]" = nxt
13.36 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "valuesFor [b]" = nxt
13.37 -( *\---broken elementwise input to lists---/*)
13.38 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "valuesFor [a, b]" = nxt
13.39 -(*/---broken elementwise input to lists---\* )
13.40 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "relations [A = a * b]" = nxt
13.41 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "relations [(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]" = nxt
13.42 -( *\---broken elementwise input to lists---/*)
13.43 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]" = nxt
13.44 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Diff_App" = nxt
13.45 -
13.46 -(*/------------------- directly to Problem model is complete --------------------------------\*)
13.47 - val thy = @{theory "Diff_App"};
13.48 - val ctxt = Proof_Context.init_global thy;
13.49 - val (o_model, _, _) = get_obj g_origin pt (fst p);
13.50 - writeln (O_Model.to_string @{context} o_model);
13.51 -if O_Model.to_string @{context} o_model = "[\n" ^
13.52 - "(1, [\"1\", \"2\", \"3\"], #Given, fixedValues, [\"[r = Arbfix]\"]), \n" ^
13.53 - "(2, [\"1\", \"2\", \"3\"], #Find, maximum, [\"A\"]), \n" ^
13.54 - "(3, [\"1\", \"2\", \"3\"], #Find, valuesFor, [\"[a]\", \"[b]\"]), \n" ^
13.55 - "(4, [\"1\", \"2\"], #Relate, relations, [\"[A = a * b]\", \"[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]\"]), \n" ^
13.56 - "(5, [\"3\"], #Relate, relations, [\"[A = a * b]\", \"[a / 2 = r * sin alpha]\", \"[b / 2 = r * cos alpha]\"]), \n" ^
13.57 - "(6, [\"1\"], #undef, boundVariable, [\"a\"]), \n" ^
13.58 - "(7, [\"2\"], #undef, boundVariable, [\"b\"]), \n" ^
13.59 - "(8, [\"3\"], #undef, boundVariable, [\"alpha\"]), \n" ^
13.60 - "(9, [\"1\", \"2\"], #undef, interval, [\"{x. 0 \<le> x \<and> x \<le> 2 * r}\"]), \n" ^
13.61 - "(10, [\"3\"], #undef, interval, [\"{x. 0 \<le> x \<and> x \<le> pi}\"]), \n" ^
13.62 - "(11, [\"1\", \"2\", \"3\"], #undef, errorBound, [\"eps = 0\"])]"
13.63 -then () else error "maximum-example: O_Model.to_string o_model CHANGED";
13.64 -
13.65 - val problem_i_model = get_obj g_pbl pt (fst p); (* is already filled *)
13.66 - writeln (I_Model.to_string ctxt problem_i_model);
13.67 -if I_Model.to_string ctxt problem_i_model = "[\n" ^
13.68 - "(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] , pen2str), \n" ^
13.69 - "(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A , pen2str), \n" ^
13.70 - "(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] , pen2str), \n" ^
13.71 - "(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str)]"
13.72 -then () else error "maximum-example: I_Model.to_string problem_i_model CHANGED";
13.73 -
13.74 - val method_i_model= get_obj g_met pt (fst p); (* is still empty *)
13.75 -if method_i_model = []then () else error "is still empty CHANGED";
13.76 - val method_i_model = I_Model.complete o_model problem_i_model
13.77 - [] ((#model o MethodC.from_store ctxt) ["Diff_App", "max_by_calculus"]);
13.78 -if I_Model.to_string ctxt method_i_model = "[\n" ^
13.79 - "(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] , pen2str), \n" ^
13.80 - "(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A , pen2str), \n" ^
13.81 - "(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] , pen2str), \n" ^
13.82 - "(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str), \n" ^
13.83 - "(6 ,[1] ,true ,#undef ,Cor boundVariable a , pen2str), \n" ^
13.84 - "(9 ,[1, 2] ,true ,#undef ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} , pen2str), \n" ^
13.85 - "(11 ,[1, 2, 3] ,true ,#undef ,Cor errorBound (eps = 0) , pen2str)]"
13.86 -then () else error "completetest.sml: new behav. in I_Model.complete 1";
13.87 -(*\------------------- directly to Problem model is complete --------------------------------/*)
13.88 -
13.89 -(*/------------------- MethodC model has a copy of Problem ----------------------------------\*)
13.90 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["maximum_of", "function"] = nxt
13.91 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Diff_App", "max_by_calculus"] = nxt
13.92 -(*\------------------- MethodC model has a copy of Problem ----------------------------------/*)
13.93 -
13.94 -(*/------------------- stepwise Specification: MethodC model --------------------------------\*)
13.95 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "boundVariable a" = nxt
13.96 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "interval {x. 0 \<le> x \<and> x \<le> 2 * r}" = nxt
13.97 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "errorBound (eps = 0)" = nxt;
13.98 -(*** MethodC model is complete ============================================================ ***)
13.99 -(** )val (p,_,f,nxt,_,pt) = me nxt p c pt; (*exception TERM raised (line 359 of "term.ML"):
13.100 - fastype_of: Bound
13.101 - B.0 *)( **)
13.102 -(*\------------------ Specification of Problem and MethodC model is complete, Solution starts/*)
13.103 -;"? show section title below ?";
13.104 -
13.105
13.106 (**** revise Specify.do_all ############################################################## ****);
13.107 "----------- revise Specify.do_all -------------------------------------------------------------";
14.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Sep 25 08:39:43 2023 +0200
14.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Sep 26 15:57:12 2023 +0200
14.3 @@ -236,7 +236,6 @@
14.4 ML_file "Minisubpbl/150a-add-given-Maximum.sml"
14.5 ML_file "Minisubpbl/150-add-given-Equation.sml"
14.6 ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml"
14.7 - ML_file "Minisubpbl/200-start-method.sml"
14.8 ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
14.9 ML_file "Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
14.10 ML_file "Minisubpbl/300-init-subpbl.sml"
14.11 @@ -360,8 +359,7 @@
14.12 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
14.13 ML \<open>
14.14 \<close> ML \<open>
14.15 -\<close> ML \<open>
14.16 -\<close> ML \<open>
14.17 +
14.18 \<close> ML \<open>
14.19 \<close>
14.20