Cleanup related to the Gauss example.

doc/invargent-manual.tm

@@ -1142,6 +1142,12 @@
   because InvarGenT, noticing the failure, generates an OCaml source with
   more type information, as if the <verbatim|-full_annot> option was used.
 
+  The example <verbatim|liquid_fft_simpler.gadt> contains assertions, but
+  despite them is nearly as hard as <verbatim|liquid_fft.gadt>. It needs the
+  option <verbatim|-same_with_assertions> to not switch to settings tuned for
+  cases where assertions capture the harder aspects of the invariants to
+  infer.
+
   Unfortunately, inference fails for some examples regardless of parameters
   setting. We discuss them in the next section.
 
@@ -1376,10 +1382,16 @@
   with the option <verbatim|-prefer_bound_to_local>. Additionally, we can
   relax the constraint on the processed portion of the matrix, coming from
   the restriction on the matrix size intended in the original source of the
-  <verbatim|liquid_gauss_harder.gadt> example. In
-  <verbatim|liquid_gauss.gadt>, the whole matrix is processed and the
-  inferred type is most general, under the default settings -- no need to
-  pass any options to InvarGenT.
+  FFT examples. In <verbatim|liquid_gauss.gadt>, the whole matrix is
+  processed and the inferred type is most general, under the default settings
+  -- no need to pass any options to InvarGenT. The reason
+  <verbatim|liquid_gauss_harder.gadt> is too difficult for InvarGenT is that
+  the nesting interferes with the propagation of use-site constraints to the
+  postcondition of the nested definition (the <verbatim|loop> inside
+  <verbatim|rowMax>). Inference works for
+  <verbatim|liquid_gauss_harder_asserted.gadt>, because the assertion
+  provides the required information to infer the <verbatim|rowMax> invariants
+  directly.
 </body>
 
 <\initial>

examples/liquid_gauss_harder.gadt

@@ -88,7 +88,7 @@ let rowElim r s n i =
 let gauss data =
   let n = matrix_dim1 data in
 
-  let rec rowMax i =
+  let rec rowMax = efunction i ->
     let x = fabs (matrix_get data i i) in
     let rec loop j x mx =
       eif j + 1 <= n then

examples/liquid_gauss_harder_asserted.gadt

@@ -87,12 +87,11 @@ let rowElim r s n i =
 
 let gauss data =
   let n = matrix_dim1 data in
-  assert num n + 1 <= matrix_dim2 data;
-  assert num matrix_dim2 data <= n + 1;
 
-  let rec rowMax i =
+  let rec rowMax = efunction i ->
     let x = fabs (matrix_get data i i) in
     let rec loop j x mx =
+      assert num mx + 1 <= n;
       eif j + 1 <= n then
         let y = fabs (matrix_get data j i) in
         eif (less x y) then loop (j+1) y j

examples/liquid_gauss_harder_asserted.gadti.target

@@ -71,4 +71,4 @@ val rowElim :
    ∀i, j, k, n[0 ≤ n ∧ n + 1 ≤ i ∧ k ≤ i ∧ k ≤ j].
    Array (Float, j) → Array (Float, i) → Num k → Num n → ()
 
-val gauss : ∀n[1 ≤ n]. Matrix (n, n + 1) → ()
+val gauss : ∀k, n[1 ≤ n ∧ n + 1 ≤ k]. Matrix (n, k) → ()

src/InvarGenTTest.ml

@@ -673,12 +673,11 @@ let tests = "InvarGenT" >::: [
            test_case "liquid_gauss_asserted" ());
       "liquid_gauss_harder_asserted" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_gauss_harder_asserted" ());
       "liquid_gauss_harder" >::
         (fun () ->
-           todo "FIXME";
+           todo "Too hard for current InvarGenT";
            skip_if !debug "debug";
            test_case "liquid_gauss_harder" ());
       "liquid_fft_ffor" >::