eliminate use of Thy_Info 11: arg. ctxt for ThmC.string_of_thm/s
1.1 --- a/src/Tools/isac/BaseDefinitions/error-pattern-def.sml Tue Jan 10 17:07:53 2023 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/error-pattern-def.sml Wed Jan 11 06:06:12 2023 +0100
1.3 @@ -9,7 +9,7 @@
1.4 sig
1.5 eqtype id
1.6 type T = id * term list * thm list
1.7 - val s_to_string : T list -> string
1.8 + val s_to_string : Proof.context -> T list -> string
1.9 val adapt_to_type: Proof.context -> T -> T
1.10
1.11 type fill_in_id
1.12 @@ -28,9 +28,9 @@
1.13 * term list (* error patterns *)
1.14 * thm list (* thms related to error patterns; note that respective lhs
1.15 do not match (which reflects student's error). *)
1.16 -fun errpat2str (id, tms, thms) =
1.17 - "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC_Def.string_of_thms thms
1.18 -fun s_to_string errpats = (strs2str' o (map errpat2str)) errpats
1.19 +fun errpat2str ctxt (id, tms, thms) =
1.20 + "(\"" ^ id ^ "\",\n" ^ UnparseC.terms_in_ctxt ctxt tms ^ ",\n" ^ ThmC_Def.string_of_thms ctxt thms
1.21 +fun s_to_string ctxt errpats = (strs2str' o (map (errpat2str ctxt))) errpats
1.22
1.23 fun adapt_to_type ctxt (id, terms, thms) =
1.24 (id, map (Model_Pattern.adapt_term_to_type ctxt) terms, thms)
2.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml Tue Jan 10 17:07:53 2023 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml Wed Jan 11 06:06:12 2023 +0100
2.3 @@ -59,7 +59,7 @@
2.4
2.5 fun to_string _ Rule_Def.Erule = "Erule"
2.6 | to_string ctxt (Rule_Def.Thm (str, thm)) =
2.7 - "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm_PIDE ctxt thm ^ ")"
2.8 + "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm ctxt thm ^ ")"
2.9 | to_string _ (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
2.10 | to_string _ (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
2.11 | to_string _ (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
3.1 --- a/src/Tools/isac/BaseDefinitions/thmC-def.sml Tue Jan 10 17:07:53 2023 +0100
3.2 +++ b/src/Tools/isac/BaseDefinitions/thmC-def.sml Wed Jan 11 06:06:12 2023 +0100
3.3 @@ -3,7 +3,7 @@
3.4 (c) due to copyright terms
3.5
3.6 Probably this structure can be dropped due to improved reflection in Isabelle.
3.7 -Here is a minimum of code required for theory Know_Store,
3.8 +Here is a minimum of code required for theory Know_Store,
3.9 further code see structure ThmC.
3.10 *)
3.11 signature THEOREM_ISAC_DEF =
3.12 @@ -11,11 +11,8 @@
3.13 type T
3.14 eqtype id
3.15
3.16 - val string_of_thm: thm -> string
3.17 - val string_of_thms: thm list -> string
3.18 -(*stepwise replace ^^^ by vvv and finally rename by eliminating "_PIDE"*)
3.19 - val string_of_thm_PIDE: Proof.context -> thm -> string
3.20 - val string_of_thms_PIDE: Proof.context -> thm list -> string
3.21 + val string_of_thm: Proof.context -> thm -> string
3.22 + val string_of_thms: Proof.context -> thm list -> string
3.23
3.24 (* required in ProgLang BEFORE definition in ---------------vvv *)
3.25 val int_opt_of_string: string -> int option (* belongs to TermC *)
3.26 @@ -29,21 +26,12 @@
3.27 type id = string; (* key into Know_Store, without point *)
3.28 type T = id * Thm.thm;
3.29
3.30 -(*this is from times before the introduction of sessions*)
3.31 -fun string_of_thm thm =
3.32 - let
3.33 - val t = Thm.prop_of thm
3.34 - val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))
3.35 - val ctxt' = Config.put show_markup false ctxt
3.36 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
3.37 -fun string_of_thms thms = (strs2str o (map (string_of_thm))) thms
3.38 -
3.39 -fun string_of_thm_PIDE ctxt thm =
3.40 +fun string_of_thm ctxt thm =
3.41 let
3.42 val t = Thm.prop_of thm
3.43 val ctxt' = Config.put show_markup false ctxt
3.44 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
3.45 -fun string_of_thms_PIDE ctxt thms = (strs2str o (map (string_of_thm_PIDE ctxt))) thms
3.46 +fun string_of_thms ctxt thms = (strs2str o (map (string_of_thm ctxt))) thms
3.47
3.48 fun int_opt_of_string str =
3.49 let
4.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Tue Jan 10 17:07:53 2023 +0100
4.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Wed Jan 11 06:06:12 2023 +0100
4.3 @@ -11,7 +11,7 @@
4.4 sig
4.5 type id = Error_Pattern_Def.id
4.6 type T = Error_Pattern_Def.T
4.7 - val s_to_string : T list -> string
4.8 + val s_to_string : Proof.context -> T list -> string
4.9 val empty: T
4.10
4.11 type fill_in_id = Error_Pattern_Def.fill_in_id
5.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Tue Jan 10 17:07:53 2023 +0100
5.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Wed Jan 11 06:06:12 2023 +0100
5.3 @@ -88,7 +88,7 @@
5.4 else();
5.5 fun msg call ctxt op_ thmC t =
5.6 call ^ ": \n" ^
5.7 - "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm_PIDE ctxt thmC) ^ ")\n" ^
5.8 + "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm ctxt thmC) ^ ")\n" ^
5.9 "but rewrite__ on " ^ quote (UnparseC.term_in_ctxt ctxt t) ^ " \<longrightarrow> NONE";
5.10
5.11 fun rewrite__ ctxt i bdv tless rls put_asm thm ct =
5.12 @@ -199,7 +199,7 @@
5.13 val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
5.14 ((#asm_rls o Rule_Set.rep) rls) put_asm thm' ct;
5.15 val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
5.16 - ThmC.string_of_thm_PIDE ctxt thm' ^ "\" " ^ UnparseC.term_in_ctxt ctxt ct ^ " = NONE")
5.17 + ThmC.string_of_thm ctxt thm' ^ "\" " ^ UnparseC.term_in_ctxt ctxt ct ^ " = NONE")
5.18 val _ = trace_in3 ctxt i "cal1. to" pairopt;
5.19 in the pairopt end
5.20 end
6.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml Tue Jan 10 17:07:53 2023 +0100
6.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Wed Jan 11 06:06:12 2023 +0100
6.3 @@ -14,12 +14,8 @@
6.4 val cut_id: string -> id
6.5 val long_id: T -> long_id
6.6
6.7 - val string_of_thm: thm -> string
6.8 - val string_of_thms: thm list -> string
6.9 -(*stepwise replace ^^^ by vvv and finally rename by eliminating "_PIDE"*)
6.10 -(*val string_of:*)
6.11 - val string_of_thm_PIDE: Proof.context -> thm -> string
6.12 - val string_of_thms_PIDE: Proof.context -> thm list -> string
6.13 + val string_of_thm: Proof.context -> thm -> string
6.14 + val string_of_thms: Proof.context -> thm list -> string
6.15
6.16 val id_of_thm: thm -> id
6.17 val of_thm: thm -> T
6.18 @@ -58,8 +54,6 @@
6.19
6.20 val string_of_thm = ThmC_Def.string_of_thm;
6.21 val string_of_thms = ThmC_Def.string_of_thms;
6.22 -val string_of_thm_PIDE = ThmC_Def.string_of_thm_PIDE;
6.23 -val string_of_thms_PIDE = ThmC_Def.string_of_thms_PIDE;
6.24
6.25 fun id_of_thm thm = thm |> Thm.get_name_hint |> cut_id;
6.26 fun of_thm thm = (id_of_thm thm, thm);
6.27 @@ -80,9 +74,12 @@
6.28 fun is_sym id =
6.29 case Symbol.explode id of "s" :: "y" :: "m" :: "_" :: _ => true
6.30 | _ => false;
6.31 +
6.32 +\<^isac_test>\<open>
6.33 fun id_drop_sym id =
6.34 case Symbol.explode id of "s" :: "y" :: "m" :: "_" :: id => implode id
6.35 | _ => id
6.36 +\<close>
6.37
6.38 (* get the theorem associated with the xstring-identifier;
6.39 if the identifier starts with "sym_" then swap "lhs = rhs" around "=";
6.40 @@ -147,7 +144,7 @@
6.41 val thm' = sym_thm thm
6.42 val thmID' = case Symbol.explode thmID of
6.43 "s" :: "y" :: "m" :: "_" :: id => implode id
6.44 - | "#" :: ":" :: _ => "#: " ^ string_of_thm_PIDE ctxt thm'
6.45 + | "#" :: ":" :: _ => "#: " ^ string_of_thm ctxt thm'
6.46 | _ => "sym_" ^ thmID
6.47 in Rule.Thm (thmID', thm') end
6.48 | make_sym_rule _ (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls)
7.1 --- a/src/Tools/isac/Test_Code/test-tool.sml Tue Jan 10 17:07:53 2023 +0100
7.2 +++ b/src/Tools/isac/Test_Code/test-tool.sml Wed Jan 11 06:06:12 2023 +0100
7.3 @@ -83,7 +83,7 @@
7.4 let val _ =
7.5 case r of
7.6 Rule.Thm (thmid, thm) =>
7.7 - writeln (string_of_int i ^ " Thm (" ^ thmid ^ ", " ^ ThmC.string_of_thm_PIDE ctxt thm ^ ")")
7.8 + writeln (string_of_int i ^ " Thm (" ^ thmid ^ ", " ^ ThmC.string_of_thm ctxt thm ^ ")")
7.9 | Rule.Eval (op_, _) =>
7.10 writeln (string_of_int i ^ " Eval (" ^ op_ ^ ", _)")
7.11 | Rule.Cal1 (op_, _) =>
8.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Tue Jan 10 17:07:53 2023 +0100
8.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Wed Jan 11 06:06:12 2023 +0100
8.3 @@ -1052,7 +1052,7 @@
8.4 {errpats, rew_rls, program = Rule.Prog prog, ...} => (errpats, rew_rls, prog)
8.5 | _ => error "inform: uncovered case of MethodC.from_store ctxt"
8.6 ;
8.7 -(*+*)if Error_Pattern.s_to_string errpats = "[(\"chain-rule-diff-both\",\n[\"d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)\", \"d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)\"],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\", \"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1) * d_d ?bdv ?u\"]]"
8.8 +(*+*)if Error_Pattern.s_to_string ctxt errpats = "[(\"chain-rule-diff-both\",\n[d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u), d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u), d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\", \"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1) * d_d ?bdv ?u\"]]"
8.9 (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3";
8.10
8.11 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
9.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Tue Jan 10 17:07:53 2023 +0100
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,90 +0,0 @@
9.4 -(* Title: test/Tools/isac/build_thydata.sml
9.5 - Author: Walther Neuper, TU Graz, 2010
9.6 - (c) due to copyright terms
9.7 -
9.8 -theory Test_Some imports Isac.Build_Isac begin
9.9 -ML_file "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
9.10 -ML_file "Knowledge/build_thydata.sml"
9.11 -*)
9.12 -
9.13 -"-----------------------------------------------------------------";
9.14 -"-----------------------------------------------------------------";
9.15 -"table of contents -----------------------------------------------";
9.16 -"-----------------------------------------------------------------";
9.17 -"----------- retrieve errpats ------------------------------------";
9.18 -"----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---";
9.19 -"-----------------------------------------------------------------";
9.20 -"-----------------------------------------------------------------";
9.21 -"-----------------------------------------------------------------";
9.22 -val thy = @{theory Build_Thydata}
9.23 -val ctxt = Proof_Context.init_global thy;
9.24 -
9.25 -"----------- retrieve errpats ------------------------------------";
9.26 -"----------- retrieve errpats ------------------------------------";
9.27 -"----------- retrieve errpats ------------------------------------";
9.28 -val {errpats, rew_rls, program = Prog prog, ...} =
9.29 - MethodC.from_store ctxt ["diff", "differentiate_on_R"];
9.30 -case errpats of [("chain-rule-diff-both", _, _)] => ()
9.31 - | _ => error "errpats chain-rule-diff-both changed"
9.32 -
9.33 -"----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---";
9.34 -"----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---";
9.35 -"----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---";
9.36 -(* "declare [[ML_print_depth = 999]]" *before* opening structure ApplicableOLD
9.37 - slows down Know_Store.get_rlss in collect_part in Build_Thydata.thy
9.38 - such, that it hangs (probably due to some full buffer)
9.39 - test below compiled with
9.40 -theory Test_Theory
9.41 -imports "$ISABELLE_ISAC/Knowledge/Isac" "$ISABELLE_ISAC/Interpret/Interpret"
9.42 - "$ISABELLE_ISAC/Knowledge/Test_Build_Thydata"
9.43 -begin
9.44 -*)
9.45 -(*/----- cp from Build_Thydata.thy -----------------------------------------------------------\*)
9.46 - val knowledge_parent = @{theory} (* should be Build_Thydata.thy, replaced by above imports;
9.47 - original = {Pure, .., Inverse_Z_Transform, Isac, Test_Build_Thydata, Build_Thydata:12}
9.48 - here = {Pure, .., Inverse_Z_Transform, Isac, Test_Build_Thydata, Test_Theory:111} *)
9.49 - val proglang_parent = @{theory ProgLang}
9.50 - val allthys = Theory.ancestors_of @{theory};
9.51 - val allthys = filter_out (member Context.eq_thy (* thys for isac bootstrap *)
9.52 - [(*@{theory ProgLang}: required in isacthys' below*) @{theory Interpret}, @{theory MathEngine},
9.53 - @{theory BridgeLibisabelle}, knowledge_parent]) allthys (*["Isac_Knowledge", ..., "Pure"]*)
9.54 - val isabthys' = (*["Complex_Main", "Taylor", .., "Pure"]*)
9.55 - drop ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
9.56 - val isacthys' = (*["Isac_Knowledge", "Inverse_Z_Transform", .., "Know_Store"]*)
9.57 - take ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
9.58 - val knowthys' = (*["Isac_Knowledge", .., "Input_Descript", "Delete"]*)
9.59 - take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys');
9.60 - val progthys' = (*["Program", "Tools", "ListC", "Know_Store"]*)
9.61 - drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys');
9.62 - val isacrlsthms = (*length = 460*)
9.63 - Thy_Hierarchy.thms_of_rlss @{theory} (Know_Store.get_rlss knowledge_parent) : (ThmC.id * thm) list
9.64 - val rlsthmsNOTisac = isacrlsthms (*length = 36*)
9.65 - |> filter (fn (deriv, _) =>
9.66 - member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))
9.67 - : (ThmC.id * thm) list
9.68 -;
9.69 -(*\----- cp from Build_Thydata.thy -----------------------------------------------------------/*)
9.70 -(*val thydata_list = ...*)
9.71 -(map (Thy_Hierarchy.collect_isab "Isabelle") rlsthmsNOTisac); (* OK *)
9.72 -Thy_Hierarchy.collect_part "IsacScripts" proglang_parent progthys'; (* OK *)
9.73 -(*collect_part "IsacKnowledge" knowledge_parent knowthys' (* NOT terminating *)*)
9.74 -
9.75 -"~~~~~ fun collect_part , args:"; val (part, parent, thys) =
9.76 - ("IsacKnowledge", knowledge_parent, knowthys');
9.77 -(map (Thy_Hierarchy.collect_thms part) thys); (* OK *)
9.78 -(*(collect_rlss part (Know_Store.get_rlss parent) thys)(* NOT terminating *)*)
9.79 -(*Know_Store.get_rlss parent (* NOT terminating *)*)
9.80 -
9.81 -"~~~~~ fun get_rlss , args:"; val () = ();
9.82 -parent; (* = {Pure, .., Inverse_Z_Transform, Isac, Test_Build_Thydata, Test_Theory:111}*)
9.83 -
9.84 -(*/----- save time in Test_Isac.thy ----------------------------------------------------------
9.85 -(* rls are stored cumulatively vvv we try them by bisection *)
9.86 -(*Know_Store.get_rlss @{theory Isac_Knowledge} (* NOT terminating *)*)
9.87 -(*Know_Store.get_rlss @{theory Inverse_Z_Transform} (* NOT terminating *)*)
9.88 - Know_Store.get_rlss @{theory Biegelinie}; (* very very very slow *)
9.89 - Know_Store.get_rlss @{theory PolyEq}; (* OK, very very slow *)
9.90 - Know_Store.get_rlss @{theory RootRatEq}; (* OK, very slow *)
9.91 - Know_Store.get_rlss @{theory RootRat}; (* OK, slow *)
9.92 - Know_Store.get_rlss @{theory RootEq}; (* OK *)
9.93 - \----- save time in Test_Isac.thy ----------------------------------------------------------/*)
10.1 --- a/test/Tools/isac/MathEngBasic/thmC.sml Tue Jan 10 17:07:53 2023 +0100
10.2 +++ b/test/Tools/isac/MathEngBasic/thmC.sml Wed Jan 11 06:06:12 2023 +0100
10.3 @@ -25,7 +25,7 @@
10.4 val A = Thm.typ_of_cterm lhs; (* "real"*)
10.5
10.6 val sym_rule = Thm.lift_rule (Thm.cprop_of thm) @{thm sym};
10.7 -if ThmC.string_of_thm sym_rule = "?s1 = ?t1 \<Longrightarrow> ?t1 = ?s1" then () else error "sym_thm 1";
10.8 +if ThmC.string_of_thm ctxt sym_rule = "?s1 = ?t1 \<Longrightarrow> ?t1 = ?s1" then () else error "sym_thm 1";
10.9 val (t, s) = dest_eq_concl sym_rule; (*Var (("t", 1), "?'a1"), Var (("s", 1), "?'a1")*)
10.10
10.11 val instT = TVars.map (K (K A)) (TVars.build (TVars.add_tvars t));
10.12 @@ -39,7 +39,7 @@
10.13 (* = [((("s", 1), "real"), "- 1 * ?z"), ((("t", 1), "real"), "- ?z")] *)
10.14
10.15 val res = Thm.implies_elim (Thm.instantiate (cinstT, cinst) sym_rule) thm;
10.16 -if ThmC.string_of_thm res = "- ?z = - 1 * ?z" then () else error "sym_thm - 1 * ?z = - ?z CHANGED"
10.17 +if ThmC.string_of_thm ctxt res = "- ?z = - 1 * ?z" then () else error "sym_thm - 1 * ?z = - ?z CHANGED"
10.18
10.19
10.20 "----------- fun revert_sym_rule ---------------------------------------------------------------";
10.21 @@ -48,7 +48,7 @@
10.22 "~~~~~ fun revert_sym_rule , args:"; val (thy, (Rule.Thm (id, thm))) =
10.23 (@{theory Isac_Knowledge}, \<^rule_thm_sym>\<open>real_mult_minus1\<close>);
10.24
10.25 -if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm thm = "- ?z1 = - 1 * ?z1" then ()
10.26 +if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm ctxt thm = "- ?z1 = - 1 * ?z1" then ()
10.27 else error "input to revert_sym_rule CHANGED";
10.28
10.29 (*if*) is_sym (cut_id id) (*then*);
10.30 @@ -59,11 +59,11 @@
10.31 val thy = @{theory Isac_Knowledge}
10.32 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy (\<^rule_thm_sym>\<open>real_mult_minus1\<close>)
10.33 ;
10.34 -if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm thm = "- 1 * ?z = - ?z"
10.35 +if thmID = "Poly.real_mult_minus1" andalso ThmC.string_of_thm ctxt thm = "- 1 * ?z = - ?z"
10.36 then () else error "fun revert_sym_rule changed 1";
10.37
10.38 val (Thm (thmID, thm)) = ThmC.revert_sym_rule thy
10.39 (Thm ("real_diff_minus", @{thm real_diff_minus}))
10.40 ;
10.41 -if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm thm = "?a - ?b = ?a + - 1 * ?b"
10.42 +if thmID = "Root.real_diff_minus" andalso ThmC.string_of_thm ctxt thm = "?a - ?b = ?a + - 1 * ?b"
10.43 then () else error "fun revert_sym_rule changed 2"
11.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Tue Jan 10 17:07:53 2023 +0100
11.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Wed Jan 11 06:06:12 2023 +0100
11.3 @@ -143,7 +143,7 @@
11.4 val thm' = sym_thm thm
11.5 val thmID' = case Symbol.explode thmID of
11.6 "s" :: "y" :: "m" :: "_" :: id => implode id
11.7 - | "#" :: ":" :: _ => "#: " ^ string_of_thm_PIDE ctxt thm'
11.8 + | "#" :: ":" :: _ => "#: " ^ string_of_thm ctxt thm'
11.9 | _ => "sym_" ^ thmID;
11.10 (*-------------------- stop step into Derive.steps -------------------------------------------*)
11.11 (*\\------------------ step into Derive.steps ----------------------------------------------//*)
12.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Tue Jan 10 17:07:53 2023 +0100
12.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Wed Jan 11 06:06:12 2023 +0100
12.3 @@ -305,7 +305,7 @@
12.4 |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
12.5 val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs);
12.6
12.7 -if ThmC.string_of_thm eq = "2 + 3 \<equiv> 5" then () else error "calcul 1";
12.8 +if ThmC.string_of_thm ctxt eq = "2 + 3 \<equiv> 5" then () else error "calcul 1";
12.9
12.10 val rhs = Thm.term_of (Thm.rhs_of eq);
12.11 val _ = \<^assert> (is_num rhs);
12.12 @@ -391,7 +391,7 @@
12.13 val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "is_num");
12.14 val t = @{term "9 is_num"};
12.15 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
12.16 -if str = "#is_num_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_num) = True"
12.17 +if str = "#is_num_9_" andalso ThmC.string_of_thm ctxt thm = "(9 is_num) = True"
12.18 then () else error "adhoc_thm 9 is_num changed";
12.19
12.20 case get_calc_prog_id ctxt \<^const_name>\<open>less\<close> of
12.21 @@ -401,7 +401,7 @@
12.22
12.23 val t = @{term "4 < (4 :: real)"};
12.24 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
12.25 -if str = "#less_4_4" andalso ThmC_Def.string_of_thm thm = "(4 < 4) = False"
12.26 +if str = "#less_4_4" andalso ThmC.string_of_thm ctxt thm = "(4 < 4) = False"
12.27 then () else error "adhoc_thm 4 < 4 changed";
12.28
12.29 val SOME t = parseNEW @{context} "a < 4";
12.30 @@ -411,13 +411,13 @@
12.31 val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "PLUS");
12.32 val SOME t = parseNEW @{context} "1 + (2::real)";
12.33 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
12.34 -if str = "#: 1 + 2 = 3" andalso ThmC_Def.string_of_thm thm = "1 + 2 = 3"
12.35 +if str = "#: 1 + 2 = 3" andalso ThmC.string_of_thm ctxt thm = "1 + 2 = 3"
12.36 then () else error "adhoc_thm 1 + 2 changed";
12.37
12.38 val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "DIVIDE");
12.39 val t = @{term "6 / -8 :: real"};
12.40 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
12.41 -if str = "#divide_e6_~8" andalso ThmC_Def.string_of_thm thm = "6 / - 8 = - 3 / 4"
12.42 +if str = "#divide_e6_~8" andalso ThmC.string_of_thm ctxt thm = "6 / - 8 = - 3 / 4"
12.43 then () else error "adhoc_thm 6 / -8 = - 3 / 4 changed";
12.44
12.45 case get_calc_prog_id ctxt "Prog_Expr.ident" of
12.46 @@ -426,12 +426,12 @@
12.47
12.48 val t = @{term "3 =!= (3 :: real)"};
12.49 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
12.50 -if str = "#ident_(3)_(3)" andalso ThmC_Def.string_of_thm thm = "(3 =!= 3) = True"
12.51 +if str = "#ident_(3)_(3)" andalso ThmC.string_of_thm ctxt thm = "(3 =!= 3) = True"
12.52 then () else error "adhoc_thm (3 =!= 3) changed";
12.53
12.54 val t = @{term "\<not> ((4 :: real) + (4 * x + x \<up> 2) =!= 0)"};
12.55 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
12.56 -if str = "#ident_(4 + (4 * x + x \<up> 2))_(0)" andalso ThmC_Def.string_of_thm thm = "(4 + (4 * x + x \<up> 2) =!= 0) = False"
12.57 +if str = "#ident_(4 + (4 * x + x \<up> 2))_(0)" andalso ThmC.string_of_thm ctxt thm = "(4 + (4 * x + x \<up> 2) =!= 0) = False"
12.58 then () else error "adhoc_thm (\<not> (4 + (4 * x + x ^ 2) =!= 0)) changed";
12.59
12.60 "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
13.1 --- a/test/Tools/isac/Test_Isac.thy Tue Jan 10 17:07:53 2023 +0100
13.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Jan 11 06:06:12 2023 +0100
13.3 @@ -254,7 +254,7 @@
13.4 ML_file "Minisubpbl/600-postcond-NEXT_STEP.sml"
13.5 ML_file "Minisubpbl/600-postcond.sml"
13.6 ML_file "Minisubpbl/700-interSteps.sml"
13.7 - ML_file "Minisubpbl/710-interSteps-short.sml"
13.8 + ML_file "Minisubpbl/710-interSteps-short.sml"
13.9 ML_file "Minisubpbl/790-complete-NEXT_STEP.sml"
13.10 ML_file "Minisubpbl/790-complete.sml"
13.11 ML_file "Minisubpbl/800-append-on-Frm.sml"
14.1 --- a/test/Tools/isac/Test_Some.thy Tue Jan 10 17:07:53 2023 +0100
14.2 +++ b/test/Tools/isac/Test_Some.thy Wed Jan 11 06:06:12 2023 +0100
14.3 @@ -120,777 +120,10 @@
14.4 \<close> ML \<open>
14.5 \<close>
14.6
14.7 -section \<open>==================== "Interpret/lucas-interpreter.sml" ============================\<close>
14.8 +section \<open>=============="Interpret/error-pattern.sml"========================================\<close>
14.9 ML \<open>
14.10 \<close> ML \<open>
14.11 -(* Title: "Interpret/lucas-interpreter.sml"
14.12 - Author: Walther Neuper
14.13 - (c) due to copyright terms
14.14 -*)
14.15 -
14.16 -"-----------------------------------------------------------------------------------------------";
14.17 -"table of contents -----------------------------------------------------------------------------";
14.18 -"-----------------------------------------------------------------------------------------------";
14.19 -"----------- Take as 1st stac in program -------------------------------------------------------";
14.20 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
14.21 -"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
14.22 -"----------- re-build: fun find_next_step, mini ------------------------------------------------";
14.23 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
14.24 -"-----------------------------------------------------------------------------------------------";
14.25 -"-----------------------------------------------------------------------------------------------";
14.26 -"-----------------------------------------------------------------------------------------------";
14.27 -
14.28 -\<close> ML \<open> (*--- Take as 1st stac in program ---ERROR: exception PTREE "get_obj: pos = [0] does not exist"*)
14.29 -"----------- Take as 1st stac in program -------------------------------------------------------";
14.30 -"----------- Take as 1st stac in program -------------------------------------------------------";
14.31 -"----------- Take as 1st stac in program -------------------------------------------------------";
14.32 -"compare --- Apply_Method with initial Take by Step.do_next --- in test/../step-solve ----------";
14.33 -val p = e_pos'; val c = [];
14.34 -val (p,_,f,nxt,_,pt) =
14.35 - Test_Code.init_calc @{context}
14.36 - [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
14.37 - ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
14.38 -val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow> Add_Given "functionTerm (x \<up> 2 + 1)"*)
14.39 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.40 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.41 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.42 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.43 -
14.44 -val (p''',_,f,nxt''',_,pt''') = me nxt p c pt; (*nxt'''= Specify_Method ["diff", "integration"]*)
14.45 -(*//------------------- step into me Specify_Method ["diff", "integration"] ---------------\\*)
14.46 -"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt''');
14.47 - val (pt, p) =
14.48 - (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
14.49 - case Step.by_tactic tac (pt, p) of
14.50 - ("ok", (_, _, ptp)) => ptp
14.51 -
14.52 -val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) = (*case*)
14.53 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
14.54 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
14.55 - = (p, ((pt, Pos.e_pos'), []));
14.56 - (*if*) Pos.on_calc_end ip (*else*);
14.57 - val (_, probl_id, _) = Calc.references (pt, p);
14.58 -val _ =
14.59 - (*case*) tacis (*of*);
14.60 - (*if*) probl_id = Problem.id_empty (*else*);
14.61 -
14.62 -val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) =
14.63 - Step.switch_specify_solve p_ (pt, ip);
14.64 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
14.65 - (*if*) Pos.on_specification ([], state_pos) (*then*);
14.66 -
14.67 - Step.specify_do_next (pt, input_pos);
14.68 -"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
14.69 - val (_, (p_', tac)) = Specify.find_next_step ptp
14.70 - val ist_ctxt = Ctree.get_loc pt (p, p_)
14.71 -val Tactic.Apply_Method mI =
14.72 - (*case*) tac (*of*);
14.73 -
14.74 -val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) =
14.75 - LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
14.76 - ist_ctxt (pt, (p, p_'));
14.77 -"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _)))
14.78 - = ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)),
14.79 - ist_ctxt, (pt, (p, p_')));
14.80 - val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
14.81 - PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
14.82 - | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
14.83 - val {model, ...} = MethodC.from_store ctxt mI;
14.84 - val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
14.85 - val prog_rls = LItool.get_simplifier (pt, pos)
14.86 - val (is, env, ctxt, prog) = case LItool.init_pstate prog_rls ctxt itms mI of
14.87 - (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
14.88 - | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate"
14.89 - val ini = LItool.implicit_take prog env;
14.90 - val pos = start_new_level pos
14.91 -val NONE =
14.92 - (*case*) ini (*of*);
14.93 -
14.94 -val Next_Step (iii, ccc, ttt) = (*case*)
14.95 - LI.find_next_step prog (pt, (lev_dn p, Res)) is ctxt (*of*);
14.96 -"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)
14.97 - = (prog, (pt, (lev_dn p, Res)), is, ctxt);
14.98 -
14.99 - (*case*)
14.100 - scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
14.101 -"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
14.102 - = ((prog, (ptp, ctxt)), (Pstate ist));
14.103 - (*if*) path = [] (*then*);
14.104 -
14.105 -val Accept_Tac (ttt, sss, ccc) =
14.106 - scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
14.107 -"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))
14.108 - = (cc, (trans_scan_dn ist), (Program.body_of prog));
14.109 -
14.110 -val Accept_Tac (ttt, sss, ccc) = (*case*)
14.111 - scan_dn cc (ist |> path_down [L, R]) e (*of*);
14.112 -"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
14.113 - = (cc, (ist |> path_down [L, R]), e);
14.114 - (*if*) Tactical.contained_in t (*else*);
14.115 -val (Program.Tac prog_tac, form_arg) =
14.116 - (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
14.117 -
14.118 -val Accept_Tac (ttt, sss, ccc) =
14.119 - check_tac cc ist (prog_tac, form_arg);
14.120 -"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
14.121 - = (cc, ist, (prog_tac, form_arg));
14.122 - val m = LItool.tac_from_prog (pt, p) prog_tac
14.123 -
14.124 -(*//------------------ step into tac_from_prog ---------------------------------------------\\*)
14.125 -(*keep for continuing check_tac ----------------------------*)
14.126 -val return_tac_from_prog = m
14.127 -(* args of tac_from_prog: ---------------------------------\*)
14.128 -(*+*)val ([0], Res) = p (*isa == isa2*);
14.129 -(*+*)pt (*Output isa == isa2*);
14.130 -(*+*)val "([\"\n(f_f, x \<up> 2 + 1)\", \"\n(v_v, x)\"], [R, L, R], empty, NONE, \n??.empty, ORundef, false, false)"
14.131 - = Istate.pstate2str ist (*isa == isa2*)
14.132 -(*+*)val "Take (Integral x \<up> 2 + 1 D x)" = UnparseC.term_in_ctxt @{context} prog_tac (*isa == isa2*)
14.133 -(*+*)val NONE = form_arg (*isa == isa2*)
14.134 -(* args of tac_from_prog: ---------------------------------/*)
14.135 -(* return value ------------------------------------------\*)
14.136 -(*+* )val Take "Integral x \<up> 2 + 1 D x" = m ( *isa <> isa2*)
14.137 -(* return value ------------------------------------------/*)
14.138 -;
14.139 -"~~~~~ fun tac_from_prog , args:"; val ((pt, pos), intac) =
14.140 - ((pt, p), prog_tac);
14.141 -
14.142 -(*+*)val ([0], Res) = pos
14.143 -
14.144 - val pos = Pos.back_from_new pos
14.145 - val ctxt = Ctree.get_ctxt pt pos
14.146 - val thy = Proof_Context.theory_of ctxt
14.147 -(*-------------------- stop step into tac_from_prog ------------------------------------------*)
14.148 -(*\\------------------ step into tac_from_prog ---------------------------------------------//*)
14.149 -
14.150 -val m = return_tac_from_prog (*kept for continuing check_tac*)
14.151 -
14.152 -val _ =
14.153 - (*case*) m (*of*);
14.154 -
14.155 - (*case*)
14.156 -Solve_Step.check m (pt, p) (*of*);
14.157 -"~~~~~ fun check , args:"; val ((Tactic.Take str), (pt, pos as (p_, p))) = (m, (pt, p));
14.158 -
14.159 -(*+*)val ([0], Res) = pos; (*<<<-------------------------*)
14.160 -(*-------------------- stop step into me Specify_Method ["diff", "integration"] -------------*)
14.161 -(*\\------------------- step into me Specify_Method ["diff", "integration"] ---------------//*)
14.162 -
14.163 -val (p,_,f,nxt,_,pt) = me nxt''' p''' c pt''';
14.164 -case nxt of (Apply_Method ["diff", "integration"]) => ()
14.165 - | _ => error "integrate.sml -- me method [diff,integration] -- spec";
14.166 -"----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
14.167 -
14.168 -"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
14.169 -"~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
14.170 -val Applicable.Yes m = Step.check tac (pt, p);
14.171 - (*if*) Tactic.for_specify' m; (*false*)
14.172 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
14.173 -
14.174 -"~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
14.175 - = (m, (pt, pos));
14.176 - val {prog_rls, ...} = MethodC.from_store ctxt mI;
14.177 - val itms = case get_obj I pt p of
14.178 - PblObj {meth=itms, ...} => itms
14.179 - | _ => error "solve Apply_Method: uncovered case get_obj"
14.180 - val thy' = get_obj g_domID pt p;
14.181 - val thy = ThyC.get_theory thy';
14.182 - val prog_rls = LItool.get_simplifier (pt, pos)
14.183 - val (is, env, ctxt, sc) = case LItool.init_pstate prog_rls ctxt itms mI of
14.184 - (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
14.185 - | _ => error "solve Apply_Method: uncovered case init_pstate";
14.186 -(*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)";
14.187 - val ini = LItool.implicit_take sc env;
14.188 - val p = lev_dn p;
14.189 -
14.190 - val NONE = (*case*) ini (*of*);
14.191 - val Next_Step (is', ctxt', m') =
14.192 - LI.find_next_step sc (pt, (p, Res)) is ctxt;
14.193 -(*+*)pstate2str (the_pstate is') = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], empty, NONE, \nIntegral x \<up> 2 + 1 D x, ORundef, false, false)";
14.194 - val Safe_Step (_, _, Take' _) = (*case*)
14.195 - locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
14.196 -"~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)
14.197 - = (sc, (pt, (p, Res)), is', ctxt', m');
14.198 -
14.199 - (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
14.200 -"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
14.201 - = ((prog, (cstate, ctxt, tac)), istate);
14.202 - (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
14.203 -
14.204 - val Accept_Tac1 (_, _, Take' _) =
14.205 - scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
14.206 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
14.207 - = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
14.208 -
14.209 -(*+*) if UnparseC.term e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
14.210 -
14.211 - (*case*)
14.212 - scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
14.213 - (*======= end of scanning tacticals, a leaf =======*)
14.214 -"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t)
14.215 - = (xxx, (ist |> path_down [L, R]), e);
14.216 -val (Program.Tac stac, a') = check_leaf "locate" ctxt eval (get_subst ist) t;
14.217 -
14.218 -
14.219 -
14.220 \<close> ML \<open>
14.221 -\<close> ML \<open> (*--- re-build: fun locate_input_tactic ---NOerror*)
14.222 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
14.223 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
14.224 -"----------- re-build: fun locate_input_tactic -------------------------------------------------";
14.225 -val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
14.226 -val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
14.227 - ["Test", "squ-equ-test-subpbl1"]);
14.228 -val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
14.229 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.230 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.231 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.232 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.233 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.234 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.235 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
14.236 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
14.237 -
14.238 -(*//------------------ begin step into ------------------------------------------------------\\*)
14.239 -(*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
14.240 -
14.241 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
14.242 -
14.243 - (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*)
14.244 - Step.by_tactic tac (pt,p) (*of*);
14.245 -"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
14.246 - val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
14.247 - (*if*) Tactic.for_specify' m; (*false*)
14.248 -
14.249 - (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **)
14.250 -Step_Solve.by_tactic m ptp;
14.251 -"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
14.252 -(*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
14.253 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
14.254 - val thy' = get_obj g_domID pt (par_pblobj pt p);
14.255 - val (is, sc) = LItool.resume_prog (p,p_) pt;
14.256 -
14.257 - locate_input_tactic sc (pt, po) (fst is) (snd is) m;
14.258 -"~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
14.259 - = (sc, (pt, po), (fst is), (snd is), m);
14.260 - val prog_rls = get_simplifier cstate;
14.261 -
14.262 - (** )val Accept_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
14.263 - (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
14.264 -"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
14.265 - = ((prog, (cstate, ctxt, tac)), istate);
14.266 - (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
14.267 -
14.268 - (** )val xxxxx_xx = ( **)
14.269 - scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
14.270 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
14.271 - = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
14.272 -
14.273 - (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
14.274 -"~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const (\<^const_name>\<open>Chain\<close>(*1*), _) $ e1 $ e2 $ a))
14.275 - = (xxx, (ist |> path_down [L, R]), e);
14.276 -
14.277 - (*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
14.278 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
14.279 - = (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
14.280 -
14.281 - (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
14.282 - (*======= end of scanning tacticals, a leaf =======*)
14.283 -"~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
14.284 - = (xxx, (ist |> path_down [R]), e);
14.285 - val (Program.Tac stac, a') =
14.286 - (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
14.287 - val LItool.Associated (m, v', ctxt) =
14.288 - (*case*) associate (pt, p) ctxt (m, stac) (*of*);
14.289 -
14.290 - Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
14.291 -"~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
14.292 - = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
14.293 -
14.294 -"~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac')
14.295 - = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
14.296 - (*if*) LibraryC.assoc (*then*);
14.297 -
14.298 - Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
14.299 -"~~~~~ from locate_input_tactic to fun Step_Solve.by_tactic return:"; val Safe_Step (istate, ctxt, tac)
14.300 - = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
14.301 -
14.302 -(*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *)
14.303 - val (p'', _, _,pt') =
14.304 - Step.add tac (istate, ctxt) (pt, (lev_on p, Pbl));
14.305 - (*in*)
14.306 -
14.307 - ("ok", ([(Tactic.input_from_T ctxt tac, tac, (p'', (istate, ctxt)))],
14.308 - [(*ctree NOT cut*)], (pt', p''))) (*return value*);
14.309 -"~~~~~ from Step_Solve.by_tactic \<longrightarrow> Step.by_tactic return:"; val ((msg, cs' : Calc.state_post))
14.310 - = ("ok", ([(Tactic.input_from_T ctxt tac, tac, (p'', (istate, ctxt)) )],
14.311 - [(*ctree NOT cut*)], (pt', p'')));
14.312 -
14.313 -"~~~~~ from Step.by_tactic to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
14.314 - val (_, ts) =
14.315 - (case Step.do_next p ((pt, Pos.e_pos'), []) of
14.316 - ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
14.317 - | ("helpless", _) => ("helpless: cannot propose tac", [])
14.318 - | ("no-fmz-spec", _) => error "no-fmz-spec"
14.319 - | ("end-of-calculation", (ts, _, _)) => ("", ts)
14.320 - | _ => error "me: uncovered case")
14.321 - handle ERROR msg => raise ERROR msg
14.322 - val tac =
14.323 - case ts of
14.324 - tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
14.325 - | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
14.326 -
14.327 - (p, [] : NEW, TESTg_form ctxt (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
14.328 -"~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
14.329 - = (*** )xxx( ***) (p, [] : NEW, TESTg_form ctxt (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
14.330 -
14.331 -(*//--------------------- check results from modified me ----------------------------------\\*)
14.332 -if p = ([2], Res) andalso
14.333 - pr_ctree ctxt pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n"
14.334 -then
14.335 - (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
14.336 - | _ => error "")
14.337 -else error "check results from modified me CHANGED";
14.338 -(*\\--------------------- check results from modified me ----------------------------------//*)
14.339 -
14.340 -"~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
14.341 -(*\\------------------ end step into --------------------------------------------------------//*)
14.342 -
14.343 -(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
14.344 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
14.345 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
14.346 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
14.347 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
14.348 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
14.349 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
14.350 -(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
14.351 -(*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
14.352 -(*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
14.353 -(*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
14.354 -(*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
14.355 -(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
14.356 -(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
14.357 -(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
14.358 -
14.359 -(*/--------------------- final test ----------------------------------\\*)
14.360 -if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree ctxt pr_short pt =
14.361 - ". ----- pblobj -----\n" ^
14.362 - "1. x + 1 = 2\n" ^
14.363 - "2. x + 1 + - 1 * 2 = 0\n" ^
14.364 - "3. ----- pblobj -----\n" ^
14.365 - "3.1. - 1 + x = 0\n" ^
14.366 - "3.2. x = 0 + - 1 * - 1\n" ^
14.367 - "4. [x = 1]\n"
14.368 -then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
14.369 -else error "re-build: fun locate_input_tactic changed 2";
14.370 -
14.371 -
14.372 -\<close> ML \<open> (*--- fun locate_input_tactic Helpless, NOerror*)
14.373 -"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
14.374 -"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
14.375 -"----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
14.376 -(*cp from -- try fun applyTactics ------- *)
14.377 -val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
14.378 - "normalform N"],
14.379 - ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
14.380 - ["simplification", "for_polynomials", "with_minus"]))];
14.381 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.382 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.383 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.384 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
14.385 -
14.386 -(*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f
14.387 -
14.388 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
14.389 -
14.390 -(*+*)if map (Tactic.input_to_string ctxt) (specific_from_prog pt p) =
14.391 - ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
14.392 - "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
14.393 -(*this is new since ThmC.numerals_to_Free.-----\\*)
14.394 - "Calculate PLUS"]
14.395 - then () else error "specific_from_prog ([1], Res) 1 CHANGED";
14.396 -(*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
14.397 -
14.398 -(*+*)if map (Tactic.input_to_string @{context}) (specific_from_prog pt p) = [
14.399 - "Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")",
14.400 - "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
14.401 - "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
14.402 - (*this is new since ThmC.numerals_to_Free.-----\\*)
14.403 - "Calculate PLUS",
14.404 - (*this is new since ThmC.numerals_to_Free.-----//*)
14.405 - "Calculate MINUS"]
14.406 - then () else error "specific_from_prog ([1], Res) 2 CHANGED";
14.407 -(* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
14.408 -
14.409 -(*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
14.410 -(**)val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
14.411 - Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
14.412 -"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (specific_from_prog pt p), (pt, p));
14.413 - val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
14.414 - (*if*) Tactic.for_specify' m; (*false*)
14.415 -
14.416 -(**) val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
14.417 -Step_Solve.by_tactic m (pt, p);
14.418 -"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
14.419 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
14.420 - val thy' = get_obj g_domID pt (par_pblobj pt p);
14.421 - val (is, sc) = LItool.resume_prog (p,p_) pt;
14.422 -
14.423 - (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
14.424 -"~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
14.425 - = (sc, (pt, po), (fst is), (snd is), m);
14.426 - val prog_rls = LItool.get_simplifier cstate (*TODO: shift into Istate.T*);
14.427 -
14.428 - (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
14.429 -"~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
14.430 - = ((prog, (cstate, ctxt, tac)), istate);
14.431 - (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
14.432 -
14.433 - go_scan_up1 (prog, cctt) ist;
14.434 -"~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
14.435 - = ((prog, cctt), ist);
14.436 - (*if*) 1 < length path (*then*);
14.437 -
14.438 - scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
14.439 -"~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ _))
14.440 - = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
14.441 -
14.442 - go_scan_up1 pcct ist;
14.443 -"~~~~~ and go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
14.444 - = (pcct, ist);
14.445 - (*if*) 1 < length path (*then*);
14.446 -
14.447 - scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
14.448 -"~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist,
14.449 - (Const (\<^const_name>\<open>Chain\<close>(*3*), _) $ _ ))
14.450 - = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
14.451 - val e2 = check_Seq_up ctxt ist prog
14.452 -;
14.453 - (*case*) scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 (*of*);
14.454 -"~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ e1 $ e2))
14.455 - = (cct, (ist |> path_up_down [R] |> set_or ORundef), e2);
14.456 -
14.457 - (*case*) scan_dn1 cct (ist |> path_down [L, R]) e1 (*of*);
14.458 -"~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
14.459 - = (cct, (ist |> path_down [L, R]), e1);
14.460 -
14.461 - (*case*) scan_dn1 cct (ist |> path_down [R]) e (*of*);
14.462 - (*======= end of scanning tacticals, a leaf =======*)
14.463 -"~~~~~ fun scan_dn1 , args:"; val ((cct as (_, ctxt, _)), (ist as {eval, ...}), t)
14.464 - = (cct, (ist |> path_down [R]), e);
14.465 - (*if*) Tactical.contained_in t (*else*);
14.466 - val (Program.Tac prog_tac, form_arg) = (*case*)
14.467 - LItool.check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
14.468 -
14.469 - check_tac1 cct ist (prog_tac, form_arg);
14.470 -"~~~~~ fun check_tac1 , args:"; val (((pt, p), ctxt, tac), (ist as {act_arg, or, ...}), (prog_tac, form_arg)) =
14.471 - (cct, ist, (prog_tac, form_arg));
14.472 -val LItool.Not_Associated = (*case*)
14.473 - LItool.associate (pt, p) ctxt (tac, prog_tac) (*of*);
14.474 - val _(*ORundef*) = (*case*) or (*of*);
14.475 -
14.476 -\<close> ML \<open> (*LItool.tac_from_prog.. corrected arg, WITHOUT ERROR BELOW..*)
14.477 -(*+*)Solve_Step.check (LItool.tac_from_prog (pt, p)prog_tac) (pt, p);
14.478 -
14.479 - val Applicable.Yes m' =
14.480 - (*case*) Solve_Step.check (LItool.tac_from_prog (pt, p) prog_tac) (pt, p) (*of*);
14.481 -
14.482 - Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
14.483 - (*return from check_tac1*);
14.484 -"~~~~~ from fun check_tac1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun locate_input_tactic , return:"; val (Reject_Tac1 _) =
14.485 - (Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac));
14.486 -
14.487 -val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f;
14.488 -val ([3], Res) = p;
14.489 -
14.490 -
14.491 -\<close> ML \<open> (*--- re-build: fun find_next_step, mini --NOerror*)
14.492 -"----------- re-build: fun find_next_step, mini ------------------------------------------------";
14.493 -"----------- re-build: fun find_next_step, mini ------------------------------------------------";
14.494 -"----------- re-build: fun find_next_step, mini ------------------------------------------------";
14.495 -val fmz = ["Term (a + a ::real)", "normalform n_n"];
14.496 -val (dI',pI',mI') = ("Poly",["polynomial", "simplification"],["simplification", "for_polynomials"]);
14.497 -val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
14.498 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*)
14.499 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory "Poly"*)
14.500 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["polynomial", "simplification"]*)
14.501 -(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["simplification", "for_polynomials"]*)
14.502 -(*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["simplification", "for_polynomials"]*)
14.503 -(*[1], Res*)val (_, ([(tac'''''_', _, _)], _, (pt'''''_', p'''''_'))) =
14.504 -
14.505 - Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_Poly"*)
14.506 -(*//------------------ go into 1 ------------------------------------------------------------\\*)
14.507 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
14.508 - = (p, ((pt, e_pos'), []));
14.509 - val pIopt = Ctree.get_pblID (pt, ip);
14.510 - (*if*) ip = ([], Res) (*else*);
14.511 - val _ = (*case*) tacis (*of*);
14.512 - val SOME _ = (*case*) pIopt (*of*);
14.513 - (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
14.514 -
14.515 -val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) =
14.516 -Step_Solve.do_next (pt, ip);
14.517 -"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
14.518 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
14.519 - val thy' = get_obj g_domID pt (par_pblobj pt p);
14.520 - val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
14.521 -
14.522 -val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) =
14.523 - LI.find_next_step sc (pt, pos) ist ctxt (*of*);
14.524 -"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
14.525 - = (sc, (pt, pos), ist, ctxt);
14.526 -
14.527 -val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
14.528 - (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
14.529 -"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
14.530 - = ((prog, (ptp, ctxt)), (Pstate ist));
14.531 - (*if*) path = [] (*then*);
14.532 -
14.533 -val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
14.534 - scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
14.535 -"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
14.536 - = (cc, (trans_scan_dn ist), (Program.body_of prog));
14.537 - (*if*) Tactical.contained_in t (*else*);
14.538 - val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
14.539 -
14.540 -val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
14.541 - check_tac cc ist (prog_tac, form_arg) (*return from xxx*);
14.542 -"~~~~~ from fun scan_dn\<longrightarrow>fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Accept_Tac (tac, ist, ctxt))
14.543 - = (check_tac cc ist (prog_tac, form_arg));
14.544 -
14.545 - Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac) (*return from find_next_step*);
14.546 -"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (Next_Step (ist, ctxt, tac))
14.547 - = (Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac));
14.548 -
14.549 - LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp (*return from and do_next*);
14.550 -"~~~~~ from and do_next\<longrightarrow>fun do_next\<longrightarrow>toplevel, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
14.551 - = (LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp);
14.552 -(*\\------------------ end of go into 1 -----------------------------------------------------//*)
14.553 -
14.554 -(*[], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) =
14.555 -
14.556 - Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []);(* Check_Postcond ["polynomial", "simplification"]*)
14.557 -(*//------------------ go into 2 ------------------------------------------------------------\\*)
14.558 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
14.559 - = (p''''', ((pt''''', e_pos'), []));
14.560 - val pIopt = Ctree.get_pblID (pt, ip);
14.561 - (*if*) ip = ([], Res) (*else*);
14.562 - val _ = (*case*) tacis (*of*);
14.563 - val SOME _ = (*case*) pIopt (*of*);
14.564 - (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
14.565 -
14.566 -val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) =
14.567 -Step_Solve.do_next (pt, ip);
14.568 -"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
14.569 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
14.570 - val thy' = get_obj g_domID pt (par_pblobj pt p);
14.571 - val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
14.572 -
14.573 - (** )val End_Program (ist, tac) =
14.574 - ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
14.575 -"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
14.576 - = (sc, (pt, pos), ist, ctxt);
14.577 -
14.578 -(* val Term_Val (Const (\<^const_name>\<open>times\<close>, _) $ Free ("2", _) $ Free ("a", _))*)
14.579 - (**)val Term_Val prog_result =
14.580 - (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
14.581 -"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
14.582 - = ((prog, (ptp, ctxt)), (Pstate ist));
14.583 - (*if*) path = [] (*else*);
14.584 -
14.585 - go_scan_up (prog, cc) (trans_scan_up ist |> set_found);
14.586 -"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
14.587 - = ((prog, cc), (trans_scan_up ist(*|> set_found !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)));
14.588 - (*if*) path = [R] (*then*);
14.589 - (*if*) found_accept = true (*then*);
14.590 -
14.591 - Term_Val act_arg (*return from go_scan_up*);
14.592 -"~~~~~ from fun go_scan_up\<longrightarrow>fun scan_to_tactic, return:"; val (Term_Val prog_result) = (Term_Val act_arg);
14.593 -
14.594 - Term_Val prog_result (*return from scan_to_tactic*);
14.595 -"~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result);
14.596 - val (true, p' as [], Rule_Set.Empty, _) = (*case*) parent_node pt pos (*of*);
14.597 - val (_, pblID, _) = get_obj g_spec pt p';
14.598 -
14.599 - End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))
14.600 - (*return from find_next_step*);
14.601 -"~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (End_Program (ist, tac))
14.602 - = (End_Program (Pstate ist, Tactic.Check_Postcond' (pblID,prog_result)));
14.603 - val _ = (*case*) tac (*of*);
14.604 -
14.605 -val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res))))
14.606 - = LI.by_tactic tac (ist, ctxt) ptp (*return from and do_next*);
14.607 -"~~~~~ from and do_next\<longrightarrow>top level, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
14.608 - = (LI.by_tactic tac (ist, ctxt) ptp);
14.609 -(*\\------------------ end of go into 2 -----------------------------------------------------//*)
14.610 -
14.611 -(*[], Und*)val (msg, ([], _, (pt, p))) = Step.do_next p''''' ((pt''''', Pos.e_pos'), []);(**)
14.612 -
14.613 -Test_Tool.show_pt_tac pt; (*[
14.614 -([], Frm), Simplify (a + a)
14.615 -. . . . . . . . . . Apply_Method ["simplification", "for_polynomials"],
14.616 -([1], Frm), a + a
14.617 -. . . . . . . . . . Rewrite_Set "norm_Poly",
14.618 -([1], Res), 2 * a
14.619 -. . . . . . . . . . Check_Postcond ["polynomial", "simplification"],
14.620 -([], Res), 2 * a]*)
14.621 -
14.622 -(*/--- final test ---------------------------------------------------------------------------\\*)
14.623 -val (res, asm) = (get_obj g_result pt (fst p));
14.624 -if UnparseC.term res = "2 * a" andalso map UnparseC.term asm = []
14.625 -andalso p = ([], Und) andalso msg = "end-of-calculation"
14.626 -andalso pr_ctree ctxt pr_short pt = ". ----- pblobj -----\n1. a + a\n"
14.627 -then
14.628 - case tac''''' of Check_Postcond ["polynomial", "simplification"] => ()
14.629 - | _ => error "re-build: fun find_next_step, mini 1"
14.630 -else error "re-build: fun find_next_step, mini 2"
14.631 -
14.632 -
14.633 -\<close> ML \<open> (*--- re-build: fun locate_input_term ---NOerror*)
14.634 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
14.635 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
14.636 -"----------- re-build: fun locate_input_term ---------------------------------------------------";
14.637 -(*cp from inform.sml
14.638 - ----------- appendFormula: on Res + late deriv ------------------------------------------------*)
14.639 -val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
14.640 -val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
14.641 - ["Test", "squ-equ-test-subpbl1"]);
14.642 -val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
14.643 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.644 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.645 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.646 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.647 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.648 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.649 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["Test", "squ-equ-test-subpbl1"]*);
14.650 -
14.651 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "norm_equation"*)
14.652 -(*+*)if f2str f = "x + 1 = 2" then () else error "locate_input_term at ([1], Frm) CHANGED";
14.653 -
14.654 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "Test_simplify"*)
14.655 -(*+*)if f2str f = "x + 1 + - 1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED";
14.656 -
14.657 -Test_Tool.show_pt_tac pt; (*[
14.658 -([], Frm), solve (x + 1 = 2, x)
14.659 -. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
14.660 -([1], Frm), x + 1 = 2
14.661 -. . . . . . . . . . Rewrite_Set "norm_equation",
14.662 -([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond..ERROR*)
14.663 -
14.664 -(*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
14.665 -"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: TermC.as_string) = ((**) "x = 1");
14.666 - val cs = (*States.get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
14.667 - val pos = (*States.get_pos cI 1*) p
14.668 -
14.669 -(*+*)val ptp''''' = (pt, p);
14.670 -(*+*)if snd ptp''''' = ([1], Res) then () else error "old_cs changed";
14.671 -(*+*)Test_Tool.show_pt_tac pt; (*[
14.672 -(*+*)([], Frm), solve (x + 1 = 2, x)
14.673 -(*+*). . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
14.674 -(*+*)([1], Frm), x + 1 = 2
14.675 -(*+*). . . . . . . . . . Rewrite_Set "norm_equation",
14.676 -(*+*)([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond*)
14.677 -
14.678 - val ("ok", cs' as (_, _, ptp')) =
14.679 - (*case*) Step.do_next pos cs (*of*);
14.680 -
14.681 -val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) = (*case*)
14.682 - Step_Solve.by_term ptp' (encode ifo) (*of*);
14.683 -"~~~~~ fun Step_Solve.by_term , args:"; val ((pt, pos as (p, _)), istr)
14.684 - = (ptp', (encode ifo));
14.685 - val SOME f_in =
14.686 - (*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*);
14.687 - val pos_pred = lev_back(*'*) pos
14.688 - val f_pred = Ctree.get_curr_formula (pt, pos_pred);
14.689 - val f_succ = Ctree.get_curr_formula (pt, pos);
14.690 - (*if*) f_succ = f_in (*else*);
14.691 - val NONE =
14.692 - (*case*) CAS_Cmd.input f_in (*of*);
14.693 -
14.694 -(*NEW*) LI.locate_input_term (pt, pos) f_in (*of*);
14.695 -"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
14.696 - val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
14.697 -
14.698 - val ("ok", (_, _, cstate as (pt', pos'))) =
14.699 - (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
14.700 -
14.701 -(*old* )
14.702 - Found_Step (cstate, get_istate_LI pt' pos', get_ctxt pt' pos') (*return from locate_input_term*);
14.703 -( *old*)
14.704 -(*NEW*) Found_Step cstate (*return from locate_input_term*);
14.705 - (*LI.Found_Step ( *)cstate(*, _(*istate*), _)( *return from locate_input_term*);
14.706 -"~~~~~ from fun locate_input_term\<longrightarrow>fun Step_Solve.by_term, return:"; val ("ok", (_(*use in DG !!!*), c, ptp as (_, p)))
14.707 - = (("ok" , ([], [], cstate (* already contains istate, ctxt *))));
14.708 -
14.709 - ("ok", ((*_ use in DG !!!,*) c, ptp(* as (_*), p))(*)*)(*return from Step_Solve.by_term*);
14.710 -"~~~~~ from fun Step_Solve.by_term\<longrightarrow>(fun appendFormula)!toplevel, return:"; val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p''''')))
14.711 - = ("ok", ([], [], ptp));
14.712 -
14.713 -(*fun me requires nxt...*)
14.714 - Step.do_next p''''' (ptp''''', []);
14.715 - val ("ok", ([(nxt'''''_' as Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _,
14.716 - (pt'''''_', p'''''_'))) = Step.do_next p''''' (ptp''''', [])
14.717 -(*\\---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------//*)
14.718 -
14.719 -(*//----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----\\* )
14.720 - (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
14.721 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
14.722 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
14.723 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
14.724 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
14.725 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
14.726 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
14.727 - (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
14.728 - (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
14.729 - (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
14.730 - (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
14.731 - (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
14.732 -( *\\----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----//*)
14.733 -
14.734 - (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_' p'''''_' [] pt'''''_'; (*nxt = Check_elementwise "Assumptions"*)
14.735 - (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
14.736 - (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
14.737 -
14.738 -(*/--- final test ---------------------------------------------------------------------------\\*)
14.739 -if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree ctxt pr_short pt =
14.740 - ". ----- pblobj -----\n" ^
14.741 - "1. x + 1 = 2\n" ^
14.742 - "2. x + 1 + - 1 * 2 = 0\n" ^
14.743 - "3. ----- pblobj -----\n" ^
14.744 - "3.1. - 1 + x = 0\n" ^
14.745 - "3.2. x = 0 + - 1 * - 1\n" ^
14.746 - "3.2.1. x = 0 + - 1 * - 1\n" ^
14.747 - "3.2.2. x = 0 + 1\n" (*ATTENTION: see complete Calc below*)
14.748 -then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_term CHANGED 1"
14.749 -else error "re-build: fun locate_input_term CHANGED 2";
14.750 -
14.751 -Test_Tool.show_pt_tac pt; (*[
14.752 -([], Frm), solve (x + 1 = 2, x)
14.753 -. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
14.754 -([1], Frm), x + 1 = 2
14.755 -. . . . . . . . . . Rewrite_Set "norm_equation",
14.756 -([1], Res), x + 1 + - 1 * 2 = 0
14.757 -. . . . . . . . . . Rewrite_Set "Test_simplify",
14.758 -([2], Res), - 1 + x = 0
14.759 -. . . . . . . . . . Subproblem (Test, ["LINEAR", "univariate", "equation", "test"]),
14.760 -([3], Pbl), solve (- 1 + x = 0, x)
14.761 -. . . . . . . . . . Apply_Method ["Test", "solve_linear"],
14.762 -([3,1], Frm), - 1 + x = 0
14.763 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"),
14.764 -([3,1], Res), x = 0 + - 1 * - 1
14.765 -. . . . . . . . . . Derive Test_simplify,
14.766 -([3,2,1], Frm), x = 0 + - 1 * - 1
14.767 -. . . . . . . . . . Rewrite ("#: - 1 * - 1 = 1", "- 1 * - 1 = 1"),
14.768 -([3,2,1], Res), x = 0 + 1
14.769 -. . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),
14.770 -([3,2,2], Res), x = 1
14.771 -. . . . . . . . . . Tactic.input_to_string not impl. for ?!,
14.772 -([3,2], Res), x = 1
14.773 -. . . . . . . . . . Check_Postcond ["LINEAR", "univariate", "equation", "test"],
14.774 -([3], Res), [x = 1]
14.775 -. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
14.776 -([], Res), [x = 1]]*)
14.777 -\<close> ML \<open>
14.778 -"################ evaluate to bottom here ##################################################";
14.779 \<close> ML \<open>
14.780 \<close>
14.781