diff -r b7071d1dd263 -r 007ef64dbb08 doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex --- a/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Mon Oct 31 18:28:36 2022 +0100 +++ b/doc-isac/jrocnik/eJMT-paper/jrocnik_eJMT.tex Mon Nov 07 17:37:20 2022 +0100 @@ -802,12 +802,12 @@ 01 val inverse_z = Rls 02 {id = "inverse_z", 03 rew_ord = dummy_ord, - 04 erls = Erls, + 04 asm_rls = Erls, 05 rules = [Thm ("rule1", @{thm rule1}), Thm ("rule2", @{thm rule1}), 06 Thm ("rule3", @{thm rule3}), Thm ("rule4", @{thm rule4}), 07 Thm ("rule5", @{thm rule5}), Thm ("rule6", @{thm rule6})], 08 errpatts = [], - 09 scr = ""} + 09 program = ""} \end{verbatim}} \noindent The items, line by line, in the above record have the following purpose: @@ -819,7 +819,7 @@ line {\rm 12}). \item[03..04] both, (a) the rewrite-order~\cite{nipk:rew-all-that} -\textit{rew\_ord} and (b) the rule-set \textit{erls} are trivial here: +\textit{rew\_ord} and (b) the rule-set \textit{asm_rls} are trivial here: (a) the \textit{rules} in {\rm 07..12} don't need ordered rewriting and (b) the assumptions of the \textit{rules} need not be evaluated (they just go into the context during rewriting). @@ -830,7 +830,7 @@ and \textit{Calc} respectively; for the purpose of reflection both contain their identifiers. -\item[08..09] are error-patterns not discussed here and \textit{scr} +\item[08..09] are error-patterns not discussed here and \textit{program} is prepared to get a program, automatically generated by {\sisac} for producing intermediate rewrites when requested by the user. @@ -1109,7 +1109,7 @@ 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]), 09 ("#Find" , ["stepResponse n_eq"]), 10 ("#Post" , [" TODO "])]) - 11 prls + 11 where_rls 12 NONE 13 [["SignalProcessing","Z_Transform","Inverse"]]); 14 *} @@ -1163,9 +1163,9 @@ % because applied terms may be from 'subthy' as well as from super; % thus we take 'maxthy'; see match_ags !*) % cas : term option,(*'CAS-command'*) -% prls : rls, (* for preds in where_*) +% where_rls : rls, (* for preds in where_*) % where_: term list, (* where - predicates*) -% ppc : pat list, +% model : pat list, % (*this is the model-pattern; % it contains "#Given","#Where","#Find","#Relate"-patterns % for constraints on identifiers see "fun copy_name"*) @@ -1225,8 +1225,8 @@ 07 [ ("#Given", ["filterExpression X_eq", "domain D"]), 08 ("#Pre" , ["(rhs X_eq) is_continuous_in D"]), 09 ("#Find" , ["stepResponse n_eq"]), - 10 rew_ord erls - 11 srls prls nrls + 10 rew_ord asm_rls + 11 prog_rls where_rls rew_rls 12 errpats 13 program); 14 *} @@ -1244,8 +1244,8 @@ is not started. \item[10..11] all concern rewriting (the respective data are defined elsewhere): \textit{rew\_ord} is the rewrite order~\cite{nipk:rew-all-that} in case -\textit{program} contains a \textit{Rewrite} tactic; and in case the respective rule is a conditional rewrite-rule, \textit{erls} features evaluating the conditions. The rule-sets -\textit{srls, prls, nrls} feature evaluating (a) the ML-functions in the program (e.g. +\textit{program} contains a \textit{Rewrite} tactic; and in case the respective rule is a conditional rewrite-rule, \textit{asm_rls} features evaluating the conditions. The rule-sets +\textit{prog_rls, where_rls, rew_rls} feature evaluating (a) the ML-functions in the program (e.g. \textit{lhs, argument\_in, rhs} in the program on p.\pageref{s:impl}, (b) the pre-condition analogous to the specification in line 11 on p.\pageref{exp-spec} and (c) is required for the derivation-machinery checking user-input formulas. @@ -1466,7 +1466,7 @@ \noindent The entry is perfect. So what is the reason~? Ah, probably there is something messed up with the many rule-sets in the method, see \S\ref{meth} --- right, the function \texttt{argument\_in} is not contained in the respective -rule-set \textit{srls} \dots this just as an example of the intricacies in +rule-set \textit{prog_rls} \dots this just as an example of the intricacies in debugging a program in the present state of the prototype. \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl} @@ -2128,8 +2128,8 @@ % LocalWords: TP IST SPSC Telematics Dialogues dialogue HOL bool nat Hindley % LocalWords: Milner tt Subproblem Formulae ruleset generalisation initialised % LocalWords: axiomatization LCF Simplifiers simplifiers Isar rew Thm Calc SML -% LocalWords: recognised hoc Trueprop redexes Unsynchronized pre rhs ord erls -% LocalWords: srls prls nrls lhs errpats InverseZTransform SubProblem IDE IDEs +% LocalWords: recognised hoc Trueprop redexes Unsynchronized where_ rhs ord asm_rls +% LocalWords: prog_rls where_rls rew_rls lhs errpats InverseZTransform SubProblem IDE IDEs % LocalWords: univariate jEdit rls RealDef calclist familiarisation ons pos eq % LocalWords: mout ctree SignalProcessing frac ZZ Postcond Atools wiki SML's % LocalWords: mechanisation multi