1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Dec 04 16:48:06 2022 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Thu Dec 08 10:16:40 2022 +0100
1.3 @@ -68,7 +68,7 @@
1.4
1.5 \<open>term Know_Store.get_*\<close> retrieves all * of the respective theory PLUS of all ancestor theories.
1.6 \<close> ML \<open>
1.7 -signature KESTORE_ELEMS(*TODO rename to KNOW_STORE*) =
1.8 +signature KNOW_STORE =
1.9 sig
1.10 val get_rew_ords: theory -> Rewrite_Ord.T list
1.11 val add_rew_ords: Rewrite_Ord.T list -> theory -> theory
1.12 @@ -92,7 +92,7 @@
1.13 val get_via_last_thy: ThyC.id -> theory (* only used for Subproblem retrieving respective thy *)
1.14 end;
1.15
1.16 -structure Know_Store(*(*TODO rename to Know_Store*)*): KESTORE_ELEMS(**) =
1.17 +structure Know_Store(**): KNOW_STORE(**) =
1.18 struct
1.19 structure Data = Theory_Data (
1.20 type T = Rewrite_Ord.T list;
2.1 --- a/src/Tools/isac/BaseDefinitions/contextC.sml Sun Dec 04 16:48:06 2022 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/contextC.sml Thu Dec 08 10:16:40 2022 +0100
2.3 @@ -10,13 +10,13 @@
2.4 val isac_ctxt : 'a -> Proof.context
2.5 val declare_constraints: term -> Proof.context -> Proof.context
2.6 val add_constraints: term list -> Proof.context -> Proof.context
2.7 - val initialise : ThyC.id -> term list -> Proof.context
2.8 + val initialise : Proof.context -> term list -> Proof.context
2.9 val initialise' : theory -> TermC.as_string list -> Proof.context
2.10 val get_assumptions : Proof.context -> term list
2.11 val insert_assumptions : term list -> Proof.context -> Proof.context
2.12 val avoid_contradict: term -> term list -> term * term list
2.13 val subpbl_to_caller : Proof.context -> term -> Proof.context -> term * Proof.context
2.14 -(*val subpbl_to_caller .. rename according to naming convention TODO*)
2.15 +
2.16 \<^isac_test>\<open>
2.17 val transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context
2.18 val contradict : term list -> term -> bool
2.19 @@ -38,9 +38,8 @@
2.20 fold Variable.declare_constraints (TermC.vars' ts) ctxt
2.21
2.22 (* in Subproblem take respective actual arguments from program *)
2.23 -fun initialise thy' ts =
2.24 +fun initialise ctxt ts =
2.25 let
2.26 - val ctxt = ThyC.get_theory thy' |> Proof_Context.init_global
2.27 val frees = TermC.vars' ts
2.28 val _ = TermC.raise_type_conflicts frees
2.29 in
2.30 @@ -48,7 +47,7 @@
2.31 end
2.32 (* in root-problem take respective formalisation *)
2.33 fun initialise' thy fmz =
2.34 - let
2.35 + let
2.36 val ctxt = thy |> Proof_Context.init_global
2.37 val frees = map (TermC.parseNEW' ctxt) fmz |> TermC.vars'
2.38 val _ = TermC.raise_type_conflicts frees
2.39 @@ -69,10 +68,10 @@
2.40 let
2.41 val to_vars = get_assumptions to_ctxt |> map TermC.vars |> flat
2.42 fun transfer [] to_ctxt = to_ctxt
2.43 - | transfer (from_asm :: fas) to_ctxt =
2.44 - if inter op = (TermC.vars from_asm) to_vars = []
2.45 - then transfer fas to_ctxt
2.46 - else transfer fas (insert_assumptions [from_asm] to_ctxt)
2.47 + | transfer (from_asm :: fas) to_ctxt =
2.48 + if inter op = (TermC.vars from_asm) to_vars = []
2.49 + then transfer fas to_ctxt
2.50 + else transfer fas (insert_assumptions [from_asm] to_ctxt)
2.51 in
2.52 transfer (get_assumptions from_ctxt) to_ctxt
2.53 end
3.1 --- a/src/Tools/isac/BaseDefinitions/theoryC.sml Sun Dec 04 16:48:06 2022 +0100
3.2 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml Thu Dec 08 10:16:40 2022 +0100
3.3 @@ -21,7 +21,7 @@
3.4 val id_empty: id
3.5 val Isac: 'a -> theory
3.6 val parent_of: theory -> theory -> theory
3.7 - val sub_common : theory * theory -> theory
3.8 +
3.9 \<^isac_test>\<open>
3.10 val get_thy: id -> theory (* restricted to session Isac *)
3.11 \<close>
3.12 @@ -70,11 +70,4 @@
3.13
3.14 fun parent_of thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1;
3.15
3.16 -fun sub_common (thy1, thy2) =
3.17 - if Context.subthy (thy1, thy2) then
3.18 - thy2
3.19 - else if Context.subthy (thy2, thy1) then
3.20 - thy1
3.21 - else get_theory "Isac_Knowledge"
3.22 -
3.23 (**)end(**)
4.1 --- a/src/Tools/isac/Build_Isac.thy Sun Dec 04 16:48:06 2022 +0100
4.2 +++ b/src/Tools/isac/Build_Isac.thy Thu Dec 08 10:16:40 2022 +0100
4.3 @@ -178,6 +178,7 @@
4.4 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method-NEXT_STEP.sml"
4.5 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml"
4.6 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
4.7 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/300-init-subpbl.sml"
4.8 ML \<open>
4.9 \<close> ML \<open>
4.10 \<close> ML \<open>
4.11 @@ -188,7 +189,6 @@
4.12 \<close> ML \<open>
4.13 \<close>
4.14 (*/------- outcomment in order to intermediately check with Test_Isac.thy ------------\(**)
4.15 - ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/300-init-subpbl.sml"
4.16 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml"
4.17 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/450-Rewrite_Set_Inst.sml"
4.18 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"
5.1 --- a/src/Tools/isac/Interpret/Interpret.thy Sun Dec 04 16:48:06 2022 +0100
5.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Thu Dec 08 10:16:40 2022 +0100
5.3 @@ -9,7 +9,6 @@
5.4 imports Specify.Specify
5.5 begin
5.6 ML_file istate.sml
5.7 - ML_file "sub-problem.sml"
5.8 ML_file "thy-read.sml"
5.9 ML_file "li-tool.sml"
5.10 ML_file "solve-step.sml"
6.1 --- a/src/Tools/isac/Interpret/li-tool.sml Sun Dec 04 16:48:06 2022 +0100
6.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Thu Dec 08 10:16:40 2022 +0100
6.3 @@ -11,7 +11,7 @@
6.4 Associated of Tactic.T * term (*..result*) * Proof.context
6.5 | Ass_Weak of Tactic.T * term (*..result*) * Proof.context
6.6 | Not_Associated;
6.7 - val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass
6.8 + val associate: Ctree.state -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass
6.9
6.10 val parent_node: Ctree.ctree -> Pos.pos' -> bool * Pos.pos * Rule_Set.T * Proof.context
6.11 val init_pstate: Rule_Set.T -> Proof.context -> I_Model.T -> MethodC.id ->
6.12 @@ -24,7 +24,7 @@
6.13
6.14 val implicit_take: Program.T -> Env.T -> term option
6.15 val get_simplifier: Calc.T -> Rule_Set.T
6.16 - val tac_from_prog: Ctree.ctree -> theory (*..for lookup in Know_Store*) -> term -> Tactic.input
6.17 + val tac_from_prog: Ctree.state -> theory (*..for lookup in Know_Store*) -> term -> Tactic.input
6.18 (*from isac_test for Minisubpbl*)
6.19 val arguments_from_model : Proof.context -> MethodC.id -> I_Model.T -> term list
6.20
7.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sun Dec 04 16:48:06 2022 +0100
7.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Dec 08 10:16:40 2022 +0100
7.3 @@ -50,14 +50,12 @@
7.4 val scan_to_tactic1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.T -> expr_val1
7.5 val scan_dn1: (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1
7.6 val check_Let_up: Istate.pstate -> term -> term * term
7.7 + val scan_up1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1;
7.8 + val go_scan_up1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> expr_val1;
7.9 + val check_tac1: Calc.T * Proof.context * Tactic.T -> Istate.pstate -> term * term option -> expr_val1
7.10
7.11 \<^isac_test>\<open>
7.12 val compare_step: State_Steps.T * Pos.pos' list * Calc.T -> term -> string * Calc.state_post
7.13 -
7.14 - val scan_up1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1;
7.15 - val go_scan_up1: term * (Calc.T * Proof.context * Tactic.T) -> Istate.pstate -> expr_val1;
7.16 -
7.17 - val check_tac1: Calc.T * Proof.context * Tactic.T -> Istate.pstate -> term * term option -> expr_val1
7.18 \<close>
7.19 end
7.20
7.21 @@ -101,12 +99,12 @@
7.22 (* check if a prog_tac found in a program is applicable_in *)
7.23 fun check_tac ((pt, p), ctxt) ist (prog_tac, form_arg) =
7.24 let
7.25 - val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
7.26 + val m = LItool.tac_from_prog (pt, p) (Proof_Context.theory_of ctxt) prog_tac
7.27 in
7.28 case m of
7.29 Tactic.Subproblem _ => (*might involve problem refinement etc*)
7.30 let
7.31 - val m' = snd (Sub_Problem.tac_from_prog pt prog_tac)
7.32 + val m' = snd (Sub_Problem.tac_from_prog (pt, p) prog_tac)
7.33 in
7.34 Accept_Tac (m', ist |> set_subst_found (form_arg, Tactic.result m'), ctxt)
7.35 end
7.36 @@ -313,7 +311,7 @@
7.37 (** check a Prog_Tac: is it associated to Tactic ? **)
7.38
7.39 fun check_tac1 ((pt, p), ctxt, tac) (ist as {act_arg, or, ...}) (prog_tac, form_arg) =
7.40 - case LItool.associate pt ctxt (tac, prog_tac) of
7.41 + case LItool.associate (pt, p) ctxt (tac, prog_tac) of
7.42 LItool.Associated (m, v', ctxt)
7.43 => Accept_Tac1 (ist |> set_subst_true (form_arg, v') |> set_found, ctxt, m)
7.44 | LItool.Ass_Weak (m, v', ctxt) (*the ONLY ones in locate_tac ^v^v^v^v^ *)
7.45 @@ -322,7 +320,7 @@
7.46 (case or of (* switch for Tactical.Or: 1st AssOnly, 2nd AssGen *)
7.47 AssOnly => Term_Val1 act_arg
7.48 | _(*ORundef*) =>
7.49 - case Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) of
7.50 + case Solve_Step.check (LItool.tac_from_prog (pt, p) (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) of
7.51 Applicable.Yes m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
7.52 | Applicable.No _ => Term_Val1 act_arg)
7.53
8.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Sun Dec 04 16:48:06 2022 +0100
8.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Thu Dec 08 10:16:40 2022 +0100
8.3 @@ -67,7 +67,7 @@
8.4 val get_somespec' : References_Def.T -> References_Def.T -> References_Def.T
8.5 exception PTREE of string;
8.6
8.7 - val rootthy : ctree -> theory
8.8 + val root_thy : ctree -> theory
8.9 (* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *)
8.10 val appl_obj : (ppobj -> ppobj) -> ctree -> Pos.pos -> ctree
8.11 val existpt : Pos.pos -> ctree -> bool
8.12 @@ -817,8 +817,8 @@
8.13
8.14 (* get the theory explicitly specified for the rootpbl;
8.15 thus use this function _after_ finishing specification *)
8.16 -fun rootthy (Nd (PblObj {spec = (thyID, _, _), ...}, _)) = ThyC.get_theory thyID
8.17 - | rootthy _ = raise ERROR "rootthy: uncovered fun def.";
8.18 +fun root_thy (Nd (PblObj {spec = (thyID, _, _), ...}, _)) = Know_Store.get_via_last_thy thyID
8.19 + | root_thy _ = raise ERROR "root_thy: uncovered fun def.";
8.20
8.21 (**)
8.22 end;
9.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Sun Dec 04 16:48:06 2022 +0100
9.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Thu Dec 08 10:16:40 2022 +0100
9.3 @@ -266,19 +266,19 @@
9.4 fun rewrite_set_ ctxt bool rls term = rewrite__set_ ctxt 1 bool [] rls term;
9.5
9.6 (* variants of rewrite; TODO del. put_asm *)
9.7 -fun rewrite_inst_ thy rew_ord rls put_asm subst thm ct =
9.8 - rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
9.9 -fun rewrite_set_inst_ thy put_asm subst rls ct = rewrite__set_ thy 1 put_asm subst rls ct;
9.10 +fun rewrite_inst_ ctxt rew_ord rls put_asm subst thm ct =
9.11 + rewrite__ ctxt 1 subst rew_ord rls put_asm thm ct;
9.12 +fun rewrite_set_inst_ ctxt put_asm subst rls ct = rewrite__set_ ctxt 1 put_asm subst rls ct;
9.13
9.14 (* given a list of equalities (lhs = rhs) and a term,
9.15 replace all occurrences of lhs in the term with rhs;
9.16 thus the order or equalities matters: put variables in lhs first. *)
9.17 -fun rewrite_terms_ thy ord asm_rls equs t =
9.18 +fun rewrite_terms_ ctxt ord asm_rls equs t =
9.19 let
9.20 fun rew_ (t', asm') [] _ = (t', asm')
9.21 | rew_ (t', asm') (rules as r::rs) t =
9.22 let
9.23 - val (t'', asm'', _(*lrd*), rew) = rew_sub thy 1 [] ord asm_rls false [] (HOLogic.Trueprop $ r) t
9.24 + val (t'', asm'', _(*lrd*), rew) = rew_sub ctxt 1 [] ord asm_rls false [] (HOLogic.Trueprop $ r) t
9.25 in
9.26 if rew
9.27 then rew_ (t'', asm' @ asm'') rules t''
9.28 @@ -289,7 +289,7 @@
9.29 end;
9.30
9.31 (* search ct for adjacent numerals and calculate them by operator isa_fn *)
9.32 -fun calculate_ ctxt (isa_fn as (id, eval_fn)) t =
9.33 +fun calculate_ ctxt (isa_fn as (id, _(*eval_fn*))) t =
9.34 case Eval.adhoc_thm ctxt isa_fn t of
9.35 NONE => NONE
9.36 | SOME (thmID, thm) =>
9.37 @@ -299,14 +299,14 @@
9.38 in SOME (rew, (thmID, thm)) end)
9.39 handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite");
9.40
9.41 -fun eval_prog_expr thy prog_rls t =
9.42 - let val rew = rewrite_set_ thy false prog_rls t;
9.43 +fun eval_prog_expr ctxt prog_rls t =
9.44 + let val rew = rewrite_set_ ctxt false prog_rls t;
9.45 in case rew of SOME (res,_) => res | NONE => t end;
9.46
9.47 fun eval_true_ _ _ (Const (\<^const_name>\<open>True\<close>,_)) = true
9.48 - | eval_true_ thy rls t =
9.49 - case rewrite_set_ thy false rls t of
9.50 - SOME (Const (\<^const_name>\<open>True\<close>,_),_) => true
9.51 + | eval_true_ ctxt rls t =
9.52 + case rewrite_set_ ctxt false rls t of
9.53 + SOME (Const (\<^const_name>\<open>True\<close>, _), _) => true
9.54 | _ => false;
9.55
9.56 end
10.1 --- a/src/Tools/isac/MathEngine/fetch-tactics.sml Sun Dec 04 16:48:06 2022 +0100
10.2 +++ b/src/Tools/isac/MathEngine/fetch-tactics.sml Thu Dec 08 10:16:40 2022 +0100
10.3 @@ -36,7 +36,7 @@
10.4 {program = Rule.Prog sc, prog_rls, ...} => (sc, prog_rls) | _ => raise ERROR "from_prog 1")
10.5 val subst = get_istate_LI pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
10.6 val ctxt = get_ctxt pt (p, p_)
10.7 - in map ((LItool.tac_from_prog pt thy) o Program.rep_stacexpr o #1 o
10.8 + in map ((LItool.tac_from_prog (pt, pos) thy) o Program.rep_stacexpr o #1 o
10.9 (LItool.check_leaf "selrul" ctxt prog_rls subst)) (Auto_Prog.stacpbls sc)
10.10 end;
10.11
10.12 @@ -69,7 +69,7 @@
10.13 |> LItool.check_leaf "selrul" ctxt prog_rls (env, (a, v))
10.14 |> #1
10.15 |> Program.rep_stacexpr
10.16 - |> LItool.tac_from_prog pt thy)
10.17 + |> LItool.tac_from_prog (pt, pos) thy)
10.18 val f =
10.19 (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
10.20 | _ => raise ERROR "specific_from_prog 3")
11.1 --- a/src/Tools/isac/Specify/Specify.thy Sun Dec 04 16:48:06 2022 +0100
11.2 +++ b/src/Tools/isac/Specify/Specify.thy Thu Dec 08 10:16:40 2022 +0100
11.3 @@ -19,6 +19,7 @@
11.4 ML_file "cas-command.sml"
11.5 ML_file "p-spec.sml"
11.6 ML_file specify.sml
11.7 + ML_file "sub-problem.sml"
11.8 ML_file "step-specify.sml"
11.9
11.10 ML \<open>
12.1 --- a/src/Tools/isac/Specify/o-model.sml Sun Dec 04 16:48:06 2022 +0100
12.2 +++ b/src/Tools/isac/Specify/o-model.sml Thu Dec 08 10:16:40 2022 +0100
12.3 @@ -33,7 +33,7 @@
12.4
12.5 val init: theory -> Formalise.model -> Model_Pattern.T -> T
12.6 val values : T -> term list
12.7 - val values': T -> Formalise.model * term list
12.8 + val values': Proof.context -> T -> Formalise.model * term list
12.9 val complete_for: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context
12.10 val associate_input: Proof.context -> m_field(*del?*) -> descriptor * values -> T -> message * single * values
12.11 val associate_input': Proof.context -> m_field -> values -> T -> message * single * values
12.12 @@ -196,12 +196,12 @@
12.13 --match_ags--> O_Model.T
12.14 O_Model.T --values'--> (["equality (1+x=2)", "boundVariable x", "solutions L"], values)
12.15 *)
12.16 -fun values' oris =
12.17 +fun values' ctxt oris =
12.18 let
12.19 fun ori2fmz_vals (_, _, _, dsc, ts) =
12.20 - case \<^try>\<open>((UnparseC.term o Input_Descript.join') (dsc, ts), last_elem ts)\<close> of
12.21 + case \<^try>\<open>(((UnparseC.term_in_ctxt ctxt) o Input_Descript.join') (dsc, ts), last_elem ts)\<close> of
12.22 SOME x => x
12.23 - | NONE => raise ERROR ("ori2fmz_env called with " ^ UnparseC.terms ts)
12.24 + | NONE => raise ERROR ("ori2fmz_env called with " ^ UnparseC.terms_in_ctxt ctxt ts)
12.25 in (split_list o (map ori2fmz_vals)) oris end
12.26
12.27
13.1 --- a/src/Tools/isac/Specify/specify.sml Sun Dec 04 16:48:06 2022 +0100
13.2 +++ b/src/Tools/isac/Specify/specify.sml Thu Dec 08 10:16:40 2022 +0100
13.3 @@ -215,8 +215,8 @@
13.4 | _ => raise ERROR "do_all: uncovered case get_obj"
13.5 val ctxt = Ctree.get_ctxt pt pos
13.6 val {model, ...} = MethodC.from_store ctxt mI
13.7 - val (_, vals) = O_Model.values' pors
13.8 - val ctxt = ContextC.initialise dI vals
13.9 + val (_, vals) = O_Model.values' ctxt pors
13.10 + val ctxt = ContextC.initialise ctxt vals
13.11 val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),
13.12 map (I_Model.complete' model) pors, map (I_Model.complete' model) pors, ctxt)
13.13 in
14.1 --- a/src/Tools/isac/Specify/step-specify.sml Sun Dec 04 16:48:06 2022 +0100
14.2 +++ b/src/Tools/isac/Specify/step-specify.sml Thu Dec 08 10:16:40 2022 +0100
14.3 @@ -231,7 +231,7 @@
14.4 val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
14.5 in (pI, (pors, pctxt), mI) end;
14.6 val {cas, model, thy = thy', ...} = Problem.from_store ctxt pI (*take dI from _refined_ pbl*)
14.7 - val dI = Context.theory_name (ThyC.sub_common (thy, thy'))
14.8 + val dI = Context.theory_name (Sub_Problem.common_sub_thy (thy, thy'))
14.9 val hdl = case cas of
14.10 NONE => Auto_Prog.pblterm dI pI
14.11 | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t
15.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Sun Dec 04 16:48:06 2022 +0100
15.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Thu Dec 08 10:16:40 2022 +0100
15.3 @@ -5,7 +5,7 @@
15.4 The structure of methods and problems is independent from theories' deductive
15.5 structure. The respective structures are built in Build_Thydata.thy.
15.6 *)
15.7 -signature KESTORE_ELEMS =
15.8 +signature KNOW_STORE =
15.9 sig
15.10 val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
15.11 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
15.12 @@ -14,7 +14,7 @@
15.13 (*etc*)
15.14 end;
15.15
15.16 -structure Test_KEStore_Elems: KESTORE_ELEMS =
15.17 +structure Test_KEStore_Elems: KNOW_STORE =
15.18 struct
15.19 fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
15.20 structure Data = Theory_Data (
16.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Sun Dec 04 16:48:06 2022 +0100
16.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Thu Dec 08 10:16:40 2022 +0100
16.3 @@ -26,7 +26,7 @@
16.4 "----------- fun initialise --------------------------------------------------------------------";
16.5 "----------- fun initialise --------------------------------------------------------------------";
16.6 val t = @{term "a * b + - 123 * c :: real"};
16.7 -val ctxt = initialise "Rational" (vars t)
16.8 +val ctxt = initialise @{context} (vars t)
16.9
16.10 (*----- now parsing infers the type *)
16.11 val SOME t = parseNEW ctxt "x";
17.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sun Dec 04 16:48:06 2022 +0100
17.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Thu Dec 08 10:16:40 2022 +0100
17.3 @@ -870,7 +870,7 @@
17.4 autoCalculate 1 CompleteCalc;
17.5
17.6 val ((pt,_),_) = States.get_calc 1;
17.7 - rootthy pt;
17.8 + root_thy pt;
17.9 Test_Tool.show_pt pt;
17.10 val p = States.get_pos 1 1;
17.11 val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
18.1 --- a/test/Tools/isac/Interpret/li-tool.sml Sun Dec 04 16:48:06 2022 +0100
18.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Thu Dec 08 10:16:40 2022 +0100
18.3 @@ -128,7 +128,7 @@
18.4 ### Tactic.applicable: not impl. for tac = 'Check_elementwise "Assumptions"'
18.5 *)
18.6
18.7 -"~~~~~ fun specific_from_prog , args:"; val (pt, (p, p_)) = (pt, p);
18.8 +"~~~~~ fun specific_from_prog , args:"; val (pt, pos as (p, p_)) = (pt, p);
18.9 (*if*) Pos.on_specification (p, p_) (*else*);
18.10 val pp = par_pblobj pt p
18.11 val thy' = (get_obj g_domID pt pp):ThyC.id
18.12 @@ -142,7 +142,7 @@
18.13 val Pstate ist = get_istate_LI pt (p,p_)
18.14 val ctxt = get_ctxt pt (p, p_)
18.15 val alltacs = (*we expect at least 1 stac in a script*)
18.16 - map ((LItool.tac_from_prog pt thy) o rep_stacexpr o #1 o
18.17 + map ((LItool.tac_from_prog (pt, pos) thy) o rep_stacexpr o #1 o
18.18 (check_leaf "selrul" ctxt prog_rls (get_subst ist) )) (stacpbls sc)
18.19 val f =
18.20 (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
19.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Sun Dec 04 16:48:06 2022 +0100
19.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Dec 08 10:16:40 2022 +0100
19.3 @@ -108,7 +108,7 @@
19.4 check_tac cc ist (prog_tac, form_arg);
19.5 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
19.6 = (cc, ist, (prog_tac, form_arg));
19.7 - val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
19.8 + val m = LItool.tac_from_prog (pt, p) (Proof_Context.theory_of ctxt) prog_tac
19.9 val _ =
19.10 (*case*) m (*of*);
19.11
19.12 @@ -243,7 +243,7 @@
19.13 val (Program.Tac stac, a') =
19.14 (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
19.15 val LItool.Associated (m, v', ctxt) =
19.16 - (*case*) associate pt ctxt (m, stac) (*of*);
19.17 + (*case*) associate (pt, p) ctxt (m, stac) (*of*);
19.18
19.19 Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
19.20 "~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
19.21 @@ -427,13 +427,13 @@
19.22 "~~~~~ fun check_tac1 , args:"; val (((pt, p), ctxt, tac), (ist as {act_arg, or, ...}), (prog_tac, form_arg)) =
19.23 (cct, ist, (prog_tac, form_arg));
19.24 val LItool.Not_Associated = (*case*)
19.25 - LItool.associate pt ctxt (tac, prog_tac) (*of*);
19.26 + LItool.associate (pt, p) ctxt (tac, prog_tac) (*of*);
19.27 val _(*ORundef*) = (*case*) or (*of*);
19.28
19.29 -(*+*)Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p);
19.30 +(*+*)Solve_Step.check (LItool.tac_from_prog (pt, p) (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p);
19.31
19.32 val Applicable.Yes m' =
19.33 - (*case*) Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) (*of*);
19.34 + (*case*) Solve_Step.check (LItool.tac_from_prog (pt, p) (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) (*of*);
19.35
19.36 Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
19.37 (*return from check_tac1*);
20.1 --- a/test/Tools/isac/Knowledge/eqsystem-1a.sml Sun Dec 04 16:48:06 2022 +0100
20.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1a.sml Thu Dec 08 10:16:40 2022 +0100
20.3 @@ -196,7 +196,7 @@
20.4 check_tac cc ist (prog_tac, form_arg);
20.5 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
20.6 = (cc, ist, (prog_tac, form_arg));
20.7 - val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
20.8 + val m = LItool.tac_from_prog (pt, p) (Proof_Context.theory_of ctxt) prog_tac
20.9 val _ =
20.10 (*case*) m (*of*); (*tac as string/input*)
20.11
20.12 @@ -340,7 +340,7 @@
20.13 check_tac cc ist (prog_tac, form_arg);
20.14 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
20.15 = (cc, ist, (prog_tac, form_arg));
20.16 - val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
20.17 + val m = LItool.tac_from_prog (pt, p) (Proof_Context.theory_of ctxt) prog_tac
20.18 val _ =
20.19 (*case*) m (*of*);
20.20
21.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Sun Dec 04 16:48:06 2022 +0100
21.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Thu Dec 08 10:16:40 2022 +0100
21.3 @@ -12,7 +12,6 @@
21.4 "----------- fun upd_penv ----------------------------------------------------------------------";
21.5 "----------- fun upd ---------------------------------------------------------------------------";
21.6 "----------- fun upds_envv ---------------------------------------------------------------------";
21.7 -"----------- fun sub_common for ThyC -----------------------------------------------------------";
21.8 "-----------------------------------------------------------------------------------------------";
21.9 "-----------------------------------------------------------------------------------------------";
21.10 "-----------------------------------------------------------------------------------------------";
21.11 @@ -199,25 +198,3 @@
21.12 (Free ("m_", "bool"),[Free (#,#)]),
21.13 (Free ("vs_", "bool List.list"),[# $ # $ Const #])])] : envv *)
21.14
21.15 -"----------- fun sub_common for ThyC -----------------------------------------------------------";
21.16 -"----------- fun sub_common for ThyC -----------------------------------------------------------";
21.17 -"----------- fun sub_common for ThyC -----------------------------------------------------------";
21.18 -val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory Inverse_Z_Transform});
21.19 -if Context.theory_name (ThyC.sub_common (thy1, thy2)) = "Inverse_Z_Transform"
21.20 -then () else error "ThyC.sub_common 1";
21.21 -
21.22 -val (thy1, thy2) = (@{theory Inverse_Z_Transform}, @{theory Partial_Fractions});(* Isac.Inverse_Z_Transform *)
21.23 -if Context.theory_name (ThyC.sub_common (thy1, thy2)) = "Inverse_Z_Transform"
21.24 -then () else error "ThyC.sub_common 2";
21.25 -
21.26 -val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory PolyEq});
21.27 -if Context.theory_name (ThyC.sub_common (thy1, thy2)) = "Isac_Knowledge" then () else error "ThyC.sub_common 3";
21.28 -
21.29 -val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory Isac_Knowledge});
21.30 -if Context.theory_name (ThyC.sub_common (thy1, thy2)) = "Isac_Knowledge" then () else error "ThyC.sub_common 4";
21.31 -
21.32 -val (thy1, thy2) = (@{theory PolyEq}, @{theory Partial_Fractions});
21.33 -if Context.theory_name (ThyC.sub_common (thy1, thy2)) = "Isac_Knowledge" then () else error "ThyC.sub_common 5";
21.34 -
21.35 -val (thy1, thy2) = (@{theory Isac_Knowledge}, @{theory Partial_Fractions});
21.36 -if Context.theory_name (ThyC.sub_common (thy1, thy2)) = "Isac_Knowledge" then () else error "ThyC.sub_common 6";
22.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method-NEXT_STEP.sml Sun Dec 04 16:48:06 2022 +0100
22.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method-NEXT_STEP.sml Thu Dec 08 10:16:40 2022 +0100
22.3 @@ -89,7 +89,7 @@
22.4 LI.check_tac cc ist (prog_tac, form_arg);
22.5 "~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
22.6 = (cc, ist, (prog_tac, form_arg));
22.7 - val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
22.8 + val m = LItool.tac_from_prog (pt, p) (Proof_Context.theory_of ctxt) prog_tac
22.9 val _ =
22.10 (*case*) m (*of*);
22.11
23.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Sun Dec 04 16:48:06 2022 +0100
23.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Dec 08 10:16:40 2022 +0100
23.3 @@ -76,7 +76,7 @@
23.4 (xxx, (ist |> path_down_form ([L, R], a)), e);
23.5 val (Program.Tac stac, a') = (*case*) LItool.check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
23.6 val LItool.Associated (Rewrite_Set' _, _, _) = (*case*)
23.7 - LItool.associate pt ctxt (m, stac) (*of*);
23.8 + LItool.associate (pt, p) ctxt (m, stac) (*of*);
23.9 "~~~~~ fun associate, args:"; val (_, ctxt, (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _))),
23.10 (Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ rls_ $ f_)) = (pt, ctxt, m, stac);
23.11
23.12 @@ -213,26 +213,31 @@
23.13
23.14 (*val m =*)
23.15 Sub_Problem.tac_from_prog pt stac;
23.16 -(*
23.17 "~~~~~ fun tac_from_prog , args:"; val (pt, _, (stac as Const (\<^const_name>\<open>SubProblem\<close>, _) $ spec' $ ags'))
23.18 = (pt, (Proof_Context.theory_of ctxt), stac);
23.19 -*)
23.20 val (dI, pI, mI) = Prog_Tac.dest_spec spec'
23.21 - val ctxt = Proof_Context.init_global (ThyC.get_theory dI)
23.22 - val thy = ThyC.sub_common (ThyC.get_theory dI, rootthy pt);
23.23 + val thy = Sub_Problem.common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt);
23.24 + val init_ctxt = Proof_Context.init_global thy
23.25 val ags = TermC.isalist2list ags';
23.26 - (*if*) mI = ["no_met"] (*else*);
23.27 val (pI, pors, mI) =
23.28 - (pI, (M_Match.arguments thy ((#model o (Problem.from_store ctxt)) pI) ags)
23.29 - handle ERROR "actual args do not match formal args"
23.30 - => (M_Match.arguments_msg ctxt pI stac ags(*raise exn*); []), mI)
23.31 - val (fmz_, vals) = O_Model.values' pors;
23.32 - val {cas, model, thy,...} = Problem.from_store ctxt pI
23.33 - val dI = Context.theory_name thy (*.take dI from _refined_ pbl.*)
23.34 - val dI = Context.theory_name (ThyC.sub_common (ThyC.get_theory dI, rootthy pt));
23.35 - val ctxt = ContextC.initialise dI (map TermC.vars vals |> flat |> distinct op =);
23.36 -
23.37 -
23.38 + if mI = ["no_met"]
23.39 + then
23.40 + let
23.41 + val pors = (M_Match.arguments thy ((#model o (Problem.from_store init_ctxt)) pI) ags): O_Model.T
23.42 + handle ERROR "actual args do not match formal args"
23.43 + => (M_Match.arguments_msg init_ctxt pI stac ags (*raise exn*);[]);
23.44 + val pI' = Refine.refine_ori' init_ctxt pors pI;
23.45 + in (pI', pors (* refinement over models with diff.prec only *),
23.46 + (hd o #solve_mets o Problem.from_store init_ctxt) pI') end
23.47 + else (pI, (M_Match.arguments thy ((#model o Problem.from_store init_ctxt) pI) ags)
23.48 + handle ERROR "actual args do not match formal args"
23.49 + => (M_Match.arguments_msg init_ctxt pI stac ags(*raise exn*); []), mI);
23.50 + val (fmz_, vals) = O_Model.values' init_ctxt pors;
23.51 + val {cas, model, thy, ...} = Problem.from_store init_ctxt pI
23.52 + val dI = Context.theory_name thy (*take dI from _refined_ pbl*)
23.53 + val dI = Context.theory_name
23.54 + (Sub_Problem.common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt))
23.55 + val ctxt = ContextC.initialise init_ctxt vals
23.56
23.57 (*-------------------- stop step into Rewrite_Set "Test_simplify" ----------------------------*)
23.58 (*\\------------------ step into Rewrite_Set "Test_simplify" -------------------------------//*)
24.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Sun Dec 04 16:48:06 2022 +0100
24.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Dec 08 10:16:40 2022 +0100
24.3 @@ -1,9 +1,11 @@
24.4 -(*//------------------ begin step into ------------------------------------------------------\\*)
24.5 -(*\\------------------ end step into --------------------------------------------------------//*)
24.6 (* Title: "Minisubpbl/300-init-subpbl.sml"
24.7 Author: Walther Neuper 1105
24.8 (c) copyright due to lincense terms.
24.9 *)
24.10 +open LI;
24.11 +open LItool;
24.12 +open Step;
24.13 +open Istate;
24.14
24.15 "----------- Minisubpbl/300-init-subpbl.sml ----------------------";
24.16 "----------- Minisubpbl/300-init-subpbl.sml ----------------------";
24.17 @@ -20,17 +22,143 @@
24.18 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
24.19 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
24.20 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
24.21 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "norm_equation"*)
24.22 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify" *)
24.23 -(*[2], Res*)val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; (*nxt = ("Subproblem"*)
24.24 -(*//--1 begin step into relevant call ----------- \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> ^-----\\
24.25 - 1 relevant for updating ctxt *)
24.26 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
24.27 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "norm_equation" *)
24.28 +(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify" *)
24.29 +(*[2], Res*)val (p'''',_,f,nxt'''',_,pt'''') = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
24.30
24.31 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
24.32 + val ctxt = Ctree.get_ctxt pt p
24.33 +val ("ok", (_, _, ptp as (pt, p))) =
24.34 + (*case*) Step.by_tactic tac (pt, p) (*of*);
24.35 +
24.36 + (*case*)
24.37 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
24.38 +(*//------------------ step into do_next ---------------------------------------------------\\*)
24.39 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
24.40 + (p, ((pt, Pos.e_pos'), []));
24.41 + (*if*) Pos.on_calc_end ip (*else*);
24.42 + val (_, probl_id, _) = Calc.references (pt, p);
24.43 +val _ =
24.44 + (*case*) tacis (*of*);
24.45 + (*if*) probl_id = Problem.id_empty (*else*);
24.46 +
24.47 + switch_specify_solve p_ (pt, ip);
24.48 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
24.49 + (*if*) Pos.on_specification ([], state_pos) (*else*);
24.50 +
24.51 + LI.do_next (pt, input_pos);
24.52 +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
24.53 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
24.54 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
24.55 +
24.56 + (*case*)
24.57 + LI.find_next_step sc (pt, pos) ist ctxt (*of*);
24.58 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt) =
24.59 + (sc, (pt, pos), ist, ctxt);
24.60 + (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
24.61 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) =
24.62 + ((prog, (ptp, ctxt)), (Pstate ist));
24.63 + (*if*) path = [] (*else*);
24.64 +
24.65 + go_scan_up (prog, cc) (trans_scan_up ist);
24.66 +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
24.67 + ((prog, cc), (trans_scan_up ist));
24.68 + (*if*) path = [R] (*root of the program body*) (*else*);
24.69 +
24.70 + scan_up pcc (ist |> path_up) (go_up path sc);
24.71 +"~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ _)) =
24.72 + (pcc, (ist |> path_up), (go_up path sc));
24.73 +
24.74 + go_scan_up pcc ist;
24.75 +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
24.76 + (pcc, ist);
24.77 + (*if*) path = [R] (*root of the program body*) (*else*);
24.78 +
24.79 + scan_up pcc (ist |> path_up) (go_up path sc);
24.80 +"~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ _ $ _)) =
24.81 + (pcc, (ist |> path_up), (go_up path sc));
24.82 +
24.83 + go_scan_up pcc ist;
24.84 +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
24.85 + (pcc, ist);
24.86 + (*if*) path = [R] (*root of the program body*) (*else*);
24.87 +
24.88 + scan_up pcc (ist |> path_up) (go_up path sc);
24.89 +"~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ _ $ _ $ _)) =
24.90 + (pcc, (ist |> path_up), (go_up path sc));
24.91 +
24.92 + go_scan_up pcc ist;
24.93 +"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...})) =
24.94 + (pcc, ist);
24.95 + (*if*) path = [R] (*root of the program body*) (*else*);
24.96 +
24.97 + scan_up pcc (ist |> path_up) (go_up path sc);
24.98 +"~~~~~ and scan_up , args:"; val (pcc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _)) =
24.99 + (pcc, (ist |> path_up), (go_up path sc));
24.100 + val (i, body) = check_Let_up ist sc;
24.101 +
24.102 + (*case*) scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
24.103 +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b)))) =
24.104 + (cc, (ist |> path_up_down [R, D] |> upd_env i), body);
24.105 +
24.106 + (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);
24.107 +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t (*fall-through*)) =
24.108 + (cc, (ist |> path_down [L, R]), e);
24.109 +(*+*)val "SubProblem\n (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],\n [''Test'', ''solve_linear''])\n [BOOL e_e, REAL v_v]" =
24.110 +(*+*) UnparseC.term_in_ctxt @{context} e;
24.111 + (*if*) Tactical.contained_in t (*else*);
24.112 +val (Program.Tac prog_tac, form_arg) =
24.113 + (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
24.114 +
24.115 + check_tac cc ist (prog_tac, form_arg);
24.116 +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg)) =
24.117 + (cc, ist, (prog_tac, form_arg));
24.118 +
24.119 + val m =
24.120 + LItool.tac_from_prog (pt, p) (Proof_Context.theory_of ctxt) prog_tac;
24.121 +"~~~~~ fun tac_from_prog , args:"; val ((pt, p), _, (ptac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _)) =
24.122 + ((pt, p), (Proof_Context.theory_of ctxt), prog_tac);
24.123 +
24.124 + fst
24.125 +(Sub_Problem.tac_from_prog (pt, p) ptac);
24.126 +"~~~~~ fun tac_from_prog , args:"; val ((pt, p), (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ spec' $ ags')) =
24.127 + ((pt, p), ptac);
24.128 + val (dI, pI, mI) = Prog_Tac.dest_spec spec'
24.129 + val thy = Sub_Problem.common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt);
24.130 + val init_ctxt = Proof_Context.init_global thy
24.131 + val ags = TermC.isalist2list ags';
24.132 + val (pI, pors, mI) =
24.133 + if mI = ["no_met"]
24.134 + then
24.135 + let
24.136 + val pors = (M_Match.arguments thy ((#model o (Problem.from_store init_ctxt)) pI) ags): O_Model.T
24.137 + handle ERROR "actual args do not match formal args"
24.138 + => (M_Match.arguments_msg init_ctxt pI stac ags (*raise exn*);[]);
24.139 + val pI' = Refine.refine_ori' init_ctxt pors pI;
24.140 + in (pI', pors (* refinement over models with diff.prec only *),
24.141 + (hd o #solve_mets o Problem.from_store init_ctxt) pI') end
24.142 + else (pI, (M_Match.arguments thy ((#model o Problem.from_store init_ctxt) pI) ags)
24.143 + handle ERROR "actual args do not match formal args"
24.144 + => (M_Match.arguments_msg init_ctxt pI stac ags(*raise exn*); []), mI);
24.145 + val (fmz_, vals) = O_Model.values' init_ctxt pors;
24.146 + val {cas, model, thy, ...} = Problem.from_store init_ctxt pI
24.147 + val dI = Context.theory_name thy (*take dI from _refined_ pbl*)
24.148 + val dI = Context.theory_name
24.149 + (Sub_Problem.common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt))
24.150 + val ctxt = ContextC.initialise init_ctxt vals
24.151 +(*-------------------- stop step into do_next ------------------------------------------------*)
24.152 +(*\\------------------ step into do_next ---------------------------------------------------//*)
24.153 +
24.154 +(*[3], Pbl*)val (p''',_,f,nxt''',_,pt''') = me nxt'''' p'''' [] pt''''; (*Model_Problem*)
24.155 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt'''', p'''', [], pt'''');
24.156 +
24.157 +(*ERROR: Specify_Step.check Model_Problem: uncovered case Ctree.get_obj*)
24.158 val ("ok", (_, _, (pt'''', p''''))) = (*case*)
24.159 Step.by_tactic tac (pt, p) (*of*);
24.160 - get_ctxt pt'''' p'''' |> ContextC.is_empty; (*should NOT be true after this step*)
24.161 -"~~~~~ fun by_tactic , args:"; val (tac, ptp as (pt, p)) = (tac, (pt''',p'''));
24.162 +(*//------------------ step into by_tactic Subproblem --------------------------------------\\*)
24.163 +(*+*)get_ctxt pt'''' p'''' |> ContextC.is_empty; (*should NOT be true after this step*)
24.164 +
24.165 +"~~~~~ fun by_tactic , args:"; val (tac, ptp as (pt, p)) = (tac, (pt, p));
24.166 val Applicable.Yes m = Step.check tac (pt, p);
24.167 (*if*) Tactic.for_specify' m; (*false*)
24.168
24.169 @@ -46,7 +174,7 @@
24.170 "~~~~~ fun locate_input_tactic , args:"; val (Rule.Prog prog, cstate, istate, ctxt, tac)
24.171 = (sc, (pt, po), (fst is), (snd is), m);
24.172
24.173 - val Accept_Tac1 (_, _, Subproblem' (_, _, _, _, _, _)) = (*case*)
24.174 +(** )val Accept_Tac1 (_, _, Subproblem' (_, _, _, _, _, _)) = ( *case*)
24.175 scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
24.176 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Pstate (ist as {path, ...})))
24.177 = ((prog, (cstate, ctxt, tac)), istate);
24.178 @@ -133,24 +261,26 @@
24.179 "~~~~~ from fun locate_input_tactic \<longrightarrow>Step_Solve.by_tactic , return:"; val (LI.Safe_Step (istate, ctxt, tac))
24.180 = (Safe_Step (Pstate ist''''', ctxt''''', tac'_'''''));
24.181 val p' = next_in_prog po
24.182 +
24.183 val (p'', _, _,pt') =
24.184 -
24.185 - Step.add tac (istate, ctxt) (pt, (p', p_));
24.186 + Step.add tac (istate, ctxt) (pt, (p', p_));
24.187 "~~~~~ fun add , args:"; val (thy, (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f)),
24.188 (l as (_, ctxt)), (pos as (p, p_)), pt)
24.189 - = ((ThyC.get_theory "Isac_Knowledge"), tac, (istate, ctxt), (p', p_), pt);
24.190 + = (@{theory}(*ThyC.get_theory "Isac_Knowledge"*), tac, (istate, ctxt), (p', p_), pt);
24.191 val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
24.192 (oris, (domID, pblID, metID), hdl, ctxt_specify);
24.193
24.194 (*+*)if ContextC.is_empty ctxt_specify then error "ERROR: Step.add should NOT get input ContextC.empty" else ();
24.195 (*+*)if (get_ctxt pt pos |> ContextC.is_empty) then error "Step.add MUST store ctxt"
24.196 (*+*)else ();
24.197 -(*\\--1 end step into relevant call ----------------------------------------------------------//*)
24.198 +(*-------------------- stop step into by_tactic Subproblem -----------------------------------*)
24.199 +(*\\------------------ step into by_tactic Subproblem -------------------------------------//*)
24.200
24.201 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''' p''' [1] pt''';(*nxt = Model_Problem*)
24.202 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''' p''' [1] pt''';(*nxt = Add_Given "equality (- 1 + x = 0)"*)
24.203
24.204 -if p = ([3], Pbl) andalso not (get_ctxt pt p |> ContextC.is_empty)
24.205 +(* final test ... ----------------------------------------------------------------------------*)
24.206 +if p''' = ([3], Pbl) andalso not (get_ctxt pt''' p''' |> ContextC.is_empty)
24.207 then
24.208 - case nxt of (Model_Problem) => ()
24.209 + case nxt''' of (Model_Problem) => ()
24.210 | _ => error "minisubpbl: Test_Code.init_calc @{context} has no nxt = Model_Problem"
24.211 else error "Minisubpbl/300-init-subpbl.sml changed";
25.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Sun Dec 04 16:48:06 2022 +0100
25.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Dec 08 10:16:40 2022 +0100
25.3 @@ -88,7 +88,7 @@
25.4 check_leaf "next " ctxt eval (get_subst ist) t;
25.5
25.6 val Check_elementwise "Assumptions" =
25.7 - LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) stac;
25.8 + LItool.tac_from_prog (pt, p) (Proof_Context.theory_of ctxt) stac;
25.9 "~~~~~ fun tac_from_prog , args:"; val (pt, thy, (Const (\<^const_name>\<open>Check_elementwise\<close>, _) $ _ $
25.10 (set as Const (\<^const_name>\<open>Collect\<close>,_) $ Abs (_,_,pred))))
25.11 = (pt, (Proof_Context.theory_of ctxt), stac);
26.1 --- a/test/Tools/isac/Test_Isac.thy Sun Dec 04 16:48:06 2022 +0100
26.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Dec 08 10:16:40 2022 +0100
26.3 @@ -277,10 +277,10 @@
26.4 ML_file "Specify/cas-command.sml"
26.5 ML_file "Specify/p-spec.sml"
26.6 ML_file "Specify/specify.sml"
26.7 + ML_file "Specify/sub-problem.sml"
26.8 ML_file "Specify/step-specify.sml"
26.9
26.10 ML_file "Interpret/istate.sml"
26.11 - ML_file "Interpret/sub-problem.sml"
26.12 ML_file "Interpret/error-pattern.sml"
26.13 ML_file "Interpret/li-tool.sml"
26.14 ML_file "Interpret/lucas-interpreter.sml"