1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Sat Dec 03 19:12:38 2022 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Dec 04 16:48:06 2022 +0100
1.3 @@ -87,8 +87,9 @@
1.4 val get_thes: theory -> (Thy_Write.thydata Store.node) list
1.5 val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory
1.6 val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
1.7 - val get_ref_thy: unit -> theory
1.8 - val set_ref_thy: theory -> unit
1.9 + val get_ref_last_thy: unit -> theory
1.10 + val set_ref_last_thy: theory -> unit
1.11 + val get_via_last_thy: ThyC.id -> theory (* only used for Subproblem retrieving respective thy *)
1.12 end;
1.13
1.14 structure Know_Store(*(*TODO rename to Know_Store*)*): KESTORE_ELEMS(**) =
1.15 @@ -192,9 +193,19 @@
1.16 in Store.update theID theID hthm' end
1.17 in Data.map (fold update_elem fis) thy end
1.18
1.19 - val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
1.20 - fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
1.21 - fun get_ref_thy () = Synchronized.value cur_thy;
1.22 + val last_thy = Synchronized.var "finally_knowledge_complete" @{theory};
1.23 + fun set_ref_last_thy thy = Synchronized.change last_thy (fn _ => thy); (* never RE-set ! *)
1.24 + fun get_ref_last_thy () = Synchronized.value last_thy;
1.25 +
1.26 +fun get_via_last_thy thy_id =
1.27 + let
1.28 + val last_thy = get_ref_last_thy ()
1.29 + val known_thys = Theory.nodes_of last_thy
1.30 + in
1.31 + (find_first (fn thy => Context.theory_name thy = thy_id) known_thys
1.32 + |> the)
1.33 + handle Option.Option => raise ERROR ("get_via_last_thy fails with " ^ quote thy_id)
1.34 + end
1.35
1.36 (**)end(*struct*);
1.37 \<close>
1.38 @@ -254,7 +265,7 @@
1.39 the final theory which comprises all knowledge defined.
1.40 \<close>
1.41 ML \<open>
1.42 -val get_ref_thy = Know_Store.get_ref_thy;
1.43 +val get_ref_last_thy = Know_Store.get_ref_last_thy;
1.44
1.45 (*val get_rew_ord: Proof.context -> string -> Rewrite_Ord.function*)
1.46 fun get_rew_ord ctxt (id: Rewrite_Ord.id) =
1.47 @@ -298,7 +309,7 @@
1.48 case AList.lookup (op =) (Know_Store.get_cass (Proof_Context.theory_of ctxt)) tm of
1.49 SOME refs__gen_fun => refs__gen_fun: References_Def.T * CAS_Def.generate_fn
1.50 | NONE => raise ERROR ("CAS_Cmd \"" ^
1.51 - UnparseC.term_in_thy (get_ref_thy ()) tm ^ "\" missing in theory \"" ^
1.52 + UnparseC.term_in_thy (get_ref_last_thy ()) tm ^ "\" missing in theory \"" ^
1.53 (ctxt |> Proof_Context.theory_of |> Context.theory_name) ^ "\" (and ancestors)" ^
1.54 "\nTODO exception hierarchy needs to be established.")
1.55
1.56 @@ -306,7 +317,7 @@
1.57 (*val get_cas_global: term -> References_Def.T * CAS_Def.generate_fn*)
1.58 fun get_cas_global tm =
1.59 let
1.60 - val thy = get_ref_thy ()
1.61 + val thy = get_ref_last_thy ()
1.62 in
1.63 case AList.lookup (op =) (Know_Store.get_cass thy) tm of
1.64 NONE => (writeln ("CAS_Cmd \"" ^
1.65 @@ -317,10 +328,10 @@
1.66 end
1.67
1.68
1.69 -fun get_pbls () = get_ref_thy () |> Know_Store.get_pbls;
1.70 -fun get_mets () = get_ref_thy () |> Know_Store.get_mets;
1.71 -fun get_thes () = get_ref_thy () |> Know_Store.get_thes;
1.72 -fun get_expls () = get_ref_thy () |> Know_Store.get_expls;
1.73 +fun get_pbls () = get_ref_last_thy () |> Know_Store.get_pbls;
1.74 +fun get_mets () = get_ref_last_thy () |> Know_Store.get_mets;
1.75 +fun get_thes () = get_ref_last_thy () |> Know_Store.get_thes;
1.76 +fun get_expls () = get_ref_last_thy () |> Know_Store.get_expls;
1.77 \<close>
1.78
1.79 rule_set_knowledge
2.1 --- a/src/Tools/isac/Build_Isac.thy Sat Dec 03 19:12:38 2022 +0100
2.2 +++ b/src/Tools/isac/Build_Isac.thy Sun Dec 04 16:48:06 2022 +0100
2.3 @@ -177,6 +177,7 @@
2.4 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method.sml"
2.5 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method-NEXT_STEP.sml"
2.6 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml"
2.7 + ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
2.8 ML \<open>
2.9 \<close> ML \<open>
2.10 \<close> ML \<open>
2.11 @@ -187,7 +188,6 @@
2.12 \<close> ML \<open>
2.13 \<close>
2.14 (*/------- outcomment in order to intermediately check with Test_Isac.thy ------------\(**)
2.15 - ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
2.16 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/300-init-subpbl.sml"
2.17 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml"
2.18 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/450-Rewrite_Set_Inst.sml"
3.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Sat Dec 03 19:12:38 2022 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Sun Dec 04 16:48:06 2022 +0100
3.3 @@ -242,7 +242,7 @@
3.4 insert_errpatIDs @{theory} ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
3.5 (["chain-rule-diff-both", "cancel"]: errpatID list);
3.6 [[[ERROR *** app_py: not found: ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
3.7 - since Know_Store.set_ref_thy has been shifted below;
3.8 + since Know_Store.set_ref_last_thy has been shifted below;
3.9 this ERROR will vanish during re-engineering towards Know_Store.]]]
3.10
3.11 ...and all other related rls by hand;
3.12 @@ -250,6 +250,6 @@
3.13 \<close>
3.14
3.15 section \<open>Link Know_Store to completed IsacKnowledge\<close>
3.16 -ML \<open>Know_Store.set_ref_thy @{theory}\<close>
3.17 +ML \<open>Know_Store.set_ref_last_thy @{theory}\<close>
3.18
3.19 end
4.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Sat Dec 03 19:12:38 2022 +0100
4.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Sun Dec 04 16:48:06 2022 +0100
4.3 @@ -84,10 +84,11 @@
4.4 val lev_dn : CTbasic.Pos.pos -> Pos.pos (* duplicate in ctree-navi.sml *)
4.5 val par_pblobj : CTbasic.ctree -> Pos.pos -> Pos.pos (* duplicate in ctree-navi.sml *)
4.6 ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*)
4.7 +(*from isac_test for Minisubpbl*)
4.8 + val pr_ctree: Proof.context -> (Proof.context -> int list -> ppobj -> string) -> ctree -> string
4.9 + val pr_short: Proof.context -> Pos.pos -> ppobj -> string
4.10
4.11 \<^isac_test>\<open>
4.12 - val pr_ctree : (Pos.pos -> ppobj -> string) -> ctree -> string
4.13 - val pr_short : Pos.pos -> ppobj -> string
4.14 val g_ctxt : ppobj -> Proof.context
4.15 val g_fmz : ppobj -> Model_Def.form_T
4.16 val get_allp : Pos.pos' list -> Pos.pos * (int list * Pos.pos_) -> ctree -> Pos.pos' list
4.17 @@ -249,13 +250,13 @@
4.18
4.19 (** convert ctree to a string **)
4.20
4.21 -\<^isac_test>\<open>
4.22 (* convert a pos from list to string *)
4.23 fun pr_pos ps = (space_implode "." (map string_of_int ps)) ^ ". ";
4.24 (* show hd origin or form only *)
4.25 -fun pr_short p (PblObj _) = pr_pos p ^ " ----- pblobj -----\n"
4.26 - | pr_short p (PrfObj {form = form, ...}) = pr_pos p ^ UnparseC.term form ^ "\n";
4.27 -fun pr_ctree f pt =
4.28 +(**)
4.29 +fun pr_short _ p (PblObj _) = pr_pos p ^ " ----- pblobj -----\n"
4.30 + | pr_short ctxt p (PrfObj {form = form, ...}) = pr_pos p ^ UnparseC.term_in_ctxt ctxt form ^ "\n";
4.31 +fun pr_ctree ctxt f pt =
4.32 let
4.33 fun pr_pt _ _ EmptyPtree = ""
4.34 | pr_pt pfn ps (Nd (b, [])) = pfn ps b
4.35 @@ -263,8 +264,9 @@
4.36 and prts _ _ _ [] = ""
4.37 | prts pfn ps p (t :: ts) = (pr_pt pfn (ps @ [p]) t)^
4.38 (prts pfn ps (p + 1) ts)
4.39 - in pr_pt f [] pt end;
4.40 -\<close>
4.41 + in pr_pt (f ctxt) [] pt end;
4.42 +
4.43 +
4.44
4.45 (** access the branches of ctree **)
4.46
5.1 --- a/test/Tools/isac/BridgeLibisabelle/interface.sml Sat Dec 03 19:12:38 2022 +0100
5.2 +++ b/test/Tools/isac/BridgeLibisabelle/interface.sml Sun Dec 04 16:48:06 2022 +0100
5.3 @@ -82,17 +82,17 @@
5.4 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
5.5 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
5.6 val ((pt,_),_) = States.get_calc 1;
5.7 -writeln(pr_ctree pr_short pt);
5.8 +writeln(pr_ctree ctxt pr_short pt);
5.9 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
5.10 ###########################################################################*)
5.11 val (pt, _) = cut_level__ [] [] pt ([4,1],Frm); (*#*)
5.12 (*##########################################################################*)
5.13 -writeln(pr_ctree pr_short pt);
5.14 +writeln(pr_ctree ctxt pr_short pt);
5.15 (*##########################################################################
5.16 attention: the ctree in states is still the old (perfect) !!!
5.17 ############################################################################*)
5.18
5.19 -writeln(pr_ctree pr_short pt);
5.20 +writeln(pr_ctree ctxt pr_short pt);
5.21 writeln(Test_Tool.posterms2str @{context} (ME_Misc.get_interval ctxt ([],Frm) ([],Res) 99999 pt));
5.22
5.23 case map fst3 (ME_Misc.get_interval ctxt ([],Frm) ([],Res) 99999 pt) of
6.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sat Dec 03 19:12:38 2022 +0100
6.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sun Dec 04 16:48:06 2022 +0100
6.3 @@ -402,7 +402,7 @@
6.4 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
6.5
6.6 val ((pt,_),_) = States.get_calc 1;
6.7 - val str = pr_ctree pr_short pt;
6.8 + val str = pr_ctree ctxt pr_short pt;
6.9 writeln str;
6.10 val ip = States.get_pos 1 1;
6.11 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
6.12 @@ -647,7 +647,7 @@
6.13 autoCalculate 1 CompleteToSubpbl;
6.14 refFormula 1 (States.get_pos 1 1); (*<ISA> - 1 + x = 0 </ISA>*);
6.15 val ((pt,_),_) = States.get_calc 1;
6.16 - val str = pr_ctree pr_short pt;
6.17 + val str = pr_ctree ctxt pr_short pt;
6.18 writeln str;
6.19 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n"
6.20 then () else
6.21 @@ -656,7 +656,7 @@
6.22 autoCalculate 1 (Steps 1); (*proceeds only, if NOT 1 step before subplb*)
6.23 autoCalculate 1 CompleteToSubpbl;
6.24 val ((pt,_),_) = States.get_calc 1;
6.25 - val str = pr_ctree pr_short pt;
6.26 + val str = pr_ctree ctxt pr_short pt;
6.27 writeln str;
6.28 autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
6.29 val ((pt,_),_) = States.get_calc 1;
7.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Sat Dec 03 19:12:38 2022 +0100
7.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Sun Dec 04 16:48:06 2022 +0100
7.3 @@ -63,7 +63,7 @@
7.4
7.5 appendFormula 1 "- 2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (States.get_pos 1 1);
7.6 val ((pt,_),_) = States.get_calc 1;
7.7 - val str = pr_ctree pr_short pt;
7.8 + val str = pr_ctree ctxt pr_short pt;
7.9 if str =
7.10 (". ----- pblobj -----\n" ^
7.11 "1. x + 1 = 2\n" ^
7.12 @@ -183,7 +183,7 @@
7.13
7.14 appendFormula 1 "x = 2" (*|> Future.join*);
7.15 val ((pt,p),_) = States.get_calc 1;
7.16 - val str = pr_ctree pr_short pt;
7.17 + val str = pr_ctree ctxt pr_short pt;
7.18 writeln str;
7.19 if str = ". ----- pblobj -----\n1. x + 1 = 2\n" andalso p = ([1], Res)
7.20 then ()
7.21 @@ -216,7 +216,7 @@
7.22
7.23 appendFormula 1 "x = 1" (*|> Future.join*);
7.24 val ((pt,p),_) = States.get_calc 1;
7.25 - val str = pr_ctree pr_short pt;
7.26 + val str = pr_ctree ctxt pr_short pt;
7.27 writeln str;
7.28 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n3.2. x = 0 + - 1 * - 1\n3.2.1. x = 0 + - 1 * - 1\n3.2.2. x = 0 + 1\n" andalso p = ([3,2], Res)
7.29 then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)
7.30 @@ -245,7 +245,7 @@
7.31 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
7.32 appendFormula 1 "[x = 3 + -2*1]" (*|> Future.join*);
7.33 val ((pt,p),_) = States.get_calc 1;
7.34 - val str = pr_ctree pr_short pt;
7.35 + val str = pr_ctree ctxt pr_short pt;
7.36 writeln str;
7.37 if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n3.2. x = 0 + - 1 * - 1\n4. [x = 1]\n4.1. [x = 1]\n4.2. [x = - 2 + 3]\n4.3. [x = 3 + - 2]\n" then ()
7.38 else error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
7.39 @@ -271,7 +271,7 @@
7.40
7.41 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (States.get_pos 1 1);
7.42 val ((pt,_),_) = States.get_calc 1;
7.43 - val str = pr_ctree pr_short pt;
7.44 + val str = pr_ctree ctxt pr_short pt;
7.45
7.46 (* before AK110725 this was
7.47 ". ----- pblobj -----\n
7.48 @@ -316,7 +316,7 @@
7.49
7.50 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (States.get_pos 1 1);
7.51 val ((pt,_),_) = States.get_calc 1;
7.52 - val str = pr_ctree pr_short pt;
7.53 + val str = pr_ctree ctxt pr_short pt;
7.54 writeln str;
7.55 if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = - 2 + 4\n1.4. x + 1 = - 2 + 4\n" then ()
7.56 else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
7.57 @@ -339,7 +339,7 @@
7.58
7.59 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (States.get_pos 1 1);
7.60 val ((pt,_),_) = States.get_calc 1;
7.61 - val str = pr_ctree pr_short pt;
7.62 + val str = pr_ctree ctxt pr_short pt;
7.63 writeln str;
7.64 if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = - 2 + 4\n1.4. x + 1 = - 2 + 4\n" then ()
7.65 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
7.66 @@ -364,7 +364,7 @@
7.67
7.68 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (States.get_pos 1 1);
7.69 val ((pt,p),_) = States.get_calc 1;
7.70 - val str = pr_ctree pr_short pt;
7.71 + val str = pr_ctree ctxt pr_short pt;
7.72 writeln str;
7.73 if p = ([1], Res) then ()
7.74 else error "inform.sml: diff.behav. cut calculation 2";
7.75 @@ -460,7 +460,7 @@
7.76
7.77 appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
7.78 val ((pt,_),_) = States.get_calc 1;
7.79 - val str = pr_ctree pr_short pt;
7.80 + val str = pr_ctree ctxt pr_short pt;
7.81 writeln str;
7.82 if str = ". ----- pblobj -----\n1. x + 1 = 2\n" then ()
7.83 else error "inform.sml: diff.behav.appendFormula: syntax error";
8.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Sat Dec 03 19:12:38 2022 +0100
8.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Sun Dec 04 16:48:06 2022 +0100
8.3 @@ -288,7 +288,7 @@
8.4
8.5 (*//--------------------- check results from modified me ----------------------------------\\*)
8.6 if p = ([2], Res) andalso
8.7 - pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n"
8.8 + pr_ctree ctxt pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n"
8.9 then
8.10 (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
8.11 | _ => error "")
8.12 @@ -315,7 +315,7 @@
8.13 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
8.14
8.15 (*/--------------------- final test ----------------------------------\\*)
8.16 -if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
8.17 +if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree ctxt pr_short pt =
8.18 ". ----- pblobj -----\n" ^
8.19 "1. x + 1 = 2\n" ^
8.20 "2. x + 1 + - 1 * 2 = 0\n" ^
8.21 @@ -578,7 +578,7 @@
8.22 val (res, asm) = (get_obj g_result pt (fst p));
8.23 if UnparseC.term res = "2 * a" andalso map UnparseC.term asm = []
8.24 andalso p = ([], Und) andalso msg = "end-of-calculation"
8.25 -andalso pr_ctree pr_short pt = ". ----- pblobj -----\n1. a + a\n"
8.26 +andalso pr_ctree ctxt pr_short pt = ". ----- pblobj -----\n1. a + a\n"
8.27 then
8.28 case tac''''' of Check_Postcond ["polynomial", "simplification"] => ()
8.29 | _ => error "re-build: fun find_next_step, mini 1"
8.30 @@ -690,7 +690,7 @@
8.31 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
8.32
8.33 (*/--- final test ---------------------------------------------------------------------------\\*)
8.34 -if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
8.35 +if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree ctxt pr_short pt =
8.36 ". ----- pblobj -----\n" ^
8.37 "1. x + 1 = 2\n" ^
8.38 "2. x + 1 + - 1 * 2 = 0\n" ^
9.1 --- a/test/Tools/isac/Knowledge/diff-app.sml Sat Dec 03 19:12:38 2022 +0100
9.2 +++ b/test/Tools/isac/Knowledge/diff-app.sml Sun Dec 04 16:48:06 2022 +0100
9.3 @@ -221,7 +221,7 @@
9.4 val (pt,_) = cappend_parent(*pbl*) pt pos loc "f_y = d/dy x \<up> 3 ..."
9.5 Empty_Tac TransitiveB;
9.6 "--- 4 ---";
9.7 -writeln (pr_ctree pr_short pt);
9.8 +writeln (pr_ctree ctxt pr_short pt);
9.9
9.10 (*
9.11 . ----- pblobj -----
10.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Sat Dec 03 19:12:38 2022 +0100
10.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Sun Dec 04 16:48:06 2022 +0100
10.3 @@ -610,7 +610,7 @@
10.4 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_plain_square";
10.5
10.6
10.7 -writeln (pr_ctree pr_short pt);
10.8 +writeln (pr_ctree ctxt pr_short pt);
10.9
10.10
10.11
11.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Sat Dec 03 19:12:38 2022 +0100
11.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Sun Dec 04 16:48:06 2022 +0100
11.3 @@ -247,19 +247,20 @@
11.4 ([4], Res)]
11.5 then () else error "ctree.sml: diff:behav. in cut_level 2a";
11.6
11.7 -if pr_ctree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n"
11.8 +val ctxt = @{context}; (* has been overwritten above *)
11.9 +if pr_ctree ctxt pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n"
11.10 then () else error "ctree.sml: diff:behav. in cut_level 2b";
11.11
11.12 val (pt',cuts) = cut_level [] [3] pt ([3,1],Frm);
11.13 if cuts = [([3, 1], Res), ([3, 2], Res)]
11.14 then () else error "ctree.sml: diff:behav. in cut_level 3a";
11.15 -if pr_ctree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n4. [x = 1]\n"
11.16 +if pr_ctree ctxt pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n4. [x = 1]\n"
11.17 then () else error "ctree.sml: diff:behav. in cut_level 3b";
11.18
11.19 val (pt',cuts) = cut_level [] [3] pt ([3,1],Res);
11.20 if cuts = [([3, 2], Res)]
11.21 then () else error "ctree.sml: diff:behav. in cut_level 4a";
11.22 -if pr_ctree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n4. [x = 1]\n"
11.23 +if pr_ctree ctxt pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n4. [x = 1]\n"
11.24 then () else error "ctree.sml: diff:behav. in cut_level 4b";
11.25
11.26
11.27 @@ -728,11 +729,11 @@
11.28 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
11.29 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
11.30 val ((pt,_),_) = States.get_calc 1;
11.31 -writeln(pr_ctree pr_short pt);
11.32 +writeln(pr_ctree ctxt pr_short pt);
11.33 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
11.34 ###########################################################################*)
11.35 val (pt, ppp) = cut_level__ [] [] pt ([4,1],Frm);
11.36 -writeln(pr_ctree pr_short pt);
11.37 +writeln(pr_ctree ctxt pr_short pt);
11.38
11.39
11.40 "-------------- ME_Misc.get_interval from ctree: incremental development--";
11.41 @@ -826,7 +827,7 @@
11.42 (take_fromto (hdp p) (hdq q) (children pt));
11.43 end;
11.44
11.45 -writeln(pr_ctree pr_short pt);
11.46 +writeln(pr_ctree ctxt pr_short pt);
11.47
11.48 case get_trace pt [1,3] [4,1,1] of
11.49 [[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => ()
12.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Sat Dec 03 19:12:38 2022 +0100
12.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Sun Dec 04 16:48:06 2022 +0100
12.3 @@ -30,7 +30,7 @@
12.4 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, ip);
12.5 val (_, (p_', tac)) = Specify.find_next_step ptp
12.6 val ist_ctxt = Ctree.get_loc pt (p, p_)
12.7 - (*val Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
12.8 +(*+*)val Apply_Method ["Test", "squ-equ-test-subpbl1"] = tac;
12.9 val Tactic.Apply_Method mI = (*case*) tac (*of*);
12.10
12.11 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt ptp;
12.12 @@ -42,7 +42,7 @@
12.13 | _ => error "begin_end_prog Apply_Method': uncovered case get_obj"
12.14 val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
12.15 val thy' = get_obj g_domID pt p;
12.16 - val thy = ThyC.get_theory thy';
12.17 + val thy = Know_Store.get_via_last_thy thy';
12.18 val prog_rls = LItool.get_simplifier (pt, pos);
12.19
12.20 (*if*) mI = ["Biegelinien", "ausBelastung"] (*else*);
12.21 @@ -54,7 +54,7 @@
12.22 (*[1], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p''''' ((pt''''', e_pos'), []);(*Rewrite_Set "norm_equation"*)
12.23 case tac of Rewrite_Set "norm_equation" => (
12.24 if p = ([1], Res) then (
12.25 - if pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n" then ()
12.26 + if pr_ctree @{context} pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n" then ()
12.27 else error "Apply_Method [Test, squ-equ-test-subpbl1] changed pt"
12.28 ) else error "Apply_Method [Test, squ-equ-test-subpbl1] changed p")
12.29 | _ => error "Apply_Method [Test, squ-equ-test-subpbl1] changed tac";
13.1 --- a/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Sat Dec 03 19:12:38 2022 +0100
13.2 +++ b/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Sun Dec 04 16:48:06 2022 +0100
13.3 @@ -33,7 +33,7 @@
13.4
13.5 (*+*)case tac of Rewrite_Set "Test_simplify" => (
13.6 (*+*) if p = ([3, 2], Res) then (
13.7 -(*+*) if pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n3.2. x = 0 + - 1 * - 1\n"
13.8 +(*+*) if pr_ctree ctxt pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n3.2. x = 0 + - 1 * - 1\n"
13.9 (*+*) then () else error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed pt"
13.10 (*+*) ) else error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed p")
13.11 (*+*)| _ => error "470-Check_elementwise-NEXT_STEP: Rewrite_Set changed tac";
14.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Sat Dec 03 19:12:38 2022 +0100
14.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Sun Dec 04 16:48:06 2022 +0100
14.3 @@ -153,7 +153,7 @@
14.4 Test_Tool.show_pt pt; (* added ([3,1,1], Frm), ([3,1,1], Res) after ([3,1], Frm)*)
14.5
14.6 (*---------- final test ----------------------------------------------------------\\*)
14.7 -if pr_ctree pr_short pt =
14.8 +if pr_ctree ctxt pr_short pt =
14.9 ". ----- pblobj -----\n1" ^
14.10 ". x + 1 = 2\n" ^
14.11 "2. x + 1 + - 1 * 2 = 0\n" ^
15.1 --- a/test/Tools/isac/Minisubpbl/710-interSteps-short.sml Sat Dec 03 19:12:38 2022 +0100
15.2 +++ b/test/Tools/isac/Minisubpbl/710-interSteps-short.sml Sun Dec 04 16:48:06 2022 +0100
15.3 @@ -56,7 +56,7 @@
15.4 (*+*)Test_Tool.show_pt_tac pt; (* \<up> +++ +++ ([3,2,1], Frm)..([3,2,2], Res) after ([3,1], Res)*)
15.5
15.6 (*---------- final test ----------------------------------------------------------\\*)
15.7 -if pr_ctree pr_short pt =
15.8 +if pr_ctree ctxt pr_short pt =
15.9 ". ----- pblobj -----\n" ^
15.10 "1. x + 1 = 2\n" ^
15.11 "2. x + 1 + - 1 * 2 = 0\n" ^
16.1 --- a/test/Tools/isac/Minisubpbl/790-complete.sml Sat Dec 03 19:12:38 2022 +0100
16.2 +++ b/test/Tools/isac/Minisubpbl/790-complete.sml Sun Dec 04 16:48:06 2022 +0100
16.3 @@ -35,7 +35,7 @@
16.4 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>End_Proof'*)
16.5
16.6 (* final test ...*)
16.7 -if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
16.8 +if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree ctxt pr_short pt =
16.9 ". ----- pblobj -----\n" ^
16.10 "1. x + 1 = 2\n" ^
16.11 "2. x + 1 + - 1 * 2 = 0\n" ^
17.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Sat Dec 03 19:12:38 2022 +0100
17.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Sun Dec 04 16:48:06 2022 +0100
17.3 @@ -356,7 +356,7 @@
17.4 val (pt,pos) = append_result pt pos Istate.empty (TermC.parse_test @{context} ct,[]) Complete;
17.5 Ctree.get_assumptions pt ([],Res);
17.6
17.7 -writeln (pr_ctree pr_short pt);
17.8 +writeln (pr_ctree ctxt pr_short pt);
17.9 (* aus src.24-11-99:
17.10 . sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0)
17.11 1. sqrt(9+4*x)=sqrt x + sqrt(5+x)
17.12 @@ -478,7 +478,7 @@
17.13 val (p,_,f,nxt,_,pt)=
17.14 me ("Check_Postcond",Check_Postcond ("Test", "solve-root-equation")) (p,Met) [17] pt;
17.15 --- *)
17.16 -writeln (pr_ctree pr_short pt);
17.17 +writeln (pr_ctree ctxt pr_short pt);
17.18 writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*;
17.19 *)
17.20
17.21 @@ -614,7 +614,7 @@
17.22 then error "root-equ.sml: diff.behav. in me + tacs input"
17.23 else ();
17.24
17.25 -writeln (pr_ctree pr_short pt);
17.26 +writeln (pr_ctree ctxt pr_short pt);
17.27 writeln("result: "^((UnparseC.term o fst o (get_obj g_result pt)) [])^
17.28 "\n==============================================================");
17.29
18.1 --- a/test/Tools/isac/OLDTESTS/script.sml Sat Dec 03 19:12:38 2022 +0100
18.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Sun Dec 04 16:48:06 2022 +0100
18.3 @@ -235,7 +235,7 @@
18.4 (~1,EdUndef,1,Nundef,
18.5 "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x \<up> 2 + 5 * x)"))
18.6 then () else error "behaviour in root-expl. Free_Solve changed";
18.7 -writeln (pr_ctree pr_short pt);
18.8 +writeln (pr_ctree ctxt pr_short pt);
18.9 ---------------------------------me raises exception with not-locatable*)
18.10
18.11
19.1 --- a/test/Tools/isac/OLDTESTS/tacis.sml Sat Dec 03 19:12:38 2022 +0100
19.2 +++ b/test/Tools/isac/OLDTESTS/tacis.sml Sun Dec 04 16:48:06 2022 +0100
19.3 @@ -26,7 +26,7 @@
19.4 fetchProposedTactic 1 (*'Rewrite_Set Test_simplify' in tacis*);
19.5 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*-1 + x = 0*);
19.6 val ((pt,_),_) = States.get_calc 1;
19.7 - val str = pr_ctree pr_short pt;
19.8 + val str = pr_ctree ctxt pr_short pt;
19.9 writeln str;
19.10
19.11 fetchProposedTactic 1 (*'Subproblem ...' in tacis*);
19.12 @@ -58,7 +58,7 @@
19.13 fetchProposedTactic 1 (*'Rewrite_Set Test_simplify' in tacis*);
19.14 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x = 1*);
19.15 val ((pt,_),_) = States.get_calc 1;
19.16 - val str = pr_ctree pr_short pt;
19.17 + val str = pr_ctree ctxt pr_short pt;
19.18 writeln str;
19.19
19.20 fetchProposedTactic 1 (*'Check_Postcond linear...' in tacis*);
19.21 @@ -99,14 +99,14 @@
19.22 setNextTactic 1 (Rewrite_Set "Test_simplify");
19.23 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*-1 + x = 0*);
19.24 val ((pt,_),_) = States.get_calc 1;
19.25 - val str = pr_ctree pr_short pt;
19.26 + val str = pr_ctree ctxt pr_short pt;
19.27 writeln str;
19.28
19.29 setNextTactic 1 (Subproblem ("Test",["LINEAR", "univariate",
19.30 "equation", "test"]));
19.31 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*solve (-1 + x = 0, x)*);
19.32 val ((pt,_),_) = States.get_calc 1;
19.33 - val str = pr_ctree pr_short pt;
19.34 + val str = pr_ctree ctxt pr_short pt;
19.35 writeln str;
19.36
19.37 setNextTactic 1 (Model_Problem (*["LINEAR", "univariate", "equation", "test"]*));
19.38 @@ -138,7 +138,7 @@
19.39 setNextTactic 1 (Check_elementwise "Assumptions");
19.40 autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*[x = 1]*);
19.41 val ((pt,_),_) = States.get_calc 1;
19.42 - val str = pr_ctree pr_short pt;
19.43 + val str = pr_ctree ctxt pr_short pt;
19.44 writeln str;
19.45
19.46 setNextTactic 1 (Check_Postcond
20.1 --- a/test/Tools/isac/Test_Isac.thy Sat Dec 03 19:12:38 2022 +0100
20.2 +++ b/test/Tools/isac/Test_Isac.thy Sun Dec 04 16:48:06 2022 +0100
20.3 @@ -131,7 +131,10 @@
20.4 open ThmC_Def
20.5 open ThmC
20.6 open Rewrite_Ord
20.7 - open UnparseC
20.8 + open UnparseC;
20.9 +
20.10 + Know_Store.set_ref_last_thy @{theory};
20.11 + (*otherwise ERRORs in pbl-met-hierarchy.sml, refine.sml, evaluate.sml*)
20.12 \<close>
20.13
20.14 ML \<open>
20.15 @@ -184,7 +187,6 @@
20.16 \<close>
20.17
20.18 ML \<open>
20.19 - Know_Store.set_ref_thy @{theory};
20.20 (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
20.21 \<close>
20.22
21.1 --- a/test/Tools/isac/Test_Isac_Short.thy Sat Dec 03 19:12:38 2022 +0100
21.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Sun Dec 04 16:48:06 2022 +0100
21.3 @@ -132,7 +132,10 @@
21.4 open ThmC_Def
21.5 open ThmC
21.6 open Rewrite_Ord
21.7 - open UnparseC
21.8 + open UnparseC;
21.9 +
21.10 + Know_Store.set_ref_last_thy @{theory};
21.11 + (*otherwise ERRORs in pbl-met-hierarchy.sml, refine.sml, evaluate.sml*)
21.12 \<close>
21.13
21.14 ML \<open>
21.15 @@ -185,7 +188,6 @@
21.16 \<close>
21.17
21.18 ML \<open>
21.19 - Know_Store.set_ref_thy @{theory};
21.20 (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
21.21 \<close>
21.22
22.1 --- a/test/Tools/isac/Test_Some.thy Sat Dec 03 19:12:38 2022 +0100
22.2 +++ b/test/Tools/isac/Test_Some.thy Sun Dec 04 16:48:06 2022 +0100
22.3 @@ -46,9 +46,11 @@
22.4 open ThmC_Def
22.5 open ThmC
22.6 open Rewrite_Ord
22.7 - open UnparseC
22.8 + open UnparseC;
22.9 +
22.10 + Know_Store.set_ref_last_thy @{theory};
22.11 + (*otherwise ERRORs in pbl-met-hierarchy.sml, refine.sml, evaluate.sml*)
22.12 \<close>
22.13 -(**)ML_file "BridgeJEdit/vscode-example.sml"(**)
22.14
22.15 section \<open>code for copy & paste ===============================================================\<close>
22.16 ML \<open>
23.1 --- a/test/Tools/isac/Test_Some_meld.thy Sat Dec 03 19:12:38 2022 +0100
23.2 +++ b/test/Tools/isac/Test_Some_meld.thy Sun Dec 04 16:48:06 2022 +0100
23.3 @@ -23,8 +23,10 @@
23.4 open Eval; get_pair;
23.5 open TermC; atomt;
23.6 open Rule; ThmC.string_of_thm;
23.7 +
23.8 + Know_Store.set_ref_last_thy @{theory};
23.9 + (*otherwise ERRORs in pbl-met-hierarchy.sml, refine.sml, evaluate.sml*)
23.10 \<close>
23.11 -ML_file "BaseDefinitions/libraryC.sml"
23.12
23.13 section \<open>code for copy & paste ===============================================================\<close>
23.14 ML \<open>
23.15 @@ -53,12 +55,6 @@
23.16 declare [[ML_print_depth = 999]]
23.17 declare [[ML_exception_trace]]
23.18 \<close>
23.19 -ML \<open>
23.20 -(*========== inhibit exn WN130909 TODO =========================================================
23.21 -============ inhibit exn WN130909 TODO ========================================================*)
23.22 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
23.23 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)
23.24 -\<close>
23.25
23.26 section \<open>===================================================================================\<close>
23.27 ML \<open>