Merge #518

518: Define ShiftLeftExpression and ShiftRightExpression evaluation for integer types r=Veykril a=scrabsha

Fix #517.

I did my best to follow the style of the rest of the specification.

Thank you for building Ferrocene!!

Co-authored-by: Sasha Pourcelot <[email protected]>

src/expressions.rst

@@ -1719,7 +1719,17 @@ The :t:`evaluation` of a :t:`shift left expression` proceeds as follows:
    The :t:`right operand` is evaluated.
 
 #. :dp:`fls_f0p70y92k14f`
-   ``core::ops::Shl::shl(left_operand, right_operand)`` is invoked.
+   If the types of both :t:`[operand]s` are :t:`[integer type]s`, then the
+   :t:`shift left expression` evaluates to the value of the left :t:`operand`
+   whose bits are shifted left by the number of positions the right :t:`operand`
+   evaluates to. Vacated bits are filled with zeros. ``lhs << rhs`` evaluates
+   to :math:`\mathrm{lhs} \times 2 ^ \mathrm{rhs}`, casted to the type of the left
+   :t:`operand`. If the value of the right :t:`operand` is negative or greater
+   than or equal to the width of the left operand, then the operation results in
+   an :t:`arithmetic overflow`.
+
+#. :dp:`fls_8QGbl2SBU3R0`
+   Otherwise, ``core::ops::Shl::shl(left_operand, right_operand)`` is invoked.
 
 :dp:`fls_303r0u6ug215`
 The :t:`evaluation` of a :t:`shift right expression` proceeds as follows:
@@ -1730,8 +1740,20 @@ The :t:`evaluation` of a :t:`shift right expression` proceeds as follows:
 #. :dp:`fls_gurl2ve58drz`
    The :t:`right operand` is evaluated.
 
+#. :dp:`fls_r02OGonXp93A`
+   If the types of both :t:`[operand]s` are :t:`[integer type]s`, then the
+   :t:`shift right expression` evaluates to the value of the left :t:`operand`
+   whose bits are shifted right by the number of positions the right
+   :t:`operand` evaluates to. If the type of the left :t:`operand` is any
+   :t:`signed integer type` and is negative, then vacated bits are filled
+   with ones. Otherwise, vacated bits are filled with zeros. ``lhs >> rhs``
+   evaluates to :math:`\mathrm{lhs} / 2^ \mathrm{rhs}`, casted to the type of
+   the left :t:`operand`. If the value of the right :t:`operand` is negative,
+   greater than or equal to the width of the left operand, then the operation
+   results in an :t:`arithmetic overflow`.
+
 #. :dp:`fls_xkyj83mcb9d5`
-   ``core::ops::Shr::shr(left_operand, right_operand)`` is invoked.
+   Otherwise, ``core::ops::Shr::shr(left_operand, right_operand)`` is invoked.
 
 .. rubric:: Examples
 
@@ -5099,9 +5121,11 @@ Arithmetic Overflow
 -------------------
 
 :dp:`fls_oFIRXBPXu6Zv`
-An :t:`arithmetic overflow` occurs when an :t:`arithmetic expression` or a
-:t:`negation expression` computes a :t:`value` of a :t:`scalar type` that lies
-outside of the range of valid :t:`[value]s` for the :t:`scalar type`.
+An :t:`arithmetic overflow` occurs when an :t:`operator expression` computes a
+:t:`value` of a :t:`scalar type` that lies outside of the range of valid
+:t:`[value]s` for the :t:`scalar type` or when one or more :t:`operand` of an
+:t:`operator expression` lies outside of the range of valid :t:`[value]s` for
+the operation.
 
 .. rubric:: Dynamic Semantics