diff --git a/Makefile b/Makefile index 50409b4..c327cda 100644 --- a/Makefile +++ b/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 diff --git a/README.md b/README.md index 666936e..9421c87 100644 --- a/README.md +++ b/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`. diff --git a/TODO.md b/TODO.md index 6e3bd7c..8a17f21 100644 --- a/TODO.md +++ b/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. \ No newline at end of file +* 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. \ No newline at end of file diff --git a/doc/invargent-manual.pdf b/doc/invargent-manual.pdf index d84de59..56a9545 100644 Binary files a/doc/invargent-manual.pdf and b/doc/invargent-manual.pdf differ diff --git a/doc/invargent-manual.tm b/doc/invargent-manual.tm index 9d96fc0..d7ed376 100644 --- a/doc/invargent-manual.tm +++ b/doc/invargent-manual.tm @@ -468,7 +468,197 @@ - \; + The default settings of InvarGenT parameters should be sufficient for most + cases. For example, after downloading InvarGenT source code and changing + current directory to , we can enter, assuming a + Unix-like shell: + + <\code> + $ make main + + $ ./invargent examples/binary_upper_bound.gadt + + + To get the inferred types printed on standard output, use the + option: + + <\code> + $ ./invargent -inform examples/binomial_heap_nonrec.gadt + + + In some situations, hopefully unlikely for simple programs, the default + parameters of the solver algorithms do not suffice. Consider this example, + where we use to generate type annotations on + and .. nodes in the + file, in addition to annotations on + 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. + + + The 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 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/equal_assert.gadt + + val equal : >a, b. (Ty a, Ty b) > a + > b > 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 + + + 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. 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 + 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 or . + + Below we discuss all of the InvarGenT options. + + <\description> + >Print type schemes of toplevel definitions as + they are inferred. + + >Do not generate the file. + + >Do not generate the file. + + >Do not call on the + generated file. + + >Annotate the and + .. 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. + + >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. + + >Limit on backtracking steps in + term joint abduction (default 4). Joint abduction combines results for + all branches of the constraints. + + >Do not include alien (e.g. numerical) + premise information in term 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. + + >Numerical abduction: + coefficients from 1/N> to 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. + + >Keep less than 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. + + >Limit on numerical simple + abduction steps (default 1000). + + >Limit on backtracking steps in + numerical joint abduction (default 10). + + >Disjunction elimination: check + coefficients from (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. + + >Include inequalities in conclusion + when solving numerical abduction. This setting leads to more inequalities + being tried for addition in numeric abduction answer. + + >Do not keep information for + annotating nodes. This may allow eliminating more + variables during initial constraint simplification. + + >Keep information for annotating + .. nodes. Will be set automatically anyway + when is passed. + + >Annotate .. + nodes in fallback mode of generation. When verifying the + resulting file fails, a retry is made with + nodes annotated. This option additionally annotates + .. nodes with types in the regenerated + file. + + + 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 : + + \ \ >n, a. List ((a, a, a, a), n) > + 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 + + + Based on user feedback, we will likely increase the default values of + parameters in a future version. <\initial> @@ -508,14 +698,14 @@ > > > - > + > > > > > > - > - > + > + > > > > @@ -543,9 +733,6 @@ <\auxiliary> <\collection> - <\associate|bib> - InvarGenT - <\associate|toc> |math-font-series||1Introduction> |.>>>>|> diff --git a/examples/flatten_quadrs.gadt b/examples/flatten_quadrs.gadt new file mode 100644 index 0000000..f960446 --- /dev/null +++ b/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)))) diff --git a/src/Infer.ml b/src/Infer.ml index d4524ad..c296ea6 100644 --- a/src/Infer.ml +++ b/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 diff --git a/src/InvarGenT.ml b/src/InvarGenT.ml index b6c3b2e..ca59e18 100644 --- a/src/InvarGenT.ml +++ b/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 diff --git a/src/NumS.ml b/src/NumS.ml index c270f4d..1cfb0bc 100644 --- a/src/NumS.ml +++ b/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 *)