1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Mon Jan 30 12:38:17 2023 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Tue Jan 31 10:49:17 2023 +0100
1.3 @@ -72,8 +72,6 @@
1.4
1.5 val matches: theory -> term -> term -> bool
1.6
1.7 -(*val parse_opt: Proof.context -> string -> term option (*kept while developing Specify*)*)
1.8 - val parseNEW: Proof.context -> string -> term option
1.9 val parseNEW': Proof.context -> string -> term (*old version to be eliminated*)
1.10 val parseNEW'': theory -> string -> term (*old version to be eliminated*)
1.11
2.1 --- a/src/Tools/isac/Specify/p-spec.sml Mon Jan 30 12:38:17 2023 +0100
2.2 +++ b/src/Tools/isac/Specify/p-spec.sml Tue Jan 31 10:49:17 2023 +0100
2.3 @@ -140,7 +140,9 @@
2.4 let
2.5 val ctxt = ThyC.get_theory dI |> Proof_Context.init_global;
2.6 in
2.7 - case TermC.parseNEW ctxt ct of
2.8 + (*/------------ replace by ParseC.term_position ------------------\*)
2.9 + case ParseC.term_opt ctxt ct of
2.10 + (*\------------ replace by ParseC.term_position ------------------/*)
2.11 NONE => (0, [], false, sel, I_Model.Syn ct)
2.12 | SOME t =>
2.13 (case O_Model.contains ctxt sel oris t of
2.14 @@ -158,7 +160,9 @@
2.15 fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
2.16 fun fstr2itm_ thy pbt (f, str) =
2.17 let
2.18 - val topt = TermC.parseNEW (Proof_Context.init_global thy) str
2.19 + (*/------------ replace by ParseC.term_position ? ------------\*)
2.20 + val topt = ParseC.term_opt (Proof_Context.init_global thy) str
2.21 + (*\------------ replace by ParseC.term_position ? ------------/*)
2.22 in
2.23 case topt of
2.24 NONE => ([], false, f, I_Model.Syn str)
3.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Jan 30 12:38:17 2023 +0100
3.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Tue Jan 31 10:49:17 2023 +0100
3.3 @@ -279,7 +279,7 @@
3.4
3.5 ML \<open>
3.6 Context.theory_name thy = "Isac_Knowledge";
3.7 - val denominator = TermC.parseNEW ctxt "-1 + -2 * z + 8 * z \<up> 2 = 0";
3.8 + val denominator = ParseC.term_opt ctxt "-1 + -2 * z + 8 * z \<up> 2 = 0";
3.9 val fmz = (*specification*)
3.10 ["equality (-1 + -2 * z + 8 * z \<up> 2 = (0::real))",(*equality*)
3.11 "solveFor z", (*bound variable*)
3.12 @@ -325,7 +325,7 @@
3.13 * [z = 1 / 2, z = -1 / 4]
3.14 *)
3.15 Test_Tool.show_pt pt;
3.16 - val SOME f = parseNEW ctxt "[z=1/2, z=-1/4]";
3.17 + val SOME f = ParseC.term_opt ctxt "[z=1/2, z=-1/4]";
3.18 \<close>
3.19
3.20 subsection \<open>Partial Fraction Decomposition\label{sec:pbz}\<close>
3.21 @@ -336,7 +336,7 @@
3.22 text\<open>\noindent We get the solutions of the before solved equation in a list.\<close>
3.23
3.24 ML \<open>
3.25 - val SOME solutions = parseNEW ctxt "[z=1/2, z=-1/4]";
3.26 + val SOME solutions = ParseC.term_opt ctxt "[z=1/2, z=-1/4]";
3.27 UnparseC.term solutions;
3.28 TermC.atom_trace_detail @{context} solutions;
3.29 \<close>
3.30 @@ -526,9 +526,9 @@
3.31
3.32 \begin{verbatim}
3.33 val SOME t1 =
3.34 - parseNEW ctxt "get_denominator ((111::real) / 222)";
3.35 + ParseC.term_opt ctxt "get_denominator ((111::real) / 222)";
3.36 val SOME t2 =
3.37 - parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";
3.38 + ParseC.term_opt ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";
3.39 \end{verbatim}
3.40
3.41 \par \noindent Rewrite the terms using prog_rls:\\
3.42 @@ -588,7 +588,7 @@
3.43
3.44 val denominator' = HOLogic.mk_binop
3.45 \<^const_name>\<open>times\<close> (s_1', s_2') ;
3.46 - val SOME numerator = parseNEW ctxt "3::real";
3.47 + val SOME numerator = ParseC.term_opt ctxt "3::real";
3.48
3.49 val expr' = HOLogic.mk_binop
3.50 \<^const_name>\<open>divide\<close> (numerator, denominator');
3.51 @@ -658,7 +658,7 @@
3.52 ML \<open>
3.53 Rewrite.trace_on := false; (*true false*)
3.54 val SOME fract1 =
3.55 - parseNEW ctxt "(z - 1/2)*(z - -1/4) * (A/(z - 1/2) + B/(z - -1/4))";
3.56 + ParseC.term_opt ctxt "(z - 1/2)*(z - -1/4) * (A/(z - 1/2) + B/(z - -1/4))";
3.57 (*
3.58 * A B !
3.59 *)
3.60 @@ -1585,7 +1585,7 @@
3.61 \begin{verbatim}
3.62 val ctxt = Proof_Context.init_global @{theory "Inverse_Z_Transform"} ;
3.63 val SOME t =
3.64 - parseNEW ctxt "(num_orig::real) =
3.65 + ParseC.term_opt ctxt "(num_orig::real) =
3.66 get_numerator(rhs f_f)";
3.67 \end{verbatim}
3.68 and see a type clash: \ttfamily rhs \normalfont from (1) requires type
4.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Mon Jan 30 12:38:17 2023 +0100
4.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Tue Jan 31 10:49:17 2023 +0100
4.3 @@ -350,9 +350,9 @@
4.4 {\isaliteral{5D}{\isacharbrackright}}\ ctxt{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.5 \isanewline
4.6 \ \ val\ SOME\ fun{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
4.7 -\ \ \ \ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.8 +\ \ \ \ ParseC.term_opt\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.9 \ \ val\ SOME\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
4.10 -\ \ \ \ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.11 +\ \ \ \ ParseC.term_opt\ ctxt\ {\isaliteral{22}{\isachardoublequote}}X\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\ term{\isadigit{2}}str\ fun{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.12 {\isaliteral{2A7D}{\isacharverbatimclose}}%
4.13 \endisatagML
4.14 {\isafoldML}%
4.15 @@ -604,7 +604,7 @@
4.16 \isatagML
4.17 \isacommand{ML}\isamarkupfalse%
4.18 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
4.19 -\ \ val\ denominator\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}z{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.20 +\ \ val\ denominator\ {\isaliteral{3D}{\isacharequal}}\ ParseC.term_opt\ ctxt\ {\isaliteral{22}{\isachardoublequote}}z{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.21 \ \ val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}equality\ {\isaliteral{28}{\isacharparenleft}}z{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isadigit{2}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{2A}{\isacharasterisk}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
4.22 \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}solveFor\ z{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
4.23 \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}solutions\ L{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.24 @@ -653,7 +653,7 @@
4.25 \isacommand{ML}\isamarkupfalse%
4.26 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
4.27 \ \ Context{\isaliteral{2E}{\isachardot}}theory{\isaliteral{5F}{\isacharunderscore}}name\ thy\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}Isac{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.28 -\ \ val\ denominator\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.29 +\ \ val\ denominator\ {\isaliteral{3D}{\isacharequal}}\ ParseC.term_opt\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.30 \ \ val\ fmz\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}specification{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
4.31 \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}equality\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{8}}\ {\isaliteral{2A}{\isacharasterisk}}\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}equality{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
4.32 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}solveFor\ z{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}bound\ variable{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
4.33 @@ -729,7 +729,7 @@
4.34 \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5B}{\isacharbrackleft}}z\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
4.35 \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
4.36 \ \ show{\isaliteral{5F}{\isacharunderscore}}pt\ pt{\isaliteral{3B}{\isacharsemicolon}}\ \isanewline
4.37 -\ \ val\ SOME\ f\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}z{\isaliteral{3D}{\isacharequal}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{3D}{\isacharequal}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.38 +\ \ val\ SOME\ f\ {\isaliteral{3D}{\isacharequal}}\ ParseC.term_opt\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}z{\isaliteral{3D}{\isacharequal}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{3D}{\isacharequal}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.39 {\isaliteral{2A7D}{\isacharverbatimclose}}%
4.40 \endisatagML
4.41 {\isafoldML}%
4.42 @@ -765,7 +765,7 @@
4.43 \isatagML
4.44 \isacommand{ML}\isamarkupfalse%
4.45 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
4.46 -\ \ val\ SOME\ solutions\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}z{\isaliteral{3D}{\isacharequal}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{3D}{\isacharequal}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.47 +\ \ val\ SOME\ solutions\ {\isaliteral{3D}{\isacharequal}}\ ParseC.term_opt\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}z{\isaliteral{3D}{\isacharequal}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{3D}{\isacharequal}}{\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.48 \ \ term{\isadigit{2}}str\ solutions{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.49 \ \ TermC.atom_trace_detail @{context}\ solutions{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.50 {\isaliteral{2A7D}{\isacharverbatimclose}}%
4.51 @@ -1011,9 +1011,9 @@
4.52
4.53 \begin{verbatim}
4.54 val SOME t1 =
4.55 - parseNEW ctxt "get_denominator ((111::real) / 222)";
4.56 + ParseC.term_opt ctxt "get_denominator ((111::real) / 222)";
4.57 val SOME t2 =
4.58 - parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";
4.59 + ParseC.term_opt ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";
4.60 \end{verbatim}
4.61
4.62 \par \noindent Rewrite the terms using srls:\\
4.63 @@ -1086,7 +1086,7 @@
4.64 \ \ \ \isanewline
4.65 \ \ val\ denominator{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\ \isanewline
4.66 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}Groups{\isaliteral{2E}{\isachardot}}times{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}times{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{1}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{5F}{\isacharunderscore}}{\isadigit{2}}{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.67 -\ \ val\ SOME\ numerator\ {\isaliteral{3D}{\isacharequal}}\ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{3}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.68 +\ \ val\ SOME\ numerator\ {\isaliteral{3D}{\isacharequal}}\ ParseC.term_opt\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isadigit{3}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}real{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.69 \isanewline
4.70 \ \ val\ expr{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ HOLogic{\isaliteral{2E}{\isachardot}}mk{\isaliteral{5F}{\isacharunderscore}}binop\isanewline
4.71 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}Rings{\isaliteral{2E}{\isachardot}}inverse{\isaliteral{5F}{\isacharunderscore}}class{\isaliteral{2E}{\isachardot}}divide{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}numerator{\isaliteral{2C}{\isacharcomma}}\ denominator{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.72 @@ -1254,7 +1254,7 @@
4.73 \isacommand{ML}\isamarkupfalse%
4.74 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
4.75 \ \ val\ SOME\ fract{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
4.76 -\ \ \ \ parseNEW\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}A{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.77 +\ \ \ \ ParseC.term_opt\ ctxt\ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}A{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ B{\isaliteral{2F}{\isacharslash}}{\isaliteral{28}{\isacharparenleft}}z\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
4.78 \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
4.79 \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ A\ B\ {\isaliteral{21}{\isacharbang}}\isanewline
4.80 \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
4.81 @@ -2688,7 +2688,7 @@
4.82 \begin{verbatim}
4.83 val ctxt = Proof_Context.init_global @ { theory } ;
4.84 val SOME t =
4.85 - parseNEW ctxt "(num_orig::real) =
4.86 + ParseC.term_opt ctxt "(num_orig::real) =
4.87 get_numerator(rhs f_f)";
4.88 \end{verbatim}
4.89 and see a type clash: \ttfamily rhs \normalfont from (1) requires type
5.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Mon Jan 30 12:38:17 2023 +0100
5.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Tue Jan 31 10:49:17 2023 +0100
5.3 @@ -89,7 +89,7 @@
5.4 will disappear), which does not encode numerals as binary numbers:
5.5 \<close>
5.6 ML \<open>
5.7 - val t = TermC.parseNEW' (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3";
5.8 + val t = ParseC.parse_test (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3";
5.9 \<close>
5.10 text \<open>From the above we see: the internal representation of a term contains
5.11 all the knowledge it is built from, see
5.12 @@ -115,7 +115,7 @@
5.13 defined ('=' etc), but not yet '+' and '*', so you get 'NONE':
5.14 \<close>
5.15 ML \<open>
5.16 - val t = TermC.parseNEW' (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3";
5.17 + val t = ParseC.parse_test (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3";
5.18 \<close>
5.19 text \<open>ISAC uses comparatively few definitions and theorems from Isabelle, see
5.20 \begin{itemize}
6.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Mon Jan 30 12:38:17 2023 +0100
6.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Tue Jan 31 10:49:17 2023 +0100
6.3 @@ -41,7 +41,7 @@
6.4 \<close>
6.5 text \<open>... and let us differentiate the term t:\<close>
6.6 ML \<open>
6.7 -val t = TermC.parseNEW' ctxt "d_d x (x\<up>2 + x + y)";
6.8 +val t = ParseC.parse_test ctxt "d_d x (x\<up>2 + x + y)";
6.9
6.10 val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_sum t; UnparseC.term t;
6.11 val SOME (t, _) = Rewrite.rewrite_inst_ ctxt ro er true inst diff_sum t; UnparseC.term t;
6.12 @@ -80,10 +80,10 @@
6.13 text \<open>We have already seen conditional rewriting above when we used the rule
6.14 diff_const; let us try:\<close>
6.15 ML \<open>
6.16 -val t1 = TermC.parseNEW' ctxt "d_d x (a*BC*x*z)";
6.17 +val t1 = ParseC.parse_test ctxt "d_d x (a*BC*x*z)";
6.18 Rewrite.rewrite_inst_ ctxt ro er true inst diff_const t1;
6.19
6.20 -val t2 = TermC.parseNEW' ctxt "d_d x (a*BC*y*z)";
6.21 +val t2 = ParseC.parse_test ctxt "d_d x (a*BC*y*z)";
6.22 Rewrite.rewrite_inst_ ctxt ro er true inst diff_const t2;
6.23 \<close>
6.24 text \<open>For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false,
6.25 @@ -98,7 +98,7 @@
6.26 \<close>
6.27 ML \<open>
6.28 (*show_brackets := true; TODO*)
6.29 -val t0 = TermC.parseNEW' ctxt "2*a + 3*b + 4*a::real"; UnparseC.term t0;
6.30 +val t0 = ParseC.parse_test ctxt "2*a + 3*b + 4*a::real"; UnparseC.term t0;
6.31 (*show_brackets := false;*)
6.32 \<close>
6.33 text \<open>Now we want to bring 4*a close to 2*a in order to get 6*a:
6.34 @@ -147,11 +147,11 @@
6.35 \<close>
6.36 ML \<open>
6.37 (*show_brackets := false; TODO*)
6.38 -val t1 = TermC.parseNEW' ctxt "(a - b) * (a\<up>2 + a*b + b\<up>2)";
6.39 +val t1 = ParseC.parse_test ctxt "(a - b) * (a\<up>2 + a*b + b\<up>2)";
6.40 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true make_polynomial t1; UnparseC.term t;
6.41 \<close>
6.42 ML \<open>
6.43 -val t2 = TermC.parseNEW' ctxt
6.44 +val t2 = ParseC.parse_test ctxt
6.45 "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x \<up> 2 - 9))";
6.46 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true norm_Rational t2; UnparseC.term t;
6.47 \<close>
6.48 @@ -185,7 +185,7 @@
6.49
6.50 subsection \<open>What already works\<close>
6.51 ML \<open>
6.52 -val t2 = TermC.parseNEW' ctxt
6.53 +val t2 = ParseC.parse_test ctxt
6.54 "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12::real";
6.55 val SOME (t, _) = Rewrite.rewrite_set_ ctxt true rls_p_33 t2; UnparseC.term t;
6.56 \<close>
6.57 @@ -225,7 +225,7 @@
6.58
6.59 subsection \<open>This does not yet work\<close>
6.60 ML \<open>
6.61 -val t = TermC.parseNEW' ctxt
6.62 +val t = ParseC.parse_test ctxt
6.63 "(2*a - 5*b) * (2*a + 5*b)";
6.64 Rewrite.rewrite_set_ ctxt true rls_p_33 t; UnparseC.term t;
6.65 \<close>
7.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Mon Jan 30 12:38:17 2023 +0100
7.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Tue Jan 31 10:49:17 2023 +0100
7.3 @@ -29,10 +29,10 @@
7.4 val ctxt = ContextC.init_for_prog @{context} (vars t)
7.5
7.6 (*----- now parsing infers the type *)
7.7 -val SOME t = parseNEW ctxt "x";
7.8 +val SOME t = ParseC.term_opt ctxt "x";
7.9 if type_of t = HOLogic.realT then error "type inference failed 1" else ();
7.10
7.11 -val SOME t = parseNEW ctxt "a";
7.12 +val SOME t = ParseC.term_opt ctxt "a";
7.13 if type_of t = HOLogic.realT then () else error "type inference failed 2";
7.14
7.15 "----------- build fun initialise'--------------------------------------------------------------";
7.16 @@ -45,7 +45,7 @@
7.17 val (thy, fmz) = (@{theory Biegelinie}, fmz);
7.18
7.19 val ctxt = thy |> Proof_Context.init_global
7.20 - val ts = (map (TermC.parseNEW' ctxt) fmz) |> map TermC.vars |> flat |> distinct op =
7.21 + val ts = (map (ParseC.term_opt ctxt) fmz) |> map the |> map TermC.vars |> flat |> distinct op =
7.22 val _ = TermC.raise_type_conflicts ts;
7.23
7.24 "----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
8.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Mon Jan 30 12:38:17 2023 +0100
8.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Tue Jan 31 10:49:17 2023 +0100
8.3 @@ -356,7 +356,7 @@
8.4 val thy = @{theory "Complex_Main"};
8.5 val ctxt = (ThyC.id_to_ctxt "Isac_Knowledge")
8.6 val str = "x + z";
8.7 - TermC.parseNEW' ctxt str;
8.8 + ParseC.term_opt ctxt str;
8.9
8.10 "---------------";
8.11 val ctxt = @{context}
8.12 @@ -364,7 +364,7 @@
8.13 val t = Syntax.read_term_global thy str;
8.14 val t = ParseC.adapt_term_to_type ctxt (Syntax.read_term_global thy str);
8.15 Thm.global_cterm_of thy t;
8.16 - case TermC.parseNEW ctxt str of
8.17 + case ParseC.term_opt ctxt str of
8.18 SOME t' => t'
8.19 | NONE => error "termC.sml parsing 'x + 2*z' failed";
8.20
8.21 @@ -407,11 +407,11 @@
8.22 val thy = @{theory Partial_Fractions};
8.23 val ctxt = Proof_Context.init_global @{theory}
8.24
8.25 -val SOME t = TermC.parseNEW ctxt "x \<up> 2 + -1 * x * y";
8.26 +val SOME t = ParseC.term_opt ctxt "x \<up> 2 + -1 * x * y";
8.27 case TermC.vars_of t of [Free ("x", _), Free ("y", _)] => ()
8.28 | _ => error "TermC.vars_of (x \<up> 2 + -1 * x * y) ..changed";
8.29
8.30 -val SOME t = TermC.parseNEW ctxt "3 = 3 * AA / 4";
8.31 +val SOME t = ParseC.term_opt ctxt "3 = 3 * AA / 4";
8.32
8.33 case TermC.vars_of t of [Const (\<^const_name>\<open>AA\<close>, _), Const (\<^const_name>\<open>HOL.eq\<close>, _)] => ()
8.34 | _ => error "TermC.vars_of (3 = 3 * AA / 4) ..changed (! use only for polynomials, not equations!)";
8.35 @@ -646,7 +646,7 @@
8.36 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";
8.37 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";
8.38 "----------- fun mk_factroot, fun mk_num_op_num, -----------------------------------------------";
8.39 -val T = type_of (TermC.parseNEW' ctxt "12::real");
8.40 +val T = type_of (ParseC.term_opt ctxt "12::real" |> the);
8.41 val t = TermC.mk_factroot "SqRoot.sqrt" T 2 3;
8.42 if UnparseC.term t = "2 * ??.SqRoot.sqrt 3" then () else error "mk_factroot";
8.43
8.44 @@ -658,7 +658,7 @@
8.45 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";
8.46 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";
8.47 "----------- fun TermC.dest_binop_typ ----------------------------------------------------------------";
8.48 -val t = TermC.parseNEW' ctxt "(3::real) ^ 4";
8.49 +val t = ParseC.term_opt ctxt "(3::real) ^ 4" |> the;
8.50 val hT = type_of (head_of t);
8.51 if (HOLogic.realT, HOLogic.natT, HOLogic.realT) = TermC.dest_binop_typ hT
8.52 then () else error "TermC.dest_binop_typ";
8.53 @@ -666,7 +666,7 @@
8.54 "----------- fun TermC.is_list -----------------------------------------------------------------------";
8.55 "----------- fun TermC.is_list -----------------------------------------------------------------------";
8.56 "----------- fun TermC.is_list -----------------------------------------------------------------------";
8.57 -val (SOME ct) = TermC.parseNEW ctxt "lll::real list";
8.58 +val (SOME ct) = ParseC.term_opt ctxt "lll::real list";
8.59 val t = ParseC.parse_test @{context} "lll::real list";
8.60 val ty = Term.type_of ct;
8.61 if TermC.is_list t = false then () else error "TermC.is_list lll::real list";
9.1 --- a/test/Tools/isac/BridgeJEdit/vscode-example.sml Mon Jan 30 12:38:17 2023 +0100
9.2 +++ b/test/Tools/isac/BridgeJEdit/vscode-example.sml Tue Jan 31 10:49:17 2023 +0100
9.3 @@ -30,7 +30,7 @@
9.4 "Domain {0 <..< \<pi> / 2}",
9.5 "ErrorBound (\<epsilon> = (0::real))"
9.6 ]: TermC.as_string list;
9.7 -if (fmz |> map (TermC.parseNEW @{context}) |> filter is_some |> length) = 14
9.8 +if (fmz |> map (ParseC.term_opt @{context}) |> filter is_some |> length) = 14
9.9 then () else error "Formalise.model not parsed completely";
9.10
9.11 val refs =
10.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Mon Jan 30 12:38:17 2023 +0100
10.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Tue Jan 31 10:49:17 2023 +0100
10.3 @@ -1036,7 +1036,7 @@
10.4 "~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Calc.state_post), istr)
10.5 = (cs', (encode ifo));
10.6 val ctxt = get_ctxt pt pos (*see TODO.thy*)
10.7 - val SOME f_in = (*case*) TermC.parseNEW ctxt istr (*of*);
10.8 + val SOME f_in = (*case*) ParseC.term_opt ctxt istr (*of*);
10.9 val pos_pred = lev_back' pos
10.10 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
10.11 (*if*) f_pred = f_in; (*else*)
10.12 @@ -1283,7 +1283,7 @@
10.13 val pos = States.get_pos cI 1;
10.14
10.15 "~~~~~ fun is_exactly_equal, args:"; val ((pt, pos as (p, p_)), istr) = ((pt, pos), ifo);
10.16 - val SOME ifo = parseNEW (ThyC.get_theory "Isac_Knowledge" |> Proof_Context.init_global) istr
10.17 + val SOME ifo = ParseC.term_opt (ThyC.get_theory "Isac_Knowledge" |> Proof_Context.init_global) istr
10.18 val p' = lev_on p;
10.19 val tac = get_obj g_tac pt p';
10.20 val Rewrite_Inst ([bbb as "(''bdv'', x)"], ("diff_sin_chain", ttt)) = tac;
11.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Jan 30 12:38:17 2023 +0100
11.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Jan 31 10:49:17 2023 +0100
11.3 @@ -666,7 +666,7 @@
11.4 "~~~~~ fun Step_Solve.by_term , args:"; val ((pt, pos as (p, _)), istr)
11.5 = (ptp', (encode ifo));
11.6 val SOME f_in =
11.7 - (*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*);
11.8 + (*case*) ParseC.term_opt (get_ctxt pt pos) istr (*of*);
11.9 val pos_pred = lev_back(*'*) pos
11.10 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
11.11 val f_succ = Ctree.get_curr_formula (pt, pos);
12.1 --- a/test/Tools/isac/Knowledge/algein.sml Mon Jan 30 12:38:17 2023 +0100
12.2 +++ b/test/Tools/isac/Knowledge/algein.sml Tue Jan 31 10:49:17 2023 +0100
12.3 @@ -26,7 +26,7 @@
12.4 \ (let t_t = (l_l = 1)\
12.5 \ in t_t)"
12.6 ;
12.7 -val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
12.8 +val sc = (inst_abs o (ParseC.parse_test ctxt)) str;
12.9 TermC.atom_trace_detail @{context} sc;
12.10 TermC.atom_trace @{context} sc;
12.11
13.1 --- a/test/Tools/isac/Knowledge/diff.sml Mon Jan 30 12:38:17 2023 +0100
13.2 +++ b/test/Tools/isac/Knowledge/diff.sml Tue Jan 31 10:49:17 2023 +0100
13.3 @@ -35,11 +35,11 @@
13.4 Find =["derivative f_f'"],
13.5 With =[],
13.6 Relate=[]}:string model;
13.7 -val chkpbt = ((map (TermC.parseNEW' ctxt)) o P_Model.to_list) pbt;
13.8 +val chkpbt = ((map (ParseC.parse_test ctxt)) o P_Model.to_list) pbt;
13.9
13.10 val org = ["functionTerm (d_d x (x \<up> 2 + 3 * x + 4))",
13.11 "differentiateFor x", "derivative f_f'"];
13.12 -val chkorg = map (TermC.parseNEW' ctxt) org;
13.13 +val chkorg = map (ParseC.parse_test ctxt) org;
13.14
13.15 Problem.from_store @{context} ["derivative_of", "function"];
13.16 MethodC.from_store ctxt ["diff", "differentiate_on_R"];
13.17 @@ -49,18 +49,18 @@
13.18 "----------- for correction of diff_const ---------------";
13.19 val ctxt = Proof_Context.init_global @{theory};
13.20 (*re-evaluate this file, otherwise > *** ME_Isa: 'asm_rls' not known*)
13.21 -val t = TermC.parseNEW' ctxt "Not (x =!= a)";
13.22 +val t = ParseC.parse_test ctxt "Not (x =!= a)";
13.23 case rewrite_set_ ctxt false erls_diff t of
13.24 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
13.25 | _ => error "rewrite_set_ Not (x =!= a) changed";
13.26
13.27 -val t = TermC.parseNEW' ctxt "2 is_num";
13.28 +val t = ParseC.parse_test ctxt "2 is_num";
13.29 case rewrite_set_ ctxt false erls_diff t of
13.30 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
13.31 | _ => error "rewrite_set_ 2 is_num changed";
13.32
13.33 val thm = @{thm diff_const};
13.34 -val ct = TermC.parseNEW' ctxt "d_d x x";
13.35 +val ct = ParseC.parse_test ctxt "d_d x x";
13.36 val subst = [(@{term "bdv::real"}, @{term "x::real"})];
13.37 val NONE = (rewrite_inst_ ctxt tless_true erls_diff false subst thm ct);
13.38
13.39 @@ -69,10 +69,10 @@
13.40 "----------- for correction of diff_quot ----------------";
13.41 val thy = @{theory "Diff"};
13.42 val ctxt = Proof_Context.init_global thy;
13.43 -val ct = TermC.parseNEW' ctxt "Not (x = 0)";
13.44 +val ct = ParseC.parse_test ctxt "Not (x = 0)";
13.45 rewrite_set_ ctxt false erls_diff ct;
13.46
13.47 -val ct = TermC.parseNEW' ctxt "d_d x ((x+1) / (x - 1))";
13.48 +val ct = ParseC.parse_test ctxt "d_d x ((x+1) / (x - 1))";
13.49 val thm = @{thm diff_quot};
13.50 val SOME (ctt,_) =
13.51 (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);
13.52 @@ -82,7 +82,7 @@
13.53 "----------- differentiate by rewrite -------------------";
13.54 val thy = @{theory "Diff"};
13.55 val ctxt = Proof_Context.init_global thy;
13.56 -val ct = TermC.parseNEW' ctxt "d_d x (x \<up> 2 + 3 * x + 4)";
13.57 +val ct = ParseC.parse_test ctxt "d_d x (x \<up> 2 + 3 * x + 4)";
13.58 "--- 1 ---";
13.59 val thm = @{thm "diff_sum"};
13.60 val (ct, _) = the (rewrite_inst_ ctxt tless_true erls_diff true subst thm ct);
13.61 @@ -105,7 +105,7 @@
13.62 "--- 7 ---";
13.63 "--- 7 ---";
13.64 val rls = Test_simplify;
13.65 -val ct = TermC.parseNEW' ctxt "2 * x \<up> (2 - 1) + 3 * 1 + 0";
13.66 +val ct = ParseC.parse_test ctxt "2 * x \<up> (2 - 1) + 3 * 1 + 0";
13.67 val (ct, _) = the (rewrite_set_ ctxt true rls ct);
13.68 if UnparseC.term ct = "3 + 2 * x" then () else error "rewrite_set_ Test_simplify 2 changed";
13.69
13.70 @@ -262,7 +262,7 @@
13.71 \ (Try (Repeat (Rewrite sym_frac_conv))) #> \
13.72 \ (Try (Repeat (Rewrite sym_root_conv))))) f_f')"
13.73 ;
13.74 -val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
13.75 +val sc = (inst_abs o (ParseC.parse_test ctxt)) str;
13.76
13.77
13.78 "----------- diff_conv, sym_diff_conv -------------------";
14.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Mon Jan 30 12:38:17 2023 +0100
14.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Tue Jan 31 10:49:17 2023 +0100
14.3 @@ -26,10 +26,10 @@
14.4 "----------- rewriting for usecase1 ---------------------";
14.5 "----------- rewriting for usecase1 ---------------------";
14.6 "----------- rewriting for usecase1 ---------------------";
14.7 -val subst = case (parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int") of
14.8 +val subst = case (ParseC.term_opt ctxt "bdv::int", ParseC.term_opt ctxt "xxx::int") of
14.9 (SOME r, SOME s) => [(r,s)]
14.10 | _ => error "diophanteq.sml: syntax error in rewriting for usecase1"
14.11 -val t = case parseNEW ctxt "xxx + 111 = abc + (123::int)" of
14.12 +val t = case ParseC.term_opt ctxt "xxx + 111 = abc + (123::int)" of
14.13 SOME t' => t'
14.14 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";
14.15
14.16 @@ -67,7 +67,7 @@
14.17 val thy = @{theory "Test"};
14.18 "----------- rewriting for usecase2 ---------------------";
14.19
14.20 -val t = case parseNEW ctxt "xxx + abc + - 1 * 111 + (123::int)" of
14.21 +val t = case ParseC.term_opt ctxt "xxx + abc + - 1 * 111 + (123::int)" of
14.22 SOME t' => t'
14.23 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2";
14.24
15.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Mon Jan 30 12:38:17 2023 +0100
15.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Tue Jan 31 10:49:17 2023 +0100
15.3 @@ -92,9 +92,9 @@
15.4 if UnparseC.term t' = "True" then ()
15.5 else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
15.6
15.7 -val SOME t = TermC.parseNEW ctxt "solution LL";
15.8 +val SOME t = ParseC.term_opt ctxt "solution LL";
15.9 TermC.atom_trace_detail @{context} t;
15.10 -val SOME t = TermC.parseNEW ctxt "solution LL";
15.11 +val SOME t = ParseC.term_opt ctxt "solution LL";
15.12 TermC.atom_trace_detail @{context} t;
15.13
15.14 val t = ParseC.parse_test @{context}
16.1 --- a/test/Tools/isac/Knowledge/inssort.sml Mon Jan 30 12:38:17 2023 +0100
16.2 +++ b/test/Tools/isac/Knowledge/inssort.sml Tue Jan 31 10:49:17 2023 +0100
16.3 @@ -35,7 +35,7 @@
16.4 "----------- insertion sort by rewrite stepwise ------------------------------";
16.5 "----------- insertion sort by rewrite stepwise ------------------------------";
16.6 val ctxt = Proof_Context.init_global @{theory};
16.7 -val SOME t = parseNEW ctxt "sort {|| 1, 3, 2 ||}";
16.8 +val SOME t = ParseC.term_opt ctxt "sort {|| 1, 3, 2 ||}";
16.9
16.10 val SOME (t', _) = rewrite_ ctxt tless_true eval_rls false @{thm sort_deff} t;
16.11 UnparseC.term t' = "xfoldr ins {|| 1, 3, 2 ||} {|| ||}";
17.1 --- a/test/Tools/isac/Knowledge/integrate.sml Mon Jan 30 12:38:17 2023 +0100
17.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Tue Jan 31 10:49:17 2023 +0100
17.3 @@ -26,7 +26,7 @@
17.4 val thy = @{theory "Integrate"};
17.5 val ctxt = Proof_Context.init_global thy;
17.6
17.7 -fun str2t str = parseNEW ctxt str |> the;
17.8 +fun str2t str = ParseC.term_opt ctxt str |> the;
17.9 fun term2s t = UnparseC.term_in_ctxt ctxt t;
17.10
17.11 val conditions_in_integration_rules =
17.12 @@ -256,52 +256,52 @@
17.13 val subs = [(@{term "bdv::real"}, @{term "x::real"})];
17.14 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
17.15
17.16 -val t = TermC.parseNEW' ctxt "Integral x D x";
17.17 +val t = ParseC.parse_test ctxt "Integral x D x";
17.18 val SOME (res, _) = rewrite_set_inst_ ctxt true subs rls t;
17.19 if UnparseC.term res = "x \<up> 2 / 2" then () else error "Integral x D x changed";
17.20
17.21 -val t = TermC.parseNEW' ctxt "Integral c * x \<up> 2 + c_2 D x";
17.22 +val t = ParseC.parse_test ctxt "Integral c * x \<up> 2 + c_2 D x";
17.23 val SOME (res, _) = rewrite_set_inst_ ctxt true subs rls t;
17.24 if UnparseC.term res = "c * (x \<up> 3 / 3) + c_2 * x" then () else error "Integral c * x \<up> 2 + c_2 D x";
17.25
17.26 val rls = add_new_c;
17.27 -val t = TermC.parseNEW' ctxt "c * (x \<up> 3 / 3) + c_2 * x";
17.28 +val t = ParseC.parse_test ctxt "c * (x \<up> 3 / 3) + c_2 * x";
17.29 val SOME (res, _) = rewrite_set_inst_ ctxt true subs rls t;
17.30 if UnparseC.term res = "c * (x \<up> 3 / 3) + c_2 * x + c_3" then ()
17.31 else error "integrate.sml: diff.behav. in add_new_c simpl.";
17.32
17.33 -val t = TermC.parseNEW' ctxt "F x = x \<up> 3 / 3 + x";
17.34 +val t = ParseC.parse_test ctxt "F x = x \<up> 3 / 3 + x";
17.35 val SOME (res, _) = rewrite_set_inst_ ctxt true subs rls t;
17.36 if UnparseC.term res = "F x = x \<up> 3 / 3 + x + c"(*not "F x + c =..."*) then ()
17.37 else error "integrate.sml: diff.behav. in add_new_c equation";
17.38
17.39 val rls = simplify_Integral;
17.40 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
17.41 -val t = TermC.parseNEW' ctxt "ff x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
17.42 +val t = ParseC.parse_test ctxt "ff x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
17.43 val SOME (res, _) = rewrite_set_inst_ ctxt true subs rls t;
17.44 if UnparseC.term res = "ff x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2"
17.45 then () else error "integrate.sml: diff.behav. in simplify_I #1";
17.46
17.47 val rls = integration;
17.48 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
17.49 -val t = TermC.parseNEW' ctxt "Integral c * x \<up> 2 + c_2 D x";
17.50 +val t = ParseC.parse_test ctxt "Integral c * x \<up> 2 + c_2 D x";
17.51 val SOME (res, _) = rewrite_set_inst_ ctxt true subs rls t;
17.52 if UnparseC.term res = "c_3 + c_2 * x + c / 3 * x \<up> 3"
17.53 then () else error "integrate.sml: diff.behav. in integration #1";
17.54
17.55 -val t = TermC.parseNEW' ctxt "Integral 3*x \<up> 2 + 2*x + 1 D x";
17.56 +val t = ParseC.parse_test ctxt "Integral 3*x \<up> 2 + 2*x + 1 D x";
17.57 val SOME (res, _) = rewrite_set_inst_ ctxt true subs rls t;
17.58 if UnparseC.term res = "c + x + x \<up> 2 + x \<up> 3" then ()
17.59 else error "integrate.sml: diff.behav. in integration #2";
17.60
17.61 -val t = TermC.parseNEW' ctxt
17.62 +val t = ParseC.parse_test ctxt
17.63 "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x";
17.64 val SOME (res, _) = rewrite_set_inst_ ctxt true subs rls t;
17.65 "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x";
17.66 if UnparseC.term res = "c + 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)"
17.67 then () else error "integrate.sml: diff.behav. in integration #3";
17.68
17.69 -val t = TermC.parseNEW' ctxt ("Integral " ^ UnparseC.term res ^ " D x");
17.70 +val t = ParseC.parse_test ctxt ("Integral " ^ UnparseC.term res ^ " D x");
17.71 val SOME (res, _) = rewrite_set_inst_ ctxt true subs rls t;
17.72 if UnparseC.term res = "c_2 + c * x +\n1 / EI * (L * q_0 / 12 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)"
17.73 then () else error "integrate.sml: diff.behav. in integration #4";
17.74 @@ -330,7 +330,7 @@
17.75 Find =["antiDerivative F_F"],
17.76 With =[],
17.77 Relate=[]}:string model;
17.78 -val chkmodel = ((map (TermC.parseNEW' ctxt)) o P_Model.to_list) model;
17.79 +val chkmodel = ((map (ParseC.parse_test ctxt)) o P_Model.to_list) model;
17.80 val t1 = (hd) chkmodel;
17.81 val t2 = (hd o tl) chkmodel;
17.82 val t3 = (hd o tl o tl) chkmodel;
17.83 @@ -342,7 +342,7 @@
17.84 Find =["antiDerivativeName F_F"],
17.85 With =[],
17.86 Relate=[]}:string model;
17.87 -val chkmodel = ((map (TermC.parseNEW' ctxt)) o P_Model.to_list) model;
17.88 +val chkmodel = ((map (ParseC.parse_test ctxt)) o P_Model.to_list) model;
17.89 val t1 = (hd) chkmodel;
17.90 val t2 = (hd o tl) chkmodel;
17.91 val t3 = (hd o tl o tl) chkmodel;
18.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Mon Jan 30 12:38:17 2023 +0100
18.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Tue Jan 31 10:49:17 2023 +0100
18.3 @@ -78,7 +78,7 @@
18.4 "----------- fun factors_from_solution ------------------";
18.5 "----------- fun factors_from_solution ------------------";
18.6 val ctxt = Proof_Context.init_global @{theory Isac_Knowledge};
18.7 -val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = - 1 / 4]";
18.8 +val SOME t = ParseC.term_opt ctxt "factors_from_solution [(z::real) = 1 / 2, z = - 1 / 4]";
18.9 val SOME (_, t') = eval_factors_from_solution "" 0 t thy;
18.10 if UnparseC.term t' =
18.11 "factors_from_solution [z = 1 / 2, z = - 1 / 4] = (z - 1 / 2) * (z - - 1 / 4)"
18.12 @@ -87,11 +87,11 @@
18.13 "----------- Logic.unvarify_global ----------------------";
18.14 "----------- Logic.unvarify_global ----------------------";
18.15 "----------- Logic.unvarify_global ----------------------";
18.16 -val A_var = parseNEW ctxt "A::real" |> the |> Logic.varify_global
18.17 -val B_var = parseNEW ctxt "B::real" |> the |> Logic.varify_global
18.18 +val A_var = ParseC.term_opt ctxt "A::real" |> the |> Logic.varify_global
18.19 +val B_var = ParseC.term_opt ctxt "B::real" |> the |> Logic.varify_global
18.20
18.21 -val denom1 = parseNEW ctxt "(z + - 1 * (1 / 2))::real" |> the;
18.22 -val denom2 = parseNEW ctxt "(z + - 1 * (- 1 / 4))::real" |> the;
18.23 +val denom1 = ParseC.term_opt ctxt "(z + - 1 * (1 / 2))::real" |> the;
18.24 +val denom2 = ParseC.term_opt ctxt "(z + - 1 * (- 1 / 4))::real" |> the;
18.25
18.26 val test = HOLogic.mk_binop \<^const_name>\<open>plus\<close>
18.27 (HOLogic.mk_binop \<^const_name>\<open>divide\<close> (A_var, denom1),
19.1 --- a/test/Tools/isac/Knowledge/poly-1.sml Mon Jan 30 12:38:17 2023 +0100
19.2 +++ b/test/Tools/isac/Knowledge/poly-1.sml Tue Jan 31 10:49:17 2023 +0100
19.3 @@ -47,136 +47,136 @@
19.4 "-------- fun has_degree_in --------------------------------------------------------------------";
19.5 val thy = @{theory}
19.6 val ctxt = Proof_Context.init_global thy
19.7 -val v = TermC.parseNEW' ctxt "x";
19.8 -val t = TermC.parseNEW' ctxt "1";
19.9 +val v = ParseC.parse_test ctxt "x";
19.10 +val t = ParseC.parse_test ctxt "1";
19.11 if has_degree_in t v = 0 then () else error "has_degree_in (1) x";
19.12
19.13 -val v = TermC.parseNEW' ctxt "AA";
19.14 -val t = TermC.parseNEW' ctxt "1";
19.15 +val v = ParseC.parse_test ctxt "AA";
19.16 +val t = ParseC.parse_test ctxt "1";
19.17 if has_degree_in t v = 0 then () else error "has_degree_in (1) AA";
19.18
19.19 (*----------*)
19.20 -val v = TermC.parseNEW' ctxt "x";
19.21 -val t = TermC.parseNEW' ctxt "a*b+c";
19.22 +val v = ParseC.parse_test ctxt "x";
19.23 +val t = ParseC.parse_test ctxt "a*b+c";
19.24 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x";
19.25
19.26 -val v = TermC.parseNEW' ctxt "AA";
19.27 -val t = TermC.parseNEW' ctxt "a*b+c";
19.28 +val v = ParseC.parse_test ctxt "AA";
19.29 +val t = ParseC.parse_test ctxt "a*b+c";
19.30 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA";
19.31
19.32 (*----------*)
19.33 -val v = TermC.parseNEW' ctxt "x";
19.34 -val t = TermC.parseNEW' ctxt "a*x+c";
19.35 +val v = ParseC.parse_test ctxt "x";
19.36 +val t = ParseC.parse_test ctxt "a*x+c";
19.37 if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x";
19.38
19.39 -val v = TermC.parseNEW' ctxt "AA";
19.40 -val t = TermC.parseNEW' ctxt "a*AA+c";
19.41 +val v = ParseC.parse_test ctxt "AA";
19.42 +val t = ParseC.parse_test ctxt "a*AA+c";
19.43 if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA";
19.44
19.45 (*----------*)
19.46 -val v = TermC.parseNEW' ctxt "x::real";
19.47 -val t = TermC.parseNEW' ctxt "((a::real)*b+c)*x \<up> 7";
19.48 +val v = ParseC.parse_test ctxt "x::real";
19.49 +val t = ParseC.parse_test ctxt "((a::real)*b+c)*x \<up> 7";
19.50 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x \<up> 7) x";
19.51
19.52 -val v = TermC.parseNEW' ctxt "AA";
19.53 -val t = TermC.parseNEW' ctxt "(a*b+c)*AA \<up> 7";
19.54 +val v = ParseC.parse_test ctxt "AA";
19.55 +val t = ParseC.parse_test ctxt "(a*b+c)*AA \<up> 7";
19.56 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA \<up> 7) AA";
19.57
19.58 (*----------*)
19.59 -val v = TermC.parseNEW' ctxt "x::real";
19.60 -val t = TermC.parseNEW' ctxt "x \<up> 7";
19.61 +val v = ParseC.parse_test ctxt "x::real";
19.62 +val t = ParseC.parse_test ctxt "x \<up> 7";
19.63 if has_degree_in t v = 7 then () else error "has_degree_in (x \<up> 7) x";
19.64
19.65 -val v = TermC.parseNEW' ctxt "AA";
19.66 -val t = TermC.parseNEW' ctxt "AA \<up> 7";
19.67 +val v = ParseC.parse_test ctxt "AA";
19.68 +val t = ParseC.parse_test ctxt "AA \<up> 7";
19.69 if has_degree_in t v = 7 then () else error "has_degree_in (AA \<up> 7) AA";
19.70
19.71 (*----------*)
19.72 -val v = TermC.parseNEW' ctxt "x::real";
19.73 -val t = TermC.parseNEW' ctxt "(a*b+c)*x::real";
19.74 +val v = ParseC.parse_test ctxt "x::real";
19.75 +val t = ParseC.parse_test ctxt "(a*b+c)*x::real";
19.76 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x";
19.77
19.78 -val v = TermC.parseNEW' ctxt "AA";
19.79 -val t = TermC.parseNEW' ctxt "(a*b+c)*AA";
19.80 +val v = ParseC.parse_test ctxt "AA";
19.81 +val t = ParseC.parse_test ctxt "(a*b+c)*AA";
19.82 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA";
19.83
19.84 (*----------*)
19.85 -val v = TermC.parseNEW' ctxt "x::real";
19.86 -val t = TermC.parseNEW' ctxt "(a*b+x)*x";
19.87 +val v = ParseC.parse_test ctxt "x::real";
19.88 +val t = ParseC.parse_test ctxt "(a*b+x)*x";
19.89 if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x";
19.90
19.91 -val v = TermC.parseNEW' ctxt "AA";
19.92 -val t = TermC.parseNEW' ctxt "(a*b+AA)*AA";
19.93 +val v = ParseC.parse_test ctxt "AA";
19.94 +val t = ParseC.parse_test ctxt "(a*b+AA)*AA";
19.95 if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA";
19.96
19.97 (*----------*)
19.98 -val v = TermC.parseNEW' ctxt "x";
19.99 -val t = TermC.parseNEW' ctxt "x";
19.100 +val v = ParseC.parse_test ctxt "x";
19.101 +val t = ParseC.parse_test ctxt "x";
19.102 if has_degree_in t v = 1 then () else error "has_degree_in (x) x";
19.103
19.104 -val v = TermC.parseNEW' ctxt "AA";
19.105 -val t = TermC.parseNEW' ctxt "AA";
19.106 +val v = ParseC.parse_test ctxt "AA";
19.107 +val t = ParseC.parse_test ctxt "AA";
19.108 if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA";
19.109
19.110 (*----------*)
19.111 -val v = TermC.parseNEW' ctxt "x::real";
19.112 -val t = TermC.parseNEW' ctxt "ab - (a*b)*(x::real)";
19.113 +val v = ParseC.parse_test ctxt "x::real";
19.114 +val t = ParseC.parse_test ctxt "ab - (a*b)*(x::real)";
19.115 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x";
19.116
19.117 -val v = TermC.parseNEW' ctxt "AA";
19.118 -val t = TermC.parseNEW' ctxt "ab - (a*b)*AA";
19.119 +val v = ParseC.parse_test ctxt "AA";
19.120 +val t = ParseC.parse_test ctxt "ab - (a*b)*AA";
19.121 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA";
19.122
19.123 "-------- fun mono_deg_in ----------------------------------------------------------------------";
19.124 "-------- fun mono_deg_in ----------------------------------------------------------------------";
19.125 "-------- fun mono_deg_in ----------------------------------------------------------------------";
19.126 -val v = TermC.parseNEW' ctxt "x::real";
19.127 +val v = ParseC.parse_test ctxt "x::real";
19.128
19.129 -val t = TermC.parseNEW' ctxt "(a*b+c)*x \<up> 7";
19.130 +val t = ParseC.parse_test ctxt "(a*b+c)*x \<up> 7";
19.131 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x \<up> 7) x changed";
19.132
19.133 -val t = TermC.parseNEW' ctxt "(x::real) \<up> 7";
19.134 +val t = ParseC.parse_test ctxt "(x::real) \<up> 7";
19.135 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x \<up> 7) x changed";
19.136
19.137 -val t = TermC.parseNEW' ctxt "(a*b+c)*x::real";
19.138 +val t = ParseC.parse_test ctxt "(a*b+c)*x::real";
19.139 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed";
19.140
19.141 -val t = TermC.parseNEW' ctxt "(a*b+x)*x";
19.142 +val t = ParseC.parse_test ctxt "(a*b+x)*x";
19.143 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed";
19.144
19.145 -val t = TermC.parseNEW' ctxt "x::real";
19.146 +val t = ParseC.parse_test ctxt "x::real";
19.147 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed";
19.148
19.149 -val t = TermC.parseNEW' ctxt "(a*b+c)";
19.150 +val t = ParseC.parse_test ctxt "(a*b+c)";
19.151 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed";
19.152
19.153 -val t = TermC.parseNEW' ctxt "ab - (a*b)*x";
19.154 +val t = ParseC.parse_test ctxt "ab - (a*b)*x";
19.155 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";
19.156
19.157 (*. . . . . . . . . . . . the same with Const (\<^const_name>\<open>AA\<close>, _) . . . . . . . . . . . *)
19.158 val thy = @{theory Partial_Fractions}
19.159 val ctxt = Proof_Context.init_global thy
19.160 -val v = TermC.parseNEW' ctxt "AA";
19.161 +val v = ParseC.parse_test ctxt "AA";
19.162
19.163 -val t = TermC.parseNEW' ctxt "(a*b+c)*AA \<up> 7";
19.164 +val t = ParseC.parse_test ctxt "(a*b+c)*AA \<up> 7";
19.165 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA \<up> 7) AA changed";
19.166
19.167 -val t = TermC.parseNEW' ctxt "AA \<up> 7";
19.168 +val t = ParseC.parse_test ctxt "AA \<up> 7";
19.169 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA \<up> 7) AA changed";
19.170
19.171 -val t = TermC.parseNEW' ctxt "(a*b+c)*AA";
19.172 +val t = ParseC.parse_test ctxt "(a*b+c)*AA";
19.173 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed";
19.174
19.175 -val t = TermC.parseNEW' ctxt "(a*b+AA)*AA";
19.176 +val t = ParseC.parse_test ctxt "(a*b+AA)*AA";
19.177 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed";
19.178
19.179 -val t = TermC.parseNEW' ctxt "AA";
19.180 +val t = ParseC.parse_test ctxt "AA";
19.181 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed";
19.182
19.183 -val t = TermC.parseNEW' ctxt "(a*b+c)";
19.184 +val t = ParseC.parse_test ctxt "(a*b+c)";
19.185 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed";
19.186
19.187 -val t = TermC.parseNEW' ctxt "ab - (a*b)*AA";
19.188 +val t = ParseC.parse_test ctxt "ab - (a*b)*AA";
19.189 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed";
19.190
19.191
19.192 @@ -791,7 +791,7 @@
19.193 else error "poly.sml: diff.behav. in make_polynomial 20";
19.194
19.195 "-----SPO ---";
19.196 -val t = TermC.parseNEW' ctxt "a \<up> 2 * (-a) \<up> 2";
19.197 +val t = ParseC.parse_test ctxt "a \<up> 2 * (-a) \<up> 2";
19.198 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
19.199 if (UnparseC.term t) = "a \<up> 4" then ()
19.200 else error "poly.sml: diff.behav. in make_polynomial 24";
20.1 --- a/test/Tools/isac/Knowledge/poly-2.sml Mon Jan 30 12:38:17 2023 +0100
20.2 +++ b/test/Tools/isac/Knowledge/poly-2.sml Tue Jan 31 10:49:17 2023 +0100
20.3 @@ -114,7 +114,7 @@
20.4 sym_real_mult_minus1 = "- ?z = - 1 * ?z" *)
20.5 @{thm real_mult_minus1}; (* = "- 1 * ?z = - ?z" *)
20.6 val thm_isac = ThmC.sym_thm @{thm real_mult_minus1}; (* = "- ?z = - 1 * ?z" *)
20.7 -val SOME t_isac = TermC.parseNEW @{context} "3 * a + - 1 * (2 * a):: real";
20.8 +val SOME t_isac = ParseC.term_opt @{context} "3 * a + - 1 * (2 * a):: real";
20.9
20.10 val SOME (t', []) = rewrite_ @{context} tless_true Rule_Set.empty true thm_isac t_isac;
20.11 if UnparseC.term t' = "3 * a + - 1 * 1 * (2 * a)" then ((*thm did NOT apply to Free ("- 1", _)*))
20.12 @@ -125,36 +125,36 @@
20.13 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
20.14 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
20.15 val thy = Proof_Context.init_global @{theory Partial_Fractions}
20.16 -val expr = TermC.parseNEW' thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
20.17 +val expr = ParseC.parse_test thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
20.18 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
20.19
20.20 -val expr = TermC.parseNEW' thy "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
20.21 +val expr = ParseC.parse_test thy "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
20.22 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
20.23
20.24 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
20.25 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
20.26 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
20.27 -val t = TermC.parseNEW' thy "(-8 - 2*x + x \<up> 2) is_expanded_in x";
20.28 +val t = ParseC.parse_test thy "(-8 - 2*x + x \<up> 2) is_expanded_in x";
20.29 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
20.30 if UnparseC.term t' = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
20.31 andalso id = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
20.32 then () else error "eval_is_expanded_in x ..changed";
20.33
20.34 val thy = Proof_Context.init_global @{theory Partial_Fractions}
20.35 -val t = TermC.parseNEW' thy "(-8 - 2*AA + AA \<up> 2) is_expanded_in AA";
20.36 +val t = ParseC.parse_test thy "(-8 - 2*AA + AA \<up> 2) is_expanded_in AA";
20.37 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
20.38 if UnparseC.term t' = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
20.39 andalso id = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
20.40 then () else error "eval_is_expanded_in AA ..changed";
20.41
20.42
20.43 -val t = TermC.parseNEW' thy "(8 + 2*x + x \<up> 2) is_poly_in x";
20.44 +val t = ParseC.parse_test thy "(8 + 2*x + x \<up> 2) is_poly_in x";
20.45 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
20.46 if UnparseC.term t' = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
20.47 andalso id = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
20.48 then () else error "is_poly_in x ..changed";
20.49
20.50 -val t = TermC.parseNEW' thy "(8 + 2*AA + AA \<up> 2) is_poly_in AA";
20.51 +val t = ParseC.parse_test thy "(8 + 2*AA + AA \<up> 2) is_poly_in AA";
20.52 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
20.53 if UnparseC.term t' = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
20.54 andalso id = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
20.55 @@ -162,10 +162,10 @@
20.56
20.57
20.58 val thy = Proof_Context.init_global @{theory Partial_Fractions}
20.59 -val expr = TermC.parseNEW' thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
20.60 +val expr = ParseC.parse_test thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
20.61 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
20.62
20.63 -val expr = TermC.parseNEW' thy "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
20.64 +val expr = ParseC.parse_test thy "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
20.65 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
20.66
20.67 "-------- investigate (new 2002) uniary minus --------------------------------------------------";
20.68 @@ -191,7 +191,7 @@
20.69 | _ => error "internal representation of \"0 - ?x = - ?x\" changed";
20.70
20.71
20.72 -val t = TermC.parseNEW' thy "- 1";
20.73 +val t = ParseC.parse_test thy "- 1";
20.74 TermC.atom_trace_detail @{context} t;
20.75 (*
20.76 ***
20.77 @@ -205,7 +205,7 @@
20.78 "======= these external values all have the same internal representation";
20.79 (* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)
20.80 (*----------------------------------- vvvvv -------------------------------------------*)
20.81 -val t = TermC.parseNEW' thy "-x";
20.82 +val t = ParseC.parse_test thy "-x";
20.83 TermC.atom_trace_detail @{context} t;
20.84 (**** -------------
20.85 *** Free ( -x, real)*)
20.86 @@ -213,7 +213,7 @@
20.87 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
20.88 | _ => error "internal representation of \"-x\" changed";
20.89 (*----------------------------------- vvvvv -------------------------------------------*)
20.90 -val t = TermC.parseNEW' thy "- x";
20.91 +val t = ParseC.parse_test thy "- x";
20.92 TermC.atom_trace_detail @{context} t;
20.93 (**** -------------
20.94 *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
20.95 @@ -221,7 +221,7 @@
20.96 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
20.97 | _ => error "internal representation of \"- x\" changed";
20.98 (*----------------------------------- vvvvvv ------------------------------------------*)
20.99 -val t = TermC.parseNEW' thy "-(x)";
20.100 +val t = ParseC.parse_test thy "-(x)";
20.101 TermC.atom_trace_detail @{context} t;
20.102 (**** -------------
20.103 *** Free ( -x, real)*)
21.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Mon Jan 30 12:38:17 2023 +0100
21.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Tue Jan 31 10:49:17 2023 +0100
21.3 @@ -53,53 +53,53 @@
21.4 val thy = @{theory};
21.5 val ctxt = Proof_Context.init_global thy;
21.6
21.7 - val t1 = TermC.parseNEW' ctxt "lhs (-8 - 2*x + x \<up> 2 = 0)";
21.8 + val t1 = ParseC.parse_test ctxt "lhs (-8 - 2*x + x \<up> 2 = 0)";
21.9 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t1;
21.10 if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
21.11 else error "polyeq.sml: diff.behav. in lhs";
21.12
21.13 - val t2 = TermC.parseNEW' ctxt "(-8 - 2*x + x \<up> 2) is_expanded_in x";
21.14 + val t2 = ParseC.parse_test ctxt "(-8 - 2*x + x \<up> 2) is_expanded_in x";
21.15 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t2;
21.16 if (UnparseC.term t) = "True" then ()
21.17 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
21.18
21.19 - val t0 = TermC.parseNEW' ctxt "(sqrt(x)) is_poly_in x";
21.20 + val t0 = ParseC.parse_test ctxt "(sqrt(x)) is_poly_in x";
21.21 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t0;
21.22 if (UnparseC.term t) = "False" then ()
21.23 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
21.24
21.25 - val t3 = TermC.parseNEW' ctxt "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
21.26 + val t3 = ParseC.parse_test ctxt "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
21.27 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t3;
21.28 if (UnparseC.term t) = "True" then ()
21.29 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
21.30
21.31 - val t4 = TermC.parseNEW' ctxt "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
21.32 + val t4 = ParseC.parse_test ctxt "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
21.33 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t4;
21.34 if (UnparseC.term t) = "True" then ()
21.35 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
21.36
21.37 - val t6 = TermC.parseNEW' ctxt "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
21.38 + val t6 = ParseC.parse_test ctxt "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
21.39 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t6;
21.40 if (UnparseC.term t) = "True" then ()
21.41 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
21.42
21.43 - val t3 = TermC.parseNEW' ctxt"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
21.44 + val t3 = ParseC.parse_test ctxt"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
21.45 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t3;
21.46 if (UnparseC.term t) = "True" then ()
21.47 else error "polyeq.sml: diff.behav. in has_degree_in_in";
21.48
21.49 - val t3 = TermC.parseNEW' ctxt "((sqrt(x)) has_degree_in x) = 2";
21.50 + val t3 = ParseC.parse_test ctxt "((sqrt(x)) has_degree_in x) = 2";
21.51 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t3;
21.52 if (UnparseC.term t) = "False" then ()
21.53 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
21.54
21.55 - val t4 = TermC.parseNEW' ctxt
21.56 + val t4 = ParseC.parse_test ctxt
21.57 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
21.58 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t4;
21.59 if (UnparseC.term t) = "False" then ()
21.60 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
21.61
21.62 -val t5 = TermC.parseNEW' ctxt
21.63 +val t5 = ParseC.parse_test ctxt
21.64 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
21.65 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t5;
21.66 if (UnparseC.term t) = "True" then ()
21.67 @@ -134,7 +134,7 @@
21.68 ----------- 28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy
21.69
21.70 (*Aufgabe zum Einstieg in die Arbeit...*)
21.71 - val t = TermC.parseNEW' ctxt "a*b - (a+b)*x + x \<up> 2 = 0";
21.72 + val t = ParseC.parse_test ctxt "a*b - (a+b)*x + x \<up> 2 = 0";
21.73 (*ein 'ruleset' aus Poly.ML wird angewandt...*)
21.74 val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
21.75 UnparseC.term t;
21.76 @@ -164,9 +164,9 @@
21.77 *)
21.78
21.79 "------ 15.11.02 --------------------------";
21.80 - val t = TermC.parseNEW' ctxt "1 + a * x + b * x";
21.81 - val bdv = TermC.parseNEW' ctxt "bdv";
21.82 - val a = TermC.parseNEW' ctxt "a";
21.83 + val t = ParseC.parse_test ctxt "1 + a * x + b * x";
21.84 + val bdv = ParseC.parse_test ctxt "bdv";
21.85 + val a = ParseC.parse_test ctxt "a";
21.86
21.87 Rewrite.trace_on := false; (*true false*)
21.88 (* Anwenden einer Regelmenge aus Termorder.ML: *)
21.89 @@ -178,7 +178,7 @@
21.90 UnparseC.term t;
21.91 "1 + b * x + x * a";
21.92
21.93 - val t = TermC.parseNEW' ctxt "1 + a * (x + b * x) + a \<up> 2";
21.94 + val t = ParseC.parse_test ctxt "1 + a * (x + b * x) + a \<up> 2";
21.95 val SOME (t,_) =
21.96 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
21.97 UnparseC.term t;
21.98 @@ -187,7 +187,7 @@
21.99 UnparseC.term t;
21.100 "1 + (x + b * x) * a + a \<up> 2";
21.101
21.102 - val t = TermC.parseNEW' ctxt "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
21.103 + val t = ParseC.parse_test ctxt "1 + a \<up> 2 * x + b * a + 7*a \<up> 2";
21.104 val SOME (t,_) =
21.105 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
21.106 UnparseC.term t;
21.107 @@ -207,7 +207,7 @@
21.108 get_thm Termorder.thy "bdv_n_collect";
21.109 get_thm (theory "Isac_Knowledge") "bdv_n_collect";
21.110 *)
21.111 - val t = TermC.parseNEW' ctxt "a \<up> 2 * x + 7 * a \<up> 2";
21.112 + val t = ParseC.parse_test ctxt "a \<up> 2 * x + 7 * a \<up> 2";
21.113 val SOME (t,_) =
21.114 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
21.115 UnparseC.term t;
21.116 @@ -340,14 +340,14 @@
21.117 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
21.118 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
21.119 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------";
21.120 - val substa = [(TermC.empty, TermC.parseNEW' ctxt "a::real")];
21.121 - val substb = [(TermC.empty, TermC.parseNEW' ctxt "b::real")];
21.122 - val substx = [(TermC.empty, TermC.parseNEW' ctxt "x::real")];
21.123 + val substa = [(TermC.empty, ParseC.parse_test ctxt "a::real")];
21.124 + val substb = [(TermC.empty, ParseC.parse_test ctxt "b::real")];
21.125 + val substx = [(TermC.empty, ParseC.parse_test ctxt "x::real")];
21.126
21.127 - val x1 = TermC.parseNEW' ctxt "a + b + x::real";
21.128 - val x2 = TermC.parseNEW' ctxt "a + x + b::real";
21.129 - val x3 = TermC.parseNEW' ctxt "a + x + b::real";
21.130 - val x4 = TermC.parseNEW' ctxt "x + a + b::real";
21.131 + val x1 = ParseC.parse_test ctxt "a + b + x::real";
21.132 + val x2 = ParseC.parse_test ctxt "a + x + b::real";
21.133 + val x3 = ParseC.parse_test ctxt "a + x + b::real";
21.134 + val x4 = ParseC.parse_test ctxt "x + a + b::real";
21.135
21.136 if ord_make_polynomial_in false(*true*) thy substx (x1,x2) = true(*LESS *) then ()
21.137 else error "termorder.sml diff.behav ord_make_polynomial_in #1";
21.138 @@ -358,22 +358,22 @@
21.139 if ord_make_polynomial_in false(*true*) thy substb (x1,x2) = false(*GREATER*) then ()
21.140 else error "termorder.sml diff.behav ord_make_polynomial_in #3";
21.141
21.142 - val aa = TermC.parseNEW' ctxt "- 1 * a * x::real";
21.143 - val bb = TermC.parseNEW' ctxt "x \<up> 3::real";
21.144 + val aa = ParseC.parse_test ctxt "- 1 * a * x::real";
21.145 + val bb = ParseC.parse_test ctxt "x \<up> 3::real";
21.146 if ord_make_polynomial_in false(*true*) thy substx (aa, bb) = true(*LESS *) then ()
21.147 else error "termorder.sml diff.behav ord_make_polynomial_in #4";
21.148
21.149 - val aa = TermC.parseNEW' ctxt "- 1 * a * x";
21.150 - val bb = TermC.parseNEW' ctxt "x \<up> 3";
21.151 + val aa = ParseC.parse_test ctxt "- 1 * a * x";
21.152 + val bb = ParseC.parse_test ctxt "x \<up> 3";
21.153 if ord_make_polynomial_in false(*true*) thy substa (aa, bb) = false(*GREATER*) then ()
21.154 else error "termorder.sml diff.behav ord_make_polynomial_in #5";
21.155
21.156 (* und nach dem Re-engineering der Termorders in den 'rulesets'
21.157 kannst Du die 'gr"osste' Variable frei w"ahlen: *)
21.158 - val bdv= TermC.parseNEW' ctxt "bdv ::real";
21.159 - val x = TermC.parseNEW' ctxt "x ::real";
21.160 - val a = TermC.parseNEW' ctxt "a ::real";
21.161 - val b = TermC.parseNEW' ctxt "b ::real";
21.162 + val bdv= ParseC.parse_test ctxt "bdv ::real";
21.163 + val x = ParseC.parse_test ctxt "x ::real";
21.164 + val a = ParseC.parse_test ctxt "a ::real";
21.165 + val b = ParseC.parse_test ctxt "b ::real";
21.166 val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,a)] make_polynomial_in x2;
21.167 if UnparseC.term t' = "b + x + a" then ()
21.168 else error "termorder.sml diff.behav ord_make_polynomial_in #11";
21.169 @@ -385,13 +385,13 @@
21.170 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
21.171
21.172 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
21.173 - val ppp = TermC.parseNEW' ctxt ppp';
21.174 + val ppp = ParseC.parse_test ctxt ppp';
21.175 val SOME (t', _) = rewrite_set_inst_ ctxt false [(bdv,x)] make_polynomial_in ppp;
21.176 if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then ()
21.177 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
21.178
21.179 val ttt' = "(3*x + 5)/18 ::real";
21.180 - val ttt = TermC.parseNEW' ctxt ttt';
21.181 + val ttt = ParseC.parse_test ctxt ttt';
21.182 val SOME (uuu,_) = rewrite_set_inst_ ctxt false [(bdv,x)] make_polynomial_in ttt;
21.183 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
21.184 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
21.185 @@ -1009,8 +1009,8 @@
21.186 see --- val rls = calculate_RootRat > calculate_Rational ---*)
21.187 val thy = @{theory PolyEq};
21.188 val ctxt = Proof_Context.init_global thy;
21.189 -val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
21.190 -val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";
21.191 +val inst = [((the o (ParseC.term_opt ctxt)) "bdv::real", (the o (ParseC.term_opt ctxt)) "x::real")];
21.192 +val t = (the o (ParseC.term_opt ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";
21.193
21.194 val rls = complete_square;
21.195 val SOME (t,asm) = rewrite_set_inst_ ctxt true inst rls t;
21.196 @@ -1060,7 +1060,7 @@
21.197 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
21.198 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
21.199 "---- test the asm_rls ----";
21.200 - val t1 = TermC.parseNEW' ctxt "0 <= (10/3/2) \<up> 2 - 1";
21.201 + val t1 = ParseC.parse_test ctxt "0 <= (10/3/2) \<up> 2 - 1";
21.202 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_erls t1;
21.203 val t' = UnparseC.term t;
21.204 (*if t'= \<^const_name>\<open>True\<close> then ()
22.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Mon Jan 30 12:38:17 2023 +0100
22.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Tue Jan 31 10:49:17 2023 +0100
22.3 @@ -338,7 +338,7 @@
22.4 \ (((Try (Rewrite_Set ordne_alphabetisch False)) #> \
22.5 \ (Try (Rewrite_Set fasse_zusammen False)) #> \
22.6 \ (Try (Rewrite_Set verschoenere False))) t_t)"
22.7 -val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
22.8 +val sc = (inst_abs o (ParseC.parse_test ctxt)) str;
22.9 TermC.atom_trace_detail @{context} sc;
22.10
22.11 "----------- me simplification.for_polynomials.with_minus";
22.12 @@ -445,7 +445,7 @@
22.13 \ in (Repeat((Try (Repeat (Calculate ''TIMES''))) #> \
22.14 \ (Try (Repeat (Calculate ''PLUS''))) #> \
22.15 \ (Try (Repeat (Calculate ''MINUS''))))) e_e)"
22.16 -val sc = (inst_abs o (TermC.parseNEW' ctxt)) str;
22.17 +val sc = (inst_abs o (ParseC.parse_test ctxt)) str;
22.18 TermC.atom_trace_detail @{context} sc;
22.19
22.20 "----------- pbl polynom probe -----------------------------------";
23.1 --- a/test/Tools/isac/Knowledge/rateq.sml Mon Jan 30 12:38:17 2023 +0100
23.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Tue Jan 31 10:49:17 2023 +0100
23.3 @@ -20,22 +20,22 @@
23.4 "------------ pbl: rational, univariate, equation ----------------";
23.5 "------------ pbl: rational, univariate, equation ----------------";
23.6 "------------ pbl: rational, univariate, equation ----------------";
23.7 -val t = TermC.parseNEW' ctxt "(1/b+1/x=1) is_ratequation_in x";
23.8 +val t = ParseC.parse_test ctxt "(1/b+1/x=1) is_ratequation_in x";
23.9 val SOME (t_, _) = rewrite_set_ ctxt false RatEq_prls t;
23.10 val result = UnparseC.term t_;
23.11 if result <> "True" then error "rateq.sml: new behaviour 1:" else ();
23.12
23.13 -val t = TermC.parseNEW' ctxt "(sqrt(x)=1) is_ratequation_in x";
23.14 +val t = ParseC.parse_test ctxt "(sqrt(x)=1) is_ratequation_in x";
23.15 val SOME (t_, _) = rewrite_set_ ctxt false RatEq_prls t;
23.16 val result = UnparseC.term t_;
23.17 if result <> "False" then error "rateq.sml: new behaviour 2:" else ();
23.18
23.19 -val t = TermC.parseNEW' ctxt "(x=- 1) is_ratequation_in x";
23.20 +val t = ParseC.parse_test ctxt "(x=- 1) is_ratequation_in x";
23.21 val SOME (t_,_) = rewrite_set_ ctxt false RatEq_prls t;
23.22 val result = UnparseC.term t_;
23.23 if result <> "False" then error "rateq.sml: new behaviour 3:" else ();
23.24
23.25 -val t = TermC.parseNEW' ctxt "(3 + x \<up> 2 + 1/(x \<up> 2+3)=1) is_ratequation_in x";
23.26 +val t = ParseC.parse_test ctxt "(3 + x \<up> 2 + 1/(x \<up> 2+3)=1) is_ratequation_in x";
23.27 val SOME (t_,_) = rewrite_set_ ctxt false RatEq_prls t;
23.28 val result = UnparseC.term t_;
23.29 if result <> "True" then error "rateq.sml: new behaviour 4:" else ();
23.30 @@ -145,7 +145,7 @@
23.31 val (f,asm) = case p_ of Frm => (get_obj g_form pt p , [])
23.32 | Res => get_obj g_result pt p;
23.33 UnparseC.term f = "[x = 1 / 5]"; (*the current formula*)
23.34 - val vp = (Proof_Context.init_global thy, pred) |-> parseNEW |> the |> mk_set thy pt p f;
23.35 + val vp = (Proof_Context.init_global thy, pred) |-> ParseC.term_opt |> the |> mk_set thy pt p f;
23.36 val (bdv, asms) = vp;
23.37
23.38 UnparseC.term bdv = "x";
24.1 --- a/test/Tools/isac/Knowledge/rational-1.sml Mon Jan 30 12:38:17 2023 +0100
24.2 +++ b/test/Tools/isac/Knowledge/rational-1.sml Tue Jan 31 10:49:17 2023 +0100
24.3 @@ -124,7 +124,7 @@
24.4 val expT = HOLogic.realT
24.5 val Free (_, baseT) = (hd o vars o ParseC.parse_test @{context}) "12 * x \<up> 3 * y \<up> 4 * z \<up> 6";
24.6 val p = [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 5])]
24.7 -val vs = TermC.vars_of (the (parseNEW ctxt "12 * x \<up> 3 * y \<up> 4 * z \<up> 6"))
24.8 +val vs = TermC.vars_of (the (ParseC.term_opt ctxt "12 * x \<up> 3 * y \<up> 4 * z \<up> 6"))
24.9 (*precondition for [(c, es),...]: legth es = length vs*)
24.10 ;
24.11 if UnparseC.term (term_of_poly baseT expT vs p) = "1 + 7 * y \<up> 8 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 5"
24.12 @@ -245,7 +245,7 @@
24.13 (*---------- fun cancel_p with Const AA *)
24.14 val thy = @{theory Partial_Fractions};
24.15 val ctxt = Proof_Context.init_global @{theory}
24.16 -val SOME t = TermC.parseNEW ctxt "2 * AA / 2"; (* Const (\<^const_name>\<open>AA\<close>, "real") *)
24.17 +val SOME t = ParseC.term_opt ctxt "2 * AA / 2"; (* Const (\<^const_name>\<open>AA\<close>, "real") *)
24.18
24.19 val SOME (t', _) = rewrite_set_ ctxt true cancel_p t;
24.20 case t' of
25.1 --- a/test/Tools/isac/Knowledge/rational-2.sml Mon Jan 30 12:38:17 2023 +0100
25.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml Tue Jan 31 10:49:17 2023 +0100
25.3 @@ -372,7 +372,7 @@
25.4 val ctxt = Proof_Context.init_global thy;
25.5
25.6 (*---------- (1) with Free A, B ----------------------------------------------------------------*)
25.7 -val t = (the o (parseNEW ctxt)) "3 = A / 2 + A / 4 + (B / 2 + - 1 * B / (2::real))";
25.8 +val t = (the o (ParseC.term_opt ctxt)) "3 = A / 2 + A / 4 + (B / 2 + - 1 * B / (2::real))";
25.9 (* required for applying thms in rewriting \<up> ^*)
25.10 (* we get details from here..*)
25.11
25.12 @@ -381,7 +381,7 @@
25.13 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + - 1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
25.14 (* |||||||||||||||||||||||||||||||||||| *)
25.15
25.16 -val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| GUESS 1 GUESS 1 GUESS 1 GUESS 1 *)
25.17 +val t = (the o (ParseC.term_opt ctxt))(* ||||||||||||||||||||||||| GUESS 1 GUESS 1 GUESS 1 GUESS 1 *)
25.18 "A / 2 + A / 4 + (B / 2 + - 1 * B / (2::real))";
25.19 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
25.20 val NONE = (*case*) check_frac_sum t (*of*)
25.21 @@ -389,7 +389,7 @@
25.22 (* Rewrite.trace_on:
25.23 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + - 1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
25.24 (* |||||||||||||||||||||||||||| *)
25.25 -val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| GUESS 2 GUESS 2 GUESS 2 GUESS 2 *)
25.26 +val t = (the o (ParseC.term_opt ctxt))(* ||||||||||||||||||||||||| GUESS 2 GUESS 2 GUESS 2 GUESS 2 *)
25.27 "A / 4 + (B / 2 + - 1 * B / (2::real))";
25.28 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
25.29 val SOME ((n1, d1), (n2, d2)) = (*case*) check_frac_sum t (*of*);
25.30 @@ -413,7 +413,7 @@
25.31 | _ => error "monom_of_term Free changed 2";
25.32
25.33 (*---------- (2) with Const AA, BB --------------------------------------------------------------*)
25.34 -val t = (the o (parseNEW ctxt)) "3 = AA / 2 + AA / 4 + (BB / 2 + - 1 * BB / 2)";
25.35 +val t = (the o (ParseC.term_opt ctxt)) "3 = AA / 2 + AA / 4 + (BB / 2 + - 1 * BB / 2)";
25.36 (*AA :: real*)
25.37 (* we get details from here..*)
25.38
25.39 @@ -421,7 +421,7 @@
25.40 (* Rewrite.trace_on:
25.41 add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + - 1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
25.42 (* |||||||||||||||||||||||||||||||||||| *)
25.43 -val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| *)
25.44 +val t = (the o (ParseC.term_opt ctxt))(* ||||||||||||||||||||||||| *)
25.45 "AA / 2 + AA / 4 + (BB / 2 + - 1 * BB / 2)";
25.46 "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
25.47 val NONE = (*case*) check_frac_sum t (*of*)
25.48 @@ -750,7 +750,7 @@
25.49 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))"
25.50 andalso ThmC.string_of_thm thm =
25.51 (string_of_thm (Thm.make_thm @{theory "Isac_Knowledge"}
25.52 - (Trueprop $ (TermC.parseNEW' ctxt "9 = 3 \<up> 2"))) then ()
25.53 + (Trueprop $ (ParseC.parse_test ctxt "9 = 3 \<up> 2"))) then ()
25.54 else error "rational.sml next_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";
25.55 \---------------------------------------------------------------------------------------/*)
25.56
25.57 @@ -769,7 +769,7 @@
25.58 val SOME (r as (Thm (str, thm))) = nex revsets t;
25.59 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso
25.60 ThmC.string_of_thm thm = (string_of_thm (ThmC_Def.make_thm @{theory "Isac_Knowledge"}
25.61 - (Trueprop $ (TermC.parseNEW' ctxt "9 = 3 \<up> 2"))) then ()
25.62 + (Trueprop $ (ParseC.parse_test ctxt "9 = 3 \<up> 2"))) then ()
25.63 else error "rational.sml next_rule (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";
25.64
25.65 (*check the next rule*)
25.66 @@ -1601,7 +1601,7 @@
25.67 "-------- fun eval_get_denominator -------------------------------------------";
25.68 val thy = @{theory Isac_Knowledge};
25.69 val ctxt = Proof_Context.init_global thy;
25.70 -val t = TermC.parseNEW' ctxt "get_denominator ((a +x)/b)";
25.71 +val t = ParseC.parse_test ctxt "get_denominator ((a +x)/b)";
25.72 val SOME (_, t') = eval_get_denominator "" 0 t ctxt;
25.73 if UnparseC.term t' = "get_denominator ((a + x) / b) = b"
25.74 then () else error "get_denominator ((a + x) / b) = b"
26.1 --- a/test/Tools/isac/Knowledge/rootrat.sml Mon Jan 30 12:38:17 2023 +0100
26.2 +++ b/test/Tools/isac/Knowledge/rootrat.sml Tue Jan 31 10:49:17 2023 +0100
26.3 @@ -22,7 +22,7 @@
26.4 *)
26.5 val thy = @{theory RootRat};
26.6 val ctxt = Proof_Context.init_global thy;
26.7 -val t = (the o (parseNEW ctxt))
26.8 +val t = (the o (ParseC.term_opt ctxt))
26.9 ("- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - -8) | \nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - -8))");
26.10
26.11 val rls = calculate_Rational;
27.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Mon Jan 30 12:38:17 2023 +0100
27.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Tue Jan 31 10:49:17 2023 +0100
27.3 @@ -28,37 +28,37 @@
27.4 "------------ tests on predicates -------------------------------";
27.5 "------------ tests on predicates -------------------------------";
27.6 "------------ tests on predicates -------------------------------";
27.7 -val t1 = TermC.parseNEW' ctxt "(-8 - sqrt(x) + x \<up> 2) is_rootRatAddTerm_in x";
27.8 +val t1 = ParseC.parse_test ctxt "(-8 - sqrt(x) + x \<up> 2) is_rootRatAddTerm_in x";
27.9 val SOME (t,_) = rewrite_set_ ctxt false RootRatEq_prls t1;
27.10 if (UnparseC.term t) = "False" then ()
27.11 else error "rootrateq.sml: diff.behav. 1 in is_rootRatAddTerm_in";
27.12
27.13 -val t1 = TermC.parseNEW' ctxt "(1/x) is_rootRatAddTerm_in x";
27.14 +val t1 = ParseC.parse_test ctxt "(1/x) is_rootRatAddTerm_in x";
27.15 val SOME (t,_) = rewrite_set_ ctxt false RootRatEq_prls t1;
27.16 if (UnparseC.term t) = "False" then ()
27.17 else error "rootrateq.sml: diff.behav. 2 in is_rootRatAddTerm_in";
27.18
27.19 -val t1 = TermC.parseNEW' ctxt "(1/sqrt(x)) is_rootRatAddTerm_in x";
27.20 +val t1 = ParseC.parse_test ctxt "(1/sqrt(x)) is_rootRatAddTerm_in x";
27.21 val SOME (t,_) = rewrite_set_ ctxt false RootRatEq_prls t1;
27.22 if (UnparseC.term t) = "False" then ()
27.23 else error "rootrateq.sml: diff.behav. 3 in is_rootRatAddTerm_in";
27.24
27.25 -val t1 = TermC.parseNEW' ctxt "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
27.26 +val t1 = ParseC.parse_test ctxt "(1/(sqrt(x)+1)) is_rootRatAddTerm_in x";
27.27 val SOME (t,_) = rewrite_set_ ctxt false RootRatEq_prls t1;
27.28 if (UnparseC.term t) = "True" then ()
27.29 else error "rootrateq.sml: diff.behav. 4 in is_rootRatAddTerm_in";
27.30
27.31 -val t1 = TermC.parseNEW' ctxt "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
27.32 +val t1 = ParseC.parse_test ctxt "(3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
27.33 val SOME (t,_) = rewrite_set_ ctxt false RootRatEq_prls t1;
27.34 if (UnparseC.term t) = "True" then ()
27.35 else error "rootrateq.sml: diff.behav. 5 in is_rootRatAddTerm_in";
27.36
27.37 -val t1 = TermC.parseNEW' ctxt "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
27.38 +val t1 = ParseC.parse_test ctxt "(1/(1+sqrt(y)) + 3 + 1/(1+sqrt(x))) is_rootRatAddTerm_in x";
27.39 val SOME (t,_) = rewrite_set_ ctxt false RootRatEq_prls t1;
27.40 if (UnparseC.term t) = "True" then ()
27.41 else error "rootrateq.sml: diff.behav. 6 in is_rootRatAddTerm_in";
27.42
27.43 -val t1 = TermC.parseNEW' ctxt "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
27.44 +val t1 = ParseC.parse_test ctxt "(1/(1+sqrt(x)) + 3 + 1/(1+sqrt(y))) is_rootRatAddTerm_in x";
27.45 val SOME (t,_) = rewrite_set_ ctxt false RootRatEq_prls t1;
27.46 if (UnparseC.term t) = "True" then ()
27.47 else error "rootrateq.sml: diff.behav. 7 in is_rootRatAddTerm_in";
27.48 @@ -96,7 +96,7 @@
27.49 f2str f = "1 = 2 * (1 + - 1 * sqrt x)";
27.50 nxt = ("Rewrite_Set", Rewrite_Set "make_rooteq");
27.51 (*... these ar the step's arguments; from these we do directly ...*)
27.52 -val SOME t = parseNEW ctxt "1 = 2 * (1 + - 1 * sqrt x)"
27.53 +val SOME t = ParseC.term_opt ctxt "1 = 2 * (1 + - 1 * sqrt x)"
27.54 val SOME (t, _) = rewrite_set_ thy true make_rooteq t;
27.55 UnparseC.term t = "1 = 2 + - 2 * sqrt x";
27.56 (*... which works; thus error must be in script interpretation*)
28.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Mon Jan 30 12:38:17 2023 +0100
28.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Tue Jan 31 10:49:17 2023 +0100
28.3 @@ -36,7 +36,7 @@
28.4 val thy = @{theory Complex_Main};
28.5 val ctxt = @{context};
28.6 val thm = @{thm add.commute};
28.7 -val t = TermC.parseNEW' ctxt "((r + u) + t) + (s::real)";
28.8 +val t = ParseC.parse_test ctxt "((r + u) + t) + (s::real)";
28.9 "----- from old: fun rewrite__";
28.10 val bdv = [];
28.11 val r = TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm));
28.12 @@ -488,7 +488,7 @@
28.13 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
28.14 val thy = @{theory RatEq};
28.15 val ctxt = Proof_Context.init_global thy;
28.16 -val SOME t = TermC.parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
28.17 +val SOME t = ParseC.term_opt ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
28.18 val rls = get_rls ctxt "RatEq_eliminate"
28.19
28.20 val SOME (t''''', asm''''') =
29.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon Jan 30 12:38:17 2023 +0100
29.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue Jan 31 10:49:17 2023 +0100
29.3 @@ -101,8 +101,8 @@
29.4 "Below there are the steps which found out the reason: \n" ^
29.5 "store_pbt mistakenly stored that theory.";
29.6 val ctxt = Proof_Context.init_global @{theory Isac_Knowledge};
29.7 -val SOME t = parseNEW ctxt "filterExpression (X = 3 / (z - 1/4 + - 1/8 * (1/(z::real))))";
29.8 -val SOME t = parseNEW ctxt "stepResponse (x[n::real]::bool)";
29.9 +val SOME t = ParseC.term_opt ctxt "filterExpression (X = 3 / (z - 1/4 + - 1/8 * (1/(z::real))))";
29.10 +val SOME t = ParseC.term_opt ctxt "stepResponse (x[n::real]::bool)";
29.11
29.12 val fmz = ["filterExpression (X = 3 / (z - 1/4 + - 1/8 * (1/(z::real))))", "boundVariable z",
29.13 "stepResponse (x[n::real]::bool)"];
29.14 @@ -308,7 +308,7 @@
29.15 (*val ("ok", (_, c, ptp as (_,p))) = *)Step_Solve.by_term ptp' (encode ifo);
29.16 "~~~~~ fun Step_Solve.by_term , args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =
29.17 (cs', (encode ifo));
29.18 -val SOME f_in = TermC.parseNEW (get_ctxt pt pos) istr
29.19 +val SOME f_in = ParseC.term_opt (get_ctxt pt pos) istr
29.20 val f_succ = get_curr_formula (pt, pos);
29.21 f_succ = f_in = false;
29.22 val NONE = CAS_Cmd.input f_in
30.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Mon Jan 30 12:38:17 2023 +0100
30.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Tue Jan 31 10:49:17 2023 +0100
30.3 @@ -39,7 +39,7 @@
30.4 then raise error "else not covered by test"
30.5 else
30.6 let
30.7 -(*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
30.8 +(*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..ParseC.parse_test*)
30.9 (*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
30.10 (*old*) in (pI, (pors, pctxt), mI) end;
30.11 ( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
31.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Mon Jan 30 12:38:17 2023 +0100
31.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Tue Jan 31 10:49:17 2023 +0100
31.3 @@ -33,13 +33,13 @@
31.4 val (p'',_,f,nxt,_,pt'') = me nxt p [] pt; (*nxt = Rewrite_Set_Inst..OK isolate_bdv*);
31.5 get_ctxt pt'' p'' |> ContextC.is_empty; (*OKfalse*)
31.6 val ctxt = get_ctxt pt'' p'';
31.7 -val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
31.8 +val SOME t = ParseC.term_opt ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
31.9 get_loc pt'' p'' |> snd |> ContextC.is_empty; (**OKfalse*)
31.10
31.11 val (p,_,f,nxt,_,pt) = me nxt p'' [] pt''; (*nxt = Rewrite_Set "Test_simplify"*);
31.12 get_ctxt pt p |> ContextC.is_empty; (*false*)
31.13 val ctxt = get_ctxt pt p;
31.14 -val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
31.15 +val SOME t = ParseC.term_opt ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
31.16 get_loc pt p |> snd |> ContextC.is_empty; (*false*)
31.17 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", ...]) *);
31.18
32.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Mon Jan 30 12:38:17 2023 +0100
32.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Tue Jan 31 10:49:17 2023 +0100
32.3 @@ -95,7 +95,7 @@
32.4 (*case*)
32.5 Step_Solve.by_term ptp (encode ifo) (*of*);
32.6 "~~~~~ fun by_term , args:"; val ((pt, pos as (p, _)), istr) = (ptp, (encode ifo));
32.7 - val SOME f_in =(*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*);
32.8 + val SOME f_in =(*case*) ParseC.term_opt (get_ctxt pt pos) istr (*of*);
32.9 val pos_pred = lev_back(*'*) pos
32.10 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
32.11 val f_succ = Ctree.get_curr_formula (pt, pos);
33.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Mon Jan 30 12:38:17 2023 +0100
33.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Tue Jan 31 10:49:17 2023 +0100
33.3 @@ -134,13 +134,13 @@
33.4 (*--------------(2): does divide work in Test_simplify ?: ------*)
33.5 val thy = @{theory Test};
33.6 val ctxt = (ThyC.id_to_ctxt "Test")
33.7 - val t = TermC.parseNEW' ctxt "6 / 2";
33.8 + val SOME t = ParseC.term_opt ctxt "6 / 2";
33.9 val rls = Test_simplify;
33.10 val (t,_) = the (rewrite_set_ ctxt false rls t);
33.11 (*val t = Free ("3", "Real.real") : term*)
33.12
33.13 (*--------------(3): is_num works ?: -------------------------------------*)
33.14 - val t = TermC.parseNEW' ctxt "2 is_num";
33.15 + val SOME t = ParseC.term_opt ctxt "2 is_num";
33.16 TermC.atom_trace_detail @{context} t;
33.17 rewrite_set_ ctxt false tval_rls t;
33.18 (*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)
33.19 @@ -155,19 +155,19 @@
33.20 (*-------------- eval_cancel works: *)
33.21 val thy = @{theory Test};
33.22 val rls = Test_simplify;
33.23 - val t = TermC.parseNEW' ctxt "(-4) / 2";
33.24 + val SOME t = ParseC.term_opt ctxt "(-4) / 2";
33.25
33.26 val SOME (_, t) = eval_cancel "xxx" \<^const_name>\<open>divide\<close> t thy;
33.27
33.28 (*--------------(5): reproduce (1) with simpler term: ------------*)
33.29 - val t = TermC.parseNEW' ctxt "(3+5)/(2::real)";
33.30 + val SOME t = ParseC.term_opt ctxt "(3+5)/(2::real)";
33.31 case rewrite_set_ ctxt false rls t of
33.32 SOME (t', []) =>
33.33 if UnparseC.term t' = "4" then ()
33.34 else error "rewrite_set_ (3+5)/2 changed 1"
33.35 | _ => error "rewrite_set_ (3+5)/2 changed 2";
33.36
33.37 - val t = TermC.parseNEW' ctxt "(3+1+2*x)/(2::real)";
33.38 + val SOME t = ParseC.term_opt ctxt "(3+1+2*x)/(2::real)";
33.39 case rewrite_set_ ctxt false rls t of
33.40 SOME (t', _) =>
33.41 if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
33.42 @@ -202,7 +202,7 @@
33.43
33.44
33.45 (*===================*)
33.46 - val t = TermC.parseNEW' ctxt "x + (- 1 + -3) / (2::real)";
33.47 + val SOME t = ParseC.term_opt ctxt "x + (- 1 + -3) / (2::real)";
33.48 val SOME (res, []) = rewrite_set_ ctxt false rls t;
33.49 if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_ x + (- 1 + -3) / 2 changed";
33.50 "x + (-4) / 2";
33.51 @@ -224,17 +224,17 @@
33.52 " ================= evaluate.sml: calculate_ 2002 =================== ";
33.53
33.54 val thy = @{theory Test};
33.55 - val t = TermC.parseNEW' ctxt "12 / 3";
33.56 + val SOME t = ParseC.term_opt ctxt "12 / 3";
33.57 val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(Know_Store.get_calcs @{theory},"DIVIDE")))t;
33.58 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
33.59 "12 / 3 = 4";
33.60 val thy = @{theory Test};
33.61 - val t = TermC.parseNEW' ctxt "4 \<up> 2";
33.62 +val SOME t = ParseC.term_opt ctxt "4 \<up> 2";
33.63 val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(Know_Store.get_calcs @{theory},"POWER"))) t;
33.64 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
33.65 "4 ^ 2 = 16";
33.66
33.67 - val t = TermC.parseNEW' ctxt "((1 + 2) * 4 / 3) \<up> 2";
33.68 + val SOME t = ParseC.term_opt ctxt "((1 + 2) * 4 / 3) \<up> 2";
33.69 val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(Know_Store.get_calcs @{theory},"PLUS"))) t;
33.70 "1 + 2 = 3";
33.71 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t;
33.72 @@ -259,7 +259,7 @@
33.73 else ();
33.74
33.75 (*13.9.02 *** calc: operator = pow not defined*)
33.76 - val t = TermC.parseNEW' ctxt "3 \<up> 2";
33.77 + val SOME t = ParseC.term_opt ctxt "3 \<up> 2";
33.78 val SOME (thmID,thm) =
33.79 adhoc_thm ctxt (the(LibraryC.assoc(Know_Store.get_calcs @{theory},"POWER"))) t;
33.80 (*** calc: operator = pow not defined*)
33.81 @@ -404,12 +404,12 @@
33.82 if str = "#less_4_4" andalso ThmC.string_of_thm ctxt thm = "(4 < 4) = False"
33.83 then () else error "adhoc_thm 4 < 4 changed";
33.84
33.85 -val SOME t = parseNEW @{context} "a < 4";
33.86 +val SOME t = ParseC.term_opt @{context} "a < 4";
33.87 case adhoc_thm ctxt (isa_str, eval_fn) t of
33.88 NONE => () | _ => error "adhoc_thm a < 4 does NOT result in NONE";
33.89
33.90 val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "PLUS");
33.91 -val SOME t = parseNEW @{context} "1 + (2::real)";
33.92 +val SOME t = ParseC.term_opt @{context} "1 + (2::real)";
33.93 val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t;
33.94 if str = "#: 1 + 2 = 3" andalso ThmC.string_of_thm ctxt thm = "1 + 2 = 3"
33.95 then () else error "adhoc_thm 1 + 2 changed";
34.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml Mon Jan 30 12:38:17 2023 +0100
34.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Tue Jan 31 10:49:17 2023 +0100
34.3 @@ -90,7 +90,7 @@
34.4 "-------- fun eval_is_num ----------------------------------------------------------------------";
34.5 "-------- fun eval_is_num ----------------------------------------------------------------------";
34.6 val ctxt = Proof_Context.init_global @{theory Test}
34.7 -val t = TermC.parseNEW' ctxt "2 is_num";
34.8 +val SOME t = ParseC.term_opt ctxt "2 is_num";
34.9 case rewrite_set_ ctxt false tval_rls t of
34.10 SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
34.11 | _ => error "2 is_num CHANGED";
34.12 @@ -253,84 +253,84 @@
34.13 "-------- fun eval_occurs_in -------------------------------------------------------------------";
34.14 "-------- fun eval_occurs_in -------------------------------------------------------------------";
34.15 "-------- fun eval_occurs_in -------------------------------------------------------------------";
34.16 -val v = TermC.parseNEW' ctxt "x";
34.17 -val t = TermC.parseNEW' ctxt "1";
34.18 +val v = ParseC.parse_test ctxt "x";
34.19 +val t = ParseC.parse_test ctxt "1";
34.20 if occurs_in v t then error "factor_right_deg (1) x ..changed" else ();
34.21
34.22 -val v = TermC.parseNEW' ctxt "AA";
34.23 -val t = TermC.parseNEW' ctxt "1";
34.24 +val v = ParseC.parse_test ctxt "AA";
34.25 +val t = ParseC.parse_test ctxt "1";
34.26 if occurs_in v t then error "factor_right_deg (1) AA ..changed" else ();
34.27
34.28 (*----------*)
34.29 -val v = TermC.parseNEW' ctxt "x";
34.30 -val t = TermC.parseNEW' ctxt "a*b+c";
34.31 +val v = ParseC.parse_test ctxt "x";
34.32 +val t = ParseC.parse_test ctxt "a*b+c";
34.33 if occurs_in v t then error "factor_right_deg (a*b+c) x ..changed" else ();
34.34
34.35 -val v = TermC.parseNEW' ctxt "AA";
34.36 -val t = TermC.parseNEW' ctxt "a*b+c";
34.37 +val v = ParseC.parse_test ctxt "AA";
34.38 +val t = ParseC.parse_test ctxt "a*b+c";
34.39 if occurs_in v t then error "factor_right_deg (a*b+c) AA ..changed" else ();
34.40
34.41 (*----------*)
34.42 -val v = TermC.parseNEW' ctxt "x";
34.43 -val t = TermC.parseNEW' ctxt "a*x+c";
34.44 +val v = ParseC.parse_test ctxt "x";
34.45 +val t = ParseC.parse_test ctxt "a*x+c";
34.46 if occurs_in v t then () else error "factor_right_deg (a*x+c) x ..changed";
34.47
34.48 -val v = TermC.parseNEW' ctxt "AA";
34.49 -val t = TermC.parseNEW' ctxt "a*AA+c";
34.50 +val v = ParseC.parse_test ctxt "AA";
34.51 +val t = ParseC.parse_test ctxt "a*AA+c";
34.52 if occurs_in v t then () else error "factor_right_deg (a*AA+c) AA ..changed";
34.53
34.54 (*----------*)
34.55 -val v = TermC.parseNEW' ctxt "x";
34.56 -val t = TermC.parseNEW' ctxt "(a*b+c)*x \<up> 7";
34.57 +val v = ParseC.parse_test ctxt "x";
34.58 +val t = ParseC.parse_test ctxt "(a*b+c)*x \<up> 7";
34.59 if occurs_in v t then () else error "factor_right_deg (a*b+c)*x \<up> 7) x ..changed";
34.60
34.61 -val v = TermC.parseNEW' ctxt "AA";
34.62 -val t = TermC.parseNEW' ctxt "(a*b+c)*AA \<up> 7";
34.63 +val v = ParseC.parse_test ctxt "AA";
34.64 +val t = ParseC.parse_test ctxt "(a*b+c)*AA \<up> 7";
34.65 if occurs_in v t then () else error "factor_right_deg (a*b+c)*AA \<up> 7) AA ..changed";
34.66
34.67 (*----------*)
34.68 -val v = TermC.parseNEW' ctxt "x";
34.69 -val t = TermC.parseNEW' ctxt "x \<up> 7";
34.70 +val v = ParseC.parse_test ctxt "x";
34.71 +val t = ParseC.parse_test ctxt "x \<up> 7";
34.72 if occurs_in v t then () else error "factor_right_deg (x \<up> 7) x ..changed";
34.73
34.74 -val v = TermC.parseNEW' ctxt "AA";
34.75 -val t = TermC.parseNEW' ctxt "AA \<up> 7";
34.76 +val v = ParseC.parse_test ctxt "AA";
34.77 +val t = ParseC.parse_test ctxt "AA \<up> 7";
34.78 if occurs_in v t then () else error "factor_right_deg (AA \<up> 7) AA ..changed";
34.79
34.80 (*----------*)
34.81 -val v = TermC.parseNEW' ctxt "x";
34.82 -val t = TermC.parseNEW' ctxt "(a*b+c)*x";
34.83 +val v = ParseC.parse_test ctxt "x";
34.84 +val t = ParseC.parse_test ctxt "(a*b+c)*x";
34.85 if occurs_in v t then () else error "factor_right_deg ((a*b+c)*x) x ..changed";
34.86
34.87 -val v = TermC.parseNEW' ctxt "AA";
34.88 -val t = TermC.parseNEW' ctxt "(a*b+c)*AA";
34.89 +val v = ParseC.parse_test ctxt "AA";
34.90 +val t = ParseC.parse_test ctxt "(a*b+c)*AA";
34.91 if occurs_in v t then () else error "factor_right_deg ((a*b+c)*AA) AA ..changed";
34.92
34.93 (*----------*)
34.94 -val v = TermC.parseNEW' ctxt "x";
34.95 -val t = TermC.parseNEW' ctxt "(a*b+x)*x";
34.96 +val v = ParseC.parse_test ctxt "x";
34.97 +val t = ParseC.parse_test ctxt "(a*b+x)*x";
34.98 if occurs_in v t then () else error "factor_right_deg ((a*b+x)*x) x ..changed";
34.99
34.100 -val v = TermC.parseNEW' ctxt "AA";
34.101 -val t = TermC.parseNEW' ctxt "(a*b+AA)*AA";
34.102 +val v = ParseC.parse_test ctxt "AA";
34.103 +val t = ParseC.parse_test ctxt "(a*b+AA)*AA";
34.104 if occurs_in v t then () else error "factor_right_deg ((a*b+AA)*AA) AA ..changed";
34.105
34.106 (*----------*)
34.107 -val v = TermC.parseNEW' ctxt "x";
34.108 -val t = TermC.parseNEW' ctxt "x";
34.109 +val v = ParseC.parse_test ctxt "x";
34.110 +val t = ParseC.parse_test ctxt "x";
34.111 if occurs_in v t then () else error "factor_right_deg (x) x ..changed";
34.112
34.113 -val v = TermC.parseNEW' ctxt "AA";
34.114 -val t = TermC.parseNEW' ctxt "AA";
34.115 +val v = ParseC.parse_test ctxt "AA";
34.116 +val t = ParseC.parse_test ctxt "AA";
34.117 if occurs_in v t then () else error "factor_right_deg (AA) AA ..changed";
34.118
34.119 (*----------*)
34.120 -val v = TermC.parseNEW' ctxt "x";
34.121 -val t = TermC.parseNEW' ctxt "ab - (a*b)*x";
34.122 +val v = ParseC.parse_test ctxt "x";
34.123 +val t = ParseC.parse_test ctxt "ab - (a*b)*x";
34.124 if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*x) x ..changed";
34.125
34.126 -val v = TermC.parseNEW' ctxt "AA";
34.127 -val t = TermC.parseNEW' ctxt "ab - (a*b)*AA";
34.128 +val v = ParseC.parse_test ctxt "AA";
34.129 +val t = ParseC.parse_test ctxt "ab - (a*b)*AA";
34.130 if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*AA) AA ..changed";
34.131
34.132
34.133 @@ -421,7 +421,7 @@
34.134 "-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------";
34.135 "-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------";
34.136 val (op_, ef) = the (LibraryC.assoc (Know_Store.get_calcs @{theory}, "TIMES"));
34.137 -val t = TermC.parseNEW' ctxt "2 * (3::real)";
34.138 +val t = ParseC.parse_test ctxt "2 * (3::real)";
34.139 (*val SOME (thmid,t') = *)get_pair ctxt op_ ef t;
34.140 ;
34.141 "~~~~~ fun get_pair, args:"; val(*3*)(thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =
35.1 --- a/test/Tools/isac/Specify/i-model.sml Mon Jan 30 12:38:17 2023 +0100
35.2 +++ b/test/Tools/isac/Specify/i-model.sml Tue Jan 31 10:49:17 2023 +0100
35.3 @@ -78,7 +78,7 @@
35.4 I_Model.check_single ctxt sel oris pbl model ct (*of*);
35.5 "~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str)
35.6 = (ctxt, sel, oris, pbl, model, ct);
35.7 - val SOME t =(*case*) TermC.parseNEW ctxt str (*of*);
35.8 + val SOME t =(*case*) ParseC.term_opt ctxt str (*of*);
35.9 (** )val ("", (2, [1], "#Given", Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), [Free ("q_0", _)]) =( **)
35.10 (**)val ("", ori', all) =(**)
35.11 (*case*) O_Model.contains ctxt m_field o_model t (*of*);
36.1 --- a/test/Tools/isac/Specify/o-model.sml Mon Jan 30 12:38:17 2023 +0100
36.2 +++ b/test/Tools/isac/Specify/o-model.sml Tue Jan 31 10:49:17 2023 +0100
36.3 @@ -48,14 +48,15 @@
36.4 (*+*)val (o_model, ctxt) = (Problem.from_store ctxt pI |> #model |>
36.5 O_Model.init thy fmz);
36.6 "~~~~~ fun init , args:"; val (fmz, thy, pbt) = (fmz, thy, Problem.from_store ctxt pI |> #model);
36.7 - val ori = (map (fn str => str
36.8 - |> TermC.parseNEW'' thy
36.9 - |> Input_Descript.split
36.10 - |> add_field thy pbt) fmz)
36.11 - |> add_variants;
36.12 + val (ts, ctxt) = ContextC.init_while_parsing fmz thy
36.13 + val ori =
36.14 + (map (fn t => t
36.15 + |> Input_Descript.split
36.16 + |> add_field thy pbt) ts)
36.17 + |> add_variants;
36.18
36.19 (*+ decompose..*)
36.20 -(*+*)val aaa as Const (\<^const_name>\<open>Traegerlaenge\<close>, _) $ Free ("L", _) = (nth 1 fmz) |> TermC.parseNEW'' thy;
36.21 +(*+*)val aaa as Const (\<^const_name>\<open>Traegerlaenge\<close>, _) $ Free ("L", _) = (nth 1 fmz) |> ParseC.parse_test @{context};
36.22 (*+*)val bbb as (Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]) = aaa |> Input_Descript.split;
36.23 (*+*)val ccc as ("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]) = bbb |> add_field thy pbt;
36.24 (*+ WHY IS THE LIST IN "#Relate" NOT DECOMPOSED?...*)
36.25 @@ -74,7 +75,7 @@
36.26 ("#undef", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]),
36.27 _, _] =
36.28 (map (fn str => str
36.29 - |> TermC.parseNEW'' thy
36.30 + |> ParseC.parse_test @{context}
36.31 |> Input_Descript.split
36.32 |> add_field thy pbt) fmz);
36.33 (*+*)val eee as [(0, ("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)])),
37.1 --- a/test/Tools/isac/Specify/refine.sml Mon Jan 30 12:38:17 2023 +0100
37.2 +++ b/test/Tools/isac/Specify/refine.sml Tue Jan 31 10:49:17 2023 +0100
37.3 @@ -27,20 +27,20 @@
37.4 val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"};
37.5
37.6 (*case 1: no refinement *)
37.7 -val (d1,ts1) = Input_Descript.split (TermC.parseNEW' ctxt "fixedValues [aaa = 0]");
37.8 -val (d2,ts2) = Input_Descript.split (TermC.parseNEW' ctxt "errorBound (ddd = 0)");
37.9 +val (d1,ts1) = Input_Descript.split (ParseC.parse_test ctxt "fixedValues [aaa = 0]");
37.10 +val (d2,ts2) = Input_Descript.split (ParseC.parse_test ctxt "errorBound (ddd = 0)");
37.11 val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: O_Model.T;
37.12
37.13 (*case 2: refined to pbt without children *)
37.14 -val (d2,ts2) = Input_Descript.split (TermC.parseNEW' ctxt "relations [aaa333]");
37.15 +val (d2,ts2) = Input_Descript.split (ParseC.parse_test ctxt "relations [aaa333]");
37.16 val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;
37.17
37.18 (*case 3: refined to pbt with children *)
37.19 -val (d2,ts2) = Input_Descript.split (TermC.parseNEW' ctxt "valuesFor [aaa222]");
37.20 +val (d2,ts2) = Input_Descript.split (ParseC.parse_test ctxt "valuesFor [aaa222]");
37.21 val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;
37.22
37.23 (*case 4: refined to children (without child)*)
37.24 -val (d3,ts3) = Input_Descript.split (TermC.parseNEW' ctxt "boundVariable aaa222yyy");
37.25 +val (d3,ts3) = Input_Descript.split (ParseC.parse_test ctxt "boundVariable aaa222yyy");
37.26 val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:O_Model.T;
37.27
37.28 (*=================================================================
38.1 --- a/test/Tools/isac/Specify/specify.sml Mon Jan 30 12:38:17 2023 +0100
38.2 +++ b/test/Tools/isac/Specify/specify.sml Tue Jan 31 10:49:17 2023 +0100
38.3 @@ -622,7 +622,7 @@
38.4 I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
38.5 "~~~~~ ~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
38.6 (ctxt, m_field, oris, i_model, m_patt, ct);
38.7 -(*.NEW*) val SOME (t as (descriptor $ _)) = (*case*) TermC.parseNEW ctxt str (*of*);
38.8 +(*.NEW*) val SOME (t as (descriptor $ _)) = (*case*) ParseC.term_opt ctxt str (*of*);
38.9 (*.NEW*) val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
38.10
38.11 val ("", (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), [Free ("x", _)]) =
38.12 @@ -913,7 +913,7 @@
38.13
38.14 "~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
38.15 (ctxt, sel, oris, met, ((#model o MethodC.from_store ctxt) cmI), ct);
38.16 - val SOME t = (*case*) TermC.parseNEW ctxt str (*of*);
38.17 + val SOME t = (*case*) ParseC.term_opt ctxt str (*of*);
38.18
38.19 (*+*)val Const (\<^const_name>\<open>Biegelinie\<close>, _) $ Free ("y", _) = t;
38.20