1.1 --- a/TODO.md Fri Oct 07 20:46:48 2022 +0200
1.2 +++ b/TODO.md Sat Oct 08 11:40:48 2022 +0200
1.3 @@ -33,7 +33,7 @@
1.4 (in the string after \<^keyword>\<open>Given\<close> etc) and not on the definition as a whole.
1.5 - in MathEngBasic/problem "Outer_Syntax.command \<^command_keyword>\<open>problem\<close>" there are writeln
1.6 and comments with testdata from "problem pbl_bieg : "Biegelinien"" in Biegelinie.thy
1.7 - - in MathEngBasic/problem there is guesswork ("TODO") how to reorganise "fun prep_input_PIDE"
1.8 + - in MathEngBasic/problem there is guesswork ("TODO") how to reorganise "fun prep_input"
1.9 such that errors in "Given" etc are indicated WITHIN the term.
1.10
1.11 * MW: In Outer_Syntax.command..‹Example› help: is there a quick fix
1.12 @@ -62,7 +62,7 @@
1.13
1.14 ***** priority of WN items is top down, most urgent/simple on top
1.15
1.16 -* WN: follow up 5: cleanup
1.17 +* WN: follow up 5b: clarify TermC.parse_patt/*_PIDE analogous to TermC.parse_strict/*_PIDE
1.18 follow up 6: ctxt_user at init Example mimiced by CalcTreeTest @{context}
1.19 Thus eliminate use of Thy_Info.get_theory
1.20 follow up 7: ANSWER: represent items, which have not yet been input IN VSCode_Example.thy WITH "__"
1.21 @@ -82,8 +82,8 @@
1.22 So: How can KEStore_Elems.get_thes and KEStore_Elems.add_thes be replaced in current Isabelle?
1.23
1.24 * WN: Specify/formalise.sml is in BaseDefinitions/ AND Specify/ DELETE ONE VERSION
1.25 -* WN: Step_Specify.initialise_PIDE: remove hdl in return-value, replace Step_Specify.nxt_specify_init_calc
1.26 - ? which uses initialise_PIDE !?
1.27 +* WN: Step_Specify.initialise: remove hdl in return-value, replace Step_Specify.nxt_specify_init_calc
1.28 + ? which uses initialise !?
1.29 * WN: ? unify "no_met" with "empty_meth_id" from References.empty ?
1.30
1.31 * WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations,
2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Fri Oct 07 20:46:48 2022 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Sat Oct 08 11:40:48 2022 +0200
2.3 @@ -77,7 +77,7 @@
2.4 val parse_strict: theory -> string -> term (*still required for CAS_Cmd*)
2.5 val parse_strict_PIDE: theory -> string -> term
2.6
2.7 - val parse_patt: theory -> string -> term
2.8 + val parse_patt: theory -> string -> term (*still required why ??? *)
2.9 val parse_patt_PIDE: theory -> string -> term
2.10 val perm: term -> term -> bool
2.11
3.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Fri Oct 07 20:46:48 2022 +0200
3.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Sat Oct 08 11:40:48 2022 +0200
3.3 @@ -102,7 +102,7 @@
3.4 Store.get (KEStore_Elems.get_expls @{theory}) example_id' example_id'
3.5 val ctxt = ContextC.initialise' thy model;
3.6
3.7 - val o_model = Problem.from_store_PIDE ctxt probl_id |> #ppc |> O_Model.init thy model
3.8 + val o_model = Problem.from_store ctxt probl_id |> #ppc |> O_Model.init thy model
3.9 in
3.10 Ctree.Nd (Ctree.PblObj {
3.11 fmz = fmz, origin = (o_model, refs, TermC.empty (*TODO handle CAS_Cmd*)),
4.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Fri Oct 07 20:46:48 2022 +0200
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Sat Oct 08 11:40:48 2022 +0200
4.3 @@ -101,7 +101,7 @@
4.4
4.5 (* interface for dialog-authoring: call in Buld_Thydata.thy only ! *)
4.6 fun update_metpair_PIDE thy metID errpats = let
4.7 - val ret = (update_metdata (MethodC.from_store'_PIDE thy metID) errpats, metID)
4.8 + val ret = (update_metdata (MethodC.from_store' thy metID) errpats, metID)
4.9 handle ERROR _ => raise ERROR ("update_metpair: " ^ (strs2str metID) ^ " must address a method");
4.10 in ret end;
4.11
5.1 --- a/src/Tools/isac/BridgeLibisabelle/present-tool.sml Fri Oct 07 20:46:48 2022 +0200
5.2 +++ b/src/Tools/isac/BridgeLibisabelle/present-tool.sml Sat Oct 08 11:40:48 2022 +0200
5.3 @@ -74,9 +74,9 @@
5.4
5.5 (* make a guh from a reference to an element in the kestore;
5.6 EXCEPT theory hierarchy ... compare 'fun keref2xml' *)
5.7 -fun pblID2guh ctxt pblID = (((#guh o (Problem.from_store_PIDE ctxt)) pblID)
5.8 +fun pblID2guh ctxt pblID = (((#guh o (Problem.from_store ctxt)) pblID)
5.9 handle ERROR _ => raise ERROR ("Ptool.pblID2guh: not for \"" ^ strs2str' pblID ^ "\""));
5.10 -fun metID2guh metID = (((#guh o MethodC.from_store_PIDE ("Isac_Knowledge" |> ThyC.get_theory |> Proof_Context.init_global)) metID)
5.11 +fun metID2guh metID = (((#guh o MethodC.from_store ("Isac_Knowledge" |> ThyC.get_theory |> Proof_Context.init_global)) metID)
5.12 handle ERROR _ => raise ERROR ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\""));
5.13 fun kestoreID2guh ctxt Pbl_ kestoreID = pblID2guh ctxt kestoreID
5.14 | kestoreID2guh _ Met_ kestoreID = metID2guh kestoreID
6.1 --- a/src/Tools/isac/Build_Isac.thy Fri Oct 07 20:46:48 2022 +0200
6.2 +++ b/src/Tools/isac/Build_Isac.thy Sat Oct 08 11:40:48 2022 +0200
6.3 @@ -185,12 +185,12 @@
6.4 \<close> ML \<open>
6.5 val id = ["univariate", "equation", "test"]
6.6 \<close> ML \<open>
6.7 -Problem.from_store_PIDE: Proof.context -> Problem.id -> Problem.T
6.8 +Problem.from_store: Proof.context -> Problem.id -> Problem.T
6.9 \<close> ML \<open>
6.10 \<close> ML \<open> (* \<rightarrow> refine.sml*)
6.11 \<close> ML \<open>
6.12 \<close> text \<open> local
6.13 -refin_PIDE
6.14 +refin
6.15 \<close> ML \<open>
6.16 \<close> text \<open> \<isac_test>
6.17 refine_PIDE
6.18 @@ -201,19 +201,19 @@
6.19 \<close> ML \<open>
6.20 KEStore_Elems.get_pbls @{theory Poly}; (*! real ! due to Simplify :: "real => real" etc*)
6.21 \<close> ML \<open>
6.22 -Problem.from_store_PIDE @{context} ["polynomial", "simplification"]
6.23 +Problem.from_store @{context} ["polynomial", "simplification"]
6.24 \<close> ML \<open>
6.25 val input = (["polynomial", "simplification"],
6.26 [("#Given", ["Simplify t_t"]), ("#Find", ["normalform n_n"])],
6.27 Rule_Set.empty, NONE (*cas*),
6.28 [["simplification","for_polynomials"]]) : Problem.input
6.29 \<close> ML \<open>
6.30 -Problem.prep_input_PIDE @{theory Poly} "guh" ["math-author-1"] ["polynomial", "simplification"]
6.31 +Problem.prep_input @{theory Poly} "guh" ["math-author-1"] ["polynomial", "simplification"]
6.32 input; (*! real !*)
6.33 \<close> ML \<open>
6.34 \<close> ML \<open>
6.35 \<close> ML \<open>
6.36 -"~~~~~ fun prep_input_PIDE , args:"; val (thy, guh, maa, init, (pblID, dsc_dats, ev, ca, metIDs)) =
6.37 +"~~~~~ fun prep_input , args:"; val (thy, guh, maa, init, (pblID, dsc_dats, ev, ca, metIDs)) =
6.38 (@{theory Poly}, "guh", ["math-author-1"], ["polynomial", "simplification"], input);
6.39 \<close> ML \<open>
6.40 fun eq f (f', _) = f = f';
6.41 @@ -222,7 +222,7 @@
6.42 \<close> ML \<open>
6.43 val (_, gi') :: [] = (*case*) gi (*of*);
6.44 \<close> ML \<open>
6.45 - map (Problem.split_did_PIDE o (Syntax.read_term_global thy)) gi'
6.46 + map (Problem.split_did o (Syntax.read_term_global thy)) gi'
6.47 \<close> ML \<open>
6.48 \<close> ML \<open>
6.49 (*+*)Syntax.read_term_global thy "Simplify t_t" (*Simplify :: "real => real"*)
7.1 --- a/src/Tools/isac/Interpret/derive.sml Fri Oct 07 20:46:48 2022 +0200
7.2 +++ b/src/Tools/isac/Interpret/derive.sml Sat Oct 08 11:40:48 2022 +0200
7.3 @@ -151,7 +151,7 @@
7.4 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::
7.5 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
7.6 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]
7.7 - val {nrls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
7.8 + val {nrls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
7.9 val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
7.10 val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
7.11 val pt = Ctree.update_branch pt p Ctree.TransitiveB
7.12 @@ -169,7 +169,7 @@
7.13 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
7.14 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
7.15 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
7.16 - val {nrls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
7.17 + val {nrls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
7.18 val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
7.19 val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
7.20 val pt = Ctree.update_branch pt p Ctree.TransitiveB
8.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Fri Oct 07 20:46:48 2022 +0200
8.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Sat Oct 08 11:40:48 2022 +0200
8.3 @@ -119,9 +119,9 @@
8.4 fun find_fill_patterns (pt, pos as (p, _): Pos.pos') id =
8.5 let
8.6 val f_curr = Ctree.get_curr_formula (pt, pos);
8.7 - val (_, _, _, ctxt) = LItool.parent_node_PIDE pt pos (*--------------- double code*)
8.8 + val (_, _, _, ctxt) = LItool.parent_node pt pos (*--------------- double code*)
8.9 val pp = Ctree.par_pblobj pt p (*by ^^^^^^^ replace with extension --- double code*)
8.10 - val (errpats, prog) = case MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
8.11 + val (errpats, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
8.12 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
8.13 | _ => raise ERROR "find_fill_patterns: uncovered case of get_met"
8.14 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
9.1 --- a/src/Tools/isac/Interpret/li-tool.sml Fri Oct 07 20:46:48 2022 +0200
9.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Sat Oct 08 11:40:48 2022 +0200
9.3 @@ -13,10 +13,10 @@
9.4 | Not_Associated;
9.5 val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass
9.6
9.7 - val parent_node_PIDE: Ctree.ctree -> Pos.pos' -> bool * Pos.pos * Rule_Set.T * Proof.context
9.8 + val parent_node: Ctree.ctree -> Pos.pos' -> bool * Pos.pos * Rule_Set.T * Proof.context
9.9 val init_pstate: Rule_Set.T -> Proof.context -> I_Model.T -> MethodC.id ->
9.10 Istate.T * Proof.context * Program.T
9.11 - val resume_prog_PIDE: Pos.pos' -> Ctree.ctree ->
9.12 + val resume_prog: Pos.pos' -> Ctree.ctree ->
9.13 (Istate.T * Proof.context) * Program.T
9.14
9.15 val check_leaf: string -> Proof.context -> Rule_Set.T -> (Env.T * (term option * term)) -> term ->
9.16 @@ -61,7 +61,7 @@
9.17 case find_first (test_dsc d) itms of
9.18 NONE => raise ERROR (error_msg_2 d itms)
9.19 | SOME (_, _, _, _, itm_) => I_Model.penvval_in itm_
9.20 - val pats = (#ppc o MethodC.from_store_PIDE ctxt) mI
9.21 + val pats = (#ppc o MethodC.from_store ctxt) mI
9.22 val _ = if pats = [] then raise ERROR error_msg_1 else ()
9.23 in (flat o (map (itm2arg itms))) pats end;
9.24
9.25 @@ -204,8 +204,8 @@
9.26 (trace_msg_3 ctxt tac; Not_Associated);
9.27
9.28 (* find the next parent, which is either a PblObj xor a PrfObj in case of detail step*)
9.29 -fun parent_node_PIDE _ ([], _) = (true, [], Rule_Set.Empty, ContextC.empty)
9.30 - | parent_node_PIDE pt (pos as (p, _)) =
9.31 +fun parent_node _ ([], _) = (true, [], Rule_Set.Empty, ContextC.empty)
9.32 + | parent_node pt (pos as (p, _)) =
9.33 let
9.34 fun par _ [] = (true, [], Rule_Set.Empty, ContextC.empty)
9.35 | par pt p =
9.36 @@ -273,7 +273,7 @@
9.37 let
9.38 val actuals = arguments_from_model ctxt metID itms
9.39 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
9.40 - val (scr, sc) = (case (#scr o MethodC.from_store_PIDE ctxt) metID of
9.41 + val (scr, sc) = (case (#scr o MethodC.from_store ctxt) metID of
9.42 scr as Rule.Prog sc => (trace_init ctxt metID; (scr, sc))
9.43 | _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string metID))
9.44 val formals = Program.formal_args sc
9.45 @@ -290,7 +290,7 @@
9.46 else
9.47 let val (f, a) = assoc_by_type f aas
9.48 in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
9.49 - val {pre, prls, ...} = MethodC.from_store_PIDE ctxt metID;
9.50 + val {pre, prls, ...} = MethodC.from_store ctxt metID;
9.51 val pres = Pre_Conds.check prls pre itms 0 |> snd |> map snd;
9.52 val ctxt = ctxt |> ContextC.insert_assumptions pres;
9.53 val ist = Istate.e_pstate
9.54 @@ -307,24 +307,24 @@
9.55 val p' = Ctree.par_pblobj pt p
9.56 val metID = Ctree.get_obj Ctree.g_metID pt p'
9.57 val ctxt = Ctree.get_ctxt pt pos
9.58 - val {srls, ...} = MethodC.from_store_PIDE ctxt metID
9.59 + val {srls, ...} = MethodC.from_store ctxt metID
9.60 in srls end
9.61
9.62 (* resume program interpretation at the beginning of a step *)
9.63 -fun resume_prog_PIDE pos pt =
9.64 +fun resume_prog pos pt =
9.65 let
9.66 - val (is_problem, p', rls', ctxt) = parent_node_PIDE pt pos (*is Ctree.PrfObj in case of detail step*)
9.67 + val (is_problem, p', rls', ctxt) = parent_node pt pos (*is Ctree.PrfObj in case of detail step*)
9.68 in
9.69 if is_problem then
9.70 let
9.71 val metID = get_obj g_metID pt p'
9.72 - val {srls, ...} = MethodC.from_store_PIDE ctxt metID
9.73 + val {srls, ...} = MethodC.from_store ctxt metID
9.74 val (is, ctxt) =
9.75 case get_loc pt pos of
9.76 (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt)
9.77 | _ => raise ERROR "resume_prog: unexpected result from get_loc"
9.78 in
9.79 - ((is, ctxt), (#scr o MethodC.from_store_PIDE ctxt) metID)
9.80 + ((is, ctxt), (#scr o MethodC.from_store ctxt) metID)
9.81 end
9.82 else
9.83 (get_loc pt pos,
10.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Fri Oct 07 20:46:48 2022 +0200
10.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Sat Oct 08 11:40:48 2022 +0200
10.3 @@ -271,7 +271,7 @@
10.4 Accept_Tac (tac, ist, ctxt) =>
10.5 Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac)
10.6 | Term_Val prog_result =>
10.7 - (case LItool.parent_node_PIDE pt pos of
10.8 + (case LItool.parent_node pt pos of
10.9 (true, p', _, _) =>
10.10 let
10.11 val (_, pblID, _) = get_obj g_spec pt p';
10.12 @@ -501,7 +501,7 @@
10.13 val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
10.14 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
10.15 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
10.16 - val {ppc, ...} = MethodC.from_store_PIDE ctxt mI;
10.17 + val {ppc, ...} = MethodC.from_store ctxt mI;
10.18 val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
10.19 val srls = LItool.get_simplifier (pt, pos)
10.20 val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
10.21 @@ -548,7 +548,7 @@
10.22 let
10.23 val parent_pos = par_pblobj pt p
10.24 val ctxt = Ctree.get_ctxt pt pos
10.25 - val {scr, ...} = MethodC.from_store_PIDE ctxt (get_obj g_metID pt parent_pos);
10.26 + val {scr, ...} = MethodC.from_store ctxt (get_obj g_metID pt parent_pos);
10.27 val prog_res =
10.28 case find_next_step scr (pt, pos) sub_ist sub_ctxt of
10.29 Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
10.30 @@ -591,7 +591,7 @@
10.31 else
10.32 let
10.33 val thy' = get_obj g_domID pt (par_pblobj pt p);
10.34 - val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
10.35 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
10.36 in
10.37 case find_next_step sc (pt, pos) ist ctxt of
10.38 Next_Step (ist, ctxt, tac) =>
10.39 @@ -617,7 +617,7 @@
10.40 let
10.41 val fo = Calc.current_formula ptp
10.42 val ctxt = Ctree.get_ctxt pt pos
10.43 - val {nrls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
10.44 + val {nrls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
10.45 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
10.46 val (found, der) = Derive.steps (Ctree.get_ctxt pt pos) rew_ord erls rules fo ifo; (*<---------------*)
10.47 in
11.1 --- a/src/Tools/isac/Interpret/solve-step.sml Fri Oct 07 20:46:48 2022 +0200
11.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Sat Oct 08 11:40:48 2022 +0200
11.3 @@ -43,13 +43,13 @@
11.4
11.5 fun get_ruleset _ (pos as (p, _)) pt =
11.6 let
11.7 - val (pbl, p', rls', ctxt) = LItool.parent_node_PIDE pt pos
11.8 + val (pbl, p', rls', ctxt) = LItool.parent_node pt pos
11.9 in
11.10 if pbl
11.11 then
11.12 let
11.13 val thy' = Ctree.get_obj Ctree.g_domID pt p'
11.14 - val {rew_ord', erls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt p')
11.15 + val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt p')
11.16 in ("OK", thy', rew_ord', erls, false) end
11.17 else
11.18 let
11.19 @@ -60,13 +60,13 @@
11.20
11.21 fun get_eval scrop (pos as (p, _)) pt =
11.22 let
11.23 - val (pbl, p', rls', ctxt) = LItool.parent_node_PIDE pt pos
11.24 + val (pbl, p', rls', ctxt) = LItool.parent_node pt pos
11.25 in
11.26 if pbl
11.27 then
11.28 let
11.29 val thy' = Ctree.get_obj Ctree.g_domID pt p'
11.30 - val {calc = scr_isa_fns, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt p')
11.31 + val {calc = scr_isa_fns, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt p')
11.32 val opt = assoc (scr_isa_fns, scrop)
11.33 in
11.34 case opt of
11.35 @@ -95,7 +95,7 @@
11.36 val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
11.37 Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
11.38 | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
11.39 - val {where_, ...} = Problem.from_store_PIDE ctxt pI
11.40 + val {where_, ...} = Problem.from_store ctxt pI
11.41 val pres = map (I_Model.environment probl |> subst_atomic) where_
11.42 val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
11.43 then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
11.44 @@ -152,7 +152,7 @@
11.45 val pp = Ctree.par_pblobj pt p;
11.46 val ctxt = Ctree.get_loc pt pos |> snd
11.47 val thy = Proof_Context.theory_of ctxt
11.48 - val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt pp);
11.49 + val {rew_ord' = ro', erls = erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp);
11.50 val f = Calc.current_formula cs;
11.51 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
11.52 in
11.53 @@ -195,7 +195,7 @@
11.54 val ctxt = Ctree.get_loc pt pos |> snd
11.55 val thy = Proof_Context.theory_of ctxt
11.56 val f = Calc.current_formula cs;
11.57 - val {rew_ord', erls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt pp)
11.58 + val {rew_ord', erls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp)
11.59 val subte = Subst.input_to_terms sube (*?TODO: input requires parse _: _ -> _ option?*)
11.60 val ro = get_rew_ord ctxt rew_ord'
11.61 in
12.1 --- a/src/Tools/isac/Interpret/step-solve.sml Fri Oct 07 20:46:48 2022 +0200
12.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Sat Oct 08 11:40:48 2022 +0200
12.3 @@ -46,7 +46,7 @@
12.4 end
12.5 else
12.6 let
12.7 - val (is, sc) = LItool.resume_prog_PIDE (p,p_) pt;
12.8 + val (is, sc) = LItool.resume_prog (p,p_) pt;
12.9 in
12.10 case LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m of
12.11 LI.Safe_Step (istate, ctxt, tac) =>
12.12 @@ -106,9 +106,9 @@
12.13 ("ok" , ([], [], cstate (* already contains istate, ctxt *)))
12.14 | LI.Not_Derivable =>
12.15 let
12.16 - val (_, _, _, ctxt) = LItool.parent_node_PIDE pt pos (*--------------- double code*)
12.17 + val (_, _, _, ctxt) = LItool.parent_node pt pos (*--------------- double code*)
12.18 val pp = Ctree.par_pblobj pt p (*by ^^^^^^^ replace with extension --- double code*)
12.19 - val (errpats, nrls, prog) = case MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
12.20 + val (errpats, nrls, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
12.21 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
12.22 | _ => raise ERROR "inform: uncovered case of get_met"
12.23 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
13.1 --- a/src/Tools/isac/Interpret/sub-problem.sml Fri Oct 07 20:46:48 2022 +0200
13.2 +++ b/src/Tools/isac/Interpret/sub-problem.sml Sat Oct 08 11:40:48 2022 +0200
13.3 @@ -18,23 +18,23 @@
13.4 if mI = ["no_met"]
13.5 then
13.6 let
13.7 - val pors = (M_Match.arguments thy ((#ppc o (Problem.from_store_PIDE ctxt)) pI) ags): O_Model.T
13.8 + val pors = (M_Match.arguments thy ((#ppc o (Problem.from_store ctxt)) pI) ags): O_Model.T
13.9 handle ERROR "actual args do not match formal args"
13.10 - => (M_Match.arguments_msg_PIDE ctxt pI stac ags (*raise exn*);[]);
13.11 - val pI' = Refine.refine_ori'_PIDE ctxt pors pI;
13.12 + => (M_Match.arguments_msg ctxt pI stac ags (*raise exn*);[]);
13.13 + val pI' = Refine.refine_ori' ctxt pors pI;
13.14 in (pI', pors (* refinement over models with diff.prec only *),
13.15 - (hd o #met o Problem.from_store_PIDE ctxt) pI') end
13.16 - else (pI, (M_Match.arguments thy ((#ppc o Problem.from_store_PIDE ctxt) pI) ags)
13.17 + (hd o #met o Problem.from_store ctxt) pI') end
13.18 + else (pI, (M_Match.arguments thy ((#ppc o Problem.from_store ctxt) pI) ags)
13.19 handle ERROR "actual args do not match formal args"
13.20 - => (M_Match.arguments_msg_PIDE ctxt pI stac ags(*raise exn*); []), mI);
13.21 + => (M_Match.arguments_msg ctxt pI stac ags(*raise exn*); []), mI);
13.22 val (fmz_, vals) = O_Model.values' pors;
13.23 - val {cas, ppc, thy, ...} = Problem.from_store_PIDE ctxt pI
13.24 + val {cas, ppc, thy, ...} = Problem.from_store ctxt pI
13.25 val dI = Context.theory_name thy (*take dI from _refined_ pbl*)
13.26 val dI = Context.theory_name (ThyC.sub_common (ThyC.get_theory dI, Ctree.rootthy pt))
13.27 val ctxt = ContextC.initialise dI vals
13.28 val hdl =
13.29 case cas of
13.30 - NONE => Auto_Prog.pblterm_PIDE dI pI
13.31 + NONE => Auto_Prog.pblterm dI pI
13.32 | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ vals) t
13.33 val f = Auto_Prog.subpbl (strip_thy dI) pI
13.34 in
14.1 --- a/src/Tools/isac/MathEngBasic/method.sml Fri Oct 07 20:46:48 2022 +0200
14.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Sat Oct 08 11:40:48 2022 +0200
14.3 @@ -19,15 +19,15 @@
14.4 val id_to_string: id -> string
14.5
14.6 type input
14.7 - (* TODO: ------------- remove always empty --- vvvvvvvvvvv -- vvv*)
14.8 - val prep_input_PIDE: theory -> Check_Unique.id -> string list -> id ->
14.9 + (* TODO: ------------ remove always empty --- vvvvvvvvvvv -- vvv*)
14.10 + val prep_input: theory -> Check_Unique.id -> string list -> id ->
14.11 id * Problem.model_input * input * thm -> T * id
14.12
14.13 val set_data: input -> theory -> theory
14.14 val the_data: theory -> input
14.15
14.16 - val from_store'_PIDE: theory -> id -> T
14.17 - val from_store_PIDE: Proof.context -> id -> T
14.18 + val from_store': theory -> id -> T
14.19 + val from_store: Proof.context -> id -> T
14.20 end
14.21
14.22 (**)
14.23 @@ -50,7 +50,7 @@
14.24 {calc: Rule_Def.eval_ml_from_prog list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T,
14.25 prls: Rule_Set.T, rew_ord': Rewrite_Ord.id, rls': Rule_Set.T, srls: Rule_Set.T}
14.26
14.27 -fun prep_input_PIDE thy guh (mathauthors: string list) (init: References_Def.id)
14.28 +fun prep_input thy guh (mathauthors: string list) (init: References_Def.id)
14.29 (metID, ppc,
14.30 {rew_ord' = ro, rls' = rls, srls = srls, prls = prls, calc = _(*scr_isa_fns*), crls = cr,
14.31 errpats = ep, nrls = nr}, scr) =
14.32 @@ -60,7 +60,7 @@
14.33 val gi = (case gi of
14.34 [] => (writeln ("prep_input: in " ^ guh ^ " #Given is empty ?!?"); [])
14.35 | ((_, gi') :: []) =>
14.36 - (*(case \<^try>\<open> *)map (Problem.split_did_PIDE o (Syntax.read_term_global thy)) gi'(*\<close> of
14.37 + (*(case \<^try>\<open> *)map (Problem.split_did o (Syntax.read_term_global thy)) gi'(*\<close> of
14.38 SOME x => x
14.39 | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID))*)
14.40 | _ => raise ERROR ("prep_pbt: more than one '#Given' in " ^ strs2str metID));
14.41 @@ -70,7 +70,7 @@
14.42 val fi = (case fi of
14.43 [] => (writeln ("prep_input: in " ^ guh ^ " #Find is empty ?!?"); [])
14.44 | ((_, fi') :: []) =>
14.45 - (*(case \<^try>\<open> *)map (Problem.split_did_PIDE o (Syntax.read_term_global thy)) fi'(*\<close> of
14.46 + (*(case \<^try>\<open> *)map (Problem.split_did o (Syntax.read_term_global thy)) fi'(*\<close> of
14.47 SOME x => x
14.48 | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID))*)
14.49 | _ => raise ERROR ("prep_pbt: more than one '#Find' in " ^ strs2str metID));
14.50 @@ -80,7 +80,7 @@
14.51 val re = (case re of
14.52 [] => (writeln ("prep_input: in " ^ guh ^ " #Relate is empty ?!?"); [])
14.53 | ((_,re') :: []) =>
14.54 - (*(case \<^try>\<open> *) map (Problem.split_did_PIDE o (Syntax.read_term_global thy)) re'(*\<close> of
14.55 + (*(case \<^try>\<open> *) map (Problem.split_did o (Syntax.read_term_global thy)) re'(*\<close> of
14.56 SOME x => x
14.57 | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID))*)
14.58 | _ => raise ERROR ("prep_pbt: more than one '#Relate' in " ^ strs2str metID));
14.59 @@ -141,7 +141,7 @@
14.60 (case program of
14.61 NONE => @{thm refl}
14.62 | SOME a => Global_Theory.get_thm thy (Global_Theory.check_fact thy a));
14.63 - val arg = prep_input_PIDE thy name maa id_empty (metID, model_input, input, thm);
14.64 + val arg = prep_input thy name maa id_empty (metID, model_input, input, thm);
14.65 in KEStore_Elems.add_mets @{context} [arg] thy end)))
14.66
14.67 in end;
14.68 @@ -161,12 +161,11 @@
14.69 end
14.70
14.71 (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)
14.72 -fun from_store'_PIDE thy id =
14.73 +fun from_store' thy id =
14.74 (Store.get (KEStore_Elems.get_mets thy) id id)
14.75 handle ERROR _ =>
14.76 raise error ("*** ERROR MethodC.from_store thy " ^ strs2str id ^ " not found");
14.77 -
14.78 -fun from_store_PIDE ctxt id =
14.79 +fun from_store ctxt id =
14.80 let
14.81 val pbl = Store.get (get_mets ()) id id
14.82 in adapt_to_type ctxt pbl end
15.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Fri Oct 07 20:46:48 2022 +0200
15.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Sat Oct 08 11:40:48 2022 +0200
15.3 @@ -21,11 +21,9 @@
15.4
15.5 type input
15.6 type model_input
15.7 -(*val split_did: term -> term * term*)
15.8 - val split_did_PIDE: term -> term * term
15.9 - (* TODO: ---------- remove always empty --- vvvvvvvvvvv -- vvv*)
15.10 -(*val prep_input : theory -> Check_Unique.id -> string list -> id -> input -> T * id*)
15.11 - val prep_input_PIDE : theory -> Check_Unique.id -> string list -> id -> input -> T * id
15.12 + val split_did: term -> term * term
15.13 + (* TODO: ---------- remove always empty ----- vvvvvvvvvvv -- vvv*)
15.14 + val prep_input : theory -> Check_Unique.id -> string list -> id -> input -> T * id
15.15
15.16 val set_data: Rule_Def.rule_set -> theory -> theory
15.17 val the_data: theory -> Rule_Def.rule_set
15.18 @@ -41,7 +39,7 @@
15.19
15.20 (*val adapt_to_type: Proof.context -> T -> T*)
15.21 (** )val from_store: id -> T( **)
15.22 - val from_store_PIDE: Proof.context -> id -> T
15.23 + val from_store: Proof.context -> id -> T
15.24 end
15.25
15.26 (**)
15.27 @@ -79,116 +77,60 @@
15.28 Meth_Def.id list; (* methods that can solve the problem *)
15.29
15.30 (* split a term into description and (id | structured variable) for pbt, met.ppc *)
15.31 -(*
15.32 fun split_did t =
15.33 let
15.34 val (hd, arg) = case strip_comb t of
15.35 (hd, [arg]) => (hd, arg)
15.36 - | _ => raise ERROR ("split_did: doesn't match (hd,[arg]) for t = " ^ UnparseC.term t)
15.37 - in (hd, arg) end
15.38 -*)
15.39 -fun split_did_PIDE t =
15.40 - let
15.41 - val (hd, arg) = case strip_comb t of
15.42 - (hd, [arg]) => (hd, arg)
15.43 - | _ => raise ERROR ("split_did_PIDE: doesn't match (hd,[arg]) for t = xxxxx" (*^ UnparseC.term t*))
15.44 + | _ => raise ERROR ("split_did: doesn't match (hd,[arg]) for t = xxxxx" (*^ UnparseC.term t*))
15.45 in (hd, arg) end
15.46
15.47 (* prepare problem-types before storing in pbltypes;
15.48 - dont forget to "check_guh_unique" before ins *)
15.49 -(*
15.50 -fun prep_input thy guh maa init ((pblID, dsc_dats, ev, ca, metIDs): input) : T * id =
15.51 + dont forget to "check_guh_unique" before inserting *)
15.52 +fun prep_input thy guh maa init (pblID, dsc_dats, ev, ca, metIDs) =
15.53 let
15.54 fun eq f (f', _) = f = f';
15.55 +val _ = writeln "#prep_input 1";
15.56 val gi = filter (eq "#Given") dsc_dats;
15.57 +val _ = writeln "#prep_input 1a";
15.58 val gi = (case gi of
15.59 [] => []
15.60 | ((_, gi') :: []) =>
15.61 - (case \<^try>\<open> map (split_did o (TermC.parseNEW'' thy)) gi'\<close> of
15.62 - SOME x => x
15.63 - | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Given' of " ^ strs2str pblID))
15.64 - | _ => raise ERROR ("prep_input: more than one '#Given' in " ^ strs2str pblID));
15.65 + map (split_did o (Syntax.read_term_global thy)) gi'
15.66 + | _ => raise ERROR ("prep_input: more than one '#Given' in xxxxx" (*^ strs2str pblID*)));
15.67 +val _ = writeln "#prep_input 1b";
15.68 val gi = map (pair "#Given") gi;
15.69
15.70 +val _ = writeln "#prep_input 2";
15.71 val fi = filter (eq "#Find") dsc_dats;
15.72 val fi = (case fi of
15.73 [] => []
15.74 | ((_, fi') :: []) =>
15.75 - (case \<^try>\<open> map (split_did o (TermC.parseNEW'' thy)) fi'\<close> of
15.76 + (*(case \<^try>\<open> *)map (split_did o (Syntax.read_term_global thy)) fi'(*\<close> of
15.77 SOME x => x
15.78 - | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Find' of " ^ strs2str pblID))
15.79 - | _ => raise ERROR ("prep_input: more than one '#Find' in " ^ strs2str pblID));
15.80 + | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Find' of " ^ strs2str pblID))*)
15.81 + | _ => raise ERROR ("prep_input: more than one '#Find' in xxxxx" (*^ strs2str pblID*)));
15.82 val fi = map (pair "#Find") fi;
15.83
15.84 +val _ = writeln "#prep_input 3";
15.85 val re = filter (eq "#Relate") dsc_dats;
15.86 val re = (case re of
15.87 [] => []
15.88 | ((_, re') :: []) =>
15.89 - (case \<^try>\<open> map (split_did o (TermC.parseNEW'' thy)) re'\<close> of
15.90 + (*(case \<^try>\<open> *)map (split_did o (Syntax.read_term_global thy)) re'(*\<close> of
15.91 SOME x => x
15.92 - | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Relate' of " ^ strs2str pblID))
15.93 - | _ => raise ERROR ("prep_input: more than one '#Relate' in " ^ strs2str pblID));
15.94 + | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Relate' of " ^ strs2str pblID))*)
15.95 + | _ => raise ERROR ("prep_input: more than one '#Relate' in xxxxx" (*^ strs2str pblID*)));
15.96 val re = map (pair "#Relate") re;
15.97
15.98 - val wh = filter (eq "#Where") dsc_dats;
15.99 - val wh = (case wh of
15.100 - [] => []
15.101 - | ((_, wh') :: []) =>
15.102 - (case \<^try>\<open> map (TermC.parse_patt thy) wh'\<close> of
15.103 - SOME x => x
15.104 - | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Where' of " ^ strs2str pblID))
15.105 - | _ => raise ERROR ("prep_input: more than one '#Where' in " ^ strs2str pblID));
15.106 - in
15.107 - ({guh = guh, mathauthors = maa, init = init, thy = thy,
15.108 - cas = Option.map (TermC.parseNEW'' thy) ca,
15.109 - prls = ev, where_ = wh, ppc = gi @ fi @ re, met = metIDs}, pblID)
15.110 - end;
15.111 -*)
15.112 -fun prep_input_PIDE thy guh maa init (pblID, dsc_dats, ev, ca, metIDs) =
15.113 - let
15.114 - fun eq f (f', _) = f = f';
15.115 -val _ = writeln "#prep_input_PIDE 1";
15.116 - val gi = filter (eq "#Given") dsc_dats;
15.117 -val _ = writeln "#prep_input_PIDE 1a";
15.118 - val gi = (case gi of
15.119 - [] => []
15.120 - | ((_, gi') :: []) =>
15.121 - map (split_did_PIDE o (Syntax.read_term_global thy)) gi'
15.122 - | _ => raise ERROR ("prep_input_PIDE: more than one '#Given' in xxxxx" (*^ strs2str pblID*)));
15.123 -val _ = writeln "#prep_input_PIDE 1b";
15.124 - val gi = map (pair "#Given") gi;
15.125 -
15.126 -val _ = writeln "#prep_input_PIDE 2";
15.127 - val fi = filter (eq "#Find") dsc_dats;
15.128 - val fi = (case fi of
15.129 - [] => []
15.130 - | ((_, fi') :: []) =>
15.131 - (*(case \<^try>\<open> *)map (split_did_PIDE o (Syntax.read_term_global thy)) fi'(*\<close> of
15.132 - SOME x => x
15.133 - | NONE => raise ERROR ("prep_input_PIDE: syntax raise ERROR in '#Find' of " ^ strs2str pblID))*)
15.134 - | _ => raise ERROR ("prep_input_PIDE: more than one '#Find' in xxxxx" (*^ strs2str pblID*)));
15.135 - val fi = map (pair "#Find") fi;
15.136 -
15.137 -val _ = writeln "#prep_input_PIDE 3";
15.138 - val re = filter (eq "#Relate") dsc_dats;
15.139 - val re = (case re of
15.140 - [] => []
15.141 - | ((_, re') :: []) =>
15.142 - (*(case \<^try>\<open> *)map (split_did_PIDE o (Syntax.read_term_global thy)) re'(*\<close> of
15.143 - SOME x => x
15.144 - | NONE => raise ERROR ("prep_input_PIDE: syntax raise ERROR in '#Relate' of " ^ strs2str pblID))*)
15.145 - | _ => raise ERROR ("prep_input_PIDE: more than one '#Relate' in xxxxx" (*^ strs2str pblID*)));
15.146 - val re = map (pair "#Relate") re;
15.147 -
15.148 -val _ = writeln "#prep_input_PIDE 4";
15.149 +val _ = writeln "#prep_input 4";
15.150 val wh = filter (eq "#Where") dsc_dats;
15.151 val wh = (case wh of
15.152 [] => []
15.153 | ((_, wh') :: []) => (*special case in parsing*)
15.154 (*(case \<^try>\<open> *)map (TermC.parse_patt_PIDE thy) wh'(*\<close> of
15.155 SOME x => x
15.156 - | NONE => raise ERROR ("prep_input_PIDE: syntax raise ERROR in '#Where' of " ^ strs2str pblID))*)
15.157 - | _ => raise ERROR ("prep_input_PIDE: more than one '#Where' in xxxxx" (*^ strs2str pblID*)));
15.158 + | NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Where' of " ^ strs2str pblID))*)
15.159 + | _ => raise ERROR ("prep_input: more than one '#Where' in xxxxx" (*^ strs2str pblID*)));
15.160 in
15.161 ({guh = guh, mathauthors = maa, init = init, thy = thy,
15.162 cas = Option.map (Syntax.read_term_global thy) ca,
15.163 @@ -261,7 +203,7 @@
15.164 |> Context.theory_map;
15.165 (*val _ = writeln ("#problem set_data: " ^ @{make_string} set_data)*)
15.166 (* Context.theory_map HAS STORED THE ml-source IN Theory_Data ALREADY,
15.167 - BUT prep_input_PIDE REQUIRES ml-source AGAIN ... *)
15.168 + BUT prep_input REQUIRES ml-source AGAIN ... *)
15.169 val input = the_data (set_data thy);
15.170 (*val _ = writeln ("#problem input: " ^ @{make_string} input)*)
15.171
15.172 @@ -277,9 +219,9 @@
15.173 * ? preserve Position.T etc within ML_Lex.token Antiquote.antiquote list ?..
15.174 ..in analogy to set_data ?!?
15.175 * by Context.theory_map notify Isabelle/PIDE of errors from model_input at Position.T
15.176 - * in case there are no errors, do prep_input_PIDE (to be simplified)
15.177 + * in case there are no errors, do prep_input (to be simplified)
15.178 *)
15.179 - val arg = prep_input_PIDE thy name maa id_empty (pblID, model_input, input, cas, metIDs);
15.180 + val arg = prep_input thy name maa id_empty (pblID, model_input, input, cas, metIDs);
15.181 in KEStore_Elems.add_pbls @{context} [arg] thy end)))
15.182
15.183 in end;
15.184 @@ -306,7 +248,7 @@
15.185 handle ERROR _ =>
15.186 raise error ("*** ERROR Problem.from_store " ^ strs2str id ^ " not found");
15.187 ( **)
15.188 -fun from_store_PIDE ctxt id =
15.189 +fun from_store ctxt id =
15.190 let
15.191 val pbl = Store.get (get_pbls ()) id (rev id)
15.192 in adapt_to_type ctxt pbl end
16.1 --- a/src/Tools/isac/MathEngine/fetch-tactics.sml Fri Oct 07 20:46:48 2022 +0200
16.2 +++ b/src/Tools/isac/MathEngine/fetch-tactics.sml Sat Oct 08 11:40:48 2022 +0200
16.3 @@ -32,7 +32,7 @@
16.4 val ctxt = Ctree.get_ctxt pt pos
16.5 val metID = get_obj g_metID pt pp;
16.6 val metID' = if metID = MethodC.id_empty then (thd3 o snd3) (get_obj g_origin pt pp) else metID
16.7 - val (sc, srls) = (case MethodC.from_store_PIDE ctxt metID' of
16.8 + val (sc, srls) = (case MethodC.from_store ctxt metID' of
16.9 {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => raise ERROR "from_prog 1")
16.10 val subst = get_istate_LI pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
16.11 val ctxt = get_ctxt pt (p, p_)
16.12 @@ -58,7 +58,7 @@
16.13 if metID = MethodC.id_empty
16.14 then (get_obj g_origin pt pp) |> #2 |> #3
16.15 else metID
16.16 - val (sc, srls, erls, ro) = (case MethodC.from_store_PIDE ctxt metID' of
16.17 + val (sc, srls, erls, ro) = (case MethodC.from_store ctxt metID' of
16.18 {scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
16.19 | _ => raise ERROR "specific_from_prog 1")
16.20 val (env, (a, v)) = (case get_istate_LI pt pos of
17.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Fri Oct 07 20:46:48 2022 +0200
17.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Sat Oct 08 11:40:48 2022 +0200
17.3 @@ -140,7 +140,7 @@
17.4 if pI' = Problem.id_empty
17.5 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
17.6 else pI'
17.7 - val {ppc, where_, prls, ...} = Problem.from_store_PIDE ctxt pblID
17.8 + val {ppc, where_, prls, ...} = Problem.from_store ctxt pblID
17.9 val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc, where_, prls) os
17.10 in
17.11 (model_ok, pblID, hdl, pbl, pre)
17.12 @@ -156,7 +156,7 @@
17.13 val metID = if mI' = MethodC.id_empty
17.14 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
17.15 else mI'
17.16 - val {ppc, pre, prls, scr, ...} = MethodC.from_store_PIDE ctxt metID
17.17 + val {ppc, pre, prls, scr, ...} = MethodC.from_store ctxt metID
17.18 val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
17.19 in
17.20 (model_ok, metID, scr, pbl, pre)
17.21 @@ -170,7 +170,7 @@
17.22 Ctree.PblObj {probl, origin = (os, ospec, hdl), spec, ...} => (probl, os, ospec, hdl, spec)
17.23 | Ctree.PrfObj _ => raise ERROR "context_pbl: uncovered case"
17.24 val ctxt = spec |> References.select_input ospec |> #1 |> ThyC.get_theory |> Proof_Context.init_global
17.25 - val {ppc, where_, prls, ...} = Problem.from_store_PIDE ctxt pI
17.26 + val {ppc, where_, prls, ...} = Problem.from_store ctxt pI
17.27 val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
17.28 in
17.29 (model_ok, pI, hdl, pbl, pre)
17.30 @@ -182,7 +182,7 @@
17.31 case Ctree.get_obj I pt p of
17.32 Ctree.PblObj {meth, origin = (os, _, _), ctxt, ...} => (meth, os, ctxt)
17.33 | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case"
17.34 - val {ppc,pre,prls,scr,...} = MethodC.from_store_PIDE ctxt mI
17.35 + val {ppc,pre,prls,scr,...} = MethodC.from_store ctxt mI
17.36 val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
17.37 in
17.38 (model_ok, mI, scr, pbl, pre)
17.39 @@ -199,7 +199,7 @@
17.40 case Refine.problem (ThyC.get_theory "Isac_Knowledge") pI probl of
17.41 NONE => (*copy from context_pbl*)
17.42 let
17.43 - val {ppc, where_, prls, ...} = Problem.from_store_PIDE ctxt pI
17.44 + val {ppc, where_, prls, ...} = Problem.from_store ctxt pI
17.45 val (_, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
17.46 in
17.47 (false, pI, hdl, pbl, pre)
18.1 --- a/src/Tools/isac/MathEngine/me-misc.sml Fri Oct 07 20:46:48 2022 +0200
18.2 +++ b/src/Tools/isac/MathEngine/me-misc.sml Sat Oct 08 11:40:48 2022 +0200
18.3 @@ -21,7 +21,7 @@
18.4 val pre = if metID = MethodC.id_empty then []
18.5 else
18.6 let
18.7 - val {prls, pre = where_, ...} = MethodC.from_store_PIDE ctxt metID
18.8 + val {prls, pre = where_, ...} = MethodC.from_store ctxt metID
18.9 val (_, pre) = Pre_Conds.check prls where_ meth 0
18.10 in pre end
18.11 val allcorrect = I_Model.is_complete meth andalso foldl and_ (true, (map #1 pre))
18.12 @@ -35,7 +35,7 @@
18.13 val pre = if pI = Problem.id_empty then []
18.14 else
18.15 let
18.16 - val {prls, where_, ...} = Problem.from_store_PIDE ctxt pI
18.17 + val {prls, where_, ...} = Problem.from_store ctxt pI
18.18 val (_, pre) = Pre_Conds.check prls where_ probl 0
18.19 in pre end
18.20 val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 pre))
18.21 @@ -49,9 +49,9 @@
18.22 let
18.23 val (dI, pI, _) = Ctree.get_somespec' spec spec'
18.24 val ctxt = Proof_Context.init_global (ThyC.get_theory dI)
18.25 - val {cas, ...} = Problem.from_store_PIDE ctxt pI
18.26 + val {cas, ...} = Problem.from_store ctxt pI
18.27 in case cas of
18.28 - NONE => Ctree.Form (Auto_Prog.pblterm_PIDE dI pI)
18.29 + NONE => Ctree.Form (Auto_Prog.pblterm dI pI)
18.30 | SOME t => Ctree.Form (subst_atomic (I_Model.environment probl) t)
18.31 end
18.32
19.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Fri Oct 07 20:46:48 2022 +0200
19.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Sat Oct 08 11:40:48 2022 +0200
19.3 @@ -28,8 +28,7 @@
19.4 val contain_bdv: Rule.rule list -> bool
19.5 val contains_bdv: thm -> bool
19.6 val subst_typs: term -> typ -> typ -> term
19.7 -(* val pblterm: ThyC.id -> Probl_Def.id -> term*)
19.8 - val pblterm_PIDE: ThyC.id -> Probl_Def.id -> term
19.9 + val pblterm: ThyC.id -> Probl_Def.id -> term
19.10 val subpbl: string -> string list -> term
19.11 val stacpbls: term -> term list
19.12 val op_of_calc: term -> string
19.13 @@ -57,18 +56,11 @@
19.14 needs to be here after def. Subproblem in Prog_Tac.thy *)
19.15 val subpbl_t $ (pair_t $ _ $ _) = (TermC.parseNEW'' @{theory Prog_Tac})
19.16 "Subproblem (''Isac_Knowledge'',[''equation'',''univar''])"
19.17 -val pbl_t $ _ =
19.18 - (TermC.parseNEW'' @{theory Prog_Tac}) "Problem (''Isac_Knowledge'',[''equation'',''univar''])"
19.19
19.20 fun subpbl domID pblID =
19.21 subpbl_t $ (pair_t $ HOLogic.mk_string domID $
19.22 list_comb (Syntax.const @{const_syntax Char}, map HOLogic.mk_string pblID));
19.23 -(*
19.24 fun pblterm domID pblID =
19.25 - pbl_t $ (pair_t $ HOLogic.mk_string domID $
19.26 - list_comb (Syntax.const @{const_syntax Char}, map HOLogic.mk_string pblID));
19.27 -*)
19.28 -fun pblterm_PIDE domID pblID =
19.29 pair_t $ HOLogic.mk_string domID $
19.30 list_comb (Syntax.const @{const_syntax Char}, map HOLogic.mk_string pblID);
19.31
19.32 @@ -156,9 +148,10 @@
19.33 | op #>@ sts (s::ss) = op #>@ (SEq $ s $ sts) ss
19.34 | op #>@ t ts =
19.35 raise ERROR ("fun #>@ not applicable to \"" ^ UnparseC.term t ^ "\" \"" ^ UnparseC.terms ts ^ "\"");
19.36 -fun #> [stac] = stac
19.37 - | #> [s1, s2] = SEq $ s1 $ s2
19.38 - | #> stacs = case rev stacs of
19.39 +(*IS NOT*)
19.40 +fun op #> [stac] = stac
19.41 + | op #> [s1, s2] = SEq $ s1 $ s2
19.42 + | op #> stacs = case rev stacs of
19.43 s3 :: s2 :: ss => op #>@ (SEq $ s2 $ s3) ss
19.44 | ts => raise ERROR ("fun #> not applicable to \"" ^ UnparseC.terms ts ^ "\"")
19.45
20.1 --- a/src/Tools/isac/Specify/cas-command.sml Fri Oct 07 20:46:48 2022 +0200
20.2 +++ b/src/Tools/isac/Specify/cas-command.sml Sat Oct 08 11:40:48 2022 +0200
20.3 @@ -43,7 +43,7 @@
20.4 let
20.5 val thy = ThyC.get_theory dI
20.6 val ctxt = Proof_Context.init_global thy
20.7 - val {ppc, ...} = Problem.from_store_PIDE ctxt pI
20.8 + val {ppc, ...} = Problem.from_store ctxt pI
20.9 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
20.10 val its = O_Model.add_enumerate its_
20.11 val pits = map flattup2 its
20.12 @@ -52,9 +52,9 @@
20.13 then (pI, mI)
20.14 else
20.15 case Refine.problem thy pI pits of
20.16 - SOME (pI,_) => (pI, (hd o #met o Problem.from_store_PIDE ctxt) pI)
20.17 - | NONE => (pI, (hd o #met o Problem.from_store_PIDE ctxt) pI)
20.18 - val {ppc, pre, prls, ...} = MethodC.from_store_PIDE ctxt mI
20.19 + SOME (pI,_) => (pI, (hd o #met o Problem.from_store ctxt) pI)
20.20 + | NONE => (pI, (hd o #met o Problem.from_store ctxt) pI)
20.21 + val {ppc, pre, prls, ...} = MethodC.from_store ctxt mI
20.22 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
20.23 val its = O_Model.add_enumerate its_
20.24 val mits = map flattup2 its
20.25 @@ -102,7 +102,7 @@
20.26 Parse.!!! (Parse.ML_source -- parse_theory -- parse_problem -- parse_method))
20.27 >> (fn (term, (((source, thry), pbl), met)) => Toplevel.theory (fn thy =>
20.28 let
20.29 - val t = TermC.parse_strict(*parse_strict_PIDE*) thy term;
20.30 + val t = TermC.parse_strict thy term;
20.31 val pblID = References_Def.explode_id pbl;
20.32 val metID = References_Def.explode_id met;
20.33 val set_data =
21.1 --- a/src/Tools/isac/Specify/m-match.sml Fri Oct 07 20:46:48 2022 +0200
21.2 +++ b/src/Tools/isac/Specify/m-match.sml Sat Oct 08 11:40:48 2022 +0200
21.3 @@ -203,29 +203,15 @@
21.4 in (map flattup ors) end
21.5
21.6 (* report part of the error-msg which is not available in match_args *)
21.7 -(*
21.8 -fun arguments_msg pI stac ags =
21.9 +fun arguments_msg ctxt pI stac ags =
21.10 let
21.11 - val pats = (#ppc o Problem.from_store) pI
21.12 + val pats = (#ppc o Problem.from_store ctxt) pI
21.13 val msg = (dots 70 ^ "\n"
21.14 ^ "*** problem " ^ strs2str pI ^ " has the ...\n"
21.15 ^ "*** model-pattern " ^ Model_Pattern.to_string pats ^ "\n"
21.16 ^ "*** stac '" ^ UnparseC.term stac ^ "' has the ...\n"
21.17 ^ "*** arg-list " ^ UnparseC.terms ags ^ "\n"
21.18 ^ dashs 70)
21.19 - (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
21.20 - in tracing msg end
21.21 -*)
21.22 -fun arguments_msg_PIDE ctxt pI stac ags =
21.23 - let
21.24 - val pats = (#ppc o Problem.from_store_PIDE ctxt) pI
21.25 - val msg = (dots 70 ^ "\n"
21.26 - ^ "*** problem " ^ strs2str pI ^ " has the ...\n"
21.27 - ^ "*** model-pattern " ^ Model_Pattern.to_string pats ^ "\n"
21.28 - ^ "*** stac '" ^ UnparseC.term stac ^ "' has the ...\n"
21.29 - ^ "*** arg-list " ^ UnparseC.terms ags ^ "\n"
21.30 - ^ dashs 70)
21.31 - (*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
21.32 in tracing msg end
21.33
21.34 (**)end(**)
22.1 --- a/src/Tools/isac/Specify/p-spec.sml Fri Oct 07 20:46:48 2022 +0200
22.2 +++ b/src/Tools/isac/Specify/p-spec.sml Sat Oct 08 11:40:48 2022 +0200
22.3 @@ -228,13 +228,13 @@
22.4 then let val its = map (parsitm (ThyC.get_theory dI)) probl;
22.5 val (its, trms) = filter_sep is_Par its;
22.6 val pbt =
22.7 - (#ppc o Problem.from_store_PIDE ctxt) (#2 (References.select_input ospec sspec))
22.8 + (#ppc o Problem.from_store ctxt) (#2 (References.select_input ospec sspec))
22.9 in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
22.10 else
22.11 if pI <> spI
22.12 then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
22.13 else
22.14 - let val pbt = (#ppc o Problem.from_store_PIDE ctxt) pI
22.15 + let val pbt = (#ppc o Problem.from_store ctxt) pI
22.16 val dI' = #1 (References.select_input ospec spec)
22.17 val oris =
22.18 if pI = #2 ospec then oris
22.19 @@ -242,20 +242,20 @@
22.20 in (Pos.Pbl, appl_adds dI' oris probl pbt
22.21 (map itms2fstr probl), meth) end
22.22 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
22.23 - then let val met = (#ppc o MethodC.from_store_PIDE ctxt) mI
22.24 + then let val met = (#ppc o MethodC.from_store ctxt) mI
22.25 val mits = I_Model.complete oris probl meth met
22.26 in if foldl and_ (true, map #3 mits)
22.27 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
22.28 end
22.29 else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)]
22.30 - ((#ppc o Problem.from_store_PIDE ctxt)
22.31 + ((#ppc o Problem.from_store ctxt)
22.32 (#2 (References.select_input ospec spec)))
22.33 (imodel2fstr imodel), meth)
22.34 val pt = Ctree.update_spec pt p spec;
22.35 in if pos_ = Pos.Pbl
22.36 then
22.37 let
22.38 - val {prls, where_,...} = Problem.from_store_PIDE ctxt
22.39 + val {prls, where_,...} = Problem.from_store ctxt
22.40 (#2 (References.select_input ospec spec))
22.41 val (_, pre) = Pre_Conds.check prls where_ pits 0
22.42 in (Ctree.update_pbl pt p pits,
22.43 @@ -263,7 +263,7 @@
22.44 end
22.45 else
22.46 let
22.47 - val {prls,pre,...} = MethodC.from_store_PIDE ctxt
22.48 + val {prls,pre,...} = MethodC.from_store ctxt
22.49 (#3 (References.select_input ospec spec))
22.50 val (_, pre) = Pre_Conds.check prls pre mits 0
22.51 in (Ctree.update_met pt p mits,
23.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Fri Oct 07 20:46:48 2022 +0200
23.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Sat Oct 08 11:40:48 2022 +0200
23.3 @@ -25,7 +25,6 @@
23.4 (*type unchecked = term list*)
23.5 (*type checked = Pre_Conds_Def.T;*)
23.6 type T = Pre_Conds_Def.T; (*= (bool * term) list;*)
23.7 -(**)
23.8 type input = string list;
23.9
23.10 fun to_str (b, t) = pair2str (bool2str b, UnparseC.term t);
24.1 --- a/src/Tools/isac/Specify/refine.sml Fri Oct 07 20:46:48 2022 +0200
24.2 +++ b/src/Tools/isac/Specify/refine.sml Sat Oct 08 11:40:48 2022 +0200
24.3 @@ -30,11 +30,9 @@
24.4 val problem: theory -> Problem.id -> I_Model.T -> (Problem.id * (I_Model.T * Pre_Conds.T)) option
24.5
24.6 (**)
24.7 -(*val refine_ori : O_Model.T -> Problem.id -> Problem.id option*)
24.8 - val refine_ori_PIDE : Proof.context -> O_Model.T -> Problem.id -> Problem.id option
24.9 + val refine_ori : Proof.context -> O_Model.T -> Problem.id -> Problem.id option
24.10 (**)
24.11 -(*val refine_ori' : O_Model.T -> Problem.id -> Problem.id*)
24.12 - val refine_ori'_PIDE : Proof.context -> O_Model.T -> Problem.id -> Problem.id
24.13 + val refine_ori' : Proof.context -> O_Model.T -> Problem.id -> Problem.id
24.14
24.15 \<^isac_test>\<open>
24.16 (*val for_author : Formalise.model -> Problem.id -> M_Match.T list*)
24.17 @@ -50,7 +48,7 @@
24.18 val refins'': theory -> Problem.id -> I_Model.T -> match_ list -> Problem.T Store.node list -> match_ list
24.19 (**)
24.20 (*val refin: Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)
24.21 - val refin_PIDE: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option
24.22 + val refin: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option
24.23 \<close>
24.24 end
24.25
24.26 @@ -191,8 +189,8 @@
24.27 ( ** )TODO clean up after "... "adapt to current ctxt"( **)
24.28
24.29 (*val refin: Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)
24.30 -(*val refin_PIDE: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)
24.31 -fun refin_PIDE ctxt pblRD ori (Store.Node (pI, [py], [])) =
24.32 +(*val refin: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)
24.33 +fun refin ctxt pblRD ori (Store.Node (pI, [py], [])) =
24.34 let
24.35 val {thy, prls, ppc, where_, ...} = py: Problem.T
24.36 val ppc = map (Model_Pattern.adapt_to_type ctxt) ppc
24.37 @@ -202,7 +200,7 @@
24.38 then SOME (pblRD @ [pI])
24.39 else NONE
24.40 end
24.41 - | refin_PIDE ctxt pblRD ori (Store.Node (pI, [py], pys)) =
24.42 + | refin ctxt pblRD ori (Store.Node (pI, [py], pys)) =
24.43 let
24.44 val {prls, ppc, where_, ...} = py: Problem.T
24.45 val ppc = map (Model_Pattern.adapt_to_type ctxt) ppc
24.46 @@ -214,10 +212,10 @@
24.47 | NONE => SOME (pblRD @ [pI]))
24.48 else NONE
24.49 end
24.50 - | refin_PIDE _ _ _ _ = raise ERROR "refin_PIDE: uncovered fun def."
24.51 + | refin _ _ _ _ = raise ERROR "refin: uncovered fun def."
24.52 and refins_PIDE _ _ _ [] = NONE
24.53 | refins_PIDE ctxt pblRD ori ((p as Store.Node _) :: pts) =
24.54 - (case refin_PIDE ctxt pblRD ori p of
24.55 + (case refin ctxt pblRD ori p of
24.56 SOME pblRD' => SOME pblRD'
24.57 | NONE => refins_PIDE ctxt pblRD ori pts);
24.58
24.59 @@ -315,35 +313,18 @@
24.60 (* TODO rename \<rightarrow> by_oris
24.61 for tactic Refine_Tacitly
24.62 oris are already created wrt. some pbt; ctxt overrides thy in pbt *)
24.63 -(*
24.64 -fun refine_ori oris pblID =
24.65 +fun refine_ori ctxt oris pblID =
24.66 let
24.67 - val opt = app_ptyp (refin ((rev o tl) pblID) oris) pblID (rev pblID);
24.68 + val opt = app_ptyp (refin ctxt ((rev o tl) pblID) oris) pblID (rev pblID);
24.69 in case opt of
24.70 SOME pblRD =>
24.71 let val pblID': Problem.id = rev pblRD
24.72 in if pblID' = pblID then NONE else SOME pblID' end
24.73 | NONE => NONE
24.74 end;
24.75 -*)
24.76 -fun refine_ori_PIDE ctxt oris pblID =
24.77 - let
24.78 - val opt = app_ptyp (refin_PIDE ctxt ((rev o tl) pblID) oris) pblID (rev pblID);
24.79 - in case opt of
24.80 - SOME pblRD =>
24.81 - let val pblID': Problem.id = rev pblRD
24.82 - in if pblID' = pblID then NONE else SOME pblID' end
24.83 - | NONE => NONE
24.84 - end;
24.85 -(*fun refine_ori' oris pI = perhaps (refine_ori oris) pI;*)
24.86 -fun refine_ori'_PIDE ctxt oris pI = perhaps (refine_ori_PIDE ctxt oris) pI;
24.87 +fun refine_ori' ctxt oris pI = perhaps (refine_ori ctxt oris) pI;
24.88
24.89 -(* for math-authoring and test; TODO: needs ctxt for parsing fmz *)
24.90 \<^isac_test>\<open>
24.91 -(*
24.92 -fun refine fmz pblID =
24.93 - app_ptyp (refin' ((rev o tl) pblID) fmz []) pblID (rev pblID);
24.94 -*)
24.95 fun refine_PIDE ctxt fmz pblID =
24.96 app_ptyp (refin'_PIDE ctxt ((rev o tl) pblID) fmz []) pblID (rev pblID);
24.97 \<close>
25.1 --- a/src/Tools/isac/Specify/specification.sml Fri Oct 07 20:46:48 2022 +0200
25.2 +++ b/src/Tools/isac/Specify/specification.sml Sat Oct 08 11:40:48 2022 +0200
25.3 @@ -118,7 +118,7 @@
25.4 Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl, ctxt, ...} => (ospec, hdf', spec, probl, ctxt)
25.5 | _ => raise ERROR "get Pbl: uncovered case get_obj"
25.6 val {prls, where_, ...} =
25.7 - Problem.from_store_PIDE (Ctree.get_ctxt pt pos) (#2 (References.select_input ospec spec))
25.8 + Problem.from_store (Ctree.get_ctxt pt pos) (#2 (References.select_input ospec spec))
25.9 val (_, pre) = Pre_Conds.check prls where_ probl 0
25.10 in
25.11 (is_complete' probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
25.12 @@ -128,7 +128,7 @@
25.13 val (ospec, hdf', spec, meth, ctxt) = case Ctree.get_obj I pt p of
25.14 Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ctxt, ...} => (ospec, hdf', spec, meth, ctxt)
25.15 | _ => raise ERROR "get Met: uncovered case get_obj"
25.16 - val {prls, pre, ...} = MethodC.from_store_PIDE ctxt (#3 (References.select_input ospec spec))
25.17 + val {prls, pre, ...} = MethodC.from_store ctxt (#3 (References.select_input ospec spec))
25.18 val (_, pre) = Pre_Conds.check prls pre meth 0
25.19 in
25.20 (is_complete' meth pre spec, Pos.Met, hdf', meth, pre, spec)
26.1 --- a/src/Tools/isac/Specify/specify-step.sml Fri Oct 07 20:46:48 2022 +0200
26.2 +++ b/src/Tools/isac/Specify/specify-step.sml Sat Oct 08 11:40:48 2022 +0200
26.3 @@ -24,7 +24,7 @@
26.4 ...} = Calc.specify_data (ctree, pos);
26.5 val ctxt = Ctree.get_ctxt ctree pos
26.6 val (dI, _, _) = References.select_input o_refs refs;
26.7 - val {ppc = m_patt, pre, prls, ...} = MethodC.from_store_PIDE ctxt mID
26.8 + val {ppc = m_patt, pre, prls, ...} = MethodC.from_store ctxt mID
26.9 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
26.10 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
26.11 val thy = ThyC.get_theory dI
26.12 @@ -50,7 +50,7 @@
26.13 val pI' = case Ctree.get_obj I pt p of
26.14 Ctree.PblObj {origin = (_, (_, pI', _),_), ...} => pI'
26.15 | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
26.16 - val {ppc, ...} = Problem.from_store_PIDE (Ctree.get_ctxt pt pos) pI'
26.17 + val {ppc, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
26.18 val pbl = I_Model.init ppc
26.19 in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
26.20 | check (Tactic.Refine_Problem pI) (pt, (p, _)) =
26.21 @@ -75,7 +75,7 @@
26.22 | _ => raise ERROR "Specify_Step.check Refine_Tacitly: uncovered case Ctree.get_obj"
26.23 val ctxt = Ctree.get_ctxt pt pos
26.24 in
26.25 - case Refine.refine_ori_PIDE ctxt oris pI of
26.26 + case Refine.refine_ori ctxt oris pI of
26.27 SOME pblID =>
26.28 Applicable.Yes (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, MethodC.id_empty, [(*filled later*)]))
26.29 | NONE => Applicable.No (Tactic.input_to_string (Tactic.Refine_Tacitly pI) ^ " not applicable")
26.30 @@ -93,7 +93,7 @@
26.31 => (oris, dI, pI, dI', pI', itms)
26.32 | _ => raise ERROR "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj"
26.33 val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
26.34 - val {ppc, where_, prls, ...} = Problem.from_store_PIDE (Ctree.get_ctxt pt pos) pID;
26.35 + val {ppc, where_, prls, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pID;
26.36 val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty
26.37 then (false, (I_Model.init ppc, []))
26.38 else M_Match.match_itms_oris thy itms (ppc, where_, prls) oris;
27.1 --- a/src/Tools/isac/Specify/specify.sml Fri Oct 07 20:46:48 2022 +0200
27.2 +++ b/src/Tools/isac/Specify/specify.sml Sat Oct 08 11:40:48 2022 +0200
27.3 @@ -3,8 +3,6 @@
27.4 val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input)
27.5 val do_all: Calc.T -> Calc.T
27.6 val finish_phase: Calc.T -> Calc.T
27.7 - val finish_phase_PIDEnote: Proof.context -> O_Model.T * References.T -> I_Model.T * References.T ->
27.8 - I_Model.T * I_Model.T
27.9
27.10 val item_to_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T ->
27.11 (Model_Def.m_field * TermC.as_string) option
27.12 @@ -80,8 +78,8 @@
27.13 val cdI = if dI = ThyC.id_empty then dI' else dI;
27.14 val cpI = if pI = Problem.id_empty then pI' else pI;
27.15 val cmI = if mI = MethodC.id_empty then mI' else mI;
27.16 - val {ppc = pbt, prls, where_, ...} = Problem.from_store_PIDE ctxt cpI;
27.17 - val {ppc = mpc, ...} = MethodC.from_store_PIDE ctxt cmI
27.18 + val {ppc = pbt, prls, where_, ...} = Problem.from_store ctxt cpI;
27.19 + val {ppc = mpc, ...} = MethodC.from_store ctxt cmI
27.20 val (preok, _) = Pre_Conds.check prls where_ pbl 0;
27.21 in
27.22 if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then
27.23 @@ -115,7 +113,7 @@
27.24 fun for_method_PIDE ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =
27.25 let
27.26 val cmI = if mI = MethodC.id_empty then mI' else mI;
27.27 - val {ppc = mpc, prls, pre, ...} = MethodC.from_store_PIDE ctxt cmI; (*..MethodC ?*)
27.28 + val {ppc = mpc, prls, pre, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
27.29 val (preok, _) = Pre_Conds.check prls pre pbl 0;
27.30 in
27.31 (case find_first (I_Model.is_error o #5) met of
27.32 @@ -164,10 +162,10 @@
27.33 val (i_model, m_patt) =
27.34 if p_ = Pos.Met then
27.35 (met,
27.36 - (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store_PIDE ctxt |> #ppc)
27.37 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #ppc)
27.38 else
27.39 (pbl,
27.40 - (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store_PIDE ctxt |> #ppc)
27.41 + (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #ppc)
27.42 in
27.43 case I_Model.check_single ctxt m_field oris i_model m_patt ct of
27.44 I_Model.Add i_single => (*..union old input *)
27.45 @@ -194,23 +192,13 @@
27.46 | _ => raise ERROR "finish_phase: unvered case get_obj"
27.47 val (_, pI, mI) = References.select_input ospec spec
27.48 val ctxt = Ctree.get_ctxt pt pos
27.49 - val mpc = (#ppc o MethodC.from_store_PIDE ctxt) mI
27.50 - val ppc = (#ppc o Problem.from_store_PIDE ctxt) pI
27.51 + val mpc = (#ppc o MethodC.from_store ctxt) mI
27.52 + val ppc = (#ppc o Problem.from_store ctxt) pI
27.53 val (pits, mits) = I_Model.complete_method (oris, mpc, ppc, probl)
27.54 val pt = Ctree.update_pblppc pt p pits
27.55 val pt = Ctree.update_metppc pt p mits
27.56 in (pt, (p, Pos.Met)) end
27.57
27.58 -(*an unclarified remainder of the transition from sessions to PIDE with ctxt*)
27.59 -fun finish_phase_PIDEnote ctxt (o_model, o_refs) (problem_model, refs) =
27.60 - let
27.61 - val (_, pI, mI) = References.select_input o_refs refs
27.62 - val method_pattern = (#ppc o MethodC.from_store_PIDE ctxt) mI
27.63 - val problem_pattern = (#ppc o Problem.from_store_PIDE ctxt) pI
27.64 - val (problem_model, method_model) =
27.65 - I_Model.complete_method (o_model, method_pattern, problem_pattern, problem_model)
27.66 - in (problem_model, method_model) end
27.67 -
27.68 (* do all specification in one single step:
27.69 complete calc-head for autocalc (sub-)pbl from oris (+ met from fmz);
27.70 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem
27.71 @@ -222,7 +210,7 @@
27.72 => (pors, dI, pI, mI)
27.73 | _ => raise ERROR "do_all: uncovered case get_obj"
27.74 val ctxt = Ctree.get_ctxt pt pos
27.75 - val {ppc, ...} = MethodC.from_store_PIDE ctxt mI
27.76 + val {ppc, ...} = MethodC.from_store ctxt mI
27.77 val (_, vals) = O_Model.values' pors
27.78 val ctxt = ContextC.initialise dI vals
27.79 val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),
28.1 --- a/src/Tools/isac/Specify/step-specify.sml Fri Oct 07 20:46:48 2022 +0200
28.2 +++ b/src/Tools/isac/Specify/step-specify.sml Sat Oct 08 11:40:48 2022 +0200
28.3 @@ -9,7 +9,7 @@
28.4 val by_tactic_input: Tactic.input -> Calc.T -> string * Calc.state_post
28.5 val by_tactic: Tactic.T -> Calc.T -> string * Calc.state_post
28.6
28.7 - val initialise_PIDE: Formalise.T ->
28.8 + val initialise: Formalise.T ->
28.9 term * term * References.T * O_Model.T * Proof.context
28.10 val nxt_specify_init_calc: Proof.context -> Formalise.T -> Calc.T * State_Steps.T
28.11 end
28.12 @@ -28,8 +28,8 @@
28.13 PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
28.14 | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
28.15 val (_, pI, mI) = References.select_input ospec spec
28.16 - val mpc = (#ppc o MethodC.from_store_PIDE ctxt) mI (* just for reuse I_Model.complete_method *)
28.17 - val {cas, ppc, ...} = Problem.from_store_PIDE (Ctree.get_ctxt pt pos) pI
28.18 + val mpc = (#ppc o MethodC.from_store ctxt) mI (* just for reuse I_Model.complete_method *)
28.19 + val {cas, ppc, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
28.20 val pbl = I_Model.init ppc (* fill in descriptions *)
28.21 (*----------------if you think, this should be done by the Dialog
28.22 in the java front-end, search there for WN060225-modelProblem----*)
28.23 @@ -52,12 +52,12 @@
28.24 val (oris, dI, ctxt) = case get_obj I pt p of
28.25 (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
28.26 | _ => raise ERROR "by_tactic_input Refine_Tacitly: uncovered case get_obj"
28.27 - val opt = Refine.refine_ori_PIDE ctxt oris pI
28.28 + val opt = Refine.refine_ori ctxt oris pI
28.29 in
28.30 case opt of
28.31 SOME pI' =>
28.32 let
28.33 - val {met, ...} = Problem.from_store_PIDE (Ctree.get_ctxt pt pos) pI'
28.34 + val {met, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
28.35 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
28.36 val mI = if length met = 0 then MethodC.id_empty else hd met
28.37 val (pos, c, _, pt) =
28.38 @@ -93,7 +93,7 @@
28.39 (oris, dI, dI', pI', probl, ctxt)
28.40 | _ => raise ERROR ""
28.41 val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
28.42 - val {ppc,where_,prls,...} = Problem.from_store_PIDE (Ctree.get_ctxt pt pos) pI
28.43 + val {ppc,where_,prls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
28.44 val pbl =
28.45 if pI' = Problem.id_empty andalso pI = Problem.id_empty
28.46 then (false, (I_Model.init ppc, []))
28.47 @@ -148,7 +148,7 @@
28.48 (* called only if no_met is specified *)
28.49 | by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) =
28.50 let
28.51 - val {met, thy,...} = Problem.from_store_PIDE (Ctree.get_ctxt pt pos) pIre
28.52 + val {met, thy,...} = Problem.from_store (Ctree.get_ctxt pt pos) pIre
28.53 val (domID, metID) = (Context.theory_name thy, if length met = 0 then MethodC.id_empty else hd met)
28.54 val ((p,_), _, _, pt) =
28.55 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
28.56 @@ -209,8 +209,8 @@
28.57 | by_tactic _ _ = raise ERROR "Step_Specify.by_tactic uncovered pattern in fun.def"
28.58
28.59 (* create a calc-tree with oris via a cas.refined pbl *)
28.60 -(* initialise_PIDE <-?-> nxt_specify_init_calc *)
28.61 -fun initialise_PIDE (fmz, (dI, pI, mI)) =
28.62 +(* initialise <-?-> nxt_specify_init_calc *)
28.63 +fun initialise (fmz, (dI, pI, mI)) =
28.64 let
28.65 val thy = ThyC.get_theory dI
28.66 val ctxt = Proof_Context.init_global thy
28.67 @@ -218,37 +218,37 @@
28.68 if mI = ["no_met"]
28.69 then
28.70 let
28.71 - val pors = Problem.from_store_PIDE ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
28.72 + val pors = Problem.from_store ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
28.73 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
28.74 - val pI' = Refine.refine_ori'_PIDE pctxt pors pI;
28.75 + val pI' = Refine.refine_ori' pctxt pors pI;
28.76 in (pI', (pors (*refinement over models with diff.precond only*), pctxt),
28.77 - (hd o #met o Problem.from_store_PIDE ctxt) pI')
28.78 + (hd o #met o Problem.from_store ctxt) pI')
28.79 end
28.80 else
28.81 let
28.82 - val pors = Problem.from_store_PIDE ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
28.83 + val pors = Problem.from_store ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
28.84 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
28.85 in (pI, (pors, pctxt), mI) end;
28.86 - val {cas, ppc, thy = thy', ...} = Problem.from_store_PIDE ctxt pI (*take dI from _refined_ pbl*)
28.87 + val {cas, ppc, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*)
28.88 val dI = Context.theory_name (ThyC.sub_common (thy, thy'))
28.89 val hdl = case cas of
28.90 - NONE => Auto_Prog.pblterm_PIDE dI pI
28.91 + NONE => Auto_Prog.pblterm dI pI
28.92 | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t
28.93 val hdlPIDE = case cas of
28.94 - NONE => Auto_Prog.pblterm_PIDE dI pI
28.95 + NONE => Auto_Prog.pblterm dI pI
28.96 | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t
28.97 in
28.98 (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)
28.99 end;
28.100 -(* nxt_specify_init_calc \<rightarrow> initialise *)
28.101 +(*TODO: HOW RELATES nxt_specify_init_calc \<longleftrightarrow> initialise *)
28.102 fun nxt_specify_init_calc ctxt ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*)
28.103 if pI <> []
28.104 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
28.105 let
28.106 - val {cas, met, ppc, thy, ...} = Problem.from_store_PIDE ctxt pI
28.107 + val {cas, met, ppc, thy, ...} = Problem.from_store ctxt pI
28.108 val dI = if dI = "" then Context.theory_name thy else dI
28.109 val mI = if mI = [] then hd met else mI
28.110 - val hdl = case cas of NONE => Auto_Prog.pblterm_PIDE dI pI | SOME t => t
28.111 + val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
28.112 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
28.113 ([], (dI,pI,mI), hdl, ContextC.empty)
28.114 val pt = update_spec pt [] (dI, pI, mI)
28.115 @@ -259,7 +259,7 @@
28.116 if mI <> []
28.117 then (* from met-browser *)
28.118 let
28.119 - val {ppc, ...} = MethodC.from_store_PIDE ctxt mI
28.120 + val {ppc, ...} = MethodC.from_store ctxt mI
28.121 val dI = if dI = "" then "Isac_Knowledge" else dI
28.122 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
28.123 ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty)
28.124 @@ -274,7 +274,7 @@
28.125 in ((pt, ([], Pbl)), []) end
28.126 | nxt_specify_init_calc _ (fmz, (dI, pI, mI)) =
28.127 let (* both ^^^ ^^^^^^^^^^^^ are either empty or complete *)
28.128 - val (_, hdl, (dI, pI, mI), pors, pctxt) = initialise_PIDE (fmz, (dI, pI, mI))
28.129 + val (_, hdl, (dI, pI, mI), pors, pctxt) = initialise (fmz, (dI, pI, mI))
28.130 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt)
28.131 (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl, pctxt)
28.132 in
29.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri Oct 07 20:46:48 2022 +0200
29.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sat Oct 08 11:40:48 2022 +0200
29.3 @@ -517,7 +517,7 @@
29.4 the original \emph{srls}.\\
29.5
29.6 \begin{verbatim}
29.7 - val {srls,...} = MethodC.from_store_PIDE ctxt ["SignalProcessing",
29.8 + val {srls,...} = MethodC.from_store ctxt ["SignalProcessing",
29.9 "Z_Transform",
29.10 "Inverse"];
29.11 \end{verbatim}
29.12 @@ -978,7 +978,7 @@
29.13 the hierarchy.\<close>
29.14
29.15 ML \<open>
29.16 - MethodC.from_store_PIDE ctxt ["SignalProcessing", "Z_Transform", "Inverse"];
29.17 + MethodC.from_store ctxt ["SignalProcessing", "Z_Transform", "Inverse"];
29.18 \<close>
29.19
29.20 section \<open>Program in TP-based language \label{prog-steps}\<close>
29.21 @@ -1235,7 +1235,7 @@
29.22 ) = O_Model.init thy fmz ((#ppc o Problem.from_store) pI);
29.23
29.24 val Prog sc
29.25 - = (#scr o MethodC.from_store_PIDE ctxt) ["SignalProcessing",
29.26 + = (#scr o MethodC.from_store ctxt) ["SignalProcessing",
29.27 "Z_Transform",
29.28 "Inverse"];
29.29 atomty sc;
29.30 @@ -1311,7 +1311,7 @@
29.31 arguments in the arguments\ldots
29.32 \begin{verbatim}
29.33 val Prog s =
29.34 - (#scr o MethodC.from_store_PIDE ctxt) ["SignalProcessing",
29.35 + (#scr o MethodC.from_store ctxt) ["SignalProcessing",
29.36 "Z_Transform",
29.37 "Inverse"];
29.38 writeln (UnparseC.term s);
29.39 @@ -1595,7 +1595,7 @@
29.40 parse-tree of the program with {\sisac}'s specific debug tools:
29.41 \begin{verbatim}
29.42 val {scr = Prog t,...} =
29.43 - MethodC.from_store_PIDE ctxt ["simplification",
29.44 + MethodC.from_store ctxt ["simplification",
29.45 "of_rationals",
29.46 "to_partial_fraction"];
29.47 atomty_thy @{theory "Inverse_Z_Transform"} t ;
30.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Fri Oct 07 20:46:48 2022 +0200
30.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Sat Oct 08 11:40:48 2022 +0200
30.3 @@ -1002,7 +1002,7 @@
30.4 the original \emph{srls}.\\
30.5
30.6 \begin{verbatim}
30.7 - val {srls,...} = MethodC.from_store_PIDE ctxt ["SignalProcessing",
30.8 + val {srls,...} = MethodC.from_store ctxt ["SignalProcessing",
30.9 "Z_Transform",
30.10 "Inverse"];
30.11 \end{verbatim}
30.12 @@ -2391,7 +2391,7 @@
30.13 arguments in the arguments\ldots
30.14 \begin{verbatim}
30.15 val Prog s =
30.16 - (#scr o MethodC.from_store_PIDE ctxt) ["SignalProcessing",
30.17 + (#scr o MethodC.from_store ctxt) ["SignalProcessing",
30.18 "Z_Transform",
30.19 "Inverse"];
30.20 writeln (UnparseC.term s);
30.21 @@ -2698,7 +2698,7 @@
30.22 parse-tree of the program with {\sisac}'s specific debug tools:
30.23 \begin{verbatim}
30.24 val {scr = Prog t,...} =
30.25 - MethodC.from_store_PIDE ctxt ["simplification",
30.26 + MethodC.from_store ctxt ["simplification",
30.27 "of_rationals",
30.28 "to_partial_fraction"];
30.29 atomty_thy @ { theory } t ;
31.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Fri Oct 07 20:46:48 2022 +0200
31.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Sat Oct 08 11:40:48 2022 +0200
31.3 @@ -30,7 +30,7 @@
31.4 the function 'get_pbt' gets the one we need:
31.5 \<close>
31.6 ML \<open>Test_Tool.show_ptyps ();
31.7 - Problem.from_store_PIDE @{context} ["plus_minus", "polynom", "vereinfachen"];
31.8 + Problem.from_store @{context} ["plus_minus", "polynom", "vereinfachen"];
31.9 \<close>
31.10 text \<open>However, 'get_pbt' shows an internal format; for a human readable format
31.11 see http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index_pbl.html
31.12 @@ -43,7 +43,7 @@
31.13 \<close>
31.14 ML \<open>
31.15 Test_Tool.show_mets ();
31.16 -MethodC.from_store_PIDE @{context} ["simplification", "for_polynomials", "with_minus"];
31.17 +MethodC.from_store @{context} ["simplification", "for_polynomials", "with_minus"];
31.18 \<close>
31.19 text \<open>For a readable format of the method look up the definition in
31.20 $ISABELLE_ISAC/Knowledge/PolyMinus.thy or
32.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Fri Oct 07 20:46:48 2022 +0200
32.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Sat Oct 08 11:40:48 2022 +0200
32.3 @@ -232,7 +232,7 @@
32.4 "~~~~~ fun by_tactic , args:"; val ((Tactic.Check_Postcond' (pI, res)), (sub_ist, sub_ctxt), (pt, pos as (p, _)))
32.5 = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp);
32.6 val parent_pos = par_pblobj pt p
32.7 - val {scr, ...} = MethodC.from_store_PIDE ctxt (get_obj g_metID pt parent_pos);
32.8 + val {scr, ...} = MethodC.from_store ctxt (get_obj g_metID pt parent_pos);
32.9 val prog_res =
32.10 case LI.find_next_step scr (pt, pos) sub_ist sub_ctxt of
32.11 (*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
33.1 --- a/test/Tools/isac/BaseDefinitions/substitution.sml Fri Oct 07 20:46:48 2022 +0200
33.2 +++ b/test/Tools/isac/BaseDefinitions/substitution.sml Sat Oct 08 11:40:48 2022 +0200
33.3 @@ -100,7 +100,7 @@
33.4 "-------- build fun for_bdv --------------------------------------------------";
33.5 Subst.program_to_input: Subst.program -> string list;
33.6
33.7 -val {scr = Prog prog, ...} = MethodC.from_store_PIDE ctxt ["diff", "differentiate_on_R"];
33.8 +val {scr = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"];
33.9 val env = [(TermC.str2term "v_v", TermC.str2term "x")] : Subst.T;
33.10
33.11 "~~~~~ fun for_bdv, args:"; val (prog, env) = (prog, env);
34.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Fri Oct 07 20:46:48 2022 +0200
34.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sat Oct 08 11:40:48 2022 +0200
34.3 @@ -193,7 +193,7 @@
34.4 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
34.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
34.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
34.7 - val (is, sc) = LItool.resume_prog_PIDE (p,p_) pt;
34.8 + val (is, sc) = LItool.resume_prog (p,p_) pt;
34.9 val Safe_Step (istate, _, tac) =
34.10 (*case*) LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
34.11
35.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Fri Oct 07 20:46:48 2022 +0200
35.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Sat Oct 08 11:40:48 2022 +0200
35.3 @@ -47,9 +47,9 @@
35.4 "--------- appendFormula: on Res + equ_nrls ----------------------";
35.5 "--------- appendFormula: on Res + equ_nrls ----------------------";
35.6 "--------- appendFormula: on Res + equ_nrls ----------------------";
35.7 - val Prog sc = (#scr o MethodC.from_store_PIDE ctxt) ["Test", "squ-equ-test-subpbl1"];
35.8 + val Prog sc = (#scr o MethodC.from_store ctxt) ["Test", "squ-equ-test-subpbl1"];
35.9 (writeln o UnparseC.term) sc;
35.10 - val Prog sc = (#scr o MethodC.from_store_PIDE ctxt) ["Test", "solve_linear"];
35.11 + val Prog sc = (#scr o MethodC.from_store ctxt) ["Test", "solve_linear"];
35.12 (writeln o UnparseC.term) sc;
35.13
35.14 States.reset ();
35.15 @@ -986,7 +986,7 @@
35.16 val (res, inf) =
35.17 (TermC.str2term "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))",
35.18 TermC.str2term "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
35.19 -val {errpats, nrls = rls, scr = Prog prog, ...} = MethodC.from_store_PIDE ctxt ["diff", "differentiate_on_R"]
35.20 +val {errpats, nrls = rls, scr = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"]
35.21
35.22 val env = [(TermC.str2term "v_v", TermC.str2term "x")];
35.23 val errpats =
35.24 @@ -1033,16 +1033,16 @@
35.25 (*if*) f_pred = f_in; (*else*)
35.26 val NONE = (*case*) CAS_Cmd.input f_in (*of*);
35.27 (*old* )val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
35.28 - (*old*)val {scr = prog, ...} = MethodC.from_store_PIDE ctxt metID
35.29 + (*old*)val {scr = prog, ...} = MethodC.from_store ctxt metID
35.30 (*old*)val istate = get_istate_LI pt pos
35.31 (*old*)val ctxt = get_ctxt pt pos
35.32 ( *old*)
35.33 val LI.Not_Derivable =
35.34 (*case*) LI.locate_input_term (pt, pos) f_in (*of*);
35.35 val pp = Ctree.par_pblobj pt p
35.36 - val (errpats, nrls, prog) = case MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
35.37 + val (errpats, nrls, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
35.38 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
35.39 - | _ => error "inform: uncovered case of MethodC.from_store_PIDE ctxt"
35.40 + | _ => error "inform: uncovered case of MethodC.from_store ctxt"
35.41 ;
35.42 (*+*)if Error_Pattern.s_to_string errpats = "[(\"chain-rule-diff-both\",\n[\"d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)\", \"d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)\", \"d_d ?bdv (LogExp.ln ?u) = 1 / ?u\", \"d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u\"],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\", \"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1) * d_d ?bdv ?u\", \"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\", \"d_d ?bdv (exp ?u) = exp ?u * d_d ?x ?u\"]]"
35.43 (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3";
35.44 @@ -1085,9 +1085,9 @@
35.45 "~~~~~ fun find_fill_patterns , args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
35.46 val f_curr = Ctree.get_curr_formula (pt, pos);
35.47 val pp = Ctree.par_pblobj pt p
35.48 - val (errpats, prog) = case MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
35.49 + val (errpats, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
35.50 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
35.51 - | _ => error "find_fill_patterns: uncovered case of MethodC.from_store_PIDE ctxt"
35.52 + | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt"
35.53 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
35.54 val subst = Subst.for_bdv prog env
35.55 val errpatthms = errpats
36.1 --- a/test/Tools/isac/Interpret/li-tool.sml Fri Oct 07 20:46:48 2022 +0200
36.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Sat Oct 08 11:40:48 2022 +0200
36.3 @@ -41,7 +41,7 @@
36.4 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = (m, ptp);
36.5 "~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,ctxt), pos as (p,_))
36.6 = (m, pos);
36.7 -val {srls, ...} = MethodC.from_store_PIDE ctxt mI;
36.8 +val {srls, ...} = MethodC.from_store ctxt mI;
36.9 val PblObj {meth=itms, ...} = get_obj I pt p;
36.10 val thy' = get_obj g_domID pt p;
36.11 val thy = ThyC.get_theory thy';
36.12 @@ -138,7 +138,7 @@
36.13 if metID = MethodC.id_empty
36.14 then (thd3 o snd3) (get_obj g_origin pt pp)
36.15 else metID
36.16 - val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = MethodC.from_store_PIDE ctxt metID'
36.17 + val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = MethodC.from_store ctxt metID'
36.18 val Pstate ist = get_istate_LI pt (p,p_)
36.19 val ctxt = get_ctxt pt (p, p_)
36.20 val alltacs = (*we expect at least 1 stac in a script*)
37.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Fri Oct 07 20:46:48 2022 +0200
37.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Sat Oct 08 11:40:48 2022 +0200
37.3 @@ -43,7 +43,7 @@
37.4
37.5 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
37.6 = (m, (pt, pos));
37.7 - val {srls, ...} = MethodC.from_store_PIDE ctxt mI;
37.8 + val {srls, ...} = MethodC.from_store ctxt mI;
37.9 val itms = case get_obj I pt p of
37.10 PblObj {meth=itms, ...} => itms
37.11 | _ => error "solve Apply_Method: uncovered case get_obj"
37.12 @@ -120,7 +120,7 @@
37.13 (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
37.14 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
37.15 val thy' = get_obj g_domID pt (par_pblobj pt p);
37.16 - val (is, sc) = LItool.resume_prog_PIDE (p,p_) pt;
37.17 + val (is, sc) = LItool.resume_prog (p,p_) pt;
37.18
37.19 locate_input_tactic sc (pt, po) (fst is) (snd is) m;
37.20 "~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
37.21 @@ -285,7 +285,7 @@
37.22 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
37.23 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
37.24 val thy' = get_obj g_domID pt (par_pblobj pt p);
37.25 - val (is, sc) = LItool.resume_prog_PIDE (p,p_) pt;
37.26 + val (is, sc) = LItool.resume_prog (p,p_) pt;
37.27
37.28 (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
37.29 "~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
37.30 @@ -382,7 +382,7 @@
37.31 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
37.32 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
37.33 val thy' = get_obj g_domID pt (par_pblobj pt p);
37.34 - val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
37.35 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
37.36
37.37 val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) =
37.38 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
37.39 @@ -433,7 +433,7 @@
37.40 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
37.41 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
37.42 val thy' = get_obj g_domID pt (par_pblobj pt p);
37.43 - val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
37.44 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
37.45
37.46 (** )val End_Program (ist, tac) =
37.47 ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
37.48 @@ -458,7 +458,7 @@
37.49
37.50 Term_Val prog_result (*return from scan_to_tactic*);
37.51 "~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result);
37.52 - val (true, p' as [], Rule_Set.Empty, _) = (*case*) parent_node_PIDE pt pos (*of*);
37.53 + val (true, p' as [], Rule_Set.Empty, _) = (*case*) parent_node pt pos (*of*);
37.54 val (_, pblID, _) = get_obj g_spec pt p';
37.55
37.56 End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))
38.1 --- a/test/Tools/isac/Knowledge/biegelinie-2.sml Fri Oct 07 20:46:48 2022 +0200
38.2 +++ b/test/Tools/isac/Knowledge/biegelinie-2.sml Sat Oct 08 11:40:48 2022 +0200
38.3 @@ -132,7 +132,7 @@
38.4 val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
38.5 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
38.6 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
38.7 - val {ppc, ...} = MethodC.from_store_PIDE ctxt mI;
38.8 + val {ppc, ...} = MethodC.from_store ctxt mI;
38.9 val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
38.10 val srls = LItool.get_simplifier (pt, pos);
38.11
38.12 @@ -172,7 +172,7 @@
38.13 NONE => raise ERROR "arguments_from_model ..."(*error_msg_2 d itms*)
38.14 | SOME (_, _, _, _, itm_) => I_Model.penvval_in itm_
38.15
38.16 - val pats = (#ppc o MethodC.from_store_PIDE ctxt) mI;
38.17 + val pats = (#ppc o MethodC.from_store ctxt) mI;
38.18 (*[("#Given", (Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), Free ("q__q", "real"))),
38.19 ("#Given", (Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), Free ("v_v", "real"))),
38.20 ("#Given", (Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), Free ("id_fun", "real \<Rightarrow> real"))),
39.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Fri Oct 07 20:46:48 2022 +0200
39.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Sat Oct 08 11:40:48 2022 +0200
39.3 @@ -20,7 +20,7 @@
39.4 "----------- retrieve errpats ------------------------------------";
39.5 "----------- retrieve errpats ------------------------------------";
39.6 "----------- retrieve errpats ------------------------------------";
39.7 -val {errpats, nrls, scr = Prog prog, ...} = MethodC.from_store_PIDE ctxt ["diff", "differentiate_on_R"];
39.8 +val {errpats, nrls, scr = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"];
39.9 case errpats of [("chain-rule-diff-both", _, _)] => ()
39.10 | _ => error "errpats chain-rule-diff-both changed"
39.11
40.1 --- a/test/Tools/isac/Knowledge/diff.sml Fri Oct 07 20:46:48 2022 +0200
40.2 +++ b/test/Tools/isac/Knowledge/diff.sml Sat Oct 08 11:40:48 2022 +0200
40.3 @@ -41,8 +41,8 @@
40.4 "differentiateFor x", "derivative f_f'"];
40.5 val chkorg = map (TermC.parseNEW' ctxt) org;
40.6
40.7 -Problem.from_store_PIDE @{context} ["derivative_of", "function"];
40.8 -MethodC.from_store_PIDE ctxt ["diff", "differentiate_on_R"];
40.9 +Problem.from_store @{context} ["derivative_of", "function"];
40.10 +MethodC.from_store ctxt ["diff", "differentiate_on_R"];
40.11
40.12 "----------- for correction of diff_const ---------------";
40.13 "----------- for correction of diff_const ---------------";
41.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Fri Oct 07 20:46:48 2022 +0200
41.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Sat Oct 08 11:40:48 2022 +0200
41.3 @@ -297,7 +297,7 @@
41.4 "~~~~~ fun Refine.refine , args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);
41.5 "~~~~~ fun refin' , args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
41.6 ((rev o tl) pblID, fmz, [(*match list*)],
41.7 - ((Store.Node ("LINEAR", [Problem.from_store_PIDE ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));
41.8 + ((Store.Node ("LINEAR", [Problem.from_store ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));
41.9 val {thy, ppc, where_, prls, ...} = py ;
41.10 "~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, ppc);
41.11 val ctxt = Proof_Context.init_global thy;
42.1 --- a/test/Tools/isac/Knowledge/eqsystem-1a.sml Fri Oct 07 20:46:48 2022 +0200
42.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1a.sml Sat Oct 08 11:40:48 2022 +0200
42.3 @@ -84,7 +84,7 @@
42.4 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
42.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
42.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
42.7 - val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
42.8 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
42.9
42.10 val Next_Step (Pstate {act_arg = t, ...}, _, _) = (*case*)
42.11 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
42.12 @@ -189,19 +189,19 @@
42.13 val ctxt = Proof_Context.init_global thy (*BETTER USE user_ctxt ?*)
42.14 val ags = TermC.isalist2list ags';
42.15 (*if*) mI = ["no_met"] (*then*);
42.16 - val pors = (M_Match.arguments thy ((#ppc o (Problem.from_store_PIDE ctxt)) pI) ags): O_Model.T
42.17 + val pors = (M_Match.arguments thy ((#ppc o (Problem.from_store ctxt)) pI) ags): O_Model.T
42.18 val pI' =
42.19 - Refine.refine_ori'_PIDE ctxt pors pI;
42.20 + Refine.refine_ori' ctxt pors pI;
42.21 val return = (pI', pors (* refinement over models with diff.prec only *),
42.22 - (hd o #met o Problem.from_store_PIDE ctxt) pI');
42.23 + (hd o #met o Problem.from_store ctxt) pI');
42.24 (*-------------^^ THIS CAUSED THE ERROR Empty*)
42.25
42.26 (*+*)val ["LINEAR", "system"] = pI;
42.27 (*+*)fun app_ptyp x = Store.apply (get_pbls ()) x; (*redefine locally hidden*)
42.28
42.29 -"~~~~~ fun refine_ori'_PIDE , args:"; val (oris, pblID) = (pors, pI);
42.30 +"~~~~~ fun refine_ori' , args:"; val (oris, pblID) = (pors, pI);
42.31 val SOME ["system", "LINEAR", "2x2", "triangular"] =
42.32 - app_ptyp (Refine.refin_PIDE ctxt ((rev o tl) pblID) oris) pblID (rev pblID);
42.33 + app_ptyp (Refine.refin ctxt ((rev o tl) pblID) oris) pblID (rev pblID);
42.34
42.35 "~~~~~ fun app_ptyp , args:"; val () = (); (*considered too expensive for testing*)
42.36 (*+*)val fmz = ["equalities [c_2 = (0::real), L * c + c_2 = q_0 * L \<up> 2 / 2]",
43.1 --- a/test/Tools/isac/Knowledge/integrate.sml Fri Oct 07 20:46:48 2022 +0200
43.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Sat Oct 08 11:40:48 2022 +0200
43.3 @@ -350,10 +350,10 @@
43.4 | _ => error "integrate.sml: Integrate.antiDerivativeName";
43.5
43.6 "----- compare 'Find's from problem, script, formalization -------";
43.7 -val {ppc,...} = Problem.from_store_PIDE @{context} ["named", "integrate", "function"];
43.8 +val {ppc,...} = Problem.from_store @{context} ["named", "integrate", "function"];
43.9 val ("#Find", (Const (\<^const_name>\<open>antiDerivativeName\<close>, _),
43.10 F1_ as Free ("F_F", F1_type))) = last_elem ppc;
43.11 -val {scr = Prog sc,... } = MethodC.from_store_PIDE ctxt ["diff", "integration", "named"];
43.12 +val {scr = Prog sc,... } = MethodC.from_store ctxt ["diff", "integration", "named"];
43.13 val [_,_, F2_] = formal_args sc;
43.14 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
43.15
43.16 @@ -364,7 +364,7 @@
43.17 else error "integrate.sml: unequal types in find's";
43.18
43.19 Test_Tool.show_ptyps();
43.20 -val pbl = Problem.from_store_PIDE @{context} ["integrate", "function"];
43.21 +val pbl = Problem.from_store @{context} ["integrate", "function"];
43.22 case #cas pbl of SOME (Const (\<^const_name>\<open>Integrate\<close>, _) $ _) => ()
43.23 | _ => error "integrate.sml: Integrate.Integrate ???";
43.24
44.1 --- a/test/Tools/isac/Knowledge/integrate.thy Fri Oct 07 20:46:48 2022 +0200
44.2 +++ b/test/Tools/isac/Knowledge/integrate.thy Sat Oct 08 11:40:48 2022 +0200
44.3 @@ -15,7 +15,7 @@
44.4 (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'') #>
44.5 (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'')) (f_f::real))"
44.6 setup \<open>KEStore_Elems.add_mets @{context}
44.7 - [MethodC.prep_input_PIDE @{theory "Isac_Knowledge"} "met_testint" [] MethodC.id_empty
44.8 + [MethodC.prep_input @{theory "Isac_Knowledge"} "met_testint" [] MethodC.id_empty
44.9 (["diff", "integration", "test"],
44.10 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find", ["antiDerivative F_F"])],
44.11 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
45.1 --- a/test/Tools/isac/Knowledge/inverse_z_transform.sml Fri Oct 07 20:46:48 2022 +0200
45.2 +++ b/test/Tools/isac/Knowledge/inverse_z_transform.sml Sat Oct 08 11:40:48 2022 +0200
45.3 @@ -16,7 +16,7 @@
45.4 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
45.5 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
45.6 Problem.from_store ["Inverse", "Z_Transform", "SignalProcessing"];
45.7 -MethodC.from_store_PIDE ctxt ["SignalProcessing", "Z_Transform", "Inverse"];
45.8 +MethodC.from_store ctxt ["SignalProcessing", "Z_Transform", "Inverse"];
45.9
45.10 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
45.11 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
46.1 --- a/test/Tools/isac/Knowledge/poly-2.sml Fri Oct 07 20:46:48 2022 +0200
46.2 +++ b/test/Tools/isac/Knowledge/poly-2.sml Sat Oct 08 11:40:48 2022 +0200
46.3 @@ -597,7 +597,7 @@
46.4
46.5 "----- 1 ---";
46.6 (*default_print_depth 7;*)
46.7 -val pbt = Problem.from_store_PIDE @{context} ["polynomial", "simplification"];
46.8 +val pbt = Problem.from_store @{context} ["polynomial", "simplification"];
46.9 (*default_print_depth 3;*)
46.10 (*if there is ...
46.11 > val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
46.12 @@ -609,7 +609,7 @@
46.13
46.14 "-----3 ---";
46.15 (*default_print_depth 7;*)
46.16 -val prls = (#prls o Problem.from_store_PIDE @{context}) ["polynomial", "simplification"];
46.17 +val prls = (#prls o Problem.from_store @{context}) ["polynomial", "simplification"];
46.18 (*default_print_depth 3;*)
46.19 val t = TermC.str2term "((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)) is_polyexp";
46.20 val SOME (t',_) = rewrite_set_ thy false prls t;
47.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Fri Oct 07 20:46:48 2022 +0200
47.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Sat Oct 08 11:40:48 2022 +0200
47.3 @@ -109,7 +109,7 @@
47.4 "----------- test matching problems --------------------------0---";
47.5 "----------- test matching problems --------------------------0---";
47.6 val fmz = ["equality (-8 - 2*x + x \<up> 2 = 0)", "solveFor x", "solutions L"];
47.7 -if M_Match.match_pbl fmz (Problem.from_store_PIDE @{context} ["expanded", "univariate", "equation"]) =
47.8 +if M_Match.match_pbl fmz (Problem.from_store @{context} ["expanded", "univariate", "equation"]) =
47.9 M_Match.Matches' {Find = [Correct "solutions L"],
47.10 With = [],
47.11 Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
47.12 @@ -118,7 +118,7 @@
47.13 Relate = []}
47.14 then () else error "M_Match.match_pbl [expanded,univariate,equation]";
47.15
47.16 -if M_Match.match_pbl fmz (Problem.from_store_PIDE @{context} ["degree_2", "expanded", "univariate", "equation"]) =
47.17 +if M_Match.match_pbl fmz (Problem.from_store @{context} ["degree_2", "expanded", "univariate", "equation"]) =
47.18 M_Match.Matches' {Find = [Correct "solutions L"],
47.19 With = [],
47.20 Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"],
48.1 --- a/test/Tools/isac/Knowledge/rateq.sml Fri Oct 07 20:46:48 2022 +0200
48.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Sat Oct 08 11:40:48 2022 +0200
48.3 @@ -41,11 +41,11 @@
48.4 if result <> "True" then error "rateq.sml: new behaviour 4:" else ();
48.5
48.6 val result = M_Match.match_pbl ["equality (x=(1::real))", "solveFor x", "solutions L"]
48.7 - (Problem.from_store_PIDE @{context} ["rational", "univariate", "equation"]);
48.8 + (Problem.from_store @{context} ["rational", "univariate", "equation"]);
48.9 case result of M_Match.NoMatch' _ => () | _ => error "rateq.sml: new behaviour: 5";
48.10
48.11 val result = M_Match.match_pbl ["equality (3 + x \<up> 2 + 1/(x \<up> 2+3)=1)", "solveFor x", "solutions L"]
48.12 - (Problem.from_store_PIDE @{context} ["rational", "univariate", "equation"]);
48.13 + (Problem.from_store @{context} ["rational", "univariate", "equation"]);
48.14 case result of M_Match.Matches' _ => () | _ => error "rateq.sml: new behaviour: 6";
48.15
48.16 "------------ solve (1/x = 5, x) by me ---------------------------";
48.17 @@ -105,7 +105,7 @@
48.18 member op = [Pbl,Met] p_; (*= false*)
48.19 "~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
48.20 val thy' = get_obj g_domID pt (par_pblobj pt p);
48.21 -val (is, sc) = resume_prog_PIDE (p,p_) pt; (*is: which ctxt?*)
48.22 +val (is, sc) = resume_prog (p,p_) pt; (*is: which ctxt?*)
48.23 "~~~~~ fun find_next_step, args:"; val () = ();
48.24 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
48.25 "~~~~~ fun go_scan_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
48.26 @@ -141,7 +141,7 @@
48.27 val thy' = (get_obj g_domID pt pp):theory';
48.28 val thy = ThyC.get_theory thy'
48.29 val metID = (get_obj g_metID pt pp)
48.30 - val {crls,...} = MethodC.from_store_PIDE ctxt metID
48.31 + val {crls,...} = MethodC.from_store ctxt metID
48.32 val (f,asm) = case p_ of Frm => (get_obj g_form pt p , [])
48.33 | Res => get_obj g_result pt p;
48.34 UnparseC.term f = "[x = 1 / 5]"; (*the current formula*)
49.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Fri Oct 07 20:46:48 2022 +0200
49.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Sat Oct 08 11:40:48 2022 +0200
49.3 @@ -548,7 +548,7 @@
49.4 val (dI',pI',mI') =
49.5 ("Test",["sqroot-test", "univariate", "equation", "test"],
49.6 ["Test", "square_equation2"]);
49.7 -val Prog sc = (#scr o MethodC.from_store_PIDE ctxt) ["Test", "square_equation2"];
49.8 +val Prog sc = (#scr o MethodC.from_store ctxt) ["Test", "square_equation2"];
49.9 (writeln o UnparseC.term) sc;
49.10
49.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
49.12 @@ -614,7 +614,7 @@
49.13
49.14
49.15
49.16 -val Prog s = (#scr o MethodC.from_store_PIDE ctxt) ["Test", "square_equation"];
49.17 +val Prog s = (#scr o MethodC.from_store ctxt) ["Test", "square_equation"];
49.18 atomt s;
49.19
49.20
49.21 @@ -685,7 +685,7 @@
49.22 val (dI',pI',mI') =
49.23 ("Test",["squareroot", "univariate", "equation", "test"],
49.24 ["Test", "square_equation"]);
49.25 - val Prog sc = (#scr o MethodC.from_store_PIDE ctxt) ["Test", "square_equation"];
49.26 + val Prog sc = (#scr o MethodC.from_store ctxt) ["Test", "square_equation"];
49.27 (writeln o UnparseC.term) sc;
49.28
49.29 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
50.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Fri Oct 07 20:46:48 2022 +0200
50.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Sat Oct 08 11:40:48 2022 +0200
50.3 @@ -341,7 +341,7 @@
50.4 val thy' = get_obj g_domID pt (par_pblobj pt p);
50.5
50.6 val (_, (ist, ctxt), sc) =
50.7 - LItool.resume_prog_PIDE (p,p_) pt;
50.8 + LItool.resume_prog (p,p_) pt;
50.9 "~~~~~ fun resume_prog , args:"; val (thy, (p, p_), pt) = (thy', (p,p_), pt);
50.10 (*if*) Pos.on_specification (p, p_) (*else*);
50.11 val (pbl, p', rls') = parent_node pt pos
51.1 --- a/test/Tools/isac/Knowledge/simplify.sml Fri Oct 07 20:46:48 2022 +0200
51.2 +++ b/test/Tools/isac/Knowledge/simplify.sml Sat Oct 08 11:40:48 2022 +0200
51.3 @@ -110,7 +110,7 @@
51.4 "~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
51.5 (oris, (o_refs, refs), (pbl, met));
51.6 val cmI = if mI = MethodC.id_empty then mI' else mI;
51.7 - val {ppc = mpc, prls, pre, ...} = MethodC.from_store_PIDE ctxt cmI; (*..MethodC ?*)
51.8 + val {ppc = mpc, prls, pre, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
51.9
51.10 (** ) val (preok as false, _) = Pre_Conds.check prls pre pbl 0; ( *isa*)
51.11 (**) val (preok as true, _) = Pre_Conds.check prls pre pbl 0; (*isa2*)
52.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Fri Oct 07 20:46:48 2022 +0200
52.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Sat Oct 08 11:40:48 2022 +0200
52.3 @@ -169,7 +169,7 @@
52.4 "----------- fun upds_envv ---------------------------------------------------------------------";
52.5 (* eval test-maximum.sml until Specify_Method ...
52.6 val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt [];
52.7 - val met = (#ppc o MethodC.from_store_PIDE ctxt) mI;
52.8 + val met = (#ppc o MethodC.from_store ctxt) mI;
52.9
52.10 val envv = [];
52.11 val eargs = flat eargs;
53.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Fri Oct 07 20:46:48 2022 +0200
53.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Sat Oct 08 11:40:48 2022 +0200
53.3 @@ -86,7 +86,7 @@
53.4 "~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
53.5 MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*false*)
53.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
53.7 -val ((ist, ctxt), sc) = resume_prog_PIDE (p,p_) pt;
53.8 +val ((ist, ctxt), sc) = resume_prog (p,p_) pt;
53.9
53.10 val Next_Step (istate, ctxt, tac) = LI.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)
53.11 case tac of Or_to_List' _ => ()
53.12 @@ -117,19 +117,19 @@
53.13 Step_Specify.nxt_specify_init_calc ctxt (fmz, sp);
53.14 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
53.15 (*val (_, hdl, (dI, pI, mI), pors, pctxt) =*)
53.16 - initialise_PIDE (fmz, (dI, pI, mI));
53.17 -"~~~~~ fun initialise_PIDE , args:"; val (fmz, (dI, pI, mI)) = (fmz, (dI, pI, mI));
53.18 + initialise (fmz, (dI, pI, mI));
53.19 +"~~~~~ fun initialise , args:"; val (fmz, (dI, pI, mI)) = (fmz, (dI, pI, mI));
53.20 val thy = ThyC.get_theory dI
53.21 val ctxt = Proof_Context.init_global thy;
53.22 (*if*) mI = ["no_met"](*else*);
53.23 - val pors = Problem.from_store_PIDE ctxt pI |> #ppc |> O_Model.init thy fmz;
53.24 + val pors = Problem.from_store ctxt pI |> #ppc |> O_Model.init thy fmz;
53.25 val pctxt = ContextC.initialise' thy fmz;
53.26 - val {cas, ppc, thy=thy',...} = Problem.from_store_PIDE ctxt pI; (*take dI from _refined_ pbl*)
53.27 + val {cas, ppc, thy=thy',...} = Problem.from_store ctxt pI; (*take dI from _refined_ pbl*)
53.28 "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
53.29 val dI = Context.theory_name (ThyC.parent_of thy thy');
53.30 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
53.31 cas = NONE; (*true*)
53.32 - val hdl = pblterm_PIDE dI pI;
53.33 + val hdl = pblterm dI pI;
53.34 val (pt, _) = cappend_problem e_ctree [] (Istate.empty, pctxt) (fmz, (dI, pI, mI))
53.35 (pors, (dI, pI, mI), hdl, ContextC.empty)
53.36 ;
53.37 @@ -198,7 +198,7 @@
53.38 "~~~~~ fun do_next , args:"; val ((ptp as (pt, pos as (p,p_)))) = (ptp);
53.39 MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;
53.40 val thy' = get_obj g_domID pt (par_pblobj pt p);
53.41 - val ((ist, ctxt), sc) = resume_prog_PIDE (p,p_) pt;
53.42 + val ((ist, ctxt), sc) = resume_prog (p,p_) pt;
53.43 val Next_Step (is, ctxt, tac_) = LI.find_next_step sc (pt,pos) ist ctxt;
53.44 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
53.45
53.46 @@ -322,7 +322,7 @@
53.47 Frm => get_obj g_form pt p
53.48 | Res => (fst o (get_obj g_result pt)) p
53.49 | _ => TermC.empty (*on PblObj is fo <> ifo*);
53.50 - val {nrls, ...} = MethodC.from_store_PIDE ctxt (get_obj g_metID pt (par_pblobj pt p))
53.51 + val {nrls, ...} = MethodC.from_store ctxt (get_obj g_metID pt (par_pblobj pt p))
53.52 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls;
53.53 (*val (found, der) = *)Derive.steps ctxt rew_ord erls rules fo ifo; (*<---------------*)
53.54 "~~~~~ fun concat_deriv, args:"; val (rew_ord, erls, rules, fo, ifo) =
54.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Fri Oct 07 20:46:48 2022 +0200
54.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Sat Oct 08 11:40:48 2022 +0200
54.3 @@ -14,7 +14,7 @@
54.4
54.5 Step_Specify.nxt_specify_init_calc ctxt (fmz, sp);
54.6 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
54.7 - val (_, hdl, (dI, pI, mI), pors, pctxt) = initialise_PIDE (fmz, (dI, pI, mI))
54.8 + val (_, hdl, (dI, pI, mI), pors, pctxt) = Step_Specify.initialise (fmz, (dI, pI, mI))
54.9 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt)
54.10 (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl, pctxt)
54.11 ;
54.12 @@ -42,7 +42,7 @@
54.13 "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
54.14 val thy = ThyC.get_theory dI;
54.15 (*if*) mI = ["no_met"] = false (*else*);
54.16 -val xxx = Problem.from_store_PIDE ctxt pI
54.17 +val xxx = Problem.from_store ctxt pI
54.18 val yyy = #ppc xxx
54.19 val oris = O_Model.init thy fmz yyy
54.20 ;
55.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Fri Oct 07 20:46:48 2022 +0200
55.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Sat Oct 08 11:40:48 2022 +0200
55.3 @@ -66,7 +66,7 @@
55.4 val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
55.5 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
55.6 | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj"
55.7 - val {ppc, ...} = MethodC.from_store_PIDE ctxt mI;
55.8 + val {ppc, ...} = MethodC.from_store ctxt mI;
55.9 val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
55.10 val srls = LItool.get_simplifier (pt, pos)
55.11 val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
56.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Fri Oct 07 20:46:48 2022 +0200
56.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Sat Oct 08 11:40:48 2022 +0200
56.3 @@ -38,7 +38,7 @@
56.4 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
56.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (* = else*);
56.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
56.7 - val (is, sc) = LItool.resume_prog_PIDE (p,p_) pt;
56.8 + val (is, sc) = LItool.resume_prog (p,p_) pt;
56.9
56.10 val Safe_Step (_, _, Rewrite_Set' (_, _, Rule_Set.Repeat {id = "norm_equation", ...}, _, _)) = (*case*)
56.11 locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
56.12 @@ -94,7 +94,7 @@
56.13 MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;
56.14 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p)(*else*);
56.15 val thy' = get_obj g_domID pt (par_pblobj pt p);
56.16 - val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
56.17 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
56.18
56.19 val Next_Step (_, _, _) =
56.20 (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
56.21 @@ -146,7 +146,7 @@
56.22 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
56.23 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
56.24 val thy' = get_obj g_domID pt (par_pblobj pt p);
56.25 - val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
56.26 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
56.27
56.28 val Next_Step (_, _, _) =
56.29 (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
56.30 @@ -218,11 +218,11 @@
56.31 val ags = TermC.isalist2list ags';
56.32 (*if*) mI = ["no_met"] (*else*);
56.33 val (pI, pors, mI) =
56.34 - (pI, (M_Match.arguments thy ((#ppc o (Problem.from_store_PIDE ctxt)) pI) ags)
56.35 + (pI, (M_Match.arguments thy ((#ppc o (Problem.from_store ctxt)) pI) ags)
56.36 handle ERROR "actual args do not match formal args"
56.37 - => (M_Match.arguments_msg_PIDE ctxt pI stac ags(*raise exn*); []), mI)
56.38 + => (M_Match.arguments_msg ctxt pI stac ags(*raise exn*); []), mI)
56.39 val (fmz_, vals) = O_Model.values' pors;
56.40 - val {cas,ppc,thy,...} = Problem.from_store_PIDE ctxt pI
56.41 + val {cas,ppc,thy,...} = Problem.from_store ctxt pI
56.42 val dI = Context.theory_name thy (*.take dI from _refined_ pbl.*)
56.43 val dI = Context.theory_name (ThyC.sub_common (ThyC.get_theory dI, rootthy pt));
56.44 val ctxt = ContextC.initialise dI (map TermC.vars vals |> flat |> distinct op =);
57.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Fri Oct 07 20:46:48 2022 +0200
57.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Sat Oct 08 11:40:48 2022 +0200
57.3 @@ -36,7 +36,7 @@
57.4 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt ptp;
57.5 "~~~~~ fun begin_end_prog , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (ist, ctxt), (pt, pos as (p, _)))
57.6 = ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, ptp);
57.7 - val {ppc, ...} = MethodC.from_store_PIDE ctxt mI;
57.8 + val {ppc, ...} = MethodC.from_store ctxt mI;
57.9 val (itms, oris, probl) = case get_obj I pt p of
57.10 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
57.11 | _ => error "begin_end_prog Apply_Method': uncovered case get_obj"
58.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Fri Oct 07 20:46:48 2022 +0200
58.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Sat Oct 08 11:40:48 2022 +0200
58.3 @@ -39,7 +39,7 @@
58.4 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, p));
58.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*false*);
58.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
58.7 - val (is, sc) = resume_prog_PIDE (p,p_) pt;
58.8 + val (is, sc) = resume_prog (p,p_) pt;
58.9
58.10 val Safe_Step (Pstate ist''''', ctxt''''', tac'_''''') =
58.11 locate_input_tactic sc (pt, po) (fst is) (snd is) m;
59.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Fri Oct 07 20:46:48 2022 +0200
59.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Sat Oct 08 11:40:48 2022 +0200
59.3 @@ -65,7 +65,7 @@
59.4 (*+isa==isa2*)if (ContextC.get_assumptions ctxt |> map UnparseC.term) = ["precond_rootmet x"]
59.5 (*+*)then () else error "assumptions 8";
59.6
59.7 - val {ppc, ...} = MethodC.from_store_PIDE ctxt mI;
59.8 + val {ppc, ...} = MethodC.from_store ctxt mI;
59.9 val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
59.10 val srls = LItool.get_simplifier (pt, pos)
59.11 val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
60.1 --- a/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Fri Oct 07 20:46:48 2022 +0200
60.2 +++ b/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Sat Oct 08 11:40:48 2022 +0200
60.3 @@ -54,7 +54,7 @@
60.4 "~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = ((pt, ip));
60.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
60.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
60.7 - val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
60.8 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
60.9
60.10 LI.find_next_step sc (pt, pos) ist ctxt;
60.11 "~~~~~ fun find_next_step , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
61.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Fri Oct 07 20:46:48 2022 +0200
61.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Sat Oct 08 11:40:48 2022 +0200
61.3 @@ -46,7 +46,7 @@
61.4 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
61.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*false*)
61.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
61.7 -val ((ist, ctxt), sc) = resume_prog_PIDE (p,p_) pt;
61.8 +val ((ist, ctxt), sc) = resume_prog (p,p_) pt;
61.9
61.10 val End_Program (ist, tac) =
61.11 (*case*) LI.find_next_step sc (pt,pos) ist ctxt (*of*);
61.12 @@ -56,7 +56,7 @@
61.13 "~~~~~ fun by_tactic , args:"; val ((Check_Postcond' (pI, _)), (sub_ist, sub_ctxt), (pt, pos as (p,_))) =
61.14 (tac, (ist, ctxt), ptp);
61.15 val parent_pos = par_pblobj pt p
61.16 - val {scr, ...} = MethodC.from_store_PIDE ctxt (get_obj g_metID pt parent_pos);
61.17 + val {scr, ...} = MethodC.from_store ctxt (get_obj g_metID pt parent_pos);
61.18 val prog_res =
61.19 case LI.find_next_step scr (pt, pos) sub_ist sub_ctxt of
61.20 (*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
61.21 @@ -82,7 +82,7 @@
61.22 (tac, (ist', ctxt'), (pt, (parent_pos, Res)));
61.23 val (pt,c) = append_result pt p l (scval, asm) Complete;
61.24
61.25 -val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["LINEAR", "uval (is, sc) = resume_prog_PIDE (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *);
61.26 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["LINEAR", "uval (is, sc) = resume_prog (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *);
61.27 case nxt of ( Check_Postcond ["LINEAR", "univariate", "equation", "test"]) => ()
61.28 | _ => error "450-nxt-Check_Postcond broken";
61.29
62.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Fri Oct 07 20:46:48 2022 +0200
62.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Sat Oct 08 11:40:48 2022 +0200
62.3 @@ -55,7 +55,7 @@
62.4 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
62.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
62.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
62.7 - val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
62.8 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
62.9
62.10 val Next_Step (_, _, Check_elementwise' _) =
62.11 (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
63.1 --- a/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml Fri Oct 07 20:46:48 2022 +0200
63.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml Sat Oct 08 11:40:48 2022 +0200
63.3 @@ -100,7 +100,7 @@
63.4 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
63.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
63.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
63.7 - val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
63.8 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
63.9
63.10 (*+*)Istate.string_of ist
63.11 = "Pstate ([\"\n(e_e, - 1 + x = 0)\",\"\n(v_v, x)\",\"\n(L_L, [x = 1])\"], [R,R,D,R,D], empty, NONE, \n[x = 1],"
64.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Fri Oct 07 20:46:48 2022 +0200
64.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Sat Oct 08 11:40:48 2022 +0200
64.3 @@ -51,7 +51,7 @@
64.4 "~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = (pt, input_pos);
64.5 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
64.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
64.7 - val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt;
64.8 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
64.9
64.10 val Next_Step (ist, ctxt, tac) = (*case*) (**..Ctree NOT updated yet**)
64.11 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
64.12 @@ -111,7 +111,7 @@
64.13 (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
64.14 "~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = (([], [], (pt, pos_pred)), tm);
64.15 val fo = Calc.current_formula ptp
64.16 - val {nrls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
64.17 + val {nrls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
64.18 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
64.19 val (found, der) = Derive.steps ctxt rew_ord erls rules fo ifo; (*<---------------*)
64.20 (*if*) found (*then*);
64.21 @@ -129,7 +129,7 @@
64.22 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
64.23 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
64.24 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
64.25 - val {nrls, ...} = MethodC.from_store_PIDE ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
64.26 + val {nrls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
64.27 val (pt, c, pos as (p, _)) =
64.28
64.29 Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res));
65.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Fri Oct 07 20:46:48 2022 +0200
65.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Sat Oct 08 11:40:48 2022 +0200
65.3 @@ -542,7 +542,7 @@
65.4 (*solve*)
65.5 val pp = par_pblobj pt p;
65.6 val metID = get_obj g_metID pt pp;
65.7 - val sc = (#scr o MethodC.from_store_PIDE ctxt) metID;
65.8 + val sc = (#scr o MethodC.from_store ctxt) metID;
65.9 val is = get_istate_LI pt (p,p_);
65.10 val thy' = get_obj g_domID pt pp;
65.11 val thy = ThyC.get_theory thy';
66.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Fri Oct 07 20:46:48 2022 +0200
66.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Sat Oct 08 11:40:48 2022 +0200
66.3 @@ -279,7 +279,7 @@
66.4 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
66.5 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
66.6 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
66.7 -val {scr, ...} = MethodC.from_store_PIDE ctxt ["Test", "sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
66.8 +val {scr, ...} = MethodC.from_store ctxt ["Test", "sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
66.9 case stacpbls sc of
66.10 [Const (\<^const_name>\<open>Rewrite\<close>, _) $ square_equation_left,
66.11 Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ Test_simplify,
67.1 --- a/test/Tools/isac/ProgLang/calculate.thy Fri Oct 07 20:46:48 2022 +0200
67.2 +++ b/test/Tools/isac/ProgLang/calculate.thy Sat Oct 08 11:40:48 2022 +0200
67.3 @@ -18,8 +18,8 @@
67.4 \<close>
67.5
67.6 setup \<open>KEStore_Elems.add_pbls @{context}
67.7 - [Problem.prep_input_PIDE @{theory "Test"} "pbl_ttest" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, []),
67.8 - Problem.prep_input_PIDE @{theory "Test"} "pbl_ttest_calc" [] Problem.id_empty
67.9 + [Problem.prep_input @{theory "Test"} "pbl_ttest" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, []),
67.10 + Problem.prep_input @{theory "Test"} "pbl_ttest_calc" [] Problem.id_empty
67.11 (["calculate", "test"],
67.12 [("#Given", ["realTestGiven t_t"]),
67.13 ("#Find", ["realTestFind s_s"])],
67.14 @@ -34,7 +34,7 @@
67.15 (Try (Repeat (Calculate ''DIVIDE''))) #>
67.16 (Try (Repeat (Calculate ''POWER''))))) t_t"
67.17 setup \<open>KEStore_Elems.add_mets @{context}
67.18 - [MethodC.prep_input_PIDE (@{theory "Test"}) "met_testcal" [] MethodC.id_empty
67.19 + [MethodC.prep_input (@{theory "Test"}) "met_testcal" [] MethodC.id_empty
67.20 (["Test", "test_calculate"],
67.21 [("#Given" , ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])],
67.22 {rew_ord'="sqrt_right",rls'=tval_rls,srls = Rule_Set.empty, prls = Rule_Set.empty,
68.1 --- a/test/Tools/isac/ProgLang/prog_tac.sml Fri Oct 07 20:46:48 2022 +0200
68.2 +++ b/test/Tools/isac/ProgLang/prog_tac.sml Sat Oct 08 11:40:48 2022 +0200
68.3 @@ -18,7 +18,7 @@
68.4 "-------- fun eval_leaf -------------------------------------------------------------------";
68.5 "-------- fun eval_leaf -------------------------------------------------------------------";
68.6 "-------- fun eval_leaf -------------------------------------------------------------------";
68.7 -val {scr = Prog sc, ...} = MethodC.from_store_PIDE ctxt ["Test", "sqrt-equ-test"];
68.8 +val {scr = Prog sc, ...} = MethodC.from_store ctxt ["Test", "sqrt-equ-test"];
68.9 case eval_leaf [] NONE TermC.empty sc of
68.10 (Expr (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
68.11 (Const (\<^const_name>\<open>Test.solve_root_equ\<close>, _) $ Free ("e_e", _) $ Free ("v_v", _)) $
69.1 --- a/test/Tools/isac/ProgLang/tactical.sml Fri Oct 07 20:46:48 2022 +0200
69.2 +++ b/test/Tools/isac/ProgLang/tactical.sml Sat Oct 08 11:40:48 2022 +0200
69.3 @@ -17,7 +17,7 @@
69.4 "-------- fun Tactical.is ----------------------------------------------------------------------";
69.5 "-------- fun Tactical.is ----------------------------------------------------------------------";
69.6 "-------- fun Tactical.is ----------------------------------------------------------------------";
69.7 -val {scr = Prog t, ...} = MethodC.from_store_PIDE ctxt ["simplification", "for_polynomials"];
69.8 +val {scr = Prog t, ...} = MethodC.from_store ctxt ["simplification", "for_polynomials"];
69.9
69.10 if Tactical.is (Program.body_of t)
69.11 then error "Tactical.is body_of [simplification,for_polynomials]" else ();
69.12 @@ -25,11 +25,11 @@
69.13 "-------- fun contained_in ---------------------------------------------------------------------";
69.14 "-------- fun contained_in ---------------------------------------------------------------------";
69.15 "-------- fun contained_in ---------------------------------------------------------------------";
69.16 -val {scr = Prog t, ...} = MethodC.from_store_PIDE ctxt ["simplification", "for_polynomials"];
69.17 +val {scr = Prog t, ...} = MethodC.from_store ctxt ["simplification", "for_polynomials"];
69.18 if contained_in t then error "NOT Tactical.contained_in [simplification,for_polynomials]" else ();
69.19
69.20 -val {scr = Prog t, ...} = MethodC.from_store_PIDE ctxt ["Test", "squ-equ-test-subpbl1"];
69.21 +val {scr = Prog t, ...} = MethodC.from_store ctxt ["Test", "squ-equ-test-subpbl1"];
69.22 if contained_in t then () else error "Tactical.contained_in [Test,squ-equ-test-subpbl1]";
69.23
69.24 -val {scr = Prog t, ...} = MethodC.from_store_PIDE ctxt ["simplification", "of_rationals"];
69.25 +val {scr = Prog t, ...} = MethodC.from_store ctxt ["simplification", "of_rationals"];
69.26 if contained_in t then () else error "Tactical.contained_in [simplification,of_rationals]";
70.1 --- a/test/Tools/isac/Specify/i-model.sml Fri Oct 07 20:46:48 2022 +0200
70.2 +++ b/test/Tools/isac/Specify/i-model.sml Sat Oct 08 11:40:48 2022 +0200
70.3 @@ -49,7 +49,7 @@
70.4 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
70.5 val cpI = if pI = Problem.id_empty then pI' else pI
70.6 val cmI = if mI = MethodC.id_empty then mI' else mI
70.7 - val {ppc, where_, prls, ...} = Problem.from_store_PIDE ctxt cpI;
70.8 + val {ppc, where_, prls, ...} = Problem.from_store ctxt cpI;
70.9
70.10 (*+*)if Model_Pattern.to_string ppc = "[\"" ^
70.11 "(#Given, (Traegerlaenge, l_l))\", \"" ^
71.1 --- a/test/Tools/isac/Specify/m-match.sml Fri Oct 07 20:46:48 2022 +0200
71.2 +++ b/test/Tools/isac/Specify/m-match.sml Sat Oct 08 11:40:48 2022 +0200
71.3 @@ -20,7 +20,7 @@
71.4 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
71.5 "solveFor x", "errorBound (eps=0)", "solutions L"];
71.6 val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =
71.7 - Problem.from_store_PIDE @{context} ["univariate", "equation"];
71.8 + Problem.from_store @{context} ["univariate", "equation"];
71.9 val xxx = M_Match.match_pbl fmz pbt;
71.10
71.11 case xxx of
71.12 @@ -42,11 +42,11 @@
71.13 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
71.14 "solveFor x", "errorBound (eps=0)", "solutions L"];
71.15 val pbt as {ppc = ppc,...} =
71.16 - Problem.from_store_PIDE @{context} ["univariate", "equation"];
71.17 + Problem.from_store @{context} ["univariate", "equation"];
71.18 val o_model = O_Model.init @{theory} fmz ppc
71.19 -val py = Problem.from_store_PIDE @{context} ["equation"];
71.20 -val py = Problem.from_store_PIDE @{context} ["univariate", "equation"];
71.21 -val py = Problem.from_store_PIDE @{context} ["sq", "rootX", "univariate", "equation"];
71.22 +val py = Problem.from_store @{context} ["equation"];
71.23 +val py = Problem.from_store @{context} ["univariate", "equation"];
71.24 +val py = Problem.from_store @{context} ["sq", "rootX", "univariate", "equation"];
71.25
71.26 if match_oris @{theory} (#prls py) o_model (#ppc py, #where_ py)
71.27 then () else error "fun match_oris CHANGED";
71.28 @@ -66,7 +66,7 @@
71.29 " REAL_LIST [c, c_2]]");
71.30 val ags = isalist2list ags';
71.31 val pI = ["LINEAR", "system"];
71.32 -val pats = (#ppc o Problem.from_store_PIDE @{context}) pI;
71.33 +val pats = (#ppc o Problem.from_store @{context}) pI;
71.34 "-a1-----------------------------------------------------";
71.35 (*M_Match.arguments = fn : theory -> pat list -> term list -> O_Model.T*)
71.36 val xxx = M_Match.arguments @{theory "EqSystem"} pats ags;
71.37 @@ -91,7 +91,7 @@
71.38 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
71.39 val ags = isalist2list ags';
71.40 val pI = ["LINEAR", "system"];
71.41 -val pats = (#ppc o Problem.from_store_PIDE @{context}) pI;
71.42 +val pats = (#ppc o Problem.from_store @{context}) pI;
71.43 "-b1-----------------------------------------------------";
71.44 val xxx = M_Match.arguments @{theory "Isac_Knowledge"} pats ags;
71.45 "-b2-----------------------------------------------------";
71.46 @@ -116,7 +116,7 @@
71.47 " [REAL_LIST [c, c_2]]");
71.48 val ags = isalist2list ags';
71.49 val pI = ["LINEAR", "system"];
71.50 -val pats = (#ppc o Problem.from_store_PIDE @{context}) pI;
71.51 +val pats = (#ppc o Problem.from_store @{context}) pI;
71.52 (*============ inhibit exn AK110726 ==============================================
71.53 val xxx - M_Match.arguments (theory "EqSystem") pats ags;
71.54 ============ inhibit exn AK110726 ==============================================*)
71.55 @@ -157,7 +157,7 @@
71.56 " REAL_LIST [c, c_2]]");
71.57 val ags = isalist2list ags';
71.58 val pI = ["LINEAR", "system"];
71.59 -val pats = (#ppc o Problem.from_store_PIDE @{context}) pI;
71.60 +val pats = (#ppc o Problem.from_store @{context}) pI;
71.61 "-a1-----------------------------------------------------";
71.62 (*M_Match.arguments = fn : theory -> pat list -> term list -> O_Model.T*)
71.63 val xxx = M_Match.arguments @{theory "EqSystem"} pats ags;
71.64 @@ -182,7 +182,7 @@
71.65 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
71.66 val ags = isalist2list ags';
71.67 val pI = ["LINEAR", "system"];
71.68 -val pats = (#ppc o Problem.from_store_PIDE @{context}) pI;
71.69 +val pats = (#ppc o Problem.from_store @{context}) pI;
71.70 "-b1-----------------------------------------------------";
71.71 val xxx = M_Match.arguments @{theory "Isac_Knowledge"} pats ags;
71.72 "-b2-----------------------------------------------------";
71.73 @@ -207,7 +207,7 @@
71.74 " [REAL_LIST [c, c_2]]");
71.75 val ags = isalist2list ags';
71.76 val pI = ["LINEAR", "system"];
71.77 -val pats = (#ppc o Problem.from_store_PIDE @{context}) pI;
71.78 +val pats = (#ppc o Problem.from_store @{context}) pI;
71.79 (*============ inhibit exn AK110726 ==============================================
71.80 val xxx - M_Match.arguments (theory "EqSystem") pats ags;
71.81 -------------------------------------------------------------------*)
71.82 @@ -238,7 +238,7 @@
71.83
71.84 case ((M_Match.arguments @{theory "EqSystem"} pats ags)
71.85 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
71.86 - [] => M_Match.arguments_msg_PIDE @{context} pI stac ags
71.87 + [] => M_Match.arguments_msg @{context} pI stac ags
71.88 | _ => error "calchead.sml M_Match.arguments 1st arg missing --------";
71.89
71.90 "-d------------------------------------------------------";
71.91 @@ -256,7 +256,7 @@
71.92
71.93 case ((M_Match.arguments @{theory "EqSystem"} pats ags)
71.94 handle ERROR _ => []) of (*why not TYPE ?WN100920*)
71.95 - [] => M_Match.arguments_msg_PIDE @{context} pI stac ags
71.96 + [] => M_Match.arguments_msg @{context} pI stac ags
71.97 | _ => error "calchead.sml M_Match.arguments 1st arg missing --------";
71.98
71.99 "-d------------------------------------------------------";
71.100 @@ -270,7 +270,7 @@
71.101 " [no_met]) [BOOL (x+1=2), REAL x]");
71.102 val AGS = isalist2list ags';
71.103 val pI = ["univariate", "equation", "test"];
71.104 -val PATS = (#ppc o Problem.from_store_PIDE @{context}) pI;
71.105 +val PATS = (#ppc o Problem.from_store @{context}) pI;
71.106 "-d1-----------------------------------------------------";
71.107 "--------------------------step through code M_Match.arguments---";
71.108 val (thy, pbt: Model_Pattern.T, ags) = (@{theory "Test"}, PATS, AGS);
72.1 --- a/test/Tools/isac/Specify/o-model.sml Fri Oct 07 20:46:48 2022 +0200
72.2 +++ b/test/Tools/isac/Specify/o-model.sml Sat Oct 08 11:40:48 2022 +0200
72.3 @@ -35,18 +35,18 @@
72.4 Step_Specify.nxt_specify_init_calc ctxt (fmz, sp);
72.5 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
72.6 (*val (_, hdl, (dI, pI, mI), pors, pctxt) = *)
72.7 - initialise_PIDE (fmz, (dI, pI, mI));
72.8 -"~~~~~ fun initialise_PIDE , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
72.9 + Step_Specify.initialise (fmz, (dI, pI, mI));
72.10 +"~~~~~ fun initialise , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
72.11 val thy = ThyC.get_theory dI
72.12 val ctxt = Proof_Context.init_global thy;
72.13 (*if*) mI = ["no_met"] (*else*);
72.14 - val pors = Problem.from_store_PIDE ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
72.15 -(*+*)Problem.from_store_PIDE ctxt pI: Problem.T;
72.16 -(*+*)(Problem.from_store_PIDE ctxt pI |> #ppc): Model_Pattern.T;
72.17 + val pors = Problem.from_store ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
72.18 +(*+*)Problem.from_store ctxt pI: Problem.T;
72.19 +(*+*)(Problem.from_store ctxt pI |> #ppc): Model_Pattern.T;
72.20
72.21 -(*+*)val o_model = (Problem.from_store_PIDE ctxt pI |> #ppc |>
72.22 +(*+*)val o_model = (Problem.from_store ctxt pI |> #ppc |>
72.23 O_Model.init thy fmz);
72.24 -"~~~~~ fun init , args:"; val (fmz, thy, pbt) = (fmz, thy, Problem.from_store_PIDE ctxt pI |> #ppc);
72.25 +"~~~~~ fun init , args:"; val (fmz, thy, pbt) = (fmz, thy, Problem.from_store ctxt pI |> #ppc);
72.26 val ori = (map (fn str => str
72.27 |> TermC.parseNEW'' thy
72.28 |> Input_Descript.split
72.29 @@ -176,7 +176,7 @@
72.30 "interval {x::real. 0 <= x & x <= pi}",
72.31 "errorBound (eps=(0::real))"]
72.32 val pbt as {ppc = ppc,...} =
72.33 - Problem.from_store_PIDE @{context} ["maximum_of", "function"];
72.34 + Problem.from_store @{context} ["maximum_of", "function"];
72.35 val o_model = O_Model.init @{theory} formalise ppc;
72.36
72.37 case o_model of
73.1 --- a/test/Tools/isac/Specify/refine.sml Fri Oct 07 20:46:48 2022 +0200
73.2 +++ b/test/Tools/isac/Specify/refine.sml Sat Oct 08 11:40:48 2022 +0200
73.3 @@ -87,23 +87,23 @@
73.4 "----------- Refine.refine_ori test-pbtyps --requires 'setup'----------------------------------";
73.5 "----------- Refine.refine_ori test-pbtyps --requires 'setup'----------------------------------";
73.6 (*case 1: no refinement *)
73.7 -case Refine.refine_ori_PIDE @{context} ori1 ["pbla", "refine", "test"] of
73.8 +case Refine.refine_ori @{context} ori1 ["pbla", "refine", "test"] of
73.9 NONE => () | _ => error "Refine.refine_ori case 1 broken";
73.10
73.11 (*case 2: refined to pbt without children *)
73.12 -case Refine.refine_ori_PIDE @{context} ori2 ["pbla", "refine", "test"] of
73.13 +case Refine.refine_ori @{context} ori2 ["pbla", "refine", "test"] of
73.14 SOME ["pbla3", "pbla", "refine", "test"] => () | _ => error "Refine.refine_ori case 2 broken";
73.15
73.16 (*case 3: refined to pbt with children *)
73.17 -case Refine.refine_ori_PIDE @{context} ori3 ["pbla", "refine", "test"] of
73.18 +case Refine.refine_ori @{context} ori3 ["pbla", "refine", "test"] of
73.19 SOME ["pbla2", "pbla", "refine", "test"] => () | _ => error "Refine.refine_ori case 3 broken";
73.20
73.21 (*case 4: refined to children (without child)*)
73.22 -case Refine.refine_ori_PIDE @{context} ori4 ["pbla", "refine", "test"] of
73.23 +case Refine.refine_ori @{context} ori4 ["pbla", "refine", "test"] of
73.24 SOME ["pbla2y", "pbla2", "pbla", "refine", "test"] => () | _ => error "Refine.refine_ori case 4 broken";
73.25
73.26 (*case 5: start refinement somewhere in ptyps*)
73.27 -case Refine.refine_ori_PIDE @{context} ori4 ["pbla2", "pbla", "refine", "test"] of
73.28 +case Refine.refine_ori @{context} ori4 ["pbla2", "pbla", "refine", "test"] of
73.29 SOME ["pbla2y", "pbla2", "pbla", "refine", "test"] => () | _ => error "Refine.refine_ori case 5 broken";
73.30
73.31
73.32 @@ -413,8 +413,8 @@
73.33 val ctxt = Proof_Context.init_global (ThyC.get_theory cdI)
73.34 val cpI = if pI = Problem.id_empty then pI' else pI;
73.35 val cmI = if mI = MethodC.id_empty then mI' else mI;
73.36 - val {ppc = pbt, prls, where_, ...} = Problem.from_store_PIDE ctxt cpI;
73.37 - val {ppc = mpc, ...} = MethodC.from_store_PIDE ctxt cmI
73.38 + val {ppc = pbt, prls, where_, ...} = Problem.from_store ctxt cpI;
73.39 + val {ppc = mpc, ...} = MethodC.from_store ctxt cmI
73.40 val (preok, (*+*)xxxxx(*+*) ) = Pre_Conds.check prls where_ pbl 0;
73.41 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
73.42 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
74.1 --- a/test/Tools/isac/Specify/refine.thy Fri Oct 07 20:46:48 2022 +0200
74.2 +++ b/test/Tools/isac/Specify/refine.thy Sat Oct 08 11:40:48 2022 +0200
74.3 @@ -14,30 +14,30 @@
74.4
74.5 section \<open>data for test "-ptyps.thy: store test-pbtyps by 'setup' ---"\<close>
74.6 setup \<open>KEStore_Elems.add_pbls @{context}
74.7 -[(Problem.prep_input_PIDE @{theory} "pbl_test_refine" [] Problem.id_empty
74.8 +[(Problem.prep_input @{theory} "pbl_test_refine" [] Problem.id_empty
74.9 (["refine", "test"], [], Rule_Set.empty, NONE, [])),
74.10 -(Problem.prep_input_PIDE @{theory Diff_App} "pbl_pbla" [] Problem.id_empty
74.11 +(Problem.prep_input @{theory Diff_App} "pbl_pbla" [] Problem.id_empty
74.12 (["pbla", "refine", "test"],
74.13 [("#Given", ["fixedValues a_a"])], Rule_Set.empty, NONE, [])),
74.14 -(Problem.prep_input_PIDE @{theory Diff_App} "pbl_pbla1" [] Problem.id_empty
74.15 +(Problem.prep_input @{theory Diff_App} "pbl_pbla1" [] Problem.id_empty
74.16 (["pbla1", "pbla", "refine", "test"],
74.17 [("#Given", ["fixedValues a_a", "maximum a_1"])], Rule_Set.empty, NONE, [])),
74.18 -(Problem.prep_input_PIDE @{theory Diff_App} "pbl_pbla2" [] Problem.id_empty
74.19 +(Problem.prep_input @{theory Diff_App} "pbl_pbla2" [] Problem.id_empty
74.20 (["pbla2", "pbla", "refine", "test"],
74.21 [("#Given", ["fixedValues a_a", "valuesFor a_2"])], Rule_Set.empty, NONE, [])),
74.22 -(Problem.prep_input_PIDE @{theory Diff_App} "pbl_pbla2x" [] Problem.id_empty
74.23 +(Problem.prep_input @{theory Diff_App} "pbl_pbla2x" [] Problem.id_empty
74.24 (["pbla2x", "pbla2", "pbla", "refine", "test"],
74.25 [("#Given", ["fixedValues a_a", "valuesFor a_2", "functionOf a2_x"])],
74.26 Rule_Set.empty, NONE, [])),
74.27 -(Problem.prep_input_PIDE @{theory Diff_App} "pbl_pbla2y" [] Problem.id_empty
74.28 +(Problem.prep_input @{theory Diff_App} "pbl_pbla2y" [] Problem.id_empty
74.29 (["pbla2y", "pbla2", "pbla", "refine", "test"],
74.30 [("#Given" ,["fixedValues a_a", "valuesFor a_2", "boundVariable a2_y"])],
74.31 Rule_Set.empty, NONE, [])),
74.32 -(Problem.prep_input_PIDE @{theory Diff_App} "pbl_pbla2z" [] Problem.id_empty
74.33 +(Problem.prep_input @{theory Diff_App} "pbl_pbla2z" [] Problem.id_empty
74.34 (["pbla2z", "pbla2", "pbla", "refine", "test"],
74.35 [("#Given" ,["fixedValues a_a", "valuesFor a_2", "interval a2_z"])],
74.36 Rule_Set.empty, NONE, [])),
74.37 -(Problem.prep_input_PIDE @{theory Diff_App} "pbl_pbla3" [] Problem.id_empty
74.38 +(Problem.prep_input @{theory Diff_App} "pbl_pbla3" [] Problem.id_empty
74.39 (["pbla3", "pbla", "refine", "test"],
74.40 [("#Given" ,["fixedValues a_a", "relations a_3"])],
74.41 Rule_Set.empty, NONE, []))]
75.1 --- a/test/Tools/isac/Specify/specify.sml Fri Oct 07 20:46:48 2022 +0200
75.2 +++ b/test/Tools/isac/Specify/specify.sml Sat Oct 08 11:40:48 2022 +0200
75.3 @@ -126,7 +126,7 @@
75.4 val method_i_model= get_obj g_met pt (fst p); (* is still empty *)
75.5 if method_i_model = []then () else error "is still empty CHANGED";
75.6 val method_i_model = I_Model.complete o_model problem_i_model
75.7 - [] ((#ppc o MethodC.from_store_PIDE ctxt) ["Diff_App", "max_by_calculus"]);
75.8 + [] ((#ppc o MethodC.from_store ctxt) ["Diff_App", "max_by_calculus"]);
75.9 if I_Model.to_string ctxt method_i_model = "[\n" ^
75.10 "(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])), \n" ^
75.11 "(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A ,(m_m, [A])), \n" ^
75.12 @@ -252,7 +252,7 @@
75.13 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
75.14 ...} = Calc.specify_data (ctree, pos);
75.15 val (dI, _, _) = References.select_input o_refs refs;
75.16 - val {ppc = m_patt, pre, prls, ...} = MethodC.from_store_PIDE ctxt mID
75.17 + val {ppc = m_patt, pre, prls, ...} = MethodC.from_store ctxt mID
75.18 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
75.19 val (o_model', ctxt') =
75.20
75.21 @@ -328,7 +328,7 @@
75.22 (*NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
75.23 (*NEW*) ...} = Calc.specify_data (pt, pos);
75.24 (*NEW*) val (dI, _, mID) = References.select_input o_refs refs;
75.25 -(*NEW*) val {ppc = m_patt, pre, prls, ...} = MethodC.from_store_PIDE ctxt mID
75.26 +(*NEW*) val {ppc = m_patt, pre, prls, ...} = MethodC.from_store ctxt mID
75.27 (*NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
75.28 (*NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
75.29 (*NEW*) val thy = ThyC.get_theory dI
75.30 @@ -412,11 +412,11 @@
75.31 "~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
75.32 (oris, (o_refs, refs), (pbl, met));
75.33 val cmI = if mI = MethodC.id_empty then mI' else mI;
75.34 - val {ppc = mpc, prls, pre, ...} = MethodC.from_store_PIDE ctxt cmI; (*..MethodC ?*)
75.35 + val {ppc = mpc, prls, pre, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
75.36 val (preok, _) = Pre_Conds.check prls pre pbl 0;
75.37 "~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return);
75.38 (*/------------------- check within find_next_step -----------------------------------------\*)
75.39 -(*+*)Model_Pattern.to_string (MethodC.from_store_PIDE ctxt mI' |> #ppc) = "[\"" ^
75.40 +(*+*)Model_Pattern.to_string (MethodC.from_store ctxt mI' |> #ppc) = "[\"" ^
75.41 "(#Given, (Traegerlaenge, l))\", \"" ^
75.42 "(#Given, (Streckenlast, q))\", \"" ^
75.43 "(#Given, (FunktionsVariable, v))\", \"" ^ (* <---------- take m_field from here !!!*)
75.44 @@ -506,7 +506,7 @@
75.45 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
75.46 (*if*) p_ = Pos.Met (*then*);
75.47 val (i_model, m_patt) = (met,
75.48 - (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store_PIDE ctxt |> #ppc)
75.49 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #ppc)
75.50
75.51 val Add (5, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) =
75.52 (*case*)
75.53 @@ -614,7 +614,7 @@
75.54 (*.NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,
75.55 (*.NEW*) ...} =Calc.specify_data (pt, pos);
75.56 (*.NEW*) val (dI, _, mID) = References.select_input o_refs refs;
75.57 -(*.NEW*) val {ppc = m_patt, pre, prls, ...} = MethodC.from_store_PIDE ctxt mID
75.58 +(*.NEW*) val {ppc = m_patt, pre, prls, ...} = MethodC.from_store ctxt mID
75.59 (*.NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
75.60 (*.NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt);
75.61
75.62 @@ -779,7 +779,7 @@
75.63 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
75.64 (*if*) p_ = Pos.Met (*then*);
75.65 val (i_model, m_patt) = (met,
75.66 - (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store_PIDE ctxt |> #ppc)
75.67 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #ppc)
75.68
75.69 val Add (4, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]), (Free ("id_fun", _), [Free ("y", _)]))) =
75.70 (*case*)
75.71 @@ -803,7 +803,7 @@
75.72 (*\------------------- check for entry to check_single -------------------------------------/*)
75.73
75.74 "~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
75.75 - (ctxt, sel, oris, met, ((#ppc o MethodC.from_store_PIDE ctxt) cmI), ct);
75.76 + (ctxt, sel, oris, met, ((#ppc o MethodC.from_store ctxt) cmI), ct);
75.77 val SOME t = (*case*) TermC.parseNEW ctxt str (*of*);
75.78
75.79 (*+*)val Const (\<^const_name>\<open>Biegelinie\<close>, _) $ Free ("y", _) = t;
75.80 @@ -839,20 +839,20 @@
75.81 (*+*)then () else error "associate_input' Model_Pattern CHANGED";
75.82 (*BUT: m_field can change from root-Problem to sub-MethodC --------------------vvv*)
75.83 (* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
75.84 -(*+*)if (Problem.from_store_PIDE ctxt ["vonBelastungZu", "Biegelinien"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
75.85 +(*+*)if (Problem.from_store ctxt ["vonBelastungZu", "Biegelinien"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
75.86 "(#Given, (Streckenlast, q_q))\", \"" ^
75.87 "(#Given, (FunktionsVariable, v_v))\", \"" ^
75.88 "(#Find, (Funktionen, funs'''))\"]"
75.89 (*+*)then () else error "associate_input' Model_Pattern of Subproblem CHANGED";
75.90 (* root-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv ------------------------------------- \<up> *)
75.91 -(*+*)if (Problem.from_store_PIDE ctxt ["Biegelinien"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
75.92 +(*+*)if (Problem.from_store ctxt ["Biegelinien"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
75.93 "(#Given, (Traegerlaenge, l_l))\", \"" ^
75.94 "(#Given, (Streckenlast, q_q))\", \"" ^
75.95 "(#Find, (Biegelinie, b_b))\", \"" ^ (*------------------------------------- \<up> *)
75.96 "(#Relate, (Randbedingungen, r_b))\"]"
75.97 (*+*)then () else error "associate_input' Model_Pattern root-problem CHANGED";
75.98 (* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
75.99 -(*+*)if (MethodC.from_store_PIDE ctxt ["Biegelinien", "ausBelastung"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
75.100 +(*+*)if (MethodC.from_store ctxt ["Biegelinien", "ausBelastung"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
75.101 "(#Given, (Streckenlast, q__q))\", \"" ^
75.102 "(#Given, (FunktionsVariable, v_v))\", \"" ^
75.103 "(#Given, (Biegelinie, id_fun))\", \"" ^ (*--------------------------------- \<up> *)