InvarGenT Manual - Solver Parameters. Bug fix: do not annotate `asser…

…t false` branch. Numerical abduction spurious translations for inequalities fix.

Makefile

@@ -13,6 +13,7 @@ docs:
 	rm -f -R doc/code
 	mv _build/src/InvarGenT.docdir doc/code
 	texmacs -c doc/invargent.tm doc/invargent.pdf -q
+	texmacs -c doc/invargent-manual.tm doc/invargent-manual.pdf -q
 
 .PHONY: clean
 

README.md

@@ -26,8 +26,7 @@ Milestones: [x] - completed, [#] - finishing (75%-95%), [+] - in the middle (25%
 - [x] Enforce convergence for numerical constraints. (Required for postconditions.)
 - [x] Factorize joint constraint abduction scheme for use across sorts.
 - [x] Add more tests and resolve issues that emerge.
-- [#] Export (print) a file with inferred types, and OCaml source. Collect examples, write user documentation.
-- [_] Write web interface.
+- [x] Export (print) a file with inferred types, and OCaml source. Collect examples, write user documentation.
 
 And version 2.0 goals:
 - [_] Export to OCaml using built-in or pervasives OCaml types, in particular `bool` instead of `boolean`.

TODO.md

@@ -3,4 +3,5 @@ Place for TODOs/FIXMEs, especially if not expressed in other places. See README.
 * TODO: perhaps `check_connected` could be simplified or even removed from abduction?
 * FIXME: repeating `newtype` and `newcons` definitions should be errors.
 * TODO: calibrate timeout parameters (number of iterations before forced exit from simple abduction, joint abduction etc.)
-* FIXME: `separate_subst` has a default argument `keep_uni=false`. Rethink for each use case if it is the correct argument.
+* FIXME: `separate_subst` has a default argument `keep_uni=false`. Rethink for each use case if it is the correct argument.
+* TODO: more parsimonious use of parentheses in printing expressions and types.

doc/invargent-manual.tm

@@ -468,7 +468,197 @@
 
   <section|Solver Parameters and CLI>
 
-  \;
+  The default settings of InvarGenT parameters should be sufficient for most
+  cases. For example, after downloading InvarGenT source code and changing
+  current directory to <verbatim|invargent>, we can enter, assuming a
+  Unix-like shell:
+
+  <\code>
+    $ make main
+
+    $ ./invargent examples/binary_upper_bound.gadt
+  </code>
+
+  To get the inferred types printed on standard output, use the
+  <verbatim|-inform> option:
+
+  <\code>
+    $ ./invargent -inform examples/binomial_heap_nonrec.gadt
+  </code>
+
+  In some situations, hopefully unlikely for simple programs, the default
+  parameters of the solver algorithms do not suffice. Consider this example,
+  where we use <verbatim|-full_annot> to generate type annotations on
+  <verbatim|function> and <verbatim|let>..<verbatim|in> nodes in the
+  <verbatim|.ml> file, in addition to annotations on <verbatim|let rec>
+  nodes:
+
+  <\code>
+    $ ./invargent -inform -full_annot examples/equal_assert.gadt
+
+    File "examples/equal_assert.gadt", line 20, characters 5-103:
+
+    No answer in type: term abduction failed
+
+    \;
+
+    Perhaps increase the -term_abduction_timeout parameter.
+
+    Perhaps increase the -term_abduction_fail parameter.
+  </code>
+
+  The <verbatim|Perhaps increase> suggestions are generated only when the
+  corresponding limit has actually been exceeded. Remember however that the
+  limits will often be exceeded for erroneus programs which should not
+  type-check. Here the default number of steps till term abduction timeout,
+  which is just <verbatim|700> to speed up failing for actually erroneous
+  programs, is too low. The complete output with timeout increased:
+
+  <\code>
+    $ ./invargent -inform -full_annot -term_abduction_timeout 4000 \\
+    examples/<no-break>equal_assert.gadt
+
+    val equal : <math|\<forall\>>a, b. (Ty a, Ty b) <math|\<rightarrow\>> a
+    <math|\<rightarrow\>> b <math|\<rightarrow\>> Boolean
+
+    InvarGenT: Generated file examples/equal_assert.gadti
+
+    InvarGenT: Generated file examples/equal_assert.ml
+
+    InvarGenT: Command "ocamlc -c examples/equal_assert.ml" exited with code
+    0
+  </code>
+
+  To understand the intent of the solver parameters, we need a rough
+  ``birds-eye view'' understanding of how InvarGenT works. The invariants and
+  postconditions that we solve for are logical formulas and can be ordered by
+  strength. Least Upper Bounds (LUBs) and Greatest Lower Bounds (GLBs)
+  computations are traditional tools used for solving recursive equations
+  over an ordered structure. In case of implicational constraints that are
+  generated for type inference with GADTs, constraint abduction is a form of
+  LUB computation. <em|Disjunction elimination> is our term for computing the
+  GLB wrt. strength for formulas that are conjunctions of atoms. We want the
+  invariants of recursive definitions -- i.e. the types of recursive
+  functions and formulas constraining their type variables -- to be as weak
+  as possible, to make the use of the corresponding definitions as easy as
+  possible. The weaker the invariant, the more general the type of
+  definition. Therefore the use of LUB, constraint abduction. For
+  postconditions -- i.e. the existential types of results computed by
+  <verbatim|efunction> expressions and formulas constraining their type
+  variables -- we want the strongest possible solutions, because stronger
+  postcondition provides more information at use sites of a definition.
+  Therefore we use LUB, disjunction elimination, but only if existential
+  types have been introduced by <verbatim|efunction> or <verbatim|ematch>.
+
+  Below we discuss all of the InvarGenT options.
+
+  <\description>
+    <item*|<verbatim|-inform>>Print type schemes of toplevel definitions as
+    they are inferred.
+
+    <item*|<verbatim|-no_sig>>Do not generate the <verbatim|.gadti> file.
+
+    <item*|<verbatim|-no_ml>>Do not generate the <verbatim|.ml> file.
+
+    <item*|<verbatim|-no_verif>>Do not call <verbatim|ocamlc -c> on the
+    generated <verbatim|.ml> file.
+
+    <item*|<verbatim|-full_annot>>Annotate the <verbatim|function> and
+    <verbatim|let>..<verbatim|in> nodes in generated OCaml code. This
+    increases the burden on inference a bit because the variables associated
+    with the nodes cannot be eliminated from the constraint during initial
+    simplification.
+
+    <item*|<verbatim|-term_abduction_timeout>>Limit on term simple abduction
+    steps (default 700). Simple abduction works with a single implication
+    branch, which roughly corresponds to a single branch -- an execution path
+    -- of the program.
+
+    <item*|<verbatim|-term_abduction_fail>>Limit on backtracking steps in
+    term joint abduction (default 4). Joint abduction combines results for
+    all branches of the constraints.
+
+    <item*|<verbatim|-no_alien_prem>>Do not include alien (e.g. numerical)
+    premise information in term abduction.
+
+    <item*|<verbatim|-early_num_abduction>>Include recursive branches in
+    numerical abduction from the start. By default, in the second iteration
+    of solving constraints, which is the first iteration that numerical
+    abduction is performed, we only pass non-recursive branches to numerical
+    abduction. This makes it faster but less likely to find the correct
+    solution.
+
+    <item*|<verbatim|-num_abduction_rotations>>Numerical abduction:
+    coefficients from <math|\<pm\>1/N> to <math|\<pm\>N> (default 3).
+    Numerical abduction answers are built, roughly speaking, by adding
+    premise equations of a branch with conclusion of a branch to get an
+    equation or inequality that does not conflict with other branches, but is
+    equivalent to the conclusion equation/inequality. This parameter decides
+    what range of coefficients is tried. If the highest coefficient in
+    correct answer is greater, abduction might fail.
+
+    <item*|<verbatim|-num_prune_at>>Keep less than <math|N> elements in
+    abduction sums (default 6). By elements here we mean distinct variables
+    -- lack of constant multipliers in concrete syntax of types is just a
+    syntactic shortcoming.
+
+    <item*|<verbatim|-num_abduction_timeout>>Limit on numerical simple
+    abduction steps (default 1000).
+
+    <item*|<verbatim|-num_abduction_fail>>Limit on backtracking steps in
+    numerical joint abduction (default 10).
+
+    <item*|<verbatim|-disjelim_rotations>>Disjunction elimination: check
+    coefficients from <math|1/N> (default 3). Numerical disjunction
+    elimination is performed by approximately finding the convex hull of the
+    polytopes corresponding to disjuncts. A step in an exact algorithm
+    involves rotating a side along a ridge -- an intersection with another
+    side -- until the side touches yet another side. We approximate by trying
+    out a couple of rotations: convex combinations of the inequalities
+    defining the sides. This parameter decides how many rotations to try.
+
+    <item*|<verbatim|-passing_ineq_trs>>Include inequalities in conclusion
+    when solving numerical abduction. This setting leads to more inequalities
+    being tried for addition in numeric abduction answer.
+
+    <item*|<verbatim|-not_annotating_fun>>Do not keep information for
+    annotating <verbatim|function> nodes. This may allow eliminating more
+    variables during initial constraint simplification.
+
+    <item*|<verbatim|-annotating_letin>>Keep information for annotating
+    <verbatim|let>..<verbatim|in> nodes. Will be set automatically anyway
+    when <verbatim|-full_annot> is passed.
+
+    <item*|<verbatim|-let_in_fallback>>Annotate <verbatim|let>..<verbatim|in>
+    nodes in fallback mode of <verbatim|.ml> generation. When verifying the
+    resulting <verbatim|.ml> file fails, a retry is made with
+    <verbatim|function> nodes annotated. This option additionally annotates
+    <verbatim|let>..<verbatim|in> nodes with types in the regenerated
+    <verbatim|.ml> file.
+  </description>
+
+  Let us see another example where parameters allowing the solver do more
+  work are needed:
+
+  <\code>
+    $ ./invargent -inform -num_abduction_rotations 4 -num_abduction_timeout
+    2000 examples/flatten_quadrs.gadt
+
+    val flatten_quadrs :
+
+    \ \ <math|\<forall\>>n, a. List ((a, a, a, a), n) <math|\<rightarrow\>>
+    List (a, n + n + n + n)
+
+    InvarGenT: Generated file examples/flatten_quadrs.gadti
+
+    InvarGenT: Generated file examples/flatten_quadrs.ml
+
+    InvarGenT: Command "ocamlc -c examples/flatten_quadrs.ml" exited with
+    code 0
+  </code>
+
+  Based on user feedback, we will likely increase the default values of
+  parameters in a future version.
 </body>
 
 <\initial>
@@ -508,14 +698,14 @@
     <associate|auto-17|<tuple|5.1|12|invargent.tm>>
     <associate|auto-18|<tuple|5.2|13|invargent.tm>>
     <associate|auto-19|<tuple|5.3|15|invargent.tm>>
-    <associate|auto-2|<tuple|2|2>>
+    <associate|auto-2|<tuple|2|1>>
     <associate|auto-20|<tuple|5.4|17|invargent.tm>>
     <associate|auto-21|<tuple|5.5|17|invargent.tm>>
     <associate|auto-22|<tuple|6|18|invargent.tm>>
     <associate|auto-23|<tuple|6|18|invargent.tm>>
     <associate|auto-24|<tuple|5.5|17>>
-    <associate|auto-3|<tuple|3|4>>
-    <associate|auto-4|<tuple|4|4>>
+    <associate|auto-3|<tuple|3|5>>
+    <associate|auto-4|<tuple|4|5>>
     <associate|auto-5|<tuple|2.2|4|invargent.tm>>
     <associate|auto-6|<tuple|3|5|invargent.tm>>
     <associate|auto-7|<tuple|3.1|5|invargent.tm>>
@@ -543,9 +733,6 @@
 
 <\auxiliary>
   <\collection>
-    <\associate|bib>
-      InvarGenT
-    </associate>
     <\associate|toc>
       <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|1<space|2spc>Introduction>
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>

examples/flatten_quadrs.gadt

@@ -0,0 +1,11 @@
+newtype Boolean
+newtype List : type * num
+newcons True : Boolean
+newcons False : Boolean
+newcons LNil : ∀a. List(a, 0)
+newcons LCons : ∀n, a [0≤n]. a * List(a, n) ⟶ List(a, n+1)
+
+let rec flatten_quadrs =
+  function LNil -> LNil
+    | LCons ((x, y, z, v), l) ->
+      LCons (x, LCons (y, LCons (z, LCons (v, flatten_quadrs l))))

src/Infer.ml

@@ -660,6 +660,9 @@ let annotate_expr q res_sb chi_sb nice_sb e : texpr =
       and evs2, e2 = aux nice_sb e2 in
       VarSet.union evs1 evs2,
       App (e1, e2, lc)
+    | Lam (_, [cl], loc) when single_assert_false cl ->
+      let evs, cl = aux_cl nice_sb cl in
+      evs, Lam (None, [cl], loc)
     | Lam (ann, cls, lc) ->
       let evs, cls = List.split (List.map (aux_cl nice_sb) cls) in
       let evs = List.fold_left VarSet.union VarSet.empty evs in

src/InvarGenT.ml

@@ -5,6 +5,7 @@
     @author Lukasz Stafiniak lukstafi (AT) gmail.com
     @since Mar 2013
 *)
+let version = "1.0"
 
 (** Annotate [let-in] nodes in fallback mode of .ml generation. *)
 let let_in_fallback = ref false
@@ -88,7 +89,7 @@ let main () =
     "-num_abduction_rotations", Arg.Set_int NumS.abd_rotations,
     "Numerical abduction: coefficients from +/- 1/N to +/- N (default 3)";
     "-num_prune_at", Arg.Set_int NumS.abd_prune_at,
-    "Keep less than N elements in abduction sums (default <6)";
+    "Keep less than N elements in abduction sums (default 6)";
     "-num_abduction_timeout", Arg.Set_int NumS.abd_timeout_count,
     "Limit on numerical simple abduction steps (default 1000)";
     "-num_abduction_fail", Arg.Set_int NumS.abd_fail_timeout_count,
@@ -106,22 +107,23 @@ let main () =
   ] in
   let fname = ref "" in
   let anon_fun f = fname := f in
-  let msg = "Usage: "^Sys.argv.(0)^"[OPTIONS] source_file.gadt" in
+  let msg = "InvarGenT version "^version^
+              ". Usage: "^Sys.argv.(0)^"[OPTIONS] source.gadt" in
   Arg.parse cli anon_fun msg;
   try
     ignore
       (process_file !fname ~do_sig:!do_sig ~do_ml:!do_ml
          ~verif_ml:!verif_ml ~full_annot:!full_annot)
-  with (Report_toplevel _ | Contradiction _) as exn ->
+  with (Report_toplevel _ | Contradiction _ | NoAnswer _) as exn ->
     Format.printf "%a@\n%!" pr_exception exn;
     if !Abduction.abd_timeout_flag then Format.printf
         "Perhaps increase the -term_abduction_timeout parameter.@\n%!";
     if !Abduction.abd_fail_flag then Format.printf
         "Perhaps increase the -term_abduction_fail parameter.@\n%!";
     if !NumS.abd_timeout_flag then Format.printf
-        "Perhaps increase the -term_abduction_timeout parameter.@\n%!";
+        "Perhaps increase the -num_abduction_timeout parameter.@\n%!";
     if !NumS.abd_fail_flag then Format.printf
-        "Perhaps increase the -term_abduction_fail parameter.@\n%!";
+        "Perhaps increase the -num_abduction_fail parameter.@\n%!";
     exit 2
 
 

src/NumS.ml

@@ -591,7 +591,7 @@ let abd_simple cmp cmp_w cmp_v uni_v ~bvs ~discard ~validate
             *]*)
             (* 7c *)
             let ineq_trs =
-              if !passing_ineq_trs
+              if not iseq && !passing_ineq_trs
               then add_ineq_tr ineq_trs a
               else ineq_trs in
             (* 7d *)