1.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue May 12 16:22:00 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue May 12 17:42:29 2020 +0200
1.3 @@ -18,7 +18,7 @@
1.4 val node: filepath -> string list -> Pos.pos -> (filepath -> Pos.pos -> string list -> 'a -> 'b) -> 'a Store.node -> unit
1.5 val nodes: filepath -> string list -> Pos.pos -> (filepath -> Pos.pos -> string list -> 'a -> 'b) -> 'a Store.node list -> unit
1.6 val pbl2file: filepath -> Pos.pos -> Method.id -> Problem.T -> unit
1.7 - val pbl2term: theory -> Specify.pblRD -> term
1.8 + val pbl2term: theory -> Problem.id -> term
1.9 val pbl2xml: Problem.id -> Problem.T -> xml
1.10 val pbl_hierarchy2file: filepath -> unit
1.11 val pbls2file: filepath -> unit
1.12 @@ -139,7 +139,7 @@
1.13 new version with <KESTOREREF>s -- not used because linking
1.14 requires elements (rls, calc, ...) to be reorganized.*)
1.15 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
1.16 -fun pbl2term thy (pblRD: Specify.pblRD) = (*WN120405.TODO.txt*)
1.17 +fun pbl2term thy (pblRD: Problem.id) = (*WN120405.TODO.txt*)
1.18 TermC.str2term ("Problem (" ^ (get_thy o Context.theory_name) thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")");
1.19 (* term2str (pbl2term (Thy_Info_get_theory "Isac_Knowledge") ["equations","univariate","normalise"]);
1.20 val it = "Problem (Isac, [normalise, univariate, equations])" : string
1.21 @@ -331,7 +331,7 @@
1.22
1.23 (* interface for dialog-authoring: call in Buld_Thydata.thy only ! *)
1.24 fun update_metpair thy metID errpats = let
1.25 - val ret = (update_metdata (Specify.get_met' thy metID) errpats, metID)
1.26 + val ret = (update_metdata (Method.from_store' thy metID) errpats, metID)
1.27 handle ERROR _ => raise ERROR ("update_metpair: " ^ (strs2str metID) ^ " must address a method");
1.28 in ret end;
1.29
2.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue May 12 16:22:00 2020 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue May 12 17:42:29 2020 +0200
2.3 @@ -308,7 +308,7 @@
2.4
2.5 fun insert_errpatIDs thy theID errpatIDs = (* TODO: redo like insert_fillpatts *)
2.6 let
2.7 - val hrls = Specify.get_the theID
2.8 + val hrls = Thy_Read.from_store theID
2.9 val hrls' = update_hrls hrls errpatIDs
2.10 handle ERROR _ => raise ERROR ("insert_errpatIDs: " ^ strs2str theID ^ "must address a rule-set")
2.11 in (hrls', theID) end
3.1 --- a/src/Tools/isac/Interpret/derive.sml Tue May 12 16:22:00 2020 +0200
3.2 +++ b/src/Tools/isac/Interpret/derive.sml Tue May 12 17:42:29 2020 +0200
3.3 @@ -153,7 +153,7 @@
3.4 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::
3.5 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
3.6 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]
3.7 - val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
3.8 + val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
3.9 val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
3.10 val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
3.11 val pt = Ctree.update_branch pt p Ctree.TransitiveB
3.12 @@ -171,7 +171,7 @@
3.13 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
3.14 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
3.15 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
3.16 - val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
3.17 + val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
3.18 val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
3.19 val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
3.20 val pt = Ctree.update_branch pt p Ctree.TransitiveB
4.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Tue May 12 16:22:00 2020 +0200
4.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Tue May 12 17:42:29 2020 +0200
4.3 @@ -103,7 +103,7 @@
4.4 val thmDeriv = Thm.get_name_hint thm
4.5 val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv
4.6 val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
4.7 - val fillpats = case Specify.get_the theID of
4.8 + val fillpats = case Thy_Read.from_store theID of
4.9 Thy_Write.Hthm {fillpats, ...} => fillpats
4.10 | _ => raise ERROR "fill_from_store: uncovered case of get_the"
4.11 val some = map (fill_form subst (thm, form) id) fillpats
4.12 @@ -113,7 +113,7 @@
4.13 let
4.14 val f_curr = Ctree.get_curr_formula (pt, pos);
4.15 val pp = Ctree.par_pblobj pt p
4.16 - val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
4.17 + val (errpats, prog) = case Method.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
4.18 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
4.19 | _ => raise ERROR "find_fill_patterns: uncovered case of get_met"
4.20 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
4.21 @@ -161,7 +161,7 @@
4.22 |Tactic.Rewrite_Set_Inst (_, rlsID) => rlsID
4.23 | _ => "empty"
4.24 val (part, thyID) = Thy_Read.thy_containing_rls "Isac_Knowledge" rlsID;
4.25 - val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of
4.26 + val rls = case Thy_Read.from_store [part, thyID, "Rulesets", rlsID] of
4.27 Thy_Write.Hrls {thy_rls = (_, rls), ...} => rls
4.28 | _ => raise ERROR "from_store: uncovered case of get_the"
4.29 in case rls of
5.1 --- a/src/Tools/isac/Interpret/li-tool.sml Tue May 12 16:22:00 2020 +0200
5.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Tue May 12 17:42:29 2020 +0200
5.3 @@ -66,7 +66,7 @@
5.4 case find_first (test_dsc d) itms of
5.5 NONE => raise ERROR (error_msg_2 d itms)
5.6 | SOME (_, _, _, _, itm_) => I_Model.penvval_in itm_
5.7 - val pats = (#ppc o Specify.get_met) mI
5.8 + val pats = (#ppc o Method.from_store) mI
5.9 val _ = if pats = [] then raise ERROR error_msg_1 else ()
5.10 in (flat o (map (itm2arg itms))) pats end;
5.11
5.12 @@ -260,7 +260,7 @@
5.13 val itms = Specify.hack_until_review_Specify_2 metID itms
5.14 val actuals = arguments_from_model metID itms
5.15 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
5.16 - val (scr, sc) = (case (#scr o Specify.get_met) metID of
5.17 + val (scr, sc) = (case (#scr o Method.from_store) metID of
5.18 scr as Rule.Prog sc => (trace_init metID; (scr, sc))
5.19 | _ => raise ERROR ("init_pstate with " ^ Method.id_to_string metID))
5.20 val formals = Program.formal_args sc
5.21 @@ -277,7 +277,7 @@
5.22 else
5.23 let val (f, a) = assoc_by_type f aas
5.24 in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
5.25 - val {pre, prls, ...} = Specify.get_met metID;
5.26 + val {pre, prls, ...} = Method.from_store metID;
5.27 val pres = Pre_Conds.check' (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
5.28 val ctxt = ctxt |> ContextC.insert_assumptions pres;
5.29 val ist = Istate.e_pstate
5.30 @@ -293,7 +293,7 @@
5.31 let
5.32 val p' = Ctree.par_pblobj pt p
5.33 val metID = Ctree.get_obj Ctree.g_metID pt p'
5.34 - val {srls, ...} = Specify.get_met metID
5.35 + val {srls, ...} = Method.from_store metID
5.36 in srls end
5.37
5.38 (* resume program interpretation at the beginning of a step *)
5.39 @@ -304,13 +304,13 @@
5.40 if is_problem then
5.41 let
5.42 val metID = get_obj g_metID pt p'
5.43 - val {srls, ...} = Specify.get_met metID
5.44 + val {srls, ...} = Method.from_store metID
5.45 val (is, ctxt) =
5.46 case get_loc pt (p, p_) of
5.47 (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt)
5.48 | _ => raise ERROR "resume_prog: unexpected result from get_loc"
5.49 in
5.50 - ((is, ctxt), (#scr o Specify.get_met) metID)
5.51 + ((is, ctxt), (#scr o Method.from_store) metID)
5.52 end
5.53 else
5.54 (get_loc pt (p, p_),
6.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Tue May 12 16:22:00 2020 +0200
6.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Tue May 12 17:42:29 2020 +0200
6.3 @@ -503,7 +503,7 @@
6.4 val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
6.5 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
6.6 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
6.7 - val {ppc, ...} = Specify.get_met mI;
6.8 + val {ppc, ...} = Method.from_store mI;
6.9 val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
6.10 val itms = Specify.hack_until_review_Specify_1 mI itms
6.11 val srls = LItool.get_simplifier (pt, pos)
6.12 @@ -550,7 +550,7 @@
6.13 | by_tactic (Tactic.Check_Postcond' (pI, _)) (sub_ist, sub_ctxt) (pt, pos as (p, _)) =
6.14 let
6.15 val parent_pos = par_pblobj pt p
6.16 - val {scr, ...} = Specify.get_met (get_obj g_metID pt parent_pos);
6.17 + val {scr, ...} = Method.from_store (get_obj g_metID pt parent_pos);
6.18 val prog_res =
6.19 case find_next_step scr (pt, pos) sub_ist sub_ctxt of
6.20 (*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
6.21 @@ -618,7 +618,7 @@
6.22 fun compare_step (tacis, c, ptp as (pt, pos as (p, _))) ifo =
6.23 let
6.24 val fo = Calc.current_formula ptp
6.25 - val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
6.26 + val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
6.27 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
6.28 val (found, der) = Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
6.29 in
7.1 --- a/src/Tools/isac/Interpret/solve-step.sml Tue May 12 16:22:00 2020 +0200
7.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Tue May 12 17:42:29 2020 +0200
7.3 @@ -52,7 +52,7 @@
7.4 then
7.5 let
7.6 val thy' = Ctree.get_obj Ctree.g_domID pt p'
7.7 - val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt p')
7.8 + val {rew_ord', erls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt p')
7.9 in ("OK", thy', rew_ord', erls, false) end
7.10 else
7.11 let
7.12 @@ -69,7 +69,7 @@
7.13 then
7.14 let
7.15 val thy' = Ctree.get_obj Ctree.g_domID pt p'
7.16 - val {calc = scr_isa_fns, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt p')
7.17 + val {calc = scr_isa_fns, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt p')
7.18 val opt = assoc (scr_isa_fns, scrop)
7.19 in
7.20 case opt of
7.21 @@ -98,7 +98,7 @@
7.22 val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
7.23 Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
7.24 | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
7.25 - val {where_, ...} = Specify.get_pbt pI
7.26 + val {where_, ...} = Problem.from_store pI
7.27 val pres = map (I_Model.mk_env probl |> subst_atomic) where_
7.28 val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
7.29 then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
7.30 @@ -154,7 +154,7 @@
7.31 val pp = Ctree.par_pblobj pt p;
7.32 val thy' = Ctree.get_obj Ctree.g_domID pt pp;
7.33 val thy = ThyC.get_theory thy';
7.34 - val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp);
7.35 + val {rew_ord' = ro', erls = erls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt pp);
7.36 val f = Calc.current_formula cs;
7.37 val subst = Subst.T_from_input thy subs; (*TODO: input requires parse _: _ -> _ option*)
7.38 in
7.39 @@ -195,7 +195,7 @@
7.40 val pp = Ctree.par_pblobj pt p
7.41 val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
7.42 val f = Calc.current_formula cs;
7.43 - val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp)
7.44 + val {rew_ord', erls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt pp)
7.45 val subte = Subst.input_to_terms sube (*TODO: input requires parse _: _ -> _ option*)
7.46 val subst = Subst.T_from_string_eqs thy sube
7.47 val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
8.1 --- a/src/Tools/isac/Interpret/step-solve.sml Tue May 12 16:22:00 2020 +0200
8.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Tue May 12 17:42:29 2020 +0200
8.3 @@ -109,7 +109,7 @@
8.4 | LI.Not_Derivable =>
8.5 let
8.6 val pp = Ctree.par_pblobj pt p
8.7 - val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
8.8 + val (errpats, nrls, prog) = case Method.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
8.9 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
8.10 | _ => raise ERROR "inform: uncovered case of get_met"
8.11 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
9.1 --- a/src/Tools/isac/Interpret/sub-problem.sml Tue May 12 16:22:00 2020 +0200
9.2 +++ b/src/Tools/isac/Interpret/sub-problem.sml Tue May 12 17:42:29 2020 +0200
9.3 @@ -23,19 +23,19 @@
9.4 if mI = ["no_met"]
9.5 then
9.6 let
9.7 - val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
9.8 + val pors = (Chead.match_ags thy ((#ppc o Problem.from_store) pI) ags)
9.9 (* Chead.match_ags : theory -> pat list -> term list -> ori list
9.10 ^^^ variables ^^^ values *)
9.11 handle ERROR "actual args do not match formal args"
9.12 => (Chead.match_ags_msg pI stac ags (*raise exn*);[]);
9.13 val pI' = Refine.refine_ori' pors pI;
9.14 in (pI', pors (* refinement over models with diff.prec only *),
9.15 - (hd o #met o Specify.get_pbt) pI') end
9.16 - else (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
9.17 + (hd o #met o Problem.from_store) pI') end
9.18 + else (pI, (Chead.match_ags thy ((#ppc o Problem.from_store) pI) ags)
9.19 handle ERROR "actual args do not match formal args"
9.20 => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
9.21 val (fmz_, vals) = Chead.oris2fmz_vals pors;
9.22 - val {cas, ppc, thy, ...} = Specify.get_pbt pI
9.23 + val {cas, ppc, thy, ...} = Problem.from_store pI
9.24 val dI = Context.theory_name thy (*take dI from _refined_ pbl*)
9.25 val dI = Context.theory_name (ThyC.sub_common (ThyC.get_theory dI, Ctree.rootthy pt))
9.26 val ctxt = ContextC.initialise dI vals
10.1 --- a/src/Tools/isac/Interpret/thy-read.sml Tue May 12 16:22:00 2020 +0200
10.2 +++ b/src/Tools/isac/Interpret/thy-read.sml Tue May 12 17:42:29 2020 +0200
10.3 @@ -11,6 +11,7 @@
10.4 val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id
10.5 val thy_containing_cal : ThyC.id -> Eval_Def.prog_calcID -> string * string
10.6
10.7 + val from_store : Thy_Write.theID -> Thy_Write.thydata (* for inform.sml *)
10.8 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.9 (* NONE *)
10.10 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.11 @@ -20,7 +21,7 @@
10.12 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
10.13 end
10.14 (**)
10.15 -structure Thy_Read(**): THEORY_STORE_READ(**) =
10.16 +structure Thy_Read(**): THEORY_STORE_READ(**) =
10.17 struct
10.18 (**)
10.19
10.20 @@ -102,4 +103,6 @@
10.21 | _ => raise ERROR ("thy_containing_cal : rls '" ^ sop ^ "' not in ancestors of thy '" ^ thy' ^ "'")
10.22 end
10.23
10.24 +fun from_store theID = Store.get (get_thes ()) theID theID;
10.25 +
10.26 (**)end(**)
11.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Tue May 12 16:22:00 2020 +0200
11.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Tue May 12 17:42:29 2020 +0200
11.3 @@ -160,7 +160,7 @@
11.4 crls = LinEq_crls, errpats = [], nrls = norm_Poly},
11.5 @{thm solve_linear_equation.simps})]
11.6 \<close>
11.7 -ML \<open>Specify.get_met' @{theory} ["LinEq","solve_lineq_equation"];\<close>
11.8 +ML \<open>Method.from_store' @{theory} ["LinEq","solve_lineq_equation"];\<close>
11.9
11.10 end
11.11
12.1 --- a/src/Tools/isac/MathEngBasic/method.sml Tue May 12 16:22:00 2020 +0200
12.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Tue May 12 17:42:29 2020 +0200
12.3 @@ -11,7 +11,9 @@
12.4 type id = Meth_Def.id
12.5 val id_empty: id
12.6 val id_to_string: id -> string
12.7 -(*val metID2str: id -> string*)
12.8 +
12.9 + val from_store: id -> T
12.10 + val from_store': theory -> id -> T
12.11
12.12 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
12.13 (*NONE*)
12.14 @@ -32,4 +34,8 @@
12.15 val id_empty = Meth_Def.id_empty;
12.16 val id_to_string = Meth_Def.id_to_string;
12.17
12.18 +(* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)
12.19 +fun from_store metID = Store.get (get_mets ()) metID metID;
12.20 +fun from_store' thy metID = Store.get (KEStore_Elems.get_mets thy) metID metID;
12.21 +
12.22 (**)end(**)
13.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Tue May 12 16:22:00 2020 +0200
13.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Tue May 12 17:42:29 2020 +0200
13.3 @@ -7,10 +7,11 @@
13.4 sig
13.5 type T = Probl_Def.T
13.6
13.7 - type id = Probl_Def.id
13.8 + type id = Probl_Def.id
13.9 val id_empty: id
13.10 val id_to_string: id -> string
13.11
13.12 + val from_store: id -> T
13.13 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
13.14 (*NONE*)
13.15 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
13.16 @@ -25,8 +26,16 @@
13.17
13.18 type T = Probl_Def.T;
13.19
13.20 +(*
13.21 + elements if the id are in reverse order as compared to Method:
13.22 + e.g. ["linear", "univariate", "equation"] has "equation" as parent node --
13.23 + -- this makes the id readable.
13.24 +*)
13.25 type id = Probl_Def.id;
13.26 +
13.27 val id_empty = Probl_Def.id_empty;
13.28 val id_to_string = Probl_Def.id_to_string;
13.29
13.30 +fun from_store id = Store.get (get_ptyps ()) id (rev id)
13.31 +
13.32 (**)end(**)
14.1 --- a/src/Tools/isac/MathEngine/fetch-tactics.sml Tue May 12 16:22:00 2020 +0200
14.2 +++ b/src/Tools/isac/MathEngine/fetch-tactics.sml Tue May 12 17:42:29 2020 +0200
14.3 @@ -31,7 +31,7 @@
14.4 val thy = ThyC.get_theory thy';
14.5 val metID = get_obj g_metID pt pp;
14.6 val metID' = if metID = Method.id_empty then (thd3 o snd3) (get_obj g_origin pt pp) else metID
14.7 - val (sc, srls) = (case Specify.get_met metID' of
14.8 + val (sc, srls) = (case Method.from_store metID' of
14.9 {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => raise ERROR "from_prog 1")
14.10 val subst = get_istate_LI pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
14.11 val ctxt = get_ctxt pt (p, p_)
14.12 @@ -56,7 +56,7 @@
14.13 if metID = Method.id_empty
14.14 then (thd3 o snd3) (get_obj g_origin pt pp)
14.15 else metID
14.16 - val (sc, srls, erls, ro) = (case Specify.get_met metID' of
14.17 + val (sc, srls, erls, ro) = (case Method.from_store metID' of
14.18 {scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
14.19 | _ => raise ERROR "specific_from_prog 1")
14.20 val (env, (a, v)) = (case get_istate_LI pt (p, p_) of
15.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Tue May 12 16:22:00 2020 +0200
15.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Tue May 12 17:42:29 2020 +0200
15.3 @@ -147,7 +147,7 @@
15.4 if pI' = Problem.id_empty
15.5 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
15.6 else pI'
15.7 - val {ppc, where_, prls, ...} = Specify.get_pbt pblID
15.8 + val {ppc, where_, prls, ...} = Problem.from_store pblID
15.9 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc, where_, prls) os
15.10 in
15.11 (model_ok, pblID, hdl, pbl, pre)
15.12 @@ -162,7 +162,7 @@
15.13 val metID = if mI' = Method.id_empty
15.14 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
15.15 else mI'
15.16 - val {ppc, pre, prls, scr, ...} = Specify.get_met metID
15.17 + val {ppc, pre, prls, scr, ...} = Method.from_store metID
15.18 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
15.19 in
15.20 (model_ok, metID, scr, pbl, pre)
15.21 @@ -175,7 +175,7 @@
15.22 case Ctree.get_obj I pt p of
15.23 Ctree.PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
15.24 | Ctree.PrfObj _ => raise ERROR "context_pbl: uncovered case"
15.25 - val {ppc,where_,prls,...} = Specify.get_pbt pI
15.26 + val {ppc,where_,prls,...} = Problem.from_store pI
15.27 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
15.28 in
15.29 (model_ok, pI, hdl, pbl, pre)
15.30 @@ -187,7 +187,7 @@
15.31 case Ctree.get_obj I pt p of
15.32 Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os)
15.33 | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case"
15.34 - val {ppc,pre,prls,scr,...} = Specify.get_met mI
15.35 + val {ppc,pre,prls,scr,...} = Method.from_store mI
15.36 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
15.37 in
15.38 (model_ok, mI, scr, pbl, pre)
15.39 @@ -203,7 +203,7 @@
15.40 case Refine.problem (ThyC.get_theory "Isac_Knowledge") pI probl of
15.41 NONE => (*copy from context_pbl*)
15.42 let
15.43 - val {ppc,where_,prls,...} = Specify.get_pbt pI
15.44 + val {ppc,where_,prls,...} = Problem.from_store pI
15.45 val (_, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
15.46 in
15.47 (false, pI, hdl, pbl, pre)
16.1 --- a/src/Tools/isac/Specify/calchead.sml Tue May 12 16:22:00 2020 +0200
16.2 +++ b/src/Tools/isac/Specify/calchead.sml Tue May 12 17:42:29 2020 +0200
16.3 @@ -441,7 +441,7 @@
16.4 (* report part of the error-msg which is not available in match_args *)
16.5 fun match_ags_msg pI stac ags =
16.6 let
16.7 - val pats = (#ppc o Specify.get_pbt) pI
16.8 + val pats = (#ppc o Problem.from_store) pI
16.9 val msg = (dots 70 ^ "\n"
16.10 ^ "*** problem " ^ strs2str pI ^ " has the ...\n"
16.11 ^ "*** model-pattern " ^ Model_Pattern.to_string pats ^ "\n"
16.12 @@ -487,7 +487,7 @@
16.13 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
16.14 val cpI = if pI = Problem.id_empty then pI' else pI
16.15 val cmI = if mI = Method.id_empty then mI' else mI
16.16 - val {ppc, pre, prls, ...} = Specify.get_met cmI
16.17 + val {ppc, pre, prls, ...} = Method.from_store cmI
16.18 in
16.19 case I_Model.check_single ctxt sel oris met ppc ct of
16.20 I_Model.Add itm => (*..union old input *)
16.21 @@ -501,7 +501,7 @@
16.22 val pb = foldl and_ (true, map fst pre')
16.23 val (p_, _) =
16.24 nxt_spec Pos.Met pb oris (dI',pI',mI') (pbl,met')
16.25 - ((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI);
16.26 + ((#ppc o Problem.from_store) cpI,ppc) (dI,pI,mI);
16.27 in
16.28 ("ok", ([], [], (pt', (p, p_))))
16.29 end
16.30 @@ -511,7 +511,7 @@
16.31 val pb = foldl and_ (true, map fst pre')
16.32 val (p_, _) =
16.33 nxt_spec Pos.Met pb oris (dI',pI',mI') (pbl,met)
16.34 - ((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI);
16.35 + ((#ppc o Problem.from_store) cpI,(#ppc o Method.from_store) cmI) (dI,pI,mI);
16.36 in
16.37 (msg, ([], [], (pt, (p, p_))))
16.38 end
16.39 @@ -522,7 +522,7 @@
16.40 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
16.41 val cpI = if pI = Problem.id_empty then pI' else pI
16.42 val cmI = if mI = Method.id_empty then mI' else mI
16.43 - val {ppc, where_, prls, ...} = Specify.get_pbt cpI
16.44 + val {ppc, where_, prls, ...} = Problem.from_store cpI
16.45 in
16.46 case I_Model.check_single ctxt sel oris pbl ppc ct of
16.47 I_Model.Add itm => (*..union old input *)
16.48 @@ -536,7 +536,7 @@
16.49 val pre = Pre_Conds.check' thy prls where_ pbl';
16.50 val pb = foldl and_ (true, map fst pre);
16.51 val (p_, _) =
16.52 - nxt_spec Pos.Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI);
16.53 + nxt_spec Pos.Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI);
16.54 in
16.55 ("ok", ([], [], (pt', (p, p_))))
16.56 end
16.57 @@ -546,7 +546,7 @@
16.58 val pb = foldl and_ (true, map fst pre)
16.59 val (p_, _(*Tactic.input*)) =
16.60 nxt_spec Pos.Pbl pb oris (dI', pI', mI') (pbl, met)
16.61 - (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
16.62 + (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI)
16.63 in
16.64 (msg, ([], [], (pt, (p, p_))))
16.65 end
16.66 @@ -563,7 +563,7 @@
16.67 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
16.68 val cpI = if pI = Problem.id_empty then pI' else pI;
16.69 in
16.70 - case I_Model.check_single ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct of
16.71 + case I_Model.check_single ctxt sel oris pbl ((#ppc o Problem.from_store) cpI) ct of
16.72 I_Model.Add itm (*..union old input *) =>
16.73 let
16.74 val pbl' = I_Model.add_single thy itm pbl
16.75 @@ -593,7 +593,7 @@
16.76 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
16.77 val cmI = if mI = Method.id_empty then mI' else mI;
16.78 in
16.79 - case I_Model.check_single ctxt sel oris met ((#ppc o Specify.get_met) cmI) ct of
16.80 + case I_Model.check_single ctxt sel oris met ((#ppc o Method.from_store) cmI) ct of
16.81 I_Model.Add itm (*..union old input *) =>
16.82 let
16.83 val met' = I_Model.add_single thy itm met;
16.84 @@ -687,8 +687,8 @@
16.85 Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
16.86 | _ => raise ERROR "complete_mod: unvered case get_obj"
16.87 val (_, pI, mI) = some_spec ospec spec
16.88 - val mpc = (#ppc o Specify.get_met) mI
16.89 - val ppc = (#ppc o Specify.get_pbt) pI
16.90 + val mpc = (#ppc o Method.from_store) mI
16.91 + val ppc = (#ppc o Problem.from_store) pI
16.92 val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
16.93 val pt = Ctree.update_pblppc pt p pits
16.94 val pt = Ctree.update_metppc pt p mits
16.95 @@ -704,7 +704,7 @@
16.96 Ctree.PblObj {origin = (pors, (dI, pI, mI), _), ...}
16.97 => (pors, dI, pI, mI)
16.98 | _ => raise ERROR "all_modspec: uncovered case get_obj"
16.99 - val {ppc, ...} = Specify.get_met mI
16.100 + val {ppc, ...} = Method.from_store mI
16.101 val (_, vals) = oris2fmz_vals pors
16.102 val ctxt = ContextC.initialise dI vals
16.103 val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),
16.104 @@ -756,7 +756,7 @@
16.105 val pre = if metID = Method.id_empty then []
16.106 else
16.107 let
16.108 - val {prls, pre= where_, ...} = Specify.get_met metID
16.109 + val {prls, pre= where_, ...} = Method.from_store metID
16.110 val pre = Pre_Conds.check prls where_ meth 0
16.111 in pre end
16.112 val allcorrect = is_complete_mod_ meth andalso foldl and_ (true, (map #1 pre))
16.113 @@ -769,7 +769,7 @@
16.114 val pre = if pI = Problem.id_empty then []
16.115 else
16.116 let
16.117 - val {prls, where_, ...} = Specify.get_pbt pI
16.118 + val {prls, where_, ...} = Problem.from_store pI
16.119 val pre = Pre_Conds.check prls where_ probl 0
16.120 in pre end
16.121 val allcorrect = is_complete_mod_ probl andalso foldl and_ (true, (map #1 pre))
16.122 @@ -782,7 +782,7 @@
16.123 | pt_form (Ctree.PblObj {probl, spec, origin = (_, spec', _), ...}) =
16.124 let
16.125 val (dI, pI, _) = Ctree.get_somespec' spec spec'
16.126 - val {cas, ...} = Specify.get_pbt pI
16.127 + val {cas, ...} = Problem.from_store pI
16.128 in case cas of
16.129 NONE => Ctree.Form (Auto_Prog.pblterm dI pI)
16.130 | SOME t => Ctree.Form (subst_atomic (I_Model.mk_env probl) t)
16.131 @@ -935,7 +935,7 @@
16.132 val (ospec, hdf', spec, probl) = case Ctree.get_obj I pt p of
16.133 Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
16.134 | _ => raise ERROR "get_ocalhd Pbl: uncovered case get_obj"
16.135 - val {prls, where_, ...} = Specify.get_pbt (#2 (some_spec ospec spec))
16.136 + val {prls, where_, ...} = Problem.from_store (#2 (some_spec ospec spec))
16.137 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls where_ probl
16.138 in
16.139 (ocalhd_complete probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
16.140 @@ -945,7 +945,7 @@
16.141 val (ospec, hdf', spec, meth) = case Ctree.get_obj I pt p of
16.142 Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
16.143 | _ => raise ERROR "get_ocalhd Met: uncovered case get_obj"
16.144 - val {prls, pre, ...} = Specify.get_met (#3 (some_spec ospec spec))
16.145 + val {prls, pre, ...} = Method.from_store (#3 (some_spec ospec spec))
16.146 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls pre meth
16.147 in
16.148 (ocalhd_complete meth pre spec, Pos.Met, hdf', meth, pre, spec)
17.1 --- a/src/Tools/isac/Specify/input-calchead.sml Tue May 12 16:22:00 2020 +0200
17.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Tue May 12 17:42:29 2020 +0200
17.3 @@ -54,7 +54,7 @@
17.4 fun cas_input_ ((dI, pI, mI): Spec.T) dtss = (*WN110515 reconsider thy..ctxt*)
17.5 let
17.6 val thy = ThyC.get_theory dI
17.7 - val {ppc, ...} = Specify.get_pbt pI
17.8 + val {ppc, ...} = Problem.from_store pI
17.9 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
17.10 val its = O_Model.add_id its_
17.11 val pits = map flattup2 its
17.12 @@ -63,9 +63,9 @@
17.13 then (pI, mI)
17.14 else
17.15 case Refine.problem thy pI pits of
17.16 - SOME (pI,_) => (pI, (hd o #met o Specify.get_pbt) pI)
17.17 - | NONE => (pI, (hd o #met o Specify.get_pbt) pI)
17.18 - val {ppc, pre, prls, ...} = Specify.get_met mI
17.19 + SOME (pI,_) => (pI, (hd o #met o Problem.from_store) pI)
17.20 + | NONE => (pI, (hd o #met o Problem.from_store) pI)
17.21 + val {ppc, pre, prls, ...} = Method.from_store mI
17.22 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
17.23 val its = O_Model.add_id its_
17.24 val mits = map flattup2 its
17.25 @@ -269,35 +269,35 @@
17.26 if dI <> sdI
17.27 then let val its = map (parsitm (ThyC.get_theory dI)) probl;
17.28 val (its, trms) = filter_sep is_Par its;
17.29 - val pbt = (#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec sspec))
17.30 + val pbt = (#ppc o Problem.from_store) (#2 (Chead.some_spec ospec sspec))
17.31 in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
17.32 else
17.33 if pI <> spI
17.34 then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
17.35 else
17.36 - let val pbt = (#ppc o Specify.get_pbt) pI
17.37 + let val pbt = (#ppc o Problem.from_store) pI
17.38 val dI' = #1 (Chead.some_spec ospec spec)
17.39 val oris = if pI = #2 ospec then oris
17.40 else O_Model.init fmz_(ThyC.get_theory"Isac_Knowledge") pbt(* |> #1*);
17.41 in (Pos.Pbl, appl_adds dI' oris probl pbt
17.42 (map itms2fstr probl), meth) end
17.43 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
17.44 - then let val met = (#ppc o Specify.get_met) mI
17.45 + then let val met = (#ppc o Method.from_store) mI
17.46 val mits = Chead.complete_metitms oris probl meth met
17.47 in if foldl and_ (true, map #3 mits)
17.48 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
17.49 end
17.50 else (Pos.Pbl, appl_adds (#1 (Chead.some_spec ospec spec)) oris [(*!!!*)]
17.51 - ((#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec spec)))
17.52 + ((#ppc o Problem.from_store) (#2 (Chead.some_spec ospec spec)))
17.53 (imodel2fstr imodel), meth)
17.54 val pt = Ctree.update_spec pt p spec;
17.55 in if pos_ = Pos.Pbl
17.56 - then let val {prls,where_,...} = Specify.get_pbt (#2 (Chead.some_spec ospec spec))
17.57 + then let val {prls,where_,...} = Problem.from_store (#2 (Chead.some_spec ospec spec))
17.58 val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls where_ pits
17.59 in (Ctree.update_pbl pt p pits,
17.60 (Chead.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Ctree.ocalhd)
17.61 end
17.62 - else let val {prls,pre,...} = Specify.get_met (#3 (Chead.some_spec ospec spec))
17.63 + else let val {prls,pre,...} = Method.from_store (#3 (Chead.some_spec ospec spec))
17.64 val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls pre mits
17.65 in (Ctree.update_met pt p mits,
17.66 (Chead.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Ctree.ocalhd)
18.1 --- a/src/Tools/isac/Specify/ptyps.sml Tue May 12 16:22:00 2020 +0200
18.2 +++ b/src/Tools/isac/Specify/ptyps.sml Tue May 12 17:42:29 2020 +0200
18.3 @@ -13,12 +13,6 @@
18.4 val match_itms_oris : theory -> I_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
18.5 O_Model.T -> bool * (I_Model.T * Pre_Conds.T)
18.6
18.7 - val get_pbt : Problem.id -> Problem.T
18.8 - val get_met : Method.id -> Method.T (* for generate.sml *)
18.9 - val get_met' : theory -> Method.id -> Method.T (* for pbl-met-hierarchy.sml *)
18.10 - val get_the : Thy_Write.theID -> Thy_Write.thydata (* for inform.sml *)
18.11 -
18.12 - type pblRD = string list (* for pbl-met-hierarchy.sml *)
18.13 val format_pblIDl : string list list -> string (* for thy-hierarchy.sml *)
18.14 val scan : string list -> 'a Store.T -> string list list (* for thy-hierarchy.sml *)
18.15 val itm_out : theory -> I_Model.feedback -> string
18.16 @@ -149,21 +143,6 @@
18.17 val e_errpat = ("e_errpatID", [TermC.parse_patt @{theory} "?a = ?b"], [@{thm refl}]): Error_Pattern_Def.T
18.18 val e_fillpat = ("e_fillpatID", TermC.parse_patt @{theory} "?a = _", "e_errpatID")
18.19
18.20 -(** breadth-first search on hierarchy of problem-types **)
18.21 -
18.22 -(* pblID are reverted _on calling_ the retrieve-funs *)
18.23 -type pblRD = (*e.g. ["equations","univariate","normalise"] for internal retrieval *)
18.24 - Problem.id; (*e.g. ["normalise","univariate","equations"] presented to student *)
18.25 -
18.26 -
18.27 -(* TODO: generalize search for subthy *)
18.28 -fun get_pbt (pblID: Problem.id) =Store.get (get_ptyps ()) pblID (rev pblID)
18.29 -
18.30 -(* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)
18.31 -fun get_met metID =Store.get (get_mets ()) metID metID;
18.32 -fun get_met' thy metID =Store.get (KEStore_Elems.get_mets thy) metID metID;
18.33 -fun get_the theID =Store.get (get_thes ()) theID theID;
18.34 -
18.35 (* lookup a guh in hierarchy of problems / methods depending on fst 4 chars in guh *)
18.36 fun guh2kestoreID guh =
18.37 case (implode o (take_fromto 1 4) o Symbol.explode) guh of
18.38 @@ -373,9 +352,9 @@
18.39 (*\------- from Celem to Specify -------/*)
18.40 (* make a guh from a reference to an element in the kestore;
18.41 EXCEPT theory hierarchy ... compare 'fun keref2xml' *)
18.42 -fun pblID2guh pblID = (((#guh o get_pbt) pblID)
18.43 +fun pblID2guh pblID = (((#guh o Problem.from_store) pblID)
18.44 handle _ => raise ERROR ("pblID2guh: not for \"" ^ strs2str' pblID ^ "\""));
18.45 -fun metID2guh metID = (((#guh o get_met) metID)
18.46 +fun metID2guh metID = (((#guh o Method.from_store) metID)
18.47 handle _ => raise ERROR ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\""));
18.48 fun kestoreID2guh Pbl_ kestoreID = pblID2guh kestoreID
18.49 | kestoreID2guh Met_ kestoreID = metID2guh kestoreID
19.1 --- a/src/Tools/isac/Specify/specify-step.sml Tue May 12 16:22:00 2020 +0200
19.2 +++ b/src/Tools/isac/Specify/specify-step.sml Tue May 12 17:42:29 2020 +0200
19.3 @@ -38,7 +38,7 @@
19.4 val pI' = case Ctree.get_obj I pt p of
19.5 Ctree.PblObj {origin = (_, (_, pI', _),_), ...} => pI'
19.6 | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
19.7 - val {ppc, ...} = Specify.get_pbt pI'
19.8 + val {ppc, ...} = Problem.from_store pI'
19.9 val pbl = I_Model.init ppc
19.10 in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
19.11 | check (Tactic.Refine_Problem pI) (pt, (p, _)) =
19.12 @@ -76,7 +76,7 @@
19.13 => (oris, dI, pI, dI', pI', itms)
19.14 | _ => raise ERROR "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj"
19.15 val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
19.16 - val {ppc, where_, prls, ...} = Specify.get_pbt pID;
19.17 + val {ppc, where_, prls, ...} = Problem.from_store pID;
19.18 val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty
19.19 then (false, (I_Model.init ppc, []))
19.20 else Specify.match_itms_oris thy itms (ppc, where_, prls) oris;
20.1 --- a/src/Tools/isac/Specify/specify.sml Tue May 12 16:22:00 2020 +0200
20.2 +++ b/src/Tools/isac/Specify/specify.sml Tue May 12 17:42:29 2020 +0200
20.3 @@ -34,11 +34,11 @@
20.4 let
20.5 val cpI = if pI = Problem.id_empty then pI' else pI;
20.6 val cmI = if mI = Method.id_empty then mI' else mI;
20.7 - val {ppc = pbt, prls, where_, ...} = Specify.get_pbt cpI;
20.8 + val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;
20.9 val pre = Pre_Conds.check' "thy 100820" prls where_ pbl;
20.10 val preok = foldl and_ (true, map fst pre);
20.11 (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
20.12 - val mpc = (#ppc o Specify.get_met) cmI
20.13 + val mpc = (#ppc o Method.from_store) cmI
20.14 in
20.15 case p_ of
20.16 Pbl =>
21.1 --- a/src/Tools/isac/Specify/step-specify.sml Tue May 12 16:22:00 2020 +0200
21.2 +++ b/src/Tools/isac/Specify/step-specify.sml Tue May 12 17:42:29 2020 +0200
21.3 @@ -31,8 +31,8 @@
21.4 | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
21.5 val (dI, pI, mI) = some_spec ospec spec
21.6 val thy = ThyC.get_theory dI
21.7 - val mpc = (#ppc o Specify.get_met) mI (* just for reuse complete_mod_ *)
21.8 - val {cas, ppc, ...} = Specify.get_pbt pI
21.9 + val mpc = (#ppc o Method.from_store) mI (* just for reuse complete_mod_ *)
21.10 + val {cas, ppc, ...} = Problem.from_store pI
21.11 val pbl = I_Model.init ppc (* fill in descriptions *)
21.12 (*----------------if you think, this should be done by the Dialog
21.13 in the java front-end, search there for WN060225-modelProblem----*)
21.14 @@ -57,7 +57,7 @@
21.15 case opt of
21.16 SOME pI' =>
21.17 let
21.18 - val {met, ...} = Specify.get_pbt pI'
21.19 + val {met, ...} = Problem.from_store pI'
21.20 (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
21.21 val mI = if length met = 0 then Method.id_empty else hd met
21.22 val thy = ThyC.get_theory dI
21.23 @@ -93,7 +93,7 @@
21.24 (oris, dI, dI', pI', probl, ctxt)
21.25 | _ => raise ERROR ""
21.26 val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
21.27 - val {ppc,where_,prls,...} = Specify.get_pbt pI
21.28 + val {ppc,where_,prls,...} = Problem.from_store pI
21.29 val pbl =
21.30 if pI' = Problem.id_empty andalso pI = Problem.id_empty
21.31 then (false, (I_Model.init ppc, []))
21.32 @@ -114,7 +114,7 @@
21.33 PblObj {origin = (oris, _, _), probl = pbl, spec = (dI, _, _), meth=met, ctxt, ...}
21.34 => (oris, pbl, dI, met, ctxt)
21.35 | _ => raise ERROR "by_tactic_input Specify_Method: uncovered case get_obj"
21.36 - val {ppc,pre,prls,...} = Specify.get_met mID
21.37 + val {ppc,pre,prls,...} = Method.from_store mID
21.38 val thy = ThyC.get_theory dI
21.39 val oris = O_Model.add thy ppc oris
21.40 val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
21.41 @@ -154,13 +154,13 @@
21.42 | _ => raise ERROR "Step_Solve.by_tactic (Model_Problem': uncovered case get_obj"
21.43 val thy' = if dI = ThyC.id_empty then dI' else dI
21.44 val thy = ThyC.get_theory thy'
21.45 - val {ppc, prls, where_, ...} = Specify.get_pbt pI'
21.46 + val {ppc, prls, where_, ...} = Problem.from_store pI'
21.47 val pre = Pre_Conds.check' thy prls where_ pbl
21.48 val pb = foldl and_ (true, map fst pre)
21.49 val ((p, _), _, _, pt) =
21.50 Specify_Step.add (Tactic.Model_Problem'([],pbl,met)) (Istate_Def.Uistate, ctxt) (pt, pos)
21.51 val (_, _) = Chead.nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
21.52 - (ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI');
21.53 + (ppc,(#ppc o Method.from_store) mI') (dI',pI',mI');
21.54 in
21.55 ("ok", ([], [], (pt, (p, Pbl))))
21.56 end
21.57 @@ -170,7 +170,7 @@
21.58 (* val (dI', ctxt) = case get_obj I pt p of
21.59 PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)
21.60 | _ => raise ERROR "Step_Solve.by_tactic (Refine_Tacitly': uncovered case get_obj"*)
21.61 - val {met, thy,...} = Specify.get_pbt pIre
21.62 + val {met, thy,...} = Problem.from_store pIre
21.63 val (domID, metID) = (Context.theory_name thy, if length met = 0 then Method.id_empty else hd met)
21.64 val ((p,_), _, _, pt) =
21.65 Specify_Step.add (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
21.66 @@ -210,7 +210,7 @@
21.67 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
21.68 (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
21.69 | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
21.70 - val {ppc, pre, prls,...} = Specify.get_met mID
21.71 + val {ppc, pre, prls,...} = Method.from_store mID
21.72 val thy = ThyC.get_theory dI
21.73 val oris = O_Model.add thy ppc oris
21.74 val met = if met = [] then pbl else met
21.75 @@ -234,9 +234,9 @@
21.76 | _ => raise ERROR "Step_Solve.by_tactic (Specify_Theory': uncovered case get_obj"
21.77 val _ = case p_ of Met => met | _ => pbl
21.78 val cpI = if pI = Problem.id_empty then pI' else pI
21.79 - val {prls = per, ppc, where_ = pwh, ...} = Specify.get_pbt cpI
21.80 + val {prls = per, ppc, where_ = pwh, ...} = Problem.from_store cpI
21.81 val cmI = if mI = Method.id_empty then mI' else mI
21.82 - val {prls = mer, ppc = mpc, pre= mwh, ...} = Specify.get_met cmI
21.83 + val {prls = mer, ppc = mpc, pre= mwh, ...} = Method.from_store cmI
21.84 val pre = case p_ of
21.85 Met => (Pre_Conds.check' thy mer mwh met)
21.86 | _ => (Pre_Conds.check' thy per pwh pbl)
21.87 @@ -264,7 +264,7 @@
21.88 if pI <> []
21.89 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
21.90 let
21.91 - val {cas, met, ppc, thy, ...} = Specify.get_pbt pI
21.92 + val {cas, met, ppc, thy, ...} = Problem.from_store pI
21.93 val dI = if dI = "" then Context.theory_name thy else dI
21.94 val mI = if mI = [] then hd met else mI
21.95 val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
21.96 @@ -278,7 +278,7 @@
21.97 if mI <> []
21.98 then (* from met-browser *)
21.99 let
21.100 - val {ppc, ...} = Specify.get_met mI
21.101 + val {ppc, ...} = Method.from_store mI
21.102 val dI = if dI = "" then "Isac_Knowledge" else dI
21.103 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
21.104 ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty)
21.105 @@ -298,18 +298,18 @@
21.106 if mI = ["no_met"]
21.107 then
21.108 let
21.109 - val (pors(*, pctxt*)) = Specify.get_pbt pI |> #ppc |> O_Model.init fmz thy;
21.110 + val (pors(*, pctxt*)) = Problem.from_store pI |> #ppc |> O_Model.init fmz thy;
21.111 val pctxt = ContextC.initialise' thy fmz;
21.112 val pI' = Refine.refine_ori' pors pI;
21.113 in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
21.114 - (hd o #met o Specify.get_pbt) pI')
21.115 + (hd o #met o Problem.from_store) pI')
21.116 end
21.117 else
21.118 let
21.119 - val pors = Specify.get_pbt pI |> #ppc |> O_Model.init fmz thy;
21.120 + val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy;
21.121 val pctxt = ContextC.initialise' thy fmz;
21.122 in (pI, (pors, pctxt), mI) end;
21.123 - val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)
21.124 + val {cas, ppc, thy = thy', ...} = Problem.from_store pI (*take dI from _refined_ pbl*)
21.125 val dI = Context.theory_name (ThyC.sub_common (thy, thy'))
21.126 val hdl = case cas of
21.127 NONE => Auto_Prog.pblterm dI pI
22.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Tue May 12 16:22:00 2020 +0200
22.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Tue May 12 17:42:29 2020 +0200
22.3 @@ -266,7 +266,7 @@
22.4 text \<open>\noindent Check if the given equation matches the specification of this
22.5 equation type.\<close>
22.6 ML \<open>
22.7 - Specify.match_pbl fmz (Specify.get_pbt ["univariate","equation"]);
22.8 + Specify.match_pbl fmz (Problem.from_store ["univariate","equation"]);
22.9 \<close>
22.10
22.11 text\<open>\noindent We switch up to the {\sisac} Context and try to solve the
22.12 @@ -290,7 +290,7 @@
22.13 specification of this equation type.\<close>
22.14
22.15 ML \<open>
22.16 - Specify.match_pbl fmz (Specify.get_pbt
22.17 + Specify.match_pbl fmz (Problem.from_store
22.18 ["abcFormula","degree_2","polynomial","univariate","equation"]);
22.19 \<close>
22.20
22.21 @@ -513,7 +513,7 @@
22.22 the original \emph{srls}.\\
22.23
22.24 \begin{verbatim}
22.25 - val {srls,...} = get_met ["SignalProcessing",
22.26 + val {srls,...} = Method.from_store ["SignalProcessing",
22.27 "Z_Transform",
22.28 "Inverse"];
22.29 \end{verbatim}
22.30 @@ -901,7 +901,7 @@
22.31 [["SignalProcessing","Z_Transform","Inverse"]])]\<close>
22.32 ML \<open>
22.33 Specify.show_ptyps() ();
22.34 - get_pbt ["Inverse","Z_Transform","SignalProcessing"];
22.35 + Problem.from_store ["Inverse","Z_Transform","SignalProcessing"];
22.36 \<close>
22.37
22.38 subsection \<open>Define Name and Signature for the Method\<close>
22.39 @@ -974,7 +974,7 @@
22.40 the hierarchy.\<close>
22.41
22.42 ML \<open>
22.43 - get_met ["SignalProcessing","Z_Transform","Inverse"];
22.44 + Method.from_store ["SignalProcessing","Z_Transform","Inverse"];
22.45 \<close>
22.46
22.47 section \<open>Program in TP-based language \label{prog-steps}\<close>
22.48 @@ -1228,10 +1228,10 @@
22.49 [Free ("x", _) $ _]
22.50 )
22.51 ],_
22.52 - ) = O_Model.init fmz thy ((#ppc o get_pbt) pI);
22.53 + ) = O_Model.init fmz thy ((#ppc o Problem.from_store) pI);
22.54
22.55 val Prog sc
22.56 - = (#scr o get_met) ["SignalProcessing",
22.57 + = (#scr o Method.from_store) ["SignalProcessing",
22.58 "Z_Transform",
22.59 "Inverse"];
22.60 atomty sc;
22.61 @@ -1307,7 +1307,7 @@
22.62 arguments in the arguments\ldots
22.63 \begin{verbatim}
22.64 val Prog s =
22.65 - (#scr o get_met) ["SignalProcessing",
22.66 + (#scr o Method.from_store) ["SignalProcessing",
22.67 "Z_Transform",
22.68 "Inverse"];
22.69 writeln (UnparseC.term s);
22.70 @@ -1591,7 +1591,7 @@
22.71 parse-tree of the program with {\sisac}'s specific debug tools:
22.72 \begin{verbatim}
22.73 val {scr = Prog t,...} =
22.74 - get_met ["simplification",
22.75 + Method.from_store ["simplification",
22.76 "of_rationals",
22.77 "to_partial_fraction"];
22.78 atomty_thy @{theory "Inverse_Z_Transform"} t ;
23.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Tue May 12 16:22:00 2020 +0200
23.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Tue May 12 17:42:29 2020 +0200
23.3 @@ -1002,7 +1002,7 @@
23.4 the original \emph{srls}.\\
23.5
23.6 \begin{verbatim}
23.7 - val {srls,...} = get_met ["SignalProcessing",
23.8 + val {srls,...} = Method.from_store ["SignalProcessing",
23.9 "Z_Transform",
23.10 "Inverse"];
23.11 \end{verbatim}
23.12 @@ -2391,7 +2391,7 @@
23.13 arguments in the arguments\ldots
23.14 \begin{verbatim}
23.15 val Prog s =
23.16 - (#scr o get_met) ["SignalProcessing",
23.17 + (#scr o Method.from_store) ["SignalProcessing",
23.18 "Z_Transform",
23.19 "Inverse"];
23.20 writeln (UnparseC.term s);
23.21 @@ -2698,7 +2698,7 @@
23.22 parse-tree of the program with {\sisac}'s specific debug tools:
23.23 \begin{verbatim}
23.24 val {scr = Prog t,...} =
23.25 - get_met ["simplification",
23.26 + Method.from_store ["simplification",
23.27 "of_rationals",
23.28 "to_partial_fraction"];
23.29 atomty_thy @ { theory } t ;
24.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Tue May 12 16:22:00 2020 +0200
24.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Tue May 12 17:42:29 2020 +0200
24.3 @@ -30,7 +30,7 @@
24.4 the function 'get_pbt' gets the one we need:
24.5 \<close>
24.6 ML \<open>Specify.show_ptyps ();
24.7 - Specify.get_pbt ["plus_minus", "polynom", "vereinfachen"];
24.8 + Problem.from_store ["plus_minus", "polynom", "vereinfachen"];
24.9 \<close>
24.10 text \<open>However, 'get_pbt' shows an internal format; for a human readable format
24.11 see http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index_pbl.html
24.12 @@ -43,7 +43,7 @@
24.13 \<close>
24.14 ML \<open>
24.15 Specify.show_mets ();
24.16 -Specify.get_met ["simplification","for_polynomials","with_minus"];
24.17 +Method.from_store ["simplification","for_polynomials","with_minus"];
24.18 \<close>
24.19 text \<open>For a readable format of the method look up the definition in
24.20 ~~/Tools/isac/Knowledge/PolyMinus.thy or
25.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Tue May 12 16:22:00 2020 +0200
25.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Tue May 12 17:42:29 2020 +0200
25.3 @@ -230,7 +230,7 @@
25.4 "~~~~~ fun by_tactic , args:"; val ((Tactic.Check_Postcond' (pI, res)), (sub_ist, sub_ctxt), (pt, pos as (p, _)))
25.5 = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp);
25.6 val parent_pos = par_pblobj pt p
25.7 - val {scr, ...} = Specify.get_met (get_obj g_metID pt parent_pos);
25.8 + val {scr, ...} = Method.from_store (get_obj g_metID pt parent_pos);
25.9 val prog_res =
25.10 case LI.find_next_step scr (pt, pos) sub_ist sub_ctxt of
25.11 (*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
26.1 --- a/test/Tools/isac/BaseDefinitions/substitution.sml Tue May 12 16:22:00 2020 +0200
26.2 +++ b/test/Tools/isac/BaseDefinitions/substitution.sml Tue May 12 17:42:29 2020 +0200
26.3 @@ -96,7 +96,7 @@
26.4 "-------- build fun for_bdv --------------------------------------------------";
26.5 Subst.program_to_input: Subst.program -> string list;
26.6
26.7 -val {scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"];
26.8 +val {scr = Prog prog, ...} = Method.from_store ["diff", "differentiate_on_R"];
26.9 val env = [(str2term "v_v", str2term "x")] : Subst.T;
26.10
26.11 "~~~~~ fun for_bdv, args:"; val (prog, env) = (prog, env);
27.1 --- a/test/Tools/isac/BridgeLibisabelle/datatypes.sml Tue May 12 16:22:00 2020 +0200
27.2 +++ b/test/Tools/isac/BridgeLibisabelle/datatypes.sml Tue May 12 17:42:29 2020 +0200
27.3 @@ -30,19 +30,19 @@
27.4 val thyID = "Test";
27.5
27.6 (*========== inhibit exn AK110725 ================================================
27.7 -val thydata = get_the ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"];
27.8 +val thydata = Thy_Read.from_store ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"];
27.9 (*AK110725
27.10 -(*val thydata = get_the ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"];
27.11 - (* ERROR: get_pbt not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)
27.12 -"~~~~~ fun get_the, args:"; val (theID:theID) = (["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]);
27.13 +(*val thydata = Thy_Read.from_store ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"];
27.14 + (* ERROR: Problem.from_store not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)
27.15 +"~~~~~ fun Thy_Read.from_store, args:"; val (theID:theID) = (["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]);
27.16 (*get_py (ThyC.get_theory "Pure") theID theID (get_thes ());
27.17 - (* ERROR: get_pbt not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)
27.18 + (* ERROR: Problem.from_store not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)
27.19 (*default_print_depth 3; 999*)
27.20 (get_thes ());
27.21
27.22 (*"~~~~~ fun get_py, args:"; val (thy, d, _, []) = ((ThyC.get_theory "Pure"), theID, theID, (get_thes ()));*)
27.23 "~~~~~ fun get_py, args:"; val (thy, d, _, [_]) = ((ThyC.get_theory "Pure"), theID, theID, (get_thes ()));
27.24 -error ("get_pbt not found: "^(strs2str d));
27.25 +error ("Problem.from_store not found: "^(strs2str d));
27.26 (*AK110725 To be continued...s*)
27.27 *)
27.28
27.29 @@ -61,7 +61,7 @@
27.30
27.31 show_thes();
27.32 val theID = ["IsacKnowledge", "Diff", "Theorems", "frac_conv"];
27.33 -val thydata = get_the theID;
27.34 +val thydata = Thy_Read.from_store theID;
27.35 val Hthm {guh=guh, thm=thm, mathauthors=ma, coursedesign=co} = thydata;
27.36 writeln(thydata2xml (theID, thydata));
27.37 "----- check 'manually' ...0 < ?n |] ==> ?a... -----";
28.1 --- a/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue May 12 16:22:00 2020 +0200
28.2 +++ b/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue May 12 17:42:29 2020 +0200
28.3 @@ -39,7 +39,7 @@
28.4 Exception- OPTION raised
28.5 *)
28.6
28.7 -if Pbl_Met_Hierarchy.pbl2xml ["Biegelinien"] (get_pbt ["Biegelinien"]) =
28.8 +if Pbl_Met_Hierarchy.pbl2xml ["Biegelinien"] (Problem.from_store ["Biegelinien"]) =
28.9 "<NODECONTENT>\n"^
28.10 " <GUH> pbl_bieg </GUH>\n"^
28.11 " <STRINGLIST>\n"^
28.12 @@ -94,7 +94,7 @@
28.13 then () else error "fun pbl2xml 'Biegelinien' changed";
28.14
28.15 (* val id = ["Biegelinie"];
28.16 - val {(*guh,*)cas,met,ppc,prls,thy,where_} = get_pbt ["Biegelinie"];
28.17 + val {(*guh,*)cas,met,ppc,prls,thy,where_} = Problem.from_store ["Biegelinie"];
28.18 AND STEP THROUGH pbl2xml ...
28.19
28.20 term2xml i (pbl2term thy id);
28.21 @@ -166,7 +166,7 @@
28.22
28.23 insert_errpats ["diff","differentiate_on_R"] errpatstest;
28.24
28.25 -val {errpats, ...} = get_met ["diff","differentiate_on_R"];
28.26 +val {errpats, ...} = Method.from_store ["diff","differentiate_on_R"];
28.27 case errpats of
28.28 ("chain-rule-diff-both", _, _) :: _ => ()
28.29 | _ => error "insert_errpats chain-rule-diff-both changed";
29.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue May 12 16:22:00 2020 +0200
29.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue May 12 17:42:29 2020 +0200
29.3 @@ -65,7 +65,7 @@
29.4 \Exception- Match raised\n";
29.5 ;
29.6 val theID = ["IsacKnowledge","Integrate","Rulesets","add_new_c"];
29.7 -val thydata = get_the theID;
29.8 +val thydata = Thy_Read.from_store theID;
29.9 ;
29.10 (* HERE WE DO NOT create a file ...
29.11 thydata2file "/tmp/" [] theID thydata (*reports Exception- Match in question*);
29.12 @@ -140,7 +140,7 @@
29.13 "----------- thes2file: thy_containing_rls : rls '...' not in ! --";
29.14 "----------- thes2file: thy_containing_rls : rls '...' not in ! --";
29.15 val theID = ["IsacKnowledge","Rational","Rulesets","norm_Rational_parenthesized"]
29.16 -val thydata = get_the theID
29.17 +val thydata = Thy_Read.from_store theID
29.18 ;
29.19 thydata2xml (theID, thydata);
29.20
29.21 @@ -217,7 +217,7 @@
29.22 "----------- repair thydata2xml for rls --------------------------";
29.23 "----------- repair thydata2xml for rls --------------------------";
29.24 val theID = ["IsacKnowledge", "Poly", "Rulesets", "expand"]
29.25 -val hrls = get_the theID
29.26 +val hrls = Thy_Read.from_store theID
29.27 ;
29.28 if thydata2xml (theID, hrls) = (
29.29 "<RULESETDATA>\n" ^
30.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Tue May 12 16:22:00 2020 +0200
30.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Tue May 12 17:42:29 2020 +0200
30.3 @@ -47,9 +47,9 @@
30.4 "--------- appendFormula: on Res + equ_nrls ----------------------";
30.5 "--------- appendFormula: on Res + equ_nrls ----------------------";
30.6 "--------- appendFormula: on Res + equ_nrls ----------------------";
30.7 - val Prog sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
30.8 + val Prog sc = (#scr o Method.from_store) ["Test","squ-equ-test-subpbl1"];
30.9 (writeln o UnparseC.term) sc;
30.10 - val Prog sc = (#scr o get_met) ["Test","solve_linear"];
30.11 + val Prog sc = (#scr o Method.from_store) ["Test","solve_linear"];
30.12 (writeln o UnparseC.term) sc;
30.13
30.14 reset_states ();
30.15 @@ -984,7 +984,7 @@
30.16 val (res, inf) =
30.17 (str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",
30.18 str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
30.19 -val {errpats, nrls = rls, scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"]
30.20 +val {errpats, nrls = rls, scr = Prog prog, ...} = Method.from_store ["diff", "differentiate_on_R"]
30.21
30.22 val env = [(str2term "v_v", str2term "x")];
30.23 val errpats =
30.24 @@ -1032,16 +1032,16 @@
30.25 (*if*) f_pred = f_in; (*else*)
30.26 val NONE = (*case*) In_Chead.cas_input f_in (*of*);
30.27 (*old* )val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
30.28 - (*old*)val {scr = prog, ...} = Specify.get_met metID
30.29 + (*old*)val {scr = prog, ...} = Method.from_store metID
30.30 (*old*)val istate = get_istate_LI pt pos
30.31 (*old*)val ctxt = get_ctxt pt pos
30.32 ( *old*)
30.33 val LI.Not_Derivable =
30.34 (*case*) LI.locate_input_term (pt, pos) f_in (*of*);
30.35 val pp = Ctree.par_pblobj pt p
30.36 - val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
30.37 + val (errpats, nrls, prog) = case Method.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
30.38 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
30.39 - | _ => error "inform: uncovered case of get_met"
30.40 + | _ => error "inform: uncovered case of Method.from_store"
30.41 ;
30.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 ^^^ ?n) = ?n * ?u ^^^ (?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 ^^^ ?n) = ?n * ?u ^^^ (?n - 1) * d_d ?bdv ?u\",\"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\",\"d_d ?bdv (E_ ^^^ ?u) = E_ ^^^ ?u * d_d ?x ?u\"]]"
30.43 (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3";
30.44 @@ -1084,9 +1084,9 @@
30.45 "~~~~~ fun find_fill_patterns , args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
30.46 val f_curr = Ctree.get_curr_formula (pt, pos);
30.47 val pp = Ctree.par_pblobj pt p
30.48 - val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
30.49 + val (errpats, prog) = case Method.from_store (Ctree.get_obj Ctree.g_metID pt pp) of
30.50 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
30.51 - | _ => error "find_fill_patterns: uncovered case of get_met"
30.52 + | _ => error "find_fill_patterns: uncovered case of Method.from_store"
30.53 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
30.54 val subst = Subst.for_bdv prog env
30.55 val errpatthms = errpats
30.56 @@ -1105,7 +1105,7 @@
30.57 val thmDeriv = Thm.get_name_hint thm
30.58 val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv
30.59 val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
30.60 - val Thy_Write.Hthm {fillpats, ...} = get_the theID
30.61 + val Thy_Write.Hthm {fillpats, ...} = Thy_Read.from_store theID
30.62 val some = map (Error_Pattern.fill_form subst (thm, form) errpatID) fillpats;
30.63
30.64 case some |> filter is_some |> map the of
30.65 @@ -1251,7 +1251,7 @@
30.66 *)
30.67 (* val (dI, oris, ppc, pbt, (selct::ss))=
30.68 (#1 (some_spec ospec spec), oris, []:I_Model.T,
30.69 - ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
30.70 + ((#ppc o Problem.from_store) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
30.71 val iii = appl_adds dI oris ppc pbt (selct::ss);
30.72 tracing(I_Model.to_string thy iii);
30.73
31.1 --- a/test/Tools/isac/Interpret/li-tool.sml Tue May 12 16:22:00 2020 +0200
31.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Tue May 12 17:42:29 2020 +0200
31.3 @@ -41,7 +41,7 @@
31.4 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = (m, ptp);
31.5 "~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,ctxt), pos as (p,_))
31.6 = (m, pos);
31.7 -val {srls, ...} = get_met mI;
31.8 +val {srls, ...} = Method.from_store mI;
31.9 val PblObj {meth=itms, ...} = get_obj I pt p;
31.10 val thy' = get_obj g_domID pt p;
31.11 val thy = ThyC.get_theory thy';
31.12 @@ -138,7 +138,7 @@
31.13 if metID = Method.id_empty
31.14 then (thd3 o snd3) (get_obj g_origin pt pp)
31.15 else metID
31.16 - val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
31.17 + val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = Method.from_store metID'
31.18 val Pstate ist = get_istate_LI pt (p,p_)
31.19 val ctxt = get_ctxt pt (p, p_)
31.20 val alltacs = (*we expect at least 1 stac in a script*)
32.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Tue May 12 16:22:00 2020 +0200
32.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Tue May 12 17:42:29 2020 +0200
32.3 @@ -43,7 +43,7 @@
32.4
32.5 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
32.6 = (m, (pt, pos));
32.7 - val {srls, ...} = get_met mI;
32.8 + val {srls, ...} = Method.from_store mI;
32.9 val itms = case get_obj I pt p of
32.10 PblObj {meth=itms, ...} => itms
32.11 | _ => error "solve Apply_Method: uncovered case get_obj"
32.12 @@ -545,7 +545,7 @@
32.13 (*case*) In_Chead.cas_input f_in (*of*);
32.14
32.15 (*old* ) val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
32.16 -(*old*) val {scr = prog, ...} = Specify.get_met metID
32.17 +(*old*) val {scr = prog, ...} = Method.from_store metID
32.18 (*old*) val istate = get_istate_LI pt pos
32.19 (*old*) val ctxt = get_ctxt pt pos
32.20 val LI.Found_Step (cstate'''''_', _(*istate*), _(*ctxt*)) = (*case*)
33.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Tue May 12 16:22:00 2020 +0200
33.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Tue May 12 17:42:29 2020 +0200
33.3 @@ -152,7 +152,7 @@
33.4 Step_Solve.by_tactic m (pt, pos);
33.5 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Tactic.Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p, _))))
33.6 = (m, (pt, pos));
33.7 -val {srls, ...} = Specify.get_met mI;
33.8 +val {srls, ...} = Method.from_store mI;
33.9 val itms = case get_obj I pt p of
33.10 PblObj {meth=itms, ...} => itms
33.11 | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case get_obj"
33.12 @@ -235,7 +235,7 @@
33.13 val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
33.14 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
33.15 (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
33.16 - val {ppc, pre, prls,...} = Specify.get_met mID
33.17 + val {ppc, pre, prls,...} = Method.from_store mID
33.18 val thy = ThyC.get_theory dI
33.19 val dI'' = if dI = ThyC.id_empty then dI' else dI
33.20 val pI'' = if pI = Problem.id_empty then pI' else pI
33.21 @@ -250,7 +250,7 @@
33.22 ","(#Given, (Biegelinie, id_fun))
33.23 ","(#Given, (AbleitungBiegelinie, id_abl))
33.24 ","(#Find, (Funktionen, fun_s))"]*)
33.25 -(*+*)writeln (Model_Pattern.to_string' ((#ppc o Specify.get_pbt) pI));
33.26 +(*+*)writeln (Model_Pattern.to_string' ((#ppc o Problem.from_store) pI));
33.27 (*["(#Given, (Streckenlast, q_q))
33.28 ","(#Given, (FunktionsVariable, v_v))
33.29 ","(#Find, (Funktionen, funs'''))"]*)
34.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Tue May 12 16:22:00 2020 +0200
34.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Tue May 12 17:42:29 2020 +0200
34.3 @@ -20,7 +20,7 @@
34.4 "----------- retrieve errpats ------------------------------------";
34.5 "----------- retrieve errpats ------------------------------------";
34.6 "----------- retrieve errpats ------------------------------------";
34.7 -val {errpats, nrls, scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"];
34.8 +val {errpats, nrls, scr = Prog prog, ...} = Method.from_store ["diff", "differentiate_on_R"];
34.9 case errpats of [("chain-rule-diff-both", _, _)] => ()
34.10 | _ => error "errpats chain-rule-diff-both changed"
34.11
35.1 --- a/test/Tools/isac/Knowledge/diff.sml Tue May 12 16:22:00 2020 +0200
35.2 +++ b/test/Tools/isac/Knowledge/diff.sml Tue May 12 17:42:29 2020 +0200
35.3 @@ -42,8 +42,8 @@
35.4 "differentiateFor x","derivative f_f'"];
35.5 val chkorg = map (the o (parse thy)) org;
35.6
35.7 -get_pbt ["derivative_of","function"];
35.8 -get_met ["diff","differentiate_on_R"];
35.9 +Problem.from_store ["derivative_of","function"];
35.10 +Method.from_store ["diff","differentiate_on_R"];
35.11
35.12 "----------- for correction of diff_const ---------------";
35.13 "----------- for correction of diff_const ---------------";
36.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Tue May 12 16:22:00 2020 +0200
36.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Tue May 12 17:42:29 2020 +0200
36.3 @@ -285,7 +285,7 @@
36.4 "~~~~~ fun Refine.refine, args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR","system"]);
36.5 "~~~~~ fun refin', args:"; val ((pblRD: pblRD), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
36.6 ((rev o tl) pblID, fmz, [(*match list*)],
36.7 - ((Store.Node ("LINEAR", [get_pbt ["LINEAR","system"]], [])): Problem.T Store.node));
36.8 + ((Store.Node ("LINEAR", [Problem.from_store ["LINEAR","system"]], [])): Problem.T Store.node));
36.9 val {thy, ppc, where_, prls, ...} = py ;
36.10 "~~~~~ fun O_Model.init, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc);
36.11 val ctxt = Proof_Context.init_global thy;
36.12 @@ -430,7 +430,7 @@
36.13 (*-----fun refin' (pblRD:pblRD) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
36.14 (* val ((pblRD:pblRD), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
36.15 (rev ["LINEAR","system"], fmz, [(*match list*)],
36.16 - ((Store.Node ("2x2",[get_pbt ["2x2","LINEAR","system"]],[])):pbt Store.store));
36.17 + ((Store.Node ("2x2",[Problem.from_store ["2x2","LINEAR","system"]],[])):pbt Store.store));
36.18 *)
36.19 > show_types:=true; UnparseC.term (hd where_); show_types:=false;
36.20 val it = "length_ (es_::real list) = (2::real)" : string
36.21 @@ -454,7 +454,7 @@
36.22 val it = "es_::bool list" : string
36.23 ~~~~~~~~~~~~~~~^^^^^^^^^ OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
36.24
36.25 -> val {where_,...} = get_pbt ["2x2", "LINEAR","system"];
36.26 +> val {where_,...} = Problem.from_store ["2x2", "LINEAR","system"];
36.27 > show_types:=true; UnparseC.term (hd where_); show_types:=false;
36.28
36.29 =========================================================================/
37.1 --- a/test/Tools/isac/Knowledge/integrate.sml Tue May 12 16:22:00 2020 +0200
37.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Tue May 12 17:42:29 2020 +0200
37.3 @@ -348,10 +348,10 @@
37.4 | _ => error "integrate.sml: Integrate.antiDerivativeName";
37.5
37.6 "----- compare 'Find's from problem, script, formalization -------";
37.7 -val {ppc,...} = get_pbt ["named","integrate","function"];
37.8 +val {ppc,...} = Problem.from_store ["named","integrate","function"];
37.9 val ("#Find", (Const ("Integrate.antiDerivativeName", _),
37.10 F1_ as Free ("F_F", F1_type))) = last_elem ppc;
37.11 -val {scr = Prog sc,... } = get_met ["diff","integration","named"];
37.12 +val {scr = Prog sc,... } = Method.from_store ["diff","integration","named"];
37.13 val [_,_, F2_] = formal_args sc;
37.14 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
37.15
37.16 @@ -362,7 +362,7 @@
37.17 else error "integrate.sml: unequal types in find's";
37.18
37.19 show_ptyps();
37.20 -val pbl = get_pbt ["integrate","function"];
37.21 +val pbl = Problem.from_store ["integrate","function"];
37.22 case #cas pbl of SOME (Const ("Integrate.Integrate",_) $ _) => ()
37.23 | _ => error "integrate.sml: Integrate.Integrate ???";
37.24
38.1 --- a/test/Tools/isac/Knowledge/inverse_z_transform.sml Tue May 12 16:22:00 2020 +0200
38.2 +++ b/test/Tools/isac/Knowledge/inverse_z_transform.sml Tue May 12 17:42:29 2020 +0200
38.3 @@ -15,8 +15,8 @@
38.4 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
38.5 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
38.6 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
38.7 -get_pbt ["Inverse","Z_Transform","SignalProcessing"];
38.8 -get_met ["SignalProcessing","Z_Transform","Inverse"];
38.9 +Problem.from_store ["Inverse","Z_Transform","SignalProcessing"];
38.10 +Method.from_store ["SignalProcessing","Z_Transform","Inverse"];
38.11
38.12 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
38.13 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
39.1 --- a/test/Tools/isac/Knowledge/poly.sml Tue May 12 16:22:00 2020 +0200
39.2 +++ b/test/Tools/isac/Knowledge/poly.sml Tue May 12 17:42:29 2020 +0200
39.3 @@ -571,7 +571,7 @@
39.4
39.5 "-----1 ---";
39.6 (*default_print_depth 7;*)
39.7 -val pbt = get_pbt ["polynomial","simplification"];
39.8 +val pbt = Problem.from_store ["polynomial","simplification"];
39.9 (*default_print_depth 3;*)
39.10 (*if there is ...
39.11 > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
39.12 @@ -585,7 +585,7 @@
39.13
39.14 "-----3 ---";
39.15 (*default_print_depth 7;*)
39.16 -val prls = (#prls o get_pbt) ["polynomial","simplification"];
39.17 +val prls = (#prls o Problem.from_store) ["polynomial","simplification"];
39.18 (*default_print_depth 3;*)
39.19 val t = str2term "((5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)) is_polyexp";
39.20 val SOME (t',_) = rewrite_set_ thy false prls t;
40.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Tue May 12 16:22:00 2020 +0200
40.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Tue May 12 17:42:29 2020 +0200
40.3 @@ -109,7 +109,7 @@
40.4 "----------- test matching problems --------------------------0---";
40.5 "----------- test matching problems --------------------------0---";
40.6 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
40.7 -if match_pbl fmz (get_pbt ["expanded","univariate","equation"]) =
40.8 +if match_pbl fmz (Problem.from_store ["expanded","univariate","equation"]) =
40.9 Matches' {Find = [Correct "solutions L"],
40.10 With = [],
40.11 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
40.12 @@ -118,7 +118,7 @@
40.13 Relate = []}
40.14 then () else error "match_pbl [expanded,univariate,equation]";
40.15
40.16 -if match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]) =
40.17 +if match_pbl fmz (Problem.from_store ["degree_2","expanded","univariate","equation"]) =
40.18 Matches' {Find = [Correct "solutions L"],
40.19 With = [],
40.20 Given = [Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)", Correct "solveFor x"],
41.1 --- a/test/Tools/isac/Knowledge/rateq.sml Tue May 12 16:22:00 2020 +0200
41.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Tue May 12 17:42:29 2020 +0200
41.3 @@ -41,11 +41,11 @@
41.4 if result <> "True" then error "rateq.sml: new behaviour 4:" else ();
41.5
41.6 val result = match_pbl ["equality (x=(1::real))","solveFor x","solutions L"]
41.7 - (get_pbt ["rational","univariate","equation"]);
41.8 + (Problem.from_store ["rational","univariate","equation"]);
41.9 case result of NoMatch' _ => () | _ => error "rateq.sml: new behaviour: 5";
41.10
41.11 val result = match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"]
41.12 - (get_pbt ["rational","univariate","equation"]);
41.13 + (Problem.from_store ["rational","univariate","equation"]);
41.14 case result of Matches' _ => () | _ => error "rateq.sml: new behaviour: 6";
41.15
41.16 "------------ solve (1/x = 5, x) by me ---------------------------";
41.17 @@ -139,7 +139,7 @@
41.18 val thy' = (get_obj g_domID pt pp):theory';
41.19 val thy = ThyC.get_theory thy'
41.20 val metID = (get_obj g_metID pt pp)
41.21 - val {crls,...} = get_met metID
41.22 + val {crls,...} = Method.from_store metID
41.23 val (f,asm) = case p_ of Frm => (get_obj g_form pt p , [])
41.24 | Res => get_obj g_result pt p;
41.25 UnparseC.term f = "[x = 1 / 5]"; (*the current formula*)
42.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Tue May 12 16:22:00 2020 +0200
42.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Tue May 12 17:42:29 2020 +0200
42.3 @@ -85,11 +85,11 @@
42.4
42.5
42.6 val result = match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"]
42.7 - (get_pbt ["rootX","univariate","equation"]);
42.8 + (Problem.from_store ["rootX","univariate","equation"]);
42.9 case result of Matches' _ => () | _ => error "rooteq.sml: new behaviour:";
42.10
42.11 val result = match_pbl ["equality (sqrt(25)=1)","solveFor x","solutions L"]
42.12 - (get_pbt ["rootX","univariate","equation"]);
42.13 + (Problem.from_store ["rootX","univariate","equation"]);
42.14 case result of NoMatch' _ => () | _ => error "rooteq.sml: new behaviour:";
42.15
42.16 (*---------rooteq---- 23.8.02 ---------------------*)
42.17 @@ -548,7 +548,7 @@
42.18 val (dI',pI',mI') =
42.19 ("Test",["sqroot-test","univariate","equation","test"],
42.20 ["Test","square_equation2"]);
42.21 -val Prog sc = (#scr o get_met) ["Test","square_equation2"];
42.22 +val Prog sc = (#scr o Method.from_store) ["Test","square_equation2"];
42.23 (writeln o UnparseC.term) sc;
42.24
42.25 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
42.26 @@ -614,7 +614,7 @@
42.27
42.28
42.29
42.30 -val Prog s = (#scr o get_met) ["Test","square_equation"];
42.31 +val Prog s = (#scr o Method.from_store) ["Test","square_equation"];
42.32 atomt s;
42.33
42.34
42.35 @@ -685,7 +685,7 @@
42.36 val (dI',pI',mI') =
42.37 ("Test",["squareroot","univariate","equation","test"],
42.38 ["Test","square_equation"]);
42.39 - val Prog sc = (#scr o get_met) ["Test","square_equation"];
42.40 + val Prog sc = (#scr o Method.from_store) ["Test","square_equation"];
42.41 (writeln o UnparseC.term) sc;
42.42
42.43 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
42.44 @@ -778,6 +778,6 @@
42.45
42.46
42.47 Refine.refine fmz ["univariate","equation","test"];
42.48 -match_pbl fmz (get_pbt ["polynomial","univariate","equation","test"]);
42.49 +match_pbl fmz (Problem.from_store ["polynomial","univariate","equation","test"]);
42.50
42.51 ===== copied here from OLDTESTS in case there is a Program ===^^^=============================*)
43.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Tue May 12 16:22:00 2020 +0200
43.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Tue May 12 17:42:29 2020 +0200
43.3 @@ -769,7 +769,7 @@
43.4 fun pt_form (PrfObj {form,...}) = UnparseC.term form
43.5 | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
43.6 let val (dI, pI, _) = get_somespec' spec spec'
43.7 - val {cas,...} = get_pbt pI
43.8 + val {cas,...} = Problem.from_store pI
43.9 in case cas of
43.10 NONE => UnparseC.term (pblterm dI pI)
43.11 | SOME t => UnparseC.term (subst_atomic (mk_env probl) t)
44.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Tue May 12 16:22:00 2020 +0200
44.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Tue May 12 17:42:29 2020 +0200
44.3 @@ -60,11 +60,11 @@
44.4 just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false=oldNB*)
44.5 val cpI = if pI = Problem.id_empty then pI' else pI;
44.6 val cmI = if mI = e_metID then mI' else mI;
44.7 - val {ppc, prls, where_, ...} = get_pbt cpI;
44.8 + val {ppc, prls, where_, ...} = Problem.from_store cpI;
44.9 val pre = Pre_Conds.check' "thy 100820" prls where_ probl;
44.10 val pb = foldl and_ (true, map fst pre);
44.11 val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
44.12 - (ppc, (#ppc o get_met) cmI) (dI, pI, mI); (*tac = Add_Given "equality (-1 + x = 0)"*)
44.13 + (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI); (*tac = Add_Given "equality (-1 + x = 0)"*)
44.14 "~~~~~ fun Step_Specify.by_tactic_input, args:"; val (Add_Given ct, ptp) = (tac, ptp);
44.15 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
44.16 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
44.17 @@ -72,7 +72,7 @@
44.18 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
44.19 val cpI = if pI = Problem.id_empty then pI' else pI;
44.20 val ctxt = get_ctxt pt (p, Pbl);
44.21 -"~~~~~ fun add_single, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct);
44.22 +"~~~~~ fun add_single, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o Problem.from_store) cpI), ct);
44.23 val SOME t = parseNEW ctxt str;
44.24 is_known ctxt sel oris t;
44.25 "~~~~~ fun is_known, args:"; val (ctxt, sel, ori, t) = (ctxt, sel, oris, t);
44.26 @@ -84,7 +84,7 @@
44.27 (*if Input_Descript.is_a d then () else error "TODO";*)
44.28 if Input_Descript.is_a d then () else error "TODO";
44.29 "----- these were the errors (call hierarchy from bottom up)";
44.30 -I_Model.check_single ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct;(*WAS
44.31 +I_Model.check_single ctxt sel oris pbl ((#ppc o Problem.from_store) cpI) ct;(*WAS
44.32 Err "[error] add_single: is_known: identifiers [equality] not in example"*)
44.33 nxt_specif_additem "#Given" ct ptp;(*WAS
44.34 Tac "[error] add_single: is_known: identifiers [equality] not in example"*)
44.35 @@ -248,7 +248,7 @@
44.36 "----------- fun upds_envv ---------------------------------------------------------------------";
44.37 (* eval test-maximum.sml until Specify_Method ...
44.38 val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt [];
44.39 - val met = (#ppc o get_met) mI;
44.40 + val met = (#ppc o Method.from_store) mI;
44.41
44.42 val envv = [];
44.43 val eargs = flat eargs;
45.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue May 12 16:22:00 2020 +0200
45.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue May 12 17:42:29 2020 +0200
45.3 @@ -148,9 +148,9 @@
45.4 "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
45.5 val thy = ThyC.get_theory dI;
45.6 mI = ["no_met"]; (*false*)
45.7 - val pors = Specify.get_pbt pI |> #ppc |> O_Model.init fmz thy;
45.8 + val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy;
45.9 val pctxt = ContextC.initialise' thy fmz;
45.10 - val {cas, ppc, thy=thy',...} = get_pbt pI; (*take dI from _refined_ pbl*)
45.11 + val {cas, ppc, thy=thy',...} = Problem.from_store pI; (*take dI from _refined_ pbl*)
45.12 "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
45.13 val dI = Context.theory_name (ThyC.parent_of thy thy');
45.14 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
45.15 @@ -347,7 +347,7 @@
45.16 Frm => get_obj g_form pt p
45.17 | Res => (fst o (get_obj g_result pt)) p
45.18 | _ => TermC.empty (*on PblObj is fo <> ifo*);
45.19 - val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
45.20 + val {nrls, ...} = Method.from_store (get_obj g_metID pt (par_pblobj pt p))
45.21 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls;
45.22 (*val (found, der) = *)Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
45.23 "~~~~~ fun .concat_deriv, args:"; val (rew_ord, erls, rules, fo, ifo) =
46.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Tue May 12 16:22:00 2020 +0200
46.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Tue May 12 17:42:29 2020 +0200
46.3 @@ -14,9 +14,9 @@
46.4 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz : Formalise.model, (dI, pI, mI) : Spec.T) = (fmz, sp);
46.5 val thy = ThyC.get_theory dI;
46.6 (*if*) mI = ["no_met"]; (*else*)
46.7 - val pors = Specify.get_pbt pI |> #ppc |> O_Model.init fmz thy;
46.8 + val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy;
46.9 val pctxt = ContextC.initialise' thy fmz;
46.10 - val {cas, ppc, thy=thy',...} = get_pbt pI
46.11 + val {cas, ppc, thy=thy',...} = Problem.from_store pI
46.12 val dI = Context.theory_name (ThyC.parent_of thy thy');
46.13 val hdl =
46.14 case cas of SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ O_Model.values pors) t
46.15 @@ -43,7 +43,7 @@
46.16 "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
46.17 val thy = ThyC.get_theory dI;
46.18 (*if*) mI = ["no_met"] = false (*else*);
46.19 -val xxx = Specify.get_pbt pI
46.20 +val xxx = Problem.from_store pI
46.21 val yyy = #ppc xxx
46.22 val oris = O_Model.init fmz thy yyy
46.23 ;
47.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Tue May 12 16:22:00 2020 +0200
47.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Tue May 12 17:42:29 2020 +0200
47.3 @@ -34,17 +34,17 @@
47.4 just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (* = false*)
47.5 val cpI = if pI = Problem.id_empty then pI' else pI;
47.6 val cmI = if mI = Method.id_empty then mI' else mI;
47.7 - val {ppc, prls, where_, ...} = get_pbt cpI;
47.8 + val {ppc, prls, where_, ...} = Problem.from_store cpI;
47.9 val pre = Pre_Conds.check' "thy 100820" prls where_ probl;
47.10 val pb = foldl and_ (true, map fst pre);
47.11
47.12 (* val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
47.13 - (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
47.14 + (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI);
47.15 ERROR: val tac = Add_Given "equality (<markup> + <markup> = <markup>)"*)
47.16 "~~~~~ fun nxt_spec, args:"; val (Pbl, preok, (oris : O_Model.T), ((dI', pI', mI') : Spec.T),
47.17 ((pbl : I_Model.T), (met : I_Model.T)), (pbt, mpc), ((dI, pI, mI) : Spec.T)) =
47.18 (p_, pb, oris, (dI',pI',mI'), (probl, meth),
47.19 - (ppc, (#ppc o get_met) cmI), (dI, pI, mI));
47.20 + (ppc, (#ppc o Method.from_store) cmI), (dI, pI, mI));
47.21
47.22 dI' = ThyC.id_empty andalso dI = ThyC.id_empty; (* = false*)
47.23 pI' = Problem.id_empty andalso pI = Problem.id_empty; (* = false*)
48.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Tue May 12 16:22:00 2020 +0200
48.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Tue May 12 17:42:29 2020 +0200
48.3 @@ -44,7 +44,7 @@
48.4 (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*);
48.5 val cpI = if pI = Problem.id_empty then pI' else pI;
48.6 val cmI = if mI = Method.id_empty then mI' else mI;
48.7 - val {ppc = pbt, prls, where_, ...} = Specify.get_pbt cpI;
48.8 + val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;
48.9
48.10 (*+* )------- in f3cac3053e7b (Rule_Set.empty just renamed, NOT deleted) we had
48.11 (*+*) prls =
49.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Tue May 12 16:22:00 2020 +0200
49.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Tue May 12 17:42:29 2020 +0200
49.3 @@ -66,7 +66,7 @@
49.4 val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
49.5 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
49.6 | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj"
49.7 - val {ppc, ...} = Specify.get_met mI;
49.8 + val {ppc, ...} = Method.from_store mI;
49.9 val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
49.10 val itms = Specify.hack_until_review_Specify_1 mI itms
49.11 val srls = LItool.get_simplifier (pt, pos)
50.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue May 12 16:22:00 2020 +0200
50.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue May 12 17:42:29 2020 +0200
50.3 @@ -217,11 +217,11 @@
50.4 val ags = TermC.isalist2list ags';
50.5 (*if*) mI = ["no_met"] (*else*);
50.6 val (pI, pors, mI) =
50.7 - (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
50.8 + (pI, (Chead.match_ags thy ((#ppc o Problem.from_store) pI) ags)
50.9 handle ERROR "actual args do not match formal args"
50.10 => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI)
50.11 val (fmz_, vals) = Chead.oris2fmz_vals pors;
50.12 - val {cas,ppc,thy,...} = Specify.get_pbt pI
50.13 + val {cas,ppc,thy,...} = Problem.from_store pI
50.14 val dI = Context.theory_name thy (*.take dI from _refined_ pbl.*)
50.15 val dI = Context.theory_name (ThyC.sub_common (ThyC.get_theory dI, rootthy pt));
50.16 val ctxt = ContextC.initialise dI (map TermC.vars vals |> flat |> Library.distinct op =);
51.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Tue May 12 16:22:00 2020 +0200
51.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Tue May 12 17:42:29 2020 +0200
51.3 @@ -37,11 +37,11 @@
51.4 (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*);
51.5 val cpI = if pI = Problem.id_empty then pI' else pI;
51.6 val cmI = if mI = Method.id_empty then mI' else mI;
51.7 - val {ppc, prls, where_, ...} = Specify.get_pbt cpI;
51.8 + val {ppc, prls, where_, ...} = Problem.from_store cpI;
51.9 val pre = Pre_Conds.check' "thy 100820" prls where_ probl;
51.10 val pb = foldl and_ (true, map fst pre);
51.11 val (_, tac) =
51.12 - Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
51.13 + Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI)
51.14 val ist_ctxt = get_loc pt (p, p_)
51.15
51.16 val Apply_Method mI = (*case*) tac (*of*);
51.17 @@ -49,7 +49,7 @@
51.18 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt ptp;
51.19 "~~~~~ fun begin_end_prog , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (ist, ctxt), (pt, pos as (p, _)))
51.20 = ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, ptp);
51.21 - val {ppc, ...} = Specify.get_met mI;
51.22 + val {ppc, ...} = Method.from_store mI;
51.23 val (itms, oris, probl) = case get_obj I pt p of
51.24 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
51.25 | _ => error "begin_end_prog Apply_Method': uncovered case get_obj"
52.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Tue May 12 16:22:00 2020 +0200
52.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Tue May 12 17:42:29 2020 +0200
52.3 @@ -56,7 +56,7 @@
52.4 "~~~~~ fun by_tactic , args:"; val ((Check_Postcond' (pI, _)), (sub_ist, sub_ctxt), (pt, pos as (p,_))) =
52.5 (tac, (ist, ctxt), ptp);
52.6 val parent_pos = par_pblobj pt p
52.7 - val {scr, ...} = Specify.get_met (get_obj g_metID pt parent_pos);
52.8 + val {scr, ...} = Method.from_store (get_obj g_metID pt parent_pos);
52.9 val prog_res =
52.10 case LI.find_next_step scr (pt, pos) sub_ist sub_ctxt of
52.11 (*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
53.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Tue May 12 16:22:00 2020 +0200
53.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Tue May 12 17:42:29 2020 +0200
53.3 @@ -112,7 +112,7 @@
53.4 (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
53.5 "~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = (([], [], (pt, pos_pred)), tm);
53.6 val fo = Calc.current_formula ptp
53.7 - val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
53.8 + val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
53.9 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
53.10 val (found, der) = Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
53.11 (*if*) found (*then*);
53.12 @@ -130,7 +130,7 @@
53.13 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
53.14 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
53.15 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
53.16 - val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
53.17 + val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
53.18 val (pt, c, pos as (p, _)) =
53.19
53.20 Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res));
54.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Tue May 12 16:22:00 2020 +0200
54.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Tue May 12 17:42:29 2020 +0200
54.3 @@ -258,7 +258,7 @@
54.4 val ct = str2term"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
54.5 val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::real","0"];
54.6 val oris = O_Model.init ctl thy
54.7 - ((#ppc o get_pbt)
54.8 + ((#ppc o Problem.from_store)
54.9 ["sqroot-test","univariate","equation","test"]);
54.10 val loc = Istate.empty;
54.11 val (pt,pos) = (e_ctree,[]);
54.12 @@ -551,7 +551,7 @@
54.13 (*solve*)
54.14 val pp = par_pblobj pt p;
54.15 val metID = get_obj g_metID pt pp;
54.16 - val sc = (#scr o get_met) metID;
54.17 + val sc = (#scr o Method.from_store) metID;
54.18 val is = get_istate_LI pt (p,p_);
54.19 val thy' = get_obj g_domID pt pp;
54.20 val thy = ThyC.get_theory thy';
55.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Tue May 12 16:22:00 2020 +0200
55.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Tue May 12 17:42:29 2020 +0200
55.3 @@ -65,7 +65,7 @@
55.4 [("Test","methode")])]
55.5 thy;
55.6
55.7 -match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (get_pbt ["rootX","univariate","equation","test"]);
55.8 +match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (Problem.from_store ["rootX","univariate","equation","test"]);
55.9
55.10 KEStore_Elems.add_pbts
55.11 [prep_pbt (theory "Isac_Knowledge")
56.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Tue May 12 16:22:00 2020 +0200
56.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Tue May 12 17:42:29 2020 +0200
56.3 @@ -118,7 +118,7 @@
56.4 "boolTestFind v_i_"];
56.5 val (dI',pI',mI') = ("Test",["met_testeq","tests"],
56.6 ["Test","testeq1"]);
56.7 -val Prog sc = (#scr o get_met) ["Test","testeq1"];
56.8 +val Prog sc = (#scr o Method.from_store) ["Test","testeq1"];
56.9 atomt sc;
56.10 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
56.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
56.12 @@ -168,7 +168,7 @@
56.13 \ e_e)\
56.14 \in [e_::bool])"
56.15 ));
56.16 -val Prog sc = (#scr o get_met) ["Test","testlet"];
56.17 +val Prog sc = (#scr o Method.from_store) ["Test","testlet"];
56.18 writeln(UnparseC.term sc);
56.19 val fmz = ["boolTestGiven (sqrt a = 0)",
56.20 "boolTestFind v_i_"];
56.21 @@ -200,7 +200,7 @@
56.22 val (dI',pI',mI') =
56.23 ("Test",["sqroot-test","univariate","equation","test"],
56.24 ["Test","sqrt-equ-test"]);
56.25 -val Prog sc = (#scr o get_met) ["Test","sqrt-equ-test"];
56.26 +val Prog sc = (#scr o Method.from_store) ["Test","sqrt-equ-test"];
56.27 writeln(UnparseC.term sc);
56.28
56.29 "--- s1 ---";
56.30 @@ -301,7 +301,7 @@
56.31 val (dI',pI',mI') =
56.32 ("Test",["sqroot-test","univariate","equation","test"],
56.33 ["Test","sqrt-equ-test"]);
56.34 - val Prog sc = (#scr o get_met) ["Test","sqrt-equ-test"];
56.35 + val Prog sc = (#scr o Method.from_store) ["Test","sqrt-equ-test"];
56.36 (writeln o UnparseC.term) sc;
56.37 "--- s1 ---";
56.38 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
57.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Tue May 12 16:22:00 2020 +0200
57.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Tue May 12 17:42:29 2020 +0200
57.3 @@ -275,7 +275,7 @@
57.4 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
57.5 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
57.6 "-------- fun stacpbls, fun eval_leaf -----------------------------------";
57.7 -val {scr, ...} = get_met ["Test","sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
57.8 +val {scr, ...} = Method.from_store ["Test","sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
57.9 case stacpbls sc of
57.10 [Const ("Prog_Tac.Rewrite", _) $ square_equation_left,
57.11 Const ("Prog_Tac.Rewrite'_Set", _) $ Test_simplify,
58.1 --- a/test/Tools/isac/ProgLang/prog_tac.sml Tue May 12 16:22:00 2020 +0200
58.2 +++ b/test/Tools/isac/ProgLang/prog_tac.sml Tue May 12 17:42:29 2020 +0200
58.3 @@ -18,7 +18,7 @@
58.4 "-------- fun eval_leaf -------------------------------------------------------------------";
58.5 "-------- fun eval_leaf -------------------------------------------------------------------";
58.6 "-------- fun eval_leaf -------------------------------------------------------------------";
58.7 -val {scr = Prog sc, ...} = get_met ["Test","sqrt-equ-test"];
58.8 +val {scr = Prog sc, ...} = Method.from_store ["Test","sqrt-equ-test"];
58.9 case eval_leaf [] NONE TermC.empty sc of
58.10 (Expr (Const ("HOL.eq", _) $
58.11 (Const ("Test.solve_root_equ", _) $ Free ("e_e", _) $ Free ("v_v", _)) $
59.1 --- a/test/Tools/isac/ProgLang/tactical.sml Tue May 12 16:22:00 2020 +0200
59.2 +++ b/test/Tools/isac/ProgLang/tactical.sml Tue May 12 17:42:29 2020 +0200
59.3 @@ -17,7 +17,7 @@
59.4 "-------- fun Tactical.is ----------------------------------------------------------------------";
59.5 "-------- fun Tactical.is ----------------------------------------------------------------------";
59.6 "-------- fun Tactical.is ----------------------------------------------------------------------";
59.7 -val {scr = Prog t, ...} = Specify.get_met ["simplification","for_polynomials"];
59.8 +val {scr = Prog t, ...} = Method.from_store ["simplification","for_polynomials"];
59.9
59.10 if Tactical.is (Program.body_of t)
59.11 then error "Tactical.is body_of [simplification,for_polynomials]" else ();
59.12 @@ -25,11 +25,11 @@
59.13 "-------- fun contained_in ---------------------------------------------------------------------";
59.14 "-------- fun contained_in ---------------------------------------------------------------------";
59.15 "-------- fun contained_in ---------------------------------------------------------------------";
59.16 -val {scr = Prog t, ...} = Specify.get_met ["simplification","for_polynomials"];
59.17 +val {scr = Prog t, ...} = Method.from_store ["simplification","for_polynomials"];
59.18 if contained_in t then error "NOT Tactical.contained_in [simplification,for_polynomials]" else ();
59.19
59.20 -val {scr = Prog t, ...} = Specify.get_met ["Test","squ-equ-test-subpbl1"];
59.21 +val {scr = Prog t, ...} = Method.from_store ["Test","squ-equ-test-subpbl1"];
59.22 if contained_in t then () else error "Tactical.contained_in [Test,squ-equ-test-subpbl1]";
59.23
59.24 -val {scr = Prog t, ...} = Specify.get_met ["simplification","of_rationals"];
59.25 +val {scr = Prog t, ...} = Method.from_store ["simplification","of_rationals"];
59.26 if contained_in t then () else error "Tactical.contained_in [simplification,of_rationals]";
60.1 --- a/test/Tools/isac/Specify/calchead.sml Tue May 12 16:22:00 2020 +0200
60.2 +++ b/test/Tools/isac/Specify/calchead.sml Tue May 12 17:42:29 2020 +0200
60.3 @@ -321,7 +321,7 @@
60.4 " REAL_LIST [c, c_2]]");
60.5 val ags = isalist2list ags';
60.6 val pI = ["LINEAR","system"];
60.7 -val pats = (#ppc o get_pbt) pI;
60.8 +val pats = (#ppc o Problem.from_store) pI;
60.9 "-a1-----------------------------------------------------";
60.10 (*match_ags = fn : theory -> pat list -> term list -> O_Model.T*)
60.11 val xxx = match_ags @{theory "EqSystem"} pats ags;
60.12 @@ -346,7 +346,7 @@
60.13 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
60.14 val ags = isalist2list ags';
60.15 val pI = ["LINEAR","system"];
60.16 -val pats = (#ppc o get_pbt) pI;
60.17 +val pats = (#ppc o Problem.from_store) pI;
60.18 "-b1-----------------------------------------------------";
60.19 val xxx = match_ags @{theory "Isac_Knowledge"} pats ags;
60.20 "-b2-----------------------------------------------------";
60.21 @@ -371,7 +371,7 @@
60.22 " [REAL_LIST [c, c_2]]");
60.23 val ags = isalist2list ags';
60.24 val pI = ["LINEAR","system"];
60.25 -val pats = (#ppc o get_pbt) pI;
60.26 +val pats = (#ppc o Problem.from_store) pI;
60.27 (*============ inhibit exn AK110726 ==============================================
60.28 val xxx - match_ags (theory "EqSystem") pats ags;
60.29 ============ inhibit exn AK110726 ==============================================*)
60.30 @@ -412,7 +412,7 @@
60.31 " REAL_LIST [c, c_2]]");
60.32 val ags = isalist2list ags';
60.33 val pI = ["LINEAR","system"];
60.34 -val pats = (#ppc o get_pbt) pI;
60.35 +val pats = (#ppc o Problem.from_store) pI;
60.36 "-a1-----------------------------------------------------";
60.37 (*match_ags = fn : theory -> pat list -> term list -> O_Model.T*)
60.38 val xxx = match_ags @{theory "EqSystem"} pats ags;
60.39 @@ -437,7 +437,7 @@
60.40 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
60.41 val ags = isalist2list ags';
60.42 val pI = ["LINEAR","system"];
60.43 -val pats = (#ppc o get_pbt) pI;
60.44 +val pats = (#ppc o Problem.from_store) pI;
60.45 "-b1-----------------------------------------------------";
60.46 val xxx = match_ags @{theory "Isac_Knowledge"} pats ags;
60.47 "-b2-----------------------------------------------------";
60.48 @@ -462,7 +462,7 @@
60.49 " [REAL_LIST [c, c_2]]");
60.50 val ags = isalist2list ags';
60.51 val pI = ["LINEAR","system"];
60.52 -val pats = (#ppc o get_pbt) pI;
60.53 +val pats = (#ppc o Problem.from_store) pI;
60.54 (*============ inhibit exn AK110726 ==============================================
60.55 val xxx - match_ags (theory "EqSystem") pats ags;
60.56 -------------------------------------------------------------------*)
60.57 @@ -525,7 +525,7 @@
60.58 " [no_met]) [BOOL (x+1=2), REAL x]");
60.59 val AGS = isalist2list ags';
60.60 val pI = ["univariate","equation","test"];
60.61 -val PATS = (#ppc o get_pbt) pI;
60.62 +val PATS = (#ppc o Problem.from_store) pI;
60.63 "-d1-----------------------------------------------------";
60.64 "--------------------------step through code match_ags---";
60.65 val (thy, pbt: Model_Pattern.T, ags) = (@{theory "Test"}, PATS, AGS);
60.66 @@ -814,7 +814,7 @@
60.67 (*#############################^^^^^^^^^ defined by Isabelle*)
60.68 (2, [1], "#Find", Const ("Simplify.normalform", _ (*"Real.real \<Rightarrow> Tools.una"*)),
60.69 [Free ("N", _ (*"Real.real"*))])](*,
60.70 - _ *)) = O_Model.init fmz thy ((#ppc o get_pbt) pI);
60.71 + _ *)) = O_Model.init fmz thy ((#ppc o Problem.from_store) pI);
60.72 "#undef means: the element with description TERM in fmz did not match ";
60.73 "with any element of pbl (fetched by pI), because there we have Simplify.Term";
60.74 "defined in Simplify.thy";
60.75 @@ -842,11 +842,11 @@
60.76 (*########################^^^^^^^^^ defined in Simplify.thy*)
60.77 (2, [1], "#Find", Const ("Simplify.normalform", _ ),
60.78 [Free ("N", _ )])](*,
60.79 - _*) ) = O_Model.init fmz thy ((#ppc o get_pbt) pI);
60.80 + _*) ) = O_Model.init fmz thy ((#ppc o Problem.from_store) pI);
60.81
60.82 "----- we could have checked the pbl at the very beginning and compare with (internal) fmz:";
60.83 val [("#Given", (Const ("Simplify.Term", _), Free ("t_t", _))),
60.84 - ("#Find", (Const ("Simplify.normalform", _), Free ("n_n", _)))] = (#ppc o get_pbt) pI;
60.85 + ("#Find", (Const ("Simplify.normalform", _), Free ("n_n", _)))] = (#ppc o Problem.from_store) pI;
60.86
60.87 "--------- fun typeless ---------------------------------";
60.88 "--------- fun typeless ---------------------------------";
61.1 --- a/test/Tools/isac/Specify/i-model.sml Tue May 12 16:22:00 2020 +0200
61.2 +++ b/test/Tools/isac/Specify/i-model.sml Tue May 12 17:42:29 2020 +0200
61.3 @@ -49,7 +49,7 @@
61.4 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
61.5 val cpI = if pI = Problem.id_empty then pI' else pI
61.6 val cmI = if mI = Method.id_empty then mI' else mI
61.7 - val {ppc, where_, prls, ...} = Specify.get_pbt cpI;
61.8 + val {ppc, where_, prls, ...} = Problem.from_store cpI;
61.9
61.10 (*+*)if Model_Pattern.to_string ppc = "[\"" ^
61.11 "(#Given, (Traegerlaenge, l_l))\",\"" ^
61.12 @@ -106,7 +106,7 @@
61.13 val pre = Pre_Conds.check' thy prls where_ pbl'
61.14 val pb = foldl and_ (true, map fst pre)
61.15 val (p_, _) =
61.16 - nxt_spec Pos.Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI);
61.17 + nxt_spec Pos.Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI);
61.18
61.19 (*+*)if pre = [] then () else error "FINAL Pre_Conds.check' CHANGED 1";
61.20 (*+*)if pb = true then () else error "FINAL Pre_Conds.check' CHANGED 1";
62.1 --- a/test/Tools/isac/Specify/o-model.sml Tue May 12 16:22:00 2020 +0200
62.2 +++ b/test/Tools/isac/Specify/o-model.sml Tue May 12 17:42:29 2020 +0200
62.3 @@ -29,14 +29,14 @@
62.4 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
62.5 val thy = ThyC.get_theory dI;
62.6 (*if*) mI = ["no_met"] (*else*);
62.7 - val (pI, pors, mI) = (pI, Specify.get_pbt pI |> #ppc |> init fmz thy, mI);
62.8 + val (pI, pors, mI) = (pI, Problem.from_store pI |> #ppc |> init fmz thy, mI);
62.9
62.10 -(*+*)Specify.get_pbt pI: Problem.T;
62.11 -(*+*)(Specify.get_pbt pI |> #ppc): Model_Pattern.T;
62.12 +(*+*)Problem.from_store pI: Problem.T;
62.13 +(*+*)(Problem.from_store pI |> #ppc): Model_Pattern.T;
62.14
62.15 -(*+*)val o_model = (Specify.get_pbt pI |> #ppc |>
62.16 +(*+*)val o_model = (Problem.from_store pI |> #ppc |>
62.17 O_Model.init fmz thy);
62.18 -"~~~~~ fun init , args:"; val (fmz, thy, pbt) = (fmz, thy, Specify.get_pbt pI |> #ppc);
62.19 +"~~~~~ fun init , args:"; val (fmz, thy, pbt) = (fmz, thy, Problem.from_store pI |> #ppc);
62.20 val ori = (map (fn str => str
62.21 |> TermC.parseNEW'' thy
62.22 |> Input_Descript.split
63.1 --- a/test/Tools/isac/Specify/ptyps.sml Tue May 12 16:22:00 2020 +0200
63.2 +++ b/test/Tools/isac/Specify/ptyps.sml Tue May 12 17:42:29 2020 +0200
63.3 @@ -137,17 +137,17 @@
63.4 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
63.5 "solveFor x","errorBound (eps=0)","solutions L"];
63.6 val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =
63.7 - get_pbt ["univariate","equation"];
63.8 + Problem.from_store ["univariate","equation"];
63.9 match_pbl fmz pbt;
63.10 *)
63.11 "----------- fun match_oris --------------------------------------";
63.12 "----------- fun match_oris --------------------------------------";
63.13 "----------- fun match_oris --------------------------------------";
63.14 (* val (pblRD,ori)=("xxx",oris);
63.15 - val py = get_pbt ["equation"];
63.16 - val py = get_pbt ["univariate","equation"];
63.17 - val py = get_pbt ["linear","univariate","equation"];
63.18 - val py = get_pbt ["root\"","univariate","equation"];
63.19 + val py = Problem.from_store ["equation"];
63.20 + val py = Problem.from_store ["univariate","equation"];
63.21 + val py = Problem.from_store ["linear","univariate","equation"];
63.22 + val py = Problem.from_store ["root\"","univariate","equation"];
63.23 match_oris (#prls py) ori (#ppc py, #where_ py);
63.24 *)
63.25
64.1 --- a/test/Tools/isac/Specify/specify.sml Tue May 12 16:22:00 2020 +0200
64.2 +++ b/test/Tools/isac/Specify/specify.sml Tue May 12 17:42:29 2020 +0200
64.3 @@ -121,7 +121,7 @@
64.4 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
64.5 val mits = get_obj g_met pt (fst p);
64.6 val mits = complete_metitms oris pits []
64.7 - ((#ppc o get_met) ["DiffApp","max_by_calculus"]);
64.8 + ((#ppc o Method.from_store) ["DiffApp","max_by_calculus"]);
64.9 writeln (I_Model.to_string ctxt mits);
64.10 (*[
64.11 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
65.1 --- a/test/Tools/isac/Specify/step-specify.sml Tue May 12 16:22:00 2020 +0200
65.2 +++ b/test/Tools/isac/Specify/step-specify.sml Tue May 12 17:42:29 2020 +0200
65.3 @@ -59,15 +59,15 @@
65.4 (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*);
65.5 val cpI = if pI = Problem.id_empty then pI' else pI;
65.6 val cmI = if mI = Method.id_empty then mI' else mI;
65.7 - val {ppc, prls, where_, ...} = Specify.get_pbt cpI;
65.8 + val {ppc, prls, where_, ...} = Problem.from_store cpI;
65.9 val pre = Pre_Conds.check' "thy 100820" prls where_ probl;
65.10 val pb = foldl and_ (true, map fst pre);
65.11
65.12 val (Pbl, Specify_Theory "Integrate") =
65.13 - Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI);
65.14 + Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI);
65.15 "~~~~~ fun nxt_spec , args:"; val (Pbl, preok, oris, (dI', pI', mI'), (pbl, met), (pbt, mpc), (dI, pI, mI))
65.16 (* vv----^^*)
65.17 - = (p_, pb, oris, (dI', pI', mI'), (probl, meth), (ppc, (#ppc o Specify.get_met) cmI), (dI, pI, mI));
65.18 + = (p_, pb, oris, (dI', pI', mI'), (probl, meth), (ppc, (#ppc o Method.from_store) cmI), (dI, pI, mI));
65.19 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
65.20 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
65.21 val NONE = (*case*) find_first (is_error o #5) pbl (*of*);