Changeset 266732e


Ignore:
Timestamp:
Mar 9, 2024, 5:40:09 PM (8 weeks ago)
Author:
Peter A. Buhr <pabuhr@…>
Branches:
master
Children:
b64d0f4
Parents:
03606ce
Message:

switch to tabs, first attempt changing program-input style

Location:
doc/theses/mike_brooks_MMath
Files:
1 added
7 edited

Legend:

Unmodified
Added
Removed

  • doc/theses/mike_brooks_MMath/array.tex

    r03606ce r266732e  
    66
    77\begin{lstlisting}
    8     array(float, 99) x;    // x contains 99 floats
    9 
    10     void f( array(float, 42) & a ) {}
    11     f(x);                  // statically rejected: types are different
    12 
    13     forall( T, [N] )
    14     void g( array(T, N) & a, int i ) {
    15         T elem = a[i];     // dynamically checked: requires 0 <= i < N
    16     }
    17     g(x, 0);               // T is float, N is 99, succeeds
    18     g(x, 1000);            // T is float, N is 99, dynamic check fails
     8array(float, 99) x;    // x contains 99 floats
     9
     10void f( array(float, 42) & a ) {}
     11f(x);                  // statically rejected: types are different
     12
     13forall( T, [N] )
     14void g( array(T, N) & a, int i ) {
     15        T elem = a[i];     // dynamically checked: requires 0 <= i < N
     16}
     17g(x, 0);               // T is float, N is 99, succeeds
     18g(x, 1000);            // T is float, N is 99, dynamic check fails
    1919\end{lstlisting}
    2020
    … …  
    3131
    3232\begin{lstlisting}
    33     forall( [N] )
    34     void declDemo() {
    35         float a1[N];         // built-in type ("C array")
    36         array(float, N) a2;  // type from library
    37     }
     33forall( [N] )
     34void declDemo() {
     35        float a1[N];         // built-in type ("C array")
     36        array(float, N) a2;  // type from library
     37}
    3838\end{lstlisting}
    3939
    … …  
    5454My contributions are
    5555\begin{itemize}
    56     \item a type system enhancement that lets polymorphic functions and generic types be parameterized by a numeric value: @forall( [N] )@
    57     \item [TODO: general parking...]
    58     \item identify specific abilities brought by @array@
    59     \item Where there is a gap concerning this feature's readiness for prime-time, identification of specific workable improvements that are likely to close the gap
     56\item a type system enhancement that lets polymorphic functions and generic types be parameterized by a numeric value: @forall( [N] )@
     57\item TODO: general parking...
     58\item identify specific abilities brought by @array@
     59\item Where there is a gap concerning this feature's readiness for prime-time, identification of specific workable improvements that are likely to close the gap
    6060\end{itemize}
    6161
    6262
    63 
    6463\section{Definitions and design considerations}
    6564
     65
    6666\subsection{Dependent typing}
    6767
    6868
    69 
    70 
    7169\section{Features Added}
    7270
    7371The present work adds a type @array@ to the \CFA standard library~\cite{Cforall}.
    7472
    75 This array's length is statically managed and dynamically valued.  This static management achieves argument safety and suggests a path to subscript safety as future work (TODO: cross reference).
     73This array's length is statically managed and dynamically valued.
     74This static management achieves argument safety and suggests a path to subscript safety as future work (TODO: cross reference).
    7675
    7776This section presents motivating examples of the new array type's usage and follows up with definitions of the notations that appear.
    7877
    79 The core of the new array management is tracking all array lengths in the type system.  Dynamically valued lengths are represented using type variables.  The stratification of type variables preceding object declarations makes a length referenceable everywhere that it is needed.  For example, a declaration can share one length, @N@, among a pair of parameters and the return.
     78The core of the new array management is tracking all array lengths in the type system.
     79Dynamically valued lengths are represented using type variables.
     80The stratification of type variables preceding object declarations makes a length referenceable everywhere that it is needed.
     81For example, a declaration can share one length, @N@, among a pair of parameters and the return.
    8082\lstinputlisting[language=CFA, firstline=10, lastline=17]{hello-array.cfa}
    8183Here, the function @f@ does a pointwise comparison, checking if each pair of numbers is within half a percent of each other, returning the answers in a newly allocated @bool@ array.
    8284
    83 The array type uses the parameterized length information in its @sizeof@ determination, illustrated in the example's call to @alloc@.  That call requests an allocation of type @array(bool, N)@, which the type system deduces from the left-hand side of the initialization, into the return type of the @alloc@ call.  Preexisting \CFA behaviour is leveraged here, both in the return-type-only polymorphism, and the @sized(T)@-aware standard-library @alloc@ routine.  The new @array@ type plugs into this behaviour by implementing the @sized@/@sizeof@ assertion to have the intuitive meaning.  As a result, this design avoids an opportunity for programmer error by making the size/length communication to a called routine implicit, compared with C's @calloc@ (or the low-level \CFA analog @aalloc@), which take an explicit length parameter not managed by the type system.
     85The array type uses the parameterized length information in its @sizeof@ determination, illustrated in the example's call to @alloc@.
     86That call requests an allocation of type @array(bool, N)@, which the type system deduces from the left-hand side of the initialization, into the return type of the @alloc@ call.
     87Preexisting \CFA behaviour is leveraged here, both in the return-type-only polymorphism, and the @sized(T)@-aware standard-library @alloc@ routine.
     88The new @array@ type plugs into this behaviour by implementing the @sized@/@sizeof@ assertion to have the intuitive meaning.
     89As a result, this design avoids an opportunity for programmer error by making the size/length communication to a called routine implicit, compared with C's @calloc@ (or the low-level \CFA analog @aalloc@), which take an explicit length parameter not managed by the type system.
    8490
    8591\VRef[Figure]{f:fHarness} shows the harness to use the @f@ function illustrating how dynamic values are fed into the system.
    86 Here, the @a@ array is loaded with decreasing values, and the @b@ array with amounts off by a constant, giving relative differences within tolerance at first and out of tolerance later.  The program main is run with two different inputs of sequence length.
     92Here, the @a@ array is loaded with decreasing values, and the @b@ array with amounts off by a constant, giving relative differences within tolerance at first and out of tolerance later.
     93The program main is run with two different inputs of sequence length.
    8794
    8895\begin{figure}
    … …  
    9299\end{figure}
    93100
    94 The loops in the program main follow the more familiar pattern of using the ordinary variable @n@ to convey the length.  The type system implicitly captures this value at the call site (@main@ calling @f@) and makes it available within the callee (@f@'s loop bound).
     101The loops in the program main follow the more familiar pattern of using the ordinary variable @n@ to convey the length.
     102The type system implicitly captures this value at the call site (@main@ calling @f@) and makes it available within the callee (@f@'s loop bound).
    95103
    96104The two parts of the example show @n@ adapting a variable into a type-system managed length (at @main@'s declarations of @a@, @b@, and @result@), @N@ adapting in the opposite direction (at @f@'s loop bound), and a pass-thru use of a managed length (at @f@'s declaration of @ret@).
    97105
    98 The @forall( ...[N] )@ participates in the user-relevant declaration of the name @N@, which becomes usable in parameter/return declarations and in the function @b@. The present form is chosen to parallel the existing @forall@ forms:
     106The @forall( ...[N] )@ participates in the user-relevant declaration of the name @N@, which becomes usable in parameter/return declarations and in the function @b@.
     107The present form is chosen to parallel the existing @forall@ forms:
    99108\begin{cfa}
    100109forall( @[N]@ ) ... // array kind
    … …  
    115124@array( thing, N0, N1, ... )@ -- a type wrapping $\prod_i N_i$ adjacent occurrences of @thing@ objects
    116125\end{itemize}
    117 Unsigned integers have a special status in this type system.  Unlike how C++ allows @template< size_t N, char * msg, typename T >...@ declarations, \CFA does not accommodate values of any user-provided type.  TODO: discuss connection with dependent types.
    118 
    119 An example of a type error demonstrates argument safety.  The running example has @f@ expecting two arrays of the same length.  A compile-time error occurs when attempting to call @f@ with arrays whose lengths may differ.
    120 \lstinputlisting[language=CFA, firstline=60, lastline=65]{hello-array.cfa}
     126Unsigned integers have a special status in this type system.
     127Unlike how C++ allows
     128\begin{lstlisting}[language=c++]
     129template< size_t N, char * msg, typename T >... // declarations
     130\end{lstlisting}
     131\CFA does not accommodate values of any user-provided type.
     132TODO: discuss connection with dependent types.
     133An example of a type error demonstrates argument safety.
     134The running example has @f@ expecting two arrays of the same length.
     135A compile-time error occurs when attempting to call @f@ with arrays whose lengths may differ.
     136\begin{cfa}
     137forall( [M], [N] )
     138void bad( array(float, M) &a, array(float, N) &b ) {
     139        f( a, a ); // ok
     140        f( b, b ); // ok
     141        f( a, b ); // error
     142}
     143\end{cfa}
     144%\lstinputlisting[language=CFA, firstline=60, lastline=65]{hello-array.cfa}
    121145As is common practice in C, the programmer is free to cast, to assert knowledge not shared with the type system.
    122 \lstinputlisting[language=CFA, firstline=70, lastline=75]{hello-array.cfa}
     146\begin{cfa}
     147forall( [M], [N] )
     148void bad_fixed( array(float, M) & a, array(float, N) & b ) {
     149        if ( M == N ) {
     150            f( a, (array(float, M) &)b ); // cast b to matching type
     151        }
     152}
     153\end{cfa}
     154%\lstinputlisting[language=CFA, firstline=70, lastline=75]{hello-array.cfa}
    123155
    124156Argument safety and the associated implicit communication of array length work with \CFA's generic types too.
    … …  
    126158Doing so gives a refinement of C's ``flexible array member'' pattern, that allows nesting structures with array members anywhere within other structures.
    127159\lstinputlisting[language=CFA, firstline=10, lastline=16]{hello-accordion.cfa}
    128 This structure's layout has the starting offset of @cost_contribs@ varying in @Nclients@, and the offset of @total_cost@ varying in both generic parameters.  For a function that operates on a @request@ structure, the type system handles this variation transparently.
     160This structure's layout has the starting offset of @cost_contribs@ varying in @Nclients@, and the offset of @total_cost@ varying in both generic parameters.
     161For a function that operates on a @request@ structure, the type system handles this variation transparently.
    129162\lstinputlisting[language=CFA, firstline=40, lastline=47]{hello-accordion.cfa}
    130163In the example, different runs of the program result in different offset values being used.
    131164\lstinputlisting[language=CFA, firstline=60, lastline=76]{hello-accordion.cfa}
    132 The output values show that @summarize@ and its caller agree on both the offsets (where the callee starts reading @cost_contribs@ and where the callee writes @total_cost@).  Yet the call site still says just, ``pass the request.''
     165The output values show that @summarize@ and its caller agree on both the offsets (where the callee starts reading @cost_contribs@ and where the callee writes @total_cost@).
     166Yet the call site still says just, ``pass the request.''
    133167
    134168
    … …  
    136170\label{toc:mdimpl}
    137171
    138 
    139172TODO: introduce multidimensional array feature and approaches
    140173
    141 The new \CFA standard library @array@ datatype supports multidimensional uses more richly than the C array.  The new array's multidimensional interface and implementation, follows an array-of-arrays setup, meaning, like C's @float[n][m]@ type, one contiguous object, with coarsely-strided dimensions directly wrapping finely-strided dimensions.  This setup is in contrast with the pattern of array of pointers to other allocations representing a sub-array.  Beyond what C's type offers, the new array brings direct support for working with a noncontiguous array slice, allowing a program to work with dimension subscripts given in a non-physical order.  C and C++ require a programmer with such a need to manage pointer/offset arithmetic manually.
     174The new \CFA standard library @array@ datatype supports multidimensional uses more richly than the C array.
     175The new array's multidimensional interface and implementation, follows an array-of-arrays setup, meaning, like C's @float[n][m]@ type, one contiguous object, with coarsely-strided dimensions directly wrapping finely-strided dimensions.
     176This setup is in contrast with the pattern of array of pointers to other allocations representing a sub-array.
     177Beyond what C's type offers, the new array brings direct support for working with a noncontiguous array slice, allowing a program to work with dimension subscripts given in a non-physical order.
     178C and C++ require a programmer with such a need to manage pointer/offset arithmetic manually.
    142179
    143180Examples are shown using a $5 \times 7$ float array, @a@, loaded with increments of $0.1$ when stepping across the length-7 finely-strided dimension shown on columns, and with increments of $1.0$ when stepping across the length-5 coarsely-strided dimension shown on rows.
    144 \lstinputlisting[language=CFA, firstline=120, lastline=126]{hello-md.cfa}
     181%\lstinputlisting[language=CFA, firstline=120, lastline=126]{hello-md.cfa}
    145182The memory layout of @a@ has strictly increasing numbers along its 35 contiguous positions.
    146183
    147 A trivial form of slicing extracts a contiguous inner array, within an array-of-arrays.  Like with the C array, a lesser-dimensional array reference can be bound to the result of subscripting a greater-dimensional array, by a prefix of its dimensions.  This action first subscripts away the most coarsely strided dimensions, leaving a result that expects to be be subscripted by the more finely strided dimensions.
     184A trivial form of slicing extracts a contiguous inner array, within an array-of-arrays.
     185Like with the C array, a lesser-dimensional array reference can be bound to the result of subscripting a greater-dimensional array, by a prefix of its dimensions.
     186This action first subscripts away the most coarsely strided dimensions, leaving a result that expects to be be subscripted by the more finely strided dimensions.
    148187\lstinputlisting[language=CFA, firstline=60, lastline=66]{hello-md.cfa}
    149188\lstinputlisting[aboveskip=0pt, language=CFA, firstline=140, lastline=140]{hello-md.cfa}
    150189
    151 This function declaration is asserting too much knowledge about its parameter @c@, for it to be usable for printing either a row slice or a column slice.  Specifically, declaring the parameter @c@ with type @array@ means that @c@ is contiguous.  However, the function does not use this fact.  For the function to do its job, @c@ need only be of a container type that offers a subscript operator (of type @ptrdiff_t@ $\rightarrow$ @float@), with managed length @N@.  The new-array library provides the trait @ix@, so-defined.  With it, the original declaration can be generalized, while still implemented with the same body, to the latter declaration:
     190This function declaration is asserting too much knowledge about its parameter @c@, for it to be usable for printing either a row slice or a column slice.
     191Specifically, declaring the parameter @c@ with type @array@ means that @c@ is contiguous.
     192However, the function does not use this fact.
     193For the function to do its job, @c@ need only be of a container type that offers a subscript operator (of type @ptrdiff_t@ $\rightarrow$ @float@), with managed length @N@.
     194The new-array library provides the trait @ix@, so-defined.
     195With it, the original declaration can be generalized, while still implemented with the same body, to the latter declaration:
    152196\lstinputlisting[language=CFA, firstline=40, lastline=44]{hello-md.cfa}
    153197\lstinputlisting[aboveskip=0pt, language=CFA, firstline=145, lastline=145]{hello-md.cfa}
    154198
    155 Nontrivial slicing, in this example, means passing a noncontiguous slice to @print1d@.  The new-array library provides a ``subscript by all'' operation for this purpose.  In a multi-dimensional subscript operation, any dimension given as @all@ is left ``not yet subscripted by a value,'' implementing the @ix@ trait, waiting for such a value.
     199Nontrivial slicing, in this example, means passing a noncontiguous slice to @print1d@.
     200The new-array library provides a ``subscript by all'' operation for this purpose.
     201In a multi-dimensional subscript operation, any dimension given as @all@ is left ``not yet subscripted by a value,'' implementing the @ix@ trait, waiting for such a value.
    156202\lstinputlisting[language=CFA, firstline=150, lastline=151]{hello-md.cfa}
    157203
    158 The example has shown that @a[2]@ and @a[[2, all]]@ both refer to the same, ``2.*'' slice.  Indeed, the various @print1d@ calls under discussion access the entry with value 2.3 as @a[2][3]@, @a[[2,all]][3]@, and @a[[all,3]][2]@.  This design preserves (and extends) C array semantics by defining @a[[i,j]]@ to be @a[i][j]@ for numeric subscripts, but also for ``subscripting by all''.  That is:
     204The example has shown that @a[2]@ and @a[[2, all]]@ both refer to the same, ``2.*'' slice.
     205Indeed, the various @print1d@ calls under discussion access the entry with value 2.3 as @a[2][3]@, @a[[2,all]][3]@, and @a[[all,3]][2]@.
     206This design preserves (and extends) C array semantics by defining @a[[i,j]]@ to be @a[i][j]@ for numeric subscripts, but also for ``subscripting by all''.
     207That is:
    159208
    160209\begin{tabular}{cccccl}
    161     @a[[2,all]][3]@  &  $=$  &  @a[2][all][3]@  & $=$  &  @a[2][3]@  & (here, @all@ is redundant)  \\
    162     @a[[all,3]][2]@  &  $=$  &  @a[all][3][2]@  & $=$  &  @a[2][3]@  & (here, @all@ is effective)
     210@a[[2,all]][3]@  &  $=$  &  @a[2][all][3]@  & $=$  &  @a[2][3]@  & (here, @all@ is redundant)  \\
     211@a[[all,3]][2]@  &  $=$  &  @a[all][3][2]@  & $=$  &  @a[2][3]@  & (here, @all@ is effective)
    163212\end{tabular}
    164213
    … …  
    168217
    169218\begin{tabular}{ll}
    170     @a@  & 2-dimensional, want subscripts for coarse then fine \\
    171     @a[2]@  & 1-dimensional, want subscript for fine; lock coarse = 2 \\
    172     @a[2][all]@  & 1-dimensional, want subscript for fine \\
    173     @a[2][all][3]@  & 0-dimensional; lock fine = 3
     219@a@  & 2-dimensional, want subscripts for coarse then fine \\
     220@a[2]@  & 1-dimensional, want subscript for fine; lock coarse = 2 \\
     221@a[2][all]@  & 1-dimensional, want subscript for fine \\
     222@a[2][all][3]@  & 0-dimensional; lock fine = 3
    174223\end{tabular}
    175224
    … …  
    177226
    178227\begin{tabular}{ll}
    179     @a@  & 2-dimensional, want subscripts for coarse then fine \\
    180     @a[all]@  & 2-dimensional, want subscripts for fine then coarse \\
    181     @a[all][3]@  & 1-dimensional, want subscript for coarse; lock fine = 3 \\
    182     @a[all][3][2]@  & 0-dimensional; lock coarse = 2
     228@a@  & 2-dimensional, want subscripts for coarse then fine \\
     229@a[all]@  & 2-dimensional, want subscripts for fine then coarse \\
     230@a[all][3]@  & 1-dimensional, want subscript for coarse; lock fine = 3 \\
     231@a[all][3][2]@  & 0-dimensional; lock coarse = 2
    183232\end{tabular}
    184233
    185 The semantics of @-[all]@ is to dequeue from the front of the ``want subscripts'' list and re-enqueue at its back.  The semantics of @-[i]@ is to dequeue from the front of the ``want subscripts'' list and lock its value to be @i@.
    186 
    187 Contiguous arrays, and slices of them, are all realized by the same underlying parameterized type.  It includes stride information in its metatdata.  The @-[all]@ operation is a conversion from a reference to one instantiation, to a reference to another instantiation.  The running example's @all@-effective step, stated more concretely, is:
     234The semantics of @-[all]@ is to dequeue from the front of the ``want subscripts'' list and re-enqueue at its back.
     235The semantics of @-[i]@ is to dequeue from the front of the ``want subscripts'' list and lock its value to be @i@.
     236
     237Contiguous arrays, and slices of them, are all realized by the same underlying parameterized type.
     238It includes stride information in its metatdata.
     239The @-[all]@ operation is a conversion from a reference to one instantiation, to a reference to another instantiation.
     240The running example's @all@-effective step, stated more concretely, is:
    188241
    189242\begin{tabular}{ll}
    190     @a@       & : 5 of ( 7 of float each spaced 1 float apart ) each spaced 7 floats apart \\
    191     @a[all]@  & : 7 of ( 5 of float each spaced 7 floats apart ) each spaced 1 float apart
     243@a@       & : 5 of ( 7 of float each spaced 1 float apart ) each spaced 7 floats apart \\
     244@a[all]@  & : 7 of ( 5 of float each spaced 7 floats apart ) each spaced 1 float apart
    192245\end{tabular}
    193246
    194247\begin{figure}
    195     \includegraphics{measuring-like-layout}
    196     \caption{Visualization of subscripting by value and by \lstinline[language=CFA,basicstyle=\ttfamily]{all}, for \lstinline[language=CFA,basicstyle=\ttfamily]{a} of type \lstinline[language=CFA,basicstyle=\ttfamily]{array( float, 5, 7 )}. The horizontal dimension represents memory addresses while vertical layout is conceptual.}
    197     \label{fig:subscr-all}
     248\includegraphics{measuring-like-layout}
     249\caption{Visualization of subscripting by value and by \lstinline[language=CFA,basicstyle=\ttfamily]{all}, for \lstinline[language=CFA,basicstyle=\ttfamily]{a} of type \lstinline[language=CFA,basicstyle=\ttfamily]{array( float, 5, 7 )}.
     250The horizontal dimension represents memory addresses while vertical layout is conceptual.}
     251\label{fig:subscr-all}
    198252\end{figure}
    199253
    200 \noindent While the latter description implies overlapping elements, Figure \ref{fig:subscr-all} shows that the overlaps only occur with unused spaces between elements.  Its depictions of @a[all][...]@ show the navigation of a memory layout with nontrivial strides, that is, with ``spaced \_ floats apart'' values that are greater or smaller than the true count of valid indices times the size of a logically indexed element.  Reading from the bottom up, the expression @a[all][3][2]@ shows a float, that is masquerading as a @float[7]@, for the purpose of being arranged among its peers; five such occurrences form @a[all][3]@.  The tail of flatter boxes extending to the right of a proper element represents this stretching.  At the next level of containment, the structure @a[all][3]@ masquerades as a @float[1]@, for the purpose of being arranged among its peers; seven such occurrences form @a[all]@.  The vertical staircase arrangement represents this compression, and resulting overlapping.
    201 
    202 The new-array library defines types and operations that ensure proper elements are accessed soundly in spite of the overlapping.  The private @arpk@ structure (array with explicit packing) is generic over these two types (and more): the contained element, what it is masquerading as.  This structure's public interface is the @array(...)@ construction macro and the two subscript operators.  Construction by @array@ initializes the masquerading-as type information to be equal to the contained-element information.  Subscripting by @all@ rearranges the order of masquerading-as types to achieve, in general, nontrivial striding.  Subscripting by a number consumes the masquerading-as size of the contained element type, does normal array stepping according to that size, and returns there element found there, in unmasked form.
     254\noindent While the latter description implies overlapping elements, Figure \ref{fig:subscr-all} shows that the overlaps only occur with unused spaces between elements.
     255Its depictions of @a[all][...]@ show the navigation of a memory layout with nontrivial strides, that is, with ``spaced \_ floats apart'' values that are greater or smaller than the true count of valid indices times the size of a logically indexed element.
     256Reading from the bottom up, the expression @a[all][3][2]@ shows a float, that is masquerading as a @float[7]@, for the purpose of being arranged among its peers; five such occurrences form @a[all][3]@.
     257The tail of flatter boxes extending to the right of a proper element represents this stretching.
     258At the next level of containment, the structure @a[all][3]@ masquerades as a @float[1]@, for the purpose of being arranged among its peers; seven such occurrences form @a[all]@.
     259The vertical staircase arrangement represents this compression, and resulting overlapping.
     260
     261The new-array library defines types and operations that ensure proper elements are accessed soundly in spite of the overlapping.
     262The private @arpk@ structure (array with explicit packing) is generic over these two types (and more): the contained element, what it is masquerading as.
     263This structure's public interface is the @array(...)@ construction macro and the two subscript operators.
     264Construction by @array@ initializes the masquerading-as type information to be equal to the contained-element information.
     265Subscripting by @all@ rearranges the order of masquerading-as types to achieve, in general, nontrivial striding.
     266Subscripting by a number consumes the masquerading-as size of the contained element type, does normal array stepping according to that size, and returns there element found there, in unmasked form.
    203267
    204268The @arpk@ structure and its @-[i]@ operator are thus defined as:
    205269\begin{lstlisting}
    206270forall( ztype(N),               // length of current dimension
    207         dtype(S) | sized(S),    // masquerading-as
    208         dtype E_im,             // immediate element, often another array
    209         dtype E_base            // base element, e.g. float, never array
    210       ) {
    211     struct arpk {
    212         S strides[N];           // so that sizeof(this) is N of S
    213     };
    214 
    215     // expose E_im, stride by S
    216     E_im & ?[?]( arpk(N, S, E_im, E_base) & a, ptrdiff_t i ) {
    217         return (E_im &) a.strides[i];
    218     }
    219 }
    220 \end{lstlisting}
    221 
    222 An instantiation of the @arpk@ generic is given by the @array(E_base, N0, N1, ...)@ expansion, which is @arpk( N0, Rec, Rec, E_base )@, where @Rec@ is @array(E_base, N1, ...)@.  In the base case, @array(E_base)@ is just @E_base@.  Because this construction uses the same value for the generic parameters @S@ and @E_im@, the resulting layout has trivial strides.
    223 
    224 Subscripting by @all@, to operate on nontrivial strides, is a dequeue-enqueue operation on the @E_im@ chain, which carries @S@ instantiations, intact, to new positions.  Expressed as an operation on types, this rotation is:
     271        dtype(S) | sized(S),    // masquerading-as
     272        dtype E_im,             // immediate element, often another array
     273        dtype E_base            // base element, e.g. float, never array
     274 ) {
     275struct arpk {
     276        S strides[N];           // so that sizeof(this) is N of S
     277};
     278
     279// expose E_im, stride by S
     280E_im & ?[?]( arpk(N, S, E_im, E_base) & a, ptrdiff_t i ) {
     281        return (E_im &) a.strides[i];
     282}
     283}
     284\end{lstlisting}
     285
     286An instantiation of the @arpk@ generic is given by the @array(E_base, N0, N1, ...)@ expansion, which is @arpk( N0, Rec, Rec, E_base )@, where @Rec@ is @array(E_base, N1, ...)@.
     287In the base case, @array(E_base)@ is just @E_base@.
     288Because this construction uses the same value for the generic parameters @S@ and @E_im@, the resulting layout has trivial strides.
     289
     290Subscripting by @all@, to operate on nontrivial strides, is a dequeue-enqueue operation on the @E_im@ chain, which carries @S@ instantiations, intact, to new positions.
     291Expressed as an operation on types, this rotation is:
    225292\begin{eqnarray*}
    226293suball( arpk(N, S, E_i, E_b) ) & = & enq( N, S, E_i, E_b ) \\
    … …  
    232299\section{Bound checks, added and removed}
    233300
    234 \CFA array subscripting is protected with runtime bound checks.  Having dependent typing causes the optimizer to remove more of these bound checks than it would without them.  This section provides a demonstration of the effect.
    235 
    236 The experiment compares the \CFA array system with the padded-room system [TODO:xref] most typically exemplified by Java arrays, but also reflected in the C++ pattern where restricted vector usage models a checked array.  The essential feature of this padded-room system is the one-to-one correspondence between array instances and the symbolic bounds on which dynamic checks are based.  The experiment compares with the C++ version to keep access to generated assembly code simple.
    237 
    238 As a control case, a simple loop (with no reused dimension sizes) is seen to get the same optimization treatment in both the \CFA and C++ versions.  When the programmer treats the array's bound correctly (making the subscript ``obviously fine''), no dynamic bound check is observed in the program's optimized assembly code.  But when the bounds are adjusted, such that the subscript is possibly invalid, the bound check appears in the optimized assembly, ready to catch an occurrence the mistake.
     301\CFA array subscripting is protected with runtime bound checks.
     302Having dependent typing causes the optimizer to remove more of these bound checks than it would without them.
     303This section provides a demonstration of the effect.
     304
     305The experiment compares the \CFA array system with the padded-room system [TODO:xref] most typically exemplified by Java arrays, but also reflected in the C++ pattern where restricted vector usage models a checked array.
     306The essential feature of this padded-room system is the one-to-one correspondence between array instances and the symbolic bounds on which dynamic checks are based.
     307The experiment compares with the C++ version to keep access to generated assembly code simple.
     308
     309As a control case, a simple loop (with no reused dimension sizes) is seen to get the same optimization treatment in both the \CFA and C++ versions.
     310When the programmer treats the array's bound correctly (making the subscript ``obviously fine''), no dynamic bound check is observed in the program's optimized assembly code.
     311But when the bounds are adjusted, such that the subscript is possibly invalid, the bound check appears in the optimized assembly, ready to catch an occurrence the mistake.
    239312
    240313TODO: paste source and assembly codes
    241314
    242 Incorporating reuse among dimension sizes is seen to give \CFA an advantage at being optimized.  The case is naive matrix multiplication over a row-major encoding.
     315Incorporating reuse among dimension sizes is seen to give \CFA an advantage at being optimized.
     316The case is naive matrix multiplication over a row-major encoding.
    243317
    244318TODO: paste source codes
    … …  
    250324\section{Comparison with other arrays}
    251325
    252 \CFA's array is the first lightweight application of dependently-typed bound tracking to an extension of C.  Other extensions of C that apply dependently-typed bound tracking are heavyweight, in that the bound tracking is part of a linearly typed ownership system that further helps guarantee statically the validity of every pointer deference.  These systems, therefore, ask the programmer to convince the type checker that every pointer dereference is valid.  \CFA imposes the lighter-weight obligation, with the more limited guarantee, that initially-declared bounds are respected thereafter.
    253 
    254 \CFA's array is also the first extension of C to use its tracked bounds to generate the pointer arithmetic implied by advanced allocation patterns.  Other bound-tracked extensions of C either forbid certain C patterns entirely, or address the problem of \emph{verifying} that the user's provided pointer arithmetic is self-consistent.  The \CFA array, applied to accordion structures [TOD: cross-reference] \emph{implies} the necessary pointer arithmetic, generated automatically, and not appearing at all in a user's program.
     326\CFA's array is the first lightweight application of dependently-typed bound tracking to an extension of C.
     327Other extensions of C that apply dependently-typed bound tracking are heavyweight, in that the bound tracking is part of a linearly typed ownership system that further helps guarantee statically the validity of every pointer deference.
     328These systems, therefore, ask the programmer to convince the type checker that every pointer dereference is valid.
     329\CFA imposes the lighter-weight obligation, with the more limited guarantee, that initially-declared bounds are respected thereafter.
     330
     331\CFA's array is also the first extension of C to use its tracked bounds to generate the pointer arithmetic implied by advanced allocation patterns.
     332Other bound-tracked extensions of C either forbid certain C patterns entirely, or address the problem of \emph{verifying} that the user's provided pointer arithmetic is self-consistent.
     333The \CFA array, applied to accordion structures [TOD: cross-reference] \emph{implies} the necessary pointer arithmetic, generated automatically, and not appearing at all in a user's program.
    255334
    256335\subsection{Safety in a padded room}
    257336
    258 Java's array [TODO:cite] is a straightforward example of assuring safety against undefined behaviour, at a cost of expressiveness for more applied properties.  Consider the array parameter declarations in:
     337Java's array [TODO:cite] is a straightforward example of assuring safety against undefined behaviour, at a cost of expressiveness for more applied properties.
     338Consider the array parameter declarations in:
    259339
    260340\begin{tabular}{rl}
    261     C      &  @void f( size_t n, size_t m, float a[n][m] );@ \\
    262     Java   &  @void f( float[][] a );@
     341C      &  @void f( size_t n, size_t m, float a[n][m] );@ \\
     342Java   &  @void f( float[][] a );@
    263343\end{tabular}
    264344
    265 Java's safety against undefined behaviour assures the callee that, if @a@ is non-null, then @a.length@ is a valid access (say, evaluating to the number $\ell$) and if @i@ is in $[0, \ell)$ then @a[i]@ is a valid access.  If a value of @i@ outside this range is used, a runtime error is guaranteed.  In these respects, C offers no guarantees at all.  Notably, the suggestion that @n@ is the intended size of the first dimension of @a@ is documentation only.  Indeed, many might prefer the technically equivalent declarations @float a[][m]@ or @float (*a)[m]@ as emphasizing the ``no guarantees'' nature of an infrequently used language feature, over using the opportunity to explain a programmer intention.  Moreover, even if @a[0][0]@ is valid for the purpose intended, C's basic infamous feature is the possibility of an @i@, such that @a[i][0]@ is not valid for the same purpose, and yet, its evaluation does not produce an error.
     345Java's safety against undefined behaviour assures the callee that, if @a@ is non-null, then @a.length@ is a valid access (say, evaluating to the number $\ell$) and if @i@ is in $[0, \ell)$ then @a[i]@ is a valid access.
     346If a value of @i@ outside this range is used, a runtime error is guaranteed.
     347In these respects, C offers no guarantees at all.
     348Notably, the suggestion that @n@ is the intended size of the first dimension of @a@ is documentation only.
     349Indeed, many might prefer the technically equivalent declarations @float a[][m]@ or @float (*a)[m]@ as emphasizing the ``no guarantees'' nature of an infrequently used language feature, over using the opportunity to explain a programmer intention.
     350Moreover, even if @a[0][0]@ is valid for the purpose intended, C's basic infamous feature is the possibility of an @i@, such that @a[i][0]@ is not valid for the same purpose, and yet, its evaluation does not produce an error.
    266351
    267352Java's lack of expressiveness for more applied properties means these outcomes are possible:
    268353\begin{itemize}
    269     \item @a[0][17]@ and @a[2][17]@ are valid accesses, yet @a[1][17]@ is a runtime error, because @a[1]@ is a null pointer
    270     \item the same observation, now because @a[1]@ refers to an array of length 5
    271     \item execution times vary, because the @float@ values within @a@ are sometimes stored nearly contiguously, and other times, not at all
     354\item @a[0][17]@ and @a[2][17]@ are valid accesses, yet @a[1][17]@ is a runtime error, because @a[1]@ is a null pointer
     355\item the same observation, now because @a[1]@ refers to an array of length 5
     356\item execution times vary, because the @float@ values within @a@ are sometimes stored nearly contiguously, and other times, not at all
    272357\end{itemize}
    273358C's array has none of these limitations, nor do any of the ``array language'' comparators discussed in this section.
    274359
    275 This Java level of safety and expressiveness is also exemplified in the C family, with the commonly given advice [TODO:cite example], for C++ programmers to use @std::vector@ in place of the C++ language's array, which is essentially the C array.  The advice is that, while a vector is also more powerful (and quirky) than an array, its capabilities include options to preallocate with an upfront size, to use an available bound-checked accessor (@a.at(i)@ in place of @a[i]@), to avoid using @push_back@, and to use a vector of vectors.  Used with these restrictions, out-of-bound accesses are stopped, and in-bound accesses never exercise the vector's ability to grow, which is to say, they never make the program slow to reallocate and copy, and they never invalidate the program's other references to the contained values.  Allowing this scheme the same referential integrity assumption that \CFA enjoys [TODO:xref], this scheme matches Java's safety and expressiveness exactly.  [TODO: decide about going deeper; some of the Java expressiveness concerns have mitigations, up to even more tradeoffs.]
     360This Java level of safety and expressiveness is also exemplified in the C family, with the commonly given advice [TODO:cite example], for C++ programmers to use @std::vector@ in place of the C++ language's array, which is essentially the C array.
     361The advice is that, while a vector is also more powerful (and quirky) than an array, its capabilities include options to preallocate with an upfront size, to use an available bound-checked accessor (@a.at(i)@ in place of @a[i]@), to avoid using @push_back@, and to use a vector of vectors.
     362Used with these restrictions, out-of-bound accesses are stopped, and in-bound accesses never exercise the vector's ability to grow, which is to say, they never make the program slow to reallocate and copy, and they never invalidate the program's other references to the contained values.
     363Allowing this scheme the same referential integrity assumption that \CFA enjoys [TODO:xref], this scheme matches Java's safety and expressiveness exactly.
     364[TODO: decide about going deeper; some of the Java expressiveness concerns have mitigations, up to even more tradeoffs.]
    276365
    277366\subsection{Levels of dependently typed arrays}
    … …  
    279368The \CFA array and the field of ``array language'' comparators all leverage dependent types to improve on the expressiveness over C and Java, accommodating examples such as:
    280369\begin{itemize}
    281     \item a \emph{zip}-style operation that consumes two arrays of equal length
    282     \item a \emph{map}-style operation whose produced length matches the consumed length
    283     \item a formulation of matrix multiplication, where the two operands must agree on a middle dimension, and where the result dimensions match the operands' outer dimensions
     370\item a \emph{zip}-style operation that consumes two arrays of equal length
     371\item a \emph{map}-style operation whose produced length matches the consumed length
     372\item a formulation of matrix multiplication, where the two operands must agree on a middle dimension, and where the result dimensions match the operands' outer dimensions
    284373\end{itemize}
    285 Across this field, this expressiveness is not just an available place to document such assumption, but these requirements are strongly guaranteed by default, with varying levels of statically/dynamically checked and ability to opt out.  Along the way, the \CFA array also closes the safety gap (with respect to bounds) that Java has over C.
    286 
    287 Dependent type systems, considered for the purpose of bound-tracking, can be full-strength or restricted.  In a full-strength dependent type system, a type can encode an arbitrarily complex predicate, with bound-tracking being an easy example.  The tradeoff of this expressiveness is complexity in the checker, even typically, a potential for its nontermination.  In a restricted dependent type system (purposed for bound tracking), the goal is to check helpful properties, while keeping the checker well-behaved; the other restricted checkers surveyed here, including \CFA's, always terminate.  [TODO: clarify how even Idris type checking terminates]
    288 
    289 Idris is a current, general-purpose dependently typed programming language.  Length checking is a common benchmark for full dependent type systems.  Here, the capability being considered is to track lengths that adjust during the execution of a program, such as when an \emph{add} operation produces a collection one element longer than the one on which it started.  [TODO: finish explaining what Data.Vect is and then the essence of the comparison]
     374Across this field, this expressiveness is not just an available place to document such assumption, but these requirements are strongly guaranteed by default, with varying levels of statically/dynamically checked and ability to opt out.
     375Along the way, the \CFA array also closes the safety gap (with respect to bounds) that Java has over C.
     376
     377Dependent type systems, considered for the purpose of bound-tracking, can be full-strength or restricted.
     378In a full-strength dependent type system, a type can encode an arbitrarily complex predicate, with bound-tracking being an easy example.
     379The tradeoff of this expressiveness is complexity in the checker, even typically, a potential for its nontermination.
     380In a restricted dependent type system (purposed for bound tracking), the goal is to check helpful properties, while keeping the checker well-behaved; the other restricted checkers surveyed here, including \CFA's, always terminate.
     381[TODO: clarify how even Idris type checking terminates]
     382
     383Idris is a current, general-purpose dependently typed programming language.
     384Length checking is a common benchmark for full dependent type systems.
     385Here, the capability being considered is to track lengths that adjust during the execution of a program, such as when an \emph{add} operation produces a collection one element longer than the one on which it started.
     386[TODO: finish explaining what Data.Vect is and then the essence of the comparison]
    290387
    291388POINTS:
    … …  
    293390it can also do these other cool checks, but watch how I can mess with its conservativeness and termination
    294391
    295 Two current, state-of-the-art array languages, Dex\cite{arr:dex:long} and Futhark\cite{arr:futhark:tytheory}, offer offer novel contributions concerning similar, restricted dependent types for tracking array length.  Unlike \CFA, both are garbage-collected functional languages.  Because they are garbage-collected, referential integrity is built-in, meaning that the heavyweight analysis, that \CFA aims to avoid, is unnecessary.  So, like \CFA, the checking in question is a lightweight bounds-only analysis.  Like \CFA, their checks that are conservatively limited by forbidding arithmetic in the depended-upon expression.
    296 
    297 
    298 
    299 The Futhark work discusses the working language's connection to a lambda calculus, with typing rules and a safety theorem proven in reference to an operational semantics.  There is a particular emphasis on an existential type, enabling callee-determined return shapes. 
     392Two current, state-of-the-art array languages, Dex\cite{arr:dex:long} and Futhark\cite{arr:futhark:tytheory}, offer offer novel contributions concerning similar, restricted dependent types for tracking array length.
     393Unlike \CFA, both are garbage-collected functional languages.
     394Because they are garbage-collected, referential integrity is built-in, meaning that the heavyweight analysis, that \CFA aims to avoid, is unnecessary.
     395So, like \CFA, the checking in question is a lightweight bounds-only analysis.
     396Like \CFA, their checks that are conservatively limited by forbidding arithmetic in the depended-upon expression.
     397
     398
     399
     400The Futhark work discusses the working language's connection to a lambda calculus, with typing rules and a safety theorem proven in reference to an operational semantics.
     401There is a particular emphasis on an existential type, enabling callee-determined return shapes.
     402
    300403
    301404Dex uses a novel conception of size, embedding its quantitative information completely into an ordinary type.
    302405
    303 Futhark and full-strength dependently typed languages treat array sizes are ordinary values.  Futhark restricts these expressions syntactically to variables and constants, while a full-strength dependent system does not.
    304 
    305 CFA's hybrid presentation, @forall( [N] )@, has @N@ belonging to the type system, yet has no instances.  Belonging to the type system means it is inferred at a call site and communicated implicitly, like in Dex and unlike in Futhark.  Having no instances means there is no type for a variable @i@ that constrains @i@ to be in the range for @N@, unlike Dex, [TODO: verify], but like Futhark.
     406Futhark and full-strength dependently typed languages treat array sizes are ordinary values.
     407Futhark restricts these expressions syntactically to variables and constants, while a full-strength dependent system does not.
     408
     409CFA's hybrid presentation, @forall( [N] )@, has @N@ belonging to the type system, yet has no instances.
     410Belonging to the type system means it is inferred at a call site and communicated implicitly, like in Dex and unlike in Futhark.
     411Having no instances means there is no type for a variable @i@ that constrains @i@ to be in the range for @N@, unlike Dex, [TODO: verify], but like Futhark.
    306412
    307413\subsection{Static safety in C extensions}
    … …  
    318424\subsection{With described enumerations}
    319425
    320 A project in \CFA's current portfolio will improve enumerations.  In the incumbent state, \CFA has C's enumerations, unmodified.  I will not discuss the core of this project, which has a tall mission already, to improve type safety, maintain appropriate C compatibility and offer more flexibility about storage use.  It also has a candidate stretch goal, to adapt \CFA's @forall@ generic system to communicate generalized enumerations:
    321 \begin{lstlisting}
    322     forall( T | is_enum(T) )
    323     void show_in_context( T val ) {
    324         for( T i ) {
    325             string decorator = "";
    326             if ( i == val-1 ) decorator = "< ready";
    327             if ( i == val   ) decorator = "< go"   ;
    328             sout | i | decorator;
    329         }
    330     }
    331     enum weekday { mon, tue, wed = 500, thu, fri };
    332     show_in_context( wed );
     426A project in \CFA's current portfolio will improve enumerations.
     427In the incumbent state, \CFA has C's enumerations, unmodified.
     428I will not discuss the core of this project, which has a tall mission already, to improve type safety, maintain appropriate C compatibility and offer more flexibility about storage use.
     429It also has a candidate stretch goal, to adapt \CFA's @forall@ generic system to communicate generalized enumerations:
     430\begin{lstlisting}
     431forall( T | is_enum(T) )
     432void show_in_context( T val ) {
     433        for( T i ) {
     434                string decorator = "";
     435                if ( i == val-1 ) decorator = "< ready";
     436                if ( i == val   ) decorator = "< go"   ;
     437                sout | i | decorator;
     438        }
     439}
     440enum weekday { mon, tue, wed = 500, thu, fri };
     441show_in_context( wed );
    333442\end{lstlisting}
    334443with output
    335444\begin{lstlisting}
    336     mon
    337     tue < ready
    338     wed < go
    339     thu
    340     fri
    341 \end{lstlisting}
    342 The details in this presentation aren't meant to be taken too precisely as suggestions for how it should look in \CFA.  But the example shows these abilities:
     445mon
     446tue < ready
     447wed < go
     448thu
     449fri
     450\end{lstlisting}
     451The details in this presentation aren't meant to be taken too precisely as suggestions for how it should look in \CFA.
     452But the example shows these abilities:
    343453\begin{itemize}
    344     \item a built-in way (the @is_enum@ trait) for a generic routine to require enumeration-like information about its instantiating type
    345     \item an implicit implementation of the trait whenever a user-written enum occurs (@weekday@'s declaration implies @is_enum@)
    346     \item a total order over the enumeration constants, with predecessor/successor (@val-1@) available, and valid across gaps in values (@tue == 1 && wed == 500 && tue == wed - 1@)
    347     \item a provision for looping (the @for@ form used) over the values of the type.
     454\item a built-in way (the @is_enum@ trait) for a generic routine to require enumeration-like information about its instantiating type
     455\item an implicit implementation of the trait whenever a user-written enum occurs (@weekday@'s declaration implies @is_enum@)
     456\item a total order over the enumeration constants, with predecessor/successor (@val-1@) available, and valid across gaps in values (@tue == 1 && wed == 500 && tue == wed - 1@)
     457\item a provision for looping (the @for@ form used) over the values of the type.
    348458\end{itemize}
    349459
    … …  
    352462[TODO: introduce Ada in the comparators]
    353463
    354 In Ada and Dex, an array is conceived as a function whose domain must satisfy only certain structural assumptions, while in C, C++, Java, Futhark and \CFA today, the domain is a prefix of the natural numbers.  The generality has obvious aesthetic benefits for programmers working on scheduling resources to weekdays, and for programmers who prefer to count from an initial number of their own choosing.
    355 
    356 This change of perspective also lets us remove ubiquitous dynamic bound checks.  [TODO: xref] discusses how automatically inserted bound checks can often be optimized away.  But this approach is unsatisfying to a programmer who believes she has written code in which dynamic checks are unnecessary, but now seeks confirmation.  To remove the ubiquitous dynamic checking is to say that an ordinary subscript operation is only valid when it can be statically verified to be in-bound (and so the ordinary subscript is not dynamically checked), and an explicit dynamic check is available when the static criterion is impractical to meet.
     464In Ada and Dex, an array is conceived as a function whose domain must satisfy only certain structural assumptions, while in C, C++, Java, Futhark and \CFA today, the domain is a prefix of the natural numbers.
     465The generality has obvious aesthetic benefits for programmers working on scheduling resources to weekdays, and for programmers who prefer to count from an initial number of their own choosing.
     466
     467This change of perspective also lets us remove ubiquitous dynamic bound checks.
     468[TODO: xref] discusses how automatically inserted bound checks can often be optimized away.
     469But this approach is unsatisfying to a programmer who believes she has written code in which dynamic checks are unnecessary, but now seeks confirmation.
     470To remove the ubiquitous dynamic checking is to say that an ordinary subscript operation is only valid when it can be statically verified to be in-bound (and so the ordinary subscript is not dynamically checked), and an explicit dynamic check is available when the static criterion is impractical to meet.
    357471
    358472[TODO, fix confusion:  Idris has this arrangement of checks, but still the natural numbers as the domain.]
    359473
    360 The structural assumptions required for the domain of an array in Dex are given by the trait (there, ``interface'') @Ix@, which says that the parameter @n@ is a type (which could take an argument like @weekday@) that provides two-way conversion with the integers and a report on the number of values.  Dex's @Ix@ is analogous the @is_enum@ proposed for \CFA above.
     474The structural assumptions required for the domain of an array in Dex are given by the trait (there, ``interface'') @Ix@, which says that the parameter @n@ is a type (which could take an argument like @weekday@) that provides two-way conversion with the integers and a report on the number of values.
     475Dex's @Ix@ is analogous the @is_enum@ proposed for \CFA above.
    361476\begin{lstlisting}
    362477interface Ix n
    363   get_size n : Unit -> Int
    364   ordinal : n -> Int
    365   unsafe_from_ordinal n : Int -> n
    366 \end{lstlisting}
    367 
    368 Dex uses this foundation of a trait (as an array type's domain) to achieve polymorphism over shapes.  This flavour of polymorphism lets a function be generic over how many (and the order of) dimensions a caller uses when interacting with arrays communicated with this function.  Dex's example is a routine that calculates pointwise differences between two samples.  Done with shape polymorphism, one function body is equally applicable to a pair of single-dimensional audio clips (giving a single-dimensional result) and a pair of two-dimensional photographs (giving a two-dimensional result).  In both cases, but with respectively dimensioned interpretations of ``size,'' this function requires the argument sizes to match, and it produces a result of the that size.
    369 
    370 The polymorphism plays out with the pointwise-difference routine advertising a single-dimensional interface whose domain type is generic.  In the audio instantiation, the duration-of-clip type argument is used for the domain.  In the photograph instantiation, it's the tuple-type of $ \langle \mathrm{img\_wd}, \mathrm{img\_ht} \rangle $.  This use of a tuple-as-index is made possible by the built-in rule for implementing @Ix@ on a pair, given @Ix@ implementations for its elements
     478 get_size n : Unit -> Int
     479 ordinal : n -> Int
     480 unsafe_from_ordinal n : Int -> n
     481\end{lstlisting}
     482
     483Dex uses this foundation of a trait (as an array type's domain) to achieve polymorphism over shapes.
     484This flavour of polymorphism lets a function be generic over how many (and the order of) dimensions a caller uses when interacting with arrays communicated with this function.
     485Dex's example is a routine that calculates pointwise differences between two samples.
     486Done with shape polymorphism, one function body is equally applicable to a pair of single-dimensional audio clips (giving a single-dimensional result) and a pair of two-dimensional photographs (giving a two-dimensional result).
     487In both cases, but with respectively dimensioned interpretations of ``size,'' this function requires the argument sizes to match, and it produces a result of the that size.
     488
     489The polymorphism plays out with the pointwise-difference routine advertising a single-dimensional interface whose domain type is generic.
     490In the audio instantiation, the duration-of-clip type argument is used for the domain.
     491In the photograph instantiation, it's the tuple-type of $ \langle \mathrm{img\_wd}, \mathrm{img\_ht} \rangle $.
     492This use of a tuple-as-index is made possible by the built-in rule for implementing @Ix@ on a pair, given @Ix@ implementations for its elements
    371493\begin{lstlisting}
    372494instance {a b} [Ix a, Ix b] Ix (a & b)
    373   get_size = \(). size a * size b
    374   ordinal = \(i, j). (ordinal i * size b) + ordinal j
    375   unsafe_from_ordinal = \o.
    376     bs = size b
    377     (unsafe_from_ordinal a (idiv o bs), unsafe_from_ordinal b (rem o bs))
     495 get_size = \(). size a * size b
     496 ordinal = \(i, j). (ordinal i * size b) + ordinal j
     497 unsafe_from_ordinal = \o.
     498bs = size b
     499(unsafe_from_ordinal a (idiv o bs), unsafe_from_ordinal b (rem o bs))
    378500\end{lstlisting}
    379501and by a user-provided adapter expression at the call site that shows how to indexing with a tuple is backed by indexing each dimension at a time
    380502\begin{lstlisting}
    381     img_trans :: (img_wd,img_ht)=>Real
    382     img_trans.(i,j) = img.i.j
    383     result = pairwise img_trans
     503img_trans :: (img_wd,img_ht)=>Real
     504img_trans.(i,j) = img.i.j
     505result = pairwise img_trans
    384506\end{lstlisting}
    385507[TODO: cite as simplification of example from https://openreview.net/pdf?id=rJxd7vsWPS section 4]

  • doc/theses/mike_brooks_MMath/background.tex

    r03606ce r266732e  
    2121This behaviour is typically one of
    2222\begin{itemize}
    23     \item my statement that the compiler accepts or rejects the program
    24     \item the program's printed output, which I show
    25     \item my implied assurance that its assertions do not fail when run
     23        \item my statement that the compiler accepts or rejects the program
     24        \item the program's printed output, which I show
     25        \item my implied assurance that its assertions do not fail when run
    2626\end{itemize}
    2727
    2828The compiler whose program semantics is shown is
    29 \begin{lstlisting}
     29\begin{cfa}
    3030$ gcc --version
    3131gcc (Ubuntu 9.4.0-1ubuntu1~20.04.1) 9.4.0
    32 \end{lstlisting}
     32\end{cfa}
    3333running on Architecture @x86_64@, with the same environment targeted.
    3434
    … …  
    3939\subsection{C reports many ill-typed expressions as warnings}
    4040
    41 TODO: typeset
    42 \lstinputlisting[language=C, firstline=13, lastline=56]{bkgd-c-tyerr.c}
     41These attempts to assign @y@ to @x@ and vice-versa are obviously ill-typed.
     42\lstinput{12-15}{bkgd-c-tyerr.c}
     43with warnings:
     44\begin{cfa}
     45warning: assignment to 'float *' from incompatible pointer type 'void (*)(void)'
     46warning: assignment to 'void (*)(void)' from incompatible pointer type 'float *'
     47\end{cfa}
     48Similarly,
     49\lstinput{17-19}{bkgd-c-tyerr.c}
     50with warning:
     51\begin{cfa}
     52warning: passing argument 1 of 'f' from incompatible pointer type
     53note: expected 'void (*)(void)' but argument is of type 'float *'
     54\end{cfa}
     55with a segmentation fault at runtime.
     56
     57That @f@'s attempt to call @g@ fails is not due to 3.14 being a particularly unlucky choice of value to put in the variable @pi@.
     58Rather, it is because obtaining a program that includes this essential fragment, yet exhibits a behaviour other than "doomed to crash," is a matter for an obfuscated coding competition.
     59
     60A "tractable syntactic method for proving the absence of certain program behaviours by classifying phrases according to the kinds of values they compute"*1 rejected the program.
     61The behaviour (whose absence is unprovable) is neither minor nor unlikely.
     62The rejection shows that the program is ill-typed.
     63
     64Yet, the rejection presents as a GCC warning.
     65
     66In the discussion following, ``ill-typed'' means giving a nonzero @gcc -Werror@ exit condition with a message that discusses typing.
     67
     68*1  TAPL-pg1 definition of a type system
    4369
    4470
    … …  
    4773\subsection{C has an array type (!)}
    4874
    49 TODO: typeset
    50 \lstinputlisting[language=C, firstline=35, lastline=116]{bkgd-carray-arrty.c}
     75When a programmer works with an array, C semantics provide access to a type that is different in every way from ``pointer to its first element.''
     76Its qualities become apparent by inspecting the declaration
     77\lstinput{34-34}{bkgd-carray-arrty.c}
     78The inspection begins by using @sizeof@ to provide definite program semantics for the intuition of an expression's type.
     79Assuming a target platform keeps things concrete:
     80\lstinput{35-36}{bkgd-carray-arrty.c}
     81Consider the sizes of expressions derived from @a@, modified by adding ``pointer to'' and ``first element'' (and including unnecessary parentheses to avoid confusion about precedence).
     82\lstinput{37-40}{bkgd-carray-arrty.c}
     83That @a@ takes up 40 bytes is common reasoning for C programmers.
     84Set aside for a moment the claim that this first assertion is giving information about a type.
     85For now, note that an array and a pointer to its first element are, sometimes, different things.
     86
     87The idea that there is such a thing as a pointer to an array may be surprising.
     88It is not the same thing as a pointer to the first element:
     89\lstinput{42-45}{bkgd-carray-arrty.c}
     90The first gets
     91\begin{cfa}
     92warning: assignment to `float (*)[10]' from incompatible pointer type `float *'
     93\end{cfa}
     94and the second gets the opposite.
     95
     96We now refute a concern that @sizeof(a)@ is reporting on special knowledge from @a@ being an local variable,
     97say that it is informing about an allocation, rather than simply a type.
     98
     99First, recognizing that @sizeof@ has two forms, one operating on an expression, the other on a type, we observe that the original answers are unaffected by using the type-parameterized form:
     100\lstinput{46-50}{bkgd-carray-arrty.c}
     101Finally, the same sizing is reported when there is no allocation at all, and we launch the analysis instead from the pointer-to-array type.
     102\lstinput{51-57}{bkgd-carray-arrty.c}
     103So, in spite of considerable programmer success enabled by an understanding that an array just a pointer to its first element (revisited TODO pointer decay), this understanding is simplistic.
     104
     105A shortened form for declaring local variables exists, provided that length information is given in the initializer:
     106\lstinput{59-63}{bkgd-carray-arrty.c}
     107In these declarations, the resulting types are both arrays, but their lengths are inferred.
     108
     109\begin{tabular}{lllllll}
     110@float x;@ & $\rightarrow$ & (base element) & @float@ & @float x;@ & @[ float ]@ & @[ float ]@ \\
     111@float * x;@ & $\rightarrow$ & pointer & @float *@ & @float * x;@ & @[ * float ]@ & @[ * float ]@ \\
     112@float x[10];@ & $\rightarrow$ & array & @float[10]@ & @float x[10];@ & @[ [10] float ]@ & @[ array(float, 10) ]@ \\
     113@float *x[10];@ & $\rightarrow$ & array of pointers & @(float*)[10]@ & @float *x[10];@ & @[ [10] * float ]@ & @[ array(*float, 10) ]@ \\
     114@float (*x)[10];@ & $\rightarrow$ & pointer to array & @float(*)[10]@ & @float (*x)[10];@ & @[ * [10] float ]@ & @[ * array(float, 10) ]@ \\
     115@float *(*x5)[10];@ & $\rightarrow$ & pointer to array & @(float*)(*)[10]@ & @float *(*x)[10];@ & @[ * [10] * float ]@ & @[ * array(*float, 10) ]@
     116\end{tabular}
     117\begin{cfa}
     118         x5 =    (float*(*)[10]) x4;
     119//      x5 =     (float(*)[10]) x4;  // wrong target type; meta test suggesting above cast uses correct type
     120
     121        // [here]
     122        // const
     123
     124        // [later]
     125        // static
     126        // star as dimension
     127        // under pointer decay:                         int p1[const 3]  being  int const *p1
     128
     129        const float * y1;
     130        float const * y2;
     131        float * const y3;
     132
     133        y1 = 0;
     134        y2 = 0;
     135        // y3 = 0; // bad
     136
     137        // *y1 = 3.14; // bad
     138        // *y2 = 3.14; // bad
     139        *y3 = 3.14;
     140
     141        const float z1 = 1.414;
     142        float const z2 = 1.414;
     143
     144        // z1 = 3.14; // bad
     145        // z2 = 3.14; // bad
     146
     147
     148}
     149
     150#define T float
     151void stx2() { const T x[10];
     152//                      x[5] = 3.14; // bad
     153                        }
     154void stx3() { T const x[10];
     155//                      x[5] = 3.14; // bad
     156                        }
     157\end{cfa}
    51158
    52159My contribution is enabled by recognizing
    53160\begin{itemize}
    54     \item There is value in using a type that knows how big the whole thing is.
    55     \item The type pointer to (first) element does not.
    56     \item C \emph{has} a type that knows the whole picture: array, e.g. @T[10]@.
    57     \item This type has all the usual derived forms, which also know the whole picture.  A usefully noteworthy example is pointer to array, e.g. @T(*)[10]@.
     161        \item There is value in using a type that knows how big the whole thing is.
     162        \item The type pointer to (first) element does not.
     163        \item C \emph{has} a type that knows the whole picture: array, e.g. @T[10]@.
     164        \item This type has all the usual derived forms, which also know the whole picture.  A usefully noteworthy example is pointer to array, e.g. @T(*)[10]@.
    58165\end{itemize}
    59166
    … …  
    75182a declaration is always the type followed by the declared identifier name;
    76183for the example of letting @x@ be a \emph{pointer to array}, the declaration is spelled:
    77 \begin{lstlisting}
     184\begin{cfa}
    78185[ * [10] T ] x;
    79 \end{lstlisting}
     186\end{cfa}
    80187The \CFA-Full column gives the spelling of a different type, introduced in TODO, which has all of my contributed improvements for safety and ergonomics.
    81188
    … …  
    83190\textbf{Unfortunate Syntactic Reference}
    84191
    85 \noindent
     192\begin{figure}
     193\centering
     194\setlength{\tabcolsep}{3pt}
    86195\begin{tabular}{llllll}
    87     & Description & Type & Declaration & \CFA-C  & \CFA-Full \\ \hline
    88     $\triangleright$ & val.
    89         & @T@
    90         & @T x;@
    91         & @[ T ]@
    92         &
    93         \\ \hline
    94     & \pbox{20cm}{ \vspace{2pt} val.\\ \footnotesize{no writing the val.\ in \lstinline{x}}   }\vspace{2pt}
    95         & \pbox{20cm}{ \vspace{2pt} \lstinline{const T} \\ \lstinline{T const}   }
    96         & \pbox{20cm}{ \vspace{2pt} \lstinline{const T x;} \\ \lstinline{T const x;}   }
    97         & @[ const T ]@
    98         &
    99         \\ \hline
    100     $\triangleright$ & ptr.\ to val.
    101         & @T *@
    102         & @T * x;@
    103         & @[ * T ]@
    104         &
    105         \\ \hline
    106     & \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x}}   }\vspace{2pt}
    107         & @T * const@
    108         & @T * const x;@
    109         & @[ const * T ]@
    110         &
    111         \\ \hline
    112     & \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{*x}}   }\vspace{2pt}
    113         & \pbox{20cm}{ \vspace{2pt} \lstinline{const T *} \\ \lstinline{T const *}   }
    114         & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * x;} \\ \lstinline{T const * x;}   }
    115         & @[ * const T ]@
    116         &
    117         \\ \hline
    118     $\triangleright$ & ar.\ of val.
    119         & @T[10]@
    120         & @T x[10];@
    121         & @[ [10] T ]@
    122         & @[ array(T, 10) ]@
    123         \\ \hline
    124     & \pbox{20cm}{ \vspace{2pt} ar.\ of val.\\ \footnotesize{no writing the val.\ in \lstinline{x[5]}}   }\vspace{2pt}
    125         & \pbox{20cm}{ \vspace{2pt} \lstinline{const T[10]} \\ \lstinline{T const[10]}   }
    126         & \pbox{20cm}{ \vspace{2pt} \lstinline{const T x[10];} \\ \lstinline{T const x[10];}   }
    127         & @[ [10] const T ]@
    128         & @[ const array(T, 10) ]@
    129         \\ \hline
    130     & ar.\ of ptr.\ to val.
    131         & @T*[10]@
    132         & @T *x[10];@
    133         & @[ [10] * T ]@
    134         & @[ array(* T, 10) ]@
    135         \\ \hline
    136     & \pbox{20cm}{ \vspace{2pt} ar.\ of ptr.\ to val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x[5]}}   }\vspace{2pt}
    137         & @T * const [10]@
    138         & @T * const x[10];@
    139         & @[ [10] const * T ]@
    140         & @[ array(const * T, 10) ]@
    141         \\ \hline
    142     & \pbox{20cm}{ \vspace{2pt} ar.\ of ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{*(x[5])}}   }\vspace{2pt}
    143         & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * [10]} \\ \lstinline{T const * [10]}   }
    144         & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * x[10];} \\ \lstinline{T const * x[10];}   }
    145         & @[ [10] * const T ]@
    146         & @[ array(* const T, 10) ]@
    147         \\ \hline
    148     $\triangleright$ & ptr.\ to ar.\ of val.
    149         & @T(*)[10]@
    150         & @T (*x)[10];@
    151         & @[ * [10] T ]@
    152         & @[ * array(T, 10) ]@
    153         \\ \hline
    154     & \pbox{20cm}{ \vspace{2pt} ptr.\ to ar.\ of val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x}}   }\vspace{2pt}
    155         & @T(* const)[10]@
    156         & @T (* const x)[10];@
    157         & @[ const * [10] T ]@
    158         & @[ const * array(T, 10) ]@
    159         \\ \hline
    160     & \pbox{20cm}{ \vspace{2pt} ptr.\ to ar.\ of val.\\ \footnotesize{no writing the val.\ in \lstinline{(*x)[5]}}   }\vspace{2pt}
    161         & \pbox{20cm}{ \vspace{2pt} \lstinline{const T(*)[10]} \\ \lstinline{T const (*) [10]}   }
    162         & \pbox{20cm}{ \vspace{2pt} \lstinline{const T (*x)[10];} \\ \lstinline{T const (*x)[10];}   }
    163         & @[ * [10] const T ]@
    164         & @[ * const array(T, 10) ]@
    165         \\ \hline
    166     & ptr.\ to ar.\ of ptr.\ to val.
    167         & @T*(*)[10]@
    168         & @T *(*x)[10];@
    169         & @[ * [10] * T ]@
    170         & @[ * array(* T, 10) ]@
    171         \\ \hline
     196        & Description & Type & Declaration & \CFA-C  & \CFA-Full \\ \hline
     197        $\triangleright$ & val.
     198            & @T@
     199            & @T x;@
     200            & @[ T ]@
     201            &
     202            \\ \hline
     203        & \pbox{20cm}{ \vspace{2pt} val.\\ \footnotesize{no writing the val.\ in \lstinline{x}}   }\vspace{2pt}
     204            & \pbox{20cm}{ \vspace{2pt} \lstinline{const T} \\ \lstinline{T const}   }
     205            & \pbox{20cm}{ \vspace{2pt} \lstinline{const T x;} \\ \lstinline{T const x;}   }
     206            & @[ const T ]@
     207            &
     208            \\ \hline \hline
     209        $\triangleright$ & ptr.\ to val.
     210            & @T *@
     211            & @T * x;@
     212            & @[ * T ]@
     213            &
     214            \\ \hline
     215        & \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x}}   }\vspace{2pt}
     216            & @T * const@
     217            & @T * const x;@
     218            & @[ const * T ]@
     219            &
     220            \\ \hline
     221        & \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{*x}}   }\vspace{2pt}
     222            & \pbox{20cm}{ \vspace{2pt} \lstinline{const T *} \\ \lstinline{T const *}   }
     223            & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * x;} \\ \lstinline{T const * x;}   }
     224            & @[ * const T ]@
     225            &
     226            \\ \hline \hline
     227        $\triangleright$ & ar.\ of val.
     228            & @T[10]@
     229            & @T x[10];@
     230            & @[ [10] T ]@
     231            & @[ array(T, 10) ]@
     232            \\ \hline
     233        & \pbox{20cm}{ \vspace{2pt} ar.\ of val.\\ \footnotesize{no writing the val.\ in \lstinline{x[5]}}   }\vspace{2pt}
     234            & \pbox{20cm}{ \vspace{2pt} \lstinline{const T[10]} \\ \lstinline{T const[10]}   }
     235            & \pbox{20cm}{ \vspace{2pt} \lstinline{const T x[10];} \\ \lstinline{T const x[10];}   }
     236            & @[ [10] const T ]@
     237            & @[ const array(T, 10) ]@
     238            \\ \hline
     239        & ar.\ of ptr.\ to val.
     240            & @T*[10]@
     241            & @T *x[10];@
     242            & @[ [10] * T ]@
     243            & @[ array(* T, 10) ]@
     244            \\ \hline
     245        & \pbox{20cm}{ \vspace{2pt} ar.\ of ptr.\ to val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x[5]}}   }\vspace{2pt}
     246            & @T * const [10]@
     247            & @T * const x[10];@
     248            & @[ [10] const * T ]@
     249            & @[ array(const * T, 10) ]@
     250            \\ \hline
     251        & \pbox{20cm}{ \vspace{2pt} ar.\ of ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{*(x[5])}}   }\vspace{2pt}
     252            & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * [10]} \\ \lstinline{T const * [10]}   }
     253            & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * x[10];} \\ \lstinline{T const * x[10];}   }
     254            & @[ [10] * const T ]@
     255            & @[ array(* const T, 10) ]@
     256            \\ \hline \hline
     257        $\triangleright$ & ptr.\ to ar.\ of val.
     258            & @T(*)[10]@
     259            & @T (*x)[10];@
     260            & @[ * [10] T ]@
     261            & @[ * array(T, 10) ]@
     262            \\ \hline
     263        & \pbox{20cm}{ \vspace{2pt} ptr.\ to ar.\ of val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x}}   }\vspace{2pt}
     264            & @T(* const)[10]@
     265            & @T (* const x)[10];@
     266            & @[ const * [10] T ]@
     267            & @[ const * array(T, 10) ]@
     268            \\ \hline
     269        & \pbox{20cm}{ \vspace{2pt} ptr.\ to ar.\ of val.\\ \footnotesize{no writing the val.\ in \lstinline{(*x)[5]}}   }\vspace{2pt}
     270            & \pbox{20cm}{ \vspace{2pt} \lstinline{const T(*)[10]} \\ \lstinline{T const (*) [10]}   }
     271            & \pbox{20cm}{ \vspace{2pt} \lstinline{const T (*x)[10];} \\ \lstinline{T const (*x)[10];}   }
     272            & @[ * [10] const T ]@
     273            & @[ * const array(T, 10) ]@
     274            \\ \hline
     275        & ptr.\ to ar.\ of ptr.\ to val.
     276            & @T*(*)[10]@
     277            & @T *(*x)[10];@
     278            & @[ * [10] * T ]@
     279            & @[ * array(* T, 10) ]@
     280            \\ \hline
    172281\end{tabular}
     282\caption{Figure}
     283\end{figure}
    173284
    174285
    175286\subsection{Arrays decay and pointers diffract}
    176287
    177 TODO: typeset
    178 \lstinputlisting[language=C, firstline=4, lastline=26]{bkgd-carray-decay.c}
    179 
     288The last section established the difference between these four types:
     289\lstinput{3-6}{bkgd-carray-decay.c}
     290But the expression used for obtaining the pointer to the first element is pedantic.
     291The root of all C programmer experience with arrays is the shortcut
     292\lstinput{8-8}{bkgd-carray-decay.c}
     293which reproduces @pa0@, in type and value:
     294\lstinput{9-9}{bkgd-carray-decay.c}
     295The validity of this initialization is unsettling, in the context of the facts established in the last section.
     296Notably, it initializes name @pa0x@ from expression @a@, when they are not of the same type:
     297\lstinput{10-10}{bkgd-carray-decay.c}
    180298
    181299So, C provides an implicit conversion from @float[10]@ to @float*@, as described in ARM-6.3.2.1.3:
    182 
    183300\begin{quote}
    184     Except when it is the operand of the @sizeof@ operator, or the unary @&@ operator, or is a
    185     string literal used to initialize an array
    186     an expression that has type ``array of type'' is
    187     converted to an expression with type ``pointer to type'' that points to the initial element of
    188     the array object
     301Except when it is the operand of the @sizeof@ operator, or the unary @&@ operator, or is a
     302string literal used to initialize an array
     303an expression that has type ``array of type'' is
     304converted to an expression with type ``pointer to type'' that points to the initial element of
     305the array object
    189306\end{quote}
    190307
    … …  
    206323leads to an expectation that the runtime handling is uniform across legal and illegal accesses.
    207324Moreover, consider the common pattern of subscripting on a malloc result:
    208 \begin{lstlisting}
    209     float * fs = malloc( 10 * sizeof(float) );
    210     fs[5] = 3.14;
    211 \end{lstlisting}
     325\begin{cfa}
     326float * fs = malloc( 10 * sizeof(float) );
     327fs[5] = 3.14;
     328\end{cfa}
    212329The @malloc@ behaviour is specified as returning a pointer to ``space for an object whose size is'' as requested (ARM-7.22.3.4.2).
    213330But program says \emph{nothing} more about this pointer value, that might cause its referent to \emph{be} an array, before doing the subscript.
    … …  
    229346the parameter's type becomes a type that I summarize as being the array-decayed type.
    230347The respective handlings of the following two parameter spellings shows that the array-spelled one is really, like the other, a pointer.
    231 \lstinputlisting[language=C, firstline=40, lastline=44]{bkgd-carray-decay.c}
     348\lstinput{12-16}{bkgd-carray-decay.c}
    232349As the @sizeof(x)@ meaning changed, compared with when run on a similarly-spelled local variariable declaration,
    233350GCC also gives this code the warning: ```sizeof' on array function parameter `x' will return size of `float *'.''
    234351
    235352The caller of such a function is left with the reality that a pointer parameter is a pointer, no matter how it's spelled:
    236 \lstinputlisting[language=C, firstline=60, lastline=63]{bkgd-carray-decay.c}
     353\lstinput{18-21}{bkgd-carray-decay.c}
    237354This fragment gives no warnings.
    238355
    … …  
    240357Note the opposite meaning of this spelling now, compared with its use in local variable declarations.
    241358This point of confusion is illustrated in:
    242 \lstinputlisting[language=C, firstline=80, lastline=87]{bkgd-carray-decay.c}
     359\lstinput{23-30}{bkgd-carray-decay.c}
    243360The basic two meanings, with a syntactic difference helping to distinguish,
    244361are illustrated in the declarations of @ca@ vs.\ @cp@,
    … …  
    252369In sumary, when a funciton is written with an array-typed parameter,
    253370\begin{itemize}
    254     \item an appearance of passing an array by value is always an incorrect understanding
    255     \item a dimension value, if any is present, is ignorred
    256     \item pointer decay is forced at the call site and the callee sees the parameter having the decayed type
     371        \item an appearance of passing an array by value is always an incorrect understanding
     372        \item a dimension value, if any is present, is ignorred
     373        \item pointer decay is forced at the call site and the callee sees the parameter having the decayed type
    257374\end{itemize}
    258375
    259376Pointer decay does not affect pointer-to-array types, because these are already pointers, not arrays.
    260377As a result, a function with a pointer-to-array parameter sees the parameter exactly as the caller does:
    261 \lstinputlisting[language=C, firstline=100, lastline=110]{bkgd-carray-decay.c}
    262 
     378\lstinput{32-42}{bkgd-carray-decay.c}
    263379
    264380\noindent
    … …  
    268384(Parameter declaration; ``no writing'' refers to the callee's ability)
    269385
    270 \noindent
     386\begin{figure}
     387\centering
    271388\begin{tabular}{llllll}
    272     & Description & Type & Param. Decl & \CFA-C  \\ \hline
    273     $\triangleright$ & ptr.\ to val.
    274         & @T *@
    275         & \pbox{20cm}{ \vspace{2pt} \lstinline{T * x,} \\ \lstinline{T x[10],} \\ \lstinline{T x[],}   }\vspace{2pt}
    276         & \pbox{20cm}{ \vspace{2pt} \lstinline{[ * T ]} \\ \lstinline{[ [10] T ]} \\ \lstinline{[ [] T  ]}   }
    277         \\ \hline
    278     & \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x}}   }\vspace{2pt}
    279         & @T * const@
    280         & \pbox{20cm}{ \vspace{2pt} \lstinline{T * const x,} \\ \lstinline{T x[const 10],} \\ \lstinline{T x[const],}   }\vspace{2pt}
    281         & \pbox{20cm}{ \vspace{2pt} \lstinline{[ const * T ]} \\ \lstinline{[ [const 10] T ]} \\ \lstinline{[ [const] T  ]}   }
    282         \\ \hline
    283     & \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{*x}}   }\vspace{2pt}
    284         & \pbox{20cm}{ \vspace{2pt} \lstinline{const T *} \\ \lstinline{T const *}   }
    285         & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * x,} \\ \lstinline{T const * x,} \\ \lstinline{const T x[10],} \\ \lstinline{T const x[10],} \\ \lstinline{const T x[],} \\ \lstinline{T const x[],}   }\vspace{2pt}
    286         & \pbox{20cm}{ \vspace{2pt} \lstinline{[* const T]} \\ \lstinline{[ [10] const T ]} \\ \lstinline{[ [] const T  ]}   }
    287         \\ \hline
    288     $\triangleright$ & ptr.\ to ar.\ of val.
    289         & @T(*)[10]@
    290         & \pbox{20cm}{ \vspace{2pt} \lstinline{T (*x)[10],} \\ \lstinline{T x[3][10],} \\ \lstinline{T x[][10],}   }\vspace{2pt}
    291         & \pbox{20cm}{ \vspace{2pt} \lstinline{[* [10] T]} \\ \lstinline{[ [3] [10] T ]} \\ \lstinline{[ [] [10] T  ]}   }
    292         \\ \hline
    293     & ptr.\ to ptr.\ to val.
    294         & @T **@
    295         & \pbox{20cm}{ \vspace{2pt} \lstinline{T ** x,} \\ \lstinline{T *x[10],} \\ \lstinline{T *x[],}   }\vspace{2pt}
    296         & \pbox{20cm}{ \vspace{2pt} \lstinline{[ * * T ]} \\ \lstinline{[ [10] * T ]} \\ \lstinline{[ [] * T  ]}   }
    297         \\ \hline
    298     & \pbox{20cm}{ \vspace{2pt} ptr.\ to ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{**argv}}   }\vspace{2pt}
    299         & @const char **@
    300         & \pbox{20cm}{ \vspace{2pt} \lstinline{const char *argv[],} \\ \footnotesize{(others elided)}   }\vspace{2pt}
    301         & \pbox{20cm}{ \vspace{2pt} \lstinline{[ [] * const char ]} \\ \footnotesize{(others elided)}   }
    302         \\ \hline
     389        & Description & Type & Param. Decl & \CFA-C  \\ \hline
     390        $\triangleright$ & ptr.\ to val.
     391            & @T *@
     392            & \pbox{20cm}{ \vspace{2pt} \lstinline{T * x,} \\ \lstinline{T x[10],} \\ \lstinline{T x[],}   }\vspace{2pt}
     393            & \pbox{20cm}{ \vspace{2pt} \lstinline{[ * T ]} \\ \lstinline{[ [10] T ]} \\ \lstinline{[ [] T  ]}   }
     394            \\ \hline
     395        & \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the ptr.\ in \lstinline{x}}   }\vspace{2pt}
     396            & @T * const@
     397            & \pbox{20cm}{ \vspace{2pt} \lstinline{T * const x,} \\ \lstinline{T x[const 10],} \\ \lstinline{T x[const],}   }\vspace{2pt}
     398            & \pbox{20cm}{ \vspace{2pt} \lstinline{[ const * T ]} \\ \lstinline{[ [const 10] T ]} \\ \lstinline{[ [const] T  ]}   }
     399            \\ \hline
     400        & \pbox{20cm}{ \vspace{2pt} ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{*x}}   }\vspace{2pt}
     401            & \pbox{20cm}{ \vspace{2pt} \lstinline{const T *} \\ \lstinline{T const *}   }
     402            & \pbox{20cm}{ \vspace{2pt} \lstinline{const T * x,} \\ \lstinline{T const * x,} \\ \lstinline{const T x[10],} \\ \lstinline{T const x[10],} \\ \lstinline{const T x[],} \\ \lstinline{T const x[],}   }\vspace{2pt}
     403            & \pbox{20cm}{ \vspace{2pt} \lstinline{[* const T]} \\ \lstinline{[ [10] const T ]} \\ \lstinline{[ [] const T  ]}   }
     404            \\ \hline \hline
     405        $\triangleright$ & ptr.\ to ar.\ of val.
     406            & @T(*)[10]@
     407            & \pbox{20cm}{ \vspace{2pt} \lstinline{T (*x)[10],} \\ \lstinline{T x[3][10],} \\ \lstinline{T x[][10],}   }\vspace{2pt}
     408            & \pbox{20cm}{ \vspace{2pt} \lstinline{[* [10] T]} \\ \lstinline{[ [3] [10] T ]} \\ \lstinline{[ [] [10] T  ]}   }
     409            \\ \hline
     410        & ptr.\ to ptr.\ to val.
     411            & @T **@
     412            & \pbox{20cm}{ \vspace{2pt} \lstinline{T ** x,} \\ \lstinline{T *x[10],} \\ \lstinline{T *x[],}   }\vspace{2pt}
     413            & \pbox{20cm}{ \vspace{2pt} \lstinline{[ * * T ]} \\ \lstinline{[ [10] * T ]} \\ \lstinline{[ [] * T  ]}   }
     414            \\ \hline
     415        & \pbox{20cm}{ \vspace{2pt} ptr.\ to ptr.\ to val.\\ \footnotesize{no writing the val.\ in \lstinline{**argv}}   }\vspace{2pt}
     416            & @const char **@
     417            & \pbox{20cm}{ \vspace{2pt} \lstinline{const char *argv[],} \\ \footnotesize{(others elided)}   }\vspace{2pt}
     418            & \pbox{20cm}{ \vspace{2pt} \lstinline{[ [] * const char ]} \\ \footnotesize{(others elided)}   }
     419            \\ \hline
    303420\end{tabular}
    304 
     421\caption{Figure}
     422\end{figure}
    305423
    306424
    … …  
    309427When the desired number of elements is unknown at compile time,
    310428a variable-length array is a solution:
    311 \begin{lstlisting}
    312     int main( int argc, const char *argv[] ) {
    313 
    314         assert( argc == 2 );
    315         size_t n = atol( argv[1] );
    316         assert( 0 < n && n < 1000 );
    317 
    318         float a[n];
    319         float b[10];
    320 
    321         // ... discussion continues here
    322     }
    323 \end{lstlisting}
    324 This arrangement allocates @n@ elements on the @main@ stack frame for @a@,
    325 just as it puts 10 elements on the @main@ stack frame for @b@.
     429\begin{cfa}
     430int main( int argc, const char *argv[] ) {
     431        assert( argc == 2 );
     432        size_t n = atol( argv[1] );
     433        assert( 0 < n && n < 1000 );
     434
     435        float a[n];
     436        float b[10];
     437
     438        // ... discussion continues here
     439}
     440\end{cfa}
     441This arrangement allocates @n@ elements on the @main@ stack frame for @a@, just as it puts 10 elements on the @main@ stack frame for @b@.
    326442The variable-sized allocation of @a@ is provided by @alloca@.
    327443
    328 In a situation where the array sizes are not known to be small enough
    329 for stack allocation to be sensible,
    330 corresponding heap allocations are achievable as:
    331 \begin{lstlisting}
    332     float *ax1 = malloc( sizeof( float[n] ) );
    333     float *ax2 = malloc( n * sizeof( float ) );
    334     float *bx1 = malloc( sizeof( float[1000000] ) );
    335     float *bx2 = malloc( 1000000 * sizeof( float ) );
    336 \end{lstlisting}
     444In a situation where the array sizes are not known to be small enough for stack allocation to be sensible, corresponding heap allocations are achievable as:
     445\begin{cfa}
     446float *ax1 = malloc( sizeof( float[n] ) );
     447float *ax2 = malloc( n * sizeof( float ) );
     448float *bx1 = malloc( sizeof( float[1000000] ) );
     449float *bx2 = malloc( 1000000 * sizeof( float ) );
     450\end{cfa}
    337451
    338452
    … …  
    353467Just as an array's element type can be @float@, so can it be @float[10]@.
    354468
    355 While any of @float*@, @float[10]@ and @float(*)[10]@ are easy to tell apart from @float@,
    356 telling them apart from each other may need occasional reference back to TODO intro section.
     469While any of @float*@, @float[10]@ and @float(*)[10]@ are easy to tell apart from @float@, telling them apart from each other may need occasional reference back to TODO intro section.
    357470The sentence derived by wrapping each type in @-[3]@ follows.
    358471
    … …  
    360473telling them apart from each other is what it takes to know what ``array of arrays'' really means.
    361474
    362 
    363475Pointer decay affects the outermost array only
    364476
    365 
    366477TODO: unfortunate syntactic reference with these cases:
    367478
    368479\begin{itemize}
    369     \item ar. of ar. of val (be sure about ordering of dimensions when the declaration is dropped)
    370     \item ptr. to ar. of ar. of val
     480        \item ar. of ar. of val (be sure about ordering of dimensions when the declaration is dropped)
     481        \item ptr. to ar. of ar. of val
    371482\end{itemize}
    372483
    373484
    374 
    375 
    376 
    377485\subsection{Arrays are (but) almost values}
    378486
    … …  
    391499
    392500\subsection{Returning an array is (but) almost possible}
    393 
    394 
    395501
    396502
    … …  
    414520which type information associated with a polymorphic return type
    415521replaces @malloc@'s use of programmer-supplied size information.
    416 \begin{lstlisting}
    417     // C, library
    418     void * malloc( size_t );
    419     // C, user
    420     struct tm * el1 = malloc(      sizeof(struct tm) );
    421     struct tm * ar1 = malloc( 10 * sizeof(struct tm) );
    422 
    423     // CFA, library
    424     forall( T * ) T * alloc();
    425     // CFA, user
    426     tm * el2 = alloc();
    427     tm (*ar2)[10] = alloc();
    428 \end{lstlisting}
     522\begin{cfa}
     523// C, library
     524void * malloc( size_t );
     525// C, user
     526struct tm * el1 = malloc(      sizeof(struct tm) );
     527struct tm * ar1 = malloc( 10 * sizeof(struct tm) );
     528
     529// CFA, library
     530forall( T * ) T * alloc();
     531// CFA, user
     532tm * el2 = alloc();
     533tm (*ar2)[10] = alloc();
     534\end{cfa}
    429535The alloc polymorphic return compiles into a hidden parameter, which receives a compiler-generated argument.
    430536This compiler's argument generation uses type information from the left-hand side of the initialization to obtain the intended type.
    … …  
    436542In the last example, the choice of ``pointer to array'' @ar2@ breaks a parallel with @ar1@.
    437543They are not subscripted in the same way.
    438 \begin{lstlisting}
    439     ar1[5];
    440     (*ar2)[5];
    441 \end{lstlisting}
     544\begin{cfa}
     545ar1[5];
     546(*ar2)[5];
     547\end{cfa}
    442548Using ``reference to array'' works at resolving this issue.  TODO: discuss connection with Doug-Lea \CC proposal.
    443 \begin{lstlisting}
    444     tm (&ar3)[10] = *alloc();
    445     ar3[5];
    446 \end{lstlisting}
     549\begin{cfa}
     550tm (&ar3)[10] = *alloc();
     551ar3[5];
     552\end{cfa}
    447553The implicit size communication to @alloc@ still works in the same ways as for @ar2@.
    448554
    … …  
    453559where the type requested is an array, making the result, much more obviously, an array object.
    454560
    455 The ``reference to array'' type has its sore spots too.  TODO see also @dimexpr-match-c/REFPARAM_CALL (under TRY_BUG_1)@
    456 
    457 
     561The ``reference to array'' type has its sore spots too.
     562TODO see also @dimexpr-match-c/REFPARAM_CALL@ (under @TRY_BUG_1@)
    458563
    459564TODO: I fixed a bug associated with using an array as a T.  I think.  Did I really?  What was the bug?

  • doc/theses/mike_brooks_MMath/programs/bkgd-c-tyerr.c

    r03606ce r266732e  
    1010
    1111int main() {
     12        float * x;                      $\C{// x points at a floating-point number}$
     13        void (*y)(void);        $\C{// y points at a function}$
     14        @x = y;@                        $\C{// wrong}$
     15        @y = x;@                        $\C{// wrong}$
    1216
    13 /*
    14     These attempts to assign @y@ to @x@ and vice-versa are obviously ill-typed.
    15 */
    16     float * x;         // x points at a floating-point number
    17     void (*y)(void);   // y points at a function
    18                        ERR(
    19     x = y;             // wrong
    20     y = x;             // wrong
    21                        )
     17        float pi = 3.14;
     18        void f( void (*g)(void) ) { g(); }
     19        @f( &pi );@                     $\C{// wrong}$
     20}
    2221
    23 /*
    24     The first gets
    25         warning: assignment to `float *' from incompatible pointer type `void (*)(void)'
    26     and the second gets the opposite.
    27 
    28     Similarly,
    29 */
    30 
    31     float pi = 3.14;
    32     void f( void (*g)(void) ) {
    33         g();
    34     }
    35                        ERR(
    36     f( & pi );         // wrong
    37                        )
    38 /*
    39     gets
    40         warning: passing argument 1 of `f' from incompatible pointer type
    41     with a segmentation fault at runtime.
    42 
    43     That @f@'s attempt to call @g@ fails is not due to 3.14 being a particularly unlucky choice of value to put in the variable @pi@.
    44     Rather, it is because obtaining a program that includes this essential fragment, yet exhibits a behaviour other than "doomed to crash," is a matter for an obfuscated coding competition.
    45 
    46     A "tractable syntactic method for proving the absence of certain program behaviours
    47     by classifying phrases according to the kinds of values they compute"*1
    48     rejected the program.  The behaviour (whose absence is unprovable) is neither minor nor unlikely.
    49     The rejection shows that the program is ill-typed.
    50 
    51     Yet, the rejection presents as a GCC warning.
    52 
    53     In the discussion following, ``ill-typed'' means giving a nonzero @gcc -Werror@ exit condition with a message that discusses typing.
    54 
    55     *1  TAPL-pg1 definition of a type system
    56 */
    57 
    58 }
     22// Local Variables: //
     23// compile-command: "sed -f sedcmd bkgd-c-tyerr.c > tmp.c; gcc tmp.c" //
     24// End: //

  • doc/theses/mike_brooks_MMath/programs/bkgd-carray-arrty.c

    r03606ce r266732e  
    2424
    2525
    26     // SHOW(sizeof( a   ), "%zd");
    27     // SHOW(sizeof(&a   ), "%zd");
    28     // SHOW(sizeof( a[0]), "%zd");
    29     // SHOW(sizeof(&a[0]), "%zd");
     26        // SHOW(sizeof( a   ), "%zd");
     27        // SHOW(sizeof(&a   ), "%zd");
     28        // SHOW(sizeof( a[0]), "%zd");
     29        // SHOW(sizeof(&a[0]), "%zd");
    3030
    3131
    3232
    3333int main() {
     34        float a[10];
     35        static_assert(sizeof(float) == 4);              $\C{// floats (array elements) are 4 bytes}$
     36        static_assert(sizeof(void*) == 8);              $\C{// pointers are 8 bytes}$
     37        static_assert(sizeof(a) == 40);                 $\C{// array}$
     38        static_assert(sizeof(&a) == 8 );                $\C{// pointer to array}$
     39        static_assert(sizeof(a[0]) == 4 );              $\C{// first element}$
     40        static_assert(sizeof(&(a[0])) == 8 );   $\C{// pointer to first element}$
    3441
    35 /*
    36 When a programmer works with an array, C semantics provide access to a type that is different in every way from ``pointer to its first element.''
     42        typeof(&a) x;                                                   $\C{// x is pointer to array}$
     43        typeof(&(a[0])) y;                                              $\C{// y is pointer to first element}$
     44        @x = y;@                                                                $\C{// ill-typed}$
     45        @y = x;@                                                                $\C{// ill-typed}$
     46        static_assert(sizeof(typeof(a)) == 40);
     47        static_assert(sizeof(typeof(&a)) == 8 );
     48        static_assert(sizeof(typeof(a[0])) == 4 );
     49        static_assert(sizeof(typeof(&(a[0]))) == 8 );
    3750
    38 Its qualities become apparent by inspecting the declaration
    39 */
    40     float a[10];
    41 /*
     51        void f( float (*pa)[10] ) {
     52            static_assert(sizeof(   *pa     ) == 40); $\C{// array}$
     53            static_assert(sizeof(    pa     ) == 8 ); $\C{// pointer to array}$
     54            static_assert(sizeof(  (*pa)[0] ) == 4 ); $\C{// first element}$
     55            static_assert(sizeof(&((*pa)[0])) == 8 ); $\C{// pointer to first element}$
     56        }
     57        f( & a );
    4258
    43 The inspection begins by using @sizeof@ to provide definite program semantics for the intuition of an expression's type.
     59        float fs[] = {3.14, 1.707};
     60        char cs[] = "hello";
    4461
    45 Assuming a target platform keeps things concrete:
    46 */
    47     static_assert(sizeof(float)==4);    // floats (array elements) are 4 bytes
    48     static_assert(sizeof(void*)==8);    // pointers are 8 bytes
    49 /*
    50 
    51 Consider the sizes of expressions derived from @a@, modified by adding ``pointer to'' and ``first element'' (and including unnecessary parentheses to avoid confusion about precedence).
    52 */
    53     static_assert(sizeof(  a    ) == 40); // array
    54     static_assert(sizeof(& a    ) == 8 ); // pointer to array
    55     static_assert(sizeof(  a[0] ) == 4 ); // first element
    56     static_assert(sizeof(&(a[0])) == 8 ); // pointer to first element
    57 /*
    58 That @a@ takes up 40 bytes is common reasoning for C programmers.
    59 Set aside for a moment the claim that this first assertion is giving information about a type.
    60 For now, note that an array and a pointer to its first element are, sometimes, different things.
    61 
    62 The idea that there is such a thing as a pointer to an array may be surprising.
    63 It is not the same thing as a pointer to the first element:
    64 */
    65     typeof(& a    ) x;   // x is pointer to array
    66     typeof(&(a[0])) y;   // y is pointer to first element
    67                        ERR(
    68     x = y;             // ill-typed
    69     y = x;             // ill-typed
    70                        )
    71 /*
    72 The first gets
    73     warning: warning: assignment to `float (*)[10]' from incompatible pointer type `float *'
    74 and the second gets the opposite.
    75 */
    76 
    77 /*
    78 We now refute a concern that @sizeof(a)@ is reporting on special knowledge from @a@ being an local variable,
    79 say that it is informing about an allocation, rather than simply a type.
    80 
    81 First, recognizing that @sizeof@ has two forms, one operating on an expression, the other on a type, we observe that the original answers are unaffected by using the type-parameterized form:
    82 */
    83     static_assert(sizeof(typeof(  a    )) == 40);
    84     static_assert(sizeof(typeof(& a    )) == 8 );
    85     static_assert(sizeof(typeof(  a[0] )) == 4 );
    86     static_assert(sizeof(typeof(&(a[0]))) == 8 );
    87 
    88 /*
    89 Finally, the same sizing is reported when there is no allocation at all, and we launch the analysis instead from the pointer-to-array type.
    90 */
    91     void f( float (*pa)[10] ) {
    92         static_assert(sizeof(   *pa     ) == 40); // array
    93         static_assert(sizeof(    pa     ) == 8 ); // pointer to array
    94         static_assert(sizeof(  (*pa)[0] ) == 4 ); // first element
    95         static_assert(sizeof(&((*pa)[0])) == 8 ); // pointer to first element
    96     }
    97     f( & a );
    98 
    99 /*
    100 So, in spite of considerable programmer success enabled by an understanding that
    101 an array just a pointer to its first element (revisited TODO pointer decay),
    102 this understanding is simplistic.
    103 */
    104 
    105 /*
    106 A shortened form for declaring local variables exists, provided that length information is given in the initializer:
    107 */
    108     float fs[] = {3.14, 1.707};
    109     char cs[] = "hello";
    110 
    111     static_assert( sizeof(fs) == 2 * sizeof(float) );
    112     static_assert( sizeof(cs) == 6 * sizeof(char) );  // 5 letters + 1 null terminator
    113 
    114 /*
    115 In these declarations, the resulting types are both arrays, but their lengths are inferred.
    116 */
    117 
     62        static_assert( sizeof(fs) == 2 * sizeof(float) );
     63        static_assert( sizeof(cs) == 6 * sizeof(char) );  $\C{// 5 letters + 1 null terminator}$
    11864}
    11965
     66void syntaxReferenceCheck(void) {
     67        // $\rightarrow$ & (base element)
     68        //     & @float@
     69        //     & @float x;@
     70        //     & @[ float ]@
     71        //     & @[ float ]@
     72        float x0;
    12073
    121 void syntaxReferenceCheck(void) {
    122     // $\rightarrow$ & (base element)
    123     //     & @float@
    124     //     & @float x;@
    125     //     & @[ float ]@
    126     //     & @[ float ]@
    127     float x0;
     74        // $\rightarrow$ & pointer
     75        //     & @float *@
     76        //     & @float * x;@
     77        //     & @[ * float ]@
     78        //     & @[ * float ]@
     79        float * x1;
    12880
    129     // $\rightarrow$ & pointer
    130     //     & @float *@
    131     //     & @float * x;@
    132     //     & @[ * float ]@
    133     //     & @[ * float ]@
    134     float * x1;
     81        // $\rightarrow$ & array
     82        //     & @float[10]@
     83        //     & @float x[10];@
     84        //     & @[ [10] float ]@
     85        //     & @[ array(float, 10) ]@
     86        float x2[10];
    13587
    136     // $\rightarrow$ & array
    137     //     & @float[10]@
    138     //     & @float x[10];@
    139     //     & @[ [10] float ]@
    140     //     & @[ array(float, 10) ]@
    141     float x2[10];
     88        typeof(float[10]) x2b;
    14289
    143     typeof(float[10]) x2b;
    144 
    145     // & array of pointers
    146     //     & @(float*)[10]@
    147     //     & @float *x[10];@
    148     //     & @[ [10] * float ]@
    149     //     & @[ array(*float, 10) ]@
    150     float *x3[10];
     90        // & array of pointers
     91        //     & @(float*)[10]@
     92        //     & @float *x[10];@
     93        //     & @[ [10] * float ]@
     94        //     & @[ array(*float, 10) ]@
     95        float *x3[10];
    15196//    (float *)x3a[10];  NO
    15297
    153     // $\rightarrow$ & pointer to array
    154     //     & @float(*)[10]@
    155     //     & @float (*x)[10];@
    156     //     & @[ * [10] float ]@
    157     //     & @[ * array(float, 10) ]@
    158     float (*x4)[10];
     98        // $\rightarrow$ & pointer to array
     99        //     & @float(*)[10]@
     100        //     & @float (*x)[10];@
     101        //     & @[ * [10] float ]@
     102        //     & @[ * array(float, 10) ]@
     103        float (*x4)[10];
    159104
    160     // & pointer to array
    161     //     & @(float*)(*)[10]@
    162     //     & @float *(*x)[10];@
    163     //     & @[ * [10] * float ]@
    164     //     & @[ * array(*float, 10) ]@
    165     float *(*x5)[10];
    166     x5 =     (float*(*)[10]) x4;
     105        // & pointer to array
     106        //     & @(float*)(*)[10]@
     107        //     & @float *(*x)[10];@
     108        //     & @[ * [10] * float ]@
     109        //     & @[ * array(*float, 10) ]@
     110        float *(*x5)[10];
     111        x5 =     (float*(*)[10]) x4;
    167112//    x5 =     (float(*)[10]) x4;  // wrong target type; meta test suggesting above cast uses correct type
    168113
    169     // [here]
    170     // const
     114        // [here]
     115        // const
    171116
    172     // [later]
    173     // static
    174     // star as dimension
    175     // under pointer decay:                int p1[const 3]  being  int const *p1
     117        // [later]
     118        // static
     119        // star as dimension
     120        // under pointer decay:                int p1[const 3]  being  int const *p1
    176121
    177     const float * y1;
    178     float const * y2;
    179     float * const y3;
     122        const float * y1;
     123        float const * y2;
     124        float * const y3;
    180125
    181     y1 = 0;
    182     y2 = 0;
    183     // y3 = 0; // bad
     126        y1 = 0;
     127        y2 = 0;
     128        // y3 = 0; // bad
    184129
    185     // *y1 = 3.14; // bad
    186     // *y2 = 3.14; // bad
    187     *y3 = 3.14;
     130        // *y1 = 3.14; // bad
     131        // *y2 = 3.14; // bad
     132        *y3 = 3.14;
    188133
    189     const float z1 = 1.414;
    190     float const z2 = 1.414;
     134        const float z1 = 1.414;
     135        float const z2 = 1.414;
    191136
    192     // z1 = 3.14; // bad
    193     // z2 = 3.14; // bad
     137        // z1 = 3.14; // bad
     138        // z2 = 3.14; // bad
    194139
    195140
    … …  
    199144void stx2() { const T x[10];
    200145//            x[5] = 3.14; // bad
    201             }
     146                }
    202147void stx3() { T const x[10];
    203148//            x[5] = 3.14; // bad
    204             }
     149                }
     150
     151// Local Variables: //
     152// compile-command: "sed -f sedcmd bkgd-carray-arrty.c > tmp.c; gcc tmp.c" //
     153// End: //

  • doc/theses/mike_brooks_MMath/programs/bkgd-carray-decay.c

    r03606ce r266732e  
    11#include <assert.h>
    22int main() {
     3        float a[10];                            $\C{// array}$
     4        float (*pa)[10] = &a;           $\C{// pointer to array}$
     5        float a0 = a[0];                        $\C{// element}$
     6        float *pa0 = &(a[0]);           $\C{// pointer to element}$
    37
    4 /*
    5 The last section established the difference between these four types:
    6 */
     8        float *pa0x = a;                        $\C{// (ok)}$
     9        assert( pa0 == pa0x );
     10        assert( sizeof(pa0x) != sizeof(a) );
    711
    8     float    a  [10] ;          // array
    9     float (*pa )[10] = & a    ; // pointer to array
    10     float    a0      =   a[0] ; // element
    11     float  *pa0      = &(a[0]); // pointer to element
     12        void f( float x[10], float *y ) {
     13                static_assert( sizeof(x) == sizeof(void*) );
     14                static_assert( sizeof(y) == sizeof(void*) );
     15        }
     16        f(0,0);
    1217
    13 /*
    14 But the expression used for obtaining the pointer to the first element is pedantic.
    15 The root of all C programmer experience with arrays is the shortcut
    16 */
    17     float  *pa0x     =   a    ; // (ok)
    18 /*
    19 which reproduces @pa0@, in type and value:
    20 */
    21     assert( pa0 == pa0x );
    22 /*
    23 The validity of this initialization is unsettling, in the context of the facts established in the last section.
    24 Notably, it initializes name @pa0x@ from expression @a@, when they are not of the same type:
    25 */
    26     assert( sizeof(pa0x) != sizeof(a) );
     18        // reusing local var `float a[10];`}
     19        float v;
     20        f(  a,  a ); $\C{// ok: two decays, one into an array spelling}$
     21        f( &v, &v ); $\C{// ok: no decays; a non-array passes to an array spelling}$
    2722
     23        char ca[] = "hello";    $\C{// array on stack, initialized from read-only data}$
     24        char *cp = "hello";     $\C{// pointer to read-only data [decay here]}$
     25        void edit(char c[]) {   $\C{// param is pointer}$
     26                c[3] = 'p';
     27        }
     28        edit(ca);               $\C{// ok [decay here]}$
     29        edit(cp);               $\C{// Segmentation fault}$
     30        edit("hello");          $\C{// Segmentation fault [decay here]}$
    2831
     32        void decay( float x[10] ) {
     33                static_assert( sizeof(x) == sizeof(void*) );
     34        }
     35        static_assert( sizeof(a) == 10 * sizeof(float) );
     36        decay(a);
    2937
     38        void no_decay( float (*px)[10] ) {
     39                static_assert( sizeof(*px) == 10 * sizeof(float) );
     40        }
     41        static_assert( sizeof(*pa) == 10 * sizeof(float) );
     42        no_decay(pa);
     43}
    3044
    31 
    32 
    33 
    34 
    35 
    36 
    37 
    38 
    39 
    40     void f( float x[10], float *y ) {
    41         static_assert( sizeof(x) == sizeof(void*) );
    42         static_assert( sizeof(y) == sizeof(void*) );
    43     }
    44     f(0,0);
    45 
    46 
    47 
    48 
    49 
    50 
    51 
    52 
    53 
    54 
    55 
    56 
    57 
    58 
    59 
    60     // reusing local var `float a[10];`
    61     float v;
    62     f(  a,  a ); // ok: two decays, one into an array spelling
    63     f( &v, &v ); // ok: no decays; a non-array passes to an array spelling
    64 
    65 
    66 
    67 
    68 
    69 
    70 
    71 
    72 
    73 
    74 
    75 
    76 
    77 
    78 
    79 
    80     char ca[] = "hello";    // array on stack, initialized from read-only data
    81     char *cp = "hello";     // pointer to read-only data [decay here]
    82     void edit(char c[]) {   // param is pointer
    83         c[3] = 'p';
    84     }
    85     edit(ca);               // ok [decay here]
    86     edit(cp);               // Segmentation fault
    87     edit("hello");          // Segmentation fault [decay here]
    88 
    89 
    90 
    91 
    92 
    93 
    94 
    95 
    96 
    97 
    98 
    99 
    100     void decay( float x[10] ) {
    101         static_assert( sizeof(x) == sizeof(void*) );
    102     }
    103     static_assert( sizeof(a) == 10 * sizeof(float) );
    104     decay(a);
    105 
    106     void no_decay( float (*px)[10] ) {
    107         static_assert( sizeof(*px) == 10 * sizeof(float) );
    108     }
    109     static_assert( sizeof(*pa) == 10 * sizeof(float) );
    110     no_decay(pa);
    111 }
     45// Local Variables: //
     46// compile-command: "sed -f sedcmd bkgd-carray-decay.c > tmp.c; gcc tmp.c" //
     47// End: //

  • doc/theses/mike_brooks_MMath/string.tex

    r03606ce r266732e  
    66
    77\input{sharing-demo.tex}
     8
     9Consider two strings @s1@ and @s1a@ that are in an aliasing relationship, and a third, @s2@, made by a simple copy from @s1@.
     10\par\noindent
     11\begin{tabular}{llll}
     12                                & @s1@  & @s1a@ & @s2@  \\
     13%\input{sharing-demo1.tex}
     14\end{tabular}
     15\par\noindent
     16
    817
    918\subsection{RAII limitations}
    … …  
    225234}
    226235\end{lstlisting}
     236
     237\section{String I/O}

  • doc/theses/mike_brooks_MMath/uw-ethesis.tex

    r03606ce r266732e  
    11%======================================================================
    2 % University of Waterloo Thesis Template for LaTeX
    3 % Last Updated November, 2020
    4 % by Stephen Carr, IST Client Services,
     2% University of Waterloo Thesis Template for LaTeX 
     3% Last Updated August 2022
     4% by IST Client Services,
    55% University of Waterloo, 200 University Ave. W., Waterloo, Ontario, Canada
    6 % FOR ASSISTANCE, please send mail to request@uwaterloo.ca
     6% FOR ASSISTANCE, please send mail to helpdesk@uwaterloo.ca
    77
    88% DISCLAIMER
    … …  
    2121
    2222% DON'T FORGET TO ADD YOUR OWN NAME AND TITLE in the "hyperref" package configuration below.
    23 % THIS INFORMATION GETS EMBEDDED IN THE PDF FINAL PDF DOCUMENT.
     23% Search for: PDFTITLE, PDFAUTHOR, PDFSUBJECT, and PDFKEYWORDS.
     24% THIS INFORMATION GETS EMBEDDED IN THE FINAL PDF DOCUMENT.
    2425% You can view the information if you view properties of the PDF document.
    2526
    26 % Many faculties/departments also require one or more printed copies.
    27 % This template attempts to satisfy both types of output.
     27% Many faculties/departments also require one or more printed copies. 
     28% This template attempts to satisfy both types of output. 
    2829% See additional notes below.
    2930% It is based on the standard "book" document class which provides all necessary sectioning structures and allows multi-part theses.
    … …  
    3233
    3334% For people who prefer to install their own LaTeX distributions on their own computers, and process the source files manually, the following notes provide the sequence of tasks:
    34 
     35 
    3536% E.g. to process a thesis called "mythesis.tex" based on this template, run:
    3637
    … …  
    5152% Tip: Photographs should be cropped and compressed so as not to be too large.
    5253
    53 % To create a PDF output that is optimized for double-sided printing:
     54% To create a PDF output that is optimized for double-sided printing: 
    5455% 1) comment-out the \documentclass statement in the preamble below, and un-comment the second \documentclass line.
    5556% 2) change the value assigned below to the boolean variable "PrintVersion" from " false" to "true".
    … …  
    6061% For hyperlinked PDF, suitable for viewing on a computer, use this:
    6162\documentclass[letterpaper,12pt,titlepage,oneside,final]{book}
    62 \usepackage{times}
    6363\usepackage[T1]{fontenc}        % Latin-1 => 256-bit characters, => | not dash, <> not Spanish question marks
    64 
     64 
    6565% For PDF, suitable for double-sided printing, change the PrintVersion variable below to "true" and use this \documentclass line instead of the one above:
    6666%\documentclass[letterpaper,12pt,titlepage,openright,twoside,final]{book}
    … …  
    6969% If you have to, it's easier to make changes to nomenclature once here than in a million places throughout your thesis!
    7070\newcommand{\package}[1]{\textbf{#1}} % package names in bold text
    71 \newcommand{\cmmd}[1]{\textbackslash\texttt{#1}} % command name in tt font
     71\newcommand{\cmmd}[1]{\textbackslash\texttt{#1}} % command name in tt font 
    7272\newcommand{\href}[1]{#1} % does nothing, but defines the command so the print-optimized version will ignore \href tags (redefined by hyperref pkg).
    7373%\newcommand{\texorpdfstring}[2]{#1} % does nothing, but defines the command
    … …  
    8282%\usepackage{nomencl} % For a nomenclature (optional; available from ctan.org)
    8383\usepackage{amsmath,amssymb,amstext} % Lots of math symbols and environments
     84\usepackage{fullpage,times,comment}
    8485\usepackage{xcolor}
    8586\usepackage{epic,eepic}
    8687\usepackage{graphicx}
    87 \graphicspath{{pictures/}} % picture directory
    88 \usepackage{comment} % Removes large sections of the document.
    8988\usepackage{tabularx}
    9089\usepackage[labelformat=simple,aboveskip=0pt,farskip=0pt,font=normalsize]{subfig}
    9190\renewcommand\thesubfigure{(\alph{subfigure})}
    9291
    93 \usepackage{algorithm}
    94 \usepackage{algpseudocode}
    95 
     92\graphicspath{{pictures/}} % picture directory
     93%\usepackage{algorithm}
     94%\usepackage{algpseudocode}
    9695\usepackage{pbox}
     96
     97\makeatletter
     98\newcommand{\lstinput}[2]{\lstinputlisting[linerange={#1},xleftmargin=4pt,escapechar={\$},moredelim={**[is][\color{red}]{@}{@}}]{#2}}
     99\makeatother
     100% cfa macros used in the document
     101\input{common}
     102%\usepackage{common}
     103\CFAStyle                                               % CFA code-style
     104\lstset{language=cfa,belowskip=-1pt} % set default language to CFA
     105\lstset{inputpath={programs}}
     106
     107\newcommand{\uCpp}{$\mu$\CC}
     108\newcommand{\PAB}[1]{{\color{red}PAB: #1}}
    97109
    98110% Hyperlinks make it very easy to navigate an electronic document.
    99111% In addition, this is where you should specify the thesis title and author as they appear in the properties of the PDF document.
    100 % Use the "hyperref" package
     112% Use the "hyperref" package 
    101113% N.B. HYPERREF MUST BE THE LAST PACKAGE LOADED; ADD ADDITIONAL PKGS ABOVE
     114\usepackage{url}
    102115\usepackage[pagebackref=true]{hyperref} % with basic options
    103116%\usepackage[pdftex,pagebackref=true]{hyperref}
    … …  
    110123    pdffitwindow=false,     % window fit to page when opened
    111124    pdfstartview={FitH},    % fits the width of the page to the window
    112     pdftitle={Cforall Memory Allocation}, % title: CHANGE THIS TEXT!
    113     pdfauthor={Mubeen Zulfiqar},    % author: CHANGE THIS TEXT! and uncomment this line
     125    pdftitle={\CFA Container Library}, % title: CHANGE THIS TEXT!
     126    pdfauthor={Mike Brooks},    % author: CHANGE THIS TEXT! and uncomment this line
    114127    pdfsubject={Cforall},  % subject: CHANGE THIS TEXT! and uncomment this line
    115     pdfkeywords={Cforall} {storage allocation} {C language}, % optional list of keywords
     128    pdfkeywords={Cforall} {container library} {C language}, % optional list of keywords
    116129    pdfnewwindow=true,      % links in new window
    117130    colorlinks=true,        % false: boxed links; true: colored links
    118131    linkcolor=blue,         % color of internal links
    119     citecolor=blue,        % color of links to bibliography
     132    citecolor=blue,         % color of links to bibliography
    120133    filecolor=magenta,      % color of file links
    121     urlcolor=blue,           % color of external links
     134    urlcolor=blue,          % color of external links
    122135    breaklinks=true
    123136}
    124137\ifthenelse{\boolean{PrintVersion}}{   % for improved print quality, change some hyperref options
    125138\hypersetup{    % override some previously defined hyperref options
     139%    colorlinks,%
    126140    citecolor=black,%
    127141    filecolor=black,%
    128142    linkcolor=black,%
    129     urlcolor=black
    130 }}{} % end of ifthenelse (no else)
     143    urlcolor=black}
     144}{} % end of ifthenelse (no else)
     145
     146\usepackage{breakurl}
    131147\urlstyle{sf}
    132148
    133149%\usepackage[automake,toc,abbreviations]{glossaries-extra} % Exception to the rule of hyperref being the last add-on package
    134 % If glossaries-extra is not in your LaTeX distribution, get it from CTAN (http://ctan.org/pkg/glossaries-extra),
    135 % although it's supposed to be in both the TeX Live and MikTeX distributions. There are also documentation and
     150% If glossaries-extra is not in your LaTeX distribution, get it from CTAN (http://ctan.org/pkg/glossaries-extra), 
     151% although it's supposed to be in both the TeX Live and MikTeX distributions. There are also documentation and 
    136152% installation instructions there.
    137153
    … …  
    140156
    141157% Setting up the page margins...
    142 \setlength{\textheight}{9in}
    143 \setlength{\topmargin}{-0.45in}
    144 \setlength{\headsep}{0.25in}
     158%\setlength{\textheight}{9in}
     159%\setlength{\topmargin}{-0.45in}
     160%\setlength{\headsep}{0.25in}
    145161% uWaterloo thesis requirements specify a minimum of 1 inch (72pt) margin at the
    146 % top, bottom, and outside page edges and a 1.125 in. (81pt) gutter margin (on binding side).
     162% top, bottom, and outside page edges and a 1.125 in. (81pt) gutter margin (on binding side). 
    147163% While this is not an issue for electronic viewing, a PDF may be printed, and so we have the same page layout for both printed and electronic versions, we leave the gutter margin in.
    148164% Set margins to minimum permitted by uWaterloo thesis regulations:
    … …  
    152168% edge is less than 15 mm (0.6 in.)
    153169\setlength{\marginparsep}{0pt} % width of space between body text and margin notes
    154 \setlength{\evensidemargin}{0.125in} % Adds 1/8 in. to binding side of all
     170\setlength{\evensidemargin}{0.125in} % Adds 1/8 in. to binding side of all 
    155171% even-numbered pages when the "twoside" printing option is selected
    156172\setlength{\oddsidemargin}{0.125in} % Adds 1/8 in. to the left of all pages when "oneside" printing is selected, and to the left of all odd-numbered pages when "twoside" printing is selected
    … …  
    161177\setlength{\parskip}{\medskipamount}
    162178
    163 % The following statement controls the line spacing.
     179% The following statement controls the line spacing. 
    164180% The default spacing corresponds to good typographic conventions and only slight changes (e.g., perhaps "1.2"), if any, should be made.
    165181\renewcommand{\baselinestretch}{1} % this is the default line space setting
    … …  
    174190\let\cleardoublepage\clearemptydoublepage
    175191
    176 % Define Glossary terms (This is properly done here, in the preamble and
    177 % could also be \input{} from a separate file...)
     192% Define Glossary terms (This is properly done here, in the preamble and could also be \input{} from a separate file...)
    178193%\input{glossaries}
    179194%\makeglossaries
    180 
    181 % cfa macros used in the document
    182 \input{common}
    183 %\usepackageinput{common}
    184 \CFAStyle                                               % CFA code-style
    185 \lstset{language=CFA}                                   % default language
    186 \lstset{basicstyle=\linespread{0.9}\sf}                 % CFA typewriter font
    187 \lstset{inputpath={programs}}
    188 \newcommand{\PAB}[1]{{\color{red}PAB: #1}}
    189 
    190 \newcommand{\uCpp}{$\mu$\CC}
    191195
    192196%======================================================================
    … …  
    202206% dedication, table of contents, list of tables, list of figures, nomenclature, etc.
    203207%----------------------------------------------------------------------
    204 \input{uw-ethesis-frontpgs}
     208\input{uw-ethesis-frontpgs} 
    205209
    206210%----------------------------------------------------------------------
    … …  
    211215% Tip: Putting each sentence on a new line is a way to simplify later editing.
    212216%----------------------------------------------------------------------
    213 \begin{sloppypar}
     217
    214218\input{intro}
    215219\input{background}
    … …  
    219223\input{conclusion}
    220224
    221 \end{sloppypar}
    222 
    223225%----------------------------------------------------------------------
    224226% END MATERIAL
    … …  
    228230% Bibliography
    229231
    230 % The following statement selects the style to use for references.
     232% The following statement selects the style to use for references. 
    231233% It controls the sort order of the entries in the bibliography and also the formatting for the in-text labels.
    232234\bibliographystyle{plain}
    233 % This specifies the location of the file containing the bibliographic information.
     235% This specifies the location of the file containing the bibliographic information. 
    234236% It assumes you're using BibTeX to manage your references (if not, why not?).
    235237\cleardoublepage % This is needed if the "book" document class is used, to place the anchor in the correct page, because the bibliography will start on its own page.
    236238% Use \clearpage instead if the document class uses the "oneside" argument
    237 \phantomsection  % With hyperref package, enables hyperlinking from the table of contents to bibliography
     239\phantomsection  % With hyperref package, enables hyperlinking from the table of contents to bibliography             
    238240% The following statement causes the title "References" to be used for the bibliography section:
    239241\renewcommand*{\bibname}{References}
    … …  
    243245
    244246\bibliography{pl,uw-ethesis}
    245 % Tip: You can create multiple .bib files to organize your references.
     247% Tip: You can create multiple .bib files to organize your references. 
    246248% Just list them all in the \bibliogaphy command, separated by commas (no spaces).
    247249
    248 % The following statement causes the specified references to be added to the bibliography even if they were not cited in the text.
     250% The following statement causes the specified references to be added to the bibliography even if they were not cited in the text. 
    249251% The asterisk is a wildcard that causes all entries in the bibliographic database to be included (optional).
    250252% \nocite{*}
    … …  
    261263% \input{appendix-matlab_plots.tex}
    262264
    263 % GLOSSARIES (Lists of definitions, abbreviations, symbols, etc.
    264 % provided by the glossaries-extra package)
     265% GLOSSARIES (Lists of definitions, abbreviations, symbols, etc. provided by the glossaries-extra package)
    265266% -----------------------------
    266267%\printglossaries
Note: See TracChangeset for help on using the changeset viewer.