Merge pull request #1406 from GaloisInc/ffi-nested-seq

Support nested sequences in FFI

docs/RefMan/FFI.rst

@@ -188,20 +188,23 @@ Other sizes of floating points are not supported.
 Sequences
 ~~~~~~~~~
 
-Let ``n : #`` be a Cryptol type, possibly containing type variables, that
-satisfies ``fin n``, and ``T`` be one of the above Cryptol *integral types* or
-*floating point types*. Let ``U`` be the C type that ``T`` corresponds to.
-
-============  ===========
-Cryptol type  C type
-============  ===========
-``[n]T``      ``U*``
-============  ===========
-
-The C pointer points to an array of ``n`` elements of type ``U``. Note that,
-while the length of the array itself is not explicitly passed along with the
-pointer, any type arguments contained in the size are passed as C ``size_t``'s
-earlier, so the C code can always know the length of the array.
+Let ``n1, n2, ..., nk : #`` be Cryptol types (with ``k >= 1``), possibly
+containing type variables, that satisfy ``fin n1, fin n2, ..., fin nk``, and
+``T`` be one of the above Cryptol *integral types* or *floating point types*.
+Let ``U`` be the C type that ``T`` corresponds to.
+
+====================  ===========
+Cryptol type          C type
+====================  ===========
+``[n1][n2]...[nk]T``  ``U*``
+====================  ===========
+
+The C pointer points to an array of ``n1 * n2 * ... * nk`` elements of type
+``U``. If the sequence is multidimensional, it is flattened and stored
+contiguously, similar to the representation of multidimensional arrays in C.
+Note that, while the dimensions of the array itself are not explicitly passed
+along with the pointer, any type arguments contained in the size are passed as C
+``size_t``'s earlier, so the C code can always know the dimensions of the array.
 
 Tuples and records
 ~~~~~~~~~~~~~~~~~~
@@ -258,12 +261,12 @@ Cryptol type (or kind)              C argument type(s)   C return type  C output
 ``[K]Bit`` where ``32 <  K <= 64``  ``uint64_t``         ``uint64_t``   ``uint64_t*``
 ``Float32``                         ``float``            ``float``      ``float*``
 ``Float64``                         ``double``           ``double``     ``double*``
-``[n]T``                            ``U*``               N/A            ``U*``
+``[n1][n2]...[nk]T``                ``U*``               N/A            ``U*``
 ``(T1, T2, ..., Tn)``               ``U1, U2, ..., Un``  N/A            ``V1, V2, ..., Vn``
 ``{f1: T1, f2: T2, ..., fn: Tn}``   ``U1, U2, ..., Un``  N/A            ``V1, V2, ..., Vn``
 ==================================  ===================  =============  =========================
 
-where ``K`` is a constant number, ``n`` is a variable number, ``Ti`` is a type,
+where ``K`` is a constant number, ``ni`` are variable numbers, ``Ti`` is a type,
 ``Ui`` is its C argument type, and ``Vi`` is its C output argument type.
 
 Memory

docs/RefMan/_build/html/FFI.html

@@ -303,29 +303,32 @@ <h3>Floating point types<a class="headerlink" href="#floating-point-types" title
 </section>
 <section id="sequences">
 <h3>Sequences<a class="headerlink" href="#sequences" title="Permalink to this heading"></a></h3>
-<p>Let <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">:</span> <span class="pre">#</span></code> be a Cryptol type, possibly containing type variables, that
-satisfies <code class="docutils literal notranslate"><span class="pre">fin</span> <span class="pre">n</span></code>, and <code class="docutils literal notranslate"><span class="pre">T</span></code> be one of the above Cryptol <em>integral types</em> or
-<em>floating point types</em>. Let <code class="docutils literal notranslate"><span class="pre">U</span></code> be the C type that <code class="docutils literal notranslate"><span class="pre">T</span></code> corresponds to.</p>
+<p>Let <code class="docutils literal notranslate"><span class="pre">n1,</span> <span class="pre">n2,</span> <span class="pre">...,</span> <span class="pre">nk</span> <span class="pre">:</span> <span class="pre">#</span></code> be Cryptol types (with <code class="docutils literal notranslate"><span class="pre">k</span> <span class="pre">&gt;=</span> <span class="pre">1</span></code>), possibly
+containing type variables, that satisfy <code class="docutils literal notranslate"><span class="pre">fin</span> <span class="pre">n1,</span> <span class="pre">fin</span> <span class="pre">n2,</span> <span class="pre">...,</span> <span class="pre">fin</span> <span class="pre">nk</span></code>, and
+<code class="docutils literal notranslate"><span class="pre">T</span></code> be one of the above Cryptol <em>integral types</em> or <em>floating point types</em>.
+Let <code class="docutils literal notranslate"><span class="pre">U</span></code> be the C type that <code class="docutils literal notranslate"><span class="pre">T</span></code> corresponds to.</p>
 <table class="docutils align-default">
 <colgroup>
-<col style="width: 52%" />
-<col style="width: 48%" />
+<col style="width: 65%" />
+<col style="width: 35%" />
 </colgroup>
 <thead>
 <tr class="row-odd"><th class="head"><p>Cryptol type</p></th>
 <th class="head"><p>C type</p></th>
 </tr>
 </thead>
 <tbody>
-<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">[n]T</span></code></p></td>
+<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">[n1][n2]...[nk]T</span></code></p></td>
 <td><p><code class="docutils literal notranslate"><span class="pre">U*</span></code></p></td>
 </tr>
 </tbody>
 </table>
-<p>The C pointer points to an array of <code class="docutils literal notranslate"><span class="pre">n</span></code> elements of type <code class="docutils literal notranslate"><span class="pre">U</span></code>. Note that,
-while the length of the array itself is not explicitly passed along with the
-pointer, any type arguments contained in the size are passed as C <code class="docutils literal notranslate"><span class="pre">size_t</span></code>’s
-earlier, so the C code can always know the length of the array.</p>
+<p>The C pointer points to an array of <code class="docutils literal notranslate"><span class="pre">n1</span> <span class="pre">*</span> <span class="pre">n2</span> <span class="pre">*</span> <span class="pre">...</span> <span class="pre">*</span> <span class="pre">nk</span></code> elements of type
+<code class="docutils literal notranslate"><span class="pre">U</span></code>. If the sequence is multidimensional, it is flattened and stored
+contiguously, similar to the representation of multidimensional arrays in C.
+Note that, while the dimensions of the array itself are not explicitly passed
+along with the pointer, any type arguments contained in the size are passed as C
+<code class="docutils literal notranslate"><span class="pre">size_t</span></code>’s earlier, so the C code can always know the dimensions of the array.</p>
 </section>
 <section id="tuples-and-records">
 <h3>Tuples and records<a class="headerlink" href="#tuples-and-records" title="Permalink to this heading"></a></h3>
@@ -432,7 +435,7 @@ <h3>Quick reference<a class="headerlink" href="#quick-reference" title="Permalin
 <td><p><code class="docutils literal notranslate"><span class="pre">double</span></code></p></td>
 <td><p><code class="docutils literal notranslate"><span class="pre">double*</span></code></p></td>
 </tr>
-<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">[n]T</span></code></p></td>
+<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">[n1][n2]...[nk]T</span></code></p></td>
 <td><p><code class="docutils literal notranslate"><span class="pre">U*</span></code></p></td>
 <td><p>N/A</p></td>
 <td><p><code class="docutils literal notranslate"><span class="pre">U*</span></code></p></td>
@@ -449,7 +452,7 @@ <h3>Quick reference<a class="headerlink" href="#quick-reference" title="Permalin
 </tr>
 </tbody>
 </table>
-<p>where <code class="docutils literal notranslate"><span class="pre">K</span></code> is a constant number, <code class="docutils literal notranslate"><span class="pre">n</span></code> is a variable number, <code class="docutils literal notranslate"><span class="pre">Ti</span></code> is a type,
+<p>where <code class="docutils literal notranslate"><span class="pre">K</span></code> is a constant number, <code class="docutils literal notranslate"><span class="pre">ni</span></code> are variable numbers, <code class="docutils literal notranslate"><span class="pre">Ti</span></code> is a type,
 <code class="docutils literal notranslate"><span class="pre">Ui</span></code> is its C argument type, and <code class="docutils literal notranslate"><span class="pre">Vi</span></code> is its C output argument type.</p>
 </section>
 </section>

docs/RefMan/_build/html/_sources/FFI.rst.txt

@@ -188,20 +188,23 @@ Other sizes of floating points are not supported.
 Sequences
 ~~~~~~~~~
 
-Let ``n : #`` be a Cryptol type, possibly containing type variables, that
-satisfies ``fin n``, and ``T`` be one of the above Cryptol *integral types* or
-*floating point types*. Let ``U`` be the C type that ``T`` corresponds to.
-
-============  ===========
-Cryptol type  C type
-============  ===========
-``[n]T``      ``U*``
-============  ===========
-
-The C pointer points to an array of ``n`` elements of type ``U``. Note that,
-while the length of the array itself is not explicitly passed along with the
-pointer, any type arguments contained in the size are passed as C ``size_t``'s
-earlier, so the C code can always know the length of the array.
+Let ``n1, n2, ..., nk : #`` be Cryptol types (with ``k >= 1``), possibly
+containing type variables, that satisfy ``fin n1, fin n2, ..., fin nk``, and
+``T`` be one of the above Cryptol *integral types* or *floating point types*.
+Let ``U`` be the C type that ``T`` corresponds to.
+
+====================  ===========
+Cryptol type          C type
+====================  ===========
+``[n1][n2]...[nk]T``  ``U*``
+====================  ===========
+
+The C pointer points to an array of ``n1 * n2 * ... * nk`` elements of type
+``U``. If the sequence is multidimensional, it is flattened and stored
+contiguously, similar to the representation of multidimensional arrays in C.
+Note that, while the dimensions of the array itself are not explicitly passed
+along with the pointer, any type arguments contained in the size are passed as C
+``size_t``'s earlier, so the C code can always know the dimensions of the array.
 
 Tuples and records
 ~~~~~~~~~~~~~~~~~~
@@ -258,12 +261,12 @@ Cryptol type (or kind)              C argument type(s)   C return type  C output
 ``[K]Bit`` where ``32 <  K <= 64``  ``uint64_t``         ``uint64_t``   ``uint64_t*``
 ``Float32``                         ``float``            ``float``      ``float*``
 ``Float64``                         ``double``           ``double``     ``double*``
-``[n]T``                            ``U*``               N/A            ``U*``
+``[n1][n2]...[nk]T``                ``U*``               N/A            ``U*``
 ``(T1, T2, ..., Tn)``               ``U1, U2, ..., Un``  N/A            ``V1, V2, ..., Vn``
 ``{f1: T1, f2: T2, ..., fn: Tn}``   ``U1, U2, ..., Un``  N/A            ``V1, V2, ..., Vn``
 ==================================  ===================  =============  =========================
 
-where ``K`` is a constant number, ``n`` is a variable number, ``Ti`` is a type,
+where ``K`` is a constant number, ``ni`` are variable numbers, ``Ti`` is a type,
 ``Ui`` is its C argument type, and ``Vi`` is its C output argument type.
 
 Memory