1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Oct 31 18:28:36 2022 +0100
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Nov 07 17:37:20 2022 +0100
1.3 @@ -513,11 +513,11 @@
1.4 but not\\ \ttfamily factors\_from\_solution.\normalfont
1.5 So we stepwise compare with an analogous case, \ttfamily get\_denominator
1.6 \normalfont successfully done above: We know that LIP evaluates
1.7 - expressions in the program by use of the \emph{srls}, so we try to get
1.8 - the original \emph{srls}.\\
1.9 + expressions in the program by use of the \emph{prog_rls}, so we try to get
1.10 + the original \emph{prog_rls}.\\
1.11
1.12 \begin{verbatim}
1.13 - val {srls,...} = MethodC.from_store ctxt ["SignalProcessing",
1.14 + val {prog_rls,...} = MethodC.from_store ctxt ["SignalProcessing",
1.15 "Z_Transform",
1.16 "Inverse"];
1.17 \end{verbatim}
1.18 @@ -531,14 +531,14 @@
1.19 parseNEW ctxt "factors_from_solution [(z::real)=1/2, z=-1/4]";
1.20 \end{verbatim}
1.21
1.22 - \par \noindent Rewrite the terms using srls:\\
1.23 - \ttfamily \par \noindent rewrite\_set\_ thy true srls t1;\\
1.24 - rewrite\_set\_ thy true srls t2;\\
1.25 + \par \noindent Rewrite the terms using prog_rls:\\
1.26 + \ttfamily \par \noindent rewrite\_set\_ thy true prog_rls t1;\\
1.27 + rewrite\_set\_ thy true prog_rls t2;\\
1.28 \par \noindent \normalfont Now we see a difference: \texttt{t1} gives
1.29 \texttt{SOME} but \texttt{t2} gives \texttt{NONE}. We look at the
1.30 - \emph{srls}:
1.31 + \emph{prog_rls}:
1.32 \begin{verbatim}
1.33 - val srls =
1.34 + val prog_rls =
1.35 Rule_Set.Repeat{id = "srls_InverseZTransform",
1.36 rules = [Eval("Rational.get_numerator",
1.37 eval_get_numerator "Rational.get_numerator"),
1.38 @@ -703,12 +703,12 @@
1.39 ML \<open>
1.40 val ansatz_rls = prep_rls @{theory} (
1.41 Rule_Set.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.42 - erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.43 + asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.44 rules = [
1.45 Thm ("ansatz_2nd_order",ThmC.numerals_to_Free @{thm ansatz_2nd_order}),
1.46 Thm ("equival_trans_2nd_order",ThmC.numerals_to_Free @{thm equival_trans_2nd_order})
1.47 ],
1.48 - scr = Empty_Prog});
1.49 + program = Empty_Prog});
1.50 \<close>
1.51
1.52 text\<open>\noindent We apply the ruleset\ldots\<close>
1.53 @@ -855,7 +855,7 @@
1.54 f2str fb;
1.55 \<close>
1.56
1.57 -text\<open>\noindent We compare our results with the pre calculated upshot.\<close>
1.58 +text\<open>\noindent We compare our results with the where_ calculated upshot.\<close>
1.59
1.60 ML \<open>
1.61 if f2str fa = "[A = 4]" then () else error "part.fract. eq4_1";
1.62 @@ -927,13 +927,13 @@
1.63 setup \<open>KEStore_Elems.add_mets
1.64 [MethodC.prep_input @{theory} "met_SP" [] e_metID
1.65 (["SignalProcessing"], [],
1.66 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.67 - errpats = [], nrls = Rule_Set.empty},
1.68 + {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
1.69 + errpats = [], rew_rls = Rule_Set.empty},
1.70 "empty_script"),
1.71 MethodC.prep_input @{theory} "met_SP_Ztrans" [] e_metID
1.72 (["SignalProcessing", "Z_Transform"], [],
1.73 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.74 - errpats = [], nrls = Rule_Set.empty},
1.75 + {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
1.76 + errpats = [], rew_rls = Rule_Set.empty},
1.77 "empty_script")]
1.78 \<close>
1.79
1.80 @@ -946,8 +946,8 @@
1.81 (["SignalProcessing", "Z_Transform", "Inverse"],
1.82 [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]),
1.83 ("#Find", ["stepResponse n_eq"])],
1.84 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.85 - errpats = [], nrls = Rule_Set.empty},
1.86 + {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
1.87 + errpats = [], rew_rls = Rule_Set.empty},
1.88 "empty_script")]
1.89 \<close>
1.90
1.91 @@ -960,8 +960,8 @@
1.92 (["SignalProcessing", "Z_Transform", "Inverse"],
1.93 [("#Given" , ["filterExpression X_eq", "boundVariable X_z"]),
1.94 ("#Find", ["stepResponse n_eq"])],
1.95 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.96 - errpats = [], nrls = Rule_Set.empty},
1.97 + {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
1.98 + errpats = [], rew_rls = Rule_Set.empty},
1.99 "Program InverseZTransform (Xeq::bool) =" ^ (*TODO boundVariable X_z*)
1.100 " (let X = Take Xeq;" ^
1.101 " X = Rewrite ruleZY X" ^
1.102 @@ -1088,17 +1088,17 @@
1.103 The evaluation of the functions is done by rewriting using this ruleset.\<close>
1.104
1.105 ML \<open>
1.106 - val srls =
1.107 + val prog_rls =
1.108 Rule_Set.Repeat {id="srls_InverseZTransform",
1.109 preconds = [],
1.110 rew_ord = ("termlessI",termlessI),
1.111 - erls = Rule_Set.append_rules "erls_in_srls_InverseZTransform" Rule_Set.empty
1.112 + asm_rls = Rule_Set.append_rules "erls_in_srls_InverseZTransform" Rule_Set.empty
1.113 [(*for asm in NTH_CONS ...*)
1.114 Eval (\<^const_name>\<open>less\<close>,eval_equ "#less_"),
1.115 (*2nd NTH_CONS pushes n+-1 into asms*)
1.116 Eval(\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")
1.117 ],
1.118 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.119 + prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.120 rules = [
1.121 Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.122 Eval(\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
1.123 @@ -1113,7 +1113,7 @@
1.124 Eval("Partial_Fractions.drop_questionmarks",
1.125 eval_drop_questionmarks "#drop_?")
1.126 ],
1.127 - scr = Empty_Prog};
1.128 + program = Empty_Prog};
1.129 \<close>
1.130
1.131
1.132 @@ -1130,8 +1130,8 @@
1.133 (["SignalProcessing", "Z_Transform", "Inverse"],
1.134 [("#Given" , ["filterExpression X_eq"]), (*TODO boundVariable X_z*)
1.135 ("#Find", ["stepResponse n_eq"])],
1.136 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = srls, prls = Rule_Set.empty, crls = Rule_Set.empty,
1.137 - errpats = [], nrls = Rule_Set.empty},
1.138 + {rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = prog_rls, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
1.139 + errpats = [], rew_rls = Rule_Set.empty},
1.140 "Program InverseZTransform (X_eq::bool) = "^
1.141 (*(1/z) instead of z \<up> -1*)
1.142 "(let X = Take X_eq; "^
1.143 @@ -1232,10 +1232,10 @@
1.144 [Free ("x", _) $ _]
1.145 )
1.146 ],_
1.147 - ) = O_Model.init thy fmz ((#ppc o Problem.from_store) pI);
1.148 + ) = O_Model.init thy fmz ((#model o Problem.from_store) pI);
1.149
1.150 val Prog sc
1.151 - = (#scr o MethodC.from_store ctxt) ["SignalProcessing",
1.152 + = (#program o MethodC.from_store ctxt) ["SignalProcessing",
1.153 "Z_Transform",
1.154 "Inverse"];
1.155 atomty sc;
1.156 @@ -1311,7 +1311,7 @@
1.157 arguments in the arguments\ldots
1.158 \begin{verbatim}
1.159 val Prog s =
1.160 - (#scr o MethodC.from_store ctxt) ["SignalProcessing",
1.161 + (#program o MethodC.from_store ctxt) ["SignalProcessing",
1.162 "Z_Transform",
1.163 "Inverse"];
1.164 writeln (UnparseC.term s);
1.165 @@ -1518,7 +1518,7 @@
1.166 \<close>
1.167
1.168 text\<open>\noindent As a last step we check the tracing output of the last calc
1.169 - tree instruction and compare it with the pre-calculated result.\<close>
1.170 + tree instruction and compare it with the where_-calculated result.\<close>
1.171
1.172 section \<open>Improve and Transfer into Knowledge\<close>
1.173 text \<open>
1.174 @@ -1594,7 +1594,7 @@
1.175 \item Type-checking can be very tedious. One might even inspect the
1.176 parse-tree of the program with {\sisac}'s specific debug tools:
1.177 \begin{verbatim}
1.178 - val {scr = Prog t,...} =
1.179 + val {program = Prog t,...} =
1.180 MethodC.from_store ctxt ["simplification",
1.181 "of_rationals",
1.182 "to_partial_fraction"];