Handle units of literal constants by means of rules for the empty unit

RationaleMCP/0027/ReadMe.md

@@ -0,0 +1,34 @@
+# Modelica Change Proposal MCP-0027<br/>Units of Literal Constants
+Francesco Casella, Henrik Tidefelt
+
+**(In Development)**
+
+## Summary
+The purpose of this MCP is to allow more unit errors to be detected by giving more expressions the unit `"1"` instead of having an undefined unit.
+The problem with undefined unit is that it gets in the way of carrying out checking of units (which tools tend to deal with by not checking units at all where this happens).
+
+## Revisions
+| Date | Description |
+| --- | --- |
+| 2022-10-04 | Henrik Tidefelt. Filling this document with initial content. |
+
+## Contributor License Agreement
+All authors of this MCP or their organizations have signed the "Modelica Contributor License Agreement".
+
+## Rationale
+FIXME
+
+## Backwards Compatibility
+As current Modelica doesn't clearly reject some models with non-sensical combination of units, this MCP will break backwards compatibility by turning at least some of these invalid.
+
+## Tool Implementation
+None, so far.
+
+### Experience with Prototype
+N/A
+
+## Required Patents
+To the best of our knowledge, there are no patents that would conflict with the incorporation of this MCP.
+
+## References
+(None.)

chapters/unitexpressions.tex

@@ -89,3 +89,171 @@ \section{The Syntax of Unit Expressions}\label{the-syntax-of-unit-expressions}
 
 The unit expression \lstinline!"T"! means tesla, but note that the letter \lstinline!T! is also the symbol for the prefix tera which has a multiplier value of 10\textsuperscript{12}.
 \end{example}
+
+
+\section{Unit Checking}\label{unit-checking}
+
+How to verify that units are used in compatible ways is current not fully determined by the specification.
+This section gives rules for certain situations, but in general tools are expected to reason according to standard dimensional analysis..
+
+
+\subsection{Standard Dimensional Analysis}\label{standard-dimensional-analysis}
+
+This section gives an incomplete characterization of \emph{standard dimensional analysis}, also referred to as just \firstuse{dimensional analysis}.
+What is described below applies to unit checking in Modelica -- \emph{standard dimensional analysis} could have additional meanings in other contexts.
+While Modelica has a concept of \willintroduce{empty units} (described in later sections), standard dimensional analysis only deals with non-empty units such as \lstinline!"m"!, \lstinline!"m/s"!, or \lstinline!"1"!.
+It consists of two parts:
+\begin{itemize}
+\item
+  Unit compatibility requirements.
+\item
+  Rules for deriving the unit of an expression.
+\end{itemize}
+
+Examples of unit compatibility requirements that must be met in Modelica:
+\begin{itemize}
+\item
+  The expression of a declaration equation must have the same unit as the component to which it belongs.
+\item
+  The two sides of an equation or assignment statement must have the same unit.
+\item
+  The two operands of the additive operators \lstinline!+! and \lstinline!-! must have the same unit.
+\item
+  In a function call, the unit of an argument expression must match the unit (unless empty, see below) of the corresponding function input component.
+\end{itemize}
+
+% TODO: Replace these examples by giving unit semantics where operators and built-in functions are defined in the specification,
+% and just include some likes to places where such semantics are given.
+Examples of unit derivation in Modelica:
+\begin{itemize}
+\item
+  The result of additive operators has the same unit as the operands.
+\item
+  The result of multiplication has a unit obtained by adding the exponents of the operands' units.
+\item
+  Built-in operators such as \lstinline!pre! and \lstinline!previous! preserve units, while \lstinline!der! changes the unit by dividing it by \lstinline!"s"!.
+\end{itemize}
+
+
+\subsection{Empty and Undefined Units}\label{empty-and-undefined-units}
+
+In situations where the specification does not prescribe how to determine the unit of an expression, the unit of that expression is said to be \firstuse[undefined unit]{undefined}.
+It is then not possible for a tool to reject the equation (or other construct) with support in the specification, and options for the tool include silently not performing unit checking, or applying checks based dimensional analysis.
+
+The unit of an expression can also be defined as being \firstuse[empty unit]{empty}, see below.
+In certain places (see below), expressions with empty unit can be implicitly cast to suitable units.
+When an expression with empty unit is implicitly cast to some unit, that unit is referred to as the \firstuse{inferred unit} of the expression.
+
+
+\subsection{Unit Inference}\label{unit-inference}
+
+Where the empty unit has no other defined meaning, it can be implicitly cast to unit \lstinline!"1"!.
+
+In some cases the empty unit can be implicitly cast to an inferred unit:
+\begin{itemize}
+\item
+  In binding equations and modifications:
+  \begin{itemize}
+  \item The entire expression of the binding or modification.
+  \item When the entire expression is an array construction, array concatenation and array range, then apply rules recursively for the direct subexpressions.
+  \end{itemize}
+\item
+  The entire argument expression in a function call.
+% To keep the design close to the bare minimum, this part is currently excluded:
+%\item
+%  For a translation-time constant with value 0.0:
+%  \begin{itemize}
+%  \item Expressions constituting the entire side of an equality or relation.
+%  \item The right hand side of an assignment.
+%  \item The direct subexpressions of array construction, array concatenation, and array range.
+%  \end{itemize}
+\end{itemize}
+
+
+\subsection{Expressions with Empty Unit}\label{expressions-with-empty-unit}
+
+This section describes conditions under which an expression has empty unit.
+Conditions not given here must not be interpreted as definitely not implying empty unit; instead, the unit may be currently undefined for some expressions, allowing the unit to be properly defined in future versions of the specification.
+
+Basic expressions defined to have empty unit:
+\begin{itemize}
+\item
+  \lstinline!Real! literals.
+\item
+  \lstinline!Integer! expressions implicitly cast to \lstinline!Real!.
+\end{itemize}
+
+Expressions defined to \emph{not} propagate the empty unit, thereby forcing inference of unit \lstinline!"1"!:
+\begin{itemize}
+\item
+  Addition, subtraction, multiplication and division operators when either operand has non-empty unit.
+\item
+  Right operand of binary exponentiation.
+\item
+  Component references outside of functions, where the component's declared \lstinline!unit!-attribute is \lstinline!""! (possibly by not being specified).
+  (Unit checking involving user-defined functions with empty unit on inputs and outputs is currently not defined.)
+\end{itemize}
+
+Built-in non-array operators, functions, and special expressions that propagate any unit (including empty):
+\begin{itemize}
+\item
+  When all operands have the same unit: negation, addition, and subtraction (scalar or element-wise).
+\end{itemize}
+
+Special situations in which the empty unit can be propagated up the expression tree:
+\begin{itemize}
+\item
+  Multiplication and division when both operands have empty unit.
+\end{itemize}
+
+\begin{example}
+Consider unit checking of the following declaration equation:
+\begin{lstlisting}[language=modelica]
+Real y(unit = "m") = 1 + 2.5 * 3;
+\end{lstlisting}
+The unit of the declaration equation right-hand side is determined as follows:
+\begin{itemize}
+\item The \lstinline!Real! literal \lstinline!2.5! has empty unit.
+\item The \lstinline!Integer! literals \lstinline!1! and \lstinline!3! are implicitly cast to \lstinline!Real!, and therefore have empty unit.
+\item The multiplication \lstinline!2.5 * 3! has empty unit, as multiplication can propagate the empty unit of both operands.
+\item The addition \lstinline!1 + (2.5 * 3)! has empty unit, as addition can propagate any unit as long as both operands have the same unit.
+\item The entire right-hand side expression gets inferred unit \lstinline!"m"! in order to be compatible with the component's declared \lstinline!unit!.
+\end{itemize}
+\end{example}
+
+\begin{example}
+Consider unit checking of the following erroneous declaration equation for \lstinline!y!:
+\begin{lstlisting}[language=modelica]
+Real x(unit = "m") = 1.0;
+Real y(unit = "m") = x^2 / 2;
+\end{lstlisting}
+The unit of the declaration equation right-hand side is determined as follows:
+\begin{itemize}
+\item The unit of \lstinline!x! is \lstinline!"m"!, and dimensional analysis gives that \lstinline!x^2! has unit \lstinline!"m2"!
+\item The \lstinline!Real! literal \lstinline!1.0! has empty unit, and gets inferred unit \lstinline!"m"!.
+\item As the left operand of \lstinline!x^2 / 2! is non-empty, the right operand cannot be empty, and hence empty unit of \lstinline!2! is implicitly cast to \lstinline!"1"!.
+\item Dimensional analysis then gives that the unit of \lstinline!x^2 / 2! is \lstinline!"m2"!, which is an error due to the required unit being \lstinline!"m"!.
+\end{itemize}
+\end{example}
+
+\begin{example}
+Consider the potential consequences of an undefined unit in the following declaration equation:
+\begin{lstlisting}[language=modelica]
+Real y(unit = "m") = sin(1.57);
+\end{lstlisting}
+To see that the unit of the declaration equation right-hand side is undefined, note that:
+\begin{itemize}
+\item The \lstinline!Real! literal \lstinline!1.57! has empty unit.
+\item The expression \lstinline!sin(1.57)! is not covered by the specification, and hence has undefined unit.
+\end{itemize}
+If a tool wants to proceed according to ``standard dimensional analysis'', alternatives include:
+\begin{itemize}
+\item
+  Assume that \lstinline!sin! is a mapping from unit \lstinline!"1"! to unit \lstinline!"1"!.
+  The unit of \lstinline!1.57! then defaults to \lstinline!"1"! (alternatively, the same unit could be obtained by inference).
+  The unit of \lstinline!sin(1.57)! is then found to be \lstinline!"1"!, which is an error due to the required unit being \lstinline!"m"!.
+\item
+  Assume that \lstinline!sin! preserves both the unit \lstinline!"1"! and the empty unit.
+  The empty unit of \lstinline!1.57! gets propagated to \lstinline!sin(1.57)!, which in turn gets inferred unit \lstinline!"m"!.
+\end{itemize}
+\end{example}