1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Tue Sep 06 11:47:00 2022 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Sep 07 10:58:12 2022 +0200
1.3 @@ -192,7 +192,8 @@
1.4 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
1.5 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
1.6 fun get_ref_thy () = Synchronized.value cur_thy;
1.7 -(**)end(**);
1.8 +
1.9 +(**)end(*struct*);
1.10 \<close>
1.11
1.12
1.13 @@ -264,6 +265,13 @@
1.14 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
1.15 "TODO exception hierarchy needs to be established.")
1.16
1.17 +fun get_rls ctxt (rls' : Rule_Set.id) =
1.18 + case AList.lookup (op =) (KEStore_Elems.get_rlss (Proof_Context.theory_of ctxt )) rls' of
1.19 + SOME (_, rls) => rls
1.20 + | NONE => raise ERROR ("rls \"" ^ rls' ^ "\" missing in theory \"" ^
1.21 + (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
1.22 + "\nTODO exception hierarchy needs to be established.")
1.23 +
1.24 fun assoc_rls' thy (rls' : Rule_Set.id) =
1.25 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
1.26 SOME (_, rls) => rls
1.27 @@ -356,6 +364,14 @@
1.28 \<close>
1.29 ML \<open>
1.30 \<close> ML \<open>
1.31 +get_rls: Proof.context -> Rule_Set.id -> Rule_Def.rule_set
1.32 +\<close> ML \<open>
1.33 +get_rls: Proof.context -> Rule_Set.id -> Rule_Set.T
1.34 +\<close> ML \<open>
1.35 +@{context} |> Proof_Context.theory_of |> Context.theory_name
1.36 +\<close> ML \<open>
1.37 +Context.theory_id
1.38 +\<close> ML \<open>
1.39 \<close> ML \<open>
1.40 \<close>
1.41 end
2.1 --- a/src/Tools/isac/Interpret/istate.sml Tue Sep 06 11:47:00 2022 +0200
2.2 +++ b/src/Tools/isac/Interpret/istate.sml Wed Sep 07 10:58:12 2022 +0200
2.3 @@ -169,27 +169,26 @@
2.4 fun init_detail (Tactic.Rewrite_Set rls) t =
2.5 let
2.6 val thy = ThyC.get_theory "Isac_Knowledge"
2.7 - val args = Auto_Prog.gen thy t (assoc_rls rls) |> Program.formal_args
2.8 + val ctxt = Proof_Context.init_global thy
2.9 + val args = Auto_Prog.gen thy t (get_rls ctxt rls) |> Program.formal_args
2.10 in
2.11 Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true [(hd args, t)])
2.12 end
2.13 | init_detail (Tactic.Rewrite_Set_Inst (subs, rls)) t =
2.14 let
2.15 - val ctxt = Proof_Context.init_global (ThyC.get_theory "Isac_Knowledge")
2.16 - val rls' = assoc_rls rls
2.17 + val thy = ThyC.get_theory "Isac_Knowledge"
2.18 + val ctxt = Proof_Context.init_global thy
2.19 + val rls' = get_rls ctxt rls
2.20 val v = case Subst.T_from_input ctxt subs of
2.21 (_, v) :: _ => v (*...we suppose the substitution of only ONE bound variable*)
2.22 | _ => raise ERROR "init_detail: uncovered case"
2.23 - val prog = Auto_Prog.gen (Proof_Context.theory_of ctxt) t rls'
2.24 + val prog = Auto_Prog.gen thy t rls'
2.25 val args = Program.formal_args prog
2.26 in
2.27 Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true (args ~~ [t, v]))
2.28 end
2.29 - | init_detail tac _ = raise ERROR ("init_detail: uncovered definition for " ^ Tactic.input_to_string tac)
2.30 -
2.31 -(** initialisation **)
2.32 -
2.33 -
2.34 + | init_detail tac _ =
2.35 + raise ERROR ("init_detail: uncovered definition for " ^ Tactic.input_to_string tac)
2.36
2.37 (**)end(**)
2.38
3.1 --- a/src/Tools/isac/Interpret/li-tool.sml Tue Sep 06 11:47:00 2022 +0200
3.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Sep 07 10:58:12 2022 +0200
3.3 @@ -118,7 +118,7 @@
3.4 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
3.5 else Not_Associated
3.6 | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>,_) $ _ $ rls_ $ f_) =>
3.7 - if Rule_Set.contains (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) then
3.8 + if Rule_Set.contains (Rule.Thm thm'') (get_rls ctxt (HOLogic.dest_string rls_)) then
3.9 if f = f_ then
3.10 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.11 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
3.12 @@ -133,7 +133,7 @@
3.13 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
3.14 else Not_Associated
3.15 | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>, _) $ rls_ $ f_) =>
3.16 - if Rule_Set.contains (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) then
3.17 + if Rule_Set.contains (Rule.Thm thm'') (get_rls ctxt (HOLogic.dest_string rls_)) then
3.18 if f = f_ then
3.19 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.20 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
3.21 @@ -161,12 +161,12 @@
3.22 else Not_Associated
3.23 | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ _ $ rls_ $ f_) =>
3.24 if Rule_Set.contains (Rule.Eval (assoc_calc' (ThyC.get_theory "Isac_Knowledge")
3.25 - op_ |> snd)) (assoc_rls (HOLogic.dest_string rls_)) then
3.26 + op_ |> snd)) (get_rls ctxt (HOLogic.dest_string rls_)) then
3.27 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
3.28 else Not_Associated
3.29 | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls_ $ f_) =>
3.30 if Rule_Set.contains (Rule.Eval (assoc_calc' ( ThyC.get_theory "Isac_Knowledge")
3.31 - op_ |> snd)) (assoc_rls (HOLogic.dest_string rls_)) then
3.32 + op_ |> snd)) (get_rls ctxt (HOLogic.dest_string rls_)) then
3.33 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
3.34 else Not_Associated
3.35 | _ => Not_Associated)
4.1 --- a/src/Tools/isac/Interpret/solve-step.sml Tue Sep 06 11:47:00 2022 +0200
4.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Wed Sep 07 10:58:12 2022 +0200
4.3 @@ -168,9 +168,9 @@
4.4 val thy' = ctxt |> Proof_Context.theory_of |> Context.theory_name
4.5 val f = Calc.current_formula cs;
4.6 in
4.7 - case Rewrite.rewrite_set_ ctxt false (assoc_rls rls) f of
4.8 + case Rewrite.rewrite_set_ ctxt false (get_rls ctxt rls) f of
4.9 SOME (f', asm)
4.10 - => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
4.11 + => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, get_rls ctxt rls, f, (f', asm)))
4.12 | NONE => Applicable.No (rls ^ " not applicable")
4.13 end
4.14 | check (Tactic.Rewrite_Set_Inst (subs, rls)) (cs as (pt, pos)) =
4.15 @@ -180,9 +180,10 @@
4.16 val f = Calc.current_formula cs;
4.17 val subst = Subst.T_from_input ctxt subs; (*TODO: input requires parse _: _ -> _ option*)
4.18 in
4.19 - case Rewrite.rewrite_set_inst_ ctxt false subst (assoc_rls rls) f of
4.20 + case Rewrite.rewrite_set_inst_ ctxt false subst (get_rls ctxt rls) f of
4.21 SOME (f', asm)
4.22 - => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
4.23 + => Applicable.Yes
4.24 + (Tactic.Rewrite_Set_Inst' (thy', false, subst, get_rls ctxt rls, f, (f', asm)))
4.25 | NONE => Applicable.No (rls ^ " not applicable")
4.26 end
4.27 | check (Tactic.Subproblem (domID, pblID)) (_, _) =
5.1 --- a/src/Tools/isac/Knowledge/Rational.thy Tue Sep 06 11:47:00 2022 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Sep 07 10:58:12 2022 +0200
5.3 @@ -474,7 +474,7 @@
5.4 ML \<open>
5.5 (**)local (* cancel_p *)
5.6
5.7 -val {rules = rules, rew_ord = (_, ro), ...} = Rule_Set.rep (assoc_rls' @{theory} "rev_rew_p");
5.8 +val {rules = rules, rew_ord = (_, ro), ...} = Rule_Set.rep (get_rls @{context} "rev_rew_p");
5.9
5.10 fun init_state thy eval_rls ro t =
5.11 let
5.12 @@ -534,8 +534,8 @@
5.13 ML \<open>
5.14 (**)local (* add_fractions_p *)
5.15
5.16 -(*val {rules = rules, rew_ord = (_, ro), ...} = Rule_Set.rep (assoc_rls "make_polynomial");*)
5.17 -val {rules, rew_ord=(_,ro),...} = Rule_Set.rep (assoc_rls' @{theory} "rev_rew_p");
5.18 +(*val {rules = rules, rew_ord = (_, ro), ...} = Rule_Set.rep (get_rls "make_polynomial");*)
5.19 +val {rules, rew_ord = (_, ro), ...} = Rule_Set.rep (get_rls @{context} "rev_rew_p");
5.20
5.21 fun init_state thy eval_rls ro t =
5.22 let
6.1 --- a/src/Tools/isac/Knowledge/Test.thy Tue Sep 06 11:47:00 2022 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Sep 07 10:58:12 2022 +0200
6.3 @@ -566,21 +566,21 @@
6.4 problem pbl_test : "test" = \<open>Rule_Set.empty\<close>
6.5
6.6 problem pbl_test_equ : "equation/test" =
6.7 - \<open>assoc_rls' @{theory} "matches"\<close>
6.8 + \<open>get_rls @{context} "matches"\<close>
6.9 CAS: "solve (e_e::bool, v_v)"
6.10 Given: "equality e_e" "solveFor v_v"
6.11 Where: "matches (?a = ?b) e_e"
6.12 Find: "solutions v_v'i'"
6.13
6.14 problem pbl_test_uni : "univariate/equation/test" =
6.15 - \<open>assoc_rls' @{theory} "matches"\<close>
6.16 + \<open>get_rls @{context} "matches"\<close>
6.17 CAS: "solve (e_e::bool, v_v)"
6.18 Given: "equality e_e" "solveFor v_v"
6.19 Where: "matches (?a = ?b) e_e"
6.20 Find: "solutions v_v'i'"
6.21
6.22 problem pbl_test_uni_lin : "LINEAR/univariate/equation/test" =
6.23 - \<open>assoc_rls' @{theory} "matches"\<close>
6.24 + \<open>get_rls @{context} "matches"\<close>
6.25 Method_Ref: "Test/solve_linear"
6.26 CAS: "solve (e_e::bool, v_v)"
6.27 Given: "equality e_e" "solveFor v_v"
6.28 @@ -694,7 +694,7 @@
6.29 section \<open>problems\<close>
6.30
6.31 problem pbl_test_uni_plain2 : "plain_square/univariate/equation/test" =
6.32 - \<open>assoc_rls' @{theory} "matches"\<close>
6.33 + \<open>get_rls @{context} "matches"\<close>
6.34 Method_Ref: "Test/solve_plain_square"
6.35 CAS: "solve (e_e::bool, v_v)"
6.36 Given: "equality e_e" "solveFor v_v"
6.37 @@ -778,7 +778,7 @@
6.38 [e_e])"
6.39 method met_test_solvelin : "Test/solve_linear" =
6.40 \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty,
6.41 - prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
6.42 + prls = get_rls @{context} "matches", calc = [], crls = tval_rls, errpats = [],
6.43 nrls = Test_simplify}\<close>
6.44 Program: solve_linear.simps
6.45 Given: "equality e_e" "solveFor v_v"
6.46 @@ -948,7 +948,7 @@
6.47 method met_test_eq_plain : "Test/solve_plain_square" =
6.48 (*solve_plain_square*)
6.49 \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
6.50 - prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,
6.51 + prls = get_rls @{context} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,
6.52 asm_rls=[],asm_thm=[]*)}\<close>
6.53 Program: solve_plain_square.simps
6.54 Given: "equality e_e" "solveFor v_v"
7.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Tue Sep 06 11:47:00 2022 +0200
7.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Sep 07 10:58:12 2022 +0200
7.3 @@ -47,6 +47,29 @@
7.4
7.5 ML \<open>
7.6 \<close> ML \<open>
7.7 +fun lev_up [] = raise Ctree.PTREE "lev_up []"
7.8 + | lev_up p = (drop_last p);
7.9 +\<close> ML \<open>
7.10 +\<close> ML \<open>
7.11 +open Ctree
7.12 +\<close> ML \<open> (*postpone after successful test*)
7.13 +fun parent_node _ [] = (true, [], Rule_Set.Empty)
7.14 + | parent_node pt p =
7.15 + let
7.16 + fun par _ [] = (true, [], Rule_Set.Empty)
7.17 + | par pt p =
7.18 + if is_pblobj (get_obj I pt p)
7.19 + then (true, p, Rule_Set.Empty)
7.20 + else
7.21 + let
7.22 + val ctxt = p |> get_obj g_loc pt |> snd |> the |> snd (*???*)
7.23 + in
7.24 + case get_obj g_tac pt p of
7.25 + Tactic.Rewrite_Set rls' => (false, p, get_rls ctxt rls')
7.26 + | Tactic.Rewrite_Set_Inst (_, rls') => (false, p, get_rls ctxt rls')
7.27 + | _ => par pt (lev_up p)
7.28 + end
7.29 + in par pt (lev_up p) end;
7.30 \<close> ML \<open>
7.31 \<close>
7.32 end
8.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Tue Sep 06 11:47:00 2022 +0200
8.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Sep 07 10:58:12 2022 +0200
8.3 @@ -457,20 +457,20 @@
8.4 fun get_loc EmptyPtree _ = (Istate_Def.empty, ContextC.empty)
8.5 | get_loc pt (p, Res) =
8.6 (case get_obj g_loc pt p of
8.7 - (SOME i, NONE) => i
8.8 - | (NONE , NONE) => (Istate_Def.empty, ContextC.empty)
8.9 - | (_ , SOME i) => i)
8.10 + (SOME ist_ctxt, NONE) => ist_ctxt
8.11 + | (NONE , NONE) => (Istate_Def.empty, ContextC.empty)
8.12 + | (_ , SOME ist_ctxt) => ist_ctxt)
8.13 | get_loc pt (p, _) =
8.14 (case get_obj g_loc pt p of
8.15 - (NONE , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
8.16 - | (NONE , NONE) => (Istate_Def.empty, ContextC.empty)
8.17 - | (SOME i, _) => i);
8.18 + (NONE , SOME ist_ctxt) => ist_ctxt (* 020813 too liberal? *)
8.19 + | (NONE , NONE) => (Istate_Def.empty, ContextC.empty)
8.20 + | (SOME ist_ctxt, _) => ist_ctxt);
8.21 fun get_istate_LI pt p = get_loc pt p |> #1;
8.22 fun get_ctxt_LI pt p = get_loc pt p |> #2;
8.23 fun get_ctxt pt (pos as (p, p_)) =
8.24 if member op = [Frm, Res] p_
8.25 then get_loc pt pos |> #2 (*for program interpretation rely on fun get_loc*)
8.26 - else (*p = Pbl: for specify phase take ctx from PblObj *)
8.27 + else (*p = Pbl: for specify phase take ctxt from PblObj *)
8.28 if (p |> get_obj g_origin pt |> LibraryC.fst3) = [] (*CAS-command ? *)
8.29 then (ThyC.get_theory "Isac_Knowledge"(*CAS-command unknown*)) |> Defs.global_context |> fst
8.30 else get_obj g_ctxt pt p
9.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Tue Sep 06 11:47:00 2022 +0200
9.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Wed Sep 07 10:58:12 2022 +0200
9.3 @@ -276,10 +276,10 @@
9.4 try_rew ctxt (ro, assoc_rew_ord (Proof_Context.theory_of ctxt) ro) erls
9.5 (Subst.T_from_input ctxt subs) f (Rule.Thm thm'')
9.6
9.7 - | applicable thy _ _ f (Rewrite_Set rls') =
9.8 - filter_appl_rews thy [] f (assoc_rls rls')
9.9 - | applicable thy _ _ f (Rewrite_Set_Inst (subs, rls')) =
9.10 - filter_appl_rews thy (Subst.T_from_input thy subs) f (assoc_rls rls')
9.11 + | applicable ctxt _ _ f (Rewrite_Set rls') =
9.12 + filter_appl_rews ctxt [] f (get_rls ctxt rls')
9.13 + | applicable ctxt _ _ f (Rewrite_Set_Inst (subs, rls')) =
9.14 + filter_appl_rews ctxt (Subst.T_from_input ctxt subs) f (get_rls ctxt rls')
9.15 | applicable _ _ _ _ tac =
9.16 (tracing ("### applicable: not impl. for tac = '" ^ input_to_string tac ^ "'"); []);
9.17
10.1 --- a/src/Tools/isac/MathEngine/detail-step.sml Tue Sep 06 11:47:00 2022 +0200
10.2 +++ b/src/Tools/isac/MathEngine/detail-step.sml Wed Sep 07 10:58:12 2022 +0200
10.3 @@ -30,8 +30,8 @@
10.4 let
10.5 val t = get_obj g_form pt p
10.6 val tac = get_obj g_tac pt p
10.7 - val rls = (assoc_rls o Tactic.rls_of) tac
10.8 val ctxt = get_ctxt pt pos
10.9 + val rls = tac |> Tactic.rls_of |> get_rls ctxt
10.10 in
10.11 case rls of
10.12 Rule_Set.Rrls {scr = Rule.Rfuns {init_state, ...}, ...} =>
11.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Tue Sep 06 11:47:00 2022 +0200
11.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Wed Sep 07 10:58:12 2022 +0200
11.3 @@ -143,7 +143,7 @@
11.4 (*ER-7*) (*Schalk I s.87 Bsp 55b*)
11.5 val fmz = ["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
11.6 "solveFor x", "solutions L"];
11.7 -val spec = ("RatEq",["univariate", "equation"],["no_met"]);
11.8 +val spec = ((** )"RatEq"( **)"PolyEq"(**),["univariate", "equation"],["no_met"]);
11.9 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)]; (* 0. specify-phase *)
11.10 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
11.11 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
12.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Tue Sep 06 11:47:00 2022 +0200
12.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Sep 07 10:58:12 2022 +0200
12.3 @@ -673,7 +673,8 @@
12.4 ---- rat-eq + subpbl: set_found in check_tac1 ----*)
12.5 CalcTree
12.6 [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x", "solutions L"],
12.7 - ("RatEq", ["univariate", "equation"], ["no_met"]))];
12.8 + ((** )"RatEq"( **)"PolyEq"(*required for "make_ratpoly_in"*),
12.9 + ["univariate", "equation"], ["no_met"]))];
12.10 Iterator 1;
12.11 moveActiveRoot 1;
12.12 fetchProposedTactic 1;
13.1 --- a/test/Tools/isac/Knowledge/rational-2.sml Tue Sep 06 11:47:00 2022 +0200
13.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml Wed Sep 07 10:58:12 2022 +0200
13.3 @@ -1574,7 +1574,7 @@
13.4 then () else error "rls chancel_p 3";
13.5
13.6 "--- with simpler ruleset";
13.7 -val {rules, rew_ord= (_, ro), ...} = Rule_Set.rep (assoc_rls "rev_rew_p");
13.8 +val {rules, rew_ord= (_, ro), ...} = Rule_Set.rep (get_rls @{context} "rev_rew_p");
13.9 val der = Derive.do_one ctxt Atools_erls rules ro NONE tt;
13.10 if length der = 12 then () else error "WN1130912 rls chancel_p 4";
13.11 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*)
13.12 @@ -1588,7 +1588,7 @@
13.13 (TermC.str2term "(1 * a + 1 * b) * (1 * a + - 1 * b)");
13.14 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*)
13.15
13.16 -val {rules, rew_ord=(_,ro),...} = Rule_Set.rep (assoc_rls "rev_rew_p");
13.17 +val {rules, rew_ord=(_,ro),...} = Rule_Set.rep (get_rls @{context} "rev_rew_p");
13.18 val der = Derive.do_one ctxt Atools_erls rules ro NONE
13.19 (TermC.str2term "(1 * a + - 1 * b) * (1 * a + - 1 * b)");
13.20 (*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*)
14.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Tue Sep 06 11:47:00 2022 +0200
14.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Wed Sep 07 10:58:12 2022 +0200
14.3 @@ -489,7 +489,7 @@
14.4 val thy = @{theory RatEq};
14.5 val ctxt = Proof_Context.init_global thy;
14.6 val SOME t = TermC.parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
14.7 -val rls = assoc_rls "RatEq_eliminate"
14.8 +val rls = get_rls ctxt "RatEq_eliminate"
14.9
14.10 val SOME (t''''', asm''''') =
14.11 rewrite_set_ ctxt true rls t;
15.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue Sep 06 11:47:00 2022 +0200
15.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Sep 07 10:58:12 2022 +0200
15.3 @@ -167,7 +167,8 @@
15.4 (* \<up> \<up> \<up> only once in test/../solve.sml*)
15.5 val t = get_obj g_form pt p
15.6 val tac = get_obj g_tac pt p
15.7 - val rls = (assoc_rls o rls_of) tac
15.8 + val ctxt = get_ctxt pt pos
15.9 + val rls = ((get_rls ctxt) o rls_of) tac
15.10 val ctxt = get_ctxt pt pos
15.11 (*rls = Rule_Set.Repeat {calc = [], erls = ...*)
15.12 val is = Istate.init_detail tac t
16.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Tue Sep 06 11:47:00 2022 +0200
16.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Wed Sep 07 10:58:12 2022 +0200
16.3 @@ -84,7 +84,7 @@
16.4 "~~~~~ fun detailrls , args:"; val (pt, (pos as (p, _))) = (pt, pos);
16.5 val t = get_obj g_form pt p
16.6 val tac = get_obj g_tac pt p
16.7 - val rls = (assoc_rls o Tactic.rls_of) tac
16.8 + val rls = ((get_rls ctxt) o Tactic.rls_of) tac
16.9 val ctxt = get_ctxt pt pos
16.10 val _ = (*case*) rls (*of*);
16.11 val is = Istate.init_detail tac t
17.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Tue Sep 06 11:47:00 2022 +0200
17.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Wed Sep 07 10:58:12 2022 +0200
17.3 @@ -25,7 +25,7 @@
17.4 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
17.5 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
17.6 "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
17.7 -val rls = assoc_rls "integration";
17.8 +val rls = get_rls @{context} "integration";
17.9 val thy' = @{theory "Integrate"}
17.10 val ctxt = Proof_Context.init_global thy'
17.11 val t = @{term "ttt :: real"};
17.12 @@ -56,14 +56,15 @@
17.13 = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), TermC.str2term "someTermWithBdv");
17.14 val v = case Subst.T_from_input ctxt subs of
17.15 (_, v) :: _ => v;
17.16 - (*case*) assoc_rls rls (*of*);
17.17 + (*case*) get_rls ctxt rls (*of*);
17.18
17.19
17.20 "-------- test the same called by interSteps norm_Poly -----------------------------------------";
17.21 "-------- test the same called by interSteps norm_Poly -----------------------------------------";
17.22 "-------- test the same called by interSteps norm_Poly -----------------------------------------";
17.23 -val rls = assoc_rls "norm_Poly";
17.24 val thy' = @{theory "Poly"}
17.25 +val ctxt = Proof_Context.init_global thy'
17.26 +val rls = get_rls ctxt "norm_Poly";
17.27 val t = @{term "ttt :: real"}
17.28 val auto_script = Auto_Prog.gen thy' t rls;
17.29
17.30 @@ -146,8 +147,10 @@
17.31 "-------- test the same called by interSteps norm_Rational -------------------------------------";
17.32 "-------- test the same called by interSteps norm_Rational -------------------------------------";
17.33 "-------- test the same called by interSteps norm_Rational -------------------------------------";
17.34 -val auto_script =
17.35 - Auto_Prog.gen @{theory "Poly"} @{term "ttt :: real"} (assoc_rls "norm_Rational");
17.36 +val thy = @{theory (** )"Poly" ( **) Rational(**) (*required for rls "norm_Rational"*)}
17.37 +val ctxt = Proof_Context.init_global thy
17.38 +val auto_script =
17.39 + Auto_Prog.gen thy @{term "ttt :: real"} (get_rls ctxt "norm_Rational");
17.40 writeln(UnparseC.term auto_script);
17.41 TermC.atomty auto_script;
17.42 (***
17.43 @@ -181,7 +184,7 @@
17.44 reset_states ();
17.45 CalcTree
17.46 [(["Term (b + a - b)", "normalform N"],
17.47 - ("Poly",["polynomial", "simplification"],
17.48 + ((** )"Poly"( **)"Rational"(**),["polynomial", "simplification"],
17.49 ["simplification", "of_rationals"]))];
17.50 Iterator 1;
17.51 moveActiveRoot 1;
17.52 @@ -328,7 +331,9 @@
17.53 "-------- fun subst_typ ------------------------------------------------------------------------";
17.54 "-------- fun subst_typ ------------------------------------------------------------------------";
17.55 "-------- fun subst_typ ------------------------------------------------------------------------";
17.56 -val prog = Auto_Prog.gen @{theory Isac_Knowledge} t (assoc_rls "isolate_bdv");
17.57 +val thy = @{theory "Isac_Knowledge"}
17.58 +val ctxt = Proof_Context.init_global thy
17.59 +val prog = Auto_Prog.gen thy t (get_rls ctxt "isolate_bdv");
17.60 (* UnparseC.term prog |> writeln
17.61 auto_generated_inst t_t v =
17.62 Repeat
17.63 @@ -362,7 +367,7 @@
17.64 "-------- fun subst_typs -----------------------------------------------------------------------";
17.65 "-------- fun subst_typs -----------------------------------------------------------------------";
17.66 "-------- fun subst_typs -----------------------------------------------------------------------";
17.67 -val prog = Auto_Prog.gen thy' t (assoc_rls "isolate_bdv");
17.68 +val prog = Auto_Prog.gen thy' t (get_rls ctxt "isolate_bdv");
17.69 val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real"), Free ("v", "'a")]*)
17.70 if length frees = 2 then () else error "test setup Auto_Prog.subst_typs changed 1";
17.71
18.1 --- a/test/Tools/isac/ProgLang/listC.sml Tue Sep 06 11:47:00 2022 +0200
18.2 +++ b/test/Tools/isac/ProgLang/listC.sml Wed Sep 07 10:58:12 2022 +0200
18.3 @@ -45,7 +45,7 @@
18.4 "--------------------- NTH ---------------------------------------------------";
18.5 "--------------------- NTH ---------------------------------------------------";
18.6 val ctxt = Proof_Context.init_global @{theory}
18.7 -val prog_expr = assoc_rls "prog_expr"
18.8 +val prog_expr = get_rls @{context} "prog_expr"
18.9
18.10 val t = TermC.str2term "NTH 1 [a,b,c,d,e]";
18.11 TermC.atomty t;
18.12 @@ -81,7 +81,7 @@
18.13 "--------------------- Length ------------------------------------------------";
18.14 "--------------------- Length ------------------------------------------------";
18.15 "--------------------- Length ------------------------------------------------";
18.16 -val prog_expr = assoc_rls "prog_expr"
18.17 +val prog_expr = get_rls @{context} "prog_expr"
18.18
18.19 val thy = @{theory ListC};
18.20 val t = TermC.str2term "Length [1, 1, 1]";